Plethystic calculus for the reciprocity law

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Formula.StateCombinatorics7import SurfaceBlowup.Reciprocity.Quantum8 9/-!10# Plethystic calculus for the reciprocity law11 12Formal-power-series tools over the coefficient ring `Coef = ℚ(q)[Z_{e,f}]` used in the proof of13the reciprocity law: truncated congruences, `exp`/`log` and formal powers, the plethystic14exponential, logarithm and powers `P_w`, multinomial expansions of Euler products into pattern15sums, the combinatorics of the tangent patterns of single-boundary states `S(a;n)`, and the16well-formedness and rational-function calculus of the weight expressions.17 18## Main results19 20* `eq_of_mul_derivative_eq_mul`: uniqueness for the ODE `g E' = w E`.21* `expSer_add`, `expSer_logSer`, `logSer_expSer`, `coeff_formalPow`: `exp`, `log` and powers.22* `pPow_pPow`, `pPow_mul_pPow`, `coeff_pPow_sub_of_scongr`: plethystic powers.23* `prod_formalPow_adamsSer_clusterSer_scongr`, `coeff_euler_families_eq_patternSum`: Euler24  products as pattern sums.25* `exists_unique_selfPattern_single`: the unique self pattern of `S(a;n)`.26* `Expr.rational_add`, `Expr.rational_sum`, `lawCoef_lawScale`, `lawCoef_lawProd`: the expression27  and law calculus.28* `clusterSer_eq_pPow`, `dilate_recipSer_eulerSer_mul_scongr_one`.29 30Provenance: `Thm_SurfaceBlowupV2_recip_{scongr_pleth, scongr_pleth_lead, ser_ode_unique,31expSer_add, expSer_logSer, logSer_mul, formalPow_basic, formalPow_coeff, formalPow_adams_series,32euler_product_families, pExp_add, pExp_pLog, pPow_comp, scongr_pPow, single_pattern_reindex,33single_self_pattern, single_self_pattern_unique, sum_triple_reindex, weights_wf,34wf_fraction_ne_zero, rational_hom, lawCoef_append_scale, clusterSer_coeff, central_inverse,35lawCoef_mul_prod, power_identities, rational_sum_prod, divisorCount_rational,36families_to_pattern, lawCoef_coeff, lawWf_safe, safe_wf}`.37-/38 39namespace SurfaceBlowup40 41/-- Truncated agreement `f ≡ g mod x^{n+1}` is preserved by `plethSum = Σ ψ_k/k`. -/42theorem SCongr.plethSum {n : ℕ} {f g : Ser} (h : SCongr n f g) :43    SCongr n (SurfaceBlowup.plethSum f) (SurfaceBlowup.plethSum g) := fun m hm ↦ by44  simp only [SurfaceBlowup.plethSum, PowerSeries.coeff_mk,45    fun k ↦ h (m / k) ((Nat.div_le_self m k).trans hm)]46 47/-- Truncated agreement `f ≡ g mod x^{n+1}` is preserved by `moebiusSum = Σ μ(k) ψ_k/k`. -/48theorem SCongr.moebiusSum {n : ℕ} {f g : Ser} (h : SCongr n f g) :49    SCongr n (SurfaceBlowup.moebiusSum f) (SurfaceBlowup.moebiusSum g) := fun m hm ↦ by50  simp only [SurfaceBlowup.moebiusSum, PowerSeries.coeff_mk,51    fun k ↦ h (m / k) ((Nat.div_le_self m k).trans hm)]52 53/-- A divisor sum `Σ_{k ∣ n} w_k ψ_k(f_{n/k})` with `w_1 = 1` sees only the top coefficient of `f`54modulo agreement in lower degrees. -/55private theorem divisorSum_sub_of_scongr (n : ℕ) (hn : 0 < n) (f g : Ser)56    (h : SCongr (n - 1) f g) (w : ℕ → ℚ) (hw : w 1 = 1) :57    (∑ k ∈ n.divisors, w k • adamsCoef k (PowerSeries.coeff (n / k) f)) -58      (∑ k ∈ n.divisors, w k • adamsCoef k (PowerSeries.coeff (n / k) g)) =59      PowerSeries.coeff n f - PowerSeries.coeff n g := by60  rw [← Finset.sum_sub_distrib, Finset.sum_eq_single 1]61  · rw [Nat.div_one, hw, one_smul, one_smul, adamsCoef_one, adamsCoef_one]62  · intro k hk hk163    have := Nat.div_lt_self hn (by have := Nat.pos_of_mem_divisors hk; omega : 1 < k)64    rw [h _ (by omega), sub_self]65  · exact fun h1 ↦ absurd (Nat.one_mem_divisors.2 hn.ne') h166 67/-- If `f ≡ g` below degree `n`, then the degree-`n` coefficients of `Σ ψ_k f/k` and68`Σ ψ_k g/k` differ exactly as those of `f` and `g`. -/69private theorem coeff_plethSum_sub_of_scongr (n : ℕ) (hn : 0 < n) (f g : Ser)70    (h : SCongr (n - 1) f g) :71    PowerSeries.coeff n (plethSum f) - PowerSeries.coeff n (plethSum g) =72      PowerSeries.coeff n f - PowerSeries.coeff n g := by73  simp only [plethSum, PowerSeries.coeff_mk]74  exact divisorSum_sub_of_scongr n hn f g h (fun k ↦ ((k : ℚ)⁻¹)) (by simp)75 76/-- If `f ≡ g` below degree `n`, then the degree-`n` coefficients of `Σ μ(k) ψ_k f/k` and77`Σ μ(k) ψ_k g/k` differ exactly as those of `f` and `g`. -/78private theorem coeff_moebiusSum_sub_of_scongr (n : ℕ) (hn : 0 < n) (f g : Ser)79    (h : SCongr (n - 1) f g) :80    PowerSeries.coeff n (moebiusSum f) - PowerSeries.coeff n (moebiusSum g) =81      PowerSeries.coeff n f - PowerSeries.coeff n g := by82  simp only [moebiusSum, PowerSeries.coeff_mk]83  exact divisorSum_sub_of_scongr n hn f g h84    (fun k ↦ (((ArithmeticFunction.moebius k : ℤ) : ℚ)) / (k : ℚ)) (by simp)85 86/-- Uniqueness for the linear ODE `g E' = w E` with `g(0) = 1`: a solution is determined by its87constant term. -/88theorem eq_of_mul_derivative_eq_mul (g w E F : Ser) (hg : PowerSeries.constantCoeff g = 1)89    (hE : g * PowerSeries.derivative Coef E = w * E)90    (hF : g * PowerSeries.derivative Coef F = w * F)91    (h0 : PowerSeries.constantCoeff E = PowerSeries.constantCoeff F) :92    E = F := by93  have := IsAddTorsionFree.of_module_rat (M := Coef)94  set D : Ser := E - F with hDdef95  have hD : g * PowerSeries.derivative Coef D = w * D := by96    simp only [hDdef, map_sub, mul_sub, hE, hF]97  have key : ∀ n, ∀ m ≤ n, PowerSeries.coeff m D = 0 := by98    intro n99    induction n with100    | zero =>101      intro m hm102      rw [Nat.le_zero.mp hm, PowerSeries.coeff_zero_eq_constantCoeff_apply, hDdef, map_sub, h0,103        sub_self]104    | succ n ih =>105      intro m hm106      rcases Nat.lt_or_eq_of_le hm with hm | rfl107      · exact ih m (by omega)108      have hc := congrArg (PowerSeries.coeff n) hD109      rw [PowerSeries.coeff_mul, PowerSeries.coeff_mul] at hc110      have hR : ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n,111          PowerSeries.coeff p.1 w * PowerSeries.coeff p.2 D = 0 :=112        Finset.sum_eq_zero fun p hp ↦ by113          rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp114          rw [ih p.2 (by omega), mul_zero]115      have hmem : ((0 : ℕ), n) ∈ Finset.HasAntidiagonal.antidiagonal n := by simp116      rw [hR, ← Finset.add_sum_erase _ _ hmem] at hc117      have hL : ∑ p ∈ (Finset.HasAntidiagonal.antidiagonal n).erase (0, n),118          PowerSeries.coeff p.1 g * PowerSeries.coeff p.2 (PowerSeries.derivative Coef D) = 0 :=119        Finset.sum_eq_zero fun p hp ↦ by120          rw [Finset.mem_erase, Finset.HasAntidiagonal.mem_antidiagonal] at hp121          have : p.1 ≠ 0 := fun h0' ↦ hp.1 (by ext <;> simp <;> omega)122          rw [PowerSeries.coeff_derivative, ih (p.2 + 1) (by omega), zero_mul, mul_zero]123      rw [hL, add_zero, PowerSeries.coeff_derivative, PowerSeries.coeff_zero_eq_constantCoeff_apply,124        hg, one_mul] at hc125      refine nsmul_right_injective (Nat.succ_ne_zero n) (?_ : (n + 1) • _ = (n + 1) • (0 : Coef))126      rw [nsmul_eq_mul, smul_zero, mul_comm]127      push_cast128      exact hc129  exact sub_eq_zero.mp (show D = 0 from PowerSeries.ext fun n ↦ by simpa using key n n le_rfl)130 131/-- The exponential is additive-to-multiplicative on series with zero constant term. -/132theorem expSer_add (f g : Ser) (hf : PowerSeries.constantCoeff f = 0)133    (hg : PowerSeries.constantCoeff g = 0) :134    expSer (f + g) = expSer f * expSer g := by135  have hfg : PowerSeries.constantCoeff (f + g) = 0 := by rw [map_add, hf, hg, add_zero]136  apply eq_of_mul_derivative_eq_mul 1 (PowerSeries.derivative Coef (f + g)) _ _137    PowerSeries.constantCoeff_one138  · rw [one_mul, derivative_expSer _ hfg]139  · rw [one_mul, Derivation.leibniz, derivative_expSer f hf, derivative_expSer g hg, map_add]140    simp only [smul_eq_mul]141    ring142  · rw [constantCoeff_expSer _ hfg, map_mul, constantCoeff_expSer f hf, constantCoeff_expSer g hg,143      mul_one]144 145/-- `exp ∘ log = id` on series with constant term `1`. -/146theorem expSer_logSer (g : Ser) (hg : PowerSeries.constantCoeff g = 1) : expSer (logSer g) = g := by(7.6)147  have hL0 := constantCoeff_logSer g hg148  apply eq_of_mul_derivative_eq_mul g (PowerSeries.derivative Coef g) _ _ hg149  · rw [derivative_expSer _ hL0, ← mul_assoc, mul_derivative_logSer g hg]150  · exact mul_comm _ _151  · rw [constantCoeff_expSer _ hL0, hg]152 153/-- `log ∘ exp = id` on series with constant term `0`. -/154theorem logSer_expSer (f : Ser) (hf : PowerSeries.constantCoeff f = 0) : logSer (expSer f) = f := by(7.6)155  have hE0 := constantCoeff_expSer f hf156  have hu : IsUnit (expSer f) := by157    rw [PowerSeries.isUnit_iff_constantCoeff, hE0]; exact isUnit_one158  have hd : PowerSeries.derivative Coef (logSer (expSer f)) = PowerSeries.derivative Coef f :=159    hu.mul_left_cancel (by rw [mul_derivative_logSer _ hE0, derivative_expSer f hf, mul_comm])160  have := IsAddTorsionFree.of_module_rat (M := Coef)161  exact PowerSeries.derivative.ext hd (by rw [constantCoeff_logSer _ hE0, hf])162 163/-- The formal power `g^c = exp(c log g)` has constant term `1` (for `g(0) = 1`). -/164private theorem constantCoeff_formalPow (c : RatFunc ℚ) (g : Ser)165    (hg : PowerSeries.constantCoeff g = 1) :166    PowerSeries.constantCoeff (formalPow c g) = 1 :=167  constantCoeff_expSer _ (by rw [map_mul, PowerSeries.constantCoeff_C, constantCoeff_logSer g hg,168    mul_zero])169 170/-- The formal power solves the ODE `g (g^c)' = c g' g^c` (for `g(0) = 1`). -/171private theorem mul_derivative_formalPow (c : RatFunc ℚ) (g : Ser)172    (hg : PowerSeries.constantCoeff g = 1) :173    g * PowerSeries.derivative Coef (formalPow c g) =174      PowerSeries.C (scalar c) * PowerSeries.derivative Coef g * formalPow c g := by175  have hl : PowerSeries.derivative Coef (PowerSeries.C (scalar c) * logSer g) =176      PowerSeries.C (scalar c) * PowerSeries.derivative Coef (logSer g) := by177    rw [Derivation.leibniz, PowerSeries.derivative_C]; simp178  rw [formalPow, derivative_expSer _ (by rw [map_mul, PowerSeries.constantCoeff_C,179    constantCoeff_logSer g hg, mul_zero]), hl, ← mul_derivative_logSer g hg]180  ring181 182/-- Binomial expansion of the formal power: the `n`-th coefficient of `g^c` is183`Σ_{k ≤ n} (1/k!) c(c-1)⋯(c-k+1) [xⁿ](g-1)^k`. -/184theorem coeff_formalPow (c : RatFunc ℚ) (g : Ser) (hg : PowerSeries.constantCoeff g = 1)185    (n : ℕ) :186    PowerSeries.coeff n (formalPow c g) = ∑ k ∈ Finset.range (n + 1), ((k.factorial : ℚ)⁻¹) •187      ((∏ j ∈ Finset.range k, (scalar c - (j : ℚ) • (1 : Coef))) *188        PowerSeries.coeff n ((g - 1) ^ k)) := by189  set B : Ser := PowerSeries.mk fun n ↦190    ((n.factorial : ℚ)⁻¹) • ∏ j ∈ Finset.range n, (scalar c - (j : ℚ) • (1 : Coef)) with hB191  set y : Ser := g - 1 with hy_def192  have hy0 : PowerSeries.constantCoeff y = 0 := by simp [y, hg]193  have hy : PowerSeries.HasSubst y := PowerSeries.HasSubst.of_constantCoeff_zero' hy0194  have hODE := binomial_series_ode c195  rw [← hB] at hODE196  have hEq : B.subst y = formalPow c g := by197    refine eq_of_mul_derivative_eq_mul g (PowerSeries.C (scalar c) * PowerSeries.derivative Coef g)198      _ _ hg ?_ (mul_derivative_formalPow c g hg) ?_199    · have hs := congrArg (fun f : Ser ↦ f.subst y) hODE200      rw [PowerSeries.subst_mul hy, PowerSeries.subst_mul hy, PowerSeries.subst_add hy,201        PowerSeries.subst_X hy] at hs202      have hone : (1 : Ser).subst y = 1 := by203        simpa using (PowerSeries.subst_C (a := y) (1 : Coef))204      have hC : (PowerSeries.C (scalar c)).subst y = PowerSeries.C (scalar c) :=205        PowerSeries.subst_C _206      rw [hone, hC, show (1 : Ser) + y = g by simp [y]] at hs207      rw [PowerSeries.derivative_subst hy, show PowerSeries.derivative Coef y =208        PowerSeries.derivative Coef g by simp [y], ← mul_assoc, hs]209      ring210    · rw [constantCoeff_formalPow c g hg, ← PowerSeries.coeff_zero_eq_constantCoeff_apply,211        coeff_subst_eq_sum 0 B y hy0]212      simp [B]213  rw [← hEq, coeff_subst_eq_sum n B y hy0]214  refine Finset.sum_congr rfl fun k _ ↦ ?_215  simp only [B, PowerSeries.coeff_mk, y]216  rw [smul_eq_mul, smul_mul_assoc]217 218/-- For `κ` with total `k`, `(k!)⁻¹ · multinomial(κ) = (Π_r κ_r!)⁻¹`. -/219private theorem inv_factorial_mul_multinomial {n k : ℕ} (κ : Fin n → ℕ) (hk : ∑ r, κ r = k) :220    ((k.factorial : ℚ))⁻¹ * (Nat.multinomial Finset.univ κ : ℚ) =221      (∏ r : Fin n, ((Nat.factorial (κ r) : ℕ) : ℚ))⁻¹ := by222  have hspec := Nat.multinomial_spec Finset.univ κ223  rw [hk] at hspec224  have hpos : (∏ r : Fin n, ((Nat.factorial (κ r) : ℕ) : ℚ)) ≠ 0 :=225    Finset.prod_ne_zero_iff.mpr (fun r _ ↦ by exact_mod_cast Nat.factorial_ne_zero _)226  have hk0 : ((k.factorial : ℚ)) ≠ 0 := by exact_mod_cast Nat.factorial_ne_zero _227  rw [← hspec] at hk0 ⊢228  push_cast at hk0 ⊢229  have hmn : (Nat.multinomial Finset.univ κ : ℚ) ≠ 0 := right_ne_zero_of_mul hk0230  field_simp231 232/-- A sum over all `κ : Fin n → ℕ` of total `≤ n`, grouped by the total, equals the sum over233`Fin (n + 1)`-valued vectors, provided the summand vanishes on vectors of total `> n`. -/234private theorem sum_range_sum_piAntidiag_eq_sum_fin {M : Type*} [AddCommMonoid M] (n : ℕ)235    (F : (Fin n → ℕ) → M) (hF : ∀ κ, n < ∑ r, κ r → F κ = 0) :236    ∑ k ∈ Finset.range (n + 1), ∑ κ ∈ Finset.piAntidiag (Finset.univ : Finset (Fin n)) k, F κ =237      ∑ κ : Fin n → Fin (n + 1), F (fun r ↦ (κ r).val) := by238  set E : Finset (Fin n → ℕ) := Fintype.piFinset (fun _ ↦ Finset.range (n + 1)) with hE239  set D : Finset (Fin n → ℕ) := E.filter (fun κ ↦ ∑ r, κ r ≤ n) with hD240  -- merge into the sum over `D`241  have h3 : ∑ k ∈ Finset.range (n + 1), ∑ κ ∈ Finset.piAntidiag (Finset.univ : Finset (Fin n)) k,242      F κ = ∑ κ ∈ D, F κ := by243    rw [← Finset.sum_fiberwise_of_maps_to (s := D) (t := Finset.range (n + 1))244        (g := fun κ ↦ ∑ r, κ r)]245    · refine Finset.sum_congr rfl (fun k hk ↦ ?_)246      rw [Finset.mem_range] at hk247      congr 1248      ext κ249      simp only [hD, hE, Finset.mem_filter, Fintype.mem_piFinset, Finset.mem_range,250          Finset.mem_piAntidiag, Finset.mem_univ, implies_true, and_true]251      constructor252      · intro h253        have h' : ∑ r, κ r = k := h254        refine ⟨⟨fun r ↦ ?_, by omega⟩, h⟩255        have : κ r ≤ ∑ r, κ r :=256          Finset.single_le_sum (f := κ) (fun _ _ ↦ Nat.zero_le _) (Finset.mem_univ r)257        omega258      · rintro ⟨_, h⟩; exact h259    · intro κ hκ260      simp only [hD, Finset.mem_filter] at hκ261      simp only [Finset.mem_range]; omega262  -- `D` to `E`263  have h4 : ∑ κ ∈ D, F κ = ∑ κ ∈ E, F κ :=264    Finset.sum_filter_of_ne fun κ _ hne ↦ by_contra fun h ↦ hne (hF κ (by omega))265  -- `E` to `Fin`-valued vectors266  rw [h3, h4]267  refine Finset.sum_nbij' (fun κ r ↦ ⟨κ r % (n + 1), Nat.mod_lt _ (Nat.succ_pos _)⟩)268      (fun κ r ↦ (κ r).val) ?_ ?_ ?_ ?_ ?_269  · intro _ _; exact Finset.mem_univ _270  · intro κ _271    simp only [hE, Fintype.mem_piFinset, Finset.mem_range]272    exact fun r ↦ (κ r).isLt273  · intro κ hκ274    simp only [hE, Fintype.mem_piFinset, Finset.mem_range] at hκ275    funext r; exact Nat.mod_eq_of_lt (hκ r)276  · intro κ _277    funext r; exact Fin.ext (Nat.mod_eq_of_lt (κ r).isLt)278  · intro κ hκ279    simp only [hE, Fintype.mem_piFinset, Finset.mem_range] at hκ280    have : (fun r ↦ κ r % (n + 1)) = κ := funext fun r ↦ Nat.mod_eq_of_lt (hκ r)281    simp only [this]282 283/-- Multinomial expansion of `ψ_m(B_a)^{C_m}` (with `C_m = availablePoints ε m`) through degree284`n`: a sum over exponent vectors `κ` of generalized binomial coefficients times monomials in the285`ψ_m(F_{S(a;r+1)})`. -/286private theorem formalPow_adamsSer_clusterSer_scongr (ε : ℤ) (a m n : ℕ) (hm : 0 < m) :287    SCongr n (formalPow (availablePoints ε m).rational (adamsSer m (clusterSer a)))288        (∑ κ : Fin n → Fin (n + 1), PowerSeries.C (scalar289        ((∏ j ∈ Finset.range (∑ r : Fin n, (κ r).val), ((availablePoints ε m).rational - RatFunc.C290        (j : ℚ))) * RatFunc.C ((∏ r : Fin n, ((Nat.factorial (κ r).val : ℕ) : ℚ))⁻¹))) *291        (PowerSeries.C (∏ r : Fin n, (adamsCoef m (lawCoef292        (stateLaw (State.single a (r.val + 1))))) ^ (κ r).val) *293        (PowerSeries.X : Ser) ^ (m * ∑ r : Fin n, (r.val + 1) * (κ r).val))) := by294  -- Expand `g^c` binomially (`coeff_formalPow`), replace `g - 1` by its truncation `S`, expand295  -- each `S^k` multinomially, and regroup the exponent vectors.296  intro d hd297  set c := (availablePoints ε m).rational with hc298  set g := adamsSer m (clusterSer a) with hgdef299  set b : ℕ → Coef := fun s ↦ adamsCoef m (lawCoef (stateLaw (State.single a s))) with hb300  set S : Ser := ∑ r : Fin n, PowerSeries.C (b (r.val + 1)) *301      (PowerSeries.X : Ser) ^ (m * (r.val + 1)) with hSdef302  set T : (Fin n → ℕ) → Ser := fun κ ↦ PowerSeries.C (scalar303      ((∏ j ∈ Finset.range (∑ r : Fin n, κ r), (c - RatFunc.C (j : ℚ))) *304      RatFunc.C ((∏ r : Fin n, ((Nat.factorial (κ r) : ℕ) : ℚ))⁻¹))) *305      (PowerSeries.C (∏ r : Fin n, b (r.val + 1) ^ κ r) *306      (PowerSeries.X : Ser) ^ (m * ∑ r : Fin n, (r.val + 1) * κ r)) with hTdef307  have hg : PowerSeries.constantCoeff g = 1 := by308    rw [hgdef, constantCoeff_adamsSer m hm.ne', ← PowerSeries.coeff_zero_eq_constantCoeff_apply]309    simp [clusterSer]310  have hpow : ∀ k : ℕ, SCongr n ((g - 1) ^ k) (S ^ k) :=311    (adamsSer_clusterSer_sub_one_scongr a m n hm).pow312  -- the summands of the target are T applied to ℕ-vectors313  have hR : (∑ κ : Fin n → Fin (n + 1), PowerSeries.C (scalar314      ((∏ j ∈ Finset.range (∑ r : Fin n, (κ r).val), ((availablePoints ε m).rational - RatFunc.C315      (j : ℚ))) * RatFunc.C ((∏ r : Fin n, ((Nat.factorial (κ r).val : ℕ) : ℚ))⁻¹))) *316      (PowerSeries.C (∏ r : Fin n, (adamsCoef m (lawCoef (stateLaw (State.single a (r.val + 1)))))317      ^ (κ r).val) * (PowerSeries.X : Ser) ^ (m * ∑ r : Fin n, (r.val + 1) * (κ r).val)))318      = ∑ κ : Fin n → Fin (n + 1), T (fun r ↦ (κ r).val) := rfl319  rw [hR, coeff_formalPow c g hg d]320  have hsum_le : ∀ κ : Fin n → ℕ, ∑ r, κ r ≤ m * ∑ r : Fin n, (r.val + 1) * κ r := by321    intro κ322    calc ∑ r, κ r ≤ ∑ r : Fin n, (r.val + 1) * κ r :=323          Finset.sum_le_sum (fun r _ ↦ Nat.le_mul_of_pos_left _ (Nat.succ_pos _))324      _ ≤ _ := Nat.le_mul_of_pos_left _ hm325  have hTcoeff : ∀ κ : Fin n → ℕ, PowerSeries.coeff d (T κ) = if d = m * ∑ r : Fin n, (r.val + 1) *326      κ r then scalar ((∏ j ∈ Finset.range (∑ r : Fin n, κ r), (c - RatFunc.C (j : ℚ))) *327      RatFunc.C ((∏ r : Fin n, ((Nat.factorial (κ r) : ℕ) : ℚ))⁻¹)) * ∏ r : Fin n,328      b (r.val + 1) ^ κ r else 0 := by329    intro κ330    rw [hTdef]; dsimp only331    rw [← mul_assoc, ← map_mul, PowerSeries.coeff_C_mul_X_pow]332  have hTzero : ∀ κ : Fin n → ℕ, n < ∑ r, κ r → PowerSeries.coeff d (T κ) = 0 := by333    intro κ hκ334    rw [hTcoeff, if_neg]335    have := hsum_le κ336    omega337  -- step 1: extend the k-range and replace g - 1 by S338  have h1 : ∑ k ∈ Finset.range (d + 1), ((k.factorial : ℚ)⁻¹) •339      ((∏ j ∈ Finset.range k, (scalar c - (j : ℚ) • (1 : Coef))) *340      PowerSeries.coeff d ((g - 1) ^ k))341      = ∑ k ∈ Finset.range (n + 1), ((k.factorial : ℚ)⁻¹) •342          ((∏ j ∈ Finset.range k, (scalar c - (j : ℚ) • (1 : Coef))) *343          PowerSeries.coeff d (S ^ k)) := by344    rw [← Finset.sum_subset (Finset.range_subset_range.mpr (by omega : d + 1 ≤ n + 1))]345    · refine Finset.sum_congr rfl (fun k _ ↦ ?_)346      rw [hpow k d hd]347    · intro k _ hk348      rw [Finset.mem_range] at hk349      have hX : (PowerSeries.X : Ser) ^ k ∣ S ^ k := by350        apply pow_dvd_pow_of_dvd351        rw [PowerSeries.X_dvd_iff, hSdef, map_sum]352        refine Finset.sum_eq_zero (fun r _ ↦ ?_)353        rw [map_mul, map_pow, PowerSeries.constantCoeff_X, zero_pow (by positivity), mul_zero]354      obtain ⟨u, hu⟩ := hX355      rw [hu, PowerSeries.coeff_X_pow_mul', if_neg (by omega), mul_zero, smul_zero]356  -- step 2: multinomial expansion per k357  have h2 : ∀ k ∈ Finset.range (n + 1), ((k.factorial : ℚ)⁻¹) •358      ((∏ j ∈ Finset.range k, (scalar c - (j : ℚ) • (1 : Coef))) * PowerSeries.coeff d (S ^ k))359      = ∑ κ ∈ Finset.piAntidiag (Finset.univ : Finset (Fin n)) k, PowerSeries.coeff d (T κ) := by360    intro k _361    rw [hSdef, sum_C_mul_X_pow_pow m n k b, map_sum, Finset.mul_sum, Finset.smul_sum]362    refine Finset.sum_congr rfl (fun κ hκ ↦ ?_)363    rw [Finset.mem_piAntidiag] at hκ364    rw [PowerSeries.coeff_C_mul_X_pow, hTcoeff]365    split_ifs366    · have hk : ∑ r, κ r = k := hκ.1367      rw [hk]368      have hq := inv_factorial_mul_multinomial κ hk369      have hM : ((Nat.multinomial Finset.univ κ : ℕ) : Coef) =370          scalar (RatFunc.C (Nat.multinomial Finset.univ κ : ℚ)) := by371        rw [scalar_eq_algebraMap, map_natCast, map_natCast]372      have hP : (∏ j ∈ Finset.range k, (scalar c - (j : ℚ) • (1 : Coef))) =373          scalar (∏ j ∈ Finset.range k, (c - RatFunc.C (j : ℚ))) := by374        simp only [rat_smul_eq_scalar_mul, mul_one, scalar_eq_algebraMap, map_prod, map_sub]375      rw [rat_smul_eq_scalar_mul, hM, hP, ← hq, map_mul]376      simp only [scalar_eq_algebraMap, map_mul]377      ring378    · rw [mul_zero, smul_zero]379  rw [h1, Finset.sum_congr rfl h2, sum_range_sum_piAntidiag_eq_sum_fin n _ hTzero, map_sum]380 381private theorem scalar_prod {ι : Type*} (s : Finset ι) (f : ι → RatFunc ℚ) :382    scalar (∏ i ∈ s, f i) = ∏ i ∈ s, scalar (f i) := by383  simp only [scalar_eq_algebraMap, map_prod]384 385private theorem scongr_prod {ι : Type*} (n : ℕ) (s : Finset ι) (f g : ι → Ser)386    (h : ∀ i ∈ s, SCongr n (f i) (g i)) : SCongr n (∏ i ∈ s, f i) (∏ i ∈ s, g i) := by387  classical388  induction s using Finset.induction_on with389  | empty => exact SCongr.refl n _390  | insert x s hx ih =>391    rw [Finset.prod_insert hx, Finset.prod_insert hx]392    exact (h x (Finset.mem_insert_self _ _)).mul (ih fun i hi ↦ h i (Finset.mem_insert_of_mem hi))393 394/-- Truncated product expansion of `Π_{m=1}^n ψ_m(B_a)^{C_m}` as a sum over exponent families395`K i r`, obtained by multiplying the expansions of `formalPow_adamsSer_clusterSer_scongr`. -/396theorem prod_formalPow_adamsSer_clusterSer_scongr (ε : ℤ) (a n : ℕ) :lem-7.2397    SCongr n (∏ m ∈ Finset.Icc 1 n, formalPow (availablePoints ε m).rational398        (adamsSer m (clusterSer a))) (∑ K : Fin n → Fin n → Fin (n + 1),399        PowerSeries.C (scalar (∏ i : Fin n, ((∏ j ∈ Finset.range (∑ r : Fin n, (K i r).val),400        ((availablePoints ε (i.val + 1)).rational - RatFunc.C (j : ℚ))) *401        RatFunc.C ((∏ r : Fin n, ((Nat.factorial (K i r).val : ℕ) : ℚ))⁻¹)))) *402        (PowerSeries.C (∏ i : Fin n, ∏ r : Fin n, (adamsCoef (i.val + 1)403        (lawCoef (stateLaw (State.single a (r.val + 1))))) ^ (K i r).val) *404        (PowerSeries.X : Ser) ^ (∑ i : Fin n, (i.val + 1) * ∑ r : Fin n, (r.val + 1) *405        (K i r).val))) := by406  have hre : ∏ m ∈ Finset.Icc 1 n, formalPow (availablePoints ε m).rational407      (adamsSer m (clusterSer a))408      = ∏ i : Fin n, formalPow (availablePoints ε (i.val + 1)).rational409          (adamsSer (i.val + 1) (clusterSer a)) := by410    rw [Fin.prod_univ_eq_prod_range (fun i ↦ formalPow (availablePoints ε (i + 1)).rational411      (adamsSer (i + 1) (clusterSer a))), ← Finset.Ico_add_one_right_eq_Icc,412      Finset.prod_Ico_eq_prod_range]413    simp only [Nat.add_sub_cancel, add_comm 1]414  rw [hre]415  have hprod := scongr_prod n Finset.univ _ _ (fun (i : Fin n) _ ↦416    formalPow_adamsSer_clusterSer_scongr ε a (i.val + 1) n (Nat.succ_pos _))417  refine hprod.trans ?_418  rw [Finset.prod_univ_sum, Fintype.piFinset_univ]419  refine SCongr.of_eq (Finset.sum_congr rfl fun K _ ↦ ?_)420  simp only [Finset.prod_mul_distrib, ← map_prod, ← scalar_prod,421      Finset.prod_pow_eq_pow_sum, Finset.mul_sum]422 423/-- The plethystic exponential is additive-to-multiplicative: `Exp(f+g) = Exp f · Exp g`. -/424private theorem pExp_add (f g : Ser) : pExp (f + g) = pExp f * pExp g := by425  rw [pExp, pExp, pExp, plethSum_add]426  exact expSer_add _ _ (constantCoeff_plethSum f) (constantCoeff_plethSum g)427 428/-- `Exp f` has constant term `1`. -/429private theorem constantCoeff_pExp (f : Ser) : PowerSeries.constantCoeff (pExp f) = 1 :=430  constantCoeff_expSer _ (constantCoeff_plethSum f)431 432/-- `Log g` has constant term `0`. -/433private theorem constantCoeff_pLog (g : Ser) : PowerSeries.constantCoeff (pLog g) = 0 :=434  constantCoeff_moebiusSum _435 436/-- `Exp ∘ Log = id` on series with constant term `1`. -/437private theorem pExp_pLog (g : Ser) (hg : PowerSeries.constantCoeff g = 1) : pExp (pLog g) = g := by438  rw [pExp, pLog, plethSum_moebiusSum _ (constantCoeff_logSer g hg), expSer_logSer g hg]439 440/-- `Log ∘ Exp = id` on series with constant term `0`. -/441private theorem pLog_pExp (f : Ser) (hf : PowerSeries.constantCoeff f = 0) : pLog (pExp f) = f := by442  rw [pExp, pLog, logSer_expSer _ (constantCoeff_plethSum f), moebiusSum_plethSum f hf]443 444/-- The plethystic power `P_w(g)` has constant term `1`. -/445theorem constantCoeff_pPow (w : RatFunc ℚ) (g : Ser) : PowerSeries.constantCoeff (pPow w g) = 1 :=446  constantCoeff_pExp _447 448private theorem constantCoeff_C_mul_pLog (a : RatFunc ℚ) (g : Ser) :449    PowerSeries.constantCoeff (PowerSeries.C (scalar a) * pLog g) = 0 := by450  simp [constantCoeff_pLog]451 452/-- `P_w ∘ P_z = P_{wz}`. -/453theorem pPow_pPow (w z : RatFunc ℚ) (g : Ser) : pPow w (pPow z g) = pPow (w * z) g := byPow_v and the first-difference rule454  rw [pPow, pPow, pLog_pExp _ (constantCoeff_C_mul_pLog z g), ← mul_assoc, ← map_mul,455    ← scalar_mul, pPow]456 457/-- `P_w P_z = P_{w+z}`. -/458theorem pPow_mul_pPow (w z : RatFunc ℚ) (g : Ser) : pPow w g * pPow z g = pPow (w + z) g := by459  rw [pPow, pPow, pPow, ← pExp_add, scalar_add, map_add, add_mul]460 461/-- `P_1 = id` on series with constant term `1`. -/462private theorem pPow_one (g : Ser) (hg : PowerSeries.constantCoeff g = 1) : pPow 1 g = g := by463  rw [pPow, scalar_one, map_one, one_mul, pExp_pLog g hg]464 465/-- If `g ≡ h` below degree `n`, then the degree-`n` coefficients of `P_w(g)` and `P_w(h)` differ466by `w` times those of `g` and `h`. -/467theorem coeff_pPow_sub_of_scongr (n : ℕ) (hn : 0 < n) (w : RatFunc ℚ) (g h : Ser)Pow_v and the first-difference rule468    (hg : PowerSeries.constantCoeff g = 1) (hh : PowerSeries.constantCoeff h = 1)469    (hgh : SCongr (n - 1) g h) :470    PowerSeries.coeff n (pPow w g) - PowerSeries.coeff n (pPow w h) =471      scalar w * (PowerSeries.coeff n g - PowerSeries.coeff n h) := by472  have hL : SCongr (n - 1) (logSer g) (logSer h) := hgh.logSer hg hh473  have hP : SCongr (n - 1) (PowerSeries.C (scalar w) * pLog g)474      (PowerSeries.C (scalar w) * pLog h) := hL.moebiusSum.C_mul _475  rw [pPow, pPow, pExp, pExp, coeff_expSer_sub_of_scongr n hn _ _ (constantCoeff_plethSum _)476    (constantCoeff_plethSum _) hP.plethSum, coeff_plethSum_sub_of_scongr n hn _ _ hP,477    PowerSeries.coeff_C_mul, PowerSeries.coeff_C_mul, ← mul_sub, pLog, pLog,478    coeff_moebiusSum_sub_of_scongr n hn _ _ hL, coeff_logSer_sub_of_scongr n hn g h hg hh hgh]479 480/-- A sum over the allowed tangent patterns of `S(a;n)` depending only on the divisor degree `d`,481the tangent depth `r`, and the off-boundary pattern, reindexed as a sum over `d`, `r` and patterns482of weight `d - r`. -/483theorem sum_allowedPatterns_single (a n : ℕ) (ha : 0 < a)484    (F : ℕ → ℕ → Pattern (State.single a n).degree → Coef) :485    ∑ P ∈ allowedPatterns (State.single a n), F P.d.val P.rt.val P.other =486      ∑ d ∈ Finset.Icc 1 n, ∑ r ∈ Finset.range (d + 1), (if ((0 < r ↔ d < n) ∧ r ≤ d) then487        ∑ m ∈ (Finset.univ : Finset (Pattern (State.single a n).degree)).filter488          (fun m ↦ patternWeight m = d - r), F d r m else 0) := by489  rw [sum_allowedPatterns_reindex (.single a n) n (Nat.le_mul_of_pos_left n ha)490    (fun d rt rx ↦ rx = 0 ∧ (0 < rt ↔ d < n)) (fun P ↦ by simp [allowedPatterns, Allowed])491    (fun d rt _ m ↦ F d rt m)]492  refine Finset.sum_congr rfl fun d _ ↦ Finset.sum_congr rfl fun r _ ↦ ?_493  rw [Finset.sum_eq_single 0 (fun rx _ h0 ↦ if_neg fun h ↦ h0 h.1.1) (by simp)]494  simp only [true_and, add_zero, Nat.sub_zero]495 496private theorem otherChildren_length {N : ℕ} (a : ℕ) (m : Pattern N) :497    (otherChildren a m).length = ∑ ij, (m ij).val := by498  unfold otherChildren499  rw [List.length_flatMap]500  simp only [List.length_replicate]501  rw [Finset.sum_map_toList]502 503private theorem mem_otherChildren {N : ℕ} (a : ℕ) (m : Pattern N) (x : ℕ × State) :504    x ∈ otherChildren a m ↔ ∃ ij, (m ij).val ≠ 0 ∧ x = (ij.1.val+1, .single a (ij.2.val+1)) := by505  unfold otherChildren506  simp [List.mem_flatMap, List.mem_replicate, eq_comm]507 508private theorem otherChildren_eq_single_iff (a n N : ℕ) (hn : 1 ≤ n) (hnN : n - 1 < N)509    (m : Pattern N) :510    otherChildren a m = [(1, State.single a n)] ↔511      ∀ ij : Fin N × Fin N, (m ij).val = (if ij.1.val = 0 ∧ ij.2.val = n - 1 then 1 else 0) := by512  have h0 : 0 < N := by omega513  let ij0 : Fin N × Fin N := (⟨0, h0⟩, ⟨n-1, hnN⟩)514  have key : ∀ ij : Fin N × Fin N, (ij.1.val = 0 ∧ ij.2.val = n - 1) ↔ ij = ij0 := by515    intro ij516    constructor517    · rintro ⟨h1, h2⟩; exact Prod.ext (Fin.ext h1) (Fin.ext h2)518    · rintro rfl; simp [ij0]519  have hrep : [(1, State.single a n)] = List.replicate 1 (1, State.single a n) := rfl520  rw [hrep, List.eq_replicate_iff, otherChildren_length]521  constructor522  · rintro ⟨hlen, hall⟩523    have hsupp : ∀ ij, (m ij).val ≠ 0 → ij = ij0 := by524      intro ij hij525      have := hall _ ((mem_otherChildren a m _).2 ⟨ij, hij, rfl⟩)526      simp only [Prod.mk.injEq, State.single.injEq] at this527      rw [← key]; omega528    have hs : ∑ ij, (m ij).val = (m ij0).val :=529      Finset.sum_eq_single ij0 (fun b _ hb ↦ by by_contra h; exact hb (hsupp b h)) (by simp)530    intro ij531    by_cases h : ij = ij0532    · subst h; rw [if_pos ((key _).2 rfl)]; omega533    · rw [if_neg (by rw [key]; exact h)]534      by_contra h'; exact h (hsupp ij h')535  · intro hm536    constructor537    · rw [Finset.sum_eq_single ij0]538      · rw [hm]; simp [ij0]539      · intro b _ hb; rw [hm, if_neg (by rw [key]; exact hb)]540      · simp541    · intro b hb542      obtain ⟨ij, hij, rfl⟩ := (mem_otherChildren a m b).1 hb543      rw [hm] at hij544      split_ifs at hij with h545      · simp only [Prod.mk.injEq, State.single.injEq]; exact ⟨by omega, trivial, by omega⟩546      · exact absurd rfl hij547 548/-- An allowed tangent pattern of `S(a;n)` (`n ≥ 2`) is the self pattern exactly when `d = n`,549there is no tangent part, and the off-boundary pattern is the single point of type `(1, n-1)`. -/550theorem selfPattern_single_iff (a n : ℕ) (ha : 0 < a) (hn : 2 ≤ n)551    (P : TangentPattern (State.single a n).degree) (hP : Allowed (State.single a n) P) :552    SelfPattern (State.single a n) P ↔ (P.d.val = n ∧ P.rt.val = 0 ∧ P.rx.val = 0 ∧553        ∀ ij : Fin (State.single a n).degree × Fin (State.single a n).degree, (P.other ij).val =554        (if ij.1.val = 0 ∧ ij.2.val = n - 1 then 1 else 0)) := by555  have hnN : n - 1 < (State.single a n).degree := by556    change n - 1 < a * n557    have : n ≤ a * n := Nat.le_mul_of_pos_left n ha558    omega559  have hO := otherChildren_eq_single_iff a n _ (by omega) hnN P.other560  obtain ⟨hd0, hsum, hdle, hrx, hrt⟩ := hP561  have hch : children (State.single a n) P =562      (if P.rt.val=0 then [] else [(1,State.crossing a a P.rt.val (n-P.d.val))]) ++563        otherChildren a P.other := rfl564  constructor565  · rintro ⟨a', c', _, hc⟩566    rw [hch] at hc567    have hrt0 : P.rt.val = 0 := by568      by_contra h569      rw [if_neg h] at hc570      simp at hc571    rw [if_pos hrt0, List.nil_append] at hc572    have hm := hO.1 hc573    refine ⟨?_, hrt0, hrx, hm⟩574    have hw : patternWeight P.other = n := by575      unfold patternWeight576      rw [Finset.sum_eq_single ((⟨0, by omega⟩, ⟨n-1, hnN⟩) : Fin (State.single a n).degree × Fin577          (State.single a n).degree)]578      · rw [hm]; simp; omega579      · intro b _ hb580        rw [hm, if_neg]581        · simp582        · rintro ⟨h1, h2⟩; exact hb (Prod.ext (Fin.ext h1) (Fin.ext h2))583      · simp584    omega585  · rintro ⟨hd, hrt0, _, hm⟩586    refine ⟨a, n, rfl, ?_⟩587    rw [hch, if_pos hrt0, List.nil_append]588    exact hO.2 hm589 590/-- For `n ≥ 2`, `S(a;n)` has exactly one allowed self pattern. -/591theorem exists_unique_selfPattern_single (a n : ℕ) (ha : 0 < a) (hn : 2 ≤ n) :(6.6)592    ∃ P₀ : TangentPattern (State.single a n).degree, Allowed (State.single a n) P₀ ∧593        SelfPattern (State.single a n) P₀ ∧ ∀ Q : TangentPattern (State.single a n).degree,594        Allowed (State.single a n) Q → SelfPattern (State.single a n) Q → Q = P₀ := by595  have hdeg : (State.single a n).degree = a * n := rfl596  have hnN : n ≤ (State.single a n).degree := by597    rw [hdeg]; exact Nat.le_mul_of_pos_left n ha598  have hn0 : 0 < n := by omega599  let m₀ : Pattern (State.single a n).degree := fun ij ↦600    if ij.1.val = 0 ∧ ij.2.val = n - 1 then ⟨1, by omega⟩ else ⟨0, by omega⟩601  let P₀ : TangentPattern (State.single a n).degree :=602    ⟨⟨n, by omega⟩, ⟨0, by omega⟩, ⟨0, by omega⟩, m₀⟩603  have hm : ∀ ij, (P₀.other ij).val = (if ij.1.val = 0 ∧ ij.2.val = n - 1 then 1 else 0) := by604    intro ij605    change (m₀ ij).val = _606    simp only [m₀]607    split_ifs <;> rfl608  have hA : Allowed (State.single a n) P₀ := by609    refine ⟨hn0, ?_, ?_⟩610    · have : patternWeight P₀.other = n := by611        unfold patternWeight612        have hlt : n - 1 < (State.single a n).degree := by omega613        have hpos : 0 < (State.single a n).degree := by omega614        rw [Finset.sum_eq_single (⟨0, hpos⟩, ⟨n - 1, hlt⟩)]615        · rw [hm]; simp; omega616        · intro ij _ hne617          rw [hm]618          have : ¬ (ij.1.val = 0 ∧ ij.2.val = n - 1) := by619            rintro ⟨h1, h2⟩620            apply hne621            exact Prod.ext (Fin.ext h1) (Fin.ext h2)622          simp [this]623        · intro h; exact absurd (Finset.mem_univ _) h624      change 0 + 0 + _ = n625      omega626    · refine ⟨le_refl _, rfl, ?_⟩627      change 0 < 0 ↔ n < n628      simp629  have hS := (selfPattern_single_iff a n ha hn P₀ hA).2630    ⟨rfl, rfl, rfl, hm⟩631  refine ⟨P₀, hA, hS, ?_⟩632  intro Q hQ hQS633  obtain ⟨h1, h2, h3, h4⟩ := (selfPattern_single_iff a n ha hn Q hQ).1 hQS634  cases Q with635  | mk d rt rx other =>636    simp only at h1 h2 h3 h4637    have e1 : d = P₀.d := Fin.ext h1638    have e2 : rt = P₀.rt := Fin.ext h2639    have e3 : rx = P₀.rx := Fin.ext h3640    have e4 : other = P₀.other := by641      funext ij; apply Fin.ext; rw [h4, hm]642    rw [e1, e2, e3, e4]643 644/-- Reindexing a triple sum over `(rx, m, rt)` with `rx + m + rt ≤ K` by the total645`d = rx + m + rt`. -/646theorem sum_triple_reindex (c K : ℕ) (hK : K ≤ c) (G : ℕ → ℕ → ℕ → Coef) :647    ∑ rx ∈ Finset.range (c + 1), ∑ m ∈ Finset.range (c + 1), ∑ rt ∈ Finset.range (c + 1),648        (if rx + m + rt ≤ K then G rx m rt else 0) = ∑ d ∈ Finset.range (c + 1),649        ∑ rt ∈ Finset.range (d + 1), ∑ rx ∈ Finset.range (d + 1),650        (if (rt + rx ≤ d ∧ d ≤ K) then G rx (d - rt - rx) rt else 0) := by651  rw [← Finset.sum_product', ← Finset.sum_product']652  have h : ∀ d : ℕ, ∑ rt ∈ Finset.range (d + 1), ∑ rx ∈ Finset.range (d + 1),653      (if (rt + rx ≤ d ∧ d ≤ K) then G rx (d - rt - rx) rt else 0) =654      ∑ p ∈ Finset.range (d + 1) ×ˢ Finset.range (d + 1),655      (if (p.1 + p.2 ≤ d ∧ d ≤ K) then G p.2 (d - p.1 - p.2) p.1 else 0) := fun d ↦656      (Finset.sum_product' _ _ _).symm657  simp_rw [h]658  rw [Finset.sum_sigma']659  rw [← Finset.sum_filter, ← Finset.sum_filter]660  refine Finset.sum_bij' (fun p _ ↦ (⟨p.1.1 + p.1.2 + p.2, (p.2, p.1.1)⟩ : (_ : ℕ) × (ℕ × ℕ)))661    (fun q _ ↦ ((q.2.2, q.1 - q.2.1 - q.2.2), q.2.1)) ?_ ?_ ?_ ?_ ?_662  · rintro ⟨⟨rx, m⟩, rt⟩ h663    simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_sigma, Finset.mem_range] at h ⊢664    omega665  · rintro ⟨d, rt, rx⟩ h666    simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_sigma, Finset.mem_range] at h ⊢667    omega668  · rintro ⟨⟨rx, m⟩, rt⟩ h669    simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_range] at h ⊢670    refine Prod.ext (Prod.ext rfl ?_) rfl671    simp only; omega672  · rintro ⟨d, rt, rx⟩ h673    simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_sigma, Finset.mem_range] at h ⊢674    have : rx + (d - rt - rx) + rt = d := by omega675    simp [this]676  · rintro ⟨⟨rx, m⟩, rt⟩ h677    simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_range] at h ⊢678    simp679 680/-! ### Well-formed expressions and their rational functions -/681 682/-- A safe expression is well formed. -/683private theorem Expr.wf_of_safe (x : Expr) (q : ℚ) (hx : x.safe q) : x.wf := by684  induction x with685  | const r => trivial686  | var => trivial687  | add a b iha ihb => exact ⟨iha hx.1, ihb hx.2⟩688  | mul a b iha ihb => exact ⟨iha hx.1, ihb hx.2⟩689  | inv a ih =>690    refine ⟨ih hx.1, fun h ↦ hx.2 ?_⟩691    obtain ⟨_, h2⟩ := expression_fraction a q hx.1692    rw [h2, h]; simp693 694/-- Powers of well-formed expressions are well formed. -/695theorem Expr.wf_pow {x : Expr} (hx : x.wf) (k : ℕ) : (Expr.pow x k).wf := by696  induction k with697  | zero => simp [Expr.pow, Expr.wf]698  | succ k ih => exact ⟨ih, hx⟩699 700private theorem fraction_pow_var_ne_zero (k : ℕ) : (Expr.pow Expr.var k).fraction.1 ≠ 0 := by701  induction k with702  | zero => simp [Expr.pow, Expr.fraction]703  | succ k ih =>704    simp only [Expr.pow, Expr.fraction]705    exact mul_ne_zero ih Polynomial.X_ne_zero706 707/-- A sum of well-formed expressions is well formed. -/708private theorem Expr.wf_sum {xs : List Expr} (h : ∀ z ∈ xs, z.wf) : (Expr.sum xs).wf := by709  induction xs with710  | nil => simp [Expr.sum, Expr.wf]711  | cons a t ih =>712    simp only [List.mem_cons, forall_eq_or_imp] at h713    exact ⟨h.1, ih h.2⟩714 715private theorem wf_pointCount (δ : ℕ) : (pointCount δ).wf := by716  refine ⟨trivial, Expr.wf_sum ?_⟩717  intro z hz718  simp only [List.mem_map] at hz719  obtain ⟨j, -, rfl⟩ := hz720  exact ⟨trivial, Expr.wf_pow (x := Expr.var) trivial _⟩721 722/-- The available-point counts are well formed. -/723private theorem wf_availablePoints (ε : ℤ) (δ : ℕ) : (availablePoints ε δ).wf := by724  unfold availablePoints725  split_ifs726  · exact ⟨trivial, trivial⟩727  · exact wf_pointCount δ728 729/-- The return weights are well formed. -/730theorem wf_returnWeight (c : ℕ) : (returnWeight c).wf :=731  ⟨trivial, Expr.wf_pow (x := Expr.var) trivial _, fraction_pow_var_ne_zero _⟩732 733/-- A well-formed expression has nonzero denominator. -/734theorem Expr.fraction_snd_ne_zero {x : Expr} (hx : x.wf) : x.fraction.2 ≠ 0 := by735  induction x with736  | const r => simp [Expr.fraction]737  | var => simp [Expr.fraction]738  | add a b iha ihb | mul a b iha ihb => exact mul_ne_zero (iha hx.1) (ihb hx.2)739  | inv a _ => exact hx.2740 741/-- `Expr.rational` is additive on well-formed expressions. -/742theorem Expr.rational_add {x y : Expr} (hx : x.wf) (hy : y.wf) :743    (Expr.add x y).rational = x.rational + y.rational := by744  have h1' := RatFunc.algebraMap_ne_zero (Expr.fraction_snd_ne_zero hx)745  have h2' := RatFunc.algebraMap_ne_zero (Expr.fraction_snd_ne_zero hy)746  simp only [Expr.rational, Expr.fraction, map_mul, map_add]747  rw [div_add_div _ _ h1' h2', mul_comm (algebraMap (Polynomial ℚ) (RatFunc ℚ) x.fraction.2)748    (algebraMap (Polynomial ℚ) (RatFunc ℚ) y.fraction.1)]749 750/-- `Expr.rational` is multiplicative. -/751theorem Expr.rational_mul (x y : Expr) : (Expr.mul x y).rational = x.rational * y.rational := by752  simp only [Expr.rational, Expr.fraction, map_mul]753  rw [div_mul_div_comm]754 755/-- `Expr.rational` commutes with inversion. -/756theorem Expr.rational_inv (x : Expr) : (Expr.inv x).rational = x.rational⁻¹ := by757  simp only [Expr.rational, Expr.fraction]758  rw [inv_div]759 760/-- The rational function of a constant. -/761theorem Expr.rational_const (r : ℚ) : (Expr.const r).rational = RatFunc.C r := by762  simp [Expr.rational, Expr.fraction, RatFunc.algebraMap_C]763 764/-- The rational function of the variable is `q`. -/765theorem Expr.rational_var : Expr.var.rational = (RatFunc.X : RatFunc ℚ) := by766  simp [Expr.rational, Expr.fraction, RatFunc.algebraMap_X]767 768/-- `lawCoef` of the empty law is `0`. -/769theorem lawCoef_nil : lawCoef ([] : Law) = 0 := lawInterp_nil _770 771/-- `lawCoef` turns `lawScale x` into multiplication by the scalar `x.rational`. -/772theorem lawCoef_lawScale (x : Expr) (L : Law) :773    lawCoef (lawScale x L) = scalar x.rational * lawCoef L :=774  lawInterp_lawScale _ Expr.rational_mul x L775 776/-- `lawCoef` of an atom is its monomial `Z_{e,f}`. -/777private theorem lawCoef_lawAtom (e f : ℕ) :778    lawCoef (lawAtom e f) = AddMonoidAlgebra.single ({(e, f)} : FactorType) (1 : RatFunc ℚ) := by779  simp [lawCoef, lawAtom, Expr.rational_const]780 781/-- `lawCoef` sends `flatMap` to the sum of the pieces. -/782theorem lawCoef_flatMap {α : Type} (xs : List α) (g : α → Law) :783    lawCoef (xs.flatMap g) = (xs.map fun u ↦ lawCoef (g u)).sum :=784  lawInterp_flatMap _ xs g785 786/-! ### The cluster series -/787 788/-- The constant term of the cluster series `B_a` is `1`. -/789theorem coeff_zero_clusterSer (a : ℕ) : PowerSeries.coeff 0 (clusterSer a) = 1 := by790  simp [clusterSer, PowerSeries.coeff_mk]791 792/-- The constant term of the cluster series `B_a` is `1`. -/793theorem constantCoeff_clusterSer (a : ℕ) : PowerSeries.constantCoeff (clusterSer a) = 1 := by794  rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply, coeff_zero_clusterSer]795 796/-- The coefficient of `x^{n+1}` in `B_a` is the law of `S(a;n+1)`. -/797theorem coeff_succ_clusterSer (a n : ℕ) :798    PowerSeries.coeff (n + 1) (clusterSer a) = lawCoef (stateLaw (State.single a (n + 1))) := by799  simp [clusterSer, PowerSeries.coeff_mk]800 801/-- The degree-one coefficient of `B_a` is `Z_{a,1}`. -/802theorem coeff_one_clusterSer (a : ℕ) :803    PowerSeries.coeff 1 (clusterSer a) = AddMonoidAlgebra.single ({(a, 1)} : FactorType) 1 := by804  rw [coeff_succ_clusterSer a 0, zero_add, terminal_law, lawCoef_lawAtom]805 806/-- The Euler transforms `eulerSer ε a` have constant term `1`. -/807theorem constantCoeff_eulerSer (ε : ℤ) (a : ℕ) : PowerSeries.constantCoeff (eulerSer ε a) = 1 :=808  constantCoeff_pPow _ _809 810/-- The Euler transforms `eulerSer ε a` have constant term `1`. -/811theorem coeff_zero_eulerSer (ε : ℤ) (a : ℕ) : PowerSeries.coeff 0 (eulerSer ε a) = 1 := by812  rw [PowerSeries.coeff_zero_eq_constantCoeff_apply, constantCoeff_eulerSer]813 814private theorem coeff_dilate_recipSer_clusterSer (a m : ℕ) :815    PowerSeries.coeff m (dilate (recipSer (clusterSer a))) =816      qpow (m : ℤ) * recipCoef (PowerSeries.coeff m (clusterSer a)) := by817  rw [coeff_dilate, coeff_recipSer]818 819/-- The constant term of `S(B_aᵛ)` is `1`. -/820theorem coeff_zero_dilate_recipSer_clusterSer (a : ℕ) :821    PowerSeries.coeff 0 (dilate (recipSer (clusterSer a))) = 1 := by822  rw [coeff_dilate_recipSer_clusterSer, coeff_zero_clusterSer, map_one, mul_one, Nat.cast_zero,823    qpow_zero]824 825/-- The degree-one coefficient of `S(B_aᵛ)` is `q Z_{a,1}`. -/826theorem coeff_one_dilate_recipSer_clusterSer (a : ℕ) :827    PowerSeries.coeff 1 (dilate (recipSer (clusterSer a))) =828      qpow 1 * AddMonoidAlgebra.single ({(a, 1)} : FactorType) 1 := by829  rw [coeff_dilate_recipSer_clusterSer, coeff_one_clusterSer, recipCoef_single, map_one]830  rfl831 832/-- If `G_b ≡ S(B_bᵛ)` through degree `M` for every `b > 0`, then `S(P_sᵛ) · P_s ≡ 1` through833degree `M`, where `P_s = eulerSer (-1) s`. -/834theorem dilate_recipSer_eulerSer_mul_scongr_one (M s : ℕ) (hs : 0 < s) (hS : ∀ a : ℕ, 0 < a →835    SCongr M (eulerSer 0 a) (dilate (recipSer (clusterSer a)))) :836    SCongr M (dilate (recipSer (eulerSer (-1) s)) * eulerSer (-1) s) 1 := by837  set B := clusterSer s with hBdef838  have hB : PowerSeries.constantCoeff B = 1 := constantCoeff_clusterSer s839  -- Step 1: `P_s B_s = G_s`.840  have h1 : eulerSer (-1) s * B = eulerSer 0 s := by841    unfold eulerSer842    rw [← hBdef]843    conv_lhs => arg 2; rw [← pPow_one B hB]844    rw [pPow_mul_pPow]845    congr 1846    push_cast; ring847  -- Step 2: apply `S ∘ v`.848  have h2 : dilate (recipSer (eulerSer (-1) s)) * dilate (recipSer B) =849      dilate (recipSer (eulerSer 0 s)) := by850    rw [← h1, recipSer_mul, dilate_mul]851  -- Step 3: `S(G_sᵛ) ≡ B_s`.852  have hG := hS s hs853  have h3a : SCongr M (recipSer (eulerSer 0 s)) (recipSer (dilate (recipSer B))) := by854    intro m hm855    rw [coeff_recipSer, coeff_recipSer, hG m hm]856  rw [recipSer_dilate, recipSer_recipSer] at h3a857  have h3 : SCongr M (dilate (recipSer (eulerSer 0 s))) B := by858    simpa only [dilate_codilate] using h3a.dilate859  -- Step 4: cancel `B_s`.860  set D := dilate (recipSer (eulerSer (-1) s))861  have h4' : SCongr M (dilate (recipSer (eulerSer 0 s))) (D * (eulerSer (-1) s * B)) := by862    rw [h1, ← h2]; exact (SCongr.refl M D).mul hG.symm863  refine SCongr.of_mul_right hB ?_864  rw [one_mul, mul_assoc]865  exact h4'.symm.trans h3866 867/-- `lawCoef` is multiplicative on finite products `lawProd`. -/868theorem lawCoef_lawProd (Ls : List Law) : lawCoef (lawProd Ls) = (Ls.map lawCoef).prod :=869  lawInterp_lawProd _ Expr.rational_mul (by simp [Expr.rational_const]) Ls870 871/-- `B_a = P_{1/q}(G_a)`: the Euler transform with parameter `q` is inverted by the plethystic872power `1/q`. -/873theorem clusterSer_eq_pPow (a : ℕ) :(9.4)874    clusterSer a = pPow (RatFunc.X : RatFunc ℚ)⁻¹ (eulerSer 0 a) := by875  rw [eulerSer, Int.cast_zero, add_zero, pPow_pPow, inv_mul_cancel₀ RatFunc.X_ne_zero,876    pPow_one _ (constantCoeff_clusterSer a)]877 878/-- `S(G_aᵛ) = P_{1/q}(S(B_aᵛ))`. -/879theorem dilate_recipSer_eulerSer_eq_pPow (a : ℕ) :880    dilate (recipSer (eulerSer 0 a)) =881      pPow (RatFunc.X : RatFunc ℚ)⁻¹ (dilate (recipSer (clusterSer a))) := by882  have hR : PowerSeries.constantCoeff (recipSer (clusterSer a)) = 1 := by883    rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply, coeff_recipSer,884      PowerSeries.coeff_zero_eq_constantCoeff_apply, constantCoeff_clusterSer, map_one]885  rw [eulerSer, Int.cast_zero, add_zero, recipSer_pPow _ _ (constantCoeff_clusterSer a),886    recipRat_X, dilate_pPow _ _ hR]887 888/-- `Expr.rational` is additive on sums of well-formed expressions. -/889theorem Expr.rational_sum {xs : List Expr} (h : ∀ z ∈ xs, z.wf) :890    (Expr.sum xs).rational = (xs.map Expr.rational).sum := by891  induction xs with892  | nil => simpa [Expr.sum] using Expr.rational_const 0893  | cons a t ih =>894    have ht : ∀ z ∈ t, z.wf := fun z hz ↦ h z (by simp [hz])895    change (Expr.add a (Expr.sum t)).rational = _896    rw [Expr.rational_add (h a (by simp)) (Expr.wf_sum ht), ih ht]; simp897 898/-- `Expr.rational` is multiplicative on products. -/899private theorem Expr.rational_prod (xs : List Expr) :900    (Expr.prod xs).rational = (xs.map Expr.rational).prod := by901  induction xs with902  | nil => simpa [Expr.prod] using Expr.rational_const 1903  | cons a t ih =>904    change (Expr.mul a (Expr.prod t)).rational = _905    rw [Expr.rational_mul, ih]; simp906 907/-- `Expr.rational` commutes with powers. -/908theorem Expr.rational_pow (x : Expr) (n : ℕ) : (Expr.pow x n).rational = x.rational ^ n := by909  induction n with910  | zero => simpa [Expr.pow] using Expr.rational_const 1911  | succ k ih =>912    change (Expr.mul (Expr.pow x k) x).rational = _913    rw [Expr.rational_mul, ih, pow_succ]914 915private theorem Expr.rational_neg (x : Expr) : (Expr.neg x).rational = - x.rational := by916  change (Expr.mul (Expr.const (-1)) x).rational = _917  rw [Expr.rational_mul, Expr.rational_const]; simp918 919/-- `Expr.rational` is additive on differences of well-formed expressions. -/920theorem Expr.rational_sub {x y : Expr} (hx : x.wf) (hy : y.wf) :921    (Expr.sub x y).rational = x.rational - y.rational := by922  change (Expr.add x y.neg).rational = _923  rw [Expr.rational_add hx (show (Expr.neg y).wf from ⟨trivial, hy⟩), Expr.rational_neg,924    sub_eq_add_neg]925 926/-- The rational function of `eminusOne` is `q - 1`. -/927theorem rational_eminusOne : eminusOne.rational = (RatFunc.X : RatFunc ℚ) - 1 := by928  change (Expr.sub Expr.var (Expr.const 1)).rational = _929  rw [Expr.rational_sub (x := Expr.var) (y := Expr.const 1) trivial trivial, Expr.rational_var,930    Expr.rational_const]931  simp932 933/-- The rational function of the divisor count of a pattern `m`: a product over rows `i` of934generalized binomial coefficients in `availablePoints ε (i+1)`. -/935theorem rational_divisorCount (N : ℕ) (ε : ℤ) (m : Pattern N) :936    (divisorCount ε m).rational = ∏ i : Fin N, ((∏ j ∈ Finset.range (∑ j : Fin N, (m (i, j)).val),937        ((availablePoints ε (i.val + 1)).rational - RatFunc.C (j : ℚ))) *938        RatFunc.C (1 / (∏ j : Fin N, ((Nat.factorial (m (i, j)).val : ℕ) : ℚ)))) := by939  have hfall : ∀ (x : Expr), x.wf → ∀ k : ℕ, (falling x k).rational =940      ∏ j ∈ Finset.range k, (x.rational - RatFunc.C (j : ℚ)) := by941    intro x hx k942    unfold falling943    have hl : (do let a ← List.range k; pure (a : ℚ) : List ℚ) =944        (List.range k).map (fun a : ℕ ↦ (a : ℚ)) := by945      simp only [bind, List.flatMap]946      induction List.range k <;> simp_all947    rw [hl, (Expr.rational_prod _), List.map_map, List.map_map]948    have hc : List.map ((Expr.rational ∘ fun j ↦ x.sub (Expr.const j)) ∘ fun a : ℕ ↦ (a : ℚ))949        (List.range k)950        = List.map (fun j : ℕ ↦ x.rational - RatFunc.C (j : ℚ)) (List.range k) := by951      apply List.map_congr_left952      intro j _953      simp only [Function.comp]954      rw [Expr.rational_sub hx (by simp [Expr.wf]),955        (Expr.rational_const (j:ℚ))]956    rw [hc]957    rw [Finset.prod_eq_multiset_prod, Finset.range_val]958    rfl959  unfold divisorCount960  rw [(Expr.rational_prod _), List.map_map]961  rw [← Finset.prod_map_toList]962  congr 1963  apply List.map_congr_left964  intro i _965  simp only [Function.comp]966  rw [Expr.rational_mul, hfall _ (wf_availablePoints _ _), Expr.rational_const]967 968/-- The degree-`n` coefficient of the family expansion of969`prod_formalPow_adamsSer_clusterSer_scongr` is the970pattern sum `patternSum ε a n n`. -/971theorem coeff_euler_families_eq_patternSum (ε : ℤ) (a n : ℕ) :972    PowerSeries.coeff n (∑ K : Fin n → Fin n → Fin (n + 1),973        PowerSeries.C (scalar (∏ i : Fin n, ((∏ j ∈ Finset.range (∑ r : Fin n, (K i r).val),974        ((availablePoints ε (i.val + 1)).rational - RatFunc.C (j : ℚ))) *975        RatFunc.C ((∏ r : Fin n, ((Nat.factorial (K i r).val : ℕ) : ℚ))⁻¹)))) *976        (PowerSeries.C (∏ i : Fin n, ∏ r : Fin n, (adamsCoef (i.val + 1)977        (lawCoef (stateLaw (State.single a (r.val + 1))))) ^ (K i r).val) *978        (PowerSeries.X : Ser) ^ (∑ i : Fin n, (i.val + 1) * ∑ r : Fin n, (r.val + 1) *979        (K i r).val))) = patternSum ε a n n := by980  rw [map_sum]981  simp_rw [← mul_assoc, ← map_mul, PowerSeries.coeff_C_mul_X_pow]982  rw [← Finset.sum_filter, patternSum]983  refine Finset.sum_equiv (Equiv.curry _ _ _).symm ?_ ?_984  · intro K985    simp only [Finset.mem_filter, Finset.mem_univ, true_and, patternWeight, Equiv.curry_symm_apply,986      Function.uncurry_apply_pair, Fintype.sum_prod_type, Finset.mul_sum]987    have e : (∑ x : Fin n, ∑ i : Fin n, (x.val + 1) * ((i.val + 1) * (K x i).val))988        = ∑ x : Fin n, ∑ i : Fin n, (x.val + 1) * (i.val + 1) * (K x i).val :=989      Finset.sum_congr rfl fun _ _ ↦ Finset.sum_congr rfl fun _ _ ↦ by ring990    rw [e]; exact eq_comm991  · intro K _992    rw [scalar_mul_eq_smul, rational_divisorCount]993    simp only [Equiv.curry_symm_apply, Function.uncurry_apply_pair, Fintype.prod_prod_type, one_div]994 995/-- For a well-formed law, the `σ`-coefficient of `lawCoef L` is the rational function of996`lawCoeff L σ`. -/997theorem coeff_lawCoef (L : Law) (hL : LawWf L) (σ : FactorType) :998    (lawCoef L).coeff σ = (lawCoeff L σ).rational := by999  have hw : ∀ z ∈ L.map (fun z ↦ if z.1 = σ then z.2 else Expr.const 0), z.wf := by1000    intro e he1001    obtain ⟨z, hz, rfl⟩ := List.mem_map.mp he1002    by_cases h : z.1 = σ1003    · simp only [h, if_true]; exact hL z hz1004    · simp only [h, if_false]; simp [Expr.wf]1005  unfold lawCoeff1006  rw [(Expr.rational_sum) hw]1007  clear hw1008  induction L with1009  | nil => simp [lawCoef]1010  | cons z L ih =>1011    have := ih (fun w hw ↦ hL w (List.mem_cons_of_mem _ hw))1012    simp only [lawCoef, List.map_cons, List.sum_cons] at this ⊢1013    rw [AddMonoidAlgebra.coeff_add, Finsupp.add_apply, this]1014    congr 11015    by_cases h : z.1 = σ1016    · subst h; simp [AddMonoidAlgebra.coeff_single]1017    · simp only [h, if_false]1018      rw [(Expr.rational_const 0)]1019      simp [AddMonoidAlgebra.coeff_single, h]1020 1021/-- Safe laws are well formed. -/1022theorem LawSafe.lawWf {L : Law} (h : LawSafe L) : LawWf L :=1023  fun z hz ↦ Expr.wf_of_safe _ 2 (h z hz 2 le_rfl)1024 1025/-- The `σ`-coefficient of a well-formed law is well formed. -/1026theorem LawWf.wf_lawCoeff {L : Law} (h : LawWf L) (σ : FactorType) : (lawCoeff L σ).wf := by1027  unfold lawCoeff1028  refine Expr.wf_sum fun x hx ↦ ?_1029  obtain ⟨z, hz, rfl⟩ := List.mem_map.1 hx1030  split_ifs1031  · exact h z hz1032  · trivial1033 1034end SurfaceBlowup