Theorem 1.1, cluster clause

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.Cluster.Defs7import SurfaceBlowup.Main8 9/-!10# Theorem 1.1, cluster clause11 12* `SurfaceBlowup.main_dvr_cluster`: over every complete DVR with finite residue field of size `q`,13  the cluster probability of type `σ` is `B_{n,σ}(q)`.14* `SurfaceBlowup.clusterDensity_eq_etale`: the cluster probability is unchanged when the event is15  restricted to separable polynomials (the étale convention).16* `SurfaceBlowup.cluster_formula_regular`: `B_{n,σ}` is regular at every prime power.17* `SurfaceBlowup.recip_cluster`: `A_n(q) = B_n(1/q)` in the paper's notation.18 19The cluster cell `(πO)^n` is the image of `Oⁿ` under `z ↦ π • z`, which scales the coefficient20measure by `q⁻ⁿ` (`scaling_image_borel_mass`); on it the published type event agrees with the21route-F event off the Haar-null inseparable locus (`monic_inseparable_null`), and the route-F22event is the image of the root event, whose mass is the root cell law `root_cell_law`.23-/24 25namespace SurfaceBlowup26 27open scoped ENNReal28open MeasureTheory29 30/-- The monic polynomial of degree `0` has type `σ` iff `σ = 0`. -/31private theorem hasPolynomialType_one_iff (O : Type) [CommRing O] [IsDomain O] (σ : FactorType) :32    HasPolynomialType O 1 σ ↔ σ = 0 := by33  constructor34  · rintro ⟨gs, hirr, -, hprod, rfl⟩35    cases gs with36    | nil => rfl37    | cons g gs =>38      exfalso39      have hg : g ∣ (g :: gs).prod := List.dvd_prod List.mem_cons_self40      rw [← hprod] at hg41      exact (hirr g List.mem_cons_self).2.not_isUnit (isUnit_of_dvd_one hg)42  · rintro rfl43    exact ⟨[], by simp, List.Pairwise.nil, by simp, rfl⟩44 45/-- The cluster cell is the image of `Oⁿ` under scaling by a uniformizer. -/46private theorem clusterCell_eq_image (O : Type) [CommRing O] [IsDomain O]47    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (n : ℕ) :48    clusterCell O n = (fun z : Fin n → O => pi • z) '' Set.univ := by49  have hI := (IsDiscreteValuationRing.irreducible_iff_uniformizer pi).1 hpi50  ext a51  simp only [clusterCell, hI, Ideal.mem_span_singleton', Set.mem_ofPred_eq, Set.image_univ,52    Set.mem_range]53  constructor54  · intro h55    choose z hz using h56    exact ⟨z, funext fun j => by simp [mul_comm, ← hz j]⟩57  · rintro ⟨z, rfl⟩ j58    exact ⟨z j, by simp [mul_comm]⟩59 60/-- On the cluster cell, the route-F type event is the scaling image of the root event. -/61private theorem clusterCell_inter_eq_image (O : Type) [CommRing O] [IsDomain O]62    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (n : ℕ) (σ : FactorType) :63    clusterCell O n ∩ {a | HasPolynomialTypeF O (monicPolynomial O a) σ} =64      (fun z : Fin n → O => pi • z) ''65        {z | HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ} := by66  rw [clusterCell_eq_image O pi hpi n]67  ext a68  constructor69  · rintro ⟨⟨z, -, rfl⟩, h⟩70    exact ⟨z, h, rfl⟩71  · rintro ⟨z, h, rfl⟩72    exact ⟨⟨z, trivial, rfl⟩, h⟩73 74/-- **Theorem 1.1, cluster clause.** Over every complete DVR with finite residue field of size75`q`, the cluster probability of type `σ` is `B_{n,σ}(q)`. -/76theorem main_dvr_cluster (O : Type) [CommRing O] [IsDomain O]Theorem 1.1Remark 1.377    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]78    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]79    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]80    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) (σ : FactorType) :81    clusterDensity O n σ =82      densityValue (clusterExpr n σ) (Nat.card (IsLocalRing.ResidueField O)) := by83  have hprob := coefficient_measure_probability O htop n84  rcases Nat.eq_zero_or_pos n with rfl | hn85  · have hC : clusterCell O 0 = Set.univ := Set.eq_univ_of_forall fun _ i => i.elim086    have hE : {a : Fin 0 → O | HasPolynomialType O (monicPolynomial O a) σ} =87        if σ = 0 then Set.univ else ∅ := by88      ext a89      have h1 : monicPolynomial O a = 1 := by simp [monicPolynomial]90      rw [Set.mem_ofPred_eq, h1, hasPolynomialType_one_iff]91      split_ifs with h <;> simp [h]92    rw [clusterDensity, hC, hE, clusterExpr, rootLaw, if_pos rfl]93    by_cases hσ : σ = 094    · subst hσ95      simp [lawCoeff, lawOne, Expr.sum, densityValue, Expr.eval]96    · rw [if_neg hσ]97      simp [lawCoeff, lawOne, Expr.sum, densityValue, Expr.eval, Ne.symm hσ]98  · obtain ⟨pi, hpi⟩ := IsDiscreteValuationRing.exists_irreducible O99    obtain ⟨hR1, hR2⟩ := root_cell_law O htop pi hpi n hn σ100    obtain ⟨-, hU2⟩ := scaling_image_borel_mass O htop pi hpi n Set.univ MeasurableSet.univ101    obtain ⟨-, hT2⟩ := scaling_image_borel_mass O htop pi hpi n _ hR1102    have hae : (clusterCell O n ∩ {a | HasPolynomialType O (monicPolynomial O a) σ} :103        Set (Fin n → O)) =ᵐ[coefficientMeasure O n]104        (clusterCell O n ∩ {a | HasPolynomialTypeF O (monicPolynomial O a) σ} :105          Set (Fin n → O)) :=106      (measure_eq_zero_iff_ae_notMem.1 (monic_inseparable_null O htop n)).mono fun _ ha =>107        propext <| and_congr_right fun _ =>108          (hasPolynomialTypeF_iff_of_separable O (not_not.1 ha)).symm109    have hc0 : (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ n ≠ 0 :=110      pow_ne_zero _ (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))111    have hct : (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ n ≠ ⊤ :=112      ENNReal.pow_ne_top (ENNReal.inv_ne_top.2 (by exact_mod_cast Nat.card_pos.ne'))113    rw [clusterDensity, measure_congr hae, clusterCell_inter_eq_image O pi hpi n σ, hT2,114      clusterCell_eq_image O pi hpi n, hU2, measure_univ, ENNReal.mul_div_mul_left _ _ hc0 hct,115      div_one, hR2, clusterExpr, rootLaw, if_neg hn.ne']116 117/-- The cluster probability is unchanged by restricting the event to separable polynomials118(the étale convention). -/119theorem clusterDensity_eq_etale (O : Type) [CommRing O] [IsDomain O]Theorem 1.1Remark 1.3120    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]121    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]122    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]123    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) (σ : FactorType) :124    clusterDensity O n σ =125      coefficientMeasure O n (clusterCell O n ∩126        {a | (monicPolynomial O a).Separable ∧ HasPolynomialType O (monicPolynomial O a) σ}) /127        coefficientMeasure O n (clusterCell O n) :=128  congrArg (· / _) <| measure_congr <|129    (measure_eq_zero_iff_ae_notMem.1 (monic_inseparable_null O htop n)).mono fun _ ha =>130      propext <| and_congr_right fun _ => (and_iff_right (not_not.1 ha)).symm131 132/-- `B_{n,σ}` is regular at every prime power. -/133theorem cluster_formula_regular (n : ℕ) (σ : FactorType) :Theorem 1.1134    ∀ q : ℕ, PrimePower q → RegularAt (clusterExpr n σ).rational q := by135  intro q hq136  have hL : LawSafe (rootLaw n) := by137    unfold rootLaw138    split_ifs with h139    · intro z hz q _140      simp only [lawOne, List.mem_singleton] at hz141      subst hz142      trivial143    · exact local_law_safe _ ⟨Nat.one_pos, Nat.pos_of_ne_zero h⟩144  refine expression_regular _ _ (expression_sum_safe _ _ fun x hx => ?_)145  obtain ⟨z, hz, rfl⟩ := List.mem_map.mp hx146  by_cases h : z.1 = σ147  · simp only [h, if_true]; exact hL z hz q (prime_power_ge_two q hq)148  · simp [h, Expr.safe]149 150/-- Reciprocity in the paper's notation: `A_n(q) = B_n(1/q)` (restates `recip_main`). -/151theorem recip_cluster (n : ℕ) (hn : 0 < n) (σ : FactorType) :152    (monicExpr n σ).rational = ((clusterExpr n σ).subst (.inv .var)).rational :=153  (recip_main n hn σ).1154 155end SurfaceBlowup