Reciprocity: definitions and basic lemmas

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.Basic7import Mathlib.FieldTheory.RatFunc.AsPolynomial8import Mathlib.RingTheory.PowerSeries.Expand9import Mathlib.RingTheory.PowerSeries.Log10 11/-!12# Reciprocity: definitions and basic lemmas13 14The algebraic setting of the reciprocity argument. Over the coefficient ring15`Coef = ℚ(q)[Z_{e,f}]` we define the substitutions `q ↦ q⁻¹` (`recipRat`, `recipCoef`) and the16Adams operations `ψ_δ` (`adamsRat`, `adamsCoef`, `adamsSer`), power series in the cluster variable17`x` (`Ser`) with their exponential, logarithm, plethystic exponential/logarithm, dilations and18congruences, and the quantum-torus side: contact series `QSer` with the twisted product `qmul`,19the embeddings `ι₊`, `ι₋`, the diagonal substitution `qdiag`, and the representation `qact`.20We then prove the first algebraic properties of these objects.21 22## Main results23 24* `adamsRat_recipRat`, `adamsRat_adamsRat`, `coeff_adamsSer`: the Adams substitutions.25* `derivative_expSer`, `mul_derivative_logSer`, `coeff_expSer_sub_of_scongr`: `exp` and `log`.26* `qact_qmul`, `qplus_qmul`, `qminus_qmul`, `qone_qmul`: the twisted product and its27  representation.28* `qmul_qplus_qdiag_qminus_apply`: the triple-sum expansion of `ι₊(A) qdiag(D) ι₋(C)`.29* `qcongr_qplus_qone`, `qcongr_qminus_qone`: `ι₊`, `ι₋` of positive series close to `1`.30 31Provenance: `Def_SurfaceBlowupV2_{RecipRational,RecipCoef,RecipSeries,RecipQuantum}`,32`Thm_SurfaceBlowupV2_recip_{adamsRat_apply, adamsSer_hom, adamsSer_cluster_trunc,33binomial_series_ode, crossing_pattern_reindex, crossing_weight_identity, expSer_basic,34gauss_exponents, logSer_basic, pattern_entry_bound, power_coeff_multinomial, qact_congr,35qact_gaussPhi_coeff, qact_leading, qact_mul, qact_one_linear, qcongr_basic, qdiag_degree,36qminus_mul, qmul_one, qmul_plus_diag_minus_expand, qplus_degree, scongr_exp_log_lead}`.37-/38 39noncomputable section40 41namespace SurfaceBlowup42 43/-! ### Definitions -/44 45namespace Expr46/-- Rational well-formedness: every inverted subexpression has a nonzero numerator polynomial, so47that `Expr.rational` is a ring homomorphism on the expression (its unreduced denominators never48vanish). -/49def wf : Expr → Prop50  | .const _ => True51  | .var => True52  | .add x y => wf x ∧ wf y53  | .mul x y => wf x ∧ wf y54  | .inv x => wf x ∧ x.fraction.1 ≠ 055end Expr56/-- Polynomials evaluated at X⁻¹ in ℚ(X). -/57def recipPoly : Polynomial ℚ →+* RatFunc ℚ :=58  Polynomial.eval₂RingHom (RatFunc.C : ℚ →+* RatFunc ℚ) (RatFunc.X)⁻¹59/-- Polynomials evaluated at X^δ in ℚ(X). -/60private def adamsPoly (δ : ℕ) : Polynomial ℚ →+* RatFunc ℚ :=61  Polynomial.eval₂RingHom (RatFunc.C : ℚ →+* RatFunc ℚ) (RatFunc.X ^ δ)62/-- Evaluating a polynomial at `X` in `ℚ(X)` is the canonical embedding. -/63theorem eval₂_C_X_eq_algebraMap (g : Polynomial ℚ) :64    Polynomial.eval₂ (RatFunc.C : ℚ →+* RatFunc ℚ) (RatFunc.X : RatFunc ℚ) g =65      algebraMap (Polynomial ℚ) (RatFunc ℚ) g := by66  induction g using Polynomial.induction_on' with67  | add p q hp hq => simp [hp, hq]68  | monomial n a => simp [RatFunc.algebraMap_monomial]69/-- A nonzero polynomial stays nonzero after the substitution `X ↦ X⁻¹`. -/70private theorem recipPoly_ne_zero (p : Polynomial ℚ) (hp : p ≠ 0) : recipPoly p ≠ 0 := by71  let _ : Invertible (RatFunc.X : RatFunc ℚ) := invertibleOfNonzero RatFunc.X_ne_zero72  have key := Polynomial.eval₂_reflect_eq_zero_iff (RatFunc.C : ℚ →+* RatFunc ℚ)73    (RatFunc.X : RatFunc ℚ) p.natDegree (p.reflect p.natDegree)74    (by simpa using Polynomial.natDegree_reflect_le (N := p.natDegree) (p := p))75  rw [Polynomial.reflect_reflect, invOf_eq_inv] at key76  intro h77  have h3 := key.mp h78  rw [eval₂_C_X_eq_algebraMap] at h379  exact hp (Polynomial.reflect_eq_zero_iff.mp80    (not_not.1 fun hne ↦ RatFunc.algebraMap_ne_zero hne h3))81/-- `recipPoly` is injective. -/82private theorem recipPoly_injective : Function.Injective recipPoly :=83  (injective_iff_map_eq_zero _).2 fun p hp ↦ not_not.1 fun hne ↦ recipPoly_ne_zero p hne hp84/-- A nonzero polynomial stays nonzero after the substitution `X ↦ X^δ`, `δ > 0`. -/85private theorem adamsPoly_ne_zero (δ : ℕ) (hδ : 0 < δ) (p : Polynomial ℚ) (hp : p ≠ 0) :86    adamsPoly δ p ≠ 0 := by87  intro h88  have h2 : Polynomial.eval₂ (RatFunc.C : ℚ →+* RatFunc ℚ) (RatFunc.X : RatFunc ℚ)89      ((Polynomial.X : Polynomial ℚ) ^ δ) = (RatFunc.X : RatFunc ℚ) ^ δ := by simp90  change Polynomial.eval₂ _ ((RatFunc.X : RatFunc ℚ) ^ δ) p = 0 at h91  rw [← h2, ← Polynomial.eval₂_comp, eval₂_C_X_eq_algebraMap] at h92  rcases Polynomial.comp_eq_zero_iff.mp93      (not_not.1 fun hne ↦ RatFunc.algebraMap_ne_zero hne h) with h4 | ⟨_, h5⟩94  · exact hp h495  · have h6 := congrArg Polynomial.natDegree h596    rw [Polynomial.natDegree_X_pow, Polynomial.natDegree_C] at h697    omega98/-- `adamsPoly δ` is injective for `δ > 0`. -/99private theorem adamsPoly_injective (δ : ℕ) (hδ : 0 < δ) : Function.Injective (adamsPoly δ) :=100  (injective_iff_map_eq_zero _).2 fun p hp ↦ not_not.1 fun hne ↦ adamsPoly_ne_zero δ hδ p hne hp101/-- The automorphism q ↦ q⁻¹ of ℚ(X) (reciprocal substitution, the proof's `v`). -/102def recipRat : RatFunc ℚ →+* RatFunc ℚ :=103  RatFunc.liftRingHom recipPoly104    (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective recipPoly recipPoly_injective)105/-- The Adams substitution q ↦ q^δ on ℚ(X) (δ > 0; the identity for δ = 0, never used). -/106def adamsRat (δ : ℕ) : RatFunc ℚ →+* RatFunc ℚ :=107  if hδ : 0 < δ then108    RatFunc.liftRingHom (adamsPoly δ)109      (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective (adamsPoly δ)110        (adamsPoly_injective δ hδ))111  else RingHom.id (RatFunc ℚ)112 113/-- The coefficient algebra ℚ(q)[Z_{e,f}]: finitely supported functions on types, multiplied by114adding the multisets (the product of Z-monomials). A law becomes an element of this commutative115ring. -/116abbrev Coef := AddMonoidAlgebra (RatFunc ℚ) FactorTypeType variables Z_{e,f}117/-- The scalar embedding ℚ(q) → Coef (the empty type is the monomial 1). -/118def scalar (f : RatFunc ℚ) : Coef := AddMonoidAlgebra.single 0 f119/-- q^k for an integer k, as a scalar of Coef. -/120def qpow (k : ℤ) : Coef := scalar (RatFunc.X ^ k)121/-- A law as an element of Coef: the sum over its entries of (rational value) · Z^{type}. -/122def lawCoef (L : Law) : Coef := (L.map fun z ↦ AddMonoidAlgebra.single z.1 z.2.rational).sumType variables Z_{e,f}123/-- scaleType δ as an additive monoid homomorphism of types (multisets add). -/124def scaleTypeHom (δ : ℕ) : FactorType →+ FactorType where125  toFun := scaleType δ126  map_zero' := by simp [scaleType]127  map_add' := fun σ τ ↦ by simp [scaleType, Multiset.map_add]128/-- The Adams operation ψ_δ on Coef: q ↦ q^δ on every coefficient and Z_{e,f} ↦ Z_{e,δf} on129types. -/130def adamsCoef (δ : ℕ) : Coef →+* Coef :=(6.4)131  (AddMonoidAlgebra.mapDomainRingHom (RatFunc ℚ) (scaleTypeHom δ)).comp132    (AddMonoidAlgebra.mapRingHom FactorType (adamsRat δ))133/-- Reciprocal substitution v on Coef: q ↦ q⁻¹ on every coefficient, types unchanged. -/134def recipCoef : Coef →+* Coef := AddMonoidAlgebra.mapRingHom FactorType recipRat135/-- Every entry of the law is a well-formed expression. -/136def LawWf (L : Law) : Prop := ∀ z ∈ L, z.2.wf137 138/-- Series in the cluster-degree variable x with coefficients in Coef. -/139abbrev Ser := PowerSeries Coef(7.5)140/-- Agreement of two series in every degree ≤ n (congruence modulo x^{n+1}). -/141def SCongr (n : ℕ) (f g : Ser) : Prop :=142  ∀ m : ℕ, m ≤ n → PowerSeries.coeff m f = PowerSeries.coeff m g143/-- The Adams operation ψ_k on series: ψ_k on every coefficient and x ↦ x^k (zero for k = 0,144never used). -/145def adamsSer (k : ℕ) (f : Ser) : Ser :=146  if hk : k = 0 then 0 else PowerSeries.expand k hk (PowerSeries.map (adamsCoef k) f)147/-- Σ_{k ≥ 1} ψ_k(f)/k, coefficientwise finite: the coefficient of xⁿ is148Σ_{k ∣ n} (1/k) ψ_k(f_{n/k}). -/149def plethSum (f : Ser) : Ser :=150  PowerSeries.mk fun n ↦ ∑ k ∈ n.divisors, ((k : ℚ)⁻¹) • adamsCoef k (PowerSeries.coeff (n / k) f)151/-- Σ_{k ≥ 1} μ(k) ψ_k(g)/k, coefficientwise finite. -/152def moebiusSum (g : Ser) : Ser :=153  PowerSeries.mk fun n ↦ ∑ k ∈ n.divisors,154    ((((ArithmeticFunction.moebius k : ℤ) : ℚ)) / (k : ℚ)) •155      adamsCoef k (PowerSeries.coeff (n / k) g)156/-- Σ_{m ≥ 1} C_m ψ_m(L) with C_m = availablePoints ε m: the coefficient of xⁿ is157Σ_{m ∣ n} C_m ψ_m(L_{n/m}). -/158def countSum (ε : ℤ) (L : Ser) : Ser :=159  PowerSeries.mk fun n ↦ ∑ m ∈ n.divisors,160    (availablePoints ε m).rational • adamsCoef m (PowerSeries.coeff (n / m) L)161/-- Ordinary exponential of a series with zero constant term (composition with Σ xⁿ/n!). -/162def expSer (f : Ser) : Ser := (PowerSeries.exp Coef).subst f163/-- Ordinary logarithm of a series with constant term one. -/164def logSer (g : Ser) : Ser := PowerSeries.logOf g165/-- The formal power g^c = exp(c · log g) for a scalar exponent c ∈ ℚ(q). -/166def formalPow (c : RatFunc ℚ) (g : Ser) : Ser := expSer (PowerSeries.C (scalar c) * logSer g)167/-- Plethystic exponential Exp f = exp(Σ_k ψ_k(f)/k). -/168def pExp (f : Ser) : Ser := expSer (plethSum f)(7.6)169/-- Plethystic logarithm Log g = Σ_k μ(k) ψ_k(log g)/k. -/170def pLog (g : Ser) : Ser := moebiusSum (logSer g)(7.6)171/-- The plethystic power P_w(g) = Exp(w · Log g) for a scalar w ∈ ℚ(q). -/172def pPow (w : RatFunc ℚ) (g : Ser) : Ser := pExp (PowerSeries.C (scalar w) * pLog g)Pow_v and the first-difference rule173/-- Reciprocal substitution on every coefficient of a series (the proof's f ↦ f^v). -/174def recipSer (f : Ser) : Ser := PowerSeries.map recipCoef f175/-- Dilation S: x ↦ qx. -/176def dilate (f : Ser) : Ser := PowerSeries.rescale (scalar RatFunc.X) f177/-- Inverse dilation S⁻¹: x ↦ x/q. -/178def codilate (f : Ser) : Ser := PowerSeries.rescale (scalar RatFunc.X⁻¹) f179/-- The cluster series B_a = 1 + Σ_{n ≥ 1} F_{S(a;n)} xⁿ of vertical multiplicity a. -/180def clusterSer (a : ℕ) : Ser :=(7.5)181  PowerSeries.mk fun n ↦ if n = 0 then 1 else lawCoef (stateLaw (State.single a n))182/-- The Euler transform P_{q+ε}(B_a) with q + ε rational points: G_a (ε = 0), P_a (ε = −1),183Q_a (ε = 1). -/184def eulerSer (ε : ℤ) (a : ℕ) : Ser := pPow (RatFunc.X + (ε : RatFunc ℚ)) (clusterSer a)lem-7.2(7.10)185/-- The off-boundary pattern sum of weight w in ambient dimension N for vertical multiplicity a and186offset ε:187Σ over patterns m of weight w of divisorCount ε m · Π_{(i,j)} ψ_{i+1}(F_{S(a;j+1)})^{m(i,j)}. -/188def patternSum (ε : ℤ) (a N w : ℕ) : Coef :=lem-7.2189  ∑ m ∈ (Finset.univ : Finset (Pattern N)).filter (fun m ↦ patternWeight m = w),190    (divisorCount ε m).rational • ∏ ij : Fin N × Fin N,191      (adamsCoef (ij.1.val + 1) (lawCoef (stateLaw (State.single a (ij.2.val + 1))))) ^ (m ij).val192 193/-- Contact series: coefficient functions on contact pairs (c,h), i.e. Σ U(c,h) E_{c,h} in the194normal basis. -/195abbrev QSer := ℕ → ℕ → Coef(8.1)196/-- The twisted product E_{c,h} E_{d,k} = q^{-ck} E_{c+d,h+k}, as a finite convolution. -/197def qmul (U V : QSer) : QSer := fun c h ↦(8.1)198  ∑ p ∈ Finset.HasAntidiagonal.antidiagonal c, ∑ r ∈ Finset.HasAntidiagonal.antidiagonal h,199    qpow (-((p.1 : ℤ) * (r.2 : ℤ))) * (U p.1 r.1 * V p.2 r.2)200/-- The unit E_{0,0}. -/201def qone : QSer := fun c h ↦ if c = 0 ∧ h = 0 then 1 else 0(8.1)202/-- Reciprocal substitution on every coefficient (the proof's V^v). -/203def qrecip (U : QSer) : QSer := fun c h ↦ recipCoef (U c h)204/-- The anti-involution †: (f E_{c,h})† = v(f) q^{c+h−ch} E_{c,h}. -/205def qdagger (U : QSer) : QSer := fun c h ↦(8.2)206  qpow ((c : ℤ) + (h : ℤ) - (c : ℤ) * (h : ℤ)) * recipCoef (U c h)207/-- ι₊: E_{c,h} ↦ q^{-C(c,2)} E_{c,c+h}. -/208def qplus (U : QSer) : QSer := fun c k ↦Lemma 8.1209  if c ≤ k then qpow (-(chooseTwo c : ℤ)) * U c (k - c) else 0210/-- ι₋: E_{c,h} ↦ q^{-C(h,2)} E_{c+h,h}. -/211def qminus (U : QSer) : QSer := fun k h ↦Lemma 8.1212  if h ≤ k then qpow (-(chooseTwo h : ℤ)) * U (k - h) h else 0213/-- Diagonal substitution x ↦ J = E_{1,1}: Σ aₘ xᵐ ↦ Σ aₘ Jᵐ with Jᵐ = q^{-C(m,2)} E_{m,m}. -/214def qdiag (f : Ser) : QSer := fun c h ↦215  if c = h then qpow (-(chooseTwo c : ℤ)) * PowerSeries.coeff c f else 0216/-- U_{a,b} = 1 + (q−1) Σ_{c,h ≥ 1} F_{T(a,b;c,h)} E_{c,h}; zero on the two axes. -/217def crossingQ (a b : ℕ) : QSer := fun c h ↦(7.5)(8.2)218  if c = 0 ∧ h = 0 then 1219  else if 0 < c ∧ 0 < h then scalar (RatFunc.X - 1) * lawCoef (stateLaw (State.crossing a b c h))220  else 0221/-- Agreement through total contact degree j. -/222def QCongr (j : ℕ) (U V : QSer) : Prop := ∀ c h : ℕ, c + h ≤ j → U c h = V c h223/-- Vanishing on the two axes away from the constant term (support in the positive quadrant plus224`(0,0)`). -/225def QPositive (U : QSer) : Prop := ∀ c h : ℕ, (c = 0 ∨ h = 0) → ¬ (c = 0 ∧ h = 0) → U c h = 0226/-- The representation ρ: ρ(E_{c,h}) f = q^{-tri c} x^{c+h} f(x/q^c); coefficient n sums over227(c+h) + m = n. -/228def qact (U : QSer) (f : Ser) : Ser := PowerSeries.mk fun n ↦(8.9)229  ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, ∑ r ∈ Finset.HasAntidiagonal.antidiagonal p.1,230    qpow (-(tri r.1 : ℤ) - (r.1 : ℤ) * (p.2 : ℤ)) * (U r.1 r.2 * PowerSeries.coeff p.2 f)231/-- The same representation with q replaced by q⁻¹ (all Gaussian exponents negated). -/232def qactRecip (U : QSer) (f : Ser) : Ser := PowerSeries.mk fun n ↦Lemma 9.1233  ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, ∑ r ∈ Finset.HasAntidiagonal.antidiagonal p.1,234    qpow ((tri r.1 : ℤ) + (r.1 : ℤ) * (p.2 : ℤ)) * (U r.1 r.2 * PowerSeries.coeff p.2 f)235/-- Φ: xᵐ ↦ q^{-tri m} xᵐ. -/236def gaussPhi (f : Ser) : Ser := PowerSeries.mk fun n ↦ qpow (-(tri n : ℤ)) * PowerSeries.coeff n f(7.10)237/-- Φ⁻¹: xᵐ ↦ q^{tri m} xᵐ. -/238def gaussPhiInv (f : Ser) : Ser := PowerSeries.mk fun n ↦ qpow (tri n : ℤ) * PowerSeries.coeff n f239 240/-! ### Gaussian exponents and `qpow` -/241 242/-- `2 · tri n = n(n+1)`, as integers. -/243theorem two_mul_tri (n : ℕ) : 2 * (tri n : ℤ) = n * (n + 1) := by244  have : 2 * tri n = n * (n + 1) := by245    unfold tri; exact Nat.two_mul_div_two_of_even (Nat.even_mul_succ_self n)246  exact_mod_cast this247 248/-- `2 · C(n,2) = n(n-1)`, as integers. -/249theorem two_mul_chooseTwo (n : ℕ) : 2 * (chooseTwo n : ℤ) = n * (n - 1) := by250  have h : 2 * chooseTwo n = n * (n - 1) := by251    unfold chooseTwo; exact Nat.two_mul_div_two_of_even (Nat.even_mul_pred_self n)252  rcases n with _ | n253  · simp [chooseTwo]254  · have h' : (2 * chooseTwo (n + 1) : ℤ) = (n + 1) * n := by exact_mod_cast h255    rw [h']; push_cast; ring256 257/-- Additivity defect of the triangular numbers: `tri (r + m) = tri r + r m + tri m`. -/258private theorem tri_add (r m : ℕ) : (tri (r + m) : ℤ) = tri r + r * m + tri m := by259  have := two_mul_tri (r + m); have := two_mul_tri r; have := two_mul_tri m260  push_cast at *; linarith261 262/-- Additivity defect of `C(·,2)`: `C(r + s, 2) = C(r,2) + C(s,2) + r s`. -/263theorem chooseTwo_add (r s : ℕ) :264    (chooseTwo (r + s) : ℤ) = chooseTwo r + chooseTwo s + r * s := by265  have := two_mul_chooseTwo (r + s); have := two_mul_chooseTwo r; have := two_mul_chooseTwo s266  push_cast at *; linarith267 268/-- `q^{j+k} = q^j q^k` in `Coef`. -/269theorem qpow_add (j k : ℤ) : qpow (j + k) = qpow j * qpow k := by270  simp [qpow, scalar, AddMonoidAlgebra.single_mul_single, zpow_add₀ (RatFunc.X_ne_zero (K := ℚ))]271 272/-- `q^0 = 1` in `Coef`. -/273theorem qpow_zero : qpow 0 = 1 := by simp [qpow, scalar, AddMonoidAlgebra.one_def]274 275/-! ### The substitutions `q ↦ q^δ` and `q ↦ q⁻¹` on `ℚ(q)` -/276 277/-- `adamsRat δ` (`δ > 0`) extends `adamsPoly δ`. -/278private theorem adamsRat_algebraMap (δ : ℕ) (hδ : 0 < δ) (g : Polynomial ℚ) :279    adamsRat δ (algebraMap (Polynomial ℚ) (RatFunc ℚ) g) = adamsPoly δ g := by280  unfold adamsRat; rw [dif_pos hδ]; simp281 282/-- `recipRat` extends `recipPoly`. -/283theorem recipRat_algebraMap (g : Polynomial ℚ) :284    recipRat (algebraMap (Polynomial ℚ) (RatFunc ℚ) g) = recipPoly g := by285  simp [recipRat]286 287/-- `recipRat` fixes the constants. -/288theorem recipRat_C (r : ℚ) : recipRat (RatFunc.C r) = RatFunc.C r := by289  rw [← RatFunc.algebraMap_C, recipRat_algebraMap]; simp [recipPoly]290 291/-- `adamsRat δ q = q^δ` for `δ > 0`. -/292theorem adamsRat_X (δ : ℕ) (hδ : 0 < δ) : adamsRat δ RatFunc.X = RatFunc.X ^ δ := by293  rw [← RatFunc.algebraMap_X, adamsRat_algebraMap δ hδ]; simp [adamsPoly]294 295/-- `recipRat q = q⁻¹`. -/296theorem recipRat_X : recipRat RatFunc.X = RatFunc.X⁻¹ := by297  rw [← RatFunc.algebraMap_X, recipRat_algebraMap]; simp [recipPoly]298 299private theorem ratFunc_ringHom_ext (φ ψ : RatFunc ℚ →+* RatFunc ℚ)300    (h : ∀ g : Polynomial ℚ, φ (algebraMap (Polynomial ℚ) (RatFunc ℚ) g)301      = ψ (algebraMap (Polynomial ℚ) (RatFunc ℚ) g)) : φ = ψ := by302  ext f303  rw [← RatFunc.num_div_denom f, map_div₀, map_div₀, h, h]304 305private theorem ringHom_eval₂ (φ : RatFunc ℚ →+* RatFunc ℚ) (g : Polynomial ℚ) (a : RatFunc ℚ) :306    φ (g.eval₂ RatFunc.C a) = g.eval₂ RatFunc.C (φ a) := by307  rw [Polynomial.hom_eval₂]308  congr 1309  ext r; simp310 311/-- The Adams substitution commutes with `q ↦ q⁻¹`. -/312theorem adamsRat_recipRat (δ : ℕ) (hδ : 0 < δ) (f : RatFunc ℚ) :313    adamsRat δ (recipRat f) = recipRat (adamsRat δ f) := by314  refine DFunLike.congr_fun (ratFunc_ringHom_ext ((adamsRat δ).comp recipRat)315    (recipRat.comp (adamsRat δ)) fun g ↦ ?_) f316  simp only [RingHom.comp_apply]317  rw [recipRat_algebraMap, adamsRat_algebraMap δ hδ]318  change adamsRat δ (g.eval₂ RatFunc.C (RatFunc.X)⁻¹) = recipRat (g.eval₂ RatFunc.C (RatFunc.X ^ δ))319  rw [ringHom_eval₂, ringHom_eval₂, map_inv₀, map_pow, adamsRat_X δ hδ, recipRat_X, inv_pow]320 321/-- `ψ_δ ∘ ψ_k = ψ_{δk}` on `ℚ(q)`. -/322theorem adamsRat_adamsRat (δ k : ℕ) (hδ : 0 < δ) (hk : 0 < k) (f : RatFunc ℚ) :323    adamsRat δ (adamsRat k f) = adamsRat (δ * k) f := by324  refine DFunLike.congr_fun (ratFunc_ringHom_ext ((adamsRat δ).comp (adamsRat k))325    (adamsRat (δ * k)) fun g ↦ ?_) f326  simp only [RingHom.comp_apply]327  rw [adamsRat_algebraMap k hk, adamsRat_algebraMap (δ * k) (Nat.mul_pos hδ hk)]328  change adamsRat δ (g.eval₂ RatFunc.C (RatFunc.X ^ k)) = g.eval₂ RatFunc.C (RatFunc.X ^ (δ * k))329  rw [ringHom_eval₂, map_pow, adamsRat_X δ hδ, pow_mul]330 331/-- `ψ_1` is the identity of `ℚ(q)`. -/332theorem adamsRat_one (f : RatFunc ℚ) : adamsRat 1 f = f := by333  refine DFunLike.congr_fun (ratFunc_ringHom_ext (adamsRat 1) (RingHom.id _) fun g ↦ ?_) f334  rw [adamsRat_algebraMap 1 one_pos]335  change g.eval₂ RatFunc.C (RatFunc.X ^ 1) = _336  rw [pow_one, eval₂_C_X_eq_algebraMap]; rfl337 338/-- `ψ_δ (q^j) = q^{δj}` for integer `j`. -/339theorem adamsRat_zpow_X (δ : ℕ) (hδ : 0 < δ) (j : ℤ) :340    adamsRat δ ((RatFunc.X : RatFunc ℚ) ^ j) = (RatFunc.X : RatFunc ℚ) ^ ((δ : ℤ) * j) := by341  rw [map_zpow₀, adamsRat_X δ hδ, ← zpow_natCast, ← zpow_mul]342 343/-! ### Adams operations on series -/344 345/-- `[xⁿ] ψ_k f = ψ_k([x^{n/k}] f)` if `k ∣ n`, and `0` otherwise (`k ≠ 0`). -/346theorem coeff_adamsSer (k : ℕ) (hk : k ≠ 0) (f : Ser) (n : ℕ) :347    PowerSeries.coeff n (adamsSer k f) =348      if k ∣ n then adamsCoef k (PowerSeries.coeff (n / k) f) else 0 := by349  simp only [adamsSer, dif_neg hk, PowerSeries.coeff_expand, PowerSeries.coeff_map]350 351/-- The constant term of `ψ_k f` is `ψ_k` of the constant term of `f` (`k ≠ 0`). -/352theorem constantCoeff_adamsSer (k : ℕ) (hk : k ≠ 0) (f : Ser) :353    PowerSeries.constantCoeff (adamsSer k f) = adamsCoef k (PowerSeries.constantCoeff f) := by354  rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply, coeff_adamsSer k hk]; simp355 356/-- `ψ_k 1 = 1` (`k ≠ 0`). -/357theorem adamsSer_one (k : ℕ) (hk : k ≠ 0) : adamsSer k (1 : Ser) = 1 := by358  simp [adamsSer, dif_neg hk]359 360/-- `ψ_k` on series is additive on differences (`k ≠ 0`). -/361theorem adamsSer_sub (k : ℕ) (hk : k ≠ 0) (f g : Ser) :362    adamsSer k (f - g) = adamsSer k f - adamsSer k g := by363  simp [adamsSer, dif_neg hk]364 365/-- Through degree `n`, `ψ_m(B_a) - 1` is the finite sum366`Σ_{r < n} ψ_m(F_{S(a;r+1)}) x^{m(r+1)}`. -/367theorem adamsSer_clusterSer_sub_one_scongr (a m n : ℕ) (hm : 0 < m) :368    SCongr n (adamsSer m (clusterSer a) - 1)369      (∑ r : Fin n, PowerSeries.C (adamsCoef m (lawCoef (stateLaw (State.single a (r.val + 1))))) *370        (PowerSeries.X : Ser) ^ (m * (r.val + 1))) := by371  intro i hi372  rw [map_sub, coeff_adamsSer m hm.ne', map_sum]373  simp only [PowerSeries.coeff_C_mul_X_pow, PowerSeries.coeff_one]374  by_cases h0 : i = 0375  · subst h0376    have : ∀ r : Fin n, ¬ (0 = m * (r.val + 1)) := fun r ↦ (Nat.mul_pos hm r.val.succ_pos).ne377    simp [this, clusterSer]378  by_cases hd : m ∣ i379  · obtain ⟨s, rfl⟩ := hd380    have hs : 0 < s := Nat.pos_of_ne_zero (fun e ↦ h0 (by simp [e]))381    have hsn : s ≤ n := by nlinarith382    rw [Finset.sum_eq_single (⟨s - 1, by omega⟩ : Fin n)]383    · have e : s - 1 + 1 = s := by omega384      simp [h0, clusterSer, Nat.mul_div_cancel_left _ hm, hs.ne', e]385    · intro r _ hr386      rw [if_neg]387      intro hh388      exact hr (Fin.ext (by have := Nat.eq_of_mul_eq_mul_left hm hh; simp; omega))389    · simp390  · rw [if_neg hd, Finset.sum_eq_zero fun r _ ↦ if_neg fun h ↦ hd ⟨_, h⟩]391    simp [h0]392 393/-! ### Exponential, logarithm and binomial series -/394 395/-- The binomial series `Σ C(c,n) xⁿ` solves `(1 + x) y' = c y`. -/396theorem binomial_series_ode (c : RatFunc ℚ) :397    (1 + PowerSeries.X) * PowerSeries.derivative Coef (PowerSeries.mk fun n ↦398      ((n.factorial : ℚ)⁻¹) • ∏ j ∈ Finset.range n, (scalar c - (j : ℚ) • (1 : Coef))) =399    PowerSeries.C (scalar c) * PowerSeries.mk (fun n ↦400      ((n.factorial : ℚ)⁻¹) • ∏ j ∈ Finset.range n, (scalar c - (j : ℚ) • (1 : Coef))) := by401  set b : ℕ → Coef := fun n ↦402    ((n.factorial : ℚ)⁻¹) • ∏ j ∈ Finset.range n, (scalar c - (j : ℚ) • (1 : Coef)) with hb403  have key : ∀ n : ℕ, ((n + 1 : ℕ) : ℚ) • b (n + 1) = (scalar c - (n : ℚ) • (1 : Coef)) * b n := by404    intro n405    simp only [hb, Finset.prod_range_succ, smul_smul, Nat.factorial_succ, Nat.cast_mul]406    rw [mul_inv, ← mul_assoc, mul_inv_cancel₀ (by positivity), one_mul, mul_comm _ (scalar c - _),407      mul_smul_comm]408  have hd : ∀ m : ℕ, PowerSeries.coeff m (PowerSeries.derivative Coef (PowerSeries.mk b))409      = ((m + 1 : ℕ) : ℚ) • b (m + 1) := by410    intro m411    rw [PowerSeries.coeff_derivative, PowerSeries.coeff_mk, mul_comm, Nat.cast_smul_eq_nsmul,412      nsmul_eq_mul]413    push_cast; rfl414  refine PowerSeries.ext fun n ↦ ?_415  rw [PowerSeries.coeff_C_mul, PowerSeries.coeff_mk, add_mul, one_mul, map_add]416  rcases n with _ | n417  · rw [PowerSeries.coeff_zero_X_mul, add_zero, hd, key]418    simp [hb]419  · rw [PowerSeries.coeff_succ_X_mul, hd, hd, key, sub_mul, smul_mul_assoc, one_mul, sub_add_cancel]420 421/-- `exp f` has constant term `1` when `f(0) = 0`. -/422theorem constantCoeff_expSer (f : Ser) (hf : PowerSeries.constantCoeff f = 0) :423    PowerSeries.constantCoeff (expSer f) = 1 := by424  change MvPowerSeries.constantCoeff _ = 1425  rw [expSer, PowerSeries.constantCoeff_subst (PowerSeries.HasSubst.of_constantCoeff_zero' hf),426    finsum_eq_single _ 0]427  · simp [PowerSeries.coeff_exp]428    rfl429  · intro d hd430    have h0 : MvPowerSeries.constantCoeff f = 0 := hf431    simp [h0, zero_pow hd]432 433/-- The chain rule `(exp f)' = f' · exp f` (for `f(0) = 0`). -/434theorem derivative_expSer (f : Ser) (hf : PowerSeries.constantCoeff f = 0) :435    PowerSeries.derivative Coef (expSer f) = PowerSeries.derivative Coef f * expSer f := by436  rw [expSer, PowerSeries.derivative_subst (PowerSeries.HasSubst.of_constantCoeff_zero' hf),437    PowerSeries.derivative_exp, mul_comm]438 439/-- `exp 0 = 1`. -/440theorem expSer_zero : expSer (0 : Ser) = 1 := by441  rw [expSer, PowerSeries.subst_zero_eq_C_constantCoeff]442  ext n443  simp444 445/-- `log g` has constant term `0` when `g(0) = 1`. -/446theorem constantCoeff_logSer (g : Ser) (hg : PowerSeries.constantCoeff g = 1) :447    PowerSeries.constantCoeff (logSer g) = 0 :=448  PowerSeries.constantCoeff_logOf hg449 450/-- The logarithmic derivative `g · (log g)' = g'` (for `g(0) = 1`). -/451theorem mul_derivative_logSer (g : Ser) (hg : PowerSeries.constantCoeff g = 1) :452    g * PowerSeries.derivative Coef (logSer g) = PowerSeries.derivative Coef g := by453  have hs : PowerSeries.HasSubst (g - 1) :=454    PowerSeries.HasSubst.of_constantCoeff_zero' (by simp [hg])455  set G : Ser := PowerSeries.mk fun n ↦ algebraMap ℚ Coef ((-1 : ℚ) ^ n) with hG456  have hgeom : (1 + PowerSeries.X) * G = 1 := by457    refine PowerSeries.ext fun n ↦ ?_458    rw [add_mul, one_mul, map_add]459    rcases n with _ | n460    · simp [hG]; rfl461    · rw [PowerSeries.coeff_succ_X_mul]462      simp only [hG, PowerSeries.coeff_mk, PowerSeries.coeff_one]463      rw [← map_add, if_neg (Nat.succ_ne_zero n), pow_succ]464      simp465  have hsub : g * G.subst (g - 1) = 1 := by466    have := congrArg (fun f : Ser ↦ f.subst (g - 1)) hgeom467    rw [PowerSeries.subst_mul hs, PowerSeries.subst_add hs, PowerSeries.subst_X hs] at this468    have h1 : (1 : Ser).subst (g - 1) = (1 : Ser) := by469      rw [← map_one (PowerSeries.C (R := Coef)), PowerSeries.subst_C]; rfl470    rwa [h1, add_sub_cancel] at this471  rw [logSer, PowerSeries.logOf_eq, PowerSeries.derivative_subst hs, PowerSeries.deriv_log, ← hG,472    map_sub, PowerSeries.derivative_one, sub_zero, ← mul_assoc, hsub, one_mul]473 474private theorem coeff_pow_eq_of_scongr (n : ℕ) (hn : 0 < n) (f g : Ser)475    (hf : PowerSeries.constantCoeff f = 0) (hg : PowerSeries.constantCoeff g = 0)476    (h : SCongr (n - 1) f g) (d : ℕ) (hd : d ≠ 1) :477    PowerSeries.coeff n (f ^ d) = PowerSeries.coeff n (g ^ d) := by478  rcases d with _ | _ | k479  · simp [PowerSeries.coeff_one, hn.ne']480  · exact absurd rfl hd481  have htr : PowerSeries.trunc n f = PowerSeries.trunc n g := by482    refine Polynomial.ext fun m ↦ ?_483    simp only [PowerSeries.coeff_trunc]484    split_ifs with hm485    · exact h m (by omega)486    · rfl487  have hk : ∀ i, i ≤ n - 1 →488      PowerSeries.coeff i (f ^ (k + 1)) = PowerSeries.coeff i (g ^ (k + 1)) := by489    intro i hi490    have e : PowerSeries.trunc n (f ^ (k + 1)) = PowerSeries.trunc n (g ^ (k + 1)) := by491      rw [← PowerSeries.trunc_trunc_pow, htr, PowerSeries.trunc_trunc_pow]492    simpa only [PowerSeries.coeff_trunc, if_pos (show i < n by omega)] using493      congrArg (fun p ↦ Polynomial.coeff p i) e494  rw [pow_succ f, pow_succ g, PowerSeries.coeff_mul, PowerSeries.coeff_mul]495  refine Finset.sum_congr rfl fun p hp ↦ ?_496  rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp497  by_cases hj : p.2 = 0498  · simp [hj, hf, hg]499  by_cases hi : p.1 = 0500  · simp [hi, hf, hg]501  rw [hk p.1 (by omega), h p.2 (by omega)]502 503/-- The `n`-th coefficient of `P ∘ f` (for `f(0) = 0`) only involves the powers `f^d`, `d ≤ n`. -/504theorem coeff_subst_eq_sum (n : ℕ) (P f : Ser) (hf : PowerSeries.constantCoeff f = 0) :505    PowerSeries.coeff n (P.subst f) =506      ∑ d ∈ Finset.range (n + 1), PowerSeries.coeff d P • PowerSeries.coeff n (f ^ d) := by507  rw [PowerSeries.coeff_subst' (PowerSeries.HasSubst.of_constantCoeff_zero' hf)]508  refine finsum_eq_sum_of_support_subset _ fun d hd ↦ ?_509  simp only [Function.mem_support, Finset.coe_range, Set.mem_Iio] at hd ⊢510  by_contra hc511  refine hd ?_512  rw [PowerSeries.X_pow_dvd_iff.1 (pow_dvd_pow_of_dvd (PowerSeries.X_dvd_iff.2 hf) d) n513    (by omega), smul_zero]514 515private theorem coeff_subst_sub (n : ℕ) (hn : 0 < n) (P f g : Ser)516    (hf : PowerSeries.constantCoeff f = 0) (hg : PowerSeries.constantCoeff g = 0)517    (h : SCongr (n - 1) f g) :518    PowerSeries.coeff n (P.subst f) - PowerSeries.coeff n (P.subst g) =519      PowerSeries.coeff 1 P • (PowerSeries.coeff n f - PowerSeries.coeff n g) := by520  rw [coeff_subst_eq_sum n P f hf, coeff_subst_eq_sum n P g hg, ← Finset.sum_sub_distrib,521    Finset.sum_eq_single 1]522  · rw [pow_one, pow_one, smul_sub]523  · intro d _ hd524    rw [coeff_pow_eq_of_scongr n hn f g hf hg h d hd, sub_self]525  · intro h1; simp at h1; omega526 527/-- If `f ≡ g` through degree `n - 1`, then the degree-`n` discrepancy of `exp f` and `exp g`528equals that of `f` and `g`. -/529theorem coeff_expSer_sub_of_scongr (n : ℕ) (hn : 0 < n) (f g : Ser)530    (hf : PowerSeries.constantCoeff f = 0) (hg : PowerSeries.constantCoeff g = 0)531    (h : SCongr (n - 1) f g) :532    PowerSeries.coeff n (expSer f) - PowerSeries.coeff n (expSer g) =533      PowerSeries.coeff n f - PowerSeries.coeff n g := by534  rw [expSer, expSer, coeff_subst_sub n hn _ f g hf hg h, PowerSeries.coeff_exp]535  simp only [Nat.factorial_one, Nat.cast_one, div_one, map_one, one_smul]536 537/-- If `u ≡ v` through degree `n - 1`, then the degree-`n` discrepancy of `log u` and `log v`538equals that of `u` and `v`. -/539theorem coeff_logSer_sub_of_scongr (n : ℕ) (hn : 0 < n) (u v : Ser)540    (hu : PowerSeries.constantCoeff u = 1) (hv : PowerSeries.constantCoeff v = 1)541    (huv : SCongr (n - 1) u v) :542    PowerSeries.coeff n (logSer u) - PowerSeries.coeff n (logSer v) =543      PowerSeries.coeff n u - PowerSeries.coeff n v := by544  rw [logSer, logSer, PowerSeries.logOf_eq, PowerSeries.logOf_eq,545    coeff_subst_sub n hn _ _ _ (by simp [hu]) (by simp [hv]) (fun m hm ↦ by simp [huv m hm]),546    PowerSeries.coeff_one_log, one_smul]547  simp [PowerSeries.coeff_one, hn.ne']548 549/-! ### Patterns and multinomials -/550 551/-- A sum over the allowed tangent patterns of a state `s` whose summand depends only on the data552`(d, rt, rx)` and the off-boundary pattern, reindexed by `d ∈ [1, D]`, `rt, rx ≤ d` and the553off-boundary patterns of weight `d - rt - rx`. Here `D` bounds the divisor degree and `Q` is the554boundary condition on `(d, rt, rx)` in the description `hmem` of the allowed patterns. -/555theorem sum_allowedPatterns_reindex (s : State) (D : ℕ) (hD : D ≤ s.degree)556    (Q : ℕ → ℕ → ℕ → Prop) [∀ d rt rx, Decidable (Q d rt rx)]557    (hmem : ∀ P, P ∈ allowedPatterns s ↔ 0 < P.d.val ∧558      P.rt.val + P.rx.val + patternWeight P.other = P.d.val ∧ P.d.val ≤ D ∧559      Q P.d.val P.rt.val P.rx.val)560    (F : ℕ → ℕ → ℕ → Pattern s.degree → Coef) :561    ∑ P ∈ allowedPatterns s, F P.d.val P.rt.val P.rx.val P.other =562    ∑ d ∈ Finset.Icc 1 D, ∑ rt ∈ Finset.range (d + 1), ∑ rx ∈ Finset.range (d + 1),563      (if Q d rt rx ∧ rt + rx ≤ d then564        ∑ m ∈ (Finset.univ : Finset (Pattern s.degree)).filter565          (fun m ↦ patternWeight m = d - rt - rx), F d rt rx m566      else 0) := by567  rw [← Finset.sum_fiberwise_of_maps_to (g := fun P ↦ P.d.val) (t := Finset.Icc 1 D)568    fun P hP ↦ by569      obtain ⟨h1, -, h3, -⟩ := (hmem P).1 hP570      simp only [Finset.mem_Icc]; omega]571  refine Finset.sum_congr rfl fun d hd ↦ ?_572  rw [← Finset.sum_product', ← Finset.sum_fiberwise_of_maps_to (g := fun P ↦ (P.rt.val, P.rx.val))573    (t := Finset.range (d + 1) ×ˢ Finset.range (d + 1)) fun P hP ↦ by574      obtain ⟨hP', rfl⟩ := Finset.mem_filter.1 hP575      obtain ⟨-, h2, -⟩ := (hmem P).1 hP'576      simp only [Finset.mem_product, Finset.mem_range]; omega]577  refine Finset.sum_congr rfl fun ⟨rt, rx⟩ hr ↦ ?_578  simp only [Finset.mem_Icc, Finset.mem_product, Finset.mem_range] at hd hr579  simp only [Finset.filter_filter, Prod.mk.injEq]580  split_ifs with hcond581  · refine Finset.sum_bij' (fun P _ ↦ P.other)582      (fun m _ ↦ ⟨⟨d, by omega⟩, ⟨rt, by omega⟩, ⟨rx, by omega⟩, m⟩) ?_ ?_ ?_ ?_ ?_583    · intro P hP584      obtain ⟨hP', rfl, rfl, rfl⟩ := Finset.mem_filter.1 hP585      obtain ⟨-, h2, -⟩ := (hmem P).1 hP'586      simp only [Finset.mem_filter, Finset.mem_univ, true_and]; omega587    · intro m hm588      simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hm589      exact Finset.mem_filter.2 ⟨(hmem _).2 ⟨by dsimp only; omega, by dsimp only; omega,590        by dsimp only; omega, hcond.1⟩, rfl, rfl, rfl⟩591    · rintro ⟨d', rt', rx', o⟩ hP592      obtain ⟨-, rfl, rfl, rfl⟩ := Finset.mem_filter.1 hP593      rfl594    · exact fun _ _ ↦ rfl595    · intro P hP596      obtain ⟨-, rfl, rfl, rfl⟩ := Finset.mem_filter.1 hP597      rfl598  · refine Finset.sum_eq_zero fun P hP ↦ (hcond ?_).elim599    obtain ⟨hP', rfl, rfl, rfl⟩ := Finset.mem_filter.1 hP600    obtain ⟨-, h2, -, h4⟩ := (hmem P).1 hP'601    exact ⟨h4, by omega⟩602 603/-- Reindexing the allowed patterns of the crossing state `T(a,b;c,h)` by their data604`(d, rt, rx)` and the off-boundary pattern of weight `d - rt - rx`. -/605theorem sum_allowedPatterns_crossing (a b c h : ℕ) (ha : 0 < a) (hb : 0 < b)606    (hh : 0 < h) (F : ℕ → ℕ → ℕ → Pattern (State.crossing a b c h).degree → Coef) :607    ∑ P ∈ allowedPatterns (State.crossing a b c h), F P.d.val P.rt.val P.rx.val P.other =608    ∑ d ∈ Finset.Icc 1 (min c h), ∑ rt ∈ Finset.range (d + 1), ∑ rx ∈ Finset.range (d + 1),609      (if ((0 < rt ↔ d < c) ∧ (0 < rx ↔ d < h) ∧ rt + rx ≤ d) then610        ∑ m ∈ (Finset.univ : Finset (Pattern (State.crossing a b c h).degree)).filter611          (fun m ↦ patternWeight m = d - rt - rx), F d rt rx m612      else 0) := by613  have hD : min c h ≤ (State.crossing a b c h).degree := by614    change min c h ≤ a * c + b * h615    have := min_le_left c h616    nlinarith617  rw [sum_allowedPatterns_reindex _ _ hD (fun d rt rx ↦ (0 < rt ↔ d < c) ∧ (0 < rx ↔ d < h))618    (fun P ↦ by simp [allowedPatterns, Allowed, and_assoc])]619  simp only [and_assoc]620 621/-- `q - 1 ≠ 0` in `ℚ(q)`. -/622private theorem X_sub_one_ne_zero : (RatFunc.X - 1 : RatFunc ℚ) ≠ 0 := by623  simpa using RatFunc.algebraMap_ne_zero (Polynomial.X_sub_C_ne_zero (1 : ℚ))624 625/-- `(q-1) · w_j = (q-1)^j` for the crossing weight `w_0 = (q-1)⁻¹`, `w_j = (q-1)^{j-1}`. -/626theorem X_sub_one_mul_crossingWeight (j : ℕ) :627    (RatFunc.X - 1) * (if j = 0 then (RatFunc.X - 1 : RatFunc ℚ)⁻¹ else (RatFunc.X - 1) ^ (j - 1))628      = (RatFunc.X - 1) ^ j := by629  rcases j with _ | k630  · simp [X_sub_one_ne_zero]631  · simp [pow_succ, mul_comm]632 633private theorem pattern_entry_mul_le (N : ℕ) (m : Pattern N) (ij : Fin N × Fin N) :634    (ij.1.val + 1) * (ij.2.val + 1) * (m ij).val ≤ patternWeight m :=635  Finset.single_le_sum (f := fun ij : Fin N × Fin N ↦ (ij.1.val+1)*(ij.2.val+1)*(m ij).val)636    (fun _ _ ↦ Nat.zero_le _) (Finset.mem_univ ij)637 638/-- Each entry of a pattern is bounded by its weight. -/639theorem pattern_entry_le_patternWeight (N : ℕ) (m : Pattern N) (ij : Fin N × Fin N) :640    (m ij).val ≤ patternWeight m :=641  le_trans (Nat.le_mul_of_pos_left _ (by positivity)) (pattern_entry_mul_le N m ij)642 643/-- An entry `m(i,j)` of a pattern of weight `< (i+1)(j+1)` vanishes. -/644theorem pattern_entry_eq_zero_of_lt (N : ℕ) (m : Pattern N) (ij : Fin N × Fin N)645    (h : patternWeight m < (ij.1.val + 1) * (ij.2.val + 1)) : (m ij).val = 0 := by646  have h1 := pattern_entry_mul_le N m ij647  by_contra hne648  have := Nat.le_mul_of_pos_right ((ij.1.val + 1) * (ij.2.val + 1)) (Nat.pos_of_ne_zero hne)649  omega650 651/-- Multinomial expansion of `(Σ_{r<n} b_{r+1} x^{m(r+1)})^k`. -/652theorem sum_C_mul_X_pow_pow (m n k : ℕ) (b : ℕ → Coef) :653    (∑ r : Fin n, PowerSeries.C (b (r.val + 1)) * (PowerSeries.X : Ser) ^ (m * (r.val + 1))) ^ k =654    ∑ κ ∈ Finset.piAntidiag (Finset.univ : Finset (Fin n)) k,655      PowerSeries.C ((Nat.multinomial Finset.univ κ : Coef) * ∏ r : Fin n, b (r.val + 1) ^ κ r) *656        (PowerSeries.X : Ser) ^ (m * ∑ r : Fin n, (r.val + 1) * κ r) := by657  rw [Finset.sum_pow_eq_sum_piAntidiag]658  refine Finset.sum_congr rfl fun κ _ ↦ ?_659  rw [Finset.prod_congr rfl (fun r _ ↦ mul_pow _ _ _), Finset.prod_mul_distrib]660  have h2 : ∏ r : Fin n, ((PowerSeries.X : Ser) ^ (m * (r.val + 1))) ^ κ r661      = (PowerSeries.X : Ser) ^ (m * ∑ r : Fin n, (r.val + 1) * κ r) := by662    rw [Finset.mul_sum, ← Finset.prod_pow_eq_pow_sum]663    exact Finset.prod_congr rfl fun r _ ↦ by rw [← pow_mul, mul_assoc]664  rw [h2]665  simp only [map_mul, map_natCast, map_prod, map_pow]666  ring667 668/-! ### The representation `qact` and the Gauss twist -/669 670/-- If `U ≡ V` through total degree `n`, then `ρ(U) f ≡ ρ(V) f` through degree `n`. -/671theorem QCongr.qact_scongr {n : ℕ} {U V : QSer} (hUV : QCongr n U V) (f : Ser) :672    SCongr n (qact U f) (qact V f) := fun m hm ↦ by673  simp only [qact, PowerSeries.coeff_mk]674  refine Finset.sum_congr rfl fun p hp ↦ Finset.sum_congr rfl fun r hr ↦ ?_675  rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp hr676  rw [hUV r.1 r.2 (by omega)]677 678/-- Coefficients of `ρ(U)(Φ f)` as a double sum over the total degree `d` and the first contact679index `r`. -/680theorem coeff_qact_gaussPhi (U : QSer) (f : Ser) (n : ℕ) :681    PowerSeries.coeff n (qact U (gaussPhi f)) = ∑ d ∈ Finset.range (n + 1),682      ∑ r ∈ Finset.range (d + 1),683        qpow (-(tri d : ℤ)) * (U r (n - d) * PowerSeries.coeff (d - r) f) := by684  simp only [qact, gaussPhi, PowerSeries.coeff_mk, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]685  have key : ∀ i r : ℕ, qpow (-(tri r : ℤ) - (r : ℤ) * ((n - i : ℕ) : ℤ)) *686      (U r (i - r) * (qpow (-(tri (n - i) : ℤ)) * PowerSeries.coeff (n - i) f)) =687      qpow (-(tri (r + (n - i)) : ℤ)) * (U r (i - r) * PowerSeries.coeff (n - i) f) := by688    intro i r689    rw [tri_add, mul_left_comm (U r (i - r)), ← mul_assoc, ← qpow_add]690    congr 2; ring691  simp only [key]692  rw [Finset.sum_sigma', Finset.sum_sigma']693  refine Finset.sum_bij' (fun x _ ↦ ⟨x.2 + (n - x.1), x.2⟩) (fun x _ ↦ ⟨n - (x.1 - x.2), x.2⟩)694    ?_ ?_ ?_ ?_ ?_695  all_goals rintro ⟨i, r⟩ h; simp only [Finset.mem_sigma, Finset.mem_range] at h696  · simp only [Finset.mem_sigma, Finset.mem_range]; omega697  · simp only [Finset.mem_sigma, Finset.mem_range]; omega698  · simp only [Sigma.mk.injEq, heq_eq_eq, and_true]; omega699  · simp only [Sigma.mk.injEq, heq_eq_eq, and_true]; omega700  · dsimp only701    rw [show n - (r + (n - i)) = i - r by omega, show r + (n - i) - r = n - i by omega]702 703/-- Leading term: if `f` vanishes below degree `n` and `U₀₀ = 1`, then704`[xⁿ] ρ(U)(Φ f) = q^{-tri n} [xⁿ] f`. -/705theorem coeff_qact_gaussPhi_of_lt (U : QSer) (hU0 : U 0 0 = 1) (f : Ser) (n : ℕ)(8.10)706    (hf : ∀ m : ℕ, m < n → PowerSeries.coeff m f = 0) :707    PowerSeries.coeff n (qact U (gaussPhi f)) = qpow (-(tri n : ℤ)) * PowerSeries.coeff n f := by708  rw [qact, gaussPhi, PowerSeries.coeff_mk, Finset.sum_eq_single (0, n)]709  · simp [PowerSeries.coeff_mk, show tri 0 = 0 from rfl, hU0, qpow_zero]710  · rintro ⟨a, b⟩ hp hne711    rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp712    have : b < n := by713      by_contra h714      exact hne (Prod.ext (by simp; omega) (by simp; omega))715    exact Finset.sum_eq_zero fun r _ ↦ by simp [PowerSeries.coeff_mk, hf _ this]716  · simp717 718/-- `ρ` is multiplicative: `ρ(U V) = ρ(U) ∘ ρ(V)`. -/719theorem qact_qmul (U V : QSer) (f : Ser) : qact (qmul U V) f = qact U (qact V f) := by720  refine PowerSeries.ext fun n ↦ ?_721  simp only [qact, qmul, PowerSeries.coeff_mk, Finset.mul_sum, Finset.sum_mul]722  simp_rw [Finset.sum_sigma']723  refine Finset.sum_nbij'724    (fun x ↦ ⟨(x.2.2.1.1 + x.2.2.2.1, x.2.2.1.2 + x.2.2.2.2 + x.1.2), (x.2.2.1.1, x.2.2.2.1),725      (x.2.2.1.2 + x.2.2.2.2, x.1.2), (x.2.2.1.2, x.2.2.2.2)⟩)726    (fun y ↦ ⟨(y.2.1.1 + y.2.1.2 + y.2.2.2.1 + y.2.2.2.2, y.2.2.1.2),727      (y.2.1.1 + y.2.2.2.1, y.2.1.2 + y.2.2.2.2), (y.2.1.1, y.2.2.2.1), (y.2.1.2, y.2.2.2.2)⟩)728    ?_ ?_ ?_ ?_ ?_729  all_goals rintro ⟨⟨a, b⟩, ⟨c, d⟩, ⟨e, g⟩, ⟨h, k⟩⟩ hx730  all_goals simp only [Finset.mem_sigma, Finset.HasAntidiagonal.mem_antidiagonal,731    Sigma.mk.injEq, Prod.mk.injEq, heq_eq_eq, and_true, true_and] at hx ⊢732  · omega733  · omega734  · omega735  · omega736  · obtain ⟨h1, rfl, rfl, rfl⟩ := hx737    have key : qpow (-((tri (e + g) : ℕ) : ℤ) - ((e + g : ℕ) : ℤ) * (b : ℤ)) *738        qpow (-((e : ℤ) * (k : ℤ))) = qpow (-(tri e : ℤ) - (e : ℤ) * ((g + k + b : ℕ) : ℤ)) *739          qpow (-(tri g : ℤ) - (g : ℤ) * (b : ℤ)) := by740      rw [← qpow_add, ← qpow_add, tri_add]741      congr 1742      push_cast743      ring744    linear_combination (U e h * V g k * PowerSeries.coeff b f) * key745 746/-- `ρ(1) = id`. -/747theorem qact_qone (f : Ser) : qact qone f = f := by748  ext n749  simp only [qact, PowerSeries.coeff_mk]750  rw [Finset.sum_eq_single (0, n)]751  · simp [qone, tri, qpow_zero]752  · rintro ⟨a, b⟩ hp hne753    rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp754    have ha : a ≠ 0 := fun h ↦ hne (Prod.ext h (by simp at hp ⊢; omega))755    refine Finset.sum_eq_zero fun r hr ↦ ?_756    rw [Finset.HasAntidiagonal.mem_antidiagonal] at hr757    have : ¬ (r.1 = 0 ∧ r.2 = 0) := by omega758    simp [qone, this]759  · simp760 761/-- `ρ(U)` is additive on differences. -/762theorem qact_sub (U : QSer) (f g : Ser) : qact U (f - g) = qact U f - qact U g := by763  ext n764  simp [qact, mul_sub, Finset.sum_sub_distrib]765 766/-! ### The twisted product -/767 768/-- Congruence of contact series through degree `j` implies congruence through any `i ≤ j`. -/769theorem QCongr.mono {i j : ℕ} {U V : QSer} (h : QCongr j U V) (hij : i ≤ j) : QCongr i U V :=770  fun c k hck ↦ h c k (hck.trans hij)771 772/-- Congruence of contact series is transitive. -/773theorem QCongr.trans {j : ℕ} {U V W : QSer} (h : QCongr j U V) (h' : QCongr j V W) :774    QCongr j U W :=775  fun c k hck ↦ (h c k hck).trans (h' c k hck)776 777/-- Congruence of contact series is compatible with the twisted product. -/778theorem QCongr.qmul {j : ℕ} {U U' V V' : QSer} (hU : QCongr j U U') (hV : QCongr j V V') :779    QCongr j (qmul U V) (qmul U' V') := fun c h hch ↦ by780  refine Finset.sum_congr rfl fun p hp ↦ Finset.sum_congr rfl fun r hr ↦ ?_781  rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp hr782  rw [hU p.1 r.1 (by omega), hV p.2 r.2 (by omega)]783 784/-- Diagonal substitution doubles the congruence degree: `f ≡ g` through `M` gives785`qdiag f ≡ qdiag g` through `2M + 1`. -/786theorem SCongr.qdiag {M : ℕ} {f g : Ser} (h : SCongr M f g) :787    QCongr (2 * M + 1) (qdiag f) (qdiag g) := by788  intro c k hck789  unfold SurfaceBlowup.qdiag790  split_ifs with e791  · subst e; rw [h c (by omega)]792  · rfl793 794private theorem antidiagonal_shift_sum {c k : ℕ} {p : ℕ × ℕ}795    (hp : p ∈ Finset.HasAntidiagonal.antidiagonal c) (G : ℕ × ℕ → Coef) (hck : c ≤ k) :796    ∑ r ∈ Finset.HasAntidiagonal.antidiagonal k,797      (if p.1 ≤ r.1 ∧ p.2 ≤ r.2 then G (r.1 - p.1, r.2 - p.2) else 0) =798        ∑ r ∈ Finset.HasAntidiagonal.antidiagonal (k - c), G r := by799  rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp800  rw [← Finset.sum_filter]801  apply Finset.sum_nbij' (fun r ↦ (r.1 - p.1, r.2 - p.2)) (fun s ↦ (s.1 + p.1, s.2 + p.2))802  all_goals intro r hr803  all_goals simp only [Finset.mem_filter, Finset.HasAntidiagonal.mem_antidiagonal] at hr ⊢804  · omega805  · omega806  · ext <;> simp <;> omega807  · ext <;> simp808 809private theorem antidiagonal_shift_sum_eq_zero {c k : ℕ} {p : ℕ × ℕ}810    (hp : p ∈ Finset.HasAntidiagonal.antidiagonal c) (G : ℕ × ℕ → Coef) (hkc : k < c) :811    ∑ r ∈ Finset.HasAntidiagonal.antidiagonal k,812      (if p.1 ≤ r.1 ∧ p.2 ≤ r.2 then G (r.1 - p.1, r.2 - p.2) else 0) = 0 := by813  rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp814  refine Finset.sum_eq_zero fun r hr ↦ ?_815  rw [Finset.HasAntidiagonal.mem_antidiagonal] at hr816  rw [if_neg]817  omega818 819/-- `ι₊` is multiplicative for the twisted product. -/820theorem qplus_qmul (U V : QSer) : qplus (qmul U V) = qmul (qplus U) (qplus V) := byLemma 8.1821  funext c k822  simp only [qplus, qmul]823  set G : ℕ × ℕ → ℕ × ℕ → Coef := fun p s ↦ qpow (-((p.1 : ℤ) * ((s.2 + p.2 : ℕ) : ℤ))) *824    ((qpow (-(chooseTwo p.1 : ℤ)) * U p.1 s.1) * (qpow (-(chooseTwo p.2 : ℤ)) * V p.2 s.2)) with hG825  have key : ∀ p ∈ Finset.HasAntidiagonal.antidiagonal c,826      (∑ r ∈ Finset.HasAntidiagonal.antidiagonal k, qpow (-((p.1 : ℤ) * (r.2 : ℤ))) *827        ((if p.1 ≤ r.1 then qpow (-(chooseTwo p.1 : ℤ)) * U p.1 (r.1 - p.1) else 0) *828         (if p.2 ≤ r.2 then qpow (-(chooseTwo p.2 : ℤ)) * V p.2 (r.2 - p.2) else 0))) =829      ∑ r ∈ Finset.HasAntidiagonal.antidiagonal k,830        (if p.1 ≤ r.1 ∧ p.2 ≤ r.2 then G p (r.1 - p.1, r.2 - p.2) else 0) := by831    intro p _832    refine Finset.sum_congr rfl fun r _ ↦ ?_833    by_cases h1 : p.1 ≤ r.1 <;> by_cases h2 : p.2 ≤ r.2 <;> simp [hG, h1, h2]834  rw [Finset.sum_congr rfl key]835  split_ifs with hck836  · rw [Finset.mul_sum]837    refine Finset.sum_congr rfl fun p hp ↦ ?_838    rw [antidiagonal_shift_sum hp (G p) hck, Finset.mul_sum]839    rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp840    subst hp841    refine Finset.sum_congr rfl fun s _ ↦ ?_842    have e2 : qpow (-(((chooseTwo (p.1 + p.2) : ℕ) : ℤ))) * qpow (-((p.1 : ℤ) * (s.2 : ℤ))) =843        qpow (-((p.1 : ℤ) * ((s.2 + p.2 : ℕ) : ℤ))) *844          (qpow (-(chooseTwo p.1 : ℤ)) * qpow (-(chooseTwo p.2 : ℤ))) := by845      rw [← qpow_add, ← qpow_add, ← qpow_add, chooseTwo_add]846      push_cast; ring_nf847    calc _ = (qpow (-(((chooseTwo (p.1 + p.2) : ℕ) : ℤ))) * qpow (-((p.1 : ℤ) * (s.2 : ℤ)))) *848          (U p.1 s.1 * V p.2 s.2) := by ring849      _ = _ := by rw [e2, hG]; ring850  · exact (Finset.sum_eq_zero fun p hp ↦ antidiagonal_shift_sum_eq_zero hp (G p) (by omega)).symm851 852/-- Transpose of a contact series. -/853private def qtranspose (U : QSer) : QSer := fun c h ↦ U h c854 855private theorem qminus_eq_transpose (U : QSer) :856    qminus U = qtranspose (qplus (qtranspose U)) := rfl857 858private theorem qtranspose_qmul (U V : QSer) :859    qtranspose (qmul U V) = qmul (qtranspose V) (qtranspose U) := by860  funext c h861  simp only [qtranspose, qmul]862  rw [Finset.sum_comm, ← Finset.Nat.sum_antidiagonal_swap]863  refine Finset.sum_congr rfl fun r _ ↦ ?_864  rw [← Finset.Nat.sum_antidiagonal_swap]865  refine Finset.sum_congr rfl fun p _ ↦ ?_866  simp only [Prod.fst_swap, Prod.snd_swap]867  rw [mul_comm (U _ _), mul_comm (r.1 : ℤ)]868 869/-- `ι₋` is multiplicative for the twisted product. -/870theorem qminus_qmul (U V : QSer) : qminus (qmul U V) = qmul (qminus U) (qminus V) := byLemma 8.1871  simp only [qminus_eq_transpose, qtranspose_qmul, qplus_qmul]872 873/-- `E_{0,0}` is a left unit for the twisted product. -/874theorem qone_qmul (U : QSer) : qmul qone U = U := by875  funext c h876  simp only [qmul, qone]877  rw [Finset.sum_eq_single (0, c), Finset.sum_eq_single (0, h)]878  · simp [qpow_zero]879  · intro r hr hne880    have : r.1 ≠ 0 := fun h2 ↦ hne (Prod.ext h2881      (by have := Finset.HasAntidiagonal.mem_antidiagonal.1 hr; simp_all))882    simp [this]883  · simp884  · intro p hp hne885    have : p.1 ≠ 0 := fun h2 ↦ hne (Prod.ext h2886      (by have := Finset.HasAntidiagonal.mem_antidiagonal.1 hp; simp_all))887    exact Finset.sum_eq_zero fun r _ ↦ by simp [this]888  · simp889 890private theorem qmul_eq_sum_range (U V : QSer) (c h : ℕ) :891    qmul U V c h = ∑ a ∈ Finset.range (c + 1), ∑ b ∈ Finset.range (h + 1),892      qpow (-((a : ℤ) * ((h - b : ℕ) : ℤ))) * (U a b * V (c - a) (h - b)) := by893  simp only [qmul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]894 895private theorem sum_range_eq_sum_range_ite {M : Type*} [AddCommMonoid M] (f : ℕ → M) (a N : ℕ)896    (haN : a ≤ N) :897    ∑ x ∈ Finset.range (a + 1), f x = ∑ x ∈ Finset.range (N + 1), if x ≤ a then f x else 0 := by898  rw [← Finset.sum_filter]899  congr 1900  ext x901  simp only [Finset.mem_range, Finset.mem_filter]902  omega903 904/-- The summand of the quadruple sum computing `(ι₊(A) · qdiag(D) · ι₋(C))_{c,h}`: the outer905product is split at `(a, b)` and the inner one at `(a', b')`. -/906private def qtripleTerm (A Cq : QSer) (D : Ser) (c h a b a' b' : ℕ) : Coef :=907  if a' ≤ a ∧ b' ≤ b then908    qpow (-((a : ℤ) * ((h - b : ℕ) : ℤ))) *909      ((qpow (-((a' : ℤ) * ((b - b' : ℕ) : ℤ))) * (qplus A a' b' * qdiag D (a - a') (b - b'))) *910        qminus Cq (c - a) (h - b))911  else 0912 913/-- The coefficient `(ι₊(A) · qdiag(D) · ι₋(C))_{c,h}` as an unrestricted quadruple sum over914the box `[0, c] × [0, h] × [0, c] × [0, h]`. -/915private theorem qmul_qplus_qdiag_qminus_eq_sum (A Cq : QSer) (D : Ser) (c h : ℕ) :916    qmul (qmul (qplus A) (qdiag D)) (qminus Cq) c h =917      ∑ x ∈ (Finset.range (c + 1) ×ˢ Finset.range (h + 1)) ×ˢ918        (Finset.range (c + 1) ×ˢ Finset.range (h + 1)),919        qtripleTerm A Cq D c h x.1.1 x.1.2 x.2.1 x.2.2 := by920  rw [qmul_eq_sum_range, Finset.sum_product, Finset.sum_product]921  refine Finset.sum_congr rfl fun a ha ↦ Finset.sum_congr rfl fun b hb ↦ ?_922  simp only [Finset.mem_range] at ha hb923  rw [Finset.sum_product, qmul_eq_sum_range, sum_range_eq_sum_range_ite _ a c (by omega),924    Finset.sum_mul, Finset.mul_sum]925  refine Finset.sum_congr rfl fun a' _ ↦ ?_926  split_ifs with h1927  · rw [sum_range_eq_sum_range_ite _ b h (by omega), Finset.sum_mul, Finset.mul_sum]928    refine Finset.sum_congr rfl fun b' _ ↦ ?_929    simp only [qtripleTerm]930    split_ifs with h2 h3 <;> first | (exfalso; omega) | simp931  · simp [qtripleTerm, h1]932 933/-- The quadruple-sum summand at the splitting determined by `(rx, m, rt)`, in closed form. -/934private theorem qtripleTerm_eq (A Cq : QSer) (D : Ser) {c h rx m rt : ℕ}935    (hc1 : rx + m + rt ≤ c) (hc2 : rx + m + rt ≤ h) :936    qtripleTerm A Cq D c h (rx + m) (h - rt) rx (h - rt - m) =937      qpow (-(chooseTwo rx : ℤ) - (chooseTwo m : ℤ) - (chooseTwo rt : ℤ) - (rx : ℤ) * (m : ℤ) -938          ((rx : ℤ) + (m : ℤ)) * (rt : ℤ)) *939        (A rx (h - (rx + m + rt)) * (PowerSeries.coeff m D * Cq (c - (rx + m + rt)) rt)) := by940  simp only [qtripleTerm, qplus, qdiag, qminus]941  rw [if_pos (by omega : rx ≤ rx + m ∧ h - rt - m ≤ h - rt),942    show rx + m - rx = m by omega, show h - rt - (h - rt - m) = m by omega,943    show h - (h - rt) = rt by omega, if_pos (show rx ≤ h - rt - m by omega), if_pos rfl,944    if_pos (show rt ≤ c - (rx + m) by omega), show h - rt - m - rx = h - (rx + m + rt) by omega,945    show c - (rx + m) - rt = c - (rx + m + rt) by omega]946  have hq : qpow (-(chooseTwo rx : ℤ) - (chooseTwo m : ℤ) - (chooseTwo rt : ℤ) -947      (rx : ℤ) * (m : ℤ) - ((rx : ℤ) + (m : ℤ)) * (rt : ℤ)) =948      qpow (-(((rx + m : ℕ) : ℤ) * (rt : ℤ))) * qpow (-((rx : ℤ) * (m : ℤ))) *949        qpow (-(chooseTwo rx : ℤ)) * qpow (-(chooseTwo m : ℤ)) * qpow (-(chooseTwo rt : ℤ)) := by950    rw [← qpow_add, ← qpow_add, ← qpow_add, ← qpow_add]951    congr 1952    push_cast953    ring954  rw [hq]; ring955 956/-- Expansion of the coefficient `(ι₊(A) · qdiag(D) · ι₋(C))_{c,h}` as a triple sum. -/957theorem qmul_qplus_qdiag_qminus_apply (A Cq : QSer) (D : Ser) (c h : ℕ) :958    qmul (qmul (qplus A) (qdiag D)) (qminus Cq) c h =959      ∑ rx ∈ Finset.range (c + 1), ∑ m ∈ Finset.range (c + 1), ∑ rt ∈ Finset.range (c + 1),960        (if (rx + m + rt ≤ c ∧ rx + m + rt ≤ h) then961          qpow (-(chooseTwo rx : ℤ) - (chooseTwo m : ℤ) - (chooseTwo rt : ℤ) - (rx : ℤ) * (m : ℤ) -962            ((rx : ℤ) + (m : ℤ)) * (rt : ℤ)) *963            (A rx (h - (rx + m + rt)) * (PowerSeries.coeff m D * Cq (c - (rx + m + rt)) rt))964        else 0) := by965  -- Reindex the quadruple sum of `qmul_qplus_qdiag_qminus_eq_sum` by its nonzero terms,966  -- which are exactly the splittings `(rx + m, h - rt, rx, h - rt - m)`.967  set G := qtripleTerm A Cq D c h with hG968  set T : ℕ → ℕ → ℕ → Coef := fun rx m rt ↦969    (if (rx + m + rt ≤ c ∧ rx + m + rt ≤ h) then970      qpow (-(chooseTwo rx : ℤ) - (chooseTwo m : ℤ) - (chooseTwo rt : ℤ) - (rx : ℤ) * (m : ℤ) -971        ((rx : ℤ) + (m : ℤ)) * (rt : ℤ)) *972        (A rx (h - (rx + m + rt)) * (PowerSeries.coeff m D * Cq (c - (rx + m + rt)) rt))973    else 0) with hT974  have hval : ∀ rx m rt : ℕ, rx + m + rt ≤ c → rx + m + rt ≤ h →975      T rx m rt = G (rx + m) (h - rt) rx (h - rt - m) := fun rx m rt hc1 hc2 ↦ by976    rw [hT, hG, qtripleTerm_eq A Cq D hc1 hc2]; exact if_pos ⟨hc1, hc2⟩977  have hT0 : ∀ x : ℕ × ℕ × ℕ, T x.1 x.2.1 x.2.2 ≠ 0 →978      x.1 + x.2.1 + x.2.2 ≤ c ∧ x.1 + x.2.1 + x.2.2 ≤ h := fun x hne ↦ by979    by_contra hc; exact hne (by simp only [hT]; rw [if_neg hc])980  have hR : ∑ rx ∈ Finset.range (c + 1), ∑ m ∈ Finset.range (c + 1), ∑ rt ∈ Finset.range (c + 1),981      T rx m rt = ∑ x ∈ Finset.range (c + 1) ×ˢ (Finset.range (c + 1) ×ˢ Finset.range (c + 1)),982        T x.1 x.2.1 x.2.2 := by983    simp only [Finset.sum_product]984  rw [qmul_qplus_qdiag_qminus_eq_sum, ← hG, hR]985  symm986  refine Finset.sum_bij_ne_zero987    (fun x _ _ ↦ ((x.1 + x.2.1, h - x.2.2), (x.1, h - x.2.2 - x.2.1))) ?_ ?_ ?_ ?_988  · intro x hx hne989    have := hT0 x hne990    simp only [Finset.mem_product, Finset.mem_range]991    omega992  · rintro ⟨x1, x2, x3⟩ _ hx ⟨y1, y2, y3⟩ _ hy hxy993    have := hT0 _ hx994    have := hT0 _ hy995    simp only [Prod.mk.injEq] at *996    omega997  · rintro ⟨⟨a, b⟩, ⟨a', b'⟩⟩ hmem hne998    simp only [Finset.mem_product, Finset.mem_range] at hmem999    have key : a' ≤ a ∧ b' ≤ b ∧ a' ≤ b' ∧ a - a' = b - b' ∧ h - b ≤ c - a := by1000      by_contra hc1001      apply hne1002      simp only [hG, qtripleTerm, qplus, qdiag, qminus]1003      split_ifs <;> first | (exfalso; omega) | simp1004    refine ⟨(a', a - a', h - b), ?_, ?_, ?_⟩1005    · simp only [Finset.mem_product, Finset.mem_range]1006      omega1007    · dsimp only1008      rw [hval _ _ _ (by omega) (by omega), show a' + (a - a') = a by omega,1009        show h - (h - b) = b by omega, show b - (a - a') = b' by omega]1010      exact hne1011    · dsimp only1012      rw [show a' + (a - a') = a by omega, show h - (h - b) = b by omega,1013        show b - (a - a') = b' by omega]1014  · intro x _ hx1015    exact hval _ _ _ (hT0 x hx).1 (hT0 x hx).21016 1017/-- If `U` is positive and agrees with `1` through degree `j - 1`, then `ι₊ U` agrees with `1`1018through degree `j`. -/1019theorem qcongr_qplus_qone (j : ℕ) (U : QSer) (hU : QPositive U) (h : QCongr (j - 1) U qone) :1020    QCongr j (qplus U) qone := by1021  intro c k hck1022  simp only [qplus, qone]1023  split_ifs with hc h1 h11024  · obtain ⟨rfl, rfl⟩ := h11025    simpa [chooseTwo, qpow_zero, qone] using h 0 0 (by omega)1026  · rcases Nat.eq_zero_or_pos c with rfl | c01027    · rw [Nat.sub_zero, hU 0 k (Or.inl rfl) (by omega), mul_zero]1028    · rw [h c (k - c) (by omega), qone, if_neg (by omega), mul_zero]1029  · omega1030  · rfl1031 1032private theorem qtranspose_qcongr_qone {j : ℕ} {U : QSer} (h : QCongr j U qone) :1033    QCongr j (qtranspose U) qone := fun c k hck ↦ by1034  simpa [qtranspose, qone, and_comm] using h k c (by omega)1035 1036/-- If `U` is positive and agrees with `1` through degree `j - 1`, then `ι₋ U` agrees with `1`1037through degree `j`. -/1038theorem qcongr_qminus_qone (j : ℕ) (U : QSer) (hU : QPositive U) (h : QCongr (j - 1) U qone) :1039    QCongr j (qminus U) qone := by1040  rw [qminus_eq_transpose]1041  exact qtranspose_qcongr_qone (qcongr_qplus_qone j _1042    (fun c k h1 h2 ↦ hU k c h1.symm (by tauto)) (qtranspose_qcongr_qone h))1043 1044end SurfaceBlowup