Main theorems

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Assembly.Formulas7import SurfaceBlowup.Reciprocity.Main8 9/-!10# Main theorems11 12* `SurfaceBlowup.main_dvr`: for every complete discrete valuation ring `O` with finite residue13  field `k` (any characteristic, any ramification), the monic and projective type densities are the14  values at `q = |k|` of the universal rational expressions `monicExpr n σ`, `projectiveExpr n σ`.15* `SurfaceBlowup.main_field_form`: the rational-function form, for the rings of integers of16  unramified finite extensions `K/ℚ_p` (the published statement).17* `SurfaceBlowup.main_field_form_ramified`: the same for arbitrary finite `K/ℚ_p`.18* `SurfaceBlowup.recip_main` (in `SurfaceBlowup.Reciprocity.Main`): the reciprocity law19  `A_n(q) = B_n(1/q)`, `R_n(1/q) = R_n(q)` of the rational functions.20 21The densities are the original definitions `monicDensity`, `projectiveDensity` of22`SurfaceBlowup.Basic`; the proof runs on the route-F densities `monicDensityF`, `projectiveDensityF`23(`Assembly.Formulas`) and transfers along the Haar-null bridges `orig_monicDensity_eq`,24`orig_projectiveDensity_eq` (`Assembly.NullBridges`).25-/26 27open scoped ENNReal28 29namespace SurfaceBlowup30 31/-- **Main theorem.** Let `O` be a complete discrete valuation ring with finite residue field `k`32(any characteristic, any ramification), with its maximal-ideal-adic compact topology, Borel33σ-algebra and normalized Haar measure. For every degree `n` and every factorization type `σ`,34the probability that a random monic polynomial of degree `n` over `O` (resp. a random primitive35binary form of degree `n`) has type `σ` is the value at `q = |k|` of the universal rational36expression `monicExpr n σ` (resp. `projectiveExpr n σ`).37 38The statement carries no hypotheses on `n` and `σ`: the certified form assumed `0 < n`,39`ValidType σ` and `typeDegree σ = n`, none of which the proof uses. -/40theorem main_dvr (O : Type) [CommRing O] [IsDomain O]Theorem 1.1Remark 1.341    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]42    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]43    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]44    (htop : IsAdic (IsLocalRing.maximalIdeal O))45    (n : ℕ) (σ : FactorType) :46    SurfaceBlowup.monicDensity O n σ =47        densityValue (monicExpr n σ) (Nat.card (IsLocalRing.ResidueField O)) ∧48    SurfaceBlowup.projectiveDensity O n σ =49        densityValue (projectiveExpr n σ) (Nat.card (IsLocalRing.ResidueField O)) := by50  rw [orig_monicDensity_eq O htop, orig_projectiveDensity_eq O htop]51  exact ⟨monicDensityF_eq_densityValue O htop n σ, projectiveDensityF_eq_densityValue O htop n σ⟩52 53/-- **Field form** (unramified `K/ℚ_p`): the densities are values of explicit rational functions54`A = (monicExpr n σ).rational`, `R = (projectiveExpr n σ).rational`, regular at every prime power,55evaluated at the residue cardinality of the ring of integers. -/56theorem main_field_form (n : ℕ) (σ : FactorType) :Theorem 1.157    ∃ A R : RatFunc ℚ, A = (monicExpr n σ).rational ∧ R = (projectiveExpr n σ).rational ∧58      (∀ q : ℕ, PrimePower q → RegularAt A q ∧ RegularAt R q) ∧59      (∀ q : ℕ, PrimePower q → RatFunc.eval (RingHom.id ℚ) q A = (monicExpr n σ).eval q ∧60        RatFunc.eval (RingHom.id ℚ) q R = (projectiveExpr n σ).eval q) ∧61      ∀ (p : ℕ) [Fact p.Prime] (K : Type) [Field K] [Algebra ℚ_[p] K] [Algebra ℤ_[p] K]62        [IsScalarTower ℤ_[p] ℚ_[p] K] [FiniteDimensional ℚ_[p] K]63        [TopologicalSpace (padicIntegers p K)] [IsTopologicalRing (padicIntegers p K)]64        [CompactSpace (padicIntegers p K)] [T2Space (padicIntegers p K)]65        [SecondCountableTopology (padicIntegers p K)] [MeasurableSpace (padicIntegers p K)]66        [BorelSpace (padicIntegers p K)],67        PadicUnramified p K → IsAdic (Ideal.span {(p : padicIntegers p K)}) →68          monicDensity (padicIntegers p K) n σ = densityValue (monicExpr n σ)69            (Nat.card (padicIntegers p K ⧸ Ideal.span {(p : padicIntegers p K)})) ∧70          projectiveDensity (padicIntegers p K) n σ = densityValue (projectiveExpr n σ)71            (Nat.card (padicIntegers p K ⧸ Ideal.span {(p : padicIntegers p K)})) ∧72          monicDensity (padicIntegers p K) n σ = ENNReal.ofReal ((RatFunc.eval (RingHom.id ℚ)73            ((Nat.card (padicIntegers p K ⧸ Ideal.span {(p : padicIntegers p K)}) : ℕ) : ℚ) A :74              ℚ) : ℝ) ∧75          projectiveDensity (padicIntegers p K) n σ = ENNReal.ofReal ((RatFunc.eval (RingHom.id ℚ)76            ((Nat.card (padicIntegers p K ⧸ Ideal.span {(p : padicIntegers p K)}) : ℕ) : ℚ) R :77              ℚ) : ℝ) := by78  refine ⟨_, _, rfl, rfl, global_formula_regular n σ, global_rational_eval n σ, ?_⟩79  intro p _ K _ _ _ _ _ _ _ _ _ _ _ _ hun had80  have hdvr := padicIntegers_isDVR p K81  have := padicIntegers_maximal_adic_complete p K hdvr82  have := padicIntegers_residueField_finite p K hdvr83  have hmax : IsLocalRing.maximalIdeal (padicIntegers p K) = Ideal.span {(p : padicIntegers p K)} :=84    hun.maximalIdeal_eq85  have hcard : Nat.card (IsLocalRing.ResidueField (padicIntegers p K)) =86      Nat.card (padicIntegers p K ⧸ Ideal.span {(p : padicIntegers p K)}) :=87    Nat.card_congr (Ideal.quotEquivOfEq hmax).toEquiv88  obtain ⟨h1, h2⟩ := main_dvr (padicIntegers p K) (hmax ▸ had) n σ89  rw [hcard] at h1 h290  obtain ⟨e1, e2⟩ := global_rational_eval n σ _ (hcard ▸ finite_field_card_primePower _)91  exact ⟨h1, h2, by rw [h1, e1], by rw [h2, e2]⟩92 93/-- **Field form, arbitrary finite `K/ℚ_p`** (ramified allowed): with the maximal-ideal-adic compact94topology on the ring of integers `𝒪_K = padicIntegers p K`, the monic and projective type densities95are the values at `q = |𝒪_K/𝔪|` of the rational functions `(monicExpr n σ).rational`,96`(projectiveExpr n σ).rational`. -/97theorem main_field_form_ramified (n : ℕ) (σ : FactorType) (p : ℕ) [Fact p.Prime] (K : Type)Theorem 1.198    [Field K] [Algebra ℚ_[p] K] [Algebra ℤ_[p] K] [IsScalarTower ℤ_[p] ℚ_[p] K]99    [FiniteDimensional ℚ_[p] K]100    [TopologicalSpace (padicIntegers p K)] [IsTopologicalRing (padicIntegers p K)]101    [CompactSpace (padicIntegers p K)] [T2Space (padicIntegers p K)]102    [SecondCountableTopology (padicIntegers p K)] [MeasurableSpace (padicIntegers p K)]103    [BorelSpace (padicIntegers p K)]104    (had : letI := padicIntegers_isDVR p K; IsAdic (IsLocalRing.maximalIdeal (padicIntegers p K))) :105    letI := padicIntegers_isDVR p K106    monicDensity (padicIntegers p K) n σ = ENNReal.ofReal ((RatFunc.eval (RingHom.id ℚ)107        (Nat.card (IsLocalRing.ResidueField (padicIntegers p K)) : ℚ) (monicExpr n σ).rational :108          ℚ) : ℝ) ∧109      projectiveDensity (padicIntegers p K) n σ = ENNReal.ofReal ((RatFunc.eval (RingHom.id ℚ)110        (Nat.card (IsLocalRing.ResidueField (padicIntegers p K)) : ℚ)111          (projectiveExpr n σ).rational : ℚ) : ℝ) := by112  let hdvr := padicIntegers_isDVR p K113  have := padicIntegers_maximal_adic_complete p K hdvr114  have := padicIntegers_residueField_finite p K hdvr115  obtain ⟨h1, h2⟩ := main_dvr (padicIntegers p K) had n σ116  obtain ⟨e1, e2⟩ := global_rational_eval n σ _117    (finite_field_card_primePower (IsLocalRing.ResidueField (padicIntegers p K)))118  exact ⟨by rw [h1, e1], by rw [h2, e2]⟩119 120end SurfaceBlowup