Strict-transform measures, type events and the projective null bridge

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.Measure.Haar7 8/-!9# Strict-transform measures, type events and the projective null bridge10 11This file computes the Haar measure of preimages under the strict-transform chart maps of the12blow-up recursion: the scaled strict map multiplies measure by `q^(a n + k)` (`q` the residue13field cardinality), the child coordinate map by a further `q⁻¹^n`, and on the ball of radius14`|pi|^(s+a-1)` the net factor is `q⁻¹^(tri d)`. It then defines the coefficient-space type15events and the `RootCellLaw` interface consumed by the density assembly, and proves that the16original monic and projective densities agree with the route-F ones: the numerator events differ17only on the Haar-null inseparable locus (and `{a_n = 0}` in the projective case).18 19## Main results20 21* `SurfaceBlowup.strict_normalizer_preimage_measure`,22  `SurfaceBlowup.child_coordinate_preimage_measure`,23  `SurfaceBlowup.strict_chart_one_ball_measure`, `SurfaceBlowup.strict_transform_translate_measure`24* `SurfaceBlowup.RootCellLaw`, `SurfaceBlowup.typeEvent`, `SurfaceBlowup.binaryTypeEvent`,25  `SurfaceBlowup.affineTypeEvent`, `SurfaceBlowup.HasArray`, `SurfaceBlowup.arrayLaw`26* `SurfaceBlowup.orig_monicDensity_eq`, `SurfaceBlowup.orig_projectiveDensity_eq`27 28Provenance: `Thm_SurfaceBlowupV2_{strict_normalizer_preimage_measure,29child_coordinate_preimage_measure, strict_chart_one_ball_measure,30strict_transform_translate_measure}`,31`Def_SurfaceBlowupV2_{RootCellLaw, TypeEvents}`, `Thm_Gen_ProjBridge`.32-/33 34noncomputable section35 36namespace SurfaceBlowup37 38/-! ### Measures of strict-transform preimages -/39 40section StrictMeasures41 42open scoped BigOperators ENNReal43 44/-- The scaled strict map multiplies Haar measure by `q^(a n + k)`, where `q` is the residue45field cardinality and `k` the length of the cokernel of the normalizer's linear part. -/46theorem strict_normalizer_preimage_measure (O R : Type) [CommRing O] [CommRing R] [Algebra O R]47    (n : ℕ) (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))48    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (H : (Fin n → O) →ₗ[O] R) (k : ℕ)49    (ha : k < a) (Q : (Fin n → O) →ₗ[O] (Fin n → O))50    (hQ : ∀ w, normalizationLinearPart E H (Q w) = (pi ^ k) • w)51    (hD : Function.Injective (normalizationLinearPart E H)) [IsDomain O]52    [IsDiscreteValuationRing O] [Finite (IsLocalRing.ResidueField O)] (hpi : Irreducible pi)53    (hk : Module.length O ((Fin n → O) ⧸ LinearMap.range (normalizationLinearPart E H)) = k)54    [IsAdicComplete (Ideal.span {pi}) (Fin n → O)] [TopologicalSpace (Fin n → O)]55    [IsTopologicalAddGroup (Fin n → O)] [CompactSpace (Fin n → O)] [T2Space (Fin n → O)]56    [MeasurableSpace (Fin n → O)] [BorelSpace (Fin n → O)] [MeasurableAdd (Fin n → O)]57    (hgen : ‹MeasurableSpace (Fin n → O)› = adicCylinderSpace (Ideal.span {pi}) (Fin n → O))58    (mu : MeasureTheory.Measure (Fin n → O)) [MeasureTheory.IsProbabilityMeasure mu]59    [MeasureTheory.Measure.IsAddHaarMeasure mu]60    (hfinite : ∀ j, Finite (AdicQuotient (Ideal.span {pi}) (Fin n → O) j))61    (hcont : Continuous (fun z : Fin n → O => (pi^a) • normalizationLinearPart E H z))62    (T : Set (Fin n → O)) (hT : MeasurableSet T) :63    mu (scaledStrictMap pi a b E H ⁻¹' T) =64      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)^(a*n + k) *65        mu (T ∩ Set.range (scaledStrictMap pi a b E H)) := by66  set D := normalizationLinearPart E H67  set L : (Fin n → O) →+ (Fin n → O) := ((pi^a) • D).toAddMonoidHom68  have hLm : Measurable (fun z : Fin n → O => (pi^a) • D z) := hcont.measurable69  have h1 : mu (scaledStrictMap pi a b E H ⁻¹' T) = mu (L ⁻¹' T) := by70    rw [← MeasureTheory.Measure.map_apply71        (scaled_strict_map_measurable O R n pi a b E H k ha Q hQ hgen hcont) hT,72      strict_normalizer_pushforward_linear O R n pi a b E H k ha Q hQ hgen mu hfinite hLm,73      MeasureTheory.Measure.map_apply hLm hT]74    rfl75  have hidx' : L.range.index = (Nat.card (IsLocalRing.ResidueField O))^(a*n + k) := by76    rw [show L.range = (LinearMap.range ((pi^a) • D)).toAddSubgroup by ext x; simp [L],77      scaled_linear_image_index O pi hpi n a k D hk]78  have : L.range.FiniteIndex := ⟨by rw [hidx']; exact pow_ne_zero _ Nat.card_pos.ne'⟩79  have : Finite ((Fin n → O) ⧸ L.range) := AddSubgroup.finite_quotient_of_finiteIndex80  have hinj : Function.Injective L := fun z w hzw =>81    hD (smul_right_injective (Fin n → O) (pow_ne_zero a hpi.ne_zero) hzw)82  have h2 := compact_injective_image_measure (Fin n → O) (Fin n → O) L hcont hinj mu mu83    (L ⁻¹' T)84  rw [Set.image_preimage_eq_inter_range, hidx'] at h285  push_cast at h286  have hRL : Set.range L = Set.range (scaledStrictMap pi a b E H) := by87    rw [strict_normalizer_lattice_image O R n pi a b E H k ha Q hQ]; rfl88  rw [h1, ← hRL, h2, ← mul_assoc, ENNReal.mul_inv_cancel, one_mul]89  · simp [Nat.card_pos.ne']90  · simp91 92/-- Membership in `(π)^j • M` means divisibility by `π^j`. -/93private theorem mem_span_pow_smul_top_iff {O M : Type} [CommRing O] [AddCommGroup M] [Module O M]94    (pi : O) (j : ℕ) (x : M) :95    x ∈ (Ideal.span {pi} ^ j • ⊤ : Submodule O M) ↔ ∃ y : M, pi ^ j • y = x := by96  rw [Ideal.span_singleton_pow, Submodule.ideal_span_singleton_smul,97    Submodule.mem_smul_pointwise_iff_exists]98  simp99 100/-- A set stable under translation by `pi^j M` is measurable for the adic cylinder σ-algebra. -/101private theorem measurableSet_of_adic_invariant {O M : Type} [CommRing O] [AddCommGroup M]102    [Module O M] [m : MeasurableSpace M] (pi : O)103    (hgen : m = adicCylinderSpace (Ideal.span {pi}) M) (j : ℕ)104    [Finite (AdicQuotient (Ideal.span {pi}) M j)] (S : Set M)105    (hS : ∀ x ∈ S, ∀ y, y - x ∈ (Ideal.span {pi} ^ j • ⊤ : Submodule O M) → y ∈ S) :106    MeasurableSet S := by107  set P := (Ideal.span {pi} ^ j • ⊤ : Submodule O M)108  have hSeq : S = ⋃ c ∈ (Submodule.Quotient.mk (p := P)) '' S,109      (Submodule.Quotient.mk (p := P)) ⁻¹' {c} := by110    ext y111    simp only [Set.mem_iUnion, Set.mem_preimage, Set.mem_singleton_iff, Set.mem_image,112      exists_prop]113    refine ⟨fun hy => ⟨_, ⟨y, hy, rfl⟩, rfl⟩, ?_⟩114    rintro ⟨_, ⟨x, hx, rfl⟩, h⟩115    exact hS x hx y ((Submodule.Quotient.eq P).1 h)116  rw [hSeq]117  refine MeasurableSet.biUnion (Set.to_countable _) ?_118  rintro _ ⟨x, -, rfl⟩119  have : (Submodule.Quotient.mk (p := P)) ⁻¹' {Submodule.Quotient.mk x} =120      {y | adicCongr (Ideal.span {pi}) j y x} := by121    ext y; simp [adicCongr, Submodule.Quotient.eq, P]122  rw [this, hgen]123  exact MeasurableSpace.measurableSet_generateFrom (Or.inr ⟨j, x, rfl⟩)124 125/-- Multiplication by `π` maps the ball of radius `j` around `x` onto the ball of radius `j + 1`126around `π x`. -/127private theorem smul_image_adicCongr {O M : Type} [CommRing O] [AddCommGroup M] [Module O M]128    (pi : O) (j : ℕ) (x : M) :129    (fun w : M => pi • w) '' {y | adicCongr (Ideal.span {pi}) j y x}130      = {z | adicCongr (Ideal.span {pi}) (j+1) z (pi • x)} := by131  ext z132  simp only [Set.mem_image, Set.mem_ofPred_eq, adicCongr, mem_span_pow_smul_top_iff]133  constructor134  · rintro ⟨y, ⟨w, hw⟩, rfl⟩135    exact ⟨w, by rw [pow_succ', mul_smul, hw, smul_sub]⟩136  · rintro ⟨w, hw⟩137    refine ⟨x + pi ^ j • w, ⟨w, by abel⟩, ?_⟩138    rw [smul_add, ← mul_smul, ← pow_succ', hw]139    abel140 141/-- Multiplication by `pi` (when injective) maps adic-measurable sets to measurable sets. -/142theorem measurableSet_smul_image {O M : Type} [CommRing O] [AddCommGroup M] [Module O M]143    (pi : O) [MeasurableSpace M]144    (hgen : ‹MeasurableSpace M› = adicCylinderSpace (Ideal.span {pi}) M)145    (hinj : Function.Injective (fun w : M => pi • w)) (S : Set M) (hS : MeasurableSet S) :146    MeasurableSet ((fun w : M => pi • w) '' S) := by147  have hcylm : ∀ j (x : M), MeasurableSet {z | adicCongr (Ideal.span {pi}) j z x} := by148    intro j x149    rw [hgen]150    exact MeasurableSpace.measurableSet_generateFrom (Or.inr ⟨j, x, rfl⟩)151  have huniv : MeasurableSet ((fun w : M => pi • w) '' Set.univ) := by152    have : (Set.univ : Set M) = {y | adicCongr (Ideal.span {pi}) 0 y 0} := by153      ext y; simp [adicCongr]154    rw [this, smul_image_adicCongr pi]155    exact hcylm _ _156  rw [hgen] at hS157  refine MeasurableSpace.generateFrom_induction _158    (fun S _ => MeasurableSet ((fun w : M => pi • w) '' S)) ?_ ?_ ?_ ?_ S hS159  · rintro t (rfl | ⟨j, x, rfl⟩) _160    · simp161    · rw [smul_image_adicCongr pi]; exact hcylm _ _162  · simp163  · intro t _ ht164    rw [Set.compl_eq_univ_sdiff, Set.image_sdiff hinj]165    exact huniv.diff ht166  · intro s _ hs167    rw [Set.image_iUnion]168    exact MeasurableSet.iUnion hs169 170/-- The child coordinate map multiplies Haar measure by `q^(a n + k) q⁻¹^n`. -/171theorem child_coordinate_preimage_measure (O R : Type) [CommRing O] [CommRing R] [Algebra O R]172    (n : ℕ) (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))173    (H : (Fin n → O) →ₗ[O] R) [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (k : ℕ)174    (ha : k < a) (Q : (Fin n → O) →ₗ[O] (Fin n → O))175    (hQ : ∀ w, normalizationLinearPart E H (Q w) = (pi ^ k) • w)176    (hD : Function.Injective (normalizationLinearPart E H)) [IsDomain O]177    [IsDiscreteValuationRing O] [Finite (IsLocalRing.ResidueField O)] (hpi : Irreducible pi)178    (hk : Module.length O ((Fin n → O) ⧸ LinearMap.range (normalizationLinearPart E H)) = k)179    [IsAdicComplete (Ideal.span {pi}) (Fin n → O)] [TopologicalSpace (Fin n → O)]180    [IsTopologicalAddGroup (Fin n → O)] [CompactSpace (Fin n → O)] [T2Space (Fin n → O)]181    [MeasurableSpace (Fin n → O)] [BorelSpace (Fin n → O)] [MeasurableAdd (Fin n → O)]182    (hgen : ‹MeasurableSpace (Fin n → O)› = adicCylinderSpace (Ideal.span {pi}) (Fin n → O))183    (mu : MeasureTheory.Measure (Fin n → O)) [MeasureTheory.IsProbabilityMeasure mu]184    [MeasureTheory.Measure.IsAddHaarMeasure mu]185    (hfinite : ∀ j, Finite (AdicQuotient (Ideal.span {pi}) (Fin n → O) j))186    (hcont : Continuous (fun z : Fin n → O => (pi^a) • normalizationLinearPart E H z))187    (hscale : ∀ (m : ℕ) (S : Set (Fin n → O)), MeasurableSet S →188      mu ((fun w : Fin n → O => (pi^m) • w) '' S) =189        (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^(m*n) * mu S)190    (T : Set (Fin n → O)) (hT : MeasurableSet T) :191    mu (childCoordinateMap pi a b E H ⁻¹' T) =192      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)^(a*n + k) *193        (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^n *194          mu (T ∩ Set.range (childCoordinateMap pi a b E H)) := by195  set s : (Fin n → O) → (Fin n → O) := fun w => pi • w with hs_def196  have hinj : Function.Injective s := smul_right_injective _ hpi.ne_zero197  obtain ⟨-, hrange, hpre⟩ := child_coordinate_map_scaled O R n pi a b E H (by omega) hinj198  have hsmeas : Measurable s := by199    have hm : @Measurable _ _ _ (adicCylinderSpace (Ideal.span {pi}) (Fin n → O)) s := by200      refine measurable_generateFrom ?_201      rintro t (rfl | ⟨j, x, rfl⟩)202      · simp203      · refine measurableSet_of_adic_invariant pi hgen j _ fun w hw y hy => ?_204        change pi • y - x ∈ (Ideal.span {pi} ^ j • ⊤ : Submodule O (Fin n → O))205        rw [show pi • y - x = (pi • w - x) + pi • (y - w) by rw [smul_sub]; abel]206        exact Submodule.add_mem _ hw (Submodule.smul_mem _ _ hy)207    rwa [← hgen] at hm208  have hrs : MeasurableSet (Set.range (scaledStrictMap pi a b E H)) := by209    rw [strict_normalizer_lattice_image O R n pi a b E H k ha Q hQ]210    refine measurableSet_of_adic_invariant pi hgen (a+k) _ ?_211    rintro _ ⟨u, rfl⟩ y hy212    obtain ⟨v, hv⟩ := (mem_span_pow_smul_top_iff pi (a+k) _).1 hy213    refine ⟨u + Q v, ?_⟩214    simp only [map_add, hQ, smul_add, smul_smul, ← pow_add, hv]215    abel216  have hrσ : MeasurableSet (Set.range (childCoordinateMap pi a b E H)) := by217    rw [← Set.preimage_image_eq (Set.range _) hinj, ← hrange]; exact hsmeas hrs218  rw [← hpre T, strict_normalizer_preimage_measure O R n pi a b E H k ha Q hQ hD hpi hk hgen mu219    hfinite hcont _ (measurableSet_smul_image pi hgen hinj T hT), hrange,220    ← Set.image_inter hinj]221  have h1 := hscale 1 _ (hT.inter hrσ)222  simp only [pow_one, one_mul] at h1223  rw [h1, mul_assoc]224 225/-- On the ball of radius `|pi|^(s+a-1)`, the child coordinate preimage of `T` has measure226`q⁻¹^(tri d)` times that of `T` inside the chart image. -/227theorem strict_chart_one_ball_measure (O R : Type) [CommRing O] [CommRing R] [Algebra O R]Theorem 5.1228    (n : ℕ) (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))229    (H : (Fin n → O) →ₗ[O] R) [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (k : ℕ)230    (ha : k < a) (Q : (Fin n → O) →ₗ[O] (Fin n → O))231    (hQ : ∀ w, normalizationLinearPart E H (Q w) = (pi ^ k) • w)232    (hD : Function.Injective (normalizationLinearPart E H)) [IsDomain O]233    [IsDiscreteValuationRing O] [Finite (IsLocalRing.ResidueField O)] (hpi : Irreducible pi)234    (hk : Module.length O ((Fin n → O) ⧸ LinearMap.range (normalizationLinearPart E H)) = k)235    [IsAdicComplete (Ideal.span {pi}) (Fin n → O)] [TopologicalSpace (Fin n → O)]236    [IsTopologicalAddGroup (Fin n → O)] [CompactSpace (Fin n → O)] [T2Space (Fin n → O)]237    [MeasurableSpace (Fin n → O)] [BorelSpace (Fin n → O)] [MeasurableAdd (Fin n → O)]238    (hgen : ‹MeasurableSpace (Fin n → O)› = adicCylinderSpace (Ideal.span {pi}) (Fin n → O))239    (mu : MeasureTheory.Measure (Fin n → O)) [MeasureTheory.IsProbabilityMeasure mu]240    [MeasureTheory.Measure.IsAddHaarMeasure mu]241    (hfinite : ∀ j, Finite (AdicQuotient (Ideal.span {pi}) (Fin n → O) j))242    (hcont : Continuous (fun z : Fin n → O => (pi^a) • normalizationLinearPart E H z))243    (hscale : ∀ (m : ℕ) (S : Set (Fin n → O)), MeasurableSet S →244      mu ((fun w : Fin n → O => (pi^m) • w) '' S) =245        (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^(m*n) * mu S)246    (s d : ℕ) (htri : tri d ≤ s*n) (hkd : k = s*n - tri d) (T : Set (Fin n → O))247    (hT : MeasurableSet T) :248    mu (coordinateScale pi (s+a-1) '' (childCoordinateMap pi a b E H ⁻¹' T)) =249      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^(tri d) *250        mu (T ∩ Set.range (childCoordinateMap pi a b E H)) := by251  have hinj : Function.Injective (fun w : Fin n → O => pi • w) :=252    smul_right_injective _ hpi.ne_zero253  obtain ⟨_, _, hpre⟩ := child_coordinate_map_scaled O R n pi a b E H (by omega) hinj254  have hmeasS : MeasurableSet (childCoordinateMap pi a b E H ⁻¹' T) := by255    rw [← hpre]256    exact scaled_strict_map_measurable O R n pi a b E H k ha Q hQ hgen hcont257      (measurableSet_smul_image pi hgen hinj T hT)258  rw [← show (fun w : Fin n → O => pi^(s+a-1) • w) = coordinateScale pi (s+a-1) from rfl,259    hscale (s+a-1) _ hmeasS, child_coordinate_preimage_measure O R n pi a b E H k ha Q hQ hD hpi260      hk hgen mu hfinite hcont hscale T hT]261  set q : ℝ≥0∞ := (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)262  have hq0 : q ≠ 0 := by simp [q, Nat.card_pos.ne']263  have he : (s+a-1)*n + n = (a*n + k) + tri d := by264    rw [show (s+a-1)*n + n = (s+a-1+1)*n by ring, show s+a-1+1 = s+a by omega, add_mul]; omega265  have hcancel : q^(a*n+k) * q⁻¹^(a*n+k) = 1 := by266    rw [← ENNReal.inv_pow]267    exact ENNReal.mul_inv_cancel (pow_ne_zero _ hq0) (ENNReal.pow_ne_top (ENNReal.natCast_ne_top _))268  calc q⁻¹ ^ ((s + a - 1) * n) * (q ^ (a * n + k) * q⁻¹ ^ n *269          mu (T ∩ Set.range (childCoordinateMap pi a b E H)))270      = (q^(a*n+k) * q⁻¹^(a*n+k)) * q⁻¹^(tri d) *271          mu (T ∩ Set.range (childCoordinateMap pi a b E H)) := by272        rw [mul_assoc (q^(a*n+k)) (q⁻¹^(a*n+k)), ← pow_add, ← he, pow_add]; ring273    _ = _ := by rw [hcancel, one_mul]274 275/-- Translating the strict-transform chart computation: the preimage of a set of chart276coordinates under the strict transform on the ball of radius `|pi|^(s+a-1)` has measure277`q⁻¹^(tri d)` times that of its image under the coordinate ideal map. -/278theorem strict_transform_translate_measure (O R C : Type) [CommRing O] [CommRing R] [CommRing C]279    [Algebra O R] [Algebra O C] (n : ℕ) (pi : O) (s a d : ℕ) (alpha : R →ₐ[O] C) (f : R)280    (g e c : C) (b : Fin n → R) (hf : alpha f = e ^ d * g)281    (hpi : (algebraMap O C pi) ^ s = e ^ d * c)282    (he : Function.Injective (fun z : C => e*z)) (ha : 0 < a)283    (hjac : algebraMap O C pi ∈ Ideal.jacobson (⊥ : Ideal C)) (bc : Fin n → C)284    (E : C ≃ₗ[O] ((Fin n → O) × C)) (hE : ∀ w, E.symm w = divisionMap g bc w)285    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × C)]286    (hΨ : Function.Injective (coordinateIdeal pi g bc)) (k : ℕ) (hk : k < a)287    (Q : (Fin n → O) →ₗ[O] (Fin n → O))288    (hQ : ∀ w, normalizationLinearPart E (pulledVariation alpha c b) (Q w) = (pi^k) • w)289    (hD : Function.Injective (normalizationLinearPart E (pulledVariation alpha c b)))290    [IsDomain O] [IsDiscreteValuationRing O] [Finite (IsLocalRing.ResidueField O)]291    (hpiO : Irreducible pi)292    (hkl : Module.length O ((Fin n → O) ⧸293      LinearMap.range (normalizationLinearPart E (pulledVariation alpha c b))) = k)294    [IsAdicComplete (Ideal.span {pi}) (Fin n → O)] [TopologicalSpace (Fin n → O)]295    [IsTopologicalAddGroup (Fin n → O)] [CompactSpace (Fin n → O)] [T2Space (Fin n → O)]296    [MeasurableSpace (Fin n → O)] [BorelSpace (Fin n → O)] [MeasurableAdd (Fin n → O)]297    (hgen : ‹MeasurableSpace (Fin n → O)› = adicCylinderSpace (Ideal.span {pi}) (Fin n → O))298    (mu : MeasureTheory.Measure (Fin n → O)) [MeasureTheory.IsProbabilityMeasure mu]299    [MeasureTheory.Measure.IsAddHaarMeasure mu]300    (hfinite : ∀ j, Finite (AdicQuotient (Ideal.span {pi}) (Fin n → O) j))301    (hcont : Continuous (fun z : Fin n → O =>302      (pi^a) • normalizationLinearPart E (pulledVariation alpha c b) z))303    (hscale : ∀ (m : ℕ) (S : Set (Fin n → O)), MeasurableSet S →304      mu ((fun w : Fin n → O => (pi^m) • w) '' S) =305        (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^(m*n) * mu S)306    (htri : tri d ≤ s*n) (hkd : k = s*n - tri d) (T : Set (Fin n → O)) (hT : MeasurableSet T) :307    mu (coordinateIdeal pi f b ⁻¹' (strictTransformIdeal alpha e d ⁻¹'308        (coordinateIdeal pi g bc '' T)) ∩ Set.range (coordinateScale pi (s+a-1))) =309      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^(tri d) *310        mu (coordinateIdeal pi g bc ⁻¹' (coordinateIdeal pi g bc '' T ∩311          strictTransformIdeal alpha e d ''312            (coordinateIdeal pi f b '' Set.range (coordinateScale pi (s+a-1))))) := by313  have hcomm := strict_chart_coordinates_commute O R C n pi s a d alpha f g e c b hf hpi he ha314    hjac bc E hE315  have h3 : coordinateIdeal pi g bc ⁻¹' (coordinateIdeal pi g bc '' T ∩316      strictTransformIdeal alpha e d ''317        (coordinateIdeal pi f b '' Set.range (coordinateScale pi (s+a-1)))) =318      T ∩ Set.range (childCoordinateMap pi a bc E (pulledVariation alpha c b)) := by319    ext w320    simp only [Set.mem_preimage, Set.mem_inter_iff, Set.mem_image, Set.mem_range]321    constructor322    · rintro ⟨⟨x, hx, hxw⟩, y, ⟨u, ⟨z, rfl⟩, rfl⟩, hy⟩323      exact ⟨hΨ hxw ▸ hx, z, hΨ ((hcomm z).symm.trans hy)⟩324    · rintro ⟨hw, z, rfl⟩325      exact ⟨⟨_, hw, rfl⟩, _, ⟨_, ⟨z, rfl⟩, rfl⟩, hcomm z⟩326  rw [h3, strict_chart_preimage_set_identity O R C n pi s a d alpha f g e c b hf hpi he ha hjac bc327    E hE hΨ T]328  exact strict_chart_one_ball_measure O C n pi a bc E (pulledVariation alpha c b) k hk Q hQ hD329    hpiO hkl hgen mu hfinite hcont hscale s d htri hkd T hT330 331end StrictMeasures332 333/-! ### The root-cell law interface -/334 335section RootCell336 337open IsLocalRing MeasureTheory338 339/-- `RootCellLaw`: for every complete DVR `O` with finite residue field and a compact adic340Borel structure, every uniformizer `pi`, every `r ≥ 1` and every type `σ`, the event341`{z : Fin r → O | X^r + ∑ (pi z_i) X^i has type σ}` is measurable and has normalized342coefficient Haar mass `coeff_σ(stateLaw (S(1;r)))(q)`, `q = |k|`. It is the interface between the343measured recursion (which proves it) and the polynomial/projective assembly (which consumes it). -/344def RootCellLaw : Prop :=Cluster model and cluster law B_n(7.1)345  ∀ (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]346    [IsAdicComplete (maximalIdeal O) O] [Finite (ResidueField O)] [TopologicalSpace O]347    [IsTopologicalRing O] [CompactSpace O] [T2Space O] [SecondCountableTopology O]348    [MeasurableSpace O] [BorelSpace O],349    IsAdic (maximalIdeal O) → ∀ (pi : O), Irreducible pi → ∀ (r : ℕ), 0 < r → ∀ (σ : FactorType),350      MeasurableSet {z : Fin r → O | HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ} ∧351      coefficientMeasure O r {z : Fin r → O | HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ} =352        densityValue (lawCoeff (stateLaw (State.single 1 r)) σ) (Nat.card (ResidueField O))353 354end RootCell355 356/-! ### Type events -/357 358section TypeEvents359 360open Polynomial IsLocalRing361open scoped BigOperators362 363section364variable (O : Type) [CommRing O] [IsDomain O]365/-- The classical monic type event in degree `n`: coefficient vectors whose monic polynomial has366type `σ`. -/367def typeEvent (n : ℕ) (σ : FactorType) : Set (Fin n → O) :=368  {a | HasPolynomialTypeF O (monicPolynomial O a) σ}369/-- The primitive binary type event (the numerator event of `projectiveDensityF`). -/370def binaryTypeEvent (n : ℕ) (σ : FactorType) : Set (Fin (n+1) → O) :=371  {a | primitive O a ∧ HasBinaryTypeF O a σ}372/-- The affine-chart type event: the top coefficient is nonzero and the monic normalization of the373affine polynomial has classical type `σ`. -/374def affineTypeEvent (n : ℕ) (σ : FactorType) : Set (Fin (n+1) → O) :=375  {a | a (Fin.last n) ≠ 0 ∧ HasPolynomialTypeF O376    (C (algebraMap O (BaseField O) (a (Fin.last n)))⁻¹ * affinePolynomial O a) σ}377/-- The repeated-root event of `RootCellLaw`: `z` with `X^r + ∑ (pi z_i) X^i` of type `σ`. -/378def rootEvent (pi : O) (r : ℕ) (σ : FactorType) : Set (Fin r → O) :=379  {z | HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ}380/-- The infinity block event in reduced coordinates: for the reversed block381`R_b = 1 + ∑ b_j X^(j+1)` (the dehomogenization of the normalized form `insertOne 0 b`), the top382coefficient `b_(r-1)` is nonzero and the monic normalization of `R_b` has type `σ`. -/383def infinityBlockEvent (r : ℕ) (σ : FactorType) : Set (Fin r → O) :=384  {b | (formPoly (insertOne (0 : Fin (r+1)) b)).coeff r ≠ 0 ∧ HasPolynomialTypeF O385    (C (algebraMap O (BaseField O) ((formPoly (insertOne (0 : Fin (r+1)) b)).coeff r))⁻¹ *386      (formPoly (insertOne (0 : Fin (r+1)) b)).map (algebraMap O (BaseField O))) σ}387end388 389section390variable (O : Type) [CommRing O] [IsLocalRing O] (Φ : Polynomial O)391/-- The point chart of a nonrational point: select the block above `θ̄` and translate it to the392`X^r` cell over `O_δ`. -/393def pointChart (r : ℕ) (a : Fin (Φ.natDegree * r) → O) : Fin r → AdjoinRoot Φ :=394  translateBlock O Φ r (selectBlock O Φ r a)395end396 397section398variable (k : Type) [Field k]399/-- `HasArray k n D m`: the divisor `D` has exactly `m (δ-1, r-1)` closed points of degree `δ`400and multiplicity `r`, for all `1 ≤ δ, r ≤ n`; infinity is counted like every other point. -/401def HasArray (n : ℕ) (D : ExceptionalDivisor k) (m : Pattern n) : Prop :=402  ∀ ij : Fin n × Fin n,403    Nat.card {Q : ClosedDirection k // directionDegree k Q = ij.1.val + 1 ∧ D Q = ij.2.val + 1} =404      (m ij).val405/-- An affine divisor of degree `n`: no multiplicity at infinity and total degree `n`. -/406def AffineDivisor (n : ℕ) (D : ExceptionalDivisor k) : Prop :=407  D (infinityDirection k) = 0 ∧ exceptionalDegree k D = n408/-- The residue vector of a divisor in degree `n`: the coefficients of its affine polynomial, read409as a binary form of degree `n` (the multiplicity at infinity is `n - natDegree`). -/410def divisorVector (n : ℕ) (D : ExceptionalDivisor k) : Fin (n+1) → k :=411  fun i => (divisorAffinePolynomial k D).coeff i412end413 414/-- The law attached to an array: the product over its points of the descended repeated-root laws415`T_δ B_r` — the inner factor of `globalLaw`. -/416def arrayLaw {n : ℕ} (m : Pattern n) : Law :=417  lawProd ((otherChildren 1 m).map fun z => lawDescend z.1 (stateLaw z.2))418 419end TypeEvents420 421/-! ### The projective null bridge -/422 423section ProjBridge424 425open MeasureTheory Polynomial426open scoped BigOperators ENNReal427 428variable (O : Type) [CommRing O] [IsDomain O]429 430omit [IsDomain O] in431private theorem affine_natDegree {n : ℕ} (a : Fin (n + 1) → O) (ha : a (Fin.last n) ≠ 0) :432    (affinePolynomial O a).natDegree = n := by433  have hc : (affinePolynomial O a).coeff n = algebraMap O (BaseField O) (a (Fin.last n)) := by434    simp only [affinePolynomial, Polynomial.finsetSum_coeff, Polynomial.coeff_C_mul_X_pow]435    rw [Finset.sum_eq_single (Fin.last n)]436    · simp437    · exact fun i _ hi => if_neg fun h => hi (Fin.ext (by simp [h]))438    · simp439  apply Polynomial.natDegree_eq_of_le_of_coeff_ne_zero440  · exact Polynomial.natDegree_sum_le_of_forall_le _ _ fun i _ =>441      (Polynomial.natDegree_C_mul_X_pow_le _ _).trans (Nat.lt_succ_iff.1 i.2)442  · rw [hc]443    exact fun h => ha (IsFractionRing.injective O (BaseField O) (by rw [h, map_zero]))444 445omit [IsDomain O] in446private theorem affine_snoc_eq {n : ℕ} (a : Fin n → O) :447    affinePolynomial O (Fin.snoc (α := fun _ => O) a 1) = monicPolynomial O a := by448  simp [affinePolynomial, monicPolynomial, Fin.sum_univ_castSucc, add_comm]449 450variable [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]451  [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O] [IsDiscreteValuationRing O]452  [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]453 454private theorem affine_bad_null (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) :455    coefficientMeasure O (n+1) ({a : Fin (n+1) → O | a (Fin.last n) = 0} ∪456      {a | MvPolynomial.eval a (MvPolynomial.map (Int.castRingHom O) (discAffine n)) = 0}) = 0 := by457  refine measure_union_null (coordinate_hyperplane_null O htop (n+1) (Fin.last n)).2 ?_458  obtain ⟨a₀, h₀⟩ := exists_separable_monic O n459  refine coefficientMeasure_zero_null O htop (n+1) _ (Fin.snoc (α := fun _ => O) a₀ 1) ?_460  have hdeg := monic_polynomial_degree O n a₀461  have := resultant_ne_zero_of_separable (monicPolynomial O a₀) n hdeg.2 hdeg.1.ne_zero h₀462  rw [← affine_snoc_eq, affine_resultant_eq] at this463  exact fun h => this (by rw [h, map_zero])464 465/-- The original monic density equals the separable-type monic density: the two events agree466off the Haar-null inseparable locus. -/467theorem orig_monicDensity_eq (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) (σ : FactorType) :Remark 1.3Remark 6.3468    monicDensity O n σ = monicDensityF O n σ :=469  measure_congr <| (measure_eq_zero_iff_ae_notMem.1 (monic_inseparable_null O htop n)).mono470    fun _ ha => propext (hasPolynomialTypeF_iff_of_separable O (not_not.1 ha)).symm471 472/-- The original projective density equals the route-F one: the two numerator events differ473only inside `{a_n = 0} ∪ {disc = 0}`, which is Haar-null. -/474theorem orig_projectiveDensity_eq (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ)Remark 1.3Remark 6.3475    (σ : FactorType) :476    SurfaceBlowup.projectiveDensity O n σ = projectiveDensityF O n σ := by477  refine congrArg (· / _) <| measure_congr <|478    (measure_eq_zero_iff_ae_notMem.1 (affine_bad_null O htop n)).mono fun a ha => ?_479  simp only [Set.mem_union, Set.mem_ofPred_eq, not_or] at ha480  refine propext <| and_congr_right fun _ => and_congr_right fun h1 => and_congr_right fun _ =>481    and_congr_right fun _ => exists_congr fun _ => and_congr_left fun _ => Iff.symm <|482      hasPolynomialTypeF_iff_of_separable O <| Separable.unit_mul483        (isUnit_C.2 <| isUnit_iff_ne_zero.2 (inv_ne_zero (leadingCoeff_ne_zero.2 h1))) <|484      separable_of_resultant _ n (affine_natDegree O a ha.1) h1 ?_485  rw [affine_resultant_eq]486  exact fun h => ha.2 (IsFractionRing.injective O (BaseField O) (by rw [h, map_zero]))487 488end ProjBridge489 490end SurfaceBlowup