The density formulas for the route-F densities

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.MonicCells7import SurfaceBlowup.Assembly.NullBridges8import SurfaceBlowup.Assembly.TypeEvents9import SurfaceBlowup.Formula.PatternCounts10import SurfaceBlowup.Formula.StateCombinatorics11import SurfaceBlowup.Formula.TypeTransport12import SurfaceBlowup.Measure.MemberCharts13import SurfaceBlowup.Measure.PrimitiveLocus14import SurfaceBlowup.Recursion.RootCellLaw15import SurfaceBlowup.Unramified.FrobeniusDescent16 17/-!18# The density formulas for the route-F densities19 20For every complete DVR `O` with finite residue field `k` (any characteristic), the route-F21densities `monicDensityF`, `projectiveDensityF` (type predicates carrying the integral-closure22finiteness conjunct) are the values at `q = |k|` of `monicExpr n σ` and `projectiveExpr n σ`.23 24## Main results25 26* `SurfaceBlowup.monicDensityF_eq_densityValue`: the monic density formula.27* `SurfaceBlowup.projectiveDensityF_eq_densityValue`: the projective density formula.28 29## Implementation notes30 31The monic formula sums the root-cell law `root_cell_law` over the residue-divisor partition of the32coefficient space; the projective formula reduces to the affine one off the Haar-null hyperplane33`{a_n = 0}`. `Main.lean` transfers both to the original densities.34 35Provenance: `Thm_Gen_MainDvr` (`SurfaceBlowupV2Gen.{monic,projective}_formula_dvr`, route-F copies36of the accepted `Thm_SurfaceBlowupV2_{monic,projective}_formula_of_root_cell_law`).37-/38 39open scoped BigOperators ENNReal40 41namespace SurfaceBlowup42 43variable (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]44  [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]45  [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]46  [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]47 48/-- **Monic formula** for the route-F density: `monicDensityF O n σ = monicExpr n σ` evaluated at49`q = |k|`. -/50theorem monicDensityF_eq_densityValue (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ)(7.3)51    (σ : FactorType) :52    monicDensityF O n σ = densityValue (monicExpr n σ) (Nat.card (IsLocalRing.ResidueField O)) := by53  classical54  set k := IsLocalRing.ResidueField O55  set q := Nat.card k56  have hq2 : 2 ≤ q := Finite.one_lt_card57  set μ := coefficientMeasure O n58  set E := typeEvent O n σ59  have hE : MeasurableSet E :=60    monic_type_event_measurable_of_root_cell_law root_cell_law O htop n σ61  obtain ⟨⟨S, hS⟩, _, hcell, hsum⟩ := monic_cells_partition O htop n62  -- nonnegativity of array laws63  have hA : ∀ m : Pattern n, 0 ≤ (lawCoeff (arrayLaw m) σ).eval (q : ℚ) := by64    refine fun m ↦ (law_coeff_nonneg_closure (q : ℚ)).2.2.1 _ (fun L hL τ ↦ ?_) σ65    simp only [List.mem_map, otherChildren, List.mem_flatMap, List.mem_replicate] at hL66    obtain ⟨z, ⟨ij, -, -, rfl⟩, rfl⟩ := hL67    exact (state_law_coeff_nonneg q (finite_field_card_primePower k) _68      (show State.Valid (.single 1 _) from ⟨Nat.one_pos, Nat.succ_pos _⟩) τ).2 _ (Nat.succ_pos _)69  -- count70  have hC : ∀ m ∈ residuePatterns n, ((divisorCount 0 m).eval (q : ℚ) : ℝ)71      = ((S.filter fun D => HasArray k n D m).card : ℝ) := by72    intro m hm73    rw [← (affine_divisor_count k n m hm).2, Nat.subtype_card (S.filter fun D ↦ HasArray k n D m)74      fun D ↦ by simp only [Finset.mem_filter, hS]; exact Iff.rfl]75    simp76  -- measure side77  have hmeas : μ E = ∑ m ∈ residuePatterns n, ((S.filter fun D => HasArray k n D m).card : ℝ≥0∞) *78      ((q : ℝ≥0∞)⁻¹ ^ n * densityValue (lawCoeff (arrayLaw m) σ) q) := by79    rw [hsum S hS E hE]80    have h1 : ∀ D ∈ S, μ (E ∩ residueCell O n (divisorAffinePolynomial k D)) =81        ∑ m ∈ residuePatterns n, if HasArray k n D m then82          (q : ℝ≥0∞)⁻¹ ^ n * densityValue (lawCoeff (arrayLaw m) σ) q else 0 := by83      intro D hD84      have hD' := (hS D).1 hD85      obtain ⟨⟨m0, hm0, hm0R⟩, huniq⟩ := divisor_array_exists_unique k n D hD'.286      rw [Finset.sum_eq_single_of_mem m0 hm0R fun m _ hne ↦ if_neg fun h ↦ hne (huniq _ _ h hm0),87        if_pos hm0, (hcell D hD').2.2 E,88        (monic_cell_law root_cell_law O htop n D hD' m0 hm0 σ).2]89    rw [Finset.sum_congr rfl h1, Finset.sum_comm]90    exact Finset.sum_congr rfl fun m _ ↦ by rw [← Finset.sum_filter, Finset.sum_const, nsmul_eq_mul]91  -- law side92  have hlaw : densityValue (monicExpr n σ) q = ∑ m ∈ residuePatterns n,93      ENNReal.ofReal ((divisorCount 0 m).eval (q : ℚ) : ℝ) *94      ((q : ℝ≥0∞)⁻¹ ^ n * densityValue (lawCoeff (arrayLaw m) σ) q) := by95    have hev : (monicExpr n σ).eval (q : ℚ) = (Expr.inv (.pow .var n)).eval (q : ℚ) *96        ∑ m ∈ residuePatterns n, (divisorCount 0 m).eval (q : ℚ) *97          (lawCoeff (arrayLaw m) σ).eval (q : ℚ) := by98      rw [monicExpr, globalLaw, law_coeff_scale, (law_coeff_flatMap _ _ _ [] [] σ _).2.2,99        ← Finset.sum_map_toList]100      simp only [Bool.false_eq_true, if_false]101      congr 2102      exact List.map_congr_left fun m _ ↦ by rw [law_coeff_scale]; rfl103    have hinv0 : 0 ≤ (Expr.inv (.pow .var n)).eval ((q : ℕ) : ℚ) := by104      have : ∀ j : ℕ, (Expr.pow .var j).eval ((q : ℕ) : ℚ) = (q : ℚ) ^ j := by105        intro j; induction j with106        | zero => rfl107        | succ j ih => simp [Expr.pow, Expr.eval, ih, pow_succ]108      simp only [Expr.eval, this]; positivity109    have hc0 : ∀ m ∈ residuePatterns n, 0 ≤ (divisorCount 0 m).eval (q : ℚ) := fun m hm ↦ by110      rw [← (affine_divisor_count k n m hm).2]; positivity111    have hinv := (density_value_arith q hq2 _ _ hinv0 hinv0 n (.single 1 1)112      ⟨Nat.one_pos, Nat.one_pos⟩).2.2.1113    rw [← hinv, densityValue, densityValue, hev, Rat.cast_mul, Rat.cast_sum,114      ENNReal.ofReal_mul (by exact_mod_cast hinv0),115      ENNReal.ofReal_sum_of_nonneg (fun m hm => by116        have := hc0 m hm; have := hA m; push_cast; positivity), Finset.mul_sum]117    refine Finset.sum_congr rfl fun m hm => ?_118    rw [Rat.cast_mul, ENNReal.ofReal_mul (by exact_mod_cast hc0 m hm)]119    ring120  change μ E = _121  rw [hmeas, hlaw]122  exact Finset.sum_congr rfl fun m hm ↦ by rw [hC m hm, ENNReal.ofReal_natCast]123 124/-- **Projective formula** for the route-F density: `projectiveDensityF O n σ = projectiveExpr n σ`125at `q = |k|`. -/126theorem projectiveDensityF_eq_densityValue (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ)(7.3)127    (σ : FactorType) :128    projectiveDensityF O n σ =129      densityValue (projectiveExpr n σ) (Nat.card (IsLocalRing.ResidueField O)) := by130  obtain ⟨hHm, hH0⟩ := coordinate_hyperplane_null O htop (n+1) (Fin.last n)131  rw [projectiveDensityF, ← (affine_type_event_primitive_density root_cell_law O htop n σ).2,132    ← (binary_type_event_decomposition O σ).1 n]133  congr 1134  change coefficientMeasure O (n+1) (binaryTypeEvent O n σ) = _135  rw [← MeasureTheory.measure_inter_add_sdiff _ hHm,136    MeasureTheory.measure_mono_null Set.inter_subset_right hH0, zero_add, Set.sdiff_eq]137  rfl138 139end SurfaceBlowup