Return and exit events of the blowup recursion

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.Recursion.ChildMembers7 8/-!9# Return and exit events of the blowup recursion10 11For a surface universe, the recursion follows an ideal through successive blowups: at a12single state `single a c` it may return to the same state (self cells) `k` times before13exiting through a non-self cell. This file computes the masses of the exit events (in terms14of the exit law and the return weight), proves measurability of all recursion events, shows15that bad exits and never-returning ideals are null, and concludes by strong induction on the16state rank that the law statement holds for every member of a surface universe.17 18## Main results19 20* `exit_cell_type_mass`, `exit_cell_coeff_nonneg`: mass of the type box of an exit cell.21* `exit_event_zero_mass`, `exit_event_succ_mass`, `return_event_mass`: masses of exit and22  return events.23* `recursion_events_measurable`, `bad_exit_null`, `never_return_null`.24* `recursion_crossing_law`, `recursion_single_law`, `universal_law_statement`: the law.25* `type_event_null_difference`, `etale_type_event_measurable`,26  `unramified_generic_fibre_ascent`.27 28Provenance: `Thm_SurfaceBlowupV2_` nodes `exit_cell_type_mass`, `exit_event_succ_mass`,29`recursion_events_measurable`, `bad_exit_null`, `exit_event_zero_mass`,30`recursion_crossing_step`, `return_event_mass`, `never_return_null`, `recursion_single_step`,31`universal_law_statement`, `type_event_null_difference`, `etale_type_event_measurable`,32`unramified_generic_fibre_ascent`.33-/34 35open scoped BigOperators ENNReal TensorProduct36 37namespace SurfaceBlowup38 39/-! ### Exit cells -/40 41private theorem piFinset_sum_reindex (σ : FactorType) (q : ℚ) {m n : ℕ} (h : m = n)42    (a : Fin n → ℕ × Law) :43    (∑ τ ∈ Fintype.piFinset (fun j : Fin m => ((a (Fin.cast h j)).2.map Prod.fst).toFinset),44      (if σ = ∑ j, scaleType (a (Fin.cast h j)).1 (τ j) then45        ∏ j, (lawCoeff (a (Fin.cast h j)).2 (τ j)).eval (q ^ (a (Fin.cast h j)).1) else 0)) =46    ∑ τ ∈ Fintype.piFinset (fun j : Fin n => ((a j).2.map Prod.fst).toFinset),47      (if σ = ∑ j, scaleType (a j).1 (τ j) then48        ∏ j, (lawCoeff (a j).2 (τ j)).eval (q ^ (a j).1) else 0) := by49  subst h; rfl50 51private theorem lawCoeff_lawProd_descend_eval (l : List (ℕ × State)) (hδ : ∀ z ∈ l, 0 < z.1)52    (σ : FactorType) (q : ℚ) :53    (lawCoeff (lawProd (l.map fun z => lawDescend z.1 (stateLaw z.2))) σ).eval q =54    ∑ τ ∈ Fintype.piFinset (fun j : Fin l.length => ((stateLaw (l.get j).2).map Prod.fst).toFinset),55      (if σ = ∑ j, scaleType (l.get j).1 (τ j) then56        ∏ j, (lawCoeff (stateLaw (l.get j).2) (τ j)).eval (q ^ (l.get j).1) else 0) := by57  have h := law_coeff_prod_descend (l.map fun z => (z.1, stateLaw z.2))58    (by intro z hz; obtain ⟨w, hw, rfl⟩ := List.mem_map.1 hz; exact hδ w hw) σ q59  rw [List.map_map] at h60  rw [show ((fun z : ℕ × Law => lawDescend z.1 z.2) ∘ fun z : ℕ × State => (z.1, stateLaw z.2)) =61    (fun z => lawDescend z.1 (stateLaw z.2)) from rfl] at h62  have hl : (l.map fun z => (z.1, stateLaw z.2)).length = l.length := List.length_map _63  have hg : (l.map fun z => (z.1, stateLaw z.2)).get =64      fun j => ((l.get (Fin.cast hl j)).1, stateLaw (l.get (Fin.cast hl j)).2) := by65    funext j; simp66  rw [hg] at h67  rw [h]68  exact piFinset_sum_reindex σ q hl (fun j => ((l.get j).1, stateLaw (l.get j).2))69 70/-- The residue field of the `j`-th child of a cell has cardinality `q ^ δⱼ`. -/71private theorem child_q_eq_pow (U : SurfaceUniverse) (i : U.ι) (c : (U.M i).cellIndex)72    (j : (U.M i).childIdx c) :73    ((U.M (U.child i c j)).q : ℚ) = ((U.M i).q : ℚ) ^ (((U.M i).childList c).get j).1 := by74  rw [U.child_residue i c j]; push_cast; rfl75 76/-- The children of an exit cell have smaller rank, so they satisfy the law statement. -/77private theorem exit_child_law (U : SurfaceUniverse) (i : U.ι)78    (hIH : ∀ i' : U.ι, (U.M i').s.rank < (U.M i).s.rank → U.LawStatement i') (c : U.exitCells i)79    (j : (U.M i).childIdx c.1) : U.LawStatement (U.child i c.1 j) :=80  hIH _ (by81    rw [U.child_state i c.1 j]82    exact nonself_child_rank_lt _ (U.M i).valid _ c.1.1.2 c.2 _ (List.get_mem _ _))83 84/-- The law coefficients of the children of an exit cell, evaluated at `q ^ δⱼ`, are85nonnegative. -/86private theorem exit_child_coeff_nonneg (U : SurfaceUniverse) (i : U.ι)87    (hIH : ∀ i' : U.ι, (U.M i').s.rank < (U.M i).s.rank → U.LawStatement i') (c : U.exitCells i)88    (j : (U.M i).childIdx c.1) (t : FactorType) :89    0 ≤ (lawCoeff (stateLaw (((U.M i).childList c.1).get j).2) t).eval90      (((U.M i).q : ℚ) ^ (((U.M i).childList c.1).get j).1) := by91  have := ((exit_child_law U i hIH c j).1 t).2.192  rwa [U.child_state i c.1 j, child_q_eq_pow] at this93 94/-- The `σ`-coefficient of the product of the descended children laws of an exit cell is95nonnegative. -/96theorem exit_cell_coeff_nonneg (U : SurfaceUniverse) (i : U.ι)97    (hIH : ∀ i' : U.ι, (U.M i').s.rank < (U.M i).s.rank → U.LawStatement i') (c : U.exitCells i)98    (σ : FactorType) :99    0 ≤ (lawCoeff (lawProd (((U.M i).childList c.1).map fun z ↦ lawDescend z.1 (stateLaw z.2)))100      σ).eval ((U.M i).q : ℚ) := by101  rw [lawCoeff_lawProd_descend_eval ((U.M i).childList c.1)102    (fun z hz ↦ children_residue_degree_pos _ _ _ hz)]103  refine Finset.sum_nonneg fun τ _ ↦ ?_104  split_ifs105  exacts [Finset.prod_nonneg fun j _ ↦ exit_child_coeff_nonneg U i hIH c j (τ j), le_rfl]106 107/-- The child box of an exit cell where the `j`-th child terminates with type `τ j` has mass108`P(d) · vol · ∏ⱼ Cⱼ(τ j)`, with `P(d)` the divisor probability of the cell and `Cⱼ` the law109coefficients of the children evaluated at `q ^ δⱼ`. -/110private theorem exit_child_box_mass (U : SurfaceUniverse) (i : U.ι)111    (hnt : (U.M i).s.terminal = false)112    (hIH : ∀ i' : U.ι, (U.M i').s.rank < (U.M i).s.rank → U.LawStatement i') (c : U.exitCells i)113    (τ : (U.M i).childIdx c.1 → FactorType) :114    (U.M i).μ (U.childBox i c.1 (fun j ↦ U.termTypeEvent (U.child i c.1 j) (τ j))) =115      ENNReal.ofReal ((((divisorProbability (U.M i).s ((U.M i).cellDegree c.1)).eval116        ((U.M i).q : ℚ) * (stateVolume (U.M i).s).eval ((U.M i).q : ℚ) *117        ∏ j, (lawCoeff (stateLaw (((U.M i).childList c.1).get j).2) (τ j)).eval118          (((U.M i).q : ℚ) ^ (((U.M i).childList c.1).get j).1) : ℚ)) : ℝ) := by119  have hq : 2 ≤ (U.M i).q := (universe_basic_facts U i).1120  have hL := exit_child_law U i hIH c121  have hsj : ∀ j, (U.M (U.child i c.1 j)).s = (((U.M i).childList c.1).get j).2 :=122    fun j ↦ U.child_state i c.1 j123  -- child volumes `V j` and child law coefficients `C j`, evaluated at `q ^ δⱼ`124  let V : (U.M i).childIdx c.1 → ℚ := fun j ↦ (stateVolume (((U.M i).childList c.1).get j).2).eval125    (((U.M i).q : ℚ) ^ (((U.M i).childList c.1).get j).1)126  let C : (U.M i).childIdx c.1 → ℚ := fun j ↦127    (lawCoeff (stateLaw (((U.M i).childList c.1).get j).2) (τ j)).eval128      (((U.M i).q : ℚ) ^ (((U.M i).childList c.1).get j).1)129  have hC : ∀ j, 0 ≤ C j := fun j ↦ exit_child_coeff_nonneg U i hIH c j (τ j)130  have hV : ∀ j, 0 < V j := by131    intro j132    have hqc : 2 ≤ (U.M (U.child i c.1 j)).q := U.child_residue i c.1 j ▸ hq.trans133      (Nat.le_self_pow (children_residue_degree_pos _ _ _ (List.get_mem _ _)).ne' _)134    have := (density_value_arith _ hqc (.const 1) (.const 1) (by simp [Expr.eval])135      (by simp [Expr.eval]) 0 _ (U.M (U.child i c.1 j)).valid).2.2.2.2.2.2.1136    rwa [hsj j, child_q_eq_pow] at this137  have hmeas : ∀ j, MeasurableSet (U.termTypeEvent (U.child i c.1 j) (τ j)) :=138    fun j ↦ ((hL j).1 (τ j)).1139  have hmu : ∀ j, (U.M (U.child i c.1 j)).μ (U.termTypeEvent (U.child i c.1 j) (τ j)) =140      ENNReal.ofReal (((C j * V j : ℚ)) : ℝ) := by141    intro j142    have e1 : (lawCoeff (stateLaw (U.M (U.child i c.1 j)).s) (τ j)).eval143        ((U.M (U.child i c.1 j)).q : ℚ) = C j := by rw [hsj j, child_q_eq_pow]144    have e2 : (stateVolume (U.M (U.child i c.1 j)).s).eval ((U.M (U.child i c.1 j)).q : ℚ) =145        V j := by rw [hsj j, child_q_eq_pow]146    rw [((hL j).1 (τ j)).2.2, U.volume]147    simp only [densityValue]148    rw [e1, e2, ← ENNReal.ofReal_mul (by exact_mod_cast hC j)]149    push_cast; rfl150  have hqpos : (0 : ℝ) < ((U.M i).q : ℝ) := by exact_mod_cast (show 0 < (U.M i).q by omega)151  -- the volume ratio `q^{-tri d} · ∏ V j / vol = P(d)`152  have hratio : ((U.M i).q : ℚ)⁻¹ ^ tri ((U.M i).cellDegree c.1) * (∏ j, V j) /153      (stateVolume (U.M i).s).eval ((U.M i).q : ℚ) =154      (divisorProbability (U.M i).s ((U.M i).cellDegree c.1)).eval ((U.M i).q : ℚ) := by155    have hprodV : (((U.M i).childList c.1).map fun z ↦156        (stateVolume z.2).eval (((U.M i).q : ℚ) ^ z.1)).prod = ∏ j, V j := by157      rw [← Fin.prod_univ_fun_getElem]; rfl158    rw [← hprodV]159    exact child_volume_ratio (U.M i).s (U.M i).valid c.1.1.1 c.1.1.2 _ hq160  have hVs := (density_value_arith _ hq (.const 1) (.const 1) (by simp [Expr.eval])161      (by simp [Expr.eval]) 0 _ (U.M i).valid).2.2.2.2.2.2.2162  change (U.M i).μ ((U.M i).cell c.1 ∩ U.Φ i c.1 ⁻¹' Set.pi Set.univ _) = _163  rw [U.Φ_measure i hnt c.1 _ hmeas, Finset.prod_congr rfl (fun j _ ↦ hmu j),164    ← ENNReal.ofReal_prod_of_nonneg (fun j _ ↦ by have := hC j; have := hV j; positivity),165    ← ENNReal.ofReal_natCast, ← ENNReal.ofReal_inv_of_pos hqpos,166    ← ENNReal.ofReal_pow (inv_nonneg.2 hqpos.le), ← ENNReal.ofReal_mul (by positivity), ← hratio]167  congr 1168  push_cast169  rw [Finset.prod_mul_distrib]170  field_simp171  exact mul_comm _ _172 173/-- The type-`σ` box of a cell is the disjoint union, over the child types `τ` adding up to `σ`174(with residue scaling), of the child boxes where the `j`-th child terminates with type `τ j`. -/175private theorem typeBox_measure_eq_tsum (U : SurfaceUniverse) (i : U.ι)176    (hnt : (U.M i).s.terminal = false) (c : (U.M i).cellIndex) (σ : FactorType)177    (hmeas : ∀ j t, MeasurableSet (U.termTypeEvent (U.child i c j) t)) :178    (U.M i).μ (U.typeBox i c σ) = ∑' τ : (U.M i).childIdx c → FactorType,179      if σ = ∑ j, scaleType ((U.M i).childDelta c j) (τ j) then180        (U.M i).μ (U.childBox i c (fun j ↦ U.termTypeEvent (U.child i c j) (τ j))) else 0 := by181  unfold SurfaceUniverse.typeBox182  rw [MeasureTheory.measure_iUnion]183  · congr 1; funext τ184    rw [Set.iUnion_eq_if]185    split_ifs186    · rfl187    · exact MeasureTheory.measure_empty188  · intro τ τ' hne189    rw [Function.onFun, Set.disjoint_left]190    intro J hJ hJ'191    simp only [Set.mem_iUnion] at hJ hJ'192    obtain ⟨_, hJ⟩ := hJ193    obtain ⟨_, hJ'⟩ := hJ'194    obtain ⟨j, hj⟩ := Function.ne_iff.1 hne195    have h1 := hJ.2 j (Set.mem_univ j)196    obtain ⟨σ0, -, huniq⟩ := terminates_type_unique U _ _ h1.2197    exact hj ((huniq _ h1.1.2).trans (huniq _ (hJ'.2 j (Set.mem_univ j)).1.2).symm)198  · exact fun τ ↦ MeasurableSet.iUnion fun _ ↦ U.Φ_measurable i hnt c _ fun j ↦ hmeas j (τ j)199 200/-- Mass of the type-`σ` box of a non-self (exit) cell: the divisor probability of the cell201times the `σ`-coefficient of the product of the descended children laws, times the volume of202the state set. -/203theorem exit_cell_type_mass (U : SurfaceUniverse) (i : U.ι) (hnt : (U.M i).s.terminal = false)204    (hIH : ∀ i' : U.ι, (U.M i').s.rank < (U.M i).s.rank → U.LawStatement i') (c : U.exitCells i)205    (σ : FactorType) :206    (U.M i).μ (U.typeBox i c.1 σ) =207      densityValue (.mul (divisorProbability (U.M i).s ((U.M i).cellDegree c.1))208        (lawCoeff (lawProd (((U.M i).childList c.1).map fun z ↦ lawDescend z.1 (stateLaw z.2))) σ))209        (U.M i).q * (U.M i).μ (U.M i).stateSet := by210  -- sum the child box masses over the finitely many child types with nonzero coefficient211  have hq : 2 ≤ (U.M i).q := (universe_basic_facts U i).1212  set A : ℚ := (divisorProbability (U.M i).s ((U.M i).cellDegree c.1)).eval ((U.M i).q : ℚ) *213    (stateVolume (U.M i).s).eval ((U.M i).q : ℚ) with hAdef214  let C : (U.M i).childIdx c.1 → FactorType → ℚ := fun j t ↦215    (lawCoeff (stateLaw (((U.M i).childList c.1).get j).2) t).eval216      (((U.M i).q : ℚ) ^ (((U.M i).childList c.1).get j).1)217  have hC : ∀ j t, 0 ≤ C j t := exit_child_coeff_nonneg U i hIH c218  have hA : 0 ≤ A := mul_nonneg (divisor_probability_pos _ hq _ _ 2 le_rfl).1.le219    (density_value_arith _ hq (.const 1) (.const 1) (by simp [Expr.eval])220      (by simp [Expr.eval]) 0 _ (U.M i).valid).2.2.2.2.2.2.1.le221  let g : ((U.M i).childIdx c.1 → FactorType) → ℚ := fun τ ↦222    if σ = ∑ j, scaleType ((U.M i).childDelta c.1 j) (τ j) then A * ∏ j, C j (τ j) else 0223  have hg : ∀ τ, 0 ≤ g τ := fun τ ↦ by224    simp only [g]; split_ifs225    exacts [mul_nonneg hA (Finset.prod_nonneg fun j _ ↦ hC j (τ j)), le_rfl]226  have hstep1 : (U.M i).μ (U.typeBox i c.1 σ) = ∑' τ, ENNReal.ofReal ((g τ : ℚ) : ℝ) := by227    rw [typeBox_measure_eq_tsum U i hnt c.1 σ fun j t ↦ ((exit_child_law U i hIH c j).1 t).1]228    congr 1; funext τ229    simp only [g]230    split_ifs231    · exact exit_child_box_mass U i hnt hIH c τ232    · simp233  have hstep2 : ∑' τ, ENNReal.ofReal ((g τ : ℚ) : ℝ) =234      ∑ τ ∈ Fintype.piFinset (fun j : (U.M i).childIdx c.1 ↦235        ((stateLaw (((U.M i).childList c.1).get j).2).map Prod.fst).toFinset),236        ENNReal.ofReal ((g τ : ℚ) : ℝ) := by237    refine tsum_eq_sum fun τ hτ ↦ ?_238    rw [Fintype.mem_piFinset] at hτ239    push Not at hτ240    obtain ⟨j, hj⟩ := hτ241    have h0 : ∏ j, C j (τ j) = 0 := Finset.prod_eq_zero (Finset.mem_univ j)242      ((law_coeff_prod_formula 0 Fin.elim0 (τ j) _).2 _ _ hj)243    simp [g, h0]244  have hVs := (density_value_arith _ hq (.const 1) (.const 1) (by simp [Expr.eval])245      (by simp [Expr.eval]) 0 _ (U.M i).valid).2.2.2.2.2.2.1246  rw [hstep1, hstep2, ← ENNReal.ofReal_sum_of_nonneg (fun τ _ ↦ by exact_mod_cast hg τ), U.volume]247  simp only [densityValue]248  rw [← ENNReal.ofReal_mul' (by exact_mod_cast hVs.le), ← Rat.cast_sum, ← Rat.cast_mul, Expr.eval,249    lawCoeff_lawProd_descend_eval ((U.M i).childList c.1)250      (fun z hz ↦ children_residue_degree_pos _ _ _ hz), Finset.mul_sum, Finset.sum_mul]251  congr 2252  refine Finset.sum_congr rfl fun τ _ ↦ ?_253  simp only [g]254  by_cases hσ : σ = ∑ j, scaleType ((U.M i).childDelta c.1 j) (τ j)255  · rw [if_pos hσ, if_pos (show σ = ∑ j, scaleType (((U.M i).childList c.1).get j).1 (τ j) from hσ)]256    ring257  · rw [if_neg hσ, if_neg (show ¬σ = ∑ j, scaleType (((U.M i).childList c.1).get j).1 (τ j) from258      hσ)]259    ring260 261/-! ### Return chains at single states -/262 263private theorem list_sum_filter {α : Type} (s : Finset α) (p : α → Prop) [DecidablePred p]264    (f : α → ℚ) :265    ((s.toList.filter (fun x => decide (p x))).map f).sum = ∑ x ∈ s.filter p, f x := by266  rw [Finset.sum_eq_multiset_sum, Finset.filter_val, ← Finset.coe_toList s]267  rw [Multiset.filter_coe, Multiset.map_coe, Multiset.sum_coe]268 269open scoped Classical in270private theorem self_facts (a c q : ℕ) (ha : 0 < a) (hc : 2 ≤ c) (s : State)271    (hs : s = State.single a c) :272    (∀ P : TangentPattern s.degree, Allowed s P → SelfPattern s P → P.d.val = c ∧ children s P =273        [(1, State.single a c)]) ∧274    (((allowedPatterns s).toList.filter (SelfPattern s)).map fun P => (tangentCount s P).eval q).sum275        = q := by276  subst hs; exact self_patterns_of_single_state a c q ha hc277 278private theorem list_get_of_eq_singleton {α : Type} (l : List α) (x : α) (h : l = [x])279    (j : Fin l.length) : l.get j = x := by280  subst h; simp281 282private theorem eval_pow_nonneg (x : Expr) (q : ℚ) (hx : 0 ≤ x.eval q) (n : ℕ) :283    0 ≤ (x.pow n).eval q :=284  expression_pow_eval x q n ▸ pow_nonneg hx n285 286open scoped Classical in287/-- The self cells of a measured surface are counted by the divisors of the self patterns. -/288private theorem natCard_selfCells (M : MeasuredSurface) (hfin : ∀ P : TangentPattern M.s.degree,289    Finite (patternDivisors (IsLocalRing.ResidueField M.R) M.s P)) :290    (Nat.card {c : M.cellIndex // M.IsSelfCell c} : ℚ) =291      ∑ P ∈ (allowedPatterns M.s).filter (SelfPattern M.s),292        (Nat.card (patternDivisors (IsLocalRing.ResidueField M.R) M.s P) : ℚ) := by293  let e : {c : M.cellIndex // M.IsSelfCell c} ≃294      Σ P : {P : TangentPattern M.s.degree // Allowed M.s P ∧ SelfPattern M.s P},295        patternDivisors (IsLocalRing.ResidueField M.R) M.s P.1 :=296    { toFun := fun c => ⟨⟨c.1.1.1, c.1.1.2, c.2⟩, c.1.2⟩297      invFun := fun c => ⟨⟨⟨c.1.1, c.1.2.1⟩, c.2⟩, c.1.2.2⟩298      left_inv := by rintro ⟨⟨⟨P, h⟩, d⟩, h'⟩; rfl299      right_inv := by rintro ⟨⟨P, h⟩, d⟩; rfl }300  rw [Nat.card_congr e, Nat.card_sigma]301  push_cast302  symm; apply Finset.sum_subtype303  intro x; simp [allowedPatterns]304 305/-- At a single state `single a c` (`a > 0`, `c ≥ 2`), every self cell has degree `c` and the306single child `(1, single a c)`, its child surfaces have the same state and residue307cardinality, and there are exactly `q` self cells. -/308private theorem self_cells_facts (U : SurfaceUniverse) {a c : ℕ} (ha : 0 < a) (hc : 2 ≤ c)309    (i : U.ι) (hs : (U.M i).s = State.single a c) :310    (∀ c' : U.selfCells i, (U.M i).cellDegree c'.1 = c ∧311      (U.M i).childList c'.1 = [(1, State.single a c)]) ∧312    (∀ (c' : U.selfCells i) (j : (U.M i).childIdx c'.1),313      (U.M (U.child i c'.1 j)).s = State.single a c ∧ (U.M (U.child i c'.1 j)).q = (U.M i).q) ∧314    Finite (U.selfCells i) ∧ (Nat.card (U.selfCells i) : ℚ) = (U.M i).q := by315  classical316  obtain ⟨hq, -, -, -, _⟩ := universe_basic_facts U i317  have hntM : (U.M i).s.terminal = false := by318    obtain ⟨c', rfl⟩ : ∃ c', c = c' + 2 := ⟨c - 2, by omega⟩319    rw [hs]; rfl320  have hsf := self_facts a c (U.M i).q ha hc (U.M i).s hs321  have hcell : ∀ c' : U.selfCells i, (U.M i).cellDegree c'.1 = c ∧322      (U.M i).childList c'.1 = [(1, State.single a c)] :=323    fun c' => hsf.1 c'.1.1.1 c'.1.1.2 c'.2324  refine ⟨hcell, fun c' j => ?_, Subtype.finite, ?_⟩325  · have hg := list_get_of_eq_singleton _ _ (hcell c').2 j326    refine ⟨?_, ?_⟩327    · rw [U.child_state]; simp only [MeasuredSurface.childState, hg]328    · rw [U.child_residue]; simp only [MeasuredSurface.childDelta, hg, pow_one]329  · rw [show Nat.card (U.selfCells i) = Nat.card {c : (U.M i).cellIndex // (U.M i).IsSelfCell c}330      from rfl, natCard_selfCells (U.M i) (U.divisors_finite i), ← hsf.2, list_sum_filter]331    exact Finset.sum_congr rfl fun P hP =>332      U.divisor_count i hntM P (Finset.mem_filter.1 (Finset.mem_filter.1 hP).1).2333 334/-- The return weight `q · q^{-tri c}` as an extended nonnegative real. -/335private theorem densityValue_returnWeight (q : ℕ) (hq : 2 ≤ q) (c : ℕ) :336    densityValue (returnWeight c) q = (q : ℝ≥0∞) * (q : ℝ≥0∞)⁻¹ ^ tri c := by337  have h := density_value_arith q hq .var (.inv (.pow .var (tri c))) (by simp [Expr.eval])338    (by simp only [Expr.eval]; exact inv_nonneg.mpr (eval_pow_nonneg _ _ (by simp [Expr.eval]) _))339    (tri c) (State.single 1 1) ⟨Nat.one_pos, Nat.one_pos⟩340  rw [returnWeight, h.1, h.2.2.1]341  simp [densityValue, Expr.eval]342 343/-- One more return at `single a c`: if an event family `E` is measurable with mass `m · vol` at344every member in state `single a c` with the same residue cardinality, then the union over the345self cells of `i` of the child boxes of `E` is measurable with mass `λ · m · vol`, where `λ` is346the return weight. -/347private theorem self_cells_union_mass (U : SurfaceUniverse) {a c : ℕ} (ha : 0 < a) (hc : 2 ≤ c)348    (i : U.ι) (hs : (U.M i).s = State.single a c) (E : ∀ i' : U.ι, Set (Ideal (U.M i').R))349    (m : ℝ≥0∞)350    (hE : ∀ i' : U.ι, (U.M i').s = State.single a c → (U.M i').q = (U.M i).q →351      (U.M i').μ (E i') = m * (U.M i').μ (U.M i').stateSet ∧ MeasurableSet (E i')) :352    (U.M i).μ (⋃ c' : U.selfCells i, U.childBox i c'.1 (fun j ↦ E (U.child i c'.1 j))) =353      densityValue (returnWeight c) (U.M i).q * m * (U.M i).μ (U.M i).stateSet ∧354    MeasurableSet (⋃ c' : U.selfCells i, U.childBox i c'.1 (fun j ↦ E (U.child i c'.1 j))) := by355  obtain ⟨hq, -, -, -, -⟩ := universe_basic_facts U i356  have hntM : (U.M i).s.terminal = false := by357    obtain ⟨c', rfl⟩ : ∃ c', c = c' + 2 := ⟨c - 2, by omega⟩358    rw [hs]; rfl359  obtain ⟨hcell, hchild, _, hcard⟩ := self_cells_facts U ha hc i hs360  -- each self cell has a single child, in the same state, with the same residue cardinality361  have hbox : ∀ c' : U.selfCells i,362      MeasurableSet (U.childBox i c'.1 (fun j ↦ E (U.child i c'.1 j))) ∧363      (U.M i).μ (U.childBox i c'.1 (fun j ↦ E (U.child i c'.1 j))) =364        ((U.M i).q : ℝ≥0∞)⁻¹ ^ tri c * (m * (U.M i).μ (U.M i).stateSet) := by365    intro c'366    have hG : ∀ j, MeasurableSet (E (U.child i c'.1 j)) :=367      fun j ↦ (hE _ (hchild c' j).1 (hchild c' j).2).2368    refine ⟨U.Φ_measurable i hntM c'.1 _ hG, ?_⟩369    unfold SurfaceUniverse.childBox370    rw [U.Φ_measure i hntM c'.1 _ hG, (hcell c').1]371    have j0 : (U.M i).childIdx c'.1 := ⟨0, by rw [(hcell c').2]; simp⟩372    have : Subsingleton ((U.M i).childIdx c'.1) := by373      change Subsingleton (Fin ((U.M i).childList c'.1).length)374      rw [(hcell c').2]; simp only [List.length_singleton]; infer_instance375    rw [Fintype.prod_subsingleton _ j0]376    congr 1377    rw [(hE _ (hchild c' j0).1 (hchild c' j0).2).1, U.volume, U.volume, (hchild c' j0).1, hs,378      (hchild c' j0).2]379  have hdisj : Pairwise (Function.onFun Disjoint fun c' : U.selfCells i ↦380      U.childBox i c'.1 (fun j ↦ E (U.child i c'.1 j))) := fun x y hxy ↦381    (U.cells_disjoint i hntM (fun h ↦ hxy (Subtype.ext h))).mono382      Set.inter_subset_left Set.inter_subset_left383  let : Fintype (U.selfCells i) := Fintype.ofFinite _384  refine ⟨?_, MeasurableSet.iUnion fun c' ↦ (hbox c').1⟩385  have hcardN : Fintype.card (U.selfCells i) = (U.M i).q := by386    rw [← Nat.card_eq_fintype_card]; exact_mod_cast hcard387  rw [MeasureTheory.measure_iUnion hdisj (fun c' ↦ (hbox c').1), tsum_fintype,388    Finset.sum_congr rfl (fun c' _ ↦ (hbox c').2), Finset.sum_const, Finset.card_univ,389    nsmul_eq_mul, hcardN, densityValue_returnWeight _ hq]390  ring391 392/-- If the immediate exit event at `single a c` has mass `G · vol`, then the exit event after393`k` returns has mass `λᵏ · G · vol`, where `λ` is the return weight; it is measurable. -/394theorem exit_event_succ_mass (U : SurfaceUniverse) (a c : ℕ) (ha : 0 < a) (hc : 2 ≤ c)Proof of Theorem 6.2395    (σ : FactorType) (q₀ : ℕ) (G : ℚ)396    (hexit : ∀ i : U.ι, (U.M i).s = State.single a c → (U.M i).q = q₀ → (U.M i).μ397        (U.exitEvent σ 0 i) = ENNReal.ofReal (G : ℝ) * (U.M i).μ (U.M i).stateSet ∧ MeasurableSet398        (U.exitEvent σ 0 i))399    (k : ℕ) :400    ∀ i : U.ι, (U.M i).s = State.single a c → (U.M i).q = q₀ →401    (U.M i).μ (U.exitEvent σ k i) = ENNReal.ofReal ((((returnWeight c).eval (q₀ : ℚ)) ^ k * G : ℚ) :402        ℝ) * (U.M i).μ (U.M i).stateSet ∧403    MeasurableSet (U.exitEvent σ k i) := by404  induction k with405  | zero =>406    intro i hs hq0407    simpa using hexit i hs hq0408  | succ k ih =>409    intro i hs hq0410    have hy : 0 ≤ (returnWeight c).eval (q₀ : ℚ) :=411      (return_weight_bounds _ c (hq0 ▸ (universe_basic_facts U i).1) hc).1.le412    obtain ⟨hmass, hmeas⟩ := self_cells_union_mass U ha hc i hs (U.exitEvent σ k) _413      fun i' hs' hq' ↦ ih i' hs' (hq'.trans hq0)414    refine ⟨hmass.trans ?_, hmeas⟩415    rw [hq0, densityValue, ← ENNReal.ofReal_mul (by exact_mod_cast hy)]416    congr 2; push_cast; ring417 418/-! ### Measurability and null sets -/419 420/-- At a nonterminal state (assuming the law for smaller ranks), all return, exit, terminating421exit and bad exit events of members in the same state are measurable. -/422theorem recursion_events_measurable (U : SurfaceUniverse) (i : U.ι)423    (hnt : (U.M i).s.terminal = false)424    (hIH : ∀ i' : U.ι, (U.M i').s.rank < (U.M i).s.rank → U.LawStatement i') :425    ∀ i' : U.ι, (U.M i').s = (U.M i).s → ∀ (k : ℕ) (σ : FactorType),426    MeasurableSet (U.returnEvent k i') ∧ MeasurableSet (U.exitEvent σ k i') ∧427    MeasurableSet (U.termExitEvent k i') ∧ MeasurableSet (U.badExitEvent k i') := by428  intro i₀ hs₀ k σ429  induction k generalizing i₀ with430  | zero =>431    have hnt' : (U.M i₀).s.terminal = false := by rw [hs₀]; exact hnt432    have : Finite (U.M i₀).cellIndex := (universe_basic_facts U i₀).2.2.2.2433    have : Countable (U.exitCells i₀) := by unfold SurfaceUniverse.exitCells; infer_instance434    have hrk : ∀ (c : U.exitCells i₀) j, (U.M (U.child i₀ c.1 j)).s.rank < (U.M i).s.rank := by435      intro c j436      rw [U.child_state, ← hs₀]437      exact nonself_child_rank_lt (U.M i₀).s (U.M i₀).valid c.1.1.1 c.1.1.2 c.2 _438        (List.get_mem _ _)439    refine ⟨U.stateSet_measurable i₀, ?_, ?_, ?_⟩440    · simp only [SurfaceUniverse.exitEvent]441      refine MeasurableSet.iUnion fun c => ?_442      unfold SurfaceUniverse.typeBox443      refine MeasurableSet.iUnion fun τ => MeasurableSet.iUnion fun _ => ?_444      exact U.Φ_measurable i₀ hnt' c.1 _ fun j => ((hIH _ (hrk c j)).1 (τ j)).1445    · simp only [SurfaceUniverse.termExitEvent]446      refine MeasurableSet.iUnion fun c => ?_447      exact U.Φ_measurable i₀ hnt' c.1 _ fun j => (hIH _ (hrk c j)).2.1448    · simp only [SurfaceUniverse.badExitEvent]449      refine MeasurableSet.iUnion fun c => MeasurableSet.iUnion fun j₀ => ?_450      refine U.Φ_measurable i₀ hnt' c.1 _ fun j => ?_451      by_cases hj : j = j₀452      · subst hj453        rw [Function.update_self]454        exact (U.stateSet_measurable _).inter (hIH _ (hrk c j)).2.1.compl455      · rw [Function.update_of_ne hj]456        exact MeasurableSet.univ457  | succ k ih =>458    have hnt' : (U.M i₀).s.terminal = false := by rw [hs₀]; exact hnt459    have : Finite (U.M i₀).cellIndex := (universe_basic_facts U i₀).2.2.2.2460    have : Countable (U.selfCells i₀) := by unfold SurfaceUniverse.selfCells; infer_instance461    have hst : ∀ (c : U.selfCells i₀) j, (U.M (U.child i₀ c.1 j)).s = (U.M i).s := by462      intro c j463      rw [U.child_state, ← hs₀]464      obtain ⟨a, b, -, h⟩ := c.2465      have hm : ∀ z ∈ (U.M i₀).childList c.1, z = (1, (U.M i₀).s) := by466        intro z hz467        unfold MeasuredSurface.childList at hz468        rw [h] at hz469        simpa using hz470      exact congrArg Prod.snd (hm _ (List.get_mem _ _))471    refine ⟨?_, ?_, ?_, ?_⟩472    · simp only [SurfaceUniverse.returnEvent]473      exact MeasurableSet.iUnion fun c =>474        U.Φ_measurable i₀ hnt' c.1 _ fun j => (ih _ (hst c j)).1475    · simp only [SurfaceUniverse.exitEvent]476      exact MeasurableSet.iUnion fun c =>477        U.Φ_measurable i₀ hnt' c.1 _ fun j => (ih _ (hst c j)).2.1478    · simp only [SurfaceUniverse.termExitEvent]479      exact MeasurableSet.iUnion fun c =>480        U.Φ_measurable i₀ hnt' c.1 _ fun j => (ih _ (hst c j)).2.2.1481    · simp only [SurfaceUniverse.badExitEvent]482      exact MeasurableSet.iUnion fun c =>483        U.Φ_measurable i₀ hnt' c.1 _ fun j => (ih _ (hst c j)).2.2.2484 485/-- Bad exit events are null at a nonterminal state, assuming the law for smaller ranks. -/486theorem bad_exit_null (U : SurfaceUniverse) (i : U.ι) (hnt : (U.M i).s.terminal = false)Proof of Theorem 6.2487    (hIH : ∀ i' : U.ι, (U.M i').s.rank < (U.M i).s.rank → U.LawStatement i') (k : ℕ) :488    ∀ i' : U.ι, (U.M i').s = (U.M i).s → (U.M i').μ (U.badExitEvent k i') = 0 := by489  induction k with490  | zero =>491    intro i' hi'492    have hnt' : (U.M i').s.terminal = false := hi' ▸ hnt493    have : Finite (U.M i').cellIndex := (universe_basic_facts U i').2.2.2.2494    have : Countable (U.exitCells i') := by unfold SurfaceUniverse.exitCells; infer_instance495    simp only [SurfaceUniverse.badExitEvent]496    refine MeasureTheory.measure_iUnion_null fun c => MeasureTheory.measure_iUnion_null fun j₀ => ?_497    have hrank : ∀ j, (U.M (U.child i' c.1 j)).s.rank < (U.M i).s.rank := by498      intro j499      rw [U.child_state, ← hi']500      exact nonself_child_rank_lt (U.M i').s (U.M i').valid c.1.1.1 c.1.1.2 c.2501        _ (List.get_mem _ _)502    have hL := hIH _ (hrank j₀)503    have hmeas : ∀ j, MeasurableSet (Function.update (fun j =>504        (Set.univ : Set (Ideal (U.M (U.child i' c.1 j)).R))) j₀505        (U.nonterminatingSet (U.child i' c.1 j₀)) j) := by506      intro j507      by_cases h : j = j₀508      · subst h; rw [Function.update_self]509        exact (U.stateSet_measurable _).inter hL.2.1.compl510      · rw [Function.update_of_ne h]; exact MeasurableSet.univ511    unfold SurfaceUniverse.childBox512    rw [U.Φ_measure i' hnt' c.1 _ hmeas]513    rw [Finset.prod_eq_zero (Finset.mem_univ j₀) (by rw [Function.update_self]; exact hL.2.2),514        mul_zero]515  | succ k ih =>516    intro i' hi'517    have hnt' : (U.M i').s.terminal = false := hi' ▸ hnt518    have : Finite (U.M i').cellIndex := (universe_basic_facts U i').2.2.2.2519    have : Countable (U.selfCells i') := by unfold SurfaceUniverse.selfCells; infer_instance520    simp only [SurfaceUniverse.badExitEvent]521    refine MeasureTheory.measure_iUnion_null fun c => ?_522    have hs : ∀ j, (U.M (U.child i' c.1 j)).s = (U.M i).s := by523      intro j524      rw [U.child_state, ← hi']525      obtain ⟨a, b, _, hch⟩ := c.2526      have hm := List.get_mem ((U.M i').childList c.1) j527      have : (U.M i').childList c.1 = [(1, (U.M i').s)] := hch528      have key : ∀ z ∈ (U.M i').childList c.1, z = (1, (U.M i').s) := by529        rw [this]; simp530      have hm := key _ hm531      unfold MeasuredSurface.childState532      rw [hm]533    have hmeas : ∀ j, MeasurableSet (U.badExitEvent k (U.child i' c.1 j)) := fun j =>534      (recursion_events_measurable U i hnt hIH _ (hs j) k ∅).2.2.2535    unfold SurfaceUniverse.childBox536    rw [U.Φ_measure i' hnt' c.1 _ hmeas]537    have hpos : 0 < ((U.M i').childList c.1).length := by538      obtain ⟨a, b, _, hch⟩ := c.2539      have : (U.M i').childList c.1 = [(1, (U.M i').s)] := hch540      rw [this]; simp541    rw [Finset.prod_eq_zero_iff.mpr ⟨⟨0, hpos⟩, Finset.mem_univ _, ih _ (hs _)⟩, mul_zero]542 543/-- Summing the weight `P(d) · (σ-coefficient of the descended children laws)` over the exit544cells gives the `σ`-coefficient of the exit law. -/545private theorem exit_cell_weight_sum (U : SurfaceUniverse) (i : U.ι)546    (hnt : (U.M i).s.terminal = false) (σ : FactorType)547    [Fintype (U.exitCells i)] :548    ∑ c : U.exitCells i,549      (divisorProbability (U.M i).s ((U.M i).cellDegree c.1)).eval ((U.M i).q : ℚ) *550        (lawCoeff (lawProd (((U.M i).childList c.1).map fun z => lawDescend z.1 (stateLaw z.2)))551          σ).eval ((U.M i).q : ℚ) =552      (lawCoeff (exitLaw (U.M i).s) σ).eval ((U.M i).q : ℚ) := by553  classical554  let : ∀ P, Fintype (patternDivisors (IsLocalRing.ResidueField (U.M i).R) (U.M i).s P) :=555    fun P => @Fintype.ofFinite _ (U.divisors_finite i P)556  set M := U.M i with hM557  set s := M.s with hs558  set qq : ℚ := (M.q : ℚ) with hqq559  let F : M.cellIndex → ℚ := fun c =>560    (divisorProbability s (M.cellDegree c)).eval qq *561      (lawCoeff (lawProd ((M.childList c).map fun z => lawDescend z.1 (stateLaw z.2))) σ).eval qq562  let g : TangentPattern s.degree → ℚ := fun P => if SelfPattern s P then 0 else563    (tangentCount s P).eval qq * ((divisorProbability s P.d.val).eval qq *564      (lawCoeff (lawProd ((children s P).map fun z => lawDescend z.1 (stateLaw z.2))) σ).eval qq)565  have h1 : ∑ c : U.exitCells i, F c.1 =566      ∑ c : M.cellIndex, if M.IsSelfCell c then 0 else F c := by567    rw [Finset.sum_ite, Finset.sum_const_zero, zero_add]568    exact (Finset.sum_subtype _ (fun x => by569      simp only [Finset.mem_filter, Finset.mem_univ, true_and]; exact Iff.rfl) F).symm570  have h2 : (∑ c : M.cellIndex, if M.IsSelfCell c then 0 else F c) =571      ∑ P : M.allowedPattern, g P.1 := by572    rw [Fintype.sum_sigma]573    refine Finset.sum_congr rfl fun P _ => ?_574    change ∑ D : patternDivisors (IsLocalRing.ResidueField M.R) s P.1,575        (if SelfPattern s P.1 then (0 : ℚ) else (divisorProbability s P.1.d.val).eval qq *576          (lawCoeff (lawProd ((children s P.1).map fun z => lawDescend z.1 (stateLaw z.2)))577              σ).eval qq)578        = g P.1579    rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, ← Nat.card_eq_fintype_card,580      U.divisor_count i hnt P.1 P.2]581    simp only [g]582    split_ifs583    · simp584    · simp only [mul_eq_mul_right_iff, mul_eq_zero]; left; rfl585  have h3 : ∑ P : M.allowedPattern, g P.1 = ∑ P ∈ allowedPatterns s, g P :=586    (Finset.sum_subtype _ (fun x => by587      simp only [allowedPatterns, Finset.mem_filter, Finset.mem_univ, true_and]588      exact Iff.rfl) g).symm589  have h4 : (lawCoeff (exitLaw s) σ).eval qq = ∑ P ∈ allowedPatterns s, g P := by590    unfold exitLaw591    rw [(law_coeff_flatMap _ _ _ [] [] σ qq).2.2, Finset.sum_map_toList]592    refine Finset.sum_congr rfl fun P _ => ?_593    simp only [g]594    split_ifs595    · exact (law_coeff_flatMap Unit [] (fun _ => []) [] [] σ qq).2.1596    · rw [law_coeff_scale]; change _ * _ * _ = _; ring597  exact h1.trans (h2.trans (h3.trans h4.symm))598 599/-- The immediate exit event of type `σ` has mass equal to the `σ`-coefficient of the exit law600times the volume of the state set; this coefficient is nonnegative and the event measurable. -/601theorem exit_event_zero_mass (U : SurfaceUniverse) (i : U.ι) (hnt : (U.M i).s.terminal = false)602    (hIH : ∀ i' : U.ι, (U.M i').s.rank < (U.M i).s.rank → U.LawStatement i') (σ : FactorType) :603    (U.M i).μ (U.exitEvent σ 0 i) = densityValue (lawCoeff (exitLaw (U.M i).s) σ) (U.M i).q *604        (U.M i).μ (U.M i).stateSet ∧605    0 ≤ (lawCoeff (exitLaw (U.M i).s) σ).eval ((U.M i).q : ℚ) ∧606      MeasurableSet (U.exitEvent σ 0 i) := by607  classical608  obtain ⟨hq, -, -, -, -⟩ := universe_basic_facts U i609  have hmeas : MeasurableSet (U.exitEvent σ 0 i) :=610    ((recursion_events_measurable U i hnt hIH) i rfl 0 σ).2.1611  set M := U.M i with hM612  set s := M.s with hs613  set qq : ℚ := (M.q : ℚ) with hqq614  -- the per-cell rational weight615  let F : M.cellIndex → ℚ := fun c =>616    (divisorProbability s (M.cellDegree c)).eval qq *617      (lawCoeff (lawProd ((M.childList c).map fun z => lawDescend z.1 (stateLaw z.2))) σ).eval qq618  have hFnn : ∀ c : U.exitCells i, 0 ≤ F c.1 := by619    intro c620    exact mul_nonneg ((divisor_probability_pos M.q hq s _ 2 le_rfl).1.le)621      (exit_cell_coeff_nonneg U i hIH c σ)622  have hbox_sub : ∀ c σ', U.typeBox i c σ' ⊆ M.cell c := by623    intro c σ' x hx624    simp only [SurfaceUniverse.typeBox, Set.mem_iUnion] at hx625    obtain ⟨τ, _, hx⟩ := hx626    exact hx.1627  have hbox_eq : ∀ c : U.exitCells i, U.typeBox i c.1 σ = U.exitEvent σ 0 i ∩ M.cell c.1 := by628    intro c629    ext x630    constructor631    · intro hx632      exact ⟨Set.mem_iUnion.2 ⟨c, hx⟩, hbox_sub _ _ hx⟩633    · rintro ⟨hE, hc⟩634      obtain ⟨c', hx'⟩ := Set.mem_iUnion.1 hE635      by_cases h : c'.1 = c.1636      · rw [← h]; exact hx'637      · exact absurd (U.cells_disjoint i hnt h) (Set.not_disjoint_iff.2 ⟨x, hbox_sub _ _ hx', hc⟩)638  let : ∀ P, Fintype (patternDivisors (IsLocalRing.ResidueField M.R) s P) :=639    fun P => @Fintype.ofFinite _ (U.divisors_finite i P)640  let : Fintype (U.exitCells i) := by unfold SurfaceUniverse.exitCells; infer_instance641  have hsum : (M.μ (U.exitEvent σ 0 i)) = ∑ c : U.exitCells i, ENNReal.ofReal ((F c.1 : ℚ) : ℝ) *642      M.μ M.stateSet := by643    rw [show U.exitEvent σ 0 i = ⋃ c : U.exitCells i, U.typeBox i c.1 σ from rfl]644    rw [MeasureTheory.measure_iUnion, tsum_fintype]645    · exact Finset.sum_congr rfl fun c _ => exit_cell_type_mass U i hnt hIH c σ646    · intro c c' hcc'647      have hne : c.1 ≠ c'.1 := fun h => hcc' (Subtype.ext h)648      exact (U.cells_disjoint i hnt hne).mono (hbox_sub _ _) (hbox_sub _ _)649    · intro c650      rw [hbox_eq c]651      exact hmeas.inter (U.cell_measurable i hnt c.1)652  have hrat : ∑ c : U.exitCells i, F c.1 = (lawCoeff (exitLaw s) σ).eval qq :=653    exit_cell_weight_sum U i hnt σ654  refine ⟨?_, ?_, hmeas⟩655  · rw [hsum, ← Finset.sum_mul, ← ENNReal.ofReal_sum_of_nonneg656      (fun c _ => by exact_mod_cast hFnn c)]657    change _ = ENNReal.ofReal (((lawCoeff (exitLaw s) σ).eval qq : ℚ) : ℝ) * _658    rw [← hrat]659    push_cast660    rfl661  · rw [← hrat]662    exact Finset.sum_nonneg fun c _ => hFnn c663 664/-! ### Crossing states, return events and the law statement -/665 666/-- The law statement at a crossing state, assuming it for all states of smaller rank. -/667theorem recursion_crossing_law (U : SurfaceUniverse) (i : U.ι) (a b c h : ℕ)Proof of Theorem 6.2668    (hs : (U.M i).s = State.crossing a b c h)669    (hIH : ∀ i' : U.ι, (U.M i').s.rank < (U.M i).s.rank → U.LawStatement i') :670    U.LawStatement i := by671  have hnt : (U.M i).s.terminal = false := by rw [hs]; rfl672  have hv : (U.M i).s.Valid := (U.M i).valid673  have h560 := (single_state_return_chain U i hnt)674  have h551 := (state_law_unfold _ hv hnt).2 a b c h hs675  refine ⟨fun σ => ?_, ?_, ?_⟩676  · have e := ((h560 σ).2 a b c h hs).1677    obtain ⟨m, nn, ms⟩ := exit_event_zero_mass U i hnt hIH σ678    rw [e, h551]679    exact ⟨ms, nn, m⟩680  · have e := ((h560 (default)).2 a b c h hs).2681    rw [e]682    exact (recursion_events_measurable U i hnt hIH i rfl 0 default).2.2.1683  · exact MeasureTheory.measure_mono_null684      ((nonterminating_subset_return_or_bad U i hnt).2 a b c h hs)685      (bad_exit_null U i hnt hIH 0 i rfl)686 687/-- At `single a c`, the event of returning `k` times has mass `λᵏ · vol`, with `λ` the return688weight, and is measurable. -/689theorem return_event_mass (U : SurfaceUniverse) (a c : ℕ) (ha : 0 < a) (hc : 2 ≤ c) (k : ℕ) :Proof of Theorem 6.2690    ∀ i : U.ι, (U.M i).s = State.single a c →691    (U.M i).μ (U.returnEvent k i) = densityValue ((returnWeight c).pow k) (U.M i).q * (U.M i).μ692        (U.M i).stateSet ∧693    MeasurableSet (U.returnEvent k i) := by694  have hvalid : (State.single a c).Valid := ⟨ha, by omega⟩695  induction k with696  | zero =>697    intro i hs698    obtain ⟨hq, -, -, -, -⟩ := universe_basic_facts U i699    refine ⟨?_, U.stateSet_measurable i⟩700    simp only [SurfaceUniverse.returnEvent, Expr.pow]701    rw [(density_value_arith (U.M i).q hq (.const 1) (.const 1) (by norm_num [Expr.eval])702      (by norm_num [Expr.eval]) 0 _ hvalid).2.2.2.1, one_mul]703  | succ k ih =>704    intro i hs705    obtain ⟨hq, -, -, -, -⟩ := universe_basic_facts U i706    obtain ⟨hmass, hmeas⟩ := self_cells_union_mass U ha hc i hs (U.returnEvent k)707      (densityValue ((returnWeight c).pow k) (U.M i).q) fun i' hs' hq' ↦ by708        rw [← hq']; exact ih i' hs'709    refine ⟨hmass.trans ?_, hmeas⟩710    have hy := (return_weight_bounds _ c hq hc).1.le711    rw [Expr.pow, (density_value_arith (U.M i).q hq _ _ (eval_pow_nonneg _ _ hy k) hy 0 _712      hvalid).1]713    ring714 715/-- At `single a c` the set of ideals that return infinitely often is measurable and null. -/716theorem never_return_null (U : SurfaceUniverse) (a c : ℕ) (ha : 0 < a) (hc : 2 ≤ c) (i : U.ι)Proof of Theorem 6.2717    (hs : (U.M i).s = State.single a c) :718    (U.M i).μ (⋂ k, U.returnEvent k i) = 0 ∧ MeasurableSet (⋂ k, U.returnEvent k i) := by719  have hmass := fun k => return_event_mass U a c ha hc k i hs720  refine ⟨?_, MeasurableSet.iInter fun k => (hmass k).2⟩721  obtain ⟨hq, -, hfin, -⟩ := universe_basic_facts U i722  obtain ⟨hpos, -, hlt⟩ := return_weight_bounds (U.M i).q c hq hc723  have hlt' : ENNReal.ofReal (((returnWeight c).eval ((U.M i).q : ℚ) : ℚ) : ℝ) < 1 := by724    rw [ENNReal.ofReal_lt_one]; exact_mod_cast hlt725  have hle : ∀ k, (U.M i).μ (⋂ k, U.returnEvent k i) ≤726      (ENNReal.ofReal (((returnWeight c).eval ((U.M i).q : ℚ) : ℚ) : ℝ)) ^ k * (U.M i).μ727          (U.M i).stateSet := by728    intro k729    refine (MeasureTheory.measure_mono (Set.iInter_subset _ k)).trans ?_730    rw [(hmass k).1, densityValue, expression_pow_eval, ← ENNReal.ofReal_pow731        (by exact_mod_cast hpos.le)]732    norm_cast733  have ht := ENNReal.Tendsto.mul_const (ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one hlt')734    (Or.inr hfin)735  rw [zero_mul] at ht736  exact le_antisymm (ge_of_tendsto' ht hle) zero_le737 738/-- The law statement at a nonterminal single state, assuming it for all states of smaller rank. -/739theorem recursion_single_law (U : SurfaceUniverse) (i : U.ι) (a c : ℕ) (hc : 2 ≤ c)Proof of Theorem 6.2740    (hs : (U.M i).s = State.single a c)741    (hIH : ∀ i' : U.ι, (U.M i').s.rank < (U.M i).s.rank → U.LawStatement i') :742    U.LawStatement i := by743  have hnt : (U.M i).s.terminal = false := by744    rw [hs]; obtain ⟨c', rfl⟩ : ∃ c', c = c' + 2 := ⟨c - 2, by omega⟩; rfl745  have hv : (U.M i).s.Valid := (U.M i).valid746  have ha : 0 < a := by rw [hs] at hv; exact hv.1747  have h560 := single_state_return_chain U i hnt748  have h551 := (state_law_unfold _ hv hnt).1 a c hs749  have hq := (universe_basic_facts U i).1750  obtain ⟨hl0, -, hl1⟩ := return_weight_bounds _ c hq hc751  refine ⟨fun σ => ?_, ?_, ?_⟩752  · set q₀ := (U.M i).q with hq₀753    set lam : ℚ := (returnWeight c).eval (q₀ : ℚ) with hlam754    set G : ℚ := (lawCoeff (exitLaw (State.single a c)) σ).eval (q₀ : ℚ) with hGdef755    have hG : 0 ≤ G := by756      have := (exit_event_zero_mass U i hnt hIH σ).2.1757      rwa [hs] at this758    have hexit : ∀ i' : U.ι, (U.M i').s = State.single a c → (U.M i').q = q₀ →759        (U.M i').μ (U.exitEvent σ 0 i') = ENNReal.ofReal (G : ℝ) * (U.M i').μ (U.M i').stateSet760          ∧ MeasurableSet (U.exitEvent σ 0 i') := by761      intro i' hs' hq'762      have hnt' : (U.M i').s.terminal = false := by rw [hs', ← hs]; exact hnt763      have hIH' : ∀ j : U.ι, (U.M j).s.rank < (U.M i').s.rank → U.LawStatement j := by764        rw [hs', ← hs]; exact hIH765      obtain ⟨m, -, ms⟩ := exit_event_zero_mass U i' hnt' hIH' σ766      rw [hs', hq'] at m767      exact ⟨m, ms⟩768    have hk := fun k => exit_event_succ_mass U a c ha hc σ q₀ G hexit k i hs rfl769    obtain ⟨e, hdisj, -⟩ := (h560 σ).1 a c hs770    have hcoef : (lawCoeff (stateLaw (U.M i).s) σ).eval (q₀ : ℚ) = (1 - lam)⁻¹ * G := by771      rw [h551, law_coeff_scale, hs]772      simp only [Expr.eval, Expr.sub, Expr.neg, neg_mul, one_mul, hlam, hGdef]773      ring774    have hpos : (0 : ℚ) < 1 - lam := by linarith775    rw [e, hcoef]776    refine ⟨MeasurableSet.iUnion fun k => (hk k).2, by positivity, ?_⟩777    rw [MeasureTheory.measure_iUnion hdisj fun k => (hk k).2]778    simp only [fun k => (hk k).1]779    rw [ENNReal.tsum_mul_right, densityValue, ← ENNReal.ofReal_tsum_of_nonneg]780    · congr 2781      have := geometric_exit_sum (lam : ℝ) (G : ℝ) (by exact_mod_cast hl0.le)782        (by exact_mod_cast hl1)783      rw [hcoef]784      push_cast785      rw [this.tsum_eq]786      field_simp787    · intro k; push_cast; positivity788    · have := geometric_exit_sum (lam : ℝ) (G : ℝ) (by exact_mod_cast hl0.le)789        (by exact_mod_cast hl1)790      push_cast791      exact this.summable792  · rw [((h560 default).1 a c hs).2.2]793    exact MeasurableSet.iUnion fun k =>794      (recursion_events_measurable U i hnt hIH i rfl k default).2.2.1795  · refine MeasureTheory.measure_mono_null796      ((nonterminating_subset_return_or_bad U i hnt).1 a c hs) ?_797    refine MeasureTheory.measure_union_null798      (never_return_null U a c ha hc i hs).1 ?_799    exact MeasureTheory.measure_iUnion_null fun k =>800      bad_exit_null U i hnt hIH k i rfl801 802/-- The law statement holds for every member of a surface universe. -/803theorem universal_law_statement (U : SurfaceUniverse) :Theorem 6.2804    ∀ i : U.ι, U.LawStatement i := by805  have key : ∀ n : ℕ, ∀ i : U.ι, (U.M i).s.rank = n → U.LawStatement i := by806    intro n807    induction n using Nat.strong_induction_on with808    | _ n ih =>809      intro i hn810      have hIH : ∀ i' : U.ι, (U.M i').s.rank < (U.M i).s.rank → U.LawStatement i' :=811        fun i' h => ih _ (hn ▸ h) i' rfl812      have hv := (U.M i).valid813      generalize hs : (U.M i).s = s at hv814      cases s with815      | single a c =>816        by_cases h1 : c = 1817        · subst h1818          exact recursion_terminal_law U i (by rw [hs]; rfl)819        · have : 2 ≤ c := by820            have := hv.2; omega821          exact recursion_single_law U i a c this hs hIH822      | crossing a b c h =>823        exact recursion_crossing_law U i a b c h hs hIH824  exact fun i => key _ i rfl825 826/-! ### Type events -/827 828/-- The terminating type-`σ` event is measurable, contained in the type-`σ` event, and differs829from it by a subset of the null nonterminating set. -/830theorem type_event_null_difference (U : SurfaceUniverse) (i : U.ι) (σ : FactorType) :831    MeasurableSet (U.termTypeEvent i σ) ∧ U.termTypeEvent i σ ⊆ U.typeEvent i σ ∧832    U.typeEvent i σ ⊆ U.termTypeEvent i σ ∪ U.nonterminatingSet i ∧833    (U.M i).μ (U.nonterminatingSet i) = 0 := by834  have h := universal_law_statement U i835  refine ⟨(h.1 σ).1, Set.inter_subset_left, ?_, h.2.2⟩836  intro J hJ837  by_cases ht : J ∈ U.terminatingSet i838  · exact Or.inl ⟨hJ, ht⟩839  · refine Or.inr ⟨?_, ht⟩840    exact hJ.1841 842/-- Under the étale type-transport hypotheses, every type event of a surface universe is843measurable. -/844theorem etale_type_event_measurable (U : SurfaceUniverse)845    (hE1 : U.ChildTypesExist) (δ : ∀ i : U.ι, Ideal (U.M i).R → ℕ) (hE2 : U.InvariantDecreases δ)846    (i : U.ι) (σ : FactorType) :847    MeasurableSet (U.typeEvent i σ) := by848  rw [etale_type_event_eq_term U hE1 δ hE2 i σ]849  exact (type_event_null_difference U i σ).1850 851/-- A decomposition `K ⊗[O] B ≃ ∏ᵢ Lᵢ` of the generic fibre ascends along an unramified extension852`O → Oδ` (with `π` remaining a uniformizer) to `Kδ ⊗[Oδ] B ≃ ∏ᵢ Lᵢ`, compatibly with the853`O`-structures. -/854theorem unramified_generic_fibre_ascent (O Oδ : Type) [CommRing O] [IsDomain O]855    [IsDiscreteValuationRing O] [CommRing Oδ] [IsDomain Oδ] [IsDiscreteValuationRing Oδ]856    [Algebra O Oδ] [Module.Finite O Oδ] [Module.Free O Oδ] (δ : ℕ) (hrank : Module.finrank O Oδ = δ)857    (pi : O) (hpi : Irreducible pi) (hpiδ : Irreducible (algebraMap O Oδ pi)) (B : Type)858    [CommRing B] [Algebra O B] [Algebra Oδ B] [IsScalarTower O Oδ B] (ι : Type)859    (L : ι → Type) [∀ i, Field (L i)] [∀ i, Algebra (BaseField O) (L i)]860    [∀ i, FiniteDimensional (BaseField O) (L i)]861    (e : TensorProduct O (BaseField O) B ≃ₐ[BaseField O] (∀ i, L i)) :862    ∃ (_ : ∀ i, Algebra (BaseField Oδ) (L i)) (_ : ∀ i, Algebra Oδ (L i))863        (_ : ∀ i, IsScalarTower Oδ (BaseField Oδ) (L i))864        (_ : ∀ i, FiniteDimensional (BaseField Oδ) (L i))865        (_ : TensorProduct Oδ (BaseField Oδ) B ≃ₐ[BaseField Oδ] (∀ i, L i)),866    ∀ i (c : O),867    algebraMap Oδ (L i) (algebraMap O Oδ c) = algebraMap (BaseField O) (L i)868        (algebraMap O (BaseField O) c) := by869  obtain ⟨-, -, hfr⟩ := unramified_fraction_base_change O Oδ δ hrank pi hpi hpiδ870  set K := BaseField O871  set Kδ := BaseField Oδ872  let rA : Algebra Oδ (TensorProduct O K Oδ) := Algebra.TensorProduct.rightAlgebra873  -- Oδ-algebra equivalence K ⊗ Oδ ≃ Oδ ⊗ K874  let c : TensorProduct O K Oδ ≃ₐ[Oδ] TensorProduct O Oδ K :=875    AlgEquiv.ofRingEquiv (f := (Algebra.TensorProduct.comm O K Oδ).toRingEquiv) (by876      intro x877      change (Algebra.TensorProduct.comm O K Oδ) ((1 : K) ⊗ₜ x) = x ⊗ₜ (1 : K)878      simp)879  have : IsFractionRing Oδ (TensorProduct O Oδ K) := IsLocalization.isLocalization_of_algEquiv _ c880  let ψ : Kδ ≃ₐ[Oδ] TensorProduct O Oδ K :=881    IsLocalization.algEquiv (nonZeroDivisors Oδ) Kδ (TensorProduct O Oδ K)882  let Θ : TensorProduct Oδ Kδ B ≃+* TensorProduct O K B :=883    ((Algebra.TensorProduct.comm Oδ Kδ B).toRingEquiv.trans884      (Algebra.TensorProduct.congr (AlgEquiv.refl : B ≃ₐ[Oδ] B) ψ).toRingEquiv).trans885      ((Algebra.TensorProduct.cancelBaseChange O Oδ Oδ B K).toRingEquiv.trans886        (Algebra.TensorProduct.comm O B K).toRingEquiv)887  let E₀ : TensorProduct Oδ Kδ B ≃+* (∀ i, L i) := Θ.trans e.toRingEquiv888  let f : ∀ i, Kδ →+* L i := fun i =>889    (Pi.evalRingHom L i).comp (E₀.toRingHom.comp Algebra.TensorProduct.includeLeftRingHom)890  let iA : ∀ i, Algebra Kδ (L i) := fun i => (f i).toAlgebra891  let iB : ∀ i, Algebra Oδ (L i) := fun i => ((algebraMap Kδ (L i)).comp892      (algebraMap Oδ Kδ)).toAlgebra893  have iC : ∀ i, IsScalarTower Oδ Kδ (L i) := fun i => IsScalarTower.of_algebraMap_eq (fun _ => rfl)894  let φ : K →+* Kδ := ψ.symm.toRingHom.comp Algebra.TensorProduct.includeRight.toRingHom895  let : Algebra K Kδ := φ.toAlgebra896  have hΘ : ∀ k : K, Θ (φ k ⊗ₜ 1) = k ⊗ₜ 1 := by897    intro k898    simp [Θ, φ]899  have : ∀ i, IsScalarTower K Kδ (L i) := fun i => IsScalarTower.of_algebraMap_eq (fun k => by900    change algebraMap K (L i) k = (e (Θ (φ k ⊗ₜ 1))) i901    rw [hΘ]902    have := e.commutes k903    rw [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply] at this904    rw [this]905    rfl)906  have iD : ∀ i, FiniteDimensional Kδ (L i) := fun i => Module.Finite.of_restrictScalars_finite K Kδ907      (L i)908  refine ⟨iA, iB, iC, iD, AlgEquiv.ofRingEquiv (f := E₀) ?_, ?_⟩909  · exact fun r => rfl910  -- the `Oδ`-structure restricts to the `O`-structure through `K`911  have hφO : ∀ c : O, φ (algebraMap O K c) = algebraMap Oδ Kδ (algebraMap O Oδ c) := by912    intro c913    change ψ.symm (Algebra.TensorProduct.includeRight (algebraMap O K c)) = _914    rw [AlgHom.commutes, IsScalarTower.algebraMap_apply O Oδ (TensorProduct O Oδ K)]915    exact ψ.symm.commutes _916  intro i c917  change algebraMap Kδ (L i) (algebraMap Oδ Kδ (algebraMap O Oδ c)) = algebraMap K (L i)918      (algebraMap O K c)919  rw [← hφO, IsScalarTower.algebraMap_apply K Kδ (L i)]920  rfl921 922end SurfaceBlowup