Pattern sums, crossing factorization and unitarity

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.Reciprocity.Plethysm7 8/-!9# Pattern sums, crossing factorization and unitarity10 11Coefficient-level identities connecting the recursion laws of single-boundary states `S(a;n)` and12crossing states `T(a,b;c,h)` to the series calculus of the reciprocity proof: pattern sums and13their independence of the ambient dimension, reciprocal and Adams substitution in laws, closed14forms of the weight rational functions, the Euler transform as a pattern sum, the crossing15factorization of the contact series `U_{a,b}`, and its unitarity `U U† ≡ 1` by induction.16 17## Main results18 19* `coeff_eulerSer`: `[xⁿ] eulerSer ε a = patternSum ε a n n`.20* `coeff_recipCoef_lawCoef`, `lawCoef_globalLaw_false`, `lawCoef_globalLaw_true`: coefficients of21  the laws in `Coef`.22* `crossingQ_eq_qmul_qplus_qdiag_qminus`: `U_{a,b} = U_{a+b,b}⁺ J(P_{a+b}) U_{a,a+b}⁻`.23* `qcongr_crossingQ_mul_qdagger`: unitarity of `U_{a,b}` through degree `2M + 1`.24* `coeff_qact_crossingQ_gaussPhi_eulerSer`, `lawCoef_single_self_term`: the two sides of the25  single-boundary operator equation.26 27## Implementation notes28 29The recursion is unfolded with `exitLaw` and `state_law_unfold` from30`SurfaceBlowup.Formula.StateCombinatorics`, so that the reciprocity proof only depends on the31combinatorics of the formula.32 33Provenance: `Thm_SurfaceBlowupV2_recip_{pattern_extend, pattern_pad, stateLaw_globalLaw_wf,34monic_projective_coef, subst_inv_var, lawCoef_recip_subst, subst_pow_var, lawCoef_descend,35otherChildren_coef, crossing_term_coef, crossing_exit_regroup, globalLaw_coef, single_term_coef,36weights_rational, closing_scalar, countSum_eq, crossing_exchange, crossingQ_basic,37euler_product_trunc, euler_coeff_product, euler_coeff_pattern, crossing_factorization_coeff,38crossing_factorization, contact_induction, eulerSer_coeff_one, cluster_base,39single_operator_coeff, single_self_term_value}`.40-/41 42namespace SurfaceBlowup43 44/-! ### Pattern sums -/45 46@[to_additive]47private theorem prod_castLE_extend {M : Type*} [CommMonoid M] (N N' : ℕ) (hNN' : N ≤ N')48    (f : Fin N' → M) (g : Fin N → M) (h1 : ∀ i : Fin N, f (Fin.castLE hNN' i) = g i)49    (h2 : ∀ i : Fin N', N ≤ i.val → f i = 1) : ∏ i, f i = ∏ i, g i := by50  rw [← Finset.prod_subset (Finset.subset_univ (Finset.univ.map (Fin.castLEEmb hNN')))]51  · rw [Finset.prod_map]52    exact Finset.prod_congr rfl (fun i _ ↦ h1 i)53  · intro i _ hi54    apply h255    by_contra hc56    exact hi (Finset.mem_map.2 ⟨⟨i.val, by omega⟩, Finset.mem_univ _, Fin.ext rfl⟩)57 58section Extend59 60variable {N N' : ℕ} (hNN' : N ≤ N') {m : Pattern N} {m' : Pattern N'}61  (h : ∀ i j : Fin N', (m' (i, j)).val =62    if hij : i.val < N ∧ j.val < N then (m (⟨i.val, hij.1⟩, ⟨j.val, hij.2⟩)).val else 0)63include h64 65@[to_additive]66private theorem prod_row_castLE {M : Type*} [CommMonoid M] (g : ℕ → ℕ → M)67    (hg : ∀ j, g j 0 = 1) (i : Fin N) :68    ∏ j : Fin N', g j (m' (Fin.castLE hNN' i, j)).val = ∏ j : Fin N, g j (m (i, j)).val :=69  prod_castLE_extend N N' hNN' _ _ (fun j ↦ by simp [h]) fun j hj ↦ by simp [h, not_lt.2 hj, hg]70 71@[to_additive]72private theorem prod_row_eq_one {M : Type*} [CommMonoid M] (g : ℕ → ℕ → M)73    (hg : ∀ j, g j 0 = 1) (i : Fin N') (hi : N ≤ i.val) :74    ∏ j : Fin N', g j (m' (i, j)).val = 1 :=75  Finset.prod_eq_one fun j _ ↦ by simp [h, not_lt.2 hi, hg]76 77include hNN' in78@[to_additive]79private theorem prod_pattern_extend {M : Type*} [CommMonoid M] (g : ℕ → ℕ → ℕ → M)80    (hg : ∀ i j, g i j 0 = 1) :81    ∏ ij : Fin N' × Fin N', g ij.1 ij.2 (m' ij).val =82      ∏ ij : Fin N × Fin N, g ij.1 ij.2 (m ij).val := by83  rw [Fintype.prod_prod_type, Fintype.prod_prod_type]84  exact prod_castLE_extend N N' hNN' _ _ (fun i ↦ prod_row_castLE hNN' h (g i) (hg i) i)85    fun i hi ↦ prod_row_eq_one h (g i) (hg i) i hi86 87include hNN' in88private theorem patternWeight_extend : patternWeight m' = patternWeight m :=89  sum_pattern_extend hNN' h (fun i j k ↦ (i + 1) * (j + 1) * k) fun _ _ ↦ mul_zero _90 91include hNN' in92private theorem rational_divisorCount_extend (ε : ℤ) :93    (divisorCount ε m').rational = (divisorCount ε m).rational := by94  rw [rational_divisorCount, rational_divisorCount]95  refine prod_castLE_extend N N' hNN' _ _ (fun i ↦ ?_) fun i hi ↦ ?_96  · rw [sum_row_castLE hNN' h (fun _ k ↦ k) (fun _ ↦ rfl),97      prod_row_castLE hNN' h (fun _ k ↦ ((k.factorial : ℕ) : ℚ)) (fun _ ↦ by simp)]98    simp99  · rw [sum_row_eq_zero h (fun _ k ↦ k) (fun _ ↦ rfl) i hi,100      prod_row_eq_one h (fun _ k ↦ ((k.factorial : ℕ) : ℚ)) (fun _ ↦ by simp) i hi]101    simp102 103end Extend104 105/-- The pattern sum of weight `w ≤ N` does not change when the ambient dimension grows from `N`106to `N' ≥ N` (patterns of weight `w` live in the first `w` rows and columns). -/107private theorem patternSum_extend (ε : ℤ) (a N N' w : ℕ) (hNN' : N ≤ N') (hw : w ≤ N) :108    patternSum ε a N w = patternSum ε a N' w := by109  let ext : Pattern N → Pattern N' := fun m ij ↦110    if hij : ij.1.val < N ∧ ij.2.val < N then111      Fin.castLE (by omega) (m (⟨ij.1.val, hij.1⟩, ⟨ij.2.val, hij.2⟩)) else 0112  let res : Pattern N' → Pattern N := fun m' ij ↦113    ⟨min (m' (Fin.castLE hNN' ij.1, Fin.castLE hNN' ij.2)).val N, by omega⟩114  have hext (m : Pattern N) (i j : Fin N') : ((ext m) (i, j)).val =115      if hij : i.val < N ∧ j.val < N then (m (⟨i.val, hij.1⟩, ⟨j.val, hij.2⟩)).val else 0 := by116    simp only [ext]117    split_ifs <;> simp118  have hres (m' : Pattern N') (hm : patternWeight m' = w) (i j : Fin N') : (m' (i, j)).val =119      if hij : i.val < N ∧ j.val < N then ((res m') (⟨i.val, hij.1⟩, ⟨j.val, hij.2⟩)).val120      else 0 := by121    split_ifs with hij122    · simpa [res, Fin.castLE] using123        (pattern_entry_le_patternWeight N' m' (i, j)).trans (hm.trans_le hw)124    · refine pattern_entry_eq_zero_of_lt N' m' (i, j) ?_125      rw [hm]126      rcases not_and_or.mp hij with h | h <;> dsimp only <;> nlinarith127  refine Finset.sum_nbij' ext res (fun m hm ↦ ?_) (fun m' hm' ↦ ?_) (fun m _ ↦ ?_)128    (fun m' hm' ↦ ?_) fun m _ ↦ ?_129  · simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hm ⊢130    rw [patternWeight_extend hNN' (hext m), hm]131  · simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hm' ⊢132    rw [← patternWeight_extend hNN' (hres m' hm'), hm']133  · funext ij134    have := (m ij).isLt135    simp only [res, Fin.ext_iff, hext, Fin.val_castLE, ij.1.isLt, ij.2.isLt, and_self, dite_true,136      Fin.eta, Prod.mk.eta]137    omega138  · simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hm'139    funext ⟨i, j⟩140    exact Fin.ext ((hext _ i j).trans (hres m' hm' i j).symm)141  · rw [rational_divisorCount_extend hNN' (hext m),142      prod_pattern_extend hNN' (hext m) (fun i j k ↦143        adamsCoef (i + 1) (lawCoef (stateLaw (State.single a (j + 1)))) ^ k) fun _ _ ↦ pow_zero _]144 145/-- The pattern sum of weight `w` is independent of the ambient dimension, as long as it is at146least `w`. -/147theorem patternSum_eq_of_le (ε : ℤ) (a N N' w : ℕ) (hN : w ≤ N) (hN' : w ≤ N') :148    patternSum ε a N w = patternSum ε a N' w := by149  rw [patternSum_extend ε a N (max N N') w (le_max_left _ _) hN,150    patternSum_extend ε a N' (max N N') w (le_max_right _ _) hN']151 152/-- The laws of valid states consist of well-formed expressions. -/153theorem lawWf_stateLaw (s : State) (hs : s.Valid) : LawWf (stateLaw s) :=154  (local_law_safe s hs).lawWf155 156/-- The global laws consist of well-formed expressions. -/157theorem lawWf_globalLaw (ε : Bool) (n : ℕ) : LawWf (globalLaw ε n) :=158  (global_law_safe n ε).lawWf159 160/-- The `σ`-coefficient of the global monic law, read in `Coef`, is the rational function of161`monicExpr n σ`. -/162theorem coeff_lawCoef_globalLaw_false (n : ℕ) (σ : FactorType) :163    (lawCoef (globalLaw false n)).coeff σ = (monicExpr n σ).rational :=164  coeff_lawCoef _ (lawWf_globalLaw false n) σ165 166/-- The `σ`-coefficient of the global projective law, read in `Coef`, is the rational function167of `projectiveExpr n σ`. -/168theorem coeff_lawCoef_globalLaw_true (n : ℕ) (σ : FactorType) :169    (lawCoef (globalLaw true n)).coeff σ = (projectiveExpr n σ).rational :=170  coeff_lawCoef _ (lawWf_globalLaw true n) σ171 172/-- Substituting a well-formed expression `e` for the variable, where `e.rational = φ(q)` for a173ring endomorphism `φ` of `ℚ(q)`, preserves well-formedness and acts on rational functions as174`φ` (the two facts are proved by a joint induction). -/175private theorem wf_subst_and_rational_subst (e : Expr) (he : e.wf) (φ : RatFunc ℚ →+* RatFunc ℚ)176    (hX : e.rational = φ RatFunc.X) (x : Expr) (hx : x.wf) :177    (x.subst e).wf ∧ (x.subst e).rational = φ x.rational := by178  induction x with179  | const r =>180    refine ⟨trivial, ?_⟩181    simp only [Expr.subst, Expr.rational_const]182    rw [eq_ratCast RatFunc.C r, map_ratCast]183  | var => exact ⟨he, by simp only [Expr.subst, Expr.rational_var, hX]⟩184  | add a b iha ihb =>185    obtain ⟨wa, ea⟩ := iha hx.1186    obtain ⟨wb, eb⟩ := ihb hx.2187    refine ⟨⟨wa, wb⟩, ?_⟩188    simp only [Expr.subst]189    rw [Expr.rational_add wa wb, Expr.rational_add hx.1 hx.2, map_add, ea, eb]190  | mul a b iha ihb =>191    obtain ⟨wa, ea⟩ := iha hx.1192    obtain ⟨wb, eb⟩ := ihb hx.2193    refine ⟨⟨wa, wb⟩, ?_⟩194    simp only [Expr.subst]195    rw [Expr.rational_mul, Expr.rational_mul a b, map_mul, ea, eb]196  | inv a iha =>197    obtain ⟨ha, hn⟩ := hx198    obtain ⟨wa, ea⟩ := iha ha199    have hr : a.rational ≠ 0 :=200      div_ne_zero (RatFunc.algebraMap_ne_zero hn)201        (RatFunc.algebraMap_ne_zero (Expr.fraction_snd_ne_zero ha))202    refine ⟨⟨wa, fun h ↦ ?_⟩, ?_⟩203    · refine hr (φ.injective ?_)204      rw [← ea, map_zero, Expr.rational, h, map_zero, zero_div]205    · simp only [Expr.subst]206      rw [Expr.rational_inv, Expr.rational_inv a, map_inv₀, ea]207 208/-- Substituting a well-formed expression `e` with `e.rational = φ(q)` for the variable of a209well-formed expression acts on rational functions as `φ`. -/210private theorem rational_subst_of_wf (e : Expr) (he : e.wf) (φ : RatFunc ℚ →+* RatFunc ℚ)211    (hX : e.rational = φ RatFunc.X) {x : Expr} (hx : x.wf) :212    (x.subst e).rational = φ x.rational :=213  (wf_subst_and_rational_subst e he φ hX x hx).2214 215/-- Substituting `q ↦ 1/q` into a well-formed expression acts on its rational function as216`recipRat`. -/217private theorem rational_subst_inv_var (x : Expr) (hx : x.wf) :218    (x.subst (.inv .var)).rational = recipRat x.rational :=219  rational_subst_of_wf (.inv .var) ⟨trivial, by simp [Expr.fraction, Polynomial.X_ne_zero]⟩ recipRat220    (by rw [Expr.rational_inv, Expr.rational_var, recipRat_X]) hx221 222/-- For a well-formed law, the `σ`-coefficient of `lawCoef L` with `q ↦ 1/q` applied is the223rational function of the coefficient expression with `q ↦ 1/q` substituted. -/224theorem coeff_recipCoef_lawCoef (L : Law) (hL : LawWf L) (σ : FactorType) :225    (recipCoef (lawCoef L)).coeff σ = ((lawCoeff L σ).subst (.inv .var)).rational := by226  rw [recipCoef_coeff, coeff_lawCoef L hL σ, rational_subst_inv_var _ (hL.wf_lawCoeff σ)]227 228/-- Descending a well-formed law along a degree-`δ` extension acts on `lawCoef` as the Adams229operation `ψ_δ`. -/230private theorem lawCoef_lawDescend (δ : ℕ) (hδ : 0 < δ) (L : Law) (hL : LawWf L) :231    lawCoef (lawDescend δ L) = adamsCoef δ (lawCoef L) := by232  unfold lawCoef lawDescend233  rw [map_list_sum, List.map_map, List.map_map]234  congr 1235  refine List.map_congr_left fun z hz ↦ ?_236  simp only [Function.comp]237  rw [rational_subst_of_wf _ (Expr.wf_pow (x := Expr.var) trivial δ) (adamsRat δ)238    (by rw [Expr.rational_pow, Expr.rational_var, adamsRat_X δ hδ]) (hL z hz), adamsCoef_single]239 240/-- The product of the descended laws of the off-boundary children of a pattern `m` is241`Π_{(i,j)} ψ_{i+1}(F_{S(a;j+1)})^{m(i,j)}`. -/242private theorem lawCoef_otherChildren (a N : ℕ) (ha : 0 < a) (m : Pattern N) :243    lawCoef (lawProd ((otherChildren a m).map fun z ↦ lawDescend z.1 (stateLaw z.2))) =244        ∏ ij : Fin N × Fin N, (adamsCoef (ij.1.val + 1) (lawCoef245        (stateLaw (State.single a (ij.2.val + 1))))) ^ (m ij).val := by246  have hf : ∀ ij : Fin N × Fin N, lawCoef (lawDescend (ij.1.val + 1)247      (stateLaw (State.single a (ij.2.val + 1)))) = adamsCoef (ij.1.val + 1)248      (lawCoef (stateLaw (State.single a (ij.2.val + 1)))) := by249    intro ij250    refine lawCoef_lawDescend _ (Nat.succ_pos _) _ ?_251    exact (lawWf_stateLaw _ (by simp [State.Valid]; omega))252  rw [(lawCoef_lawProd _)]253  unfold otherChildren254  simp only [List.map_flatMap, List.map_replicate, hf]255  rw [List.flatMap_def, List.prod_flatten, List.map_map, Finset.prod_eq_multiset_prod,256      ← Multiset.prod_map_toList]257  simp [List.prod_replicate, Finset.toList, Function.comp_def]258 259private theorem prod_lawCoef_optional_child (p : Prop) [Decidable p] (s' : State)260    (hv : ¬p → s'.Valid) :261    ((if p then [] else [((1 : ℕ), s')]).map262        (lawCoef ∘ fun z : ℕ × State ↦ lawDescend z.1 (stateLaw z.2))).prod263      = if p then 1 else lawCoef (stateLaw s') := by264  split_ifs with h265  · simp266  · simp only [List.map_cons, List.map_nil, List.prod_cons, List.prod_nil, mul_one,267      Function.comp]268    rw [lawCoef_lawDescend 1 one_pos _ (lawWf_stateLaw _ (hv h)), adamsCoef_one]269 270/-- The contribution of an allowed tangent pattern `P` of the crossing state `T(a,b;c,h)` to its271recursion, as an element of `Coef`: the weights times the laws of the crossing children and the272off-boundary product. -/273private theorem lawCoef_crossing_term (a b c h : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)274    (hh : 0 < h)275    (P : TangentPattern (State.crossing a b c h).degree) (hP : Allowed (State.crossing a b c h) P) :276    lawCoef (lawScale (.mul (tangentCount (State.crossing a b c h) P)277        (divisorProbability (State.crossing a b c h) P.d.val))278        (lawProd ((children (State.crossing a b c h) P).map fun z ↦279        lawDescend z.1 (stateLaw z.2)))) = scalar ((divisorCount (-1) P.other).rational *280        (divisorProbability (State.crossing a b c h) P.d.val).rational) *281        ((if P.rt.val = 0 then 1 else lawCoef (stateLaw (State.crossing (a + b) a P.rt.val282        (c - P.d.val)))) * (if P.rx.val = 0 then 1 else lawCoef283        (stateLaw (State.crossing (a + b) b P.rx.val (h - P.d.val)))) *284        ∏ ij : Fin (State.crossing a b c h).degree × Fin (State.crossing a b c h).degree,285        (adamsCoef (ij.1.val + 1) (lawCoef (stateLaw (State.single (a + b) (ij.2.val + 1))))) ^286        (P.other ij).val) := by287  have hv : ∀ z ∈ children (State.crossing a b c h) P, z.2.Valid :=288    children_valid (State.crossing a b c h) ⟨ha, hb, hc, hh⟩ P hP289  rw [lawCoef_lawScale, Expr.rational_mul]290  congr 1291  have hch : children (State.crossing a b c h) P =292      (if P.rt.val=0 then [] else [(1,State.crossing (a+b) a P.rt.val (c-P.d.val))]) ++293      (if P.rx.val=0 then [] else [(1,State.crossing (a+b) b P.rx.val (h-P.d.val))]) ++294      otherChildren (a+b) P.other := rfl295  have hoth := lawCoef_otherChildren (a+b) _ (by omega) P.other296  rw [lawCoef_lawProd, List.map_map] at hoth297  rw [lawCoef_lawProd, List.map_map, hch, List.map_append, List.map_append, List.prod_append,298    List.prod_append, ← hoth, prod_lawCoef_optional_child _ _ ?_,299    prod_lawCoef_optional_child _ _ ?_]300  all_goals first | rfl | exact fun h1 ↦ hv (1, _) (by rw [hch]; simp [h1])301 302/-- Summing the pattern terms `scalar (divisorCount ε m · Y) · B · Π ψ_{i+1}(F_{S(a;j+1)})^{m(i,j)}`303over the patterns `m` of weight `w` gives `scalar Y · B · patternSum ε a N w`. -/304theorem sum_patterns_scalar_mul_eq_patternSum (ε : ℤ) (a N w : ℕ) (Y : RatFunc ℚ) (B : Coef) :305    ∑ m ∈ (Finset.univ : Finset (Pattern N)).filter (fun m ↦ patternWeight m = w),306      scalar ((divisorCount ε m).rational * Y) * (B * ∏ ij : Fin N × Fin N,307        (adamsCoef (ij.1.val + 1) (lawCoef (stateLaw (State.single a (ij.2.val + 1))))) ^308          (m ij).val) = scalar Y * (B * patternSum ε a N w) := by309  unfold patternSum310  rw [Finset.mul_sum, Finset.mul_sum]311  refine Finset.sum_congr rfl fun m _ ↦ ?_312  rw [scalar_mul, Algebra.smul_def, ← scalar_eq_algebraMap]313  ring314 315/-- The exit law of `T(a,b;c,h)` regrouped by divisor degree `d` and tangent depths `rt`, `rx`316into crossing-child laws and pattern sums `patternSum (-1) (a+b) (ac+bh) (d-rt-rx)`. -/317private theorem lawCoef_exitLaw_crossing (a b c h : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)318    (hh : 0 < h) :319    lawCoef (exitLaw (State.crossing a b c h)) = ∑ d ∈ Finset.Icc 1 (min c h),320        ∑ rt ∈ Finset.range (d + 1), ∑ rx ∈ Finset.range (d + 1),321        (if ((0 < rt ↔ d < c) ∧ (0 < rx ↔ d < h) ∧ rt + rx ≤ d) then scalar322        (divisorProbability (State.crossing a b c h) d).rational *323        ((if rt = 0 then 1 else lawCoef (stateLaw (State.crossing (a + b) a rt (c - d)))) *324        (if rx = 0 then 1 else lawCoef (stateLaw (State.crossing (a + b) b rx (h - d)))) *325        patternSum (-1) (a + b) (a * c + b * h) (d - rt - rx)) else 0) := by326  classical327  unfold exitLaw328  rw [lawCoef_flatMap, Finset.sum_map_toList]329  have hns : ∀ P, ¬ SelfPattern (State.crossing a b c h) P := by330    rintro P ⟨a', c', h1, -⟩331    exact State.noConfusion h1332  simp only [hns, if_false]333  refine (Finset.sum_congr rfl (fun P hP ↦ lawCoef_crossing_term a b c h ha hb hc hh P334    (by unfold allowedPatterns at hP; exact (Finset.mem_filter.mp hP).2))).trans ?_335  rw [sum_allowedPatterns_crossing a b c h ha hb hh (fun d rt rx m ↦336    scalar ((divisorCount (-1) m).rational * (divisorProbability (State.crossing a b c h)337        d).rational) *338      ((if rt = 0 then 1 else lawCoef (stateLaw (State.crossing (a + b) a rt (c - d)))) *339        (if rx = 0 then 1 else lawCoef (stateLaw (State.crossing (a + b) b rx (h - d)))) *340        ∏ ij : Fin (State.crossing a b c h).degree × Fin (State.crossing a b c h).degree,341          (adamsCoef (ij.1.val + 1) (lawCoef (stateLaw (State.single (a + b) (ij.2.val + 1))))) ^342              (m ij).val))]343  refine Finset.sum_congr rfl (fun d _ ↦ Finset.sum_congr rfl344      (fun rt _ ↦ Finset.sum_congr rfl (fun rx _ ↦ ?_)))345  by_cases hcond : ((0 < rt ↔ d < c) ∧ (0 < rx ↔ d < h) ∧ rt + rx ≤ d)346  · rw [if_pos hcond, if_pos hcond]; exact sum_patterns_scalar_mul_eq_patternSum _ _ _ _ _ _347  · rw [if_neg hcond, if_neg hcond]348 349private theorem lawCoef_residue_flatMap (n : ℕ) (b : Bool) :350    lawCoef ((residuePatterns n).toList.flatMap fun m ↦351      lawScale (divisorCount (if b then 1 else 0) m)352        (lawProd ((otherChildren 1 m).map fun z ↦ lawDescend z.1 (stateLaw z.2))))353      = patternSum (if b then 1 else 0) 1 n n := by354  rw [lawCoef_flatMap]355  unfold patternSum residuePatterns356  rw [Finset.sum_map_toList]357  refine Finset.sum_congr rfl fun m _ ↦ ?_358  rw [lawCoef_lawScale, lawCoef_otherChildren 1 n Nat.one_pos m, Algebra.smul_def]359  rfl360 361/-- The global monic law is `q^{-n}` times the pattern sum `patternSum 0 1 n n`. -/362theorem lawCoef_globalLaw_false (n : ℕ) :(G) = (7.9)363    lawCoef (globalLaw false n) = qpow (-(n : ℤ)) * patternSum 0 1 n n := by364  have k0 := lawCoef_residue_flatMap n false365  simp only [Bool.false_eq_true, if_false] at k0366  unfold globalLaw367  simp only [Bool.false_eq_true, if_false]368  rw [lawCoef_lawScale, k0, Expr.rational_inv, Expr.rational_pow, Expr.rational_var, qpow,369    zpow_neg, zpow_natCast]370 371/-- The global projective law is the pattern sum `patternSum 1 1 n n` divided by372`1 + q + ⋯ + qⁿ`. -/373theorem lawCoef_globalLaw_true (n : ℕ) :(G) = (7.9)374    lawCoef (globalLaw true n) =375      scalar (((projectiveNormalizer n).rational)⁻¹) * patternSum 1 1 n n := by376  have k1 := lawCoef_residue_flatMap n true377  simp only [if_true] at k1378  unfold globalLaw379  simp only [if_true]380  rw [lawCoef_lawScale, k1, Expr.rational_inv]381 382/-- The contribution of an allowed tangent pattern `P` of `S(a;n)` to its recursion, as an element383of `Coef`. -/384theorem lawCoef_single_term (a n : ℕ) (ha : 0 < a) (hn : 0 < n)385    (P : TangentPattern (State.single a n).degree) (hP : Allowed (State.single a n) P) :386    lawCoef (lawScale (.mul (tangentCount (State.single a n) P)387        (divisorProbability (State.single a n) P.d.val))388        (lawProd ((children (State.single a n) P).map fun z ↦ lawDescend z.1 (stateLaw z.2)))) =389        scalar ((divisorCount 0 P.other).rational * (divisorProbability (State.single a n)390        P.d.val).rational) * ((if P.rt.val = 0 then 1 else lawCoef391        (stateLaw (State.crossing a a P.rt.val (n - P.d.val)))) *392        ∏ ij : Fin (State.single a n).degree × Fin (State.single a n).degree,393        (adamsCoef (ij.1.val + 1) (lawCoef (stateLaw (State.single a (ij.2.val + 1))))) ^394        (P.other ij).val) := by395  have hv : ∀ z ∈ children (State.single a n) P, z.2.Valid :=396    children_valid (State.single a n) ⟨ha, hn⟩ P hP397  rw [lawCoef_lawScale, Expr.rational_mul]398  congr 1399  have hch : children (State.single a n) P =400      (if P.rt.val=0 then [] else [(1,State.crossing a a P.rt.val (n-P.d.val))]) ++401      otherChildren a P.other := rfl402  have hoth := lawCoef_otherChildren a _ ha P.other403  rw [lawCoef_lawProd, List.map_map] at hoth404  rw [lawCoef_lawProd, List.map_map, hch, List.map_append, List.prod_append, ← hoth,405    prod_lawCoef_optional_child _ _ ?_]406  all_goals first | rfl | exact fun h1 ↦ hv (1, _) (by rw [hch]; simp [h1])407 408/-! ### Closed forms of the weights -/409 410/-- The divisor probability of `S(a;c)` at degree `d` is `q^{-tri d} (q-1)^{[d < c]}`. -/411theorem rational_divisorProbability_single (a c d : ℕ) :Proposition 6.1412    (divisorProbability (State.single a c) d).rational =413      ((RatFunc.X : RatFunc ℚ) ^ tri d)⁻¹ *414        ((RatFunc.X : RatFunc ℚ) - 1) ^ (if d < c then 1 else 0) := by415  simp only [divisorProbability, Expr.rational_mul, Expr.rational_inv, Expr.rational_pow,416    Expr.rational_var, rational_eminusOne]417 418/-- The divisor probability of `T(a,b;c,h)` at degree `d` is `q^{-C(d,2)}` times the crossing weight419`w_j` (`w_0 = (q-1)⁻¹`, `w_j = (q-1)^{j-1}`) with `j = [d < c] + [d < h]`. -/420private theorem rational_divisorProbability_crossing (a b c h d : ℕ) :421    (divisorProbability (State.crossing a b c h) d).rational =422      ((RatFunc.X : RatFunc ℚ) ^ chooseTwo d)⁻¹ * (if (if d < c then 1 else 0) +423        (if d < h then 1 else 0) = 0 then ((RatFunc.X : RatFunc ℚ) - 1)⁻¹ else424        ((RatFunc.X : RatFunc ℚ) - 1) ^425          ((if d < c then 1 else 0) + (if d < h then 1 else 0) - 1)) := by426  simp only [divisorProbability]427  rw [Expr.rational_mul, Expr.rational_inv, Expr.rational_pow, Expr.rational_var]428  split_ifs <;> simp [Expr.rational_inv, Expr.rational_pow, rational_eminusOne]429 430/-- The return weight is `q · q^{-tri c}`. -/431theorem rational_returnWeight (c : ℕ) :432    (returnWeight c).rational = (RatFunc.X : RatFunc ℚ) * ((RatFunc.X : RatFunc ℚ) ^ tri c)⁻¹ := by433  simp only [returnWeight, Expr.rational_mul, Expr.rational_inv, Expr.rational_pow,434    Expr.rational_var]435 436/-- The point count `(1/δ) Σ_{j ∣ δ} μ(j) q^{δ/j}` of degree-`δ` points. -/437private theorem rational_pointCount (δ : ℕ) : (pointCount δ).rational = RatFunc.C (1 / (δ : ℚ)) *438    ∑ j ∈ δ.divisors, RatFunc.C (((ArithmeticFunction.moebius j : ℤ) : ℚ)) *439    (RatFunc.X : RatFunc ℚ) ^ (δ / j) := by440  unfold pointCount441  rw [Expr.rational_mul, Expr.rational_const, Expr.rational_sum]442  · rw [List.map_map, ← Finset.sum_map_toList]443    congr 2444    refine List.map_congr_left fun j _ ↦ ?_445    simp [Expr.rational_mul, Expr.rational_const, Expr.rational_pow, Expr.rational_var]446  · intro z hz447    obtain ⟨j, _, rfl⟩ := List.mem_map.1 hz448    exact ⟨trivial, Expr.wf_pow (x := Expr.var) trivial _⟩449 450/-- The available points: `q + ε` in degree `1`, and the point count in higher degree. -/451private theorem rational_availablePoints (ε : ℤ) (δ : ℕ) :452    (availablePoints ε δ).rational =453      if δ = 1 then (RatFunc.X : RatFunc ℚ) + (ε : RatFunc ℚ) else (pointCount δ).rational := by454  unfold availablePoints455  split_ifs456  · rw [Expr.rational_add (x := Expr.var) (y := Expr.const (ε : ℚ)) trivial trivial,457      Expr.rational_var, Expr.rational_const, map_intCast]458  · rfl459 460/-- `q (q⁻¹ - q^{-tri n}) = 1 - returnWeight n`. -/461private theorem X_mul_X_inv_sub_X_zpow_neg_tri (n : ℕ) :462    (RatFunc.X : RatFunc ℚ) * ((RatFunc.X : RatFunc ℚ)⁻¹ - (RatFunc.X : RatFunc ℚ) ^463      (-(tri n : ℤ))) = 1 - (returnWeight n).rational := by464  rw [rational_returnWeight n, zpow_neg, zpow_natCast, mul_sub, mul_inv_cancel₀ RatFunc.X_ne_zero]465 466/-- For `n ≥ 2`, the return weight is not `1`: `1 - returnWeight n ≠ 0`. -/467theorem one_sub_rational_returnWeight_ne_zero (n : ℕ) (hn : 2 ≤ n) :468    1 - (returnWeight n).rational ≠ 0 := by469  have h3 : 3 ≤ tri n := by470    unfold tri471    have : 6 ≤ n * (n + 1) := by nlinarith472    omega473  intro h0474  have hX : (RatFunc.X : RatFunc ℚ) ≠ 0 := RatFunc.X_ne_zero475  have h1 : (returnWeight n).rational = 1 := by linear_combination -h0476  rw [rational_returnWeight] at h1477  have hk : (RatFunc.X : RatFunc ℚ) = (RatFunc.X : RatFunc ℚ) ^ tri n := by478    have := congrArg (· * (RatFunc.X : RatFunc ℚ) ^ tri n) h1479    simpa [mul_assoc, inv_mul_cancel₀ (pow_ne_zero _ hX)] using this480  have hp : (Polynomial.X : Polynomial ℚ) = Polynomial.X ^ tri n := by481    apply RatFunc.algebraMap_injective ℚ482    simpa [RatFunc.algebraMap_X] using hk483  have := congrArg Polynomial.natDegree hp484  simp at this485  omega486 487/-- For `n ≥ 2`, the scalar `q⁻¹ - q^{-tri n}` is nonzero. -/488theorem X_inv_sub_X_zpow_neg_tri_ne_zero (n : ℕ) (hn : 2 ≤ n) :Proof of monic/cluster reciprocity489    (RatFunc.X : RatFunc ℚ)⁻¹ - (RatFunc.X : RatFunc ℚ) ^ (-(tri n : ℤ)) ≠ 0 := fun h ↦ by490  have := X_mul_X_inv_sub_X_zpow_neg_tri n491  rw [h, mul_zero] at this492  exact one_sub_rational_returnWeight_ne_zero n hn this.symm493 494private theorem adamsRat_X_add_int (k : ℕ) (hk : 0 < k) (ε : ℤ) :495    adamsRat k (RatFunc.X + (ε : RatFunc ℚ)) = RatFunc.X ^ k + (ε : RatFunc ℚ) := by496  rw [map_add, map_intCast, (adamsRat_X k hk)]497 498private theorem availablePoints_rational_eq_sum (ε : ℤ) (m : ℕ) (hm : 0 < m) :499    ∑ k ∈ m.divisors, (RatFunc.C ((k : ℚ)⁻¹ * (((ArithmeticFunction.moebius (m / k) : ℤ) : ℚ) /500        ((m / k : ℕ) : ℚ))))501      * ((RatFunc.X : RatFunc ℚ) ^ k + (ε : RatFunc ℚ)) = (availablePoints ε m).rational := by502  rw [rational_availablePoints]503  have hm' : (m : ℚ) ≠ 0 := by exact_mod_cast hm.ne'504  have ht : ∀ k ∈ m.divisors,505      RatFunc.C ((k : ℚ)⁻¹ * (((ArithmeticFunction.moebius (m / k) : ℤ) : ℚ) / ((m / k : ℕ) : ℚ)))506        * ((RatFunc.X : RatFunc ℚ) ^ k + (ε : RatFunc ℚ))507      = (fun j : ℕ ↦ RatFunc.C (((ArithmeticFunction.moebius j : ℤ) : ℚ) / m)508          * ((RatFunc.X : RatFunc ℚ) ^ (m / j) + (ε : RatFunc ℚ))) (m / k) := by509    intro k hk510    have hk0 : (k : ℚ) ≠ 0 := by exact_mod_cast (Nat.pos_of_mem_divisors hk).ne'511    simp only [Nat.div_div_self (Nat.dvd_of_mem_divisors hk) hm.ne']512    congr 2513    rw [Nat.cast_div (Nat.dvd_of_mem_divisors hk) hk0]514    field_simp515  rw [Finset.sum_congr rfl ht, Nat.sum_div_divisors m (fun j : ℕ ↦516      RatFunc.C (((ArithmeticFunction.moebius j : ℤ) : ℚ) / m)517          * ((RatFunc.X : RatFunc ℚ) ^ (m / j) + (ε : RatFunc ℚ)))]518  split_ifs with h1519  · subst h1; simp520  · rw [rational_pointCount]521    simp only [mul_add, Finset.sum_add_distrib, Finset.mul_sum]522    have h0 : ∑ j ∈ m.divisors, RatFunc.C (((ArithmeticFunction.moebius j : ℤ) : ℚ) / m) *523        (ε : RatFunc ℚ) = 0 := by524      rw [← Finset.sum_mul, ← map_sum, ← Finset.sum_div, sum_divisors_moebius, if_neg h1]; simp525    rw [h0, add_zero]526    refine Finset.sum_congr rfl fun j _ ↦ ?_527    rw [← mul_assoc, ← map_mul]528    congr 2529    field_simp530 531/-- `Σ_k ψ_k((q+ε) · Σ_j μ(j) ψ_j(L)/j)/k` equals `Σ_m C_m ψ_m(L)` with532`C_m = availablePoints ε m`. -/533private theorem plethSum_C_mul_moebiusSum (ε : ℤ) (L : Ser) :534    plethSum (PowerSeries.C (scalar (RatFunc.X + (ε : RatFunc ℚ))) * moebiusSum L) =535        countSum ε L := by536  ext n : 1537  simp only [plethSum, moebiusSum, countSum, PowerSeries.coeff_mk, PowerSeries.coeff_C_mul,538    Finset.mul_sum, map_sum, Finset.smul_sum]539  have h1 : ∀ k ∈ n.divisors, ∀ j ∈ (n / k).divisors,540      (k : ℚ)⁻¹ • adamsCoef k (scalar (RatFunc.X + (ε : RatFunc ℚ)) *541        ((((ArithmeticFunction.moebius j : ℤ) : ℚ)) / (j : ℚ)) •542            adamsCoef j (PowerSeries.coeff (n / k / j) L))543        = (fun (k j : ℕ) ↦ scalar (RatFunc.C ((k : ℚ)⁻¹ *544            (((ArithmeticFunction.moebius j : ℤ) : ℚ) / (j : ℚ))) *545            ((RatFunc.X : RatFunc ℚ) ^ k + (ε : RatFunc ℚ))) *546            adamsCoef (k * j) (PowerSeries.coeff (n / (k * j)) L)) k j := by547    intro k hk j hj548    have hk0 : 0 < k := Nat.pos_of_mem_divisors hk549    have hj0 : 0 < j := Nat.pos_of_mem_divisors hj550    rw [mul_smul_comm, map_rat_smul, map_mul, adamsCoef_adamsCoef k j hk0 hj0,551        Nat.div_div_eq_div_mul,552      adamsCoef_scalar k, adamsRat_X_add_int k hk0, smul_smul, rat_smul_eq_scalar_mul, ← mul_assoc,553      ← scalar_mul]554  rw [Finset.sum_congr rfl fun k hk ↦ Finset.sum_congr rfl (h1 k hk),555    sum_divisors_sum_divisors_div]556  refine Finset.sum_congr rfl fun m hm ↦ ?_557  have hm0 : 0 < m := Nat.pos_of_mem_divisors hm558  have h2 : ∀ k ∈ m.divisors, k * (m / k) = m := fun k hk ↦559      Nat.mul_div_cancel' (Nat.dvd_of_mem_divisors hk)560  rw [Finset.sum_congr rfl fun k hk ↦ by561      rw [h2 k hk], ← Finset.sum_mul, ← availablePoints_rational_eq_sum ε m hm0]562  simp only [scalar_eq_algebraMap, ← map_sum, Algebra.smul_def]563 564/-- The law of a crossing state is symmetric under exchanging the two branches:565`F_{T(a,b;c,h)} = F_{T(b,a;h,c)}`. -/566private theorem lawCoef_stateLaw_crossing_comm (a b c h : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)567    (hh : 0 < h) :568    lawCoef (stateLaw (State.crossing a b c h)) = lawCoef (stateLaw (State.crossing b a h c)) := by569  have h1 := (state_law_unfold (.crossing a b c h) ⟨ha, hb, hc, hh⟩ rfl).2 a b c h rfl570  have h2 := (state_law_unfold (.crossing b a h c) ⟨hb, ha, hh, hc⟩ rfl).2 b a h c rfl571  rw [h1, h2, lawCoef_exitLaw_crossing a b c h ha hb hc hh,572    lawCoef_exitLaw_crossing b a h c hb ha hh hc, Nat.min_comm h c]573  refine Finset.sum_congr rfl fun d _ ↦ ?_574  conv_rhs => rw [Finset.sum_comm]575  refine Finset.sum_congr rfl fun rt _ ↦ Finset.sum_congr rfl fun rx _ ↦ ?_576  have hp : (divisorProbability (State.crossing b a h c) d).rational577      = (divisorProbability (State.crossing a b c h) d).rational := by578    rw [rational_divisorProbability_crossing b a h c d,579      rational_divisorProbability_crossing a b c h d,580      Nat.add_comm (if d < h then 1 else 0)]581  rw [hp, Nat.add_comm b a, Nat.add_comm (b * h) (a * c), Nat.sub_right_comm d rx rt]582  by_cases hc1 : ((0 < rt ↔ d < c) ∧ (0 < rx ↔ d < h) ∧ rt + rx ≤ d)583  · have hc2 : ((0 < rx ↔ d < h) ∧ (0 < rt ↔ d < c) ∧ rx + rt ≤ d) := by584      obtain ⟨x, y, z⟩ := hc1; exact ⟨y, x, by omega⟩585    rw [if_pos hc1, if_pos hc2, mul_comm (if rx = 0 then _ else _)]586  · have hc2 : ¬ ((0 < rx ↔ d < h) ∧ (0 < rt ↔ d < c) ∧ rx + rt ≤ d) := by587      rintro ⟨y, x, z⟩; exact hc1 ⟨x, y, by omega⟩588    rw [if_neg hc1, if_neg hc2]589 590/-- The contact series `U_{a,b}` has constant term `1`. -/591theorem crossingQ_zero_zero (a b : ℕ) : crossingQ a b 0 0 = 1 := by simp [crossingQ]592 593/-- The contact series `U_{a,b}` vanishes on the axes away from `(0,0)`. -/594private theorem qPositive_crossingQ (a b : ℕ) : QPositive (crossingQ a b) := by595  intro c h h1 h2596  have : ¬ (0 < c ∧ 0 < h) := by omega597  simp [crossingQ, h2, this]598 599/-- The off-axis coefficients of `U_{a,b}` are `(q-1) F_{T(a,b;c,h)}`. -/600private theorem crossingQ_of_pos (a b c h : ℕ) (hc : 0 < c) (hh : 0 < h) :601    crossingQ a b c h = scalar (RatFunc.X - 1) * lawCoef (stateLaw (State.crossing a b c h)) := by602  have : ¬ (c = 0 ∧ h = 0) := by omega603  simp [crossingQ, this, hc, hh]604 605/-- The symmetry `U_{a,b}(c,h) = U_{b,a}(h,c)`. -/606theorem crossingQ_symm (a b c h : ℕ) (ha : 0 < a) (hb : 0 < b) :(H) = (7.4)607    crossingQ a b c h = crossingQ b a h c := by608  by_cases h1 : c = 0 ∧ h = 0609  · obtain ⟨rfl, rfl⟩ := h1610    simp [crossingQ]611  · by_cases h2 : 0 < c ∧ 0 < h612    · rw [crossingQ_of_pos a b c h h2.1 h2.2, crossingQ_of_pos b a h c h2.2 h2.1,613        lawCoef_stateLaw_crossing_comm a b c h ha hb h2.1 h2.2]614    · rw [qPositive_crossingQ a b c h (by omega) h1,615        qPositive_crossingQ b a h c (by omega) (by tauto)]616 617private theorem expSer_sum (s : Finset ℕ) (F : ℕ → Ser)618    (hF : ∀ m ∈ s, PowerSeries.constantCoeff (F m) = 0) :619    expSer (∑ m ∈ s, F m) = ∏ m ∈ s, expSer (F m) := by620  induction s using Finset.induction_on with621  | empty => simpa using expSer_zero622  | insert a s ha ih =>623    rw [Finset.sum_insert ha, Finset.prod_insert ha,624      expSer_add _ _ (hF a (Finset.mem_insert_self _ _)),625          ih (fun m hm ↦ hF m (Finset.mem_insert_of_mem hm))]626    rw [map_sum]627    exact Finset.sum_eq_zero (fun m hm ↦ hF m (Finset.mem_insert_of_mem hm))628 629/-- Through degree `N`, the plethystic power `P_{q+ε}(B)` is the Euler product630`Π_{m=1}^N ψ_m(B)^{C_m}`. -/631private theorem pPow_scongr_prod_formalPow_adamsSer (ε : ℤ) (B : Ser)632    (hB : PowerSeries.constantCoeff B = 1) (N : ℕ) :633    SCongr N (pPow (RatFunc.X + (ε : RatFunc ℚ)) B) (∏ m ∈ Finset.Icc 1 N,634        formalPow (availablePoints ε m).rational (adamsSer m B)) := by635  set L := logSer B with hLdef636  have hL : PowerSeries.constantCoeff L = 0 := (constantCoeff_logSer B hB)637  have hp : pPow (RatFunc.X + (ε : RatFunc ℚ)) B = expSer (countSum ε L) := by638    rw [pPow, pExp, pLog, plethSum_C_mul_moebiusSum]639  set S : Ser := ∑ m ∈ Finset.Icc 1 N,640    PowerSeries.C (scalar (availablePoints ε m).rational) * adamsSer m L with hS641  have hterm : ∀ m ∈ Finset.Icc 1 N, PowerSeries.constantCoeff642      (PowerSeries.C (scalar (availablePoints ε m).rational) * adamsSer m L) = 0 := by643    intro m hm644    have hm0 : m ≠ 0 := by have := (Finset.mem_Icc.1 hm).1; omega645    rw [map_mul, (constantCoeff_adamsSer m hm0 L), hL, map_zero, mul_zero]646  have hS0 : PowerSeries.constantCoeff S = 0 := by647    rw [hS, map_sum]; exact Finset.sum_eq_zero hterm648  have hc0 : PowerSeries.constantCoeff (countSum ε L) = 0 := by649    rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply]; simp [countSum]650  have h1 : SCongr N (countSum ε L) S := by651    intro n hn652    rw [hS, map_sum]653    have hrw : ∀ m ∈ Finset.Icc 1 N, PowerSeries.coeff n654        (PowerSeries.C (scalar (availablePoints ε m).rational) * adamsSer m L) =655        if m ∣ n then (availablePoints ε m).rational • adamsCoef m (PowerSeries.coeff (n / m) L)656            else 0 := by657      intro m hm658      have hm0 : m ≠ 0 := by have := (Finset.mem_Icc.1 hm).1; omega659      rw [PowerSeries.coeff_C_mul, (coeff_adamsSer m hm0 L n), scalar_mul_eq_smul]660      split_ifs <;> simp661    rw [Finset.sum_congr rfl hrw, ← Finset.sum_filter]662    simp only [countSum, PowerSeries.coeff_mk]663    rcases Nat.eq_zero_or_pos n with rfl | hnpos664    · simp only [Nat.divisors_zero, Finset.sum_empty, Nat.zero_div]665      rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply] at hL666      simp [hL]667    · apply Finset.sum_congr _ (fun _ _ ↦ rfl)668      ext m669      simp only [Nat.mem_divisors, Finset.mem_filter, Finset.mem_Icc]670      constructor671      · rintro ⟨hd, hn0⟩672        exact ⟨⟨Nat.pos_of_dvd_of_pos hd hnpos, (Nat.le_of_dvd hnpos hd).trans hn⟩, hd⟩673      · rintro ⟨_, hd⟩674        exact ⟨hd, by omega⟩675  have h2 := (SCongr.expSer hc0 hS0 h1)676  have h3 : expSer S = ∏ m ∈ Finset.Icc 1 N, formalPow (availablePoints ε m).rational677      (adamsSer m B) := by678    rw [hS, expSer_sum _ _ hterm]679    apply Finset.prod_congr rfl680    intro m hm681    have hm0 : m ≠ 0 := by have := (Finset.mem_Icc.1 hm).1; omega682    rw [formalPow, ← (adamsSer_logSer m hm0 B hB)]683  rw [hp, ← h3]; exact h2684 685/-- The `n`-th coefficient of the Euler transform `eulerSer ε a` is that of the finite Euler686product `Π_{m=1}^n ψ_m(B_a)^{C_m}`. -/687private theorem coeff_eulerSer_eq_coeff_prod (ε : ℤ) (a n : ℕ) :688    PowerSeries.coeff n (eulerSer ε a) = PowerSeries.coeff n689        (∏ m ∈ Finset.Icc 1 n, formalPow (availablePoints ε m).rational690        (adamsSer m (clusterSer a))) := by691  have hB : PowerSeries.constantCoeff (clusterSer a) = 1 := by692    rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply]693    simp [clusterSer]694  exact pPow_scongr_prod_formalPow_adamsSer ε (clusterSer a) hB n n le_rfl695 696/-- The `n`-th coefficient of the Euler transform `eulerSer ε a` is the pattern sum697`patternSum ε a n n`. -/698theorem coeff_eulerSer (ε : ℤ) (a n : ℕ) :lem-7.2(G) = (7.9)699    PowerSeries.coeff n (eulerSer ε a) = patternSum ε a n n := by700  rw [coeff_eulerSer_eq_coeff_prod,701    prod_formalPow_adamsSer_clusterSer_scongr ε a n n le_rfl,702    coeff_euler_families_eq_patternSum]703 704private theorem crossing_factorization_term (a b c h d rt rx : ℕ) (ha : 0 < a) (hb : 0 < b)705    (hdc : d ≤ min c h) :706    (if (rt + rx ≤ d ∧ d ≤ min c h) then707      qpow (-(chooseTwo (rx + (d - rt - rx) + rt) : ℤ)) *708        (crossingQ (a + b) b rx (h - (rx + (d - rt - rx) + rt)) *709          (PowerSeries.coeff (d - rt - rx) (eulerSer (-1) (a + b)) *710            crossingQ a (a + b) (c - (rx + (d - rt - rx) + rt)) rt)) else 0)711    = scalar (RatFunc.X - 1) * (if ((0 < rt ↔ d < c) ∧ (0 < rx ↔ d < h) ∧ rt + rx ≤ d) then scalar712        (divisorProbability (State.crossing a b c h) d).rational *713        ((if rt = 0 then 1 else lawCoef (stateLaw (State.crossing (a + b) a rt (c - d)))) *714        (if rx = 0 then 1 else lawCoef (stateLaw (State.crossing (a + b) b rx (h - d)))) *715        patternSum (-1) (a + b) (a * c + b * h) (d - rt - rx)) else 0) := by716  by_cases hsum : rt + rx ≤ d717  swap718  · simp [hsum]719  rw [show rx + (d - rt - rx) + rt = d by omega]720  simp only [hsum, hdc, and_self, if_true, and_true]721  rw [coeff_eulerSer,722    patternSum_eq_of_le (-1) (a + b) (d - rt - rx) (a * c + b * h) (d - rt - rx) le_rfl (by723      have : c ≤ a * c := Nat.le_mul_of_pos_left c ha724      have := min_le_left c h725      omega)]726  set P := patternSum (-1) (a + b) (a * c + b * h) (d - rt - rx)727  by_cases hT : (0 < rt ↔ d < c)728  swap729  · have : crossingQ a (a + b) (c - d) rt = 0 := by730      unfold crossingQ; rw [if_neg (by omega), if_neg (by omega)]731    simp [this, hT]732  by_cases hX : (0 < rx ↔ d < h)733  swap734  · have : crossingQ (a + b) b rx (h - d) = 0 := by735      unfold crossingQ; rw [if_neg (by omega), if_neg (by omega)]736    simp [this, hX]737  simp only [hT, hX, and_self, if_true]738  set Bt := (if rt = 0 then 1 else lawCoef (stateLaw (State.crossing (a + b) a rt (c - d))))739  set Bx := (if rx = 0 then 1 else lawCoef (stateLaw (State.crossing (a + b) b rx (h - d))))740  set i := (if d < c then 1 else 0)741  set k := (if d < h then 1 else 0)742  have eT : crossingQ a (a + b) (c - d) rt = scalar ((RatFunc.X - 1) ^ i) * Bt := by743    by_cases h1 : d < c744    · have hrt : 0 < rt := hT.2 h1745      simp only [i, Bt, crossingQ, if_pos h1, pow_one, if_neg746          (show ¬ (c - d = 0 ∧ rt = 0) by omega),747        if_pos (show 0 < c - d ∧ 0 < rt by omega), if_neg (show ¬ rt = 0 by omega)]748      rw [lawCoef_stateLaw_crossing_comm a (a + b) (c - d) rt ha (by omega) (by omega) hrt]749    · have hrt : rt = 0 := by omega750      simp only [i, Bt, crossingQ, if_neg h1, pow_zero, scalar_one, if_pos hrt, mul_one,751        if_pos (show c - d = 0 ∧ rt = 0 by omega)]752  have eX : crossingQ (a + b) b rx (h - d) = scalar ((RatFunc.X - 1) ^ k) * Bx := by753    by_cases h1 : d < h754    · have hrx : 0 < rx := hX.2 h1755      simp only [k, Bx, crossingQ, if_pos h1, pow_one, if_neg756          (show ¬ (rx = 0 ∧ h - d = 0) by omega),757        if_pos (show 0 < rx ∧ 0 < h - d by omega), if_neg (show ¬ rx = 0 by omega)]758    · have hrx : rx = 0 := by omega759      simp only [k, Bx, crossingQ, if_neg h1, pow_zero, scalar_one, if_pos hrx, mul_one,760        if_pos (show rx = 0 ∧ h - d = 0 by omega)]761  rw [eT, eX, rational_divisorProbability_crossing a b c h d,762    show qpow (-(chooseTwo d : ℤ)) = scalar (((RatFunc.X : RatFunc ℚ) ^ chooseTwo d)⁻¹) by763      rw [qpow, zpow_neg, zpow_natCast]]764  calc scalar ((RatFunc.X ^ chooseTwo d)⁻¹) * (scalar ((RatFunc.X - 1) ^ k) * Bx *765      (P * (scalar ((RatFunc.X - 1) ^ i) * Bt)))766      = scalar ((RatFunc.X ^ chooseTwo d)⁻¹ * ((RatFunc.X - 1) ^ (i + k))) * (Bt * Bx * P) := by767        rw [pow_add, scalar_mul, scalar_mul]; ring768    _ = _ := by769        rw [← X_sub_one_mul_crossingWeight (i + k), ← mul_assoc (scalar (RatFunc.X - 1)),770          ← scalar_mul]771        simp only [mul_assoc]772        congr 2773        ring774 775/-- The `(c,h)` coefficient of `U_{a+b,b}⁺ · J(P_{a+b}) · U_{a,a+b}⁻` (`c > 0`) is `(q-1)` times776the regrouped exit sum of `T(a,b;c,h)`. -/777private theorem qmul_qplus_qdiag_qminus_crossingQ_apply (a b c h : ℕ) (ha : 0 < a) (hb : 0 < b)778    (hc : 0 < c) :779    qmul (qmul (qplus (crossingQ (a + b) b)) (qdiag (eulerSer (-1) (a + b))))780        (qminus (crossingQ a (a + b))) c h = scalar (RatFunc.X - 1) *781        (∑ d ∈ Finset.Icc 1 (min c h), ∑ rt ∈ Finset.range (d + 1), ∑ rx ∈ Finset.range (d + 1),782        (if ((0 < rt ↔ d < c) ∧ (0 < rx ↔ d < h) ∧ rt + rx ≤ d) then scalar783        (divisorProbability (State.crossing a b c h) d).rational *784        ((if rt = 0 then 1 else lawCoef (stateLaw (State.crossing (a + b) a rt (c - d)))) *785        (if rx = 0 then 1 else lawCoef (stateLaw (State.crossing (a + b) b rx (h - d)))) *786        patternSum (-1) (a + b) (a * c + b * h) (d - rt - rx)) else 0)) := by787  rw [qmul_qplus_qdiag_qminus_apply]788  set G : ℕ → ℕ → ℕ → Coef := fun rx m rt ↦789    qpow (-(chooseTwo (rx + m + rt) : ℤ)) *790        (crossingQ (a + b) b rx (h - (rx + m + rt)) *791          (PowerSeries.coeff m (eulerSer (-1) (a + b)) *792            crossingQ a (a + b) (c - (rx + m + rt)) rt)) with hG793  have step1 : ∀ rx m rt : ℕ, (if (rx + m + rt ≤ c ∧ rx + m + rt ≤ h) then qpow794      (-(chooseTwo rx : ℤ) - (chooseTwo m : ℤ) - (chooseTwo rt : ℤ) - (rx : ℤ) *795      (m : ℤ) - ((rx : ℤ) + (m : ℤ)) * (rt : ℤ)) * (crossingQ (a + b) b rx (h - (rx + m + rt)) *796      (PowerSeries.coeff m (eulerSer (-1) (a + b)) * crossingQ a (a + b) (c - (rx + m + rt)) rt))797      else 0)798      = if rx + m + rt ≤ min c h then G rx m rt else 0 := by799    intro rx m rt800    have e : (chooseTwo rx : ℤ) + chooseTwo m + chooseTwo rt + rx * m + rx * rt + m * rt =801        ((chooseTwo (rx + m + rt) : ℕ) : ℤ) := by802      rw [chooseTwo_add, chooseTwo_add]; push_cast; ring803    rw [hG]804    simp only [le_min_iff]805    split_ifs806    · congr 2807      rw [← e]; ring808    · rfl809  simp only [step1]810  rw [sum_triple_reindex c (min c h) (min_le_left _ _) G, Finset.mul_sum]811  symm812  have hsub : Finset.Icc 1 (min c h) ⊆ Finset.range (c + 1) := fun d hd ↦ by813    simp only [Finset.mem_Icc, Finset.mem_range] at hd ⊢; omega814  have hzero : ∀ d ∈ Finset.range (c + 1), d ∉ Finset.Icc 1 (min c h) →815      (∑ rt ∈ Finset.range (d + 1), ∑ rx ∈ Finset.range (d + 1), if rt + rx ≤ d ∧ d ≤816          min c h then G rx (d - rt - rx) rt else 0) = 0 := by817    intro d hd hnot818    simp only [Finset.mem_Icc, not_and_or, not_le] at hnot819    refine Finset.sum_eq_zero fun rt hrt ↦ Finset.sum_eq_zero fun rx hrx ↦ ?_820    rcases hnot with h0 | h1821    · obtain rfl : d = 0 := by omega822      simp only [Finset.mem_range] at hrt hrx823      obtain ⟨rfl, rfl⟩ : rt = 0 ∧ rx = 0 := by omega824      have hz : crossingQ a (a + b) c 0 = 0 := qPositive_crossingQ _ _ c 0 (Or.inr rfl) (by omega)825      simp [hG, hz]826    · exact if_neg (by omega)827  rw [← Finset.sum_subset hsub hzero]828  refine Finset.sum_congr rfl fun d hd ↦ ?_829  simp only [Finset.mul_sum]830  exact Finset.sum_congr rfl fun rt _ ↦ Finset.sum_congr rfl fun rx _ ↦831    (crossing_factorization_term a b c h d rt rx ha hb (Finset.mem_Icc.1 hd).2).symm832 833/-- **Crossing factorization.** `U_{a,b} = U_{a+b,b}⁺ · J(P_{a+b}) · U_{a,a+b}⁻`, where `J` is the834diagonal substitution and `P_{a+b} = eulerSer (-1) (a+b)`. -/835theorem crossingQ_eq_qmul_qplus_qdiag_qminus (a b c h : ℕ) (ha : 0 < a) (hb : 0 < b) :(T) = (7.12)Lemma 8.2836    crossingQ a b c h = qmul (qmul (qplus (crossingQ (a + b) b)) (qdiag (eulerSer (-1) (a + b))))837        (qminus (crossingQ a (a + b))) c h := by838  have Q2 : QPositive (qmul (qplus (crossingQ (a + b) b)) (qdiag (eulerSer (-1) (a + b)))) :=839    (qPositive_crossingQ _ _).qplus.qmul (qPositive_qdiag _)840  by_cases h00 : c = 0 ∧ h = 0841  · obtain ⟨rfl, rfl⟩ := h00842    rw [qmul_zero_zero, qmul_zero_zero, crossingQ_zero_zero]843    simp [qplus, qminus, qdiag, chooseTwo, crossingQ_zero_zero, qpow_zero, coeff_zero_eulerSer]844  · by_cases hp : 0 < c ∧ 0 < h845    · rw [qmul_qplus_qdiag_qminus_crossingQ_apply a b c h ha hb hp.1,846        ← lawCoef_exitLaw_crossing a b c h ha hb hp.1 hp.2,847        ← (state_law_unfold (.crossing a b c h) ⟨ha, hb, hp.1, hp.2⟩ rfl).2 a b c h rfl,848        crossingQ_of_pos a b c h hp.1 hp.2]849    · have z : c = 0 ∨ h = 0 := by omega850      rw [Q2.qmul (qPositive_crossingQ _ _).qminus c h z h00, qPositive_crossingQ a b c h z h00]851 852/-- If `G_b ≡ S(B_bᵛ)` through degree `M` for all `b > 0`, then `U_{a,b}` is unitary,853`U_{a,b} U_{a,b}† ≡ 1`, through total contact degree `2M + 1`. -/854theorem qcongr_crossingQ_mul_qdagger (M : ℕ) (hS : ∀ a : ℕ, 0 < a →Lemma 8.3Theorem 9.3855    SCongr M (eulerSer 0 a) (dilate (recipSer (clusterSer a)))) (j : ℕ) (hj : j ≤ 2 * M + 1)856    (a b : ℕ) (ha : 0 < a) (hb : 0 < b) :857    QCongr j (qmul (crossingQ a b) (qdagger (crossingQ a b))) qone := by858  have refl : ∀ (k : ℕ) (U : QSer), QCongr k U U := fun k U c h _ ↦ rfl859  have posUU : ∀ x y : ℕ, QPositive (qmul (crossingQ x y) (qdagger (crossingQ x y))) :=860    fun x y ↦ (qPositive_crossingQ x y).qmul (qPositive_crossingQ x y).qdagger861  induction j generalizing a b with862  | zero =>863    intro c h hc864    obtain ⟨rfl, rfl⟩ : c = 0 ∧ h = 0 := by omega865    rw [qmul_zero_zero]866    simp [qdagger, qone, crossingQ_zero_zero, qpow_zero]867  | succ j ih =>868    have hj' : j ≤ 2 * M + 1 := by omega869    set s := a + b with hs870    have hs0 : 0 < s := by omega871    set A := crossingQ s b872    set D := qdiag (eulerSer (-1) s)873    set Cq := crossingQ a s874    have hfac : crossingQ a b = qmul (qmul (qplus A) D) (qminus Cq) := by875      funext c h; exact crossingQ_eq_qmul_qplus_qdiag_qminus a b c h ha hb876    have hdag : qdagger (crossingQ a b) =877        qmul (qminus (qdagger Cq)) (qmul (qdagger D) (qplus (qdagger A))) := by878      rw [hfac, qdagger_qmul, qdagger_qmul, qdagger_qplus, qdagger_qminus]879    rw [hdag, hfac]880    -- rearrange881    have e1 : qmul (qmul (qmul (qplus A) D) (qminus Cq))882        (qmul (qminus (qdagger Cq)) (qmul (qdagger D) (qplus (qdagger A)))) =883        qmul (qmul (qplus A) D) (qmul (qminus (qmul Cq (qdagger Cq)))884          (qmul (qdagger D) (qplus (qdagger A)))) := by885      rw [qminus_qmul, qmul_assoc, ← qmul_assoc (qminus Cq)]886    rw [e1]887    have hC : QCongr (j + 1) (qminus (qmul Cq (qdagger Cq))) qone :=888      qcongr_qminus_qone (j + 1) _ (posUU a s) (by simpa using ih hj' a s ha hs0)889    have hA : QCongr (j + 1) (qplus (qmul A (qdagger A))) qone :=890      qcongr_qplus_qone (j + 1) _ (posUU s b) (by simpa using ih hj' s b hs0 hb)891    have hD : QCongr (j + 1) (qmul D (qdagger D)) qone :=892      (qcongr_qdiag_mul_qdagger M s893        (dilate_recipSer_eulerSer_mul_scongr_one M s hs0 hS)).mono (by omega)894    refine ((refl _ _).qmul (hC.qmul (refl _ _))).trans ?_895    rw [qone_qmul, qmul_assoc, ← qmul_assoc D]896    refine ((refl _ _).qmul (hD.qmul (refl _ _))).trans ?_897    rw [qone_qmul, ← qplus_qmul]898    exact hA899 900/-- The degree-one coefficient of `G_a = eulerSer 0 a` is `q Z_{a,1}`. -/901theorem coeff_one_eulerSer_zero (a : ℕ) :902    PowerSeries.coeff 1 (eulerSer 0 a) = qpow 1 * AddMonoidAlgebra.single ({(a, 1)} : FactorType)903        1 := by904  rw [coeff_eulerSer]905  let m1 : Pattern 1 := fun _ ↦ 1906  have hf : (Finset.univ : Finset (Pattern 1)).filter (fun m ↦ patternWeight m = 1) = {m1} := by907    ext m908    have key : patternWeight m = (m (0,0)).val := by909      simp [patternWeight, Fintype.sum_prod_type]910    rw [Finset.mem_filter, Finset.mem_singleton, key]911    simp only [Finset.mem_univ, true_and]912    constructor913    · intro h914      funext ij915      have : ij = (0,0) := Subsingleton.elim _ _916      subst this917      apply Fin.ext918      simpa [m1] using h919    · intro h; subst h; rfl920  unfold patternSum921  rw [hf, Finset.sum_singleton]922  have hc : lawCoef (stateLaw (State.single a 1)) =923      AddMonoidAlgebra.single ({(a, 1)} : FactorType) 1 :=924    (coeff_succ_clusterSer a 0).symm.trans (coeff_one_clusterSer a)925  have hP : (∏ ij : Fin 1 × Fin 1,926      (adamsCoef (ij.1.val + 1) (lawCoef (stateLaw (State.single a (ij.2.val + 1))))) ^ (m1 ij).val)927      = AddMonoidAlgebra.single ({(a, 1)} : FactorType) 1 := by928    simp [m1, hc, adamsCoef_one]929  have hD : (divisorCount 0 m1).rational = RatFunc.X := by930    rw [rational_divisorCount]931    simp [m1, rational_availablePoints]932  rw [hP, hD, Algebra.smul_def, qpow_one, scalar_eq_algebraMap]933 934/-- Base case of cluster reciprocity: `G_a ≡ S(B_aᵛ)` through degree `1`. -/935theorem cluster_reciprocity_one (a : ℕ) :Proof of monic/cluster reciprocity936    SCongr 1 (eulerSer 0 a) (dilate (recipSer (clusterSer a))) := by937  intro m hm938  interval_cases m939  · rw [coeff_zero_eulerSer, coeff_zero_dilate_recipSer_clusterSer]940  · rw [coeff_one_eulerSer_zero a, coeff_one_dilate_recipSer_clusterSer]941 942/-- The `n`-th coefficient of `ρ(U_{a,a}) Φ(G_a)`, expanded by divisor degree `d` and crossing943depth `r` into crossing laws and pattern sums (plus `1` in degree `0`). -/944theorem coeff_qact_crossingQ_gaussPhi_eulerSer (a n : ℕ) (ha : 0 < a) :(S) = (7.11)945    PowerSeries.coeff n (qact (crossingQ a a) (gaussPhi (eulerSer 0 a))) =946        (∑ d ∈ Finset.Icc 1 n, ∑ r ∈ Finset.range (d + 1),947        (if ((0 < r ↔ d < n) ∧ r ≤ d) then scalar (divisorProbability (State.single a n)948        d).rational * ((if r = 0 then 1 else lawCoef (stateLaw (State.crossing a a r (n - d)))) *949        patternSum 0 a (a * n) (d - r)) else 0)) + (if n = 0 then 1 else 0) := by950  have hG : ∀ d r, d ≤ n → PowerSeries.coeff (d - r) (eulerSer 0 a) =951      patternSum 0 a (a * n) (d - r) := by952    intro d r hd953    rw [coeff_eulerSer]954    apply patternSum_eq_of_le955    · exact le_rfl956    · have := Nat.le_mul_of_pos_left n ha; omega957  rw [coeff_qact_gaussPhi, Finset.sum_range_succ']958  congr 1959  · have hI : Finset.Icc 1 n = Finset.Ico 1 (n + 1) := by960      ext x; simp only [Finset.mem_Icc, Finset.mem_Ico]; omega961    rw [hI, Finset.sum_Ico_eq_sum_range, Nat.add_sub_cancel]962    refine Finset.sum_congr rfl fun d hd ↦ ?_963    rw [Finset.mem_range] at hd964    rw [add_comm 1 d]965    refine Finset.sum_congr rfl fun r hr ↦ ?_966    rw [Finset.mem_range] at hr967    rw [hG _ _ (by omega), rational_divisorProbability_single a n (d+1)]968    simp only [crossingQ, qpow]969    have hX : (RatFunc.X : RatFunc ℚ) ^ (-((tri (d+1) : ℕ) : ℤ)) =970        ((RatFunc.X : RatFunc ℚ) ^ tri (d+1))⁻¹ := by971      rw [zpow_neg, zpow_natCast]972    rw [hX]973    rcases Nat.eq_zero_or_pos r with h0 | h0974    · subst h0975      by_cases hdn : d + 1 < n976      · have : ¬ (n - (d+1) = 0) := by omega977        simp [hdn, this]978      · have : n - (d+1) = 0 := by omega979        simp [hdn, this]980    · by_cases hdn : d + 1 < n981      · have : 0 < n - (d+1) := by omega982        have hr' : r ≤ d + 1 := by omega983        simp only [h0.ne', false_and, if_false, h0, this, hdn, iff_self, hr', and_self, if_true,984            pow_one, scalar_mul]985        ring986      · have : ¬ (0 < n - (d+1)) := by omega987        simp [h0.ne', hdn, this]988  · have ht : tri 0 = 0 := rfl989    simp only [zero_add, Finset.sum_range_one, Nat.sub_self, ht, Nat.cast_zero, neg_zero, qpow_zero,990      one_mul, coeff_zero_eulerSer, mul_one, crossingQ]991    by_cases hn : n = 0 <;> simp [hn]992 993/-- The self-pattern term of the recursion of `S(a;n)` (`n ≥ 2`) is994`q^{-tri n} · q · F_{S(a;n)}`. -/995theorem lawCoef_single_self_term (a n : ℕ) (ha : 0 < a) (hn : 2 ≤ n)(S) = (7.11)996    (P : TangentPattern (State.single a n).degree) (hP : Allowed (State.single a n) P)997    (hself : SelfPattern (State.single a n) P) :998    lawCoef (lawScale (.mul (tangentCount (State.single a n) P)999        (divisorProbability (State.single a n) P.d.val))1000        (lawProd ((children (State.single a n) P).map fun z ↦ lawDescend z.1 (stateLaw z.2)))) =1001        qpow (-(tri n : ℤ)) * (qpow 1 * lawCoef (stateLaw (State.single a n))) := by1002  rw [lawCoef_single_term a n ha (by omega) P hP]1003  obtain ⟨hd, hrt, -, hother⟩ := (selfPattern_single_iff a n ha hn P hP).1 hself1004  have hdeg : (State.single a n).degree = a * n := rfl1005  have hpos : 0 < (State.single a n).degree := by rw [hdeg]; exact Nat.mul_pos ha (by omega)1006  have hn1 : n - 1 < (State.single a n).degree := by1007    rw [hdeg]; have := Nat.le_mul_of_pos_left n ha; omega1008  have hprob : (divisorProbability (State.single a n) P.d.val).rational1009      = ((RatFunc.X : RatFunc ℚ) ^ tri n)⁻¹ := by1010    rw [hd, rational_divisorProbability_single a n n]; simp1011  have hf : ∀ b, (∏ j : Fin (State.single a n).degree,1012      ((Nat.factorial (P.other (b, j)).val : ℕ) : ℚ)) = 1 := fun b ↦1013    Finset.prod_eq_one fun j _ ↦ by rw [hother]; split_ifs <;> simp1014  have hcount : (divisorCount 0 P.other).rational = (RatFunc.X : RatFunc ℚ) := by1015    rw [rational_divisorCount, Finset.prod_eq_single (⟨0, hpos⟩ : Fin (State.single a n).degree)]1016    · rw [Finset.sum_eq_single (⟨n - 1, hn1⟩ : Fin (State.single a n).degree), hf]1017      · simp [hother, rational_availablePoints]1018      · intro b _ hb1019        simp [hother, show b.val ≠ n - 1 from fun h ↦ hb (Fin.ext h)]1020      · simp1021    · intro b _ hb1022      rw [Finset.sum_eq_zero fun j _ ↦ by1023        simp [hother, show b.val ≠ 0 from fun h ↦ hb (Fin.ext h)], hf]1024      simp1025    · simp1026  have hprod : (∏ ij : Fin (State.single a n).degree × Fin (State.single a n).degree,1027      (adamsCoef (ij.1.val + 1) (lawCoef (stateLaw (State.single a (ij.2.val + 1))))) ^1028          (P.other ij).val)1029      = lawCoef (stateLaw (State.single a n)) := by1030    rw [Finset.prod_eq_single ((⟨0, hpos⟩, ⟨n - 1, hn1⟩) : Fin (State.single a n).degree × Fin1031        (State.single a n).degree)]1032    · rw [hother]1033      simp only [and_self, if_true, pow_one]1034      rw [show n - 1 + 1 = n by omega, adamsCoef_one]1035    · intro b _ hb1036      rw [hother, if_neg, pow_zero]1037      rintro ⟨h1, h2⟩1038      exact hb (Prod.ext (Fin.ext h1) (Fin.ext h2))1039    · simp1040  rw [hprod, hprob, hcount, if_pos hrt, one_mul, scalar_mul, ← qpow_one,1041    show qpow (-(tri n : ℤ)) = scalar (((RatFunc.X : RatFunc ℚ) ^ tri n)⁻¹) by1042      rw [qpow, zpow_neg, zpow_natCast]]1043  ring1044 1045end SurfaceBlowup