Combinatorics of states, ranks and safety of the laws

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.Formula.LawAlgebra7 8/-!9# Combinatorics of states, ranks and safety of the laws10 11Combinatorial facts about states and their children under one blowup step: positivity of12degrees, the unique self pattern of a single-branch state, strict decrease of the rank along13non-self children (which makes the fuel-based recursion `stateLawFuel` stable), and the14resulting safety (no division by zero at integers `q ≥ 2`) of the local and global laws, hence15regularity of the global formula. Also small arithmetic facts on `tri`, return weights,16divisor probabilities and scaled types.17 18## Main results19 20* `SurfaceBlowup.self_patterns_of_single_state`: `S(a; c)` has a unique self pattern.21* `SurfaceBlowup.nonself_child_rank_lt`: non-self children have strictly smaller rank.22* `SurfaceBlowup.state_fuel_stable`: `stateLawFuel k s = stateLaw s` once `rank s < k`.23* `SurfaceBlowup.state_law_unfold`: the law of a non-terminal state in terms of its exit law24  `exitLaw` (the non-self part of the recursion).25* `SurfaceBlowup.local_law_safe`, `SurfaceBlowup.global_law_safe`: safety of the laws.26* `SurfaceBlowup.global_formula_regular`: the global formula is regular at prime powers.27* `SurfaceBlowup.scale_type_valid_degree_iff`: scaling types by `δ` preserves validity and28  multiplies degrees by `δ`.29 30Provenance: `Thm_SurfaceBlowupV2_*` for self_patterns_of_single_state, state_degree_pos,31equal_degree_child_is_unique, state_weight_le_degree, rank_lt_of_weight_gt, nonself_child_rank_lt,32state_fuel_stable, exitLaw, state_law_unfold, tangent_weight_safe, terminal_law, tri_chooseTwo,33tri_ge_three, return_weight_bounds, divisor_probability_pos, local_law_safe, global_law_safe,34global_coefficients_safe, global_formula_regular, type_degree_scale,35scale_type_valid_degree_iff.36-/37 38open scoped BigOperators ENNReal39 40namespace SurfaceBlowup41 42/-! ### The self pattern of a single-branch state -/43 44/-- Multiplicity of a given "other" child in `otherChildren a m`. -/45private theorem count_otherChildren {n : ℕ} (a : ℕ) (m : Pattern n) (i j : Fin n) :46    (otherChildren a m).count (i.val + 1, State.single a (j.val + 1)) = (m (i, j)).val := by47  unfold otherChildren48  rw [List.count_flatMap, Finset.sum_map_toList]49  simp only [Function.comp, List.count_replicate]50  rw [Finset.sum_eq_single (i,j)]51  · simp52  · intro b _ hb53    refine if_neg fun h ↦ hb ?_54    simp only [beq_iff_eq, Prod.mk.injEq, State.single.injEq, add_left_inj, true_and] at h55    exact Prod.ext (Fin.ext h.1) (Fin.ext h.2)56  · simp57 58/-- The indicator pattern of the cell `(0, c - 1)`. -/59private abbrev IsSelfOther {n : ℕ} (c : ℕ) (m : Pattern n) : Prop :=60  ∀ ij, (m ij).val = if ij.1.val = 0 ∧ ij.2.val + 1 = c then 1 else 061 62/-- Sums over `Fin n × Fin n` of the indicator of the cell `(0, c - 1)`. -/63private theorem sum_selfOther {n : ℕ} (c : ℕ) (hc : 0 < c) (hcn : c ≤ n) (f : Fin n × Fin n → ℕ)64    (hf : ∀ ij, ¬ (ij.1.val = 0 ∧ ij.2.val + 1 = c) → f ij = 0) :65    ∑ ij, f ij = f (⟨0, by omega⟩, ⟨c-1, by omega⟩) := by66  refine Finset.sum_eq_single _ (fun b _ hb ↦ hf b fun ⟨h1, h2⟩ ↦ hb ?_) (by simp)67  exact Prod.ext (Fin.ext h1) (Fin.ext (by simp; omega))68 69private theorem weight_selfOther {n : ℕ} (c : ℕ) (hc : 0 < c) (hcn : c ≤ n) (m : Pattern n)70    (hm : IsSelfOther c m) : patternWeight m = c := by71  unfold patternWeight72  rw [sum_selfOther c hc hcn _ fun ij h ↦ by rw [hm, if_neg h, mul_zero], hm,73    if_pos ⟨rfl, show c - 1 + 1 = c by omega⟩]74  change (0+1)*((c-1)+1)*1 = c; omega75 76private theorem otherChildren_selfOther {n : ℕ} (a c : ℕ) (hc : 0 < c) (hcn : c ≤ n)77    (m : Pattern n) (hm : IsSelfOther c m) :78    otherChildren a m = [(1, State.single a c)] := by79  have h1 : (otherChildren a m).length = 1 := by80    rw [otherChildren, List.length_flatMap, Finset.sum_map_toList]81    simp only [List.length_replicate]82    rw [sum_selfOther c hc hcn _ fun ij h ↦ by rw [hm, if_neg h], hm,83      if_pos ⟨rfl, show c - 1 + 1 = c by omega⟩]84  have h2 := count_otherChildren a m ⟨0, by omega⟩ ⟨c-1, by omega⟩85  rw [hm, if_pos ⟨rfl, show c - 1 + 1 = c by omega⟩] at h286  simp only [show c - 1 + 1 = c by omega] at h287  obtain ⟨y, hy⟩ := List.length_eq_one_iff.1 h188  rw [hy] at h2 ⊢89  by_cases e : y = (1, State.single a c)90  · rw [e]91  · simp [e] at h292 93/-- The unique self pattern of `S(a; c)`. -/94private def selfPattern (a c : ℕ) (hc : 0 < c) (hca : c ≤ a * c) :95    TangentPattern (State.single a c).degree where96  d := ⟨c, by change c < a*c+1; omega⟩97  rt := ⟨0, by change 0 < a*c+1; omega⟩98  rx := ⟨0, by change 0 < a*c+1; omega⟩99  other := fun ij ↦ if ij.1.val = 0 ∧ ij.2.val + 1 = c then ⟨1, by change 1 < a*c+1; omega⟩100    else ⟨0, by change 0 < a*c+1; omega⟩101 102private theorem selfPattern_other (a c : ℕ) (hc : 0 < c) (hca : c ≤ a * c) :103    IsSelfOther c (selfPattern a c hc hca).other := fun ij ↦ by104  simp only [selfPattern]; split_ifs <;> rfl105 106/-- Every allowed self pattern of `S(a; c)` is `selfPattern a c`. -/107private theorem eq_selfPattern (a c : ℕ) (hc : 0 < c) (hca : c ≤ a * c)108    (P : TangentPattern (State.single a c).degree) (hA : Allowed (.single a c) P)109    (hS : SelfPattern (.single a c) P) : P = selfPattern a c hc hca := by110  obtain ⟨a', c', hs, hch⟩ := hS111  cases hs112  have hrt : P.rt.val = 0 := by113    by_contra h114    simp [children, h] at hch115  simp only [children, hrt, if_true, List.nil_append] at hch116  have hm : IsSelfOther c P.other := by117    intro ij118    rw [← count_otherChildren a P.other ij.1 ij.2, hch]119    simp [List.count_cons]120    split_ifs <;> omega121  have hw := weight_selfOther (n := (State.single a c).degree) c hc hca _ hm122  obtain ⟨hd0, hsum, hdc, hrx, hiff⟩ := hA123  obtain ⟨d, rt, rx, other⟩ := P124  simp only at hrt hrx hsum hm hw hd0 hdc hiff125  unfold selfPattern126  congr 1127  · ext; change d.val = c; omega128  · ext; change rt.val = 0; omega129  · ext; change rx.val = 0; omega130  · funext ij; ext; rw [hm]; split_ifs <;> rfl131 132open scoped Classical in133/-- The self patterns among the allowed patterns of `S(a; c)` are exactly `[selfPattern a c]`. -/134private theorem filter_selfPattern_eq (a c : ℕ) (hc : 0 < c) (hca : c ≤ a * c) :135    (allowedPatterns (.single a c)).toList.filter (SelfPattern (.single a c)) =136      [selfPattern a c hc hca] := by137  have hmem : selfPattern a c hc hca ∈138      (allowedPatterns (.single a c)).toList.filter (SelfPattern (.single a c)) := by139    simp only [List.mem_filter, Finset.mem_toList, allowedPatterns, Finset.mem_filter,140      Finset.mem_univ, true_and, decide_eq_true_eq]141    have hw := weight_selfOther (n := (State.single a c).degree) c hc hca _142      (selfPattern_other a c hc hca)143    have ho := otherChildren_selfOther (n := (State.single a c).degree) a c hc hca _144      (selfPattern_other a c hc hca)145    refine ⟨⟨hc, ?_, ?_⟩, a, c, rfl, by simp only [children, ho]; rfl⟩146    · rw [hw]; change 0 + 0 + c = c; omega147    · change c ≤ c ∧ 0 = 0 ∧ (0 < 0 ↔ c < c); omega148  refine ((List.perm_ext_iff_of_nodup ((Finset.nodup_toList _).filter _)149    (List.nodup_singleton _)).2 fun b ↦ ⟨fun hb ↦ ?_, fun hb ↦ ?_⟩).eq_singleton150  · simp only [List.mem_filter, Finset.mem_toList, allowedPatterns, Finset.mem_filter,151      decide_eq_true_eq] at hb152    exact List.mem_singleton.2 (eq_selfPattern a c hc hca b hb.1.2 hb.2)153  · exact List.mem_singleton.1 hb ▸ hmem154 155/-- The tangent count of `selfPattern a c` evaluates to `q`. -/156private theorem tangentCount_selfPattern_eval (a c q : ℕ) (hc : 0 < c) (hca : c ≤ a * c) :157    (tangentCount (.single a c) (selfPattern a c hc hca)).eval (q:ℚ) = q := by158  simp only [tangentCount, divisorCount]159  rw [expression_prod_eval, List.map_map, Finset.prod_map_toList,160    Finset.prod_eq_single (⟨0, by change 0 < a*c; omega⟩ : Fin (State.single a c).degree)]161  · simp only [Function.comp, Expr.eval, selfPattern_other, true_and]162    have hs : (∑ x : Fin (State.single a c).degree, if x.val + 1 = c then 1 else 0) = 1 := by163      rw [Finset.sum_eq_single (⟨c-1, by change c-1 < a*c; omega⟩ :164        Fin (State.single a c).degree)]165      · simp; omega166      · exact fun b _ hb ↦ if_neg fun h ↦ hb (Fin.ext (by simp; omega))167      · simp168    have hp : (∏ x : Fin (State.single a c).degree,169        (((if x.val + 1 = c then 1 else 0 : ℕ)).factorial : ℚ)) = 1 :=170      Finset.prod_eq_one fun j _ ↦ by split_ifs <;> simp171    rw [hs, hp]172    simp [falling, expression_prod_eval, availablePoints, Expr.sub, Expr.neg, Expr.eval]173  · intro b _ hb174    simp [selfPattern_other, Fin.val_ne_iff.2 hb, falling, expression_prod_eval, Expr.eval]175  · simp176 177open scoped Classical in178/-- A single-branch state `S(a; c)` with `c ≥ 2` has exactly one self pattern (of179multiplicity `d = c`, with the state itself as only child), whose tangent count at `q` is180`q`. -/181theorem self_patterns_of_single_state (a c q : ℕ) (ha : 0 < a) (hc : 2 ≤ c) :(6.6)182    (∀ P : TangentPattern (State.single a c).degree, Allowed (State.single a c) P →183        SelfPattern (State.single a c) P →184          P.d.val = c ∧ children (State.single a c) P = [(1, State.single a c)]) ∧185      (((allowedPatterns (State.single a c)).toList.filter (SelfPattern (State.single a c))).map186        fun P ↦ (tangentCount (State.single a c) P).eval q).sum = q := by187  have hc : 0 < c := by omega188  have hca : c ≤ a*c := Nat.le_mul_of_pos_left c ha189  refine ⟨fun P hA hS ↦ ⟨by rw [eq_selfPattern a c hc hca P hA hS]; rfl,190    hS.choose_spec.choose_spec.2⟩, ?_⟩191  simpa [filter_selfPattern_eq a c hc hca] using tangentCount_selfPattern_eval a c q hc hca192 193/-! ### Degrees, weights and ranks -/194 195/-- A valid state has positive degree. -/196private theorem state_degree_pos (s : State) (hs : s.Valid) :197    0 < s.degree := by198  cases s with199  | single a c => exact Nat.mul_pos hs.1 hs.2200  | crossing a b c h =>201    have := Nat.mul_pos hs.1 hs.2.2.1202    change 0 < a*c+b*h203    omega204 205/-- If a child has the same degree as its parent, it is the only child and has residue206degree `1`. -/207private theorem equal_degree_child_is_unique (s : State) (hs : s.Valid)208    (P : TangentPattern s.degree)209    (hP : Allowed s P) (z : ℕ × State) (hz : z ∈ children s P) (heq : z.2.degree = s.degree) :210    children s P = [z] ∧ z.1 = 1 := by211  have hsum := children_degree_identity s hs P hP212  have hD := state_degree_pos s hs213  have hpos : ∀ w ∈ children s P, 0 < w.1 * w.2.degree := fun w hw ↦214    Nat.mul_pos (children_residue_degree_pos s P w hw)215      (state_degree_pos _ (children_valid s hs P hP w hw))216  have hz1 := children_residue_degree_pos s P z hz217  obtain ⟨l1, l2, hL⟩ := List.append_of_mem hz218  have empty : ∀ l : List (ℕ × State), (∀ w ∈ l, w ∈ children s P) →219      (l.map fun z ↦ z.1*z.2.degree).sum = 0 → l = [] := by220    rintro (_ | ⟨a, t⟩) hl h0221    · rfl222    · have := hpos a (hl a (by simp))223      simp only [List.map_cons, List.sum_cons] at h0224      omega225  rw [hL] at hsum226  simp only [List.map_append, List.map_cons, List.sum_append, List.sum_cons, heq] at hsum227  have hge : s.degree ≤ z.1 * s.degree := Nat.le_mul_of_pos_left _ hz1228  obtain rfl := empty l1 (fun w hw ↦ by rw [hL]; simp [hw]) (by omega)229  obtain rfl := empty l2 (fun w hw ↦ by rw [hL]; simp [hw]) (by omega)230  refine ⟨by simpa using hL, Nat.eq_of_mul_eq_mul_right hD ?_⟩231  simp at hsum232  omega233 234/-- The weight of a valid state is at most its degree. -/235private theorem state_weight_le_degree (s : State) (hs : s.Valid) :236    s.weight ≤ s.degree := by237  cases s with238  | single a c => exact Nat.le_mul_of_pos_right a hs.2239  | crossing a b c h =>240    exact Nat.add_le_add (Nat.le_mul_of_pos_right a hs.2.2.1) (Nat.le_mul_of_pos_right b hs.2.2.2)241 242/-- Among valid states of equal degree, larger weight forces smaller rank. -/243private theorem rank_lt_of_weight_gt (s u : State) (hs : s.Valid) (hu : u.Valid)244    (hN : u.degree = s.degree)245    (hw : s.weight < u.weight) :246    u.rank < s.rank := by247  have h1 := state_weight_le_degree s hs248  have h2 := state_weight_le_degree u hu249  have ht : u.tag ≤ 1 := by cases u <;> simp [State.tag]250  unfold State.rank251  rw [hN] at h2 ⊢252  omega253 254/-- Every child of a non-self allowed pattern has strictly smaller rank than its parent. -/255theorem nonself_child_rank_lt (s : State) (hs : s.Valid) (P : TangentPattern s.degree)Contact-size order(6.6)256    (hP : Allowed s P) (hself : ¬ SelfPattern s P) (z : ℕ × State) (hz : z ∈ children s P) :257    z.2.rank < s.rank := by258  have hv := children_valid s hs P hP z hz259  rcases Nat.lt_or_eq_of_le (child_degree_le s hs P hP z hz) with hlt | heq260  · exact rank_lt_of_degree_lt s z.2 hv hlt261  obtain ⟨hch, hz1⟩ := equal_degree_child_is_unique s hs P hP z hz heq262  have hw : s.weight < z.2.weight → z.2.rank < s.rank :=263    rank_lt_of_weight_gt s z.2 hs hv heq264  cases s with265  | single a c =>266    obtain ⟨ha, hc⟩ := hs267    simp only [children, otherChildren, List.mem_append, List.mem_flatMap,268      List.mem_replicate] at hz269    rcases hz with hz | ⟨ij, -, -, rfl⟩270    · split_ifs at hz271      · simp at hz272      · obtain rfl := List.mem_singleton.1 hz273        exact hw (by simp [State.weight]; omega)274    · refine absurd ⟨a, c, rfl, ?_⟩ hself275      have hj : ij.2.val + 1 = c :=276        Nat.eq_of_mul_eq_mul_left ha (by simpa [State.degree] using heq)277      rw [hch]278      simp only at hz1279      rw [hz1, hj]280  | crossing a b c h =>281    obtain ⟨ha, hb, hc, hh⟩ := hs282    simp only [children, otherChildren, List.mem_append, List.mem_flatMap,283      List.mem_replicate] at hz284    rcases hz with (hz | hz) | ⟨ij, -, -, rfl⟩285    pick_goal 3286    · simp only [State.rank, State.weight, State.tag] at heq ⊢287      rw [heq]288      omega289    all_goals290      split_ifs at hz291      · simp at hz292      · obtain rfl := List.mem_singleton.1 hz293        exact hw (by simp [State.weight]; omega)294 295/-- Two fuel values above the rank give the same law (strong induction on a rank bound). -/296private theorem stateLawFuel_stable (n : ℕ) : ∀ (s : State), s.Valid → s.rank < n →297    ∀ k1 k2 : ℕ, s.rank < k1 → s.rank < k2 → stateLawFuel k1 s = stateLawFuel k2 s := by298  classical299  induction n with300  | zero => intro s _ h; omega301  | succ n ih =>302    intro s hs hn k1 k2 h1 h2303    obtain ⟨j1, rfl⟩ : ∃ j, k1 = j + 1 := ⟨k1 - 1, by omega⟩304    obtain ⟨j2, rfl⟩ : ∃ j, k2 = j + 1 := ⟨k2 - 1, by omega⟩305    have hterms : ((allowedPatterns s).toList.flatMap fun P ↦306        if SelfPattern s P then [] else307          lawScale (.mul (tangentCount s P) (divisorProbability s P.d.val))308            (lawProd ((children s P).map fun z ↦ lawDescend z.1 (stateLawFuel j1 z.2)))) =309        ((allowedPatterns s).toList.flatMap fun P ↦310        if SelfPattern s P then [] else311          lawScale (.mul (tangentCount s P) (divisorProbability s P.d.val))312            (lawProd ((children s P).map fun z ↦ lawDescend z.1 (stateLawFuel j2 z.2)))) := by313      simp only [List.flatMap]314      congr 1315      refine List.map_congr_left fun P hP ↦ ?_316      have hA : Allowed s P := by simpa [allowedPatterns] using hP317      split_ifs with hself318      · rfl319      · congr 2320        refine List.map_congr_left fun z hz ↦ ?_321        have hlt := nonself_child_rank_lt s hs P hA hself z hz322        rw [ih z.2 (children_valid s hs P hA z hz) (by omega) j1 j2 (by omega) (by omega)]323    cases s with324    | single a c =>325      rcases c with _ | _ | c326      · simp only [stateLawFuel]; rw [hterms]327      · simp only [stateLawFuel]328      · simp only [stateLawFuel]; rw [hterms]329    | crossing a b c h =>330      simp only [stateLawFuel]; rw [hterms]331 332/-- The fuel-based recursion is stable: any fuel `k > rank s` computes `stateLaw s`. -/333theorem state_fuel_stable (s : State) (hs : s.Valid) (k : ℕ) (hk : s.rank < k) :334    stateLawFuel k s = stateLaw s :=335  stateLawFuel_stable (s.rank + 1) s hs (by omega) k (s.rank + 1) hk (by omega)336 337/-! ### Unfolding the state law -/338 339open scoped Classical in340/-- The non-self part of the recursion of a state `s`: over the allowed tangent patterns `P` that341are not self patterns, the weight `tangentCount · divisorProbability` times the product of the342descended laws of the children of `P`. -/343noncomputable def exitLaw (s : State) : Law :=(6.6)344  (allowedPatterns s).toList.flatMap fun P ↦345    if SelfPattern s P then [] else346      lawScale (.mul (tangentCount s P) (divisorProbability s P.d.val))347        (lawProd ((children s P).map fun z ↦ lawDescend z.1 (stateLaw z.2)))348 349open scoped Classical in350private theorem flatMap_terms_eq_exitLaw (s : State) (hs : s.Valid) :351    ((allowedPatterns s).toList.flatMap fun P ↦352        if SelfPattern s P then [] else353          lawScale (.mul (tangentCount s P) (divisorProbability s P.d.val))354            (lawProd ((children s P).map fun z ↦ lawDescend z.1 (stateLawFuel s.rank z.2))))355      = exitLaw s := by356  unfold exitLaw357  refine List.flatMap_congr fun P hP ↦ ?_358  have hA : Allowed s P := by simpa [allowedPatterns] using hP359  split_ifs with hself360  · rfl361  · congr 2362    refine List.map_congr_left fun z hz ↦ ?_363    rw [state_fuel_stable z.2 (children_valid s hs P hA z hz) s.rank364      (nonself_child_rank_lt s hs P hA hself z hz)]365 366/-- Unfolding of the state law: for a single state it is the exit law rescaled by367`1 / (1 - returnWeight c)`, and for a crossing state it is the exit law itself. -/368theorem state_law_unfold (s : State) (hs : s.Valid) (hnt : s.terminal = false) :(6.7)Theorem 6.2369    (∀ a c : ℕ, s = State.single a c → stateLaw s =370      lawScale (.inv (.sub (.const 1) (returnWeight c))) (exitLaw s)) ∧371      (∀ a b c h : ℕ, s = State.crossing a b c h → stateLaw s = exitLaw s) := by372  refine ⟨?_, ?_⟩373  · rintro a c rfl374    obtain ⟨_, hc⟩ := id hs375    obtain _ | _ | c := c376    · omega377    · simp [State.terminal] at hnt378    · rw [← flatMap_terms_eq_exitLaw _ hs]379      rfl380  · rintro a b c h rfl381    rw [← flatMap_terms_eq_exitLaw _ hs]382    rfl383 384/-! ### Arithmetic of weights and probabilities -/385 386/-- The weight `tangentCount · divisorProbability` of a pattern is safe at all `q ≥ 2`. -/387private theorem tangent_weight_safe (s : State) (P : TangentPattern s.degree) :388    (Expr.mul (tangentCount s P) (divisorProbability s P.d.val)).allSafe := fun q hq ↦389  ⟨divisor_count_safe s.degree _ P.other q hq, divisor_probability_safe s P.d.val q hq⟩390 391/-- The law of the terminal state `S(a; 1)` is the atom `[(a, 1)]`. -/392theorem terminal_law (a : ℕ) :Lemma 2.2393    stateLaw (State.single a 1) = lawAtom a 1 := by394  rw [stateLaw, State.rank, stateLawFuel]395 396/-- `tri d = chooseTwo d + d`. -/397theorem tri_chooseTwo (d : ℕ) :398    tri d = chooseTwo d + d := by399  cases d with400  | zero => simp [tri, chooseTwo]401  | succ n =>402    unfold tri chooseTwo403    have h : (n+1)*(n+1+1) = (n+1)*(n+1-1) + 2*(n+1) := by404      simp only [Nat.add_sub_cancel]; ring405    rw [h, Nat.add_mul_div_left _ _ (by norm_num : 0 < 2)]406 407/-- `tri c ≥ 3` for `c ≥ 2`. -/408private theorem tri_ge_three (c : ℕ) (hc : 2 ≤ c) :409    3 ≤ tri c := by410  unfold tri411  have : 6 ≤ c*(c+1) := by nlinarith412  omega413 414/-- For `q, c ≥ 2`, the return weight `q · q^(-tri c)` lies in `(0, q⁻²]`, in particular415below `1`. -/416theorem return_weight_bounds (q c : ℕ) (hq : 2 ≤ q) (hc : 2 ≤ c) :417    0 < (returnWeight c).eval q ∧ (returnWeight c).eval q ≤ (q : ℚ)⁻¹^2 ∧418      (returnWeight c).eval q < 1 := by419  have hev : (returnWeight c).eval (q:ℚ) = (q:ℚ) * ((q:ℚ)^(tri c))⁻¹ := by420    simp [returnWeight, Expr.eval, expression_pow_eval]421  rw [hev]422  have hq2 : (2:ℚ) ≤ q := by exact_mod_cast hq423  have hqpos : (0:ℚ) < q := by linarith424  have hp3 : (q:ℚ)^3 ≤ (q:ℚ)^(tri c) := pow_le_pow_right₀ (by linarith) (tri_ge_three c hc)425  have hle : (q:ℚ) * ((q:ℚ)^(tri c))⁻¹ ≤ (q:ℚ)⁻¹^2 := by426    calc (q:ℚ) * ((q:ℚ)^(tri c))⁻¹ ≤ (q:ℚ) * ((q:ℚ)^3)⁻¹ :=427          mul_le_mul_of_nonneg_left (inv_anti₀ (by positivity) hp3) hqpos.le428      _ = (q:ℚ)⁻¹^2 := by field_simp429  refine ⟨by positivity, hle, lt_of_le_of_lt hle ?_⟩430  have : (q:ℚ)⁻¹ ≤ 1/2 := by431    rw [one_div]; exact inv_anti₀ (by norm_num) hq2432  have h0 : (0:ℚ) ≤ (q:ℚ)⁻¹ := by positivity433  nlinarith434 435/-- Divisor probabilities and the inverse `1 / (1 - returnWeight c)` are positive at `q ≥ 2`. -/436theorem divisor_probability_pos (q : ℕ) (hq : 2 ≤ q) (s : State) (d c : ℕ) (hc : 2 ≤ c) :437    0 < (divisorProbability s d).eval q ∧438      0 < (Expr.inv (.sub (.const 1) (returnWeight c))).eval q := by439  have hQ : (2:ℚ) ≤ (q:ℚ) := by exact_mod_cast hq440  have hE : (eminusOne).eval q = (q:ℚ) - 1 := by441    simp [eminusOne, Expr.sub, Expr.neg, Expr.eval]; ring442  have hE0 : 0 < (q:ℚ) - 1 := by linarith443  have hP : ∀ n : ℕ, 0 < ((Expr.pow .var n).eval q) := fun n ↦ by444    rw [expression_pow_eval]; simp only [Expr.eval]; positivity445  have hEp : ∀ n : ℕ, 0 < ((Expr.pow eminusOne n).eval q) := fun n ↦ by446    rw [expression_pow_eval, hE]; exact pow_pos hE0 _447  refine ⟨?_, ?_⟩448  · cases s with449    | single a c' => exact mul_pos (inv_pos.mpr (hP _)) (hEp _)450    | crossing a b c' h =>451      simp only [divisorProbability, Expr.eval]452      refine mul_pos (inv_pos.mpr (hP _)) ?_453      split_ifs454      all_goals first455        | exact hEp _456        | (simp only [Expr.eval]; rw [hE]; exact inv_pos.mpr hE0)457  · have := (return_weight_bounds q c hq hc).2.2458    simp only [Expr.sub, Expr.neg, Expr.eval]459    exact inv_pos.mpr (by linarith)460 461/-! ### Safety of the laws -/462 463/-- Products of safe laws are safe. -/464private theorem lawProd_safe (Ls : List Law) (h : ∀ L ∈ Ls, LawSafe L) :465    LawSafe (lawProd Ls) := by466  induction Ls with467  | nil =>468    intro z hz q _469    simp only [lawProd, lawOne, List.foldr_nil, List.mem_singleton] at hz470    subst hz471    trivial472  | cons L Ls ih =>473    exact law_safe_mul _ _ (h L (by simp)) (ih fun M hM ↦ h M (by simp [hM]))474 475open scoped Classical in476/-- The non-self part of the recursion for `stateLaw s` is safe, given safety for states of477smaller rank. -/478private theorem stateLaw_terms_safe (s : State) (hs : s.Valid)479    (ih : ∀ t : State, t.rank < s.rank → t.Valid → LawSafe (stateLaw t)) :480    LawSafe ((allowedPatterns s).toList.flatMap fun P ↦481        if SelfPattern s P then [] else482          lawScale (.mul (tangentCount s P) (divisorProbability s P.d.val))483            (lawProd ((children s P).map fun z ↦ lawDescend z.1 (stateLawFuel s.rank z.2)))) := by484  intro z hz485  rw [List.mem_flatMap] at hz486  obtain ⟨P, hP, hz⟩ := hz487  have hA : Allowed s P := by simpa [allowedPatterns] using hP488  by_cases hself : SelfPattern s P489  · simp [hself] at hz490  · rw [if_neg hself] at hz491    refine law_safe_scale _ _ (tangent_weight_safe s P) (lawProd_safe _ ?_) z hz492    simp only [List.mem_map]493    rintro _ ⟨w, hw, rfl⟩494    have hv := children_valid s hs P hA w hw495    have hr := nonself_child_rank_lt s hs P hA hself w hw496    rw [state_fuel_stable w.2 hv _ hr]497    exact law_safe_descend _ (children_residue_degree_pos s P w hw) _ (ih _ hr hv)498 499/-- The local law of every valid state is safe. -/500theorem local_law_safe (s : State) (hs : s.Valid) :Theorem 6.2501    LawSafe (stateLaw s) := by502  classical503  induction hn : s.rank using Nat.strong_induction_on generalizing s with504  | _ n IH =>505  have hT := stateLaw_terms_safe s hs fun t ht htv ↦ IH t.rank (hn ▸ ht) t htv rfl506  unfold stateLaw507  cases s with508  | single a c =>509    by_cases hc : c = 1510    · subst hc511      intro z hz q _512      simp only [stateLawFuel, lawAtom, List.mem_singleton] at hz513      subst hz514      trivial515    · have hc2 : 2 ≤ c := by have := hs.2; omega516      have hfuel : stateLawFuel ((State.single a c).rank + 1) (State.single a c) =517          lawScale (.inv (.sub (.const 1) (returnWeight c)))518            ((allowedPatterns (State.single a c)).toList.flatMap fun P ↦519              if SelfPattern (State.single a c) P then [] else520                lawScale (.mul (tangentCount (State.single a c) P)521                    (divisorProbability (State.single a c) P.d.val))522                  (lawProd ((children (State.single a c) P).map fun z ↦523                    lawDescend z.1 (stateLawFuel (State.single a c).rank z.2)))) := by524        rw [stateLawFuel]525        all_goals first | rfl | (intro a1 h; cases h; exact hc rfl)526      rw [hfuel]527      refine law_safe_scale _ _ (fun q hq ↦ ?_) hT528      obtain ⟨hpos, -, hlt⟩ := return_weight_bounds q c hq hc2529      have hne : (Expr.pow .var (tri c)).eval (q : ℚ) ≠ 0 := fun h0 ↦ by530        simp [returnWeight, Expr.eval, h0] at hpos531      refine ⟨⟨trivial, trivial, ⟨trivial, expression_pow_safe _ _ _ trivial, hne⟩⟩, ?_⟩532      simp only [Expr.sub, Expr.neg, Expr.eval]533      intro h0534      linarith535  | crossing a b c h =>536    rw [stateLawFuel]537    exact hT538 539/-- The global law (monic for `ε = false`, projective for `ε = true`) of degree `n` is safe. -/540theorem global_law_safe (n : ℕ) (ε : Bool) :541    LawSafe (globalLaw ε n) := by542  have normSafe : (Expr.inv (if ε then projectiveNormalizer n else .pow .var n)).allSafe := by543    intro q hq544    cases ε with545    | true =>546      refine ⟨?_, ne_of_gt (projective_normalizer_positive n q (by positivity))⟩547      refine expression_sum_safe _ _ ?_548      simp only [List.mem_map]549      rintro _ ⟨i, _, rfl⟩550      exact expression_pow_safe _ _ _ trivial551    | false =>552      refine ⟨expression_pow_safe _ _ _ trivial, ?_⟩553      have : (2:ℚ) ≤ q := by exact_mod_cast hq554      simpa [expression_pow_eval, Expr.eval] using pow_ne_zero n (by linarith : (q:ℚ) ≠ 0)555  refine law_safe_scale _ _ normSafe fun z hz ↦ ?_556  simp only [List.mem_flatMap] at hz557  obtain ⟨m, _, hz⟩ := hz558  refine law_safe_scale _ _ (divisor_count_safe _ _ m) (lawProd_safe _ ?_) z hz559  simp only [List.mem_map, otherChildren, List.mem_flatMap, List.mem_replicate]560  rintro _ ⟨w, ⟨ij, _, _, rfl⟩, rfl⟩561  exact law_safe_descend _ (Nat.succ_pos _) _ (local_law_safe _ ⟨Nat.one_pos, Nat.succ_pos _⟩)562 563/-- The coefficients of the monic and projective global laws are safe. -/564theorem global_coefficients_safe (n : ℕ) (σ : FactorType) :565    (monicExpr n σ).allSafe ∧ (projectiveExpr n σ).allSafe := by566  have hsafe : ∀ L : Law, LawSafe L → (lawCoeff L σ).allSafe := by567    intro L hL q hq568    refine expression_sum_safe _ _ fun x hx ↦ ?_569    obtain ⟨z, hz, rfl⟩ := List.mem_map.mp hx570    by_cases h : z.1 = σ571    · simp only [h, if_true]; exact hL z hz q hq572    · simp [h, Expr.safe]573  exact ⟨hsafe _ (global_law_safe n false), hsafe _ (global_law_safe n true)⟩574 575/-- The global formula is regular at every prime power. -/576theorem global_formula_regular (n : ℕ) (σ : FactorType) :Theorem 1.1Theorem 6.2577    FormulaRegular n σ := by578  intro q hq579  have h2 := prime_power_ge_two q hq580  obtain ⟨h1, h3⟩ := global_coefficients_safe n σ581  exact ⟨expression_regular _ _ (h1 q h2), expression_regular _ _ (h3 q h2)⟩582 583/-! ### Scaled types -/584 585/-- `typeDegree (scaleType δ σ) = δ · typeDegree σ`. -/586private theorem type_degree_scale (δ : ℕ) (σ : FactorType) :587    typeDegree (scaleType δ σ) = δ * typeDegree σ := by588  unfold typeDegree scaleType589  rw [Multiset.map_map, ← Multiset.sum_map_mul_left]590  congr 1591  refine Multiset.map_congr rfl fun z _ ↦ ?_592  simp only [Function.comp]593  ring594 595/-- Scaling by `δ > 0` is injective on types, preserves validity, and multiplies the degree596by `δ`. -/597theorem scale_type_valid_degree_iff (δ r : ℕ) (hδ : 0 < δ) (τ : FactorType) :598    ((ValidType (scaleType δ τ) ∧ typeDegree (scaleType δ τ) = δ * r) ↔599      (ValidType τ ∧ typeDegree τ = r)) ∧ Function.Injective (scaleType δ) := by600  refine ⟨?_, ?_⟩601  · have hv : ValidType (scaleType δ τ) ↔ ValidType τ := by602      unfold ValidType scaleType603      simp only [Multiset.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]604      exact forall₂_congr fun z _ ↦ by simp [hδ]605    rw [hv, type_degree_scale, Nat.mul_left_cancel_iff hδ]606  · apply Multiset.map_injective607    intro a b h608    simp only [Prod.mk.injEq] at h609    exact Prod.ext h.1 (Nat.eq_of_mul_eq_mul_left hδ h.2)610 611end SurfaceBlowup