Regression guards for the universal density expressions

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.Main7import Tests.NonVacuity8 9/-!10# Regression guards for the universal density expressions11 12Pins the statement-level definitions of `SurfaceBlowup.Basic` (the recursion `stateLaw`, the global13laws and the universal expressions `monicExpr n σ`, `projectiveExpr n σ`) to independently known14numbers, and turns them, via `SurfaceBlowup.main_dvr`, into explicit density statements. Any change15to the definitions that alters these values breaks this file.16 17## Main results18 19* `SurfaceBlowup.Tests.monicExpr_two_eval`, `SurfaceBlowup.Tests.projectiveExpr_two_eval`: the20  quadratic expressions as rational functions of `q > 1`.21* `SurfaceBlowup.Tests.monicExpr_three_eval`: the cubic monic expressions for `q > 1`.22* `SurfaceBlowup.Tests.monicExpr_four_eval_two`, `SurfaceBlowup.Tests.projectiveExpr_four_eval_two`:23  all quartic values at `q = 2`.24* Point values, e.g. `SurfaceBlowup.Tests.monicExpr_three_totally_ramified_eval_three`25  (`10/121`), `SurfaceBlowup.Tests.monicExpr_four_totally_ramified_eval_two` (`107/1533`),26  `SurfaceBlowup.Tests.projectiveExpr_four_totally_ramified_eval_two` (`856/15841`).27* Density corollaries, e.g. `SurfaceBlowup.Tests.monicDensity_two_ramified` (`1/(q+1)` over every28  complete DVR with residue field of order `q`),29  `SurfaceBlowup.Tests.monicDensity_four_totally_ramified_of_card_eq_two`, and the end-to-end30  `SurfaceBlowup.Tests.monicDensity_powerSeries_zmod_two_four_totally_ramified` over `𝔽₂⟦X⟧`.31 32## Implementation notes33 34The expressions are not computable by brute force (`allowedPatterns` filters a Fintype of size35about `5^19` with classical decidability), so the values are computed by unfolding the recursion36state by state: the coefficient algebra of laws, a one-step unfolding of `stateLaw` (re-derived37here: fuel stability and the rank decrease of children), explicit enumerations of the allowed38tangent and residue patterns (children lists are computed by `decide` through an explicit39enumeration of the cells), and the laws of the small states `S(a;1)`, `S(a;2)`, `T(a,b;1,h)`,40`T(a,b;c,1)`, `T(1,1;2,2)`, `S(1;3)` and (at `q = 2`) `S(1;4)`. Final identities are checked as41linear combinations of type indicators. All of this is private and depends only on42`SurfaceBlowup.Basic` (plus `main_dvr` for the corollaries).43 44Provenance: port of the certified Prove2Me theorems `SurfaceBlowupV2.{quadratic_monic_formula,45quadratic_projective_formula, cubic_monic_formula, quartic_monic_law_at_two,46quartic_projective_law_at_two}` and their point-value corollaries, with their helper closure.47-/48 49set_option autoImplicit false50 51open scoped BigOperators ENNReal52 53namespace SurfaceBlowup.Tests54 55/-- `coeffAt q L σ` is the value at `q` of the coefficient of the type `σ` in the law `L`. -/56local notation "coeffAt " q:max L:max σ:max => Expr.eval q (lawCoeff L σ)57 58/-- Sorts the types `K` of the indicators `indicator σ K` into a canonical form. -/59local macro "sort_types" : tactic => `(tactic| simp only [Multiset.insert_eq_cons,60  Multiset.singleton_add, Multiset.cons_add, zero_add, ← Multiset.cons_zero, Multiset.cons_swap])61 62-- `hygiene false`: the macro names private lemmas of this file declared further below.63set_option hygiene false in64/-- Evaluates coefficients of products of laws of children, terminal ones first. -/65local macro "simp_children" : tactic => `(tactic| simp only [childProd, List.map_cons,66  List.map_nil, stateLaw_terminal, lawDescend_lawAtom, lawProd_cons, lawProd_nil, coeff_mul_lawOne,67  coeff_descend_one, coeff_mul_atom, coeff_lawAtom, coeff_lawOne, ite_mem_erase, ite_add_zero,68  Multiset.cons_zero])69 70/-! ### Evaluating expressions -/71 72section Eval73 74private theorem eval_sum (q : ℚ) (xs : List Expr) :75    (Expr.sum xs).eval q = (xs.map (Expr.eval q)).sum := by76  induction xs with77  | nil => rfl78  | cons x xs ih => rw [Expr.sum, List.foldr_cons, Expr.eval, ← Expr.sum, ih]; rfl79 80private theorem eval_prod (q : ℚ) (xs : List Expr) :81    (Expr.prod xs).eval q = (xs.map (Expr.eval q)).prod := by82  induction xs with83  | nil => rfl84  | cons x xs ih => rw [Expr.prod, List.foldr_cons, Expr.eval, ← Expr.prod, ih]; rfl85 86private theorem eval_pow (q : ℚ) (x : Expr) (n : ℕ) : (x.pow n).eval q = x.eval q ^ n := by87  induction n with88  | zero => simp [Expr.pow, Expr.eval]89  | succ n ih => rw [Expr.pow, Expr.eval, ih, pow_succ]90 91private theorem eval_subst (q : ℚ) (x y : Expr) : (x.subst y).eval q = x.eval (y.eval q) := by92  induction x with93  | const r => rfl94  | var => rfl95  | add x z hx hz => simp only [Expr.subst, Expr.eval, hx, hz]96  | mul x z hx hz => simp only [Expr.subst, Expr.eval, hx, hz]97  | inv x hx => simp only [Expr.subst, Expr.eval, hx]98 99private theorem pointCount_eval (q : ℚ) (n : ℕ) : (pointCount n).eval q =100    1 / n * ∑ j ∈ n.divisors, ((ArithmeticFunction.moebius j : ℤ) : ℚ) * q ^ (n / j) := by101  simp only [pointCount, Expr.eval, eval_sum, List.map_map]102  rw [Finset.sum_map_toList]103  simp [Function.comp_def, Expr.eval, eval_pow]104 105private theorem pointCount_two (q : ℚ) : (pointCount 2).eval q = (q ^ 2 - q) / 2 := by106  rw [pointCount_eval, show Nat.divisors 2 = {1, 2} by decide]107  simp [ArithmeticFunction.moebius_apply_prime Nat.prime_two]108  ring109 110private theorem pointCount_three (q : ℚ) : (pointCount 3).eval q = (q ^ 3 - q) / 3 := by111  rw [pointCount_eval, show Nat.divisors 3 = {1, 3} by decide]112  simp [ArithmeticFunction.moebius_apply_prime Nat.prime_three]113  ring114 115private theorem pointCount_four (q : ℚ) : (pointCount 4).eval q = (q ^ 4 - q ^ 2) / 4 := by116  have h4 : ArithmeticFunction.moebius 4 = 0 :=117    ArithmeticFunction.moebius_apply_prime_pow Nat.prime_two (k := 2) (by norm_num)118  rw [pointCount_eval, show Nat.divisors 4 = {1, 2, 4} by decide]119  simp [ArithmeticFunction.moebius_apply_prime Nat.prime_two, h4]120  ring121 122end Eval123 124/-! ### Coefficients of laws -/125 126section Coefficients127 128private theorem coeff_nil (q : ℚ) (σ : FactorType) : coeffAt q [] σ = 0 := rfl129 130private theorem coeff_cons (q : ℚ) (z : FactorType × Expr) (L : Law) (σ : FactorType) :131    coeffAt q (z :: L) σ = (if z.1 = σ then z.2.eval q else 0) + coeffAt q L σ := by132  simp only [lawCoeff, List.map_cons, Expr.sum, List.foldr_cons, Expr.eval]133  split_ifs <;> rfl134 135private theorem coeff_append (q : ℚ) (L M : Law) (σ : FactorType) :136    coeffAt q (L ++ M) σ = coeffAt q L σ + coeffAt q M σ := by137  induction L with138  | nil => simp [coeff_nil]139  | cons z L ih => rw [List.cons_append, coeff_cons, coeff_cons, ih, add_assoc]140 141private theorem coeff_flatMap {α : Type} (q : ℚ) (l : List α) (f : α → Law) (σ : FactorType) :142    coeffAt q (l.flatMap f) σ = (l.map fun x ↦ coeffAt q (f x) σ).sum := by143  induction l with144  | nil => rfl145  | cons x l ih => rw [List.flatMap_cons, coeff_append, ih, List.map_cons, List.sum_cons]146 147private theorem coeff_scale (q : ℚ) (x : Expr) (L : Law) (σ : FactorType) :148    coeffAt q (lawScale x L) σ = x.eval q * coeffAt q L σ := by149  induction L with150  | nil => simp [coeff_nil, lawScale]151  | cons z L ih =>152    simp only [lawScale, List.map_cons] at *153    rw [coeff_cons, coeff_cons, ih]; simp only [Expr.eval]; split_ifs <;> ring154 155private theorem coeff_lawOne (q : ℚ) (σ : FactorType) :156    coeffAt q lawOne σ = if σ = 0 then 1 else 0 := by157  simp only [lawOne, coeff_cons, coeff_nil, Expr.eval, add_zero, eq_comm]158 159private theorem coeff_prod_singleton (q : ℚ) (L : Law) (σ : FactorType) :160    coeffAt q (lawProd [L]) σ = coeffAt q L σ := by161  induction L with162  | nil => rfl163  | cons z L ih =>164    simp only [lawProd, List.foldr_cons, List.foldr_nil, lawMul, lawOne, List.flatMap_cons,165      List.map_cons, List.map_nil] at *166    rw [List.singleton_append, coeff_cons, coeff_cons, ih]; simp [Expr.eval]167 168private theorem lawProd_cons (L : Law) (Ls : List Law) :169    lawProd (L :: Ls) = lawMul L (lawProd Ls) := rfl170 171private theorem scaleType_injective {δ : ℕ} (hδ : 0 < δ) : Function.Injective (scaleType δ) :=172  Multiset.map_injective fun _ _ h ↦173    Prod.ext (Prod.mk.inj h).1 (Nat.eq_of_mul_eq_mul_left hδ (Prod.mk.inj h).2)174 175private theorem coeff_descend_scaleType (q : ℚ) {δ : ℕ} (hδ : 0 < δ) (L : Law) (τ : FactorType) :176    coeffAt q (lawDescend δ L) (scaleType δ τ) = coeffAt (q ^ δ) L τ := by177  induction L with178  | nil => rfl179  | cons z L ih =>180    simp only [lawDescend, List.map_cons] at *181    rw [coeff_cons, coeff_cons, ih]182    simp only [(scaleType_injective hδ).eq_iff, eval_subst, eval_pow]183    rfl184 185private theorem coeff_descend_of_ne (q : ℚ) (δ : ℕ) (L : Law) (σ : FactorType)186    (h : ∀ τ, σ ≠ scaleType δ τ) : coeffAt q (lawDescend δ L) σ = 0 := by187  induction L with188  | nil => rfl189  | cons z L ih =>190    simp only [lawDescend, List.map_cons] at *191    rw [coeff_cons, ih, if_neg fun e ↦ h _ e.symm, zero_add]192 193private theorem coeff_descend_one (q : ℚ) (L : Law) (σ : FactorType) :194    coeffAt q (lawDescend 1 L) σ = coeffAt q L σ := by195  simpa [scaleType] using coeff_descend_scaleType q one_pos L σ196 197private theorem lawDescend_lawAtom (δ a : ℕ) : lawDescend δ (lawAtom a 1) = lawAtom a δ := by198  simp [lawDescend, lawAtom, scaleType, Expr.subst]199 200private theorem lawProd_nil : lawProd [] = lawOne := rfl201 202private theorem coeff_mul_lawOne (q : ℚ) (L : Law) (σ : FactorType) :203    coeffAt q (lawMul L lawOne) σ = coeffAt q L σ :=204  coeff_prod_singleton q L σ205 206private theorem coeff_lawAtom (q : ℚ) (e f : ℕ) (σ : FactorType) :207    coeffAt q (lawAtom e f) σ = if σ = {(e, f)} then 1 else 0 := by208  simp [lawAtom, coeff_cons, coeff_nil, Expr.eval, eq_comm]209 210private theorem coeff_mul_atom (q : ℚ) (e f : ℕ) (M : Law) (σ : FactorType) :211    coeffAt q (lawMul (lawAtom e f) M) σ =212      if (e, f) ∈ σ then coeffAt q M (σ.erase (e, f)) else 0 := by213  have key : ∀ t : FactorType, {(e, f)} + t = σ ↔ (e, f) ∈ σ ∧ σ.erase (e, f) = t := fun t ↦214    ⟨by rintro rfl; simp [Multiset.singleton_add],215      by rintro ⟨h, rfl⟩; rw [Multiset.singleton_add, Multiset.cons_erase h]⟩216  simp only [lawAtom, lawMul, List.flatMap_cons, List.flatMap_nil, List.append_nil]217  induction M with218  | nil => simp [coeff_nil]219  | cons w M ih =>220    rw [List.map_cons, coeff_cons, ih, coeff_cons]221    simp only [key, Expr.eval, one_mul]222    by_cases h : (e, f) ∈ σ <;> simp [h, eq_comm]223 224private theorem coeff_eq_zero_of_not_mem (q : ℚ) (L : Law) (τ : FactorType)225    (h : τ ∉ (L.map Prod.fst).toFinset) : coeffAt q L τ = 0 := by226  induction L with227  | nil => rfl228  | cons z L ih =>229    simp only [List.map_cons, List.toFinset_cons, Finset.mem_insert, not_or] at h230    rw [coeff_cons, ih h.2, if_neg (Ne.symm h.1), add_zero]231 232private theorem coeff_map_add (q : ℚ) (z : FactorType × Expr) (M : Law) (σ : FactorType) :233    coeffAt q (M.map fun w ↦ (z.1 + w.1, Expr.mul z.2 w.2)) σ =234      if z.1 ≤ σ then z.2.eval q * coeffAt q M (σ - z.1) else 0 := by235  induction M with236  | nil => simp [coeff_nil]237  | cons w M ih =>238    rw [List.map_cons, coeff_cons, coeff_cons, ih]239    by_cases h : z.1 ≤ σ240    · have e : z.1 + w.1 = σ ↔ w.1 = σ - z.1 :=241        ⟨fun e ↦ by rw [← e, add_tsub_cancel_left], fun e ↦ by rw [e, add_tsub_cancel_of_le h]⟩242      simp only [e, if_pos h, Expr.eval]; split_ifs <;> ring243    · have e : ¬ z.1 + w.1 = σ := fun e ↦ h (e ▸ le_self_add)244      simp [h, e]245 246private theorem coeff_mul_of_mem (q : ℚ) (L M : Law) (σ : FactorType) (S : Finset FactorType)247    (hS : ∀ z ∈ L, z.1 ∈ S) : coeffAt q (lawMul L M) σ =248      ∑ τ ∈ S, if τ ≤ σ then coeffAt q L τ * coeffAt q M (σ - τ) else 0 := by249  induction L with250  | nil => simp [lawMul, coeff_nil]251  | cons z L ih =>252    have e : lawMul (z :: L) M = (M.map fun w ↦ (z.1 + w.1, Expr.mul z.2 w.2)) ++ lawMul L M := by253      simp [lawMul]254    rw [e, coeff_append, coeff_map_add, ih fun y hy ↦ hS y (List.mem_cons_of_mem _ hy)]255    have : ∀ τ ∈ S, (if τ ≤ σ then coeffAt q (z :: L) τ * coeffAt q M (σ - τ) else 0) =256        (if z.1 = τ then (if τ ≤ σ then z.2.eval q * coeffAt q M (σ - τ) else 0) else 0) +257          (if τ ≤ σ then coeffAt q L τ * coeffAt q M (σ - τ) else 0) := by258      intro τ _; rw [coeff_cons]; split_ifs <;> ring259    rw [Finset.sum_congr rfl this, Finset.sum_add_distrib, Finset.sum_ite_eq,260      if_pos (hS z (by simp))]261 262/-- The coefficients of a product, summed over any finite set containing the support of the263first factor. -/264private theorem coeff_mul (q : ℚ) (L M : Law) (S : Finset FactorType)265    (hS : ∀ τ ∉ S, coeffAt q L τ = 0) (σ : FactorType) : coeffAt q (lawMul L M) σ =266      ∑ τ ∈ S, if τ ≤ σ then coeffAt q L τ * coeffAt q M (σ - τ) else 0 := by267  set T := (L.map Prod.fst).toFinset268  rw [coeff_mul_of_mem q L M σ T fun z hz ↦ List.mem_toFinset.2 (List.mem_map_of_mem hz)]269  rw [Finset.sum_subset (Finset.subset_union_left (s₂ := S)) fun τ _ hτ ↦ by270      simp [coeff_eq_zero_of_not_mem q L τ hτ],271    ← Finset.sum_subset (Finset.subset_union_right (s₁ := T)) fun τ _ hτ ↦ by simp [hS τ hτ]]272 273/-- The coefficient of `σ` in the law `M` with all types shifted by `τ`. -/274private noncomputable def shiftedCoeff (q : ℚ) (M : Law) (τ σ : FactorType) : ℚ :=275  (M.map fun w ↦ if τ + w.1 = σ then w.2.eval q else 0).sum276 277private theorem shiftedCoeff_mul (q : ℚ) (L M : Law) (τ σ : FactorType) :278    shiftedCoeff q (lawMul L M) τ σ =279      (L.map fun z ↦ z.2.eval q * shiftedCoeff q M (τ + z.1) σ).sum := by280  induction L with281  | nil => simp [shiftedCoeff, lawMul]282  | cons z L ih =>283    have : lawMul (z :: L) M = (M.map fun w ↦ (z.1 + w.1, Expr.mul z.2 w.2)) ++ lawMul L M := by284      simp [lawMul]285    rw [this]286    unfold shiftedCoeff at ih ⊢287    rw [List.map_append, List.sum_append, ih, List.map_cons, List.sum_cons, List.map_map,288      ← List.sum_map_mul_left]289    congr 2290    refine List.map_congr_left fun w _ ↦ ?_291    simp only [Function.comp, add_assoc]292    split_ifs <;> simp [Expr.eval]293 294private theorem list_sum_comm {α β : Type} (l : List α) (m : List β) (f : α → β → ℚ) :295    (l.map fun a ↦ (m.map fun b ↦ f a b).sum).sum =296      (m.map fun b ↦ (l.map fun a ↦ f a b).sum).sum := by297  induction l with298  | nil => simp299  | cons a l ih =>300    simp only [List.map_cons, List.sum_cons, ih]301    clear ih302    induction m with303    | nil => simp304    | cons b m ihm => simp only [List.map_cons, List.sum_cons]; rw [← ihm]; ring305 306private theorem shiftedCoeff_prod_perm (q : ℚ) {Ls Ls' : List Law} (hperm : Ls.Perm Ls') :307    ∀ τ σ, shiftedCoeff q (lawProd Ls) τ σ = shiftedCoeff q (lawProd Ls') τ σ := by308  induction hperm with309  | nil => intros; rfl310  | cons x _ ih =>311    intro τ σ312    simp only [lawProd_cons, shiftedCoeff_mul, ih]313  | swap x y l =>314    intro τ σ315    simp only [lawProd_cons, shiftedCoeff_mul, ← List.sum_map_mul_left]316    rw [list_sum_comm]317    refine congrArg _ (List.map_congr_left fun w _ ↦318      congrArg _ (List.map_congr_left fun z _ ↦ ?_))319    rw [add_right_comm τ w.1 z.1]320    ring321  | trans _ _ ih1 ih2 => intro τ σ; rw [ih1, ih2]322 323/-- Coefficients of products of laws do not depend on the order of the factors. -/324private theorem coeff_prod_perm {Ls Ls' : List Law} (hperm : Ls.Perm Ls') (q : ℚ)325    (σ : FactorType) : coeffAt q (lawProd Ls) σ = coeffAt q (lawProd Ls') σ := by326  have h : ∀ M : Law, coeffAt q M σ = shiftedCoeff q M 0 σ := fun M ↦ by327    unfold lawCoeff shiftedCoeff328    rw [eval_sum, List.map_map]329    exact congrArg _ (List.map_congr_left fun w _ ↦ by330      by_cases h : w.1 = σ <;> simp [h, Expr.eval])331  rw [h, h, shiftedCoeff_prod_perm q hperm]332 333/-- The indicator `[σ = K]`. -/334private def indicator (σ K : FactorType) : ℚ := if σ = K then 1 else 0335 336private theorem ite_eq_mul_indicator (σ K : FactorType) (c : ℚ) [Decidable (σ = K)] :337    (if σ = K then c else 0) = c * indicator σ K := by338  unfold indicator; split_ifs <;> simp339 340private theorem ite_mem_erase (p : ℕ × ℕ) (σ t : FactorType) (x : ℚ) :341    (if p ∈ σ then (if σ.erase p = t then x else 0) else 0) = if σ = p ::ₘ t then x else 0 := by342  by_cases h : p ∈ σ343  · rw [if_pos h]344    by_cases h2 : σ.erase p = t345    · rw [if_pos h2, if_pos]; rw [← h2, Multiset.cons_erase h]346    · rw [if_neg h2, if_neg]; rintro rfl; exact h2 (by simp)347  · rw [if_neg h, if_neg]; rintro rfl; exact h (by simp)348 349private theorem ite_add_zero (c : Prop) [Decidable c] (a b : ℚ) :350    (if c then a + b else 0) = (if c then a else 0) + (if c then b else 0) := by351  split_ifs <;> simp352 353private theorem ite_le_sub (t σ u : FactorType) (c d : ℚ) :354    (if t ≤ σ then c * (if σ - t = u then d else 0) else 0) = if σ = t + u then c * d else 0 := by355  by_cases h : σ = t + u356  · subst h; simp357  · rw [if_neg h]358    split_ifs with h1 h2359    · exact absurd (by rw [← h2, add_tsub_cancel_of_le h1]) h360    · simp361    · rfl362 363private theorem ite_le_sub_one (t σ u : FactorType) (d : ℚ) :364    (if t ≤ σ then (if σ - t = u then d else 0) else 0) = if σ = t + u then d else 0 := by365  simpa using ite_le_sub t σ u 1 d366 367end Coefficients368 369/-! ### Patterns -/370 371section Patterns372 373/-- The pattern with the single nonzero entry `v` at `ij₀`. -/374private def spat {n : ℕ} (ij₀ : Fin n × Fin n) (v : Fin (n + 1)) : Pattern n :=375  fun ij ↦ if ij = ij₀ then v else 0376 377private theorem spat_val {n : ℕ} (ij₀ : Fin n × Fin n) (v : Fin (n + 1)) (ij : Fin n × Fin n) :378    ((spat ij₀ v ij : Fin (n+1)) : ℕ) = if ij = ij₀ then (v : ℕ) else 0 := by379  unfold spat; split_ifs <;> simp380 381private theorem eq_spat {n : ℕ} (m : Pattern n) (ij₀ : Fin n × Fin n) (v : Fin (n + 1))382    (h₀ : (m ij₀).val = v.val) (h : ∀ ij, ij ≠ ij₀ → (m ij).val = 0) : m = spat ij₀ v := by383  funext ij; apply Fin.ext; rw [spat_val]384  split_ifs with hij385  · subst hij; exact h₀386  · exact h ij hij387 388private theorem flatMap_replicate_eq {α β : Type} (l : List α) (x₀ : α) (g : α → β) (f : α → ℕ)389    (hf : ∀ x, x ≠ x₀ → f x = 0) (hnd : l.Nodup) (hm : x₀ ∈ l) :390    l.flatMap (fun x ↦ List.replicate (f x) (g x)) = List.replicate (f x₀) (g x₀) := by391  induction l with392  | nil => simp at hm393  | cons y l ih =>394    rw [List.flatMap_cons]395    rw [List.nodup_cons] at hnd396    by_cases h : y = x₀397    · subst h398      rw [List.flatMap_eq_nil_iff.2]399      · simp400      · intro x hx; rw [hf x (fun e ↦ hnd.1 (e ▸ hx))]; rfl401    · rw [hf y h, ih hnd.2 ((List.mem_cons.1 hm).resolve_left (Ne.symm h))]; rfl402 403private theorem otherChildren_spat {n : ℕ} (a : ℕ) (ij₀ : Fin n × Fin n) (v : Fin (n + 1)) :404    otherChildren a (spat ij₀ v) = List.replicate v (ij₀.1.val+1, .single a (ij₀.2.val+1)) := by405  unfold otherChildren406  rw [flatMap_replicate_eq _ ij₀407    (fun ij : Fin n × Fin n ↦ (ij.1.val+1, State.single a (ij.2.val+1)))408    (fun ij ↦ (spat ij₀ v ij : ℕ)) (fun x hx ↦ by rw [spat_val, if_neg hx])409    (Finset.nodup_toList _) (Finset.mem_toList.2 (Finset.mem_univ _)), spat_val, if_pos rfl]410 411private theorem patternWeight_spat {n : ℕ} (ij₀ : Fin n × Fin n) (v : Fin (n + 1)) :412    patternWeight (spat ij₀ v) = (ij₀.1.val+1)*(ij₀.2.val+1)*v := by413  unfold patternWeight414  rw [Finset.sum_eq_single ij₀]415  · rw [spat_val, if_pos rfl]416  · intro ij _ h; rw [spat_val, if_neg h]; simp417  · simp418 419private theorem divisorCount_eval {n : ℕ} (q : ℚ) (off : ℤ) (m : Pattern n) :420    (divisorCount off m).eval q = ∏ i : Fin n,421      (falling (availablePoints off (i.val+1)) (∑ j, (m (i, j)).val)).eval q *422        (1 / ∏ j, ((m (i, j)).val.factorial : ℚ)) := by423  simp only [divisorCount, eval_prod, List.map_map, Finset.prod_map_toList]424  rfl425 426private theorem divisorCount_spat {n : ℕ} (q : ℚ) (off : ℤ) (ij₀ : Fin n × Fin n)427    (v : Fin (n + 1)) :428    (divisorCount off (spat ij₀ v)).eval q =429      (falling (availablePoints off (ij₀.1.val+1)) v).eval q / ((v : ℕ).factorial : ℚ) := by430  rw [divisorCount_eval, Finset.prod_eq_single ij₀.1 _ (by simp)]431  · have h1 : (∑ j, ((spat ij₀ v (ij₀.1, j)) : ℕ)) = v := by432      rw [Finset.sum_eq_single ij₀.2 (fun j _ hj ↦ by simp [spat_val, Prod.ext_iff, hj]) (by simp),433        spat_val, if_pos rfl]434    have h2 : (∏ j, (((spat ij₀ v (ij₀.1, j)) : ℕ).factorial : ℚ)) = ((v : ℕ).factorial : ℚ) := by435      rw [Finset.prod_eq_single ij₀.2 (fun j _ hj ↦ by simp [spat_val, Prod.ext_iff, hj])436        (by simp), spat_val, if_pos rfl]437    rw [h1, h2]; ring438  · intro i _ hi439    have h1 : (∑ j, ((spat ij₀ v (i, j)) : ℕ)) = 0 :=440      Finset.sum_eq_zero fun j _ ↦ by simp [spat_val, Prod.ext_iff, hi]441    have h2 : (∏ j, (((spat ij₀ v (i, j)) : ℕ).factorial : ℚ)) = 1 :=442      Finset.prod_eq_one fun j _ ↦ by simp [spat_val, Prod.ext_iff, hi]443    simp [h1, h2, falling, Expr.prod, Expr.eval]444 445private theorem divisorCount_zero {n : ℕ} (q : ℚ) (off : ℤ) :446    (divisorCount off fun _ : Fin n × Fin n ↦ (0 : Fin (n+1))).eval q = 1 := by447  simp [divisorCount_eval, falling, Expr.prod, Expr.eval]448 449private theorem divisorCount_cell {n : ℕ} (q : ℚ) (off : ℤ) (a b : ℕ) (ha : a < n) (hb : b < n)450    (v : Fin (n + 1)) :451    (divisorCount off fun ij : Fin n × Fin n ↦452      if ij.1.val = a ∧ ij.2.val = b then v else 0).eval q =453      (falling (availablePoints off (a+1)) v).eval q / ((v : ℕ).factorial : ℚ) := by454  rw [show (fun ij : Fin n × Fin n ↦ if ij.1.val = a ∧ ij.2.val = b then v else 0) =455      spat (⟨a, ha⟩, ⟨b, hb⟩) v from funext fun ij ↦ by simp [spat, Prod.ext_iff, Fin.ext_iff],456    divisorCount_spat]457 458/-- A cell whose weight `(i + 1)(j + 1)` exceeds the total weight is empty. -/459private theorem cell_eq_zero {n : ℕ} (m : Pattern n) (ij : Fin n × Fin n)460    (h : patternWeight m < (ij.1.val + 1) * (ij.2.val + 1)) : (m ij).val = 0 := by461  have hle : (ij.1.val+1)*(ij.2.val+1)*(m ij).val ≤ patternWeight m :=462    Finset.single_le_sum (f := fun ij : Fin n × Fin n ↦ (ij.1.val+1)*(ij.2.val+1)*(m ij).val)463      (fun _ _ ↦ Nat.zero_le _) (Finset.mem_univ ij)464  by_contra hc465  exact absurd (hle.trans_lt h) (not_lt.2 (Nat.le_mul_of_pos_right _ (Nat.pos_of_ne_zero hc)))466 467private theorem pattern_eq_zero {n : ℕ} (m : Pattern n) (h : patternWeight m = 0)468    (ij₀ : Fin n × Fin n) : m = spat ij₀ 0 :=469  eq_spat _ _ _ (cell_eq_zero m ij₀ (by rw [h]; positivity))470    fun ij _ ↦ cell_eq_zero m ij (by rw [h]; positivity)471 472private theorem pattern_eq_of_weight_one {n : ℕ} (hn : 0 < n) (m : Pattern n)473    (h : patternWeight m = 1) : m = spat (⟨0, hn⟩, ⟨0, hn⟩) ⟨1, by omega⟩ := by474  have hz : ∀ ij, ij ≠ (⟨0, hn⟩, ⟨0, hn⟩) → (m ij).val = 0 := by475    rintro ⟨i, j⟩ hij476    have : 0 < i.val ∨ 0 < j.val := by477      by_contra hc; push Not at hc478      exact hij (Prod.ext (Fin.ext (by simp; omega)) (Fin.ext (by simp; omega)))479    refine cell_eq_zero m _ ?_480    rw [h]; change 1 < (i.val+1)*(j.val+1)481    rcases this with hi | hi <;> nlinarith482  refine eq_spat _ _ _ ?_ hz483  have : patternWeight m = (m (⟨0, hn⟩, ⟨0, hn⟩)).val := by484    rw [patternWeight, Finset.sum_eq_single (⟨0, hn⟩, ⟨0, hn⟩) (fun ij _ hij ↦ by simp [hz ij hij])485      (by simp)]486    simp487  simp only; omega488 489private theorem pattern_eq_of_weight_two {n : ℕ} (hn : 2 ≤ n) (m : Pattern n)490    (h : patternWeight m = 2) :491    m = spat (⟨0, Nat.lt_of_lt_of_le Nat.two_pos hn⟩, ⟨0, Nat.lt_of_lt_of_le Nat.two_pos hn⟩)492        ⟨2, Nat.lt_succ_of_le hn⟩ ∨493    m = spat (⟨0, Nat.lt_of_lt_of_le Nat.two_pos hn⟩, ⟨1, Nat.lt_of_lt_of_le Nat.one_lt_two hn⟩)494        ⟨1, Nat.succ_lt_succ (Nat.lt_of_lt_of_le Nat.two_pos hn)⟩ ∨495    m = spat (⟨1, Nat.lt_of_lt_of_le Nat.one_lt_two hn⟩, ⟨0, Nat.lt_of_lt_of_le Nat.two_pos hn⟩)496        ⟨1, Nat.succ_lt_succ (Nat.lt_of_lt_of_le Nat.two_pos hn)⟩ := by497  set x00 : Fin n × Fin n := (⟨0, by omega⟩, ⟨0, by omega⟩)498  set x01 : Fin n × Fin n := (⟨0, by omega⟩, ⟨1, by omega⟩)499  set x10 : Fin n × Fin n := (⟨1, by omega⟩, ⟨0, by omega⟩)500  have hz : ∀ ij, ij ≠ x00 → ij ≠ x01 → ij ≠ x10 → (m ij).val = 0 := by501    rintro ⟨⟨i, hi⟩, ⟨j, hj⟩⟩ h0 h1 h2502    refine cell_eq_zero m _ (h ▸ ?_)503    simp only [x00, x01, x10, ne_eq, Prod.mk.injEq, Fin.mk.injEq] at h0 h1 h2 ⊢504    rcases i with _ | _ | i <;> rcases j with _ | _ | j <;> simp_all505    nlinarith506  have hsum : patternWeight m = (m x00).val + 2*(m x01).val + 2*(m x10).val := by507    unfold patternWeight508    rw [← Finset.sum_subset (Finset.subset_univ ({x00, x01, x10} : Finset (Fin n × Fin n)))]509    · rw [Finset.sum_insert (by simp [x00, x01, x10]), Finset.sum_insert (by simp [x01, x10]),510        Finset.sum_singleton]511      simp [x00, x01, x10]; ring512    · intro ij _ hij513      simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hij514      rw [hz ij hij.1 hij.2.1 hij.2.2]; simp515  rcases (by omega : ((m x00).val = 2 ∧ (m x01).val = 0 ∧ (m x10).val = 0) ∨516      ((m x00).val = 0 ∧ (m x01).val = 1 ∧ (m x10).val = 0) ∨517      ((m x00).val = 0 ∧ (m x01).val = 0 ∧ (m x10).val = 1))518    with ⟨e0, e1, e2⟩ | ⟨e0, e1, e2⟩ | ⟨e0, e1, e2⟩519  · refine .inl (eq_spat _ _ _ e0 fun ij hij ↦ ?_)520    by_cases h1 : ij = x01; · rw [h1, e1]521    by_cases h2 : ij = x10; · rw [h2, e2]522    exact hz ij hij h1 h2523  · refine .inr (.inl (eq_spat _ _ _ e1 fun ij hij ↦ ?_))524    by_cases h1 : ij = x00; · rw [h1, e0]525    by_cases h2 : ij = x10; · rw [h2, e2]526    exact hz ij h1 hij h2527  · refine .inr (.inr (eq_spat _ _ _ e2 fun ij hij ↦ ?_))528    by_cases h1 : ij = x00; · rw [h1, e0]529    by_cases h2 : ij = x01; · rw [h2, e1]530    exact hz ij h1 h2 hij531 532private theorem univ_toList_perm (n : ℕ) :533    (Finset.univ : Finset (Fin n × Fin n)).toList.Perm (List.finRange n ×ˢ List.finRange n) :=534  List.perm_of_nodup_nodup_toFinset_eq (Finset.nodup_toList _)535    ((List.nodup_finRange n).product (List.nodup_finRange n))536    (by ext ⟨a, b⟩; simp [List.mem_product])537 538/-- `otherChildren` with an explicit enumeration of the cells (computable by `decide`). -/539private def otherChildrenList {n : ℕ} (a : ℕ) (m : Pattern n) : List (ℕ × State) :=540  (List.finRange n ×ˢ List.finRange n).flatMap fun ij ↦541    List.replicate (m ij).val (ij.1.val+1, State.single a (ij.2.val+1))542 543private theorem otherChildren_perm {n : ℕ} (a : ℕ) (m : Pattern n) {l : List (ℕ × State)}544    (h : (otherChildrenList a m).Perm l) : (otherChildren a m).Perm l :=545  ((univ_toList_perm n).flatMap_right _).trans h546 547/-- The product of the descended laws of a list of children. -/548private noncomputable def childProd (l : List (ℕ × State)) : Law :=549  lawProd (l.map fun z ↦ lawDescend z.1 (stateLaw z.2))550 551private theorem coeff_childProd_perm {l l' : List (ℕ × State)} (h : l.Perm l') (q : ℚ)552    (σ : FactorType) : coeffAt q (childProd l) σ = coeffAt q (childProd l') σ :=553  coeff_prod_perm (h.map _) q σ554 555private theorem coeff_otherChildren {n : ℕ} (m : Pattern n) (l : List (ℕ × State))556    (h : (otherChildrenList 1 m).Perm l) (q : ℚ) (σ : FactorType) :557    coeffAt q (childProd (otherChildren 1 m)) σ = coeffAt q (childProd l) σ :=558  coeff_childProd_perm (otherChildren_perm 1 m h) q σ559 560end Patterns561 562/-! ### Unfolding the recursion563 564These facts are re-derived here (and not imported from the development) so that this file depends565only on the definitions in `SurfaceBlowup.Basic`. -/566 567section Recursion568 569private theorem mem_otherChildren {n : ℕ} {a : ℕ} {m : Pattern n} {z : ℕ × State}570    (h : z ∈ otherChildren a m) :571    ∃ ij : Fin n × Fin n, z = (ij.1.val+1, .single a (ij.2.val+1)) := by572  simp only [otherChildren, List.mem_flatMap, List.mem_replicate] at h573  obtain ⟨ij, -, -, rfl⟩ := h574  exact ⟨ij, rfl⟩575 576private theorem children_valid (s : State) (hs : s.Valid) (P : TangentPattern s.degree)577    (hP : Allowed s P) (z : ℕ × State) (hz : z ∈ children s P) : z.2.Valid := by578  have other : ∀ a (m : Pattern s.degree), 0 < a → z ∈ otherChildren a m → z.2.Valid :=579    fun a m ha h ↦ by obtain ⟨ij, rfl⟩ := mem_otherChildren h; exact ⟨ha, Nat.succ_pos _⟩580  obtain ⟨-, -, hrest⟩ := hP581  cases s with582  | single a c =>583    obtain ⟨ha, hc⟩ := hs584    obtain ⟨-, -, hrt⟩ := hrest585    rcases List.mem_append.1 hz with hz | hz586    · split_ifs at hz with h0587      · simp at hz588      · obtain rfl := List.mem_singleton.1 hz589        exact ⟨ha, ha, Nat.pos_of_ne_zero h0, by have := hrt.mp (Nat.pos_of_ne_zero h0); omega⟩590    · exact other a _ ha hz591  | crossing a b c h =>592    obtain ⟨ha, hb, hc, hh⟩ := hs593    obtain ⟨-, -, hrt, hrx⟩ := hrest594    simp only [children, List.mem_append] at hz595    rcases hz with (hz | hz) | hz596    · split_ifs at hz with h0597      · simp at hz598      · obtain rfl := List.mem_singleton.1 hz599        exact ⟨by omega, ha, Nat.pos_of_ne_zero h0,600          by have := hrt.mp (Nat.pos_of_ne_zero h0); omega⟩601    · split_ifs at hz with h0602      · simp at hz603      · obtain rfl := List.mem_singleton.1 hz604        exact ⟨by omega, hb, Nat.pos_of_ne_zero h0,605          by have := hrx.mp (Nat.pos_of_ne_zero h0); omega⟩606    · exact other (a+b) _ (by omega) hz607 608private theorem weight_le_degree (s : State) (hs : s.Valid) : s.weight ≤ s.degree := by609  cases s with610  | single a c => exact Nat.le_mul_of_pos_right a hs.2611  | crossing a b c h =>612    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)613 614private theorem degree_pos (s : State) (hs : s.Valid) : 0 < s.degree := by615  cases s with616  | single a c => exact Nat.mul_pos hs.1 hs.2617  | crossing a b c h => exact Nat.add_pos_left (Nat.mul_pos hs.1 hs.2.2.1) _618 619private theorem tag_le_one (s : State) : s.tag ≤ 1 := by cases s <;> simp [State.tag]620 621private theorem rank_lt_of_degree_lt (s u : State) (h : u.degree < s.degree) : u.rank < s.rank := by622  have := tag_le_one u623  have h3 : (u.degree + 1) * (u.degree + 1) ≤ s.degree * s.degree := Nat.mul_le_mul h h624  unfold State.rank625  have := Nat.sub_le u.degree u.weight626  nlinarith627 628private theorem rank_lt_of_weight_lt (s u : State) (hs : s.Valid) (hu : u.Valid)629    (hN : u.degree = s.degree) (hw : s.weight < u.weight) : u.rank < s.rank := by630  have := weight_le_degree s hs631  have := weight_le_degree u hu632  have := tag_le_one u633  unfold State.rank634  rw [hN] at *635  omega636 637private theorem otherChildren_degree_sum {n : ℕ} (a : ℕ) (m : Pattern n) :638    ((otherChildren a m).map fun z ↦ z.1*z.2.degree).sum = a * patternWeight m := by639  unfold otherChildren patternWeight640  rw [List.map_flatMap, List.flatMap_def, List.sum_flatten, List.map_map, Finset.mul_sum,641    Finset.sum_map_toList]642  refine Finset.sum_congr rfl fun ij _ ↦ ?_643  simp [List.map_replicate, List.sum_replicate, State.degree]644  ring645 646private theorem children_degree_sum (s : State) (P : TangentPattern s.degree) (hP : Allowed s P) :647    ((children s P).map fun z ↦ z.1*z.2.degree).sum = s.degree := by648  obtain ⟨-, hsum, hrest⟩ := hP649  cases s with650  | single a c =>651    obtain ⟨hdc, hrx, hrt⟩ := hrest652    obtain ⟨W, hW⟩ : ∃ W, patternWeight P.other = W := ⟨_, rfl⟩653    simp only [children, List.map_append, List.sum_append, otherChildren_degree_sum, hW]654    rw [hW] at hsum655    simp only [State.degree]656    generalize P.d.val = D at *657    generalize P.rt.val = R at *658    generalize P.rx.val = X at *659    subst hrx660    obtain ⟨k, rfl⟩ : ∃ k, c = D + k := ⟨c - D, by omega⟩661    subst hsum662    split_ifs with h0663    · obtain rfl : k = 0 := by omega664      subst h0; simp665    · simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]666      rw [Nat.add_sub_cancel_left]; ring667  | crossing a b c h =>668    obtain ⟨hdc, hdh, hrt, hrx⟩ := hrest669    obtain ⟨W, hW⟩ : ∃ W, patternWeight P.other = W := ⟨_, rfl⟩670    simp only [children, List.map_append, List.sum_append, otherChildren_degree_sum, hW]671    rw [hW] at hsum672    simp only [State.degree]673    generalize P.d.val = D at *674    generalize P.rt.val = R at *675    generalize P.rx.val = X at *676    obtain ⟨k, rfl⟩ : ∃ k, c = D + k := ⟨c - D, by omega⟩677    obtain ⟨l, rfl⟩ : ∃ l, h = D + l := ⟨h - D, by omega⟩678    subst hsum679    simp only [Nat.add_sub_cancel_left]680    have e1 : R = 0 → k = 0 := by omega681    have e2 : X = 0 → l = 0 := by omega682    split_ifs <;>683      simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil] <;>684      (try (obtain rfl := e1 ‹R = 0›; subst ‹R = 0›)) <;>685      (try (obtain rfl := e2 ‹X = 0›; subst ‹X = 0›)) <;> ring686 687private theorem children_fst_pos (s : State) (P : TangentPattern s.degree) (z : ℕ × State)688    (hz : z ∈ children s P) : 0 < z.1 := by689  cases s with690  | single a c =>691    rcases List.mem_append.1 hz with hz | hz692    · split_ifs at hz <;> simp at hz; simp [hz]693    · obtain ⟨ij, rfl⟩ := mem_otherChildren hz; simp694  | crossing a b c h =>695    simp only [children, List.mem_append] at hz696    rcases hz with (hz | hz) | hz697    · split_ifs at hz <;> simp at hz; simp [hz]698    · split_ifs at hz <;> simp at hz; simp [hz]699    · obtain ⟨ij, rfl⟩ := mem_otherChildren hz; simp700 701/-- A child of the same degree as its parent is the only child, with residue degree one. -/702private theorem children_eq_singleton (s : State) (hs : s.Valid) (P : TangentPattern s.degree)703    (hP : Allowed s P) (z : ℕ × State) (hz : z ∈ children s P) (heq : z.2.degree = s.degree) :704    children s P = [z] ∧ z.1 = 1 := by705  have hsum := children_degree_sum s P hP706  have hD := degree_pos s hs707  have hpos : ∀ w ∈ children s P, 0 < w.1 * w.2.degree := fun w hw ↦708    Nat.mul_pos (children_fst_pos s P w hw) (degree_pos _ (children_valid s hs P hP w hw))709  have hz1 := children_fst_pos s P z hz710  obtain ⟨l1, l2, hL⟩ := List.append_of_mem hz711  have empty : ∀ l : List (ℕ × State), (∀ w ∈ l, w ∈ children s P) →712      (l.map fun z ↦ z.1*z.2.degree).sum = 0 → l = [] := by713    rintro (_ | ⟨a, t⟩) hl h0714    · rfl715    · have := hpos a (hl a (by simp))716      simp only [List.map_cons, List.sum_cons] at h0717      omega718  rw [hL] at hsum719  simp only [List.map_append, List.map_cons, List.sum_append, List.sum_cons, heq] at hsum720  have hge : s.degree ≤ z.1 * s.degree := Nat.le_mul_of_pos_left _ hz1721  obtain rfl := empty l1 (fun w hw ↦ by rw [hL]; simp [hw]) (by omega)722  obtain rfl := empty l2 (fun w hw ↦ by rw [hL]; simp [hw]) (by omega)723  refine ⟨by simpa using hL, Nat.eq_of_mul_eq_mul_right hD ?_⟩724  simp at hsum725  omega726 727private theorem nonself_child_rank_lt (s : State) (hs : s.Valid) (P : TangentPattern s.degree)728    (hP : Allowed s P) (hself : ¬ SelfPattern s P) (z : ℕ × State) (hz : z ∈ children s P) :729    z.2.rank < s.rank := by730  have hv := children_valid s hs P hP z hz731  have hle : z.2.degree ≤ s.degree := calc732    z.2.degree ≤ z.1 * z.2.degree := Nat.le_mul_of_pos_left _ (children_fst_pos s P z hz)733    _ ≤ ((children s P).map fun z ↦ z.1*z.2.degree).sum :=734      List.single_le_sum (fun _ _ ↦ Nat.zero_le _) _ (List.mem_map.2 ⟨z, hz, rfl⟩)735    _ = s.degree := children_degree_sum s P hP736  rcases Nat.lt_or_eq_of_le hle with hlt | heq737  · exact rank_lt_of_degree_lt s z.2 hlt738  obtain ⟨hch, hz1⟩ := children_eq_singleton s hs P hP z hz heq739  have hw : ∀ u : State, s.weight < u.weight → z.2 = u → z.2.rank < s.rank := by740    rintro u hwu rfl741    exact rank_lt_of_weight_lt s z.2 hs hv heq hwu742  cases s with743  | single a c =>744    simp only [children, otherChildren, List.mem_append, List.mem_flatMap,745      List.mem_replicate] at hz746    rcases hz with hz | ⟨ij, -, -, rfl⟩747    · split_ifs at hz with h0748      · simp at hz749      · obtain rfl := List.mem_singleton.1 hz750        exact hw _ (by have := hs.1; simp [State.weight]; omega) rfl751    · refine absurd ⟨a, c, rfl, ?_⟩ hself752      have hj : ij.2.val + 1 = c :=753        Nat.eq_of_mul_eq_mul_left hs.1 (by simpa [State.degree] using heq)754      rw [hch]755      simp only at hz1756      rw [hz1, hj]757  | crossing a b c h =>758    simp only [children, otherChildren, List.mem_append, List.mem_flatMap,759      List.mem_replicate] at hz760    rcases hz with (hz | hz) | ⟨ij, -, -, rfl⟩761    · split_ifs at hz with h0762      · simp at hz763      · obtain rfl := List.mem_singleton.1 hz764        exact hw _ (by have := hs.1; simp [State.weight]; omega) rfl765    · split_ifs at hz with h0766      · simp at hz767      · obtain rfl := List.mem_singleton.1 hz768        exact hw _ (by have := hs.2.1; simp [State.weight]; omega) rfl769    · simp only [State.rank, State.weight, State.tag] at heq ⊢770      rw [heq]771      omega772 773open scoped Classical in774/-- The recursion sum of a state with fuel `k` for the children. -/775private noncomputable def exitLawFuel (k : ℕ) (s : State) : Law :=776  (allowedPatterns s).toList.flatMap fun P ↦777    if SelfPattern s P then [] else778      lawScale (.mul (tangentCount s P) (divisorProbability s P.d.val))779        (lawProd ((children s P).map fun z ↦ lawDescend z.1 (stateLawFuel k z.2)))780 781open scoped Classical in782/-- The non-self part of the recursion sum of a state, with the children's laws `stateLaw`. -/783private noncomputable def exitLaw (s : State) : Law :=784  (allowedPatterns s).toList.flatMap fun P ↦785    if SelfPattern s P then [] else786      lawScale (.mul (tangentCount s P) (divisorProbability s P.d.val))787        (lawProd ((children s P).map fun z ↦ lawDescend z.1 (stateLaw z.2)))788 789private theorem exitLawFuel_congr (s : State) (hs : s.Valid) (k₁ k₂ : ℕ)790    (h : ∀ z : ℕ × State, z.2.Valid → z.2.rank < s.rank →791      stateLawFuel k₁ z.2 = stateLawFuel k₂ z.2) :792    exitLawFuel k₁ s = exitLawFuel k₂ s := by793  refine List.flatMap_congr fun P hP ↦ ?_794  have hA : Allowed s P := by simpa [allowedPatterns] using hP795  split_ifs with hself796  · rfl797  · refine congrArg _ (congrArg _ (List.map_congr_left fun z hz ↦ ?_))798    rw [h z (children_valid s hs P hA z hz) (nonself_child_rank_lt s hs P hA hself z hz)]799 800/-- One step of the fuelled recursion at a non-terminal state `s`: the recursion sum801`exitLawFuel k s`, scaled by `(1 - returnWeight c)⁻¹` when `s` is a single state of contact `c`. -/802noncomputable def stateLawFuelStep (k : ℕ) (s : State) : Law :=803  match s with804  | .single _ c => lawScale (.inv (.sub (.const 1) (returnWeight c))) (exitLawFuel k s)805  | .crossing _ _ _ _ => exitLawFuel k s806 807private theorem stateLawFuel_succ (k : ℕ) (s : State) (hnt : s.terminal = false) :808    stateLawFuel (k+1) s = stateLawFuelStep k s := by809  rcases s with ⟨a, _ | _ | c⟩ | ⟨a, b, c, h⟩810  · rfl811  · simp [State.terminal] at hnt812  · rfl813  · rfl814 815private theorem stateLawFuel_eq (k : ℕ) (s : State) (hs : s.Valid) (hk : s.rank < k) :816    stateLawFuel k s = stateLaw s := by817  suffices ∀ n s, s.Valid → s.rank < n → ∀ k₁ k₂, s.rank < k₁ → s.rank < k₂ →818      stateLawFuel k₁ s = stateLawFuel k₂ s from this _ s hs (Nat.lt_succ_self _) _ _ hk819      (Nat.lt_succ_self _)820  intro n821  induction n with822  | zero => intro s _ h; omega823  | succ n ih =>824    intro s hs hn k₁ k₂ h₁ h₂825    obtain ⟨j₁, rfl⟩ : ∃ j, k₁ = j + 1 := ⟨k₁ - 1, by omega⟩826    obtain ⟨j₂, rfl⟩ : ∃ j, k₂ = j + 1 := ⟨k₂ - 1, by omega⟩827    have := exitLawFuel_congr s hs j₁ j₂ fun z hz hlt ↦828      ih z.2 hz (by omega) j₁ j₂ (by omega) (by omega)829    rcases s with ⟨a, _ | _ | c⟩ | ⟨a, b, c, h⟩ <;>830      first | rw [stateLawFuel_succ _ _ rfl, stateLawFuel_succ _ _ rfl, stateLawFuelStep,831        stateLawFuelStep, this] | rfl832 833private theorem exitLawFuel_rank (s : State) (hs : s.Valid) : exitLawFuel s.rank s = exitLaw s :=834  List.flatMap_congr fun P hP ↦ by835    have hA : Allowed s P := by simpa [allowedPatterns] using hP836    split_ifs with hself837    · rfl838    · refine congrArg _ (congrArg _ (List.map_congr_left fun z hz ↦ ?_))839      rw [stateLawFuel_eq _ _ (children_valid s hs P hA z hz)840        (nonself_child_rank_lt s hs P hA hself z hz)]841 842private theorem stateLaw_single (a c : ℕ) (hs : (State.single a c).Valid) (hc : c ≠ 1) :843    stateLaw (.single a c) =844      lawScale (.inv (.sub (.const 1) (returnWeight c))) (exitLaw (.single a c)) := by845  rw [stateLaw, stateLawFuel_succ _ _ (by rcases c with _ | _ | c <;> simp_all [State.terminal]),846    stateLawFuelStep, exitLawFuel_rank _ hs]847 848private theorem stateLaw_crossing (a b c h : ℕ) (hs : (State.crossing a b c h).Valid) :849    stateLaw (.crossing a b c h) = exitLaw (.crossing a b c h) := by850  rw [stateLaw, stateLawFuel_succ _ _ rfl, stateLawFuelStep, exitLawFuel_rank _ hs]851 852private theorem stateLaw_terminal (a : ℕ) : stateLaw (.single a 1) = lawAtom a 1 := by853  rw [stateLaw, State.rank, stateLawFuel]854 855open scoped Classical in856/-- The coefficients of `exitLaw s`, as a sum over the allowed patterns. -/857private theorem coeff_exitLaw (q : ℚ) (s : State) (σ : FactorType) : coeffAt q (exitLaw s) σ =858    ∑ P ∈ allowedPatterns s, if SelfPattern s P then 0 else859      ((tangentCount s P).mul (divisorProbability s P.d.val)).eval q *860        coeffAt q (childProd (children s P)) σ := by861  rw [exitLaw, coeff_flatMap, Finset.sum_map_toList]862  refine Finset.sum_congr rfl fun P _ ↦ ?_863  split_ifs864  · rfl865  · rw [coeff_scale]; rfl866 867/-- The coefficients of the global law, as a sum over the residue patterns. -/868private theorem coeff_globalLaw (proj : Bool) (n : ℕ) (q : ℚ) (σ : FactorType) :869    coeffAt q (globalLaw proj n) σ =870      (Expr.inv (if proj then projectiveNormalizer n else .pow .var n)).eval q *871        ∑ m ∈ residuePatterns n, (divisorCount (if proj then 1 else 0) m).eval q *872          coeffAt q (childProd (otherChildren 1 m)) σ := by873  rw [globalLaw, coeff_scale, coeff_flatMap, Finset.sum_map_toList]874  simp only [coeff_scale]; rfl875 876end Recursion877 878/-! ### The laws of the crossing states `T(a,b;c,h)` with `c = 1` or `h = 1` -/879 880section Crossing881 882/-- A crossing state with a unique allowed pattern, of weight one, with a unique child of residue883degree one has the law of that child. -/884private theorem coeff_crossing_of_unique {a b c h : ℕ} (hv : (State.crossing a b c h).Valid)885    (P : TangentPattern (State.crossing a b c h).degree)886    (hA : allowedPatterns (.crossing a b c h) = {P}) (s' : State)887    (hch : children (.crossing a b c h) P = [(1, s')]) (q : ℚ)888    (hX : ((tangentCount (.crossing a b c h) P).mul889      (divisorProbability (.crossing a b c h) P.d.val)).eval q = 1) (σ : FactorType) :890    coeffAt q (stateLaw (.crossing a b c h)) σ = coeffAt q (stateLaw s') σ := by891  rw [stateLaw_crossing _ _ _ _ hv, coeff_exitLaw, hA, Finset.sum_singleton,892    if_neg (by rintro ⟨_, _, h, _⟩; cases h), hX, one_mul, hch, childProd, List.map_singleton,893    coeff_prod_singleton, coeff_descend_one]894 895/-- `T(a,b;1,1)` has the law of the terminal state `S(a+b;1)`. -/896private theorem crossing_one_one_law (a b : ℕ) (ha : 0 < a) (hb : 0 < b) (q : ℚ) (hq : 1 < q)897    (σ : FactorType) :898    coeffAt q (stateLaw (.crossing a b 1 1)) σ = if σ = {(a+b, 1)} then 1 else 0 := by899  have hn : 0 < (State.crossing a b 1 1).degree := by simp [State.degree]; omega900  set D := (State.crossing a b 1 1).degree901  let x : Fin D × Fin D := (⟨0, hn⟩, ⟨0, hn⟩)902  let P : TangentPattern D := ⟨⟨1, by omega⟩, 0, 0, spat x ⟨1, by omega⟩⟩903  have hA : allowedPatterns (.crossing a b 1 1) = {P} := by904    ext Q905    simp only [allowedPatterns, Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_singleton]906    constructor907    · obtain ⟨d, rt, rx, other⟩ := Q908      rintro ⟨h0, hw, h1, h2, h3, h4⟩909      simp only at h0 hw h1 h2 h3 h4910      have hrt : rt.val = 0 := by by_contra h; have := h3.1 (by omega); omega911      have hrx : rx.val = 0 := by by_contra h; have := h4.1 (by omega); omega912      rw [pattern_eq_of_weight_one hn other (by omega)]913      simp only [P, x, TangentPattern.mk.injEq, Fin.ext_iff, Fin.val_zero, and_true]914      omega915    · rintro rfl916      exact ⟨by simp [P], by simp [P, patternWeight_spat, x], by simp [P]⟩917  rw [coeff_crossing_of_unique ⟨ha, hb, one_pos, one_pos⟩ P hA (.single (a+b) 1) ?_ q ?_ σ,918    stateLaw_terminal, coeff_lawAtom]919  · simp [children, P, otherChildren_spat, x]920  · have hq1 : q + -1 ≠ 0 := by linarith921    simp [P, tangentCount, divisorCount_spat, divisorProbability, chooseTwo, falling,922      availablePoints, x, Expr.eval, eminusOne, Expr.sub, Expr.neg, Expr.pow, Expr.prod, hq1]923 924/-- For `c = 1` or `h = 1` (not both) the unique allowed pattern of `T(a,b;c,h)` has weight one925and a unique child, of residue degree one. -/926private theorem crossing_unique_pattern (a b c h : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)927    (hh : 0 < h) (q : ℚ) (hone : c = 1 ∨ h = 1) (hnot : ¬ (c = 1 ∧ h = 1)) :928    ∃ P : TangentPattern (State.crossing a b c h).degree,929      allowedPatterns (State.crossing a b c h) = {P} ∧930      children (State.crossing a b c h) P =931        (if 1 < c then [(1, .crossing (a+b) a 1 (c-1))] else []) ++932        (if 1 < h then [(1, .crossing (a+b) b 1 (h-1))] else []) ∧933      ((tangentCount (State.crossing a b c h) P).mul934        (divisorProbability (State.crossing a b c h) P.d.val)).eval q = 1 := by935  have hn : 1 < (State.crossing a b c h).degree := by936    change 1 < a*c+b*h937    have := Nat.mul_pos ha hc; have := Nat.mul_pos hb hh; omega938  let P : TangentPattern (State.crossing a b c h).degree :=939    ⟨⟨1, by omega⟩, ⟨if 1 < c then 1 else 0, by split_ifs <;> omega⟩,940      ⟨if 1 < h then 1 else 0, by split_ifs <;> omega⟩, fun _ ↦ 0⟩941  have hpw0 : patternWeight P.other = 0 := by simp [patternWeight, P]942  refine ⟨P, ?_, ?_, ?_⟩943  · ext Q944    simp only [allowedPatterns, Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_singleton]945    constructor946    · obtain ⟨d, rt, rx, other⟩ := Q947      rintro ⟨h0, hw, h1, h2, h3, h4⟩948      simp only at h0 hw h1 h2 h3 h4949      have hrt : rt.val = if 1 < c then 1 else 0 := by950        split_ifs with hc1951        · have := h3.2 (by omega); omega952        · by_contra hne; have := h3.1 (by omega); omega953      have hrx : rx.val = if 1 < h then 1 else 0 := by954        split_ifs with hh1955        · have := h4.2 (by omega); omega956        · by_contra hne; have := h4.1 (by omega); omega957      have hpw : patternWeight other = 0 := by rw [hrt, hrx] at hw; split_ifs at hw <;> omega958      have := pattern_eq_zero other hpw (⟨0, by omega⟩, ⟨0, by omega⟩)959      simp only [P, TangentPattern.mk.injEq, Fin.ext_iff, hrt, hrx, true_and]960      refine ⟨by omega, this.trans (funext fun _ ↦ ?_)⟩961      simp [spat]962    · rintro rfl963      refine ⟨by simp [P], ?_, ?_⟩964      · rw [hpw0]; simp only [P]; split_ifs <;> omega965      · simp only [P]; refine ⟨by omega, by omega, ?_, ?_⟩ <;> split_ifs <;> omega966  · simp only [children, show otherChildren (a+b) P.other = [] by simp [otherChildren, P], P,967      List.append_nil]968    rcases hone with rfl | rfl969    · simp [show 1 < h by omega]970    · simp [show 1 < c by omega]971  · have hj : (if 1 < c then 1 else 0) + (if 1 < h then 1 else 0) = 1 := by split_ifs <;> omega972    simp only [Expr.eval, divisorProbability, P, chooseTwo, hj, tangentCount, divisorCount, falling,973      eval_prod]974    simp [Expr.prod, Expr.pow, Expr.eval]975 976/-- `T(a,b;1,h)` has the law of the terminal state `S(a+hb;1)`. -/977private theorem crossing_left_one_law (a b h : ℕ) (ha : 0 < a) (hb : 0 < b) (hh : 0 < h) (q : ℚ)Lemma 2.2978    (hq : 1 < q) (σ : FactorType) :979    coeffAt q (stateLaw (.crossing a b 1 h)) σ = if σ = {(a+h*b, 1)} then 1 else 0 := by980  induction h generalizing a with981  | zero => omega982  | succ h ih =>983    rcases Nat.eq_zero_or_pos h with rfl | h0984    · simpa using crossing_one_one_law a b ha hb q hq σ985    obtain ⟨P, hA, hch, hX⟩ :=986      crossing_unique_pattern a b 1 (h+1) ha hb one_pos (by omega) q (.inl rfl) (by omega)987    rw [if_neg (by omega), if_pos (by omega), List.nil_append, Nat.add_sub_cancel] at hch988    rw [coeff_crossing_of_unique ⟨ha, hb, one_pos, by omega⟩ P hA _ hch q hX,989      ih (a+b) (by omega) h0]990    congr 2; ring_nf991 992/-- `T(a,b;c,1)` has the law of the terminal state `S(ca+b;1)`. -/993private theorem crossing_right_one_law (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (q : ℚ)Lemma 2.2994    (hq : 1 < q) (σ : FactorType) :995    coeffAt q (stateLaw (.crossing a b c 1)) σ = if σ = {(c*a+b, 1)} then 1 else 0 := by996  rcases Nat.lt_or_ge 1 c with hc1 | hc1997  · obtain ⟨P, hA, hch, hX⟩ :=998      crossing_unique_pattern a b c 1 ha hb hc one_pos q (.inr rfl) (by omega)999    rw [if_pos hc1, if_neg (by omega), List.append_nil] at hch1000    rw [coeff_crossing_of_unique ⟨ha, hb, hc, one_pos⟩ P hA _ hch q hX,1001      crossing_left_one_law (a+b) a (c-1) (by omega) ha (by omega) q hq]1002    obtain ⟨k, rfl⟩ : ∃ k, c = k+1 := ⟨c-1, by omega⟩1003    simp only [Nat.add_sub_cancel]1004    congr 2; ring_nf1005  · obtain rfl : c = 1 := by omega1006    simpa using crossing_one_one_law a b ha hb q hq σ1007 1008end Crossing1009 1010/-! ### The law of `S(a;2)` -/1011 1012section SingleTwo1013 1014private theorem returnWeight_eval (q : ℚ) (c : ℕ) :1015    (Expr.inv (.sub (.const 1) (returnWeight c))).eval q = (1 - q / q ^ tri c)⁻¹ := by1016  simp [returnWeight, Expr.eval, Expr.sub, Expr.neg, eval_pow, div_eq_mul_inv, sub_eq_add_neg]1017 1018/-- The tangent-point patterns of `S(a;2)`: a transverse tangent with a node, a double point, a1019point of contact two (a self pattern) and a point of degree two. -/1020private theorem single_two_law (a : ℕ) (ha : 0 < a) (q : ℚ) (hq : 1 < q) (σ : FactorType) :(1.3)Example 6.4Example 7.31021    coeffAt q (stateLaw (.single a 2)) σ = (if σ = {(2*a,1)} then q/(q+1) else 0) +1022      (if σ = {(a,1),(a,1)} then 1/(2*(q+1)) else 0) +1023      (if σ = {(a,2)} then 1/(2*(q+1)) else 0) := by1024  have hn : 2 ≤ (State.single a 2).degree := by simp [State.degree]; omega1025  set D := (State.single a 2).degree1026  let i0 : Fin D := ⟨0, by omega⟩1027  let i1 : Fin D := ⟨1, by omega⟩1028  let f1 : Fin (D+1) := ⟨1, by omega⟩1029  let f2 : Fin (D+1) := ⟨2, by omega⟩1030  let P1 : TangentPattern D := ⟨f1, f1, 0, spat (i0, i0) 0⟩1031  let P2 : TangentPattern D := ⟨f2, 0, 0, spat (i0, i0) f2⟩1032  let P3 : TangentPattern D := ⟨f2, 0, 0, spat (i0, i1) f1⟩1033  let P4 : TangentPattern D := ⟨f2, 0, 0, spat (i1, i0) f1⟩1034  have hA : allowedPatterns (.single a 2) = {P1, P2, P3, P4} := by1035    ext P1036    simp only [allowedPatterns, Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_insert,1037      Finset.mem_singleton]1038    constructor1039    · obtain ⟨d, rt, rx, other⟩ := P1040      rintro ⟨h0, hw, h1, h2, h3⟩1041      simp only at h0 hw h1 h2 h31042      obtain rfl : rx = 0 := Fin.ext h21043      rcases (by omega : d.val = 1 ∨ d.val = 2) with hd | hd1044      · have hrt : rt.val = 1 := by have := h3.1 (by omega); simp at hw; omega1045        left1046        rw [pattern_eq_zero other (by simp at hw; omega) (i0, i0)]1047        simp only [P1, TangentPattern.mk.injEq, Fin.ext_iff, and_true]1048        exact ⟨hd, hrt⟩1049      · obtain rfl : rt = 0 := Fin.ext (by by_contra hc; have := h3.2 (by omega); omega)1050        obtain rfl : d = f2 := Fin.ext hd1051        right1052        rcases pattern_eq_of_weight_two hn other (by simp at hw; omega) with ho | ho | ho <;>1053          rw [ho]1054        · left; rfl1055        · right; left; rfl1056        · right; right; rfl1057    · rintro (rfl | rfl | rfl | rfl) <;> refine ⟨by simp [P1, P2, P3, P4, f1, f2], ?_, ?_⟩ <;>1058        simp [P1, P2, P3, P4, patternWeight_spat, f1, f2, i0, i1]1059  have hi01 : i0 ≠ i1 := by simp [i0, i1]1060  have hne : P1 ≠ P2 ∧ P1 ≠ P3 ∧ P1 ≠ P4 ∧ P2 ≠ P3 ∧ P2 ≠ P4 ∧ P3 ≠ P4 := by1061    refine ⟨by simp [P1, P2, f1, f2], by simp [P1, P3, f1, f2], by simp [P1, P4, f1, f2],1062      ?_, ?_, ?_⟩1063    all_goals intro h1064    · simpa [P2, P3, spat, hi01, f2] using congrArg (fun P ↦ (P.other (i0, i0)).val) h1065    · simpa [P2, P4, spat, hi01, f2] using congrArg (fun P ↦ (P.other (i0, i0)).val) h1066    · simpa [P3, P4, spat, hi01, f1] using congrArg (fun P ↦ (P.other (i0, i1)).val) h1067  rw [stateLaw_single _ _ ⟨ha, two_pos⟩ (by norm_num), coeff_scale, coeff_exitLaw, hA,1068    Finset.sum_insert (by simp [hne]), Finset.sum_insert (by simp [hne]),1069    Finset.sum_insert (by simp [hne]), Finset.sum_singleton]1070  have hch1 : children (.single a 2) P1 = [(1, .crossing a a 1 1)] := by1071    simp [children, P1, f1, otherChildren_spat]1072  have hch2 : children (.single a 2) P2 = [(1, .single a 1), (1, .single a 1)] := by1073    simp [children, P2, f2, otherChildren_spat, i0]1074  have hch3 : children (.single a 2) P3 = [(1, .single a 2)] := by1075    simp [children, P3, f1, otherChildren_spat, i0, i1]1076  have hch4 : children (.single a 2) P4 = [(2, .single a 1)] := by1077    simp [children, P4, f1, otherChildren_spat, i0, i1]1078  have notSelf (P : TangentPattern D) (z : ℕ × State) (hz : children (.single a 2) P = [z])1079      (h : z ≠ (1, .single a 2)) : ¬ SelfPattern (.single a 2) P := by1080    rintro ⟨_, _, he, h'⟩; rw [hz] at h'; simp only [List.cons.injEq] at h'; exact h (he ▸ h'.1)1081  have hS2 : ¬ SelfPattern (.single a 2) P2 := by1082    rintro ⟨_, _, _, h⟩; rw [hch2] at h; simp at h1083  rw [if_neg (notSelf P1 _ hch1 (by simp)), if_neg hS2,1084    if_pos (show SelfPattern (.single a 2) P3 from ⟨a, 2, rfl, hch3⟩),1085    if_neg (notSelf P4 _ hch4 (by simp)), hch1, hch2, hch4]1086  simp only [childProd, List.map_cons, List.map_nil, stateLaw_terminal, lawDescend_lawAtom,1087    lawProd_cons, lawProd_nil, coeff_mul_lawOne, coeff_descend_one,1088    crossing_one_one_law a a ha ha q hq,1089    coeff_mul_atom, coeff_lawAtom, ite_mem_erase]1090  have hq0 : q ≠ 0 := by positivity1091  have hq1 : q - 1 ≠ 0 := by linarith1092  have hN1 : ((tangentCount (.single a 2) P1).mul1093      (divisorProbability (.single a 2) P1.d.val)).eval q = (q - 1) / q := by1094    simp [tangentCount, divisorCount_spat, P1, f1, divisorProbability, tri, Expr.eval, Expr.pow,1095      eminusOne, Expr.sub, Expr.neg, falling, Expr.prod]1096    field_simp; ring1097  have hN2 : ((tangentCount (.single a 2) P2).mul1098      (divisorProbability (.single a 2) P2.d.val)).eval q = q * (q - 1) / 2 / q ^ 3 := by1099    simp [tangentCount, divisorCount_spat, P2, f2, divisorProbability, tri, Expr.eval, Expr.pow,1100      Expr.sub, Expr.neg, falling, Expr.prod, availablePoints, i0, List.range_succ]1101    ring1102  have hN4 : ((tangentCount (.single a 2) P4).mul1103      (divisorProbability (.single a 2) P4.d.val)).eval q = (q ^ 2 - q) / 2 / q ^ 3 := by1104    simp [tangentCount, divisorCount_spat, P4, f1, f2, divisorProbability, tri, Expr.eval, Expr.pow,1105      falling, Expr.prod, availablePoints, i1, pointCount_two, List.range_succ, Expr.sub, Expr.neg]1106    ring1107  have hR : (1 - q / q ^ tri 2)⁻¹ = q ^ 2 / ((q - 1) * (q + 1)) := by1108    rw [show tri 2 = 3 from rfl, inv_eq_iff_eq_inv, inv_div]; field_simp; ring1109  rw [hN1, hN2, hN4, returnWeight_eval, hR, ← two_mul]1110  simp only [Multiset.insert_eq_cons, ite_eq_mul_indicator]1111  have : q + 1 ≠ 0 := by linarith1112  field_simp1113  ring1114 1115end SingleTwo1116 1117/-! ### Quadratic expressions -/1118 1119section Quadratic1120 1121private theorem residuePatterns_two :1122    residuePatterns 2 = {spat (0, 0) 2, spat (1, 0) 1, spat (0, 1) 1} := by1123  unfold residuePatterns; decide1124 1125/-- The global law in degree two: two rational points, a point of degree two, or a point of1126contact two (with the law of `S(1;2)`). -/1127private theorem coeff_globalLaw_two (proj : Bool) (q : ℚ) (σ : FactorType) :1128    coeffAt q (globalLaw proj 2) σ =1129      (Expr.inv (if proj then projectiveNormalizer 2 else .pow .var 2)).eval q *1130        ((divisorCount (if proj then 1 else 0) (spat (n := 2) (0, 0) 2)).eval q *1131            (if σ = {(1,1), (1,1)} then 1 else 0) +1132          ((divisorCount (if proj then 1 else 0) (spat (n := 2) (1, 0) 1)).eval q *1133            (if σ = {(1,2)} then 1 else 0) +1134          (divisorCount (if proj then 1 else 0) (spat (n := 2) (0, 1) 1)).eval q *1135            coeffAt q (stateLaw (.single 1 2)) σ)) := by1136  rw [globalLaw, coeff_scale, coeff_flatMap, Finset.sum_map_toList, residuePatterns_two,1137    Finset.sum_insert (by decide), Finset.sum_insert (by decide), Finset.sum_singleton]1138  simp only [coeff_scale, otherChildren_spat]1139  simp [List.replicate, stateLaw_terminal, lawDescend_lawAtom, lawProd_cons, lawProd_nil,1140    coeff_mul_lawOne, coeff_descend_one, coeff_mul_atom, coeff_lawAtom, ite_mem_erase,1141    Multiset.insert_eq_cons]1142 1143/-- **Quadratic monic densities.** For every `q > 1`, the universal monic expressions of degree `2`1144take the values `q / (2(q + 1))` (split and inert types) and `1 / (q + 1)` (ramified type), and1145vanish on every other type. -/1146theorem monicExpr_two_eval (q : ℚ) (hq : 1 < q) (σ : FactorType) :(1.3)Example 7.3(10.8)(11.8)(11.9)–(11.10)1147    (monicExpr 2 σ).eval q =1148      (if σ = {(1,1), (1,1)} then q / (2 * (q + 1)) else 0) +1149      (if σ = {(1,2)} then q / (2 * (q + 1)) else 0) +1150      (if σ = {(2,1)} then 1 / (q + 1) else 0) := by1151  rw [monicExpr, coeff_globalLaw_two, single_two_law 1 one_pos q hq]1152  simp [divisorCount_spat, falling, availablePoints, Expr.eval, eval_prod, eval_pow, pointCount_two,1153    Expr.sub, Expr.neg, List.range_succ, Multiset.insert_eq_cons, ite_eq_mul_indicator]1154  have : q + 1 ≠ 0 := by positivity1155  have : q ≠ 0 := by positivity1156  field_simp1157  ring1158 1159/-- **Quadratic projective densities.** For every `q > 1`, the universal projective expressions of1160degree `2` take the values `1/2` (split), `(q² - q + 1) / (2(q² + q + 1))` (inert) and1161`q / (q² + q + 1)` (ramified), and vanish on every other type. -/1162theorem projectiveExpr_two_eval (q : ℚ) (hq : 1 < q) (σ : FactorType) :Example 7.3(11.8)1163    (projectiveExpr 2 σ).eval q =1164      (if σ = {(1,1), (1,1)} then 1 / 2 else 0) +1165      (if σ = {(1,2)} then (q ^ 2 - q + 1) / (2 * (q ^ 2 + q + 1)) else 0) +1166      (if σ = {(2,1)} then q / (q ^ 2 + q + 1) else 0) := by1167  rw [projectiveExpr, coeff_globalLaw_two, single_two_law 1 one_pos q hq]1168  simp [divisorCount_spat, falling, availablePoints, Expr.eval, eval_prod, eval_pow, pointCount_two,1169    Expr.sub, Expr.neg, List.range_succ, Multiset.insert_eq_cons, ite_eq_mul_indicator,1170    projectiveNormalizer,1171    eval_sum]1172  have : q + 1 ≠ 0 := by positivity1173  have : q ^ 2 + q + 1 ≠ 0 := by positivity1174  field_simp1175  ring1176 1177end Quadratic1178 1179/-! ### Children of single-boundary states -/1180 1181section SingleChildren1182 1183private theorem children_single_perm {a c : ℕ} (P : TangentPattern (State.single a c).degree)1184    {l : List (ℕ × State)}1185    (h : ((if P.rt.val = 0 then [] else [(1, State.crossing a a P.rt.val (c - P.d.val))]) ++1186      otherChildrenList a P.other).Perm l) : (children (.single a c) P).Perm l :=1187  (List.Perm.append_left _ ((univ_toList_perm _).flatMap_right _)).trans h1188 1189/-- Self patterns, decidably. -/1190private theorem selfPattern_single_iff {a c : ℕ} (P : TangentPattern (State.single a c).degree) :1191    SelfPattern (.single a c) P ↔1192      ((if P.rt.val = 0 then [] else [(1, State.crossing a a P.rt.val (c - P.d.val))]) ++1193        otherChildrenList a P.other).Perm [(1, .single a c)] := by1194  have hp := children_single_perm P (List.Perm.refl _)1195  constructor1196  · rintro ⟨_, _, -, h⟩; exact hp.symm.trans (h ▸ List.Perm.refl _)1197  · intro h; exact ⟨a, c, rfl, List.perm_singleton.1 (hp.trans h)⟩1198 1199end SingleChildren1200 1201/-! ### Degree three: patterns1202 1203Cells `(i, j)` of a pattern record points of degree `i + 1` and contact `j + 1`. -/1204 1205section DegreeThree1206 1207/-- One rational point of contact three (the self pattern of `S(1;3)`). -/1208private abbrev m3Contact : Pattern 3 := fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 2 then 1 else 01209/-- One point of degree three. -/1210private abbrev m3Inert : Pattern 3 := fun ij ↦ if ij.1.val = 2 ∧ ij.2.val = 0 then 1 else 01211/-- Two rational points, of contacts one and two. -/1212private abbrev m3Tangent : Pattern 3 := fun ij ↦1213  if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else if ij.1.val = 0 ∧ ij.2.val = 1 then 1 else 01214/-- A rational point and a point of degree two. -/1215private abbrev m3Quadratic : Pattern 3 := fun ij ↦1216  if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else if ij.1.val = 1 ∧ ij.2.val = 0 then 1 else 01217/-- Three rational points. -/1218private abbrev m3Split : Pattern 3 := fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 3 else 01219 1220private theorem allowed_single_one_three_iff (d rt rx : Fin 4) (m : Pattern 3) :1221    Allowed (State.single 1 3) (⟨d, rt, rx, m⟩ : TangentPattern 3) ↔1222      (⟨d, rt, rx, m⟩ : TangentPattern 3) ∈ ({⟨1, 1, 0, fun _ ↦ 0⟩, ⟨2, 2, 0, fun _ ↦ 0⟩,1223        ⟨2, 1, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else 0⟩, ⟨3, 0, 0, m3Inert⟩,1224        ⟨3, 0, 0, m3Quadratic⟩, ⟨3, 0, 0, m3Tangent⟩, ⟨3, 0, 0, m3Split⟩, ⟨3, 0, 0, m3Contact⟩} :1225        Finset (TangentPattern 3)) := by1226  change 0 < d.val ∧ rt.val + rx.val + patternWeight m = d.val ∧ d.val ≤ 3 ∧ rx.val = 0 ∧1227    (0 < rt.val ↔ d.val < 3) ↔ _1228  simp only [patternWeight, Fintype.sum_prod_type, Fin.sum_univ_three, Finset.mem_insert,1229    Finset.mem_singleton, TangentPattern.mk.injEq, funext_iff, Prod.forall, Fin.forall_fin_succ,1230    Fin.ext_iff, Fin.succ_zero_eq_one, Fin.succ_one_eq_two, IsEmpty.forall_iff, and_true,1231    m3Inert, m3Quadratic, m3Tangent, m3Split, m3Contact]1232  simp only [Fin.isValue, Fin.val_zero, Fin.val_one, Fin.val_two, and_self, and_true, and_false,1233    ↓reduceIte, Nat.reduceEqDiff, show ((3 : Fin 4) : ℕ) = 3 from rfl]1234  have := (m (0,0)).isLt; have := (m (0,1)).isLt; have := (m (0,2)).isLt1235  have := (m (1,0)).isLt; have := (m (1,1)).isLt; have := (m (1,2)).isLt1236  have := (m (2,0)).isLt; have := (m (2,1)).isLt; have := (m (2,2)).isLt1237  have := d.isLt; have := rt.isLt; have := rx.isLt1238  generalize (m (0,0)).val = a00 at *; generalize (m (0,1)).val = a01 at *1239  generalize (m (0,2)).val = a02 at *; generalize (m (1,0)).val = a10 at *1240  generalize (m (1,1)).val = a11 at *; generalize (m (1,2)).val = a12 at *1241  generalize (m (2,0)).val = a20 at *; generalize (m (2,1)).val = a21 at *1242  generalize (m (2,2)).val = a22 at *1243  generalize d.val = dd at *; generalize rt.val = r at *; generalize rx.val = x at *1244  constructor1245  · rintro ⟨h1, h2, h3, h4, h5⟩1246    obtain ⟨rfl, rfl, rfl, rfl, rfl⟩ : a11 = 0 ∧ a12 = 0 ∧ a21 = 0 ∧ a22 = 0 ∧ x = 0 := by omega1247    have : a01 ≤ 1 := by omega1248    have : a10 ≤ 1 := by omega1249    have : a02 ≤ 1 := by omega1250    have : a20 ≤ 1 := by omega1251    have : r ≤ 2 := by omega1252    interval_cases dd <;> interval_cases r <;> (try (exfalso; omega)) <;>1253      interval_cases a00 <;> (try (exfalso; omega)) <;> interval_cases a01 <;>1254      (try (exfalso; omega)) <;> interval_cases a10 <;> (try (exfalso; omega)) <;>1255      interval_cases a02 <;> (try (exfalso; omega)) <;> interval_cases a20 <;>1256      (try (exfalso; omega)) <;> simp1257  · rintro (h|h|h|h|h|h|h|h) <;> omega1258 1259open scoped Classical in1260private def allowedThree : Finset (TangentPattern (State.single 1 3).degree) :=1261  {⟨1, 1, 0, fun _ ↦ 0⟩, ⟨2, 2, 0, fun _ ↦ 0⟩,1262    ⟨2, 1, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else 0⟩, ⟨3, 0, 0, m3Inert⟩,1263    ⟨3, 0, 0, m3Quadratic⟩, ⟨3, 0, 0, m3Tangent⟩, ⟨3, 0, 0, m3Split⟩, ⟨3, 0, 0, m3Contact⟩}1264 1265private theorem allowedPatterns_single_one_three :1266    allowedPatterns (.single 1 3) = allowedThree := by1267  classical1268  ext ⟨d, rt, rx, m⟩1269  exact Finset.mem_filter.trans ((and_iff_right (Finset.mem_univ _)).trans1270    (allowed_single_one_three_iff d rt rx m))1271 1272private theorem residuePatterns_three :1273    residuePatterns 3 = {m3Inert, m3Quadratic, m3Tangent, m3Split, m3Contact} := by1274  ext m1275  have h := allowed_single_one_three_iff 3 0 0 m1276  change 0 < 3 ∧ 0 + 0 + patternWeight m = 3 ∧ 3 ≤ 3 ∧ 0 = 0 ∧ (0 < 0 ↔ 3 < 3) ↔ _ at h1277  simp only [residuePatterns, Finset.mem_filter, Finset.mem_univ, true_and]1278  simpa using h1279 1280open scoped Classical in1281private theorem sum_allowed_single_one_three (f : TangentPattern (State.single 1 3).degree → ℚ) :1282    ∑ P ∈ allowedPatterns (.single 1 3), (if SelfPattern (.single 1 3) P then 0 else f P) =1283      f ⟨1, 1, 0, fun _ ↦ 0⟩ + f ⟨2, 2, 0, fun _ ↦ 0⟩ +1284        f ⟨2, 1, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else 0⟩ +1285        f ⟨3, 0, 0, m3Inert⟩ + f ⟨3, 0, 0, m3Quadratic⟩ + f ⟨3, 0, 0, m3Tangent⟩ +1286        f ⟨3, 0, 0, m3Split⟩ := by1287  rw [allowedPatterns_single_one_three, allowedThree]1288  repeat rw [Finset.sum_insert (by decide)]1289  rw [Finset.sum_singleton]1290  simp +decide only [selfPattern_single_iff, if_true, if_false, add_zero, add_assoc]1291 1292/-! ### Degree three: laws -/1293 1294private theorem coeff_m3Inert (q : ℚ) (σ : FactorType) :1295    coeffAt q (childProd (otherChildren 1 m3Inert)) σ = if σ = {(1,3)} then 1 else 0 := by1296  rw [coeff_otherChildren _ [(3, .single 1 1)] (by decide)]; simp_children1297 1298private theorem coeff_m3Quadratic (q : ℚ) (σ : FactorType) :1299    coeffAt q (childProd (otherChildren 1 m3Quadratic)) σ =1300      if σ = (1,1) ::ₘ {(1,2)} then 1 else 0 := by1301  rw [coeff_otherChildren _ [(1, .single 1 1), (2, .single 1 1)] (by decide)]; simp_children1302 1303private theorem coeff_m3Split (q : ℚ) (σ : FactorType) :1304    coeffAt q (childProd (otherChildren 1 m3Split)) σ =1305      if σ = (1,1) ::ₘ (1,1) ::ₘ {(1,1)} then 1 else 0 := by1306  rw [coeff_otherChildren _ [(1, .single 1 1), (1, .single 1 1), (1, .single 1 1)] (by decide)]1307  simp_children1308 1309private theorem coeff_m3Tangent (q : ℚ) (hq : 1 < q) (σ : FactorType) :1310    coeffAt q (childProd (otherChildren 1 m3Tangent)) σ =1311      (if σ = (1,1) ::ₘ {(2,1)} then q/(q+1) else 0) +1312        (if σ = (1,1) ::ₘ (1,1) ::ₘ {(1,1)} then 1/(2*(q+1)) else 0) +1313        (if σ = (1,1) ::ₘ {(1,2)} then 1/(2*(q+1)) else 0) := by1314  rw [coeff_otherChildren _ [(1, .single 1 1), (1, .single 1 2)] (by decide)]1315  simp_children1316  rw [single_two_law 1 one_pos q hq]1317  simp only [ite_add_zero, ite_mem_erase, Multiset.insert_eq_cons]1318 1319private theorem divisorCount_m3 (q : ℚ) :1320    (divisorCount 0 m3Inert).eval q = (q^3 - q) / 3 ∧1321    (divisorCount 0 m3Quadratic).eval q = q * ((q^2 - q) / 2) ∧1322    (divisorCount 0 m3Tangent).eval q = q * (q - 1) ∧1323    (divisorCount 0 m3Split).eval q = q * (q - 1) * (q - 2) / 6 ∧1324    (divisorCount 0 m3Contact).eval q = q := by1325  refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;>1326  simp [divisorCount_eval, Fin.prod_univ_three, Fin.sum_univ_three, falling, eval_prod,1327    availablePoints, Expr.eval, Expr.sub, Expr.neg, List.range_succ, pointCount_two,1328    pointCount_three, m3Inert, m3Quadratic, m3Tangent, m3Split, m3Contact,1329    -mul_eq_mul_left_iff] <;>1330  ring_nf1331 1332private theorem children_single_one_three (m : Pattern 3) :1333    children (.single 1 3) ⟨3, 0, 0, m⟩ = otherChildren (n := 3) 1 m := rfl1334 1335private theorem tangentCount_single_one_three (m : Pattern 3) :1336    tangentCount (.single 1 3) ⟨3, 0, 0, m⟩ = divisorCount (n := 3) 0 m := rfl1337 1338private theorem single_three_law (q : ℚ) (hq : 1 < q) (σ : FactorType) :1339    coeffAt q (stateLaw (.single 1 3)) σ =1340      (if σ = {(3,1)} then q^2*(q^2+1)/(q^4+q^3+q^2+q+1) else 0) +1341      (if σ = {(1,3)} then (q+1)/(3*(q^4+q^3+q^2+q+1)) else 0) +1342      (if σ = {(1,1),(2,1)} then q*(q^3+q^2+1)/((q+1)*(q^4+q^3+q^2+q+1)) else 0) +1343      (if σ = {(1,1),(1,2)} then (q^2+q+1)/(2*(q+1)*(q^4+q^3+q^2+q+1)) else 0) +1344      (if σ = {(1,1),(1,1),(1,1)} then (q^2-q+1)/(6*(q+1)*(q^4+q^3+q^2+q+1)) else 0) := by1345  obtain ⟨d1, d2, d3, d4, -⟩ := divisorCount_m3 q1346  have hq0 : q ≠ 0 := by positivity1347  have h5 : q ^ 5 - 1 ≠ 0 := by have : 1 < q ^ 5 := one_lt_pow₀ hq (by norm_num); linarith1348  have hR : (Expr.inv (.sub (.const 1) (returnWeight 3))).eval q = q ^ 5 / (q ^ 5 - 1) := by1349    rw [returnWeight_eval, show tri 3 = 6 from rfl, inv_eq_iff_eq_inv, inv_div]; field_simp1350  rw [stateLaw_single 1 3 ⟨one_pos, by norm_num⟩ (by norm_num), coeff_scale, coeff_exitLaw,1351    sum_allowed_single_one_three, hR]1352  simp only [children_single_one_three, coeff_m3Inert, coeff_m3Quadratic, coeff_m3Split,1353    coeff_m3Tangent q hq]1354  rw [coeff_childProd_perm (children_single_perm _ (l := [(1, .crossing 1 1 1 2)]) (by decide)),1355    coeff_childProd_perm (children_single_perm _ (l := [(1, .crossing 1 1 2 1)]) (by decide)),1356    coeff_childProd_perm1357      (children_single_perm _ (l := [(1, .single 1 1), (1, .crossing 1 1 1 1)]) (by decide))]1358  simp_children1359  rw [crossing_left_one_law 1 1 2 one_pos one_pos two_pos q hq,1360    crossing_right_one_law 1 1 2 one_pos one_pos two_pos q hq,1361    crossing_one_one_law 1 1 one_pos one_pos q hq]1362  simp only [Expr.eval, tangentCount_single_one_three, d1, d2, d3, d4, ite_mem_erase]1363  simp (disch := decide) only [tangentCount, divisorCount_zero, divisorCount_cell]1364  simp [falling, availablePoints, Expr.prod, divisorProbability, tri, Expr.eval, eval_pow,1365    eminusOne, Expr.sub, Expr.neg, State.degree, Multiset.insert_eq_cons, ite_eq_mul_indicator]1366  have : q + 1 ≠ 0 := by positivity1367  have : q ^ 4 + q ^ 3 + q ^ 2 + q + 1 ≠ 0 := by positivity1368  field_simp1369  ring1370 1371/-- **Cubic monic densities.** For every `q > 1`, the universal monic expressions of degree `3` on1372the five valid cubic types, with `Φ₅(q) = q⁴ + q³ + q² + q + 1`; they vanish on every other type. -/1373theorem monicExpr_three_eval (q : ℚ) (hq : 1 < q) (σ : FactorType) :1374    (monicExpr 3 σ).eval q =1375      (if σ = {(3,1)} then (q ^ 2 + 1) / (q ^ 4 + q ^ 3 + q ^ 2 + q + 1) else 0) +1376      (if σ = {(1,3)} then q ^ 3 * (q + 1) / (3 * (q ^ 4 + q ^ 3 + q ^ 2 + q + 1)) else 0) +1377      (if σ = {(1,1), (2,1)} then1378        q * (q ^ 3 + q + 1) / ((q + 1) * (q ^ 4 + q ^ 3 + q ^ 2 + q + 1)) else 0) +1379      (if σ = {(1,1), (1,2)} then1380        q ^ 3 * (q ^ 2 + q + 1) / (2 * (q + 1) * (q ^ 4 + q ^ 3 + q ^ 2 + q + 1)) else 0) +1381      (if σ = {(1,1), (1,1), (1,1)} then1382        q ^ 3 * (q ^ 2 - q + 1) / (6 * (q + 1) * (q ^ 4 + q ^ 3 + q ^ 2 + q + 1)) else 0) := by1383  obtain ⟨d1, d2, d3, d4, d5⟩ := divisorCount_m3 q1384  rw [monicExpr, coeff_globalLaw, residuePatterns_three]1385  repeat rw [Finset.sum_insert (by decide)]1386  rw [Finset.sum_singleton, coeff_m3Inert, coeff_m3Quadratic, coeff_m3Tangent q hq, coeff_m3Split,1387    coeff_otherChildren _ [(1, .single 1 3)] (by decide)]1388  simp only [childProd, List.map_cons, List.map_nil, lawProd_cons, lawProd_nil, coeff_mul_lawOne,1389    coeff_descend_one, single_three_law q hq, Bool.false_eq_true, if_false]1390  simp [d1, d2, d3, d4, d5, Expr.eval, eval_pow, Multiset.insert_eq_cons, ite_eq_mul_indicator]1391  have : q ≠ 0 := by positivity1392  have : q + 1 ≠ 0 := by positivity1393  have : q ^ 4 + q ^ 3 + q ^ 2 + q + 1 ≠ 0 := by positivity1394  field_simp1395  ring1396 1397end DegreeThree1398 1399/-! ### The law of `T(1,1;2,2)` -/1400 1401/-- The crossing state `T(1,1;2,2)` (tangent conic through the node): a point of degree two, a1402rational point of contact two, or two rational points. -/1403private theorem crossing_two_two_law (q : ℚ) (hq : 1 < q) (σ : FactorType) :Example 9.41404    coeffAt q (stateLaw (.crossing 1 1 2 2)) σ = (if σ = {(4,1)} then 1/(q+1) else 0) +1405      (if σ = {(2,2)} then (q^2+q+1)/(2*q*(q+1)) else 0) +1406      (if σ = {(2,1),(2,1)} then (q^2-q-1)/(2*q*(q+1)) else 0) := by1407  have hn : 2 ≤ (State.crossing 1 1 2 2).degree := by decide1408  set D := (State.crossing 1 1 2 2).degree1409  let i0 : Fin D := ⟨0, by omega⟩1410  let i1 : Fin D := ⟨1, by omega⟩1411  let f1 : Fin (D+1) := ⟨1, by omega⟩1412  let f2 : Fin (D+1) := ⟨2, by omega⟩1413  let P1 : TangentPattern D := ⟨f2, 0, 0, spat (i1, i0) f1⟩1414  let P2 : TangentPattern D := ⟨f2, 0, 0, spat (i0, i1) f1⟩1415  let P3 : TangentPattern D := ⟨f2, 0, 0, spat (i0, i0) f2⟩1416  have hA : allowedPatterns (.crossing 1 1 2 2) = {P1, P2, P3} := by1417    ext P1418    simp only [allowedPatterns, Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_insert,1419      Finset.mem_singleton]1420    constructor1421    · obtain ⟨d, rt, rx, other⟩ := P1422      rintro ⟨h0, hw, h1, h2, h3, h4⟩1423      simp only at h0 hw h1 h2 h3 h41424      have hd : d.val = 2 := by1425        by_contra hd; have := h3.2 (by omega); have := h4.2 (by omega); omega1426      obtain rfl : rt = 0 :=1427        Fin.ext (by rw [Fin.val_zero]; by_contra hc; have := h3.1 (by omega); omega)1428      obtain rfl : rx = 0 :=1429        Fin.ext (by rw [Fin.val_zero]; by_contra hc; have := h4.1 (by omega); omega)1430      obtain rfl : d = f2 := Fin.ext hd1431      rcases pattern_eq_of_weight_two hn other (by simp at hw; omega) with ho | ho | ho <;> rw [ho]1432      · right; right; rfl1433      · right; left; rfl1434      · left; rfl1435    · rintro (rfl | rfl | rfl) <;> refine ⟨by simp [P1, P2, P3, f2], ?_, ?_⟩ <;>1436        simp [P1, P2, P3, patternWeight_spat, f1, f2, i0, i1]1437  have hi01 : i0 ≠ i1 := by simp [i0, i1]1438  have hne : P1 ≠ P2 ∧ P1 ≠ P3 ∧ P2 ≠ P3 := by1439    refine ⟨fun h ↦ ?_, fun h ↦ ?_, fun h ↦ ?_⟩1440    · simpa [P1, P2, spat, hi01, hi01.symm, f1] using congrArg (fun P ↦ (P.other (i1, i0)).val) h1441    · simpa [P1, P3, spat, hi01.symm, f1] using congrArg (fun P ↦ (P.other (i1, i0)).val) h1442    · simpa [P2, P3, spat, hi01.symm, f1] using congrArg (fun P ↦ (P.other (i0, i1)).val) h1443  have hS : ∀ P, ¬ SelfPattern (.crossing 1 1 2 2) P := by rintro P ⟨_, _, h, _⟩; cases h1444  rw [stateLaw_crossing _ _ _ _ ⟨one_pos, one_pos, two_pos, two_pos⟩, coeff_exitLaw, hA,1445    Finset.sum_insert (by simp [hne]), Finset.sum_insert (by simp [hne]), Finset.sum_singleton]1446  simp only [if_neg (hS _)]1447  have hch1 : children (.crossing 1 1 2 2) P1 = [(2, .single 2 1)] := by1448    simp [children, P1, f1, otherChildren_spat, i0, i1]1449  have hch2 : children (.crossing 1 1 2 2) P2 = [(1, .single 2 2)] := by1450    simp [children, P2, f1, otherChildren_spat, i0, i1]1451  have hch3 : children (.crossing 1 1 2 2) P3 = [(1, .single 2 1), (1, .single 2 1)] := by1452    simp [children, P3, f2, otherChildren_spat, i0]1453  rw [hch1, hch2, hch3]1454  simp_children1455  rw [single_two_law 2 two_pos q hq]1456  have hq0 : q ≠ 0 := by positivity1457  have hq1 : q - 1 ≠ 0 := by linarith1458  have hDP : (divisorProbability (.crossing 1 1 2 2) 2).eval q = 1/(q*(q-1)) := by1459    simp [divisorProbability, chooseTwo, Expr.eval, Expr.pow, eminusOne, Expr.sub, Expr.neg]1460    ring1461  simp only [Expr.eval, show P1.d.val = 2 from rfl, show P2.d.val = 2 from rfl,1462    show P3.d.val = 2 from rfl, hDP]1463  simp [tangentCount, divisorCount_spat, P1, P2, P3, f1, f2, falling, Expr.prod, availablePoints,1464    i0, i1, pointCount_two, List.range_succ, Expr.sub, Expr.neg, Expr.eval, Multiset.insert_eq_cons,1465    ite_eq_mul_indicator]1466  have : q + 1 ≠ 0 := by positivity1467  field_simp1468  ring1469 1470/-! ### Degree four: patterns -/1471 1472section DegreeFour1473 1474/-- One rational point of contact four (the self pattern of `S(1;4)`). -/1475private abbrev m4Contact : Pattern 4 := fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 3 then 1 else 01476/-- One point of degree two and contact two. -/1477private abbrev m4QuadraticContact : Pattern 4 := fun ij ↦1478  if ij.1.val = 1 ∧ ij.2.val = 1 then 1 else 01479/-- One point of degree four. -/1480private abbrev m4Inert : Pattern 4 := fun ij ↦ if ij.1.val = 3 ∧ ij.2.val = 0 then 1 else 01481/-- A rational point of contact two and a point of degree two. -/1482private abbrev m4TangentQuadratic : Pattern 4 := fun ij ↦1483  if ij.1.val = 0 ∧ ij.2.val = 1 then 1 else if ij.1.val = 1 ∧ ij.2.val = 0 then 1 else 01484/-- Two rational points of contact two. -/1485private abbrev m4TwoTangent : Pattern 4 := fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 1 then 2 else 01486/-- Two points of degree two. -/1487private abbrev m4TwoQuadratic : Pattern 4 := fun ij ↦1488  if ij.1.val = 1 ∧ ij.2.val = 0 then 2 else 01489/-- A rational point and a rational point of contact three. -/1490private abbrev m4ContactThree : Pattern 4 := fun ij ↦1491  if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else if ij.1.val = 0 ∧ ij.2.val = 2 then 1 else 01492/-- A rational point and a point of degree three. -/1493private abbrev m4Cubic : Pattern 4 := fun ij ↦1494  if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else if ij.1.val = 2 ∧ ij.2.val = 0 then 1 else 01495/-- Two rational points and a rational point of contact two. -/1496private abbrev m4SplitTangent : Pattern 4 := fun ij ↦1497  if ij.1.val = 0 ∧ ij.2.val = 0 then 2 else if ij.1.val = 0 ∧ ij.2.val = 1 then 1 else 01498/-- Two rational points and a point of degree two. -/1499private abbrev m4SplitQuadratic : Pattern 4 := fun ij ↦1500  if ij.1.val = 0 ∧ ij.2.val = 0 then 2 else if ij.1.val = 1 ∧ ij.2.val = 0 then 1 else 01501/-- Four rational points. -/1502private abbrev m4Split : Pattern 4 := fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 4 else 01503 1504open scoped Classical in1505/-- The allowed patterns of `S(1;4)`. -/1506private def allowedFour : Finset (TangentPattern (State.single 1 4).degree) :=1507  {⟨1, 1, 0, fun _ ↦ 0⟩, ⟨2, 2, 0, fun _ ↦ 0⟩,1508    ⟨2, 1, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else 0⟩, ⟨3, 3, 0, fun _ ↦ 0⟩,1509    ⟨3, 2, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else 0⟩,1510    ⟨3, 1, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 2 else 0⟩,1511    ⟨3, 1, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 1 then 1 else 0⟩,1512    ⟨3, 1, 0, fun ij ↦ if ij.1.val = 1 ∧ ij.2.val = 0 then 1 else 0⟩,1513    ⟨4, 0, 0, m4Split⟩, ⟨4, 0, 0, m4SplitTangent⟩, ⟨4, 0, 0, m4SplitQuadratic⟩,1514    ⟨4, 0, 0, m4ContactThree⟩, ⟨4, 0, 0, m4Cubic⟩, ⟨4, 0, 0, m4TwoTangent⟩,1515    ⟨4, 0, 0, m4TangentQuadratic⟩, ⟨4, 0, 0, m4TwoQuadratic⟩, ⟨4, 0, 0, m4QuadraticContact⟩,1516    ⟨4, 0, 0, m4Inert⟩, ⟨4, 0, 0, m4Contact⟩}1517 1518private theorem allowed_single_one_four_iff (d rt rx : Fin 5) (m : Pattern 4) :1519    Allowed (State.single 1 4) (⟨d, rt, rx, m⟩ : TangentPattern 4) ↔1520      (⟨d, rt, rx, m⟩ : TangentPattern 4) ∈ ({⟨1, 1, 0, fun _ ↦ 0⟩, ⟨2, 2, 0, fun _ ↦ 0⟩,1521    ⟨2, 1, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else 0⟩, ⟨3, 3, 0, fun _ ↦ 0⟩,1522    ⟨3, 2, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else 0⟩,1523    ⟨3, 1, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 2 else 0⟩,1524    ⟨3, 1, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 1 then 1 else 0⟩,1525    ⟨3, 1, 0, fun ij ↦ if ij.1.val = 1 ∧ ij.2.val = 0 then 1 else 0⟩,1526    ⟨4, 0, 0, m4Split⟩, ⟨4, 0, 0, m4SplitTangent⟩, ⟨4, 0, 0, m4SplitQuadratic⟩,1527    ⟨4, 0, 0, m4ContactThree⟩, ⟨4, 0, 0, m4Cubic⟩, ⟨4, 0, 0, m4TwoTangent⟩,1528    ⟨4, 0, 0, m4TangentQuadratic⟩, ⟨4, 0, 0, m4TwoQuadratic⟩, ⟨4, 0, 0, m4QuadraticContact⟩,1529    ⟨4, 0, 0, m4Inert⟩, ⟨4, 0, 0, m4Contact⟩} : Finset (TangentPattern 4)) := by1530  have fa4 (p : Fin 4 → Prop) : (∀ i, p i) ↔ p 0 ∧ p 1 ∧ p 2 ∧ p 3 :=1531    ⟨fun h ↦ ⟨h 0, h 1, h 2, h 3⟩, fun ⟨h0, h1, h2, h3⟩ i ↦ by fin_cases i <;> assumption⟩1532  change 0 < d.val ∧ rt.val + rx.val + patternWeight m = d.val ∧ d.val ≤ 4 ∧ rx.val = 0 ∧1533    (0 < rt.val ↔ d.val < 4) ↔ _1534  simp only [patternWeight, Fintype.sum_prod_type, Fin.sum_univ_four,1535    Finset.mem_insert, Finset.mem_singleton, TangentPattern.mk.injEq, funext_iff, Prod.forall, fa4,1536    Fin.ext_iff, m4Contact, m4QuadraticContact, m4Inert, m4TangentQuadratic, m4TwoTangent,1537    m4TwoQuadratic, m4ContactThree, m4Cubic, m4SplitTangent, m4SplitQuadratic, m4Split]1538  simp only [Fin.isValue, Fin.val_zero, Fin.val_one, Fin.val_two, and_self, and_true, and_false,1539    ↓reduceIte, Nat.reduceEqDiff, show ((3 : Fin 5) : ℕ) = 3 from rfl,1540    show ((4 : Fin 5) : ℕ) = 4 from rfl, show ((3 : Fin 4) : ℕ) = 3 from rfl]1541  have := (m (0,0)).isLt; have := (m (0,1)).isLt; have := (m (0,2)).isLt; have := (m (0,3)).isLt1542  have := (m (1,0)).isLt; have := (m (1,1)).isLt; have := (m (1,2)).isLt; have := (m (1,3)).isLt1543  have := (m (2,0)).isLt; have := (m (2,1)).isLt; have := (m (2,2)).isLt; have := (m (2,3)).isLt1544  have := (m (3,0)).isLt; have := (m (3,1)).isLt; have := (m (3,2)).isLt; have := (m (3,3)).isLt1545  have := d.isLt; have := rt.isLt; have := rx.isLt1546  generalize (m (0,0)).val = a00 at *; generalize (m (0,1)).val = a01 at *1547  generalize (m (0,2)).val = a02 at *; generalize (m (0,3)).val = a03 at *1548  generalize (m (1,0)).val = a10 at *; generalize (m (1,1)).val = a11 at *1549  generalize (m (1,2)).val = a12 at *; generalize (m (1,3)).val = a13 at *1550  generalize (m (2,0)).val = a20 at *; generalize (m (2,1)).val = a21 at *1551  generalize (m (2,2)).val = a22 at *; generalize (m (2,3)).val = a23 at *1552  generalize (m (3,0)).val = a30 at *; generalize (m (3,1)).val = a31 at *1553  generalize (m (3,2)).val = a32 at *; generalize (m (3,3)).val = a33 at *1554  generalize d.val = dd at *; generalize rt.val = r at *; generalize rx.val = x at *1555  constructor1556  · rintro ⟨h1, h2, h3, h4, h5⟩1557    obtain ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩ : a12 = 0 ∧ a13 = 0 ∧ a21 = 0 ∧ a22 = 0 ∧1558      a23 = 0 ∧ a31 = 0 ∧ a32 = 0 ∧ a33 = 0 ∧ x = 0 := by omega1559    have : a01 ≤ 2 := by omega1560    have : a02 ≤ 1 := by omega1561    have : a03 ≤ 1 := by omega1562    have : a10 ≤ 2 := by omega1563    have : a11 ≤ 1 := by omega1564    have : a20 ≤ 1 := by omega1565    have : a30 ≤ 1 := by omega1566    have : r ≤ 3 := by omega1567    interval_cases dd <;> interval_cases r <;> (try (exfalso; omega)) <;>1568      interval_cases a00 <;> (try (exfalso; omega)) <;> interval_cases a01 <;>1569      (try (exfalso; omega)) <;> interval_cases a02 <;> (try (exfalso; omega)) <;>1570      interval_cases a03 <;> (try (exfalso; omega)) <;> interval_cases a10 <;>1571      (try (exfalso; omega)) <;> interval_cases a11 <;> (try (exfalso; omega)) <;>1572      interval_cases a20 <;> (try (exfalso; omega)) <;> interval_cases a30 <;>1573      (try (exfalso; omega)) <;> simp1574  · rintro (h|h|h|h|h|h|h|h|h|h|h|h|h|h|h|h|h|h|h) <;> omega1575 1576private theorem allowedPatterns_single_one_four : allowedPatterns (.single 1 4) = allowedFour := by1577  classical1578  ext ⟨d, rt, rx, m⟩1579  exact Finset.mem_filter.trans ((and_iff_right (Finset.mem_univ _)).trans1580    (allowed_single_one_four_iff d rt rx m))1581 1582private theorem residuePatterns_four :1583    residuePatterns 4 = {m4Split, m4SplitTangent, m4SplitQuadratic, m4ContactThree, m4Cubic,1584      m4TwoTangent, m4TangentQuadratic, m4TwoQuadratic, m4QuadraticContact, m4Inert,1585      m4Contact} := by1586  ext m1587  have h := allowed_single_one_four_iff 4 0 0 m1588  change 0 < 4 ∧ 0 + 0 + patternWeight m = 4 ∧ 4 ≤ 4 ∧ 0 = 0 ∧ (0 < 0 ↔ 4 < 4) ↔ _ at h1589  simp only [residuePatterns, Finset.mem_filter, Finset.mem_univ, true_and]1590  simpa using h1591 1592open scoped Classical in1593private theorem sum_allowed_single_one_four (f : TangentPattern (State.single 1 4).degree → ℚ) :1594    ∑ P ∈ allowedPatterns (.single 1 4), (if SelfPattern (.single 1 4) P then 0 else f P) =1595      f ⟨1, 1, 0, fun _ ↦ 0⟩ + f ⟨2, 2, 0, fun _ ↦ 0⟩ +1596        f ⟨2, 1, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else 0⟩ +1597        f ⟨3, 3, 0, fun _ ↦ 0⟩ +1598        f ⟨3, 2, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 1 else 0⟩ +1599        f ⟨3, 1, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 0 then 2 else 0⟩ +1600        f ⟨3, 1, 0, fun ij ↦ if ij.1.val = 0 ∧ ij.2.val = 1 then 1 else 0⟩ +1601        f ⟨3, 1, 0, fun ij ↦ if ij.1.val = 1 ∧ ij.2.val = 0 then 1 else 0⟩ +1602        f ⟨4, 0, 0, m4Split⟩ + f ⟨4, 0, 0, m4SplitTangent⟩ + f ⟨4, 0, 0, m4SplitQuadratic⟩ +1603        f ⟨4, 0, 0, m4ContactThree⟩ + f ⟨4, 0, 0, m4Cubic⟩ + f ⟨4, 0, 0, m4TwoTangent⟩ +1604        f ⟨4, 0, 0, m4TangentQuadratic⟩ + f ⟨4, 0, 0, m4TwoQuadratic⟩ +1605        f ⟨4, 0, 0, m4QuadraticContact⟩ + f ⟨4, 0, 0, m4Inert⟩ := by1606  rw [allowedPatterns_single_one_four, allowedFour]1607  repeat rw [Finset.sum_insert (by decide)]1608  rw [Finset.sum_singleton]1609  simp +decide only [selfPattern_single_iff, if_true, if_false, add_zero, add_assoc]1610 1611/-! ### Degree four: laws at `q = 2` -/1612 1613private theorem single_two_law_at_two (σ : FactorType) : coeffAt 2 (stateLaw (.single 1 2)) σ =1614    (if σ = {(2,1)} then 2/3 else 0) + (if σ = (1,1) ::ₘ {(1,1)} then 1/6 else 0) +1615      (if σ = {(1,2)} then 1/6 else 0) := by1616  rw [single_two_law 1 one_pos 2 (by norm_num)]; norm_num [Multiset.insert_eq_cons]1617 1618private theorem single_two_law_at_four (σ : FactorType) :1619    coeffAt (2^2) (stateLaw (.single 1 2)) σ =1620      (if σ = {(2,1)} then 4/5 else 0) + (if σ = (1,1) ::ₘ {(1,1)} then 1/10 else 0) +1621        (if σ = {(1,2)} then 1/10 else 0) := by1622  rw [single_two_law 1 one_pos (2^2) (by norm_num)]; norm_num [Multiset.insert_eq_cons]1623 1624private theorem single_three_law_at_two (σ : FactorType) : coeffAt 2 (stateLaw (.single 1 3)) σ =1625    (if σ = {(3,1)} then 20/31 else 0) + (if σ = {(1,3)} then 1/31 else 0) +1626      (if σ = (1,1) ::ₘ {(2,1)} then 26/93 else 0) + (if σ = (1,1) ::ₘ {(1,2)} then 7/186 else 0) +1627      (if σ = (1,1) ::ₘ (1,1) ::ₘ {(1,1)} then 1/186 else 0) := by1628  rw [single_three_law 2 (by norm_num)]; norm_num [Multiset.insert_eq_cons]1629 1630private theorem crossing_two_two_law_at_two (σ : FactorType) :Example 9.41631    coeffAt 2 (stateLaw (.crossing 1 1 2 2)) σ = (if σ = {(4,1)} then 1/3 else 0) +1632      (if σ = {(2,2)} then 7/12 else 0) + (if σ = (2,1) ::ₘ {(2,1)} then 1/12 else 0) := by1633  rw [crossing_two_two_law 2 (by norm_num)]; norm_num [Multiset.insert_eq_cons]1634 1635private theorem coeff_m4Inert (q : ℚ) (σ : FactorType) :1636    coeffAt q (childProd (otherChildren 1 m4Inert)) σ = if σ = {(1,4)} then 1 else 0 := by1637  rw [coeff_otherChildren _ [(4, .single 1 1)] (by decide)]; simp_children1638 1639private theorem coeff_m4Cubic (q : ℚ) (σ : FactorType) :1640    coeffAt q (childProd (otherChildren 1 m4Cubic)) σ = if σ = (1,1) ::ₘ {(1,3)} then 1 else 0 := by1641  rw [coeff_otherChildren _ [(1, .single 1 1), (3, .single 1 1)] (by decide)]; simp_children1642 1643private theorem coeff_m4SplitQuadratic (q : ℚ) (σ : FactorType) :1644    coeffAt q (childProd (otherChildren 1 m4SplitQuadratic)) σ =1645      if σ = (1,1) ::ₘ (1,1) ::ₘ {(1,2)} then 1 else 0 := by1646  rw [coeff_otherChildren _ [(1, .single 1 1), (1, .single 1 1), (2, .single 1 1)] (by decide)]1647  simp_children1648 1649private theorem coeff_m4ContactThree (σ : FactorType) :1650    coeffAt 2 (childProd (otherChildren 1 m4ContactThree)) σ =1651      (if σ = (1,1) ::ₘ {(3,1)} then 20/31 else 0) + (if σ = (1,1) ::ₘ {(1,3)} then 1/31 else 0) +1652      (if σ = (1,1) ::ₘ (1,1) ::ₘ {(2,1)} then 26/93 else 0) +1653      (if σ = (1,1) ::ₘ (1,1) ::ₘ {(1,2)} then 7/186 else 0) +1654      (if σ = (1,1) ::ₘ (1,1) ::ₘ (1,1) ::ₘ {(1,1)} then 1/186 else 0) := by1655  rw [coeff_otherChildren _ [(1, .single 1 1), (1, .single 1 3)] (by decide)]1656  simp_children1657  rw [single_three_law_at_two]1658  simp only [ite_add_zero, ite_mem_erase]1659 1660private theorem coeff_m4TangentQuadratic (σ : FactorType) :1661    coeffAt 2 (childProd (otherChildren 1 m4TangentQuadratic)) σ =1662      (if σ = (1,2) ::ₘ {(2,1)} then 2/3 else 0) +1663      (if σ = (1,2) ::ₘ (1,1) ::ₘ {(1,1)} then 1/6 else 0) +1664      (if σ = (1,2) ::ₘ {(1,2)} then 1/6 else 0) := by1665  rw [coeff_otherChildren _ [(2, .single 1 1), (1, .single 1 2)] (by decide)]1666  simp_children1667  rw [single_two_law_at_two]1668  simp only [ite_add_zero, ite_mem_erase]1669 1670private theorem coeff_m4SplitTangent (σ : FactorType) :1671    coeffAt 2 (childProd (otherChildren 1 m4SplitTangent)) σ =1672      (if σ = (1,1) ::ₘ (1,1) ::ₘ {(2,1)} then 2/3 else 0) +1673      (if σ = (1,1) ::ₘ (1,1) ::ₘ (1,1) ::ₘ {(1,1)} then 1/6 else 0) +1674      (if σ = (1,1) ::ₘ (1,1) ::ₘ {(1,2)} then 1/6 else 0) := by1675  rw [coeff_otherChildren _ [(1, .single 1 1), (1, .single 1 1), (1, .single 1 2)] (by decide)]1676  simp_children1677  rw [single_two_law_at_two]1678  simp only [ite_add_zero, ite_mem_erase]1679 1680private theorem coeff_m4QuadraticContact (σ : FactorType) :1681    coeffAt 2 (childProd (otherChildren 1 m4QuadraticContact)) σ =1682      (if σ = {(2,2)} then 4/5 else 0) + (if σ = (1,2) ::ₘ {(1,2)} then 1/10 else 0) +1683        (if σ = {(1,4)} then 1/10 else 0) := by1684  rw [coeff_otherChildren _ [(2, .single 1 2)] (by decide)]1685  simp only [childProd, List.map_cons, List.map_nil, lawProd_cons, lawProd_nil, coeff_mul_lawOne]1686  rw [show ({(2,2)} : FactorType) = scaleType 2 {(2,1)} by decide,1687    show ((1,2) ::ₘ {(1,2)} : FactorType) = scaleType 2 ((1,1) ::ₘ {(1,1)}) by decide,1688    show ({(1,4)} : FactorType) = scaleType 2 {(1,2)} by decide]1689  by_cases h : ∃ τ, σ = scaleType 2 τ1690  · obtain ⟨τ, rfl⟩ := h1691    rw [coeff_descend_scaleType 2 two_pos, single_two_law_at_four]1692    simp only [(scaleType_injective two_pos).eq_iff]1693  · push Not at h1694    rw [coeff_descend_of_ne 2 2 _ σ h, if_neg (h _), if_neg (h _), if_neg (h _)]1695    norm_num1696 1697private theorem coeff_m4TwoTangent (σ : FactorType) :1698    coeffAt 2 (childProd (otherChildren 1 m4TwoTangent)) σ =1699      (if σ = {(2,1)} + {(2,1)} then 2/3 * (2/3) else 0) +1700        (if σ = {(2,1)} + (1,1) ::ₘ {(1,1)} then 2/3 * (1/6) else 0) +1701        (if σ = {(2,1)} + {(1,2)} then 2/3 * (1/6) else 0) +1702      ((if σ = (1,1) ::ₘ {(1,1)} + {(2,1)} then 1/6 * (2/3) else 0) +1703        (if σ = (1,1) ::ₘ {(1,1)} + (1,1) ::ₘ {(1,1)} then 1/6 * (1/6) else 0) +1704        (if σ = (1,1) ::ₘ {(1,1)} + {(1,2)} then 1/6 * (1/6) else 0)) +1705      ((if σ = {(1,2)} + {(2,1)} then 1/6 * (2/3) else 0) +1706        (if σ = {(1,2)} + (1,1) ::ₘ {(1,1)} then 1/6 * (1/6) else 0) +1707        (if σ = {(1,2)} + {(1,2)} then 1/6 * (1/6) else 0)) := by1708  rw [coeff_otherChildren _ [(1, .single 1 2), (1, .single 1 2)] (by decide)]1709  simp only [childProd, List.map_cons, List.map_nil, lawProd_cons]1710  have hS : ∀ τ ∉ ({{(2,1)}, (1,1) ::ₘ {(1,1)}, {(1,2)}} : Finset FactorType),1711      coeffAt 2 (lawDescend 1 (stateLaw (.single 1 2))) τ = 0 := by1712    intro τ h1713    simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at h1714    rw [coeff_descend_one, single_two_law_at_two, if_neg h.1, if_neg h.2.1, if_neg h.2.2]; simp1715  rw [coeff_mul 2 _ _ _ hS, Finset.sum_insert (by decide), Finset.sum_insert (by decide),1716    Finset.sum_singleton]1717  simp only [lawProd_nil, coeff_mul_lawOne, coeff_descend_one, single_two_law_at_two]1718  simp +decide only [if_true, if_false, add_zero, zero_add]1719  simp only [mul_add, ite_add_zero, ite_le_sub]1720  ring1721 1722private theorem children_single_one_four (m : Pattern 4) :1723    children (.single 1 4) ⟨4, 0, 0, m⟩ = otherChildren (n := 4) 1 m := rfl1724 1725private theorem tangentCount_single_one_four (m : Pattern 4) :1726    tangentCount (.single 1 4) ⟨4, 0, 0, m⟩ = divisorCount (n := 4) 0 m := rfl1727 1728private theorem divisorCount_m4_at_two :1729    (divisorCount 0 m4Split).eval 2 = 0 ∧ (divisorCount 0 m4SplitTangent).eval 2 = 0 ∧1730    (divisorCount 0 m4SplitQuadratic).eval 2 = 1 ∧ (divisorCount 0 m4ContactThree).eval 2 = 2 ∧1731    (divisorCount 0 m4Cubic).eval 2 = 4 ∧ (divisorCount 0 m4TwoTangent).eval 2 = 1 ∧1732    (divisorCount 0 m4TangentQuadratic).eval 2 = 2 ∧ (divisorCount 0 m4TwoQuadratic).eval 2 = 0 ∧1733    (divisorCount 0 m4QuadraticContact).eval 2 = 1 ∧ (divisorCount 0 m4Inert).eval 2 = 3 ∧1734    (divisorCount 0 m4Contact).eval 2 = 2 := by1735  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;>1736  simp [divisorCount_eval, Fin.prod_univ_four, Fin.sum_univ_four, falling, eval_prod,1737    availablePoints, Expr.eval, Expr.sub, Expr.neg, List.range_succ, pointCount_two,1738    pointCount_three, pointCount_four, m4Split, m4SplitTangent, m4SplitQuadratic, m4ContactThree,1739    m4Cubic, m4TwoTangent, m4TangentQuadratic, m4TwoQuadratic, m4QuadraticContact, m4Inert,1740    m4Contact] <;> norm_num [Nat.factorial]1741 1742/-- The children `T(1,1;1,1)` and `S(1;2)` (from the tangent pattern of `S(1;4)` with a point of1743contact two). -/1744private theorem coeff_crossing_one_one_single_two_at_two (σ : FactorType) :1745    coeffAt 2 (childProd [(1, .crossing 1 1 1 1), (1, .single 1 2)]) σ =1746      (if σ = {(2,1)} + {(2,1)} then 2/3 else 0) +1747        (if σ = {(2,1)} + (1,1) ::ₘ {(1,1)} then 1/6 else 0) +1748        (if σ = {(2,1)} + {(1,2)} then 1/6 else 0) := by1749  have hS : ∀ τ ∉ ({{(2,1)}} : Finset FactorType),1750      coeffAt 2 (lawDescend 1 (stateLaw (.crossing 1 1 1 1))) τ = 0 := fun τ h ↦ by1751    rw [coeff_descend_one, crossing_one_one_law 1 1 one_pos one_pos 2 (by norm_num),1752      if_neg (Finset.mem_singleton.not.1 h)]1753  simp only [childProd, List.map_cons, List.map_nil, lawProd_cons]1754  rw [coeff_mul 2 _ _ _ hS, Finset.sum_singleton, coeff_descend_one,1755    crossing_one_one_law 1 1 one_pos one_pos 2 (by norm_num), if_pos rfl, lawProd_nil,1756    coeff_mul_lawOne, coeff_descend_one, single_two_law_at_two]1757  simp only [one_mul, ite_add_zero, ite_le_sub_one]1758 1759private theorem single_four_law_at_two (σ : FactorType) :1760    coeffAt 2 (stateLaw (.single 1 4)) σ = (if σ = {(4,1)} then 856/1533 else 0) +1761      (if σ = {(2,2)} then 566/7665 else 0) + (if σ = {(1,4)} then 31/10220 else 0) +1762      (if σ = {(2,1),(2,1)} then 2/63 else 0) + (if σ = {(1,2),(1,2)} then 83/183960 else 0) +1763      (if σ = {(1,2),(2,1)} then 103/4599 else 0) +1764      (if σ = {(1,1),(3,1)} then 4484/15841 else 0) + (if σ = {(1,1),(1,3)} then 9/2263 else 0) +1765      (if σ = {(1,1),(1,1),(2,1)} then 3085/142569 else 0) +1766      (if σ = {(1,1),(1,1),(1,2)} then 817/570276 else 0) +1767      (if σ = {(1,1),(1,1),(1,1),(1,1)} then 43/1140552 else 0) := by1768  obtain ⟨d1, d2, d3, d4, d5, d6, d7, d8, d9, d10, -⟩ := divisorCount_m4_at_two1769  have hR : (Expr.inv (.sub (.const 1) (returnWeight 4))).eval 2 = 512/511 := by1770    rw [returnWeight_eval, show tri 4 = 10 from rfl]; norm_num1771  rw [stateLaw_single 1 4 ⟨one_pos, by norm_num⟩ (by norm_num), coeff_scale, coeff_exitLaw,1772    sum_allowed_single_one_four, hR]1773  simp only [children_single_one_four, coeff_m4Inert, coeff_m4Cubic, coeff_m4SplitQuadratic,1774    coeff_m4ContactThree, coeff_m4TangentQuadratic, coeff_m4TwoTangent, coeff_m4QuadraticContact]1775  rw [coeff_childProd_perm (children_single_perm _ (l := [(1, .crossing 1 1 1 3)]) (by decide)),1776    coeff_childProd_perm (children_single_perm _ (l := [(1, .crossing 1 1 2 2)]) (by decide)),1777    coeff_childProd_perm1778      (children_single_perm _ (l := [(1, .single 1 1), (1, .crossing 1 1 1 2)]) (by decide)),1779    coeff_childProd_perm (children_single_perm _ (l := [(1, .crossing 1 1 3 1)]) (by decide)),1780    coeff_childProd_perm1781      (children_single_perm _ (l := [(1, .single 1 1), (1, .crossing 1 1 2 1)]) (by decide)),1782    coeff_childProd_perm (children_single_perm _1783      (l := [(1, .single 1 1), (1, .single 1 1), (1, .crossing 1 1 1 1)]) (by decide)),1784    coeff_childProd_perm1785      (children_single_perm _ (l := [(1, .crossing 1 1 1 1), (1, .single 1 2)]) (by decide)),1786    coeff_childProd_perm1787      (children_single_perm _ (l := [(2, .single 1 1), (1, .crossing 1 1 1 1)]) (by decide)),1788    coeff_crossing_one_one_single_two_at_two]1789  simp_children1790  simp only [crossing_left_one_law 1 1 3 one_pos one_pos (by norm_num) 2 (by norm_num),1791    crossing_two_two_law_at_two,1792    crossing_left_one_law 1 1 2 one_pos one_pos two_pos 2 (by norm_num),1793    crossing_right_one_law 1 1 3 one_pos one_pos (by norm_num) 2 (by norm_num),1794    crossing_right_one_law 1 1 2 one_pos one_pos two_pos 2 (by norm_num),1795    crossing_one_one_law 1 1 one_pos one_pos 2 (by norm_num)]1796  simp only [Expr.eval, tangentCount_single_one_four, d1, d2, d3, d4, d5, d6, d7, d8, d9, d10,1797    ite_mem_erase, zero_mul]1798  simp only [ite_eq_mul_indicator]1799  simp (disch := decide) only [tangentCount, divisorCount_zero, divisorCount_cell]1800  simp only [divisorProbability, tri, State.degree, Nat.reduceMul, Nat.reduceAdd, Fin.isValue,1801    Fin.coe_ofNat_eq_mod, one_mul, Nat.one_mod, Order.lt_two_iff, zero_le, Nat.div_self, eminusOne,1802    Expr.sub, Expr.neg, Nat.one_lt_ofNat, ↓reduceIte, Expr.eval, eval_pow, pow_one, mul_one,1803    Nat.reduceMod, Nat.reduceDiv, Nat.reduceLT, one_div, falling, availablePoints, zero_add,1804    Int.cast_zero, List.range_succ, List.range_zero, List.nil_append, List.pure_def,1805    List.bind_eq_flatMap, List.flatMap_cons, CharP.cast_eq_zero, List.flatMap_nil, List.append_nil,1806    List.map_cons, List.map_nil, eval_prod, add_zero, mul_zero, List.prod_cons, List.prod_nil,1807    Nat.factorial_one, Nat.cast_one, div_one, Nat.lt_add_one, List.cons_append, Nat.factorial_two,1808    Nat.cast_ofNat, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, mul_div_cancel_left₀,1809    Multiset.singleton_add, Multiset.add_cons, OfNat.ofNat_ne_one, pointCount_two, Nat.mod_succ,1810    lt_self_iff_false, pow_zero, Multiset.cons_add, Multiset.insert_eq_cons]1811  sort_types1812  ring1813 1814private theorem divisorCount_m4_projective_at_two :1815    (divisorCount 1 m4Split).eval 2 = 0 ∧ (divisorCount 1 m4SplitTangent).eval 2 = 3 ∧1816    (divisorCount 1 m4SplitQuadratic).eval 2 = 3 ∧ (divisorCount 1 m4ContactThree).eval 2 = 6 ∧1817    (divisorCount 1 m4Cubic).eval 2 = 6 ∧ (divisorCount 1 m4TwoTangent).eval 2 = 3 ∧1818    (divisorCount 1 m4TangentQuadratic).eval 2 = 3 ∧ (divisorCount 1 m4TwoQuadratic).eval 2 = 0 ∧1819    (divisorCount 1 m4QuadraticContact).eval 2 = 1 ∧ (divisorCount 1 m4Inert).eval 2 = 3 ∧1820    (divisorCount 1 m4Contact).eval 2 = 3 := by1821  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;>1822  simp [divisorCount_eval, Fin.prod_univ_four, Fin.sum_univ_four, falling, eval_prod,1823    availablePoints, Expr.eval, Expr.sub, Expr.neg, List.range_succ, pointCount_two,1824    pointCount_three, pointCount_four, m4Split, m4SplitTangent, m4SplitQuadratic, m4ContactThree,1825    m4Cubic, m4TwoTangent, m4TangentQuadratic, m4TwoQuadratic, m4QuadraticContact, m4Inert,1826    m4Contact] <;> norm_num [Nat.factorial]1827 1828private theorem coeff_m4Contact_at_two (σ : FactorType) :1829    coeffAt 2 (childProd (otherChildren 1 m4Contact)) σ = coeffAt 2 (stateLaw (.single 1 4)) σ := by1830  rw [coeff_otherChildren _ [(1, .single 1 4)] (by decide)]1831  simp only [childProd, List.map_cons, List.map_nil, lawProd_cons, lawProd_nil, coeff_mul_lawOne,1832    coeff_descend_one]1833 1834/-- **Quartic monic densities at `q = 2`.** The values at `q = 2` of the universal monic1835expressions of degree `4` on all eleven valid quartic types (and `0` on every other type). -/1836theorem monicExpr_four_eval_two (σ : FactorType) :1837    (monicExpr 4 σ).eval 2 =1838      (if σ = {(4,1)} then 107/1533 else 0) + (if σ = {(2,2)} then 454/7665 else 0) +1839      (if σ = {(1,4)} then 496/2555 else 0) + (if σ = {(2,1), (2,1)} then 2/63 else 0) +1840      (if σ = {(1,2), (1,2)} then 664/22995 else 0) +1841      (if σ = {(1,2), (2,1)} then 460/4599 else 0) +1842      (if σ = {(1,1), (3,1)} then 1838/15841 else 0) +1843      (if σ = {(1,1), (1,3)} then 576/2263 else 0) +1844      (if σ = {(1,1), (1,1), (2,1)} then 7348/142569 else 0) +1845      (if σ = {(1,1), (1,1), (1,2)} then 13072/142569 else 0) +1846      (if σ = {(1,1), (1,1), (1,1), (1,1)} then 344/142569 else 0) := by1847  obtain ⟨d1, d2, d3, d4, d5, d6, d7, d8, d9, d10, d11⟩ := divisorCount_m4_at_two1848  rw [monicExpr, coeff_globalLaw, residuePatterns_four]1849  repeat rw [Finset.sum_insert (by decide)]1850  rw [Finset.sum_singleton]1851  simp only [Bool.false_eq_true, if_false, d1, d2, d3, d4, d5, d6, d7, d8, d9, d10, d11, zero_mul,1852    zero_add, coeff_m4Inert, coeff_m4Cubic, coeff_m4SplitQuadratic, coeff_m4ContactThree,1853    coeff_m4TangentQuadratic, coeff_m4TwoTangent, coeff_m4QuadraticContact, coeff_m4Contact_at_two,1854    single_four_law_at_two]1855  simp only [ite_eq_mul_indicator]1856  simp only [Expr.eval, eval_pow]1857  sort_types1858  ring1859 1860/-- **Quartic projective densities at `q = 2`.** The values at `q = 2` of the universal projective1861expressions of degree `4` on all eleven valid quartic types (and `0` on every other type). -/1862theorem projectiveExpr_four_eval_two (σ : FactorType) :1863    (projectiveExpr 4 σ).eval 2 =1864      (if σ = {(4,1)} then 856/15841 else 0) + (if σ = {(2,2)} then 522/15841 else 0) +1865      (if σ = {(1,4)} then 205/2044 else 0) + (if σ = {(2,1), (2,1)} then 10/217 else 0) +1866      (if σ = {(1,2), (1,2)} then 2799/126728 else 0) +1867      (if σ = {(1,2), (2,1)} then 1397/15841 else 0) +1868      (if σ = {(1,1), (3,1)} then 2412/15841 else 0) +1869      (if σ = {(1,1), (1,3)} then 453/2263 else 0) +1870      (if σ = {(1,1), (1,1), (2,1)} then 2253/15841 else 0) +1871      (if σ = {(1,1), (1,1), (1,2)} then 8987/63364 else 0) +1872      (if σ = {(1,1), (1,1), (1,1), (1,1)} then 2517/126728 else 0) := by1873  obtain ⟨d1, d2, d3, d4, d5, d6, d7, d8, d9, d10, d11⟩ := divisorCount_m4_projective_at_two1874  rw [projectiveExpr, coeff_globalLaw, residuePatterns_four]1875  repeat rw [Finset.sum_insert (by decide)]1876  rw [Finset.sum_singleton]1877  simp only [if_true, d1, d2, d3, d4, d5, d6, d7, d8, d9, d10, d11, zero_mul, zero_add,1878    coeff_m4Inert, coeff_m4Cubic, coeff_m4SplitQuadratic, coeff_m4ContactThree,1879    coeff_m4TangentQuadratic, coeff_m4TwoTangent, coeff_m4QuadraticContact, coeff_m4Contact_at_two,1880    coeff_m4SplitTangent, single_four_law_at_two]1881  simp only [ite_eq_mul_indicator]1882  simp only [Expr.eval, projectiveNormalizer, eval_sum, List.range_succ, List.range_zero,1883    List.map_append, List.map_cons, List.map_nil, eval_pow]1884  sort_types1885  norm_num1886  ring1887 1888end DegreeFour1889 1890/-! ### Regression guards: point values of the universal expressions -/1891 1892/-- The three quadratic monic types are equidistributed at `q = 2`: split. -/1893theorem monicExpr_two_split_eval_two : (monicExpr 2 {(1,1), (1,1)}).eval 2 = 1/3 := by1894  rw [monicExpr_two_eval 2 one_lt_two]; simp +decide; norm_num1895 1896/-- The three quadratic monic types are equidistributed at `q = 2`: inert. -/1897theorem monicExpr_two_inert_eval_two : (monicExpr 2 {(1,2)}).eval 2 = 1/3 := by1898  rw [monicExpr_two_eval 2 one_lt_two]; simp +decide; norm_num1899 1900/-- The three quadratic monic types are equidistributed at `q = 2`: ramified. -/1901theorem monicExpr_two_ramified_eval_two : (monicExpr 2 {(2,1)}).eval 2 = 1/3 := byExample 7.31902  rw [monicExpr_two_eval 2 one_lt_two]; simp +decide; norm_num1903 1904/-- Totally ramified cubics at `q = 3`: `A_{3,(3,1)}(3) = 10/121`. -/1905theorem monicExpr_three_totally_ramified_eval_three : (monicExpr 3 {(3,1)}).eval 3 = 10/121 := by(10.8)1906  rw [monicExpr_three_eval 3 (by norm_num)]; simp +decide; norm_num1907 1908/-- Totally ramified quartics at `q = 2`: `A_{4,(4,1)}(2) = 107/1533`. -/1909theorem monicExpr_four_totally_ramified_eval_two : (monicExpr 4 {(4,1)}).eval 2 = 107/1533 := byExample 10.41910  rw [monicExpr_four_eval_two]; simp +decide1911 1912/-- Totally ramified binary quartic forms at `q = 2`: `B_{4,(4,1)}(2) = 856/15841`. -/1913theorem projectiveExpr_four_totally_ramified_eval_two :Example 10.41914    (projectiveExpr 4 {(4,1)}).eval 2 = 856/15841 := by1915  rw [projectiveExpr_four_eval_two]; simp +decide1916 1917/-- Quartics generating a ramified quadratic extension of a quadratic one (type `(2,2)`) at1918`q = 2`: `454/7665`. -/1919theorem monicExpr_four_ramified_quadratic_eval_two : (monicExpr 4 {(2,2)}).eval 2 = 454/7665 := by1920  rw [monicExpr_four_eval_two]; simp +decide1921 1922/-- Products of two distinct inert quadratics (type `(1,2),(1,2)`) at `q = 2`: `664/22995`. -/1923theorem monicExpr_four_two_inert_quadratics_eval_two :1924    (monicExpr 4 {(1,2), (1,2)}).eval 2 = 664/22995 := by1925  rw [monicExpr_four_eval_two]; simp +decide1926 1927/-! ### Density corollaries of `main_dvr` -/1928 1929section Densities1930 1931open IsLocalRing1932 1933variable (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]1934  [IsAdicComplete (maximalIdeal O) O] [Finite (ResidueField O)] [TopologicalSpace O]1935  [IsTopologicalRing O] [CompactSpace O] [T2Space O] [SecondCountableTopology O]1936  [MeasurableSpace O] [BorelSpace O]1937 1938private theorem densityValue_eq {x : Expr} {q : ℕ} {r : ℚ} (h : x.eval q = r) :1939    densityValue x q = ENNReal.ofReal r := by1940  rw [densityValue, h]1941 1942omit [IsAdicComplete (maximalIdeal O) O] [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O]1943  [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O] in1944private theorem one_lt_card_residueField : 1 < (Nat.card (ResidueField O) : ℚ) := by1945  exact_mod_cast Finite.one_lt_card1946 1947/-- Over any complete DVR with finite residue field of cardinality `q`, a random monic quadratic1948is ramified (type `(2,1)`) with probability `1 / (q + 1)`. -/1949theorem monicDensity_two_ramified (htop : IsAdic (maximalIdeal O)) :(1.3)1950    monicDensity O 2 {(2,1)} = ENNReal.ofReal (1 / (Nat.card (ResidueField O) + 1)) := by1951  rw [(main_dvr O htop 2 {(2,1)}).1, densityValue_eq1952    (monicExpr_two_eval _ (one_lt_card_residueField O) _)]1953  simp +decide1954 1955/-- Over any complete DVR with finite residue field of cardinality `q`, a random primitive binary1956quadratic form is ramified (type `(2,1)`) with probability `q / (q² + q + 1)`. -/1957theorem projectiveDensity_two_ramified (htop : IsAdic (maximalIdeal O)) :Example 7.31958    projectiveDensity O 2 {(2,1)} = ENNReal.ofReal (Nat.card (ResidueField O) /1959      ((Nat.card (ResidueField O)) ^ 2 + Nat.card (ResidueField O) + 1)) := by1960  rw [(main_dvr O htop 2 {(2,1)}).2, densityValue_eq1961    (projectiveExpr_two_eval _ (one_lt_card_residueField O) _)]1962  simp +decide1963 1964/-- Residue field `𝔽₃`: a random monic cubic is totally ramified with probability `10/121`. -/1965theorem monicDensity_three_totally_ramified_of_card_eq_three (htop : IsAdic (maximalIdeal O))(10.8)1966    (hq : Nat.card (ResidueField O) = 3) : monicDensity O 3 {(3,1)} = ENNReal.ofReal (10/121) := by1967  rw [(main_dvr O htop 3 {(3,1)}).1, hq,1968    densityValue_eq monicExpr_three_totally_ramified_eval_three]1969  norm_num1970 1971/-- Residue field `𝔽₂`: a random monic quartic is totally ramified with probability `107/1533`. -/1972theorem monicDensity_four_totally_ramified_of_card_eq_two (htop : IsAdic (maximalIdeal O))Example 10.41973    (hq : Nat.card (ResidueField O) = 2) :1974    monicDensity O 4 {(4,1)} = ENNReal.ofReal (107/1533) := by1975  rw [(main_dvr O htop 4 {(4,1)}).1, hq,1976    densityValue_eq monicExpr_four_totally_ramified_eval_two]1977  norm_num1978 1979/-- Residue field `𝔽₂`: a random primitive binary quartic form is totally ramified with1980probability `856/15841`. -/1981theorem projectiveDensity_four_totally_ramified_of_card_eq_two (htop : IsAdic (maximalIdeal O))1982    (hq : Nat.card (ResidueField O) = 2) :1983    projectiveDensity O 4 {(4,1)} = ENNReal.ofReal (856/15841) := by1984  rw [(main_dvr O htop 4 {(4,1)}).2, hq,1985    densityValue_eq projectiveExpr_four_totally_ramified_eval_two]1986  norm_num1987 1988/-- Residue field `𝔽₂`: a random monic quartic is irreducible of type `(2,2)` with probability1989`454/7665`. -/1990theorem monicDensity_four_ramified_quadratic_of_card_eq_two (htop : IsAdic (maximalIdeal O))1991    (hq : Nat.card (ResidueField O) = 2) :1992    monicDensity O 4 {(2,2)} = ENNReal.ofReal (454/7665) := by1993  rw [(main_dvr O htop 4 {(2,2)}).1, hq,1994    densityValue_eq monicExpr_four_ramified_quadratic_eval_two]1995  norm_num1996 1997/-- Residue field `𝔽₂`: a random monic quartic is a product of two distinct inert quadratics with1998probability `664/22995`. -/1999theorem monicDensity_four_two_inert_quadratics_of_card_eq_two (htop : IsAdic (maximalIdeal O))2000    (hq : Nat.card (ResidueField O) = 2) :2001    monicDensity O 4 {(1,2), (1,2)} = ENNReal.ofReal (664/22995) := by2002  rw [(main_dvr O htop 4 {(1,2), (1,2)}).1, hq,2003    densityValue_eq monicExpr_four_two_inert_quadratics_eval_two]2004  norm_num2005 2006end Densities2007 2008open PowerSeries in2009open scoped PowerSeries.WithPiTopology in2010/-- End-to-end test: over `𝔽₂⟦X⟧`, a random monic quartic is totally ramified with probability2011`107/1533`. -/2012theorem monicDensity_powerSeries_zmod_two_four_totally_ramified :Example 10.42013    monicDensity (ZMod 2)⟦X⟧ 4 {(4,1)} = ENNReal.ofReal (107/1533) := by2014  rw [(main_dvr_zmod 2 4 {(4,1)}).1,2015    densityValue_eq monicExpr_four_totally_ramified_eval_two]2016  norm_num2017 2018end SurfaceBlowup.Tests2019 2020#print axioms SurfaceBlowup.Tests.monicExpr_four_eval_two2021#print axioms SurfaceBlowup.Tests.projectiveExpr_four_eval_two2022#print axioms SurfaceBlowup.Tests.monicExpr_three_eval2023#print axioms SurfaceBlowup.Tests.projectiveExpr_two_eval2024#print axioms SurfaceBlowup.Tests.monicDensity_two_ramified2025#print axioms SurfaceBlowup.Tests.projectiveDensity_two_ramified2026#print axioms SurfaceBlowup.Tests.monicDensity_three_totally_ramified_of_card_eq_three2027#print axioms SurfaceBlowup.Tests.monicDensity_four_totally_ramified_of_card_eq_two2028#print axioms SurfaceBlowup.Tests.projectiveDensity_four_totally_ramified_of_card_eq_two2029#print axioms SurfaceBlowup.Tests.monicDensity_four_ramified_quadratic_of_card_eq_two2030#print axioms SurfaceBlowup.Tests.monicDensity_four_two_inert_quadratics_of_card_eq_two2031#print axioms SurfaceBlowup.Tests.monicDensity_powerSeries_zmod_two_four_totally_ramified