The reciprocity law (Theorem R)

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Reciprocity.Patterns7 8/-!9# The reciprocity law (Theorem R)10 11This file assembles the proof of Theorem R: the universal monic density `monicExpr n σ` is the12`σ`-coefficient of the root law `rootLaw n` with `q ↦ 1/q` substituted (`A_n(q) = B_n(1/q)`),13and the universal projective density `projectiveExpr n σ` is self-reciprocal14(`R_n(1/q) = R_n(q)`).15 16The single-boundary cluster series `B_a = clusterSer a` satisfies an operator equation17`B_a = ρ(U_{a,a}) Φ(G_a)` for the contact series `U_{a,a} = crossingQ a a`, where18`G_a = eulerSer 0 a` is its Euler transform. Conjugating by reciprocal substitution `q ↦ q⁻¹`19and using the unitarity of `U_{a,a}` through a given degree, an induction on the cluster degree20shows `G_a = S(B_aᵛ)` (`S` the dilation `x ↦ qx`, `ᵛ` the reciprocal substitution). Reading off21coefficients for `a = 1` gives both statements.22 23## Main results24 25* `coeff_clusterSer_eq_coeff_qact`: `B_a = ρ(U_{a,a}) Φ(G_a)` coefficientwise.26* `cluster_reciprocity`: `G_a ≡ S(B_aᵛ)` in every degree.27* `lawCoef_globalLaw_false_eq_recipCoef`, `recipCoef_lawCoef_globalLaw_true`: the coefficient28  forms.29* `recip_main`: Theorem R.30 31Provenance: `Thm_SurfaceBlowupV2_recip_{single_exit_regroup, single_operator_equation,32reciprocal_operator_equation, second_operator_equation, cluster_step, cluster_all, affine_coef,33projective_coef, main}`.34-/35 36namespace SurfaceBlowup37 38/-! ### The operator equation for single-boundary clusters -/39 40/-- The exit part of the recursion of `S(a;n)` (`n ≥ 2`), plus the self-return term41`q^{-tri n} q F_{S(a;n)}`, regroups by divisor degree `d` and crossing depth `r` into the42pattern sums `patternSum 0 a (a n) (d - r)`, weighted by the divisor probabilities and the laws43of the crossing children `T(a,a;r,n-d)`. -/44private theorem lawCoef_exitLaw_single_add_self (a n : ℕ) (ha : 0 < a) (hn : 2 ≤ n) :45    lawCoef (exitLaw (State.single a n)) +46        qpow (-(tri n : ℤ)) * (qpow 1 * lawCoef (stateLaw (State.single a n))) =47      ∑ d ∈ Finset.Icc 1 n, ∑ r ∈ Finset.range (d + 1),48        (if ((0 < r ↔ d < n) ∧ r ≤ d) then49          scalar (divisorProbability (State.single a n) d).rational *50            ((if r = 0 then 1 else lawCoef (stateLaw (State.crossing a a r (n - d)))) *51              patternSum 0 a (a * n) (d - r))52        else 0) := by53  classical54  have hn0 : 0 < n := by omega55  have hA : ∀ P ∈ allowedPatterns (State.single a n), Allowed (State.single a n) P :=56    fun P hP ↦ (Finset.mem_filter.mp hP).257  set T : TangentPattern (State.single a n).degree → Coef := fun P ↦58    lawCoef (lawScale (.mul (tangentCount (State.single a n) P)59      (divisorProbability (State.single a n) P.d.val))60        (lawProd ((children (State.single a n) P).map fun z ↦ lawDescend z.1 (stateLaw z.2))))61    with hT62  have hexit : lawCoef (exitLaw (State.single a n)) = ∑ P ∈ allowedPatterns (State.single a n),63      (if SelfPattern (State.single a n) P then 0 else T P) := by64    unfold exitLaw65    rw [lawCoef_flatMap, Finset.sum_map_toList]66    refine Finset.sum_congr rfl fun P _ ↦ ?_67    split_ifs <;> simp [lawCoef_nil, hT]68  obtain ⟨P₀, hA₀, hS₀, huniq⟩ := exists_unique_selfPattern_single a n ha hn69  have hself : ∑ P ∈ allowedPatterns (State.single a n),70      (if SelfPattern (State.single a n) P then T P else 0) = T P₀ := by71    rw [Finset.sum_eq_single P₀ (fun Q hQ hne ↦ if_neg fun hSQ ↦ hne (huniq Q (hA Q hQ) hSQ))72      (fun h ↦ absurd (Finset.mem_filter.mpr ⟨Finset.mem_univ _, hA₀⟩) h), if_pos hS₀]73  have hsplit : lawCoef (exitLaw (State.single a n)) + T P₀ =74      ∑ P ∈ allowedPatterns (State.single a n), T P := by75    rw [hexit, ← hself, ← Finset.sum_add_distrib]76    refine Finset.sum_congr rfl fun P _ ↦ ?_77    split_ifs <;> simp78  rw [← lawCoef_single_self_term a n ha hn P₀ hA₀ hS₀]79  refine hsplit.trans <| (Finset.sum_congr rfl fun P hP ↦80    lawCoef_single_term a n ha hn0 P (hA P hP)).trans ?_81  rw [sum_allowedPatterns_single a n ha (fun d r m ↦82    scalar ((divisorCount 0 m).rational * (divisorProbability (State.single a n) d).rational) *83      ((if r = 0 then 1 else lawCoef (stateLaw (State.crossing a a r (n - d)))) *84        ∏ ij : Fin (State.single a n).degree × Fin (State.single a n).degree,85          (adamsCoef (ij.1.val + 1) (lawCoef (stateLaw (State.single a (ij.2.val + 1))))) ^86            (m ij).val))]87  refine Finset.sum_congr rfl fun d _ ↦ Finset.sum_congr rfl fun r _ ↦ ?_88  by_cases hcond : ((0 < r ↔ d < n) ∧ r ≤ d)89  · rw [if_pos hcond, if_pos hcond]; exact sum_patterns_scalar_mul_eq_patternSum _ _ _ _ _ _90  · rw [if_neg hcond, if_neg hcond]91 92/-- **Operator equation.** The cluster series is obtained from its Euler transform by the93Gaussian twist and the contact representation: `B_a = ρ(U_{a,a}) Φ(G_a)`, coefficientwise. -/94theorem coeff_clusterSer_eq_coeff_qact (a n : ℕ) (ha : 0 < a) :(S) = (7.11)(8.9)(9.4)95    PowerSeries.coeff n (clusterSer a) =96      PowerSeries.coeff n (qact (crossingQ a a) (gaussPhi (eulerSer 0 a))) := by97  have hqp : ∀ k : ℤ, qpow k = algebraMap (RatFunc ℚ) Coef ((RatFunc.X : RatFunc ℚ) ^ k) :=98    fun k ↦ scalar_eq_algebraMap _99  rw [coeff_qact_crossingQ_gaussPhi_eulerSer a n ha]100  rcases Nat.lt_or_ge n 2 with hn | hn101  · interval_cases n102    · simp [(coeff_zero_clusterSer a)]103    · rw [(coeff_one_clusterSer a)]104      simp only [Finset.Icc_self, Finset.sum_singleton, Finset.sum_range_succ, Finset.range_one]105      have hp : patternSum 0 a (a * 1) 1 =106          qpow 1 * AddMonoidAlgebra.single ({(a, 1)} : FactorType) 1 := by107        rw [patternSum_eq_of_le 0 a (a * 1) 1 1 (by omega) le_rfl, ← coeff_eulerSer,108          coeff_one_eulerSer_zero a]109      have hd : (divisorProbability (State.single a 1) 1).rational =110          (RatFunc.X : RatFunc ℚ)⁻¹ := by111        rw [rational_divisorProbability_single a 1 1]; simp [tri]112      simp only [hp, hd, lt_irrefl, iff_self, zero_le, and_self, if_true, one_ne_zero, if_false,113        one_mul, Nat.sub_zero, zero_lt_one, iff_false, not_true, false_and, add_zero]114      rw [scalar_eq_algebraMap, hqp, ← mul_assoc, ← map_mul, zpow_one,115        inv_mul_cancel₀ RatFunc.X_ne_zero, map_one,116        one_mul]117  · have hB := (coeff_succ_clusterSer a (n - 1))118    rw [show n - 1 + 1 = n by omega] at hB119    have hreg := lawCoef_exitLaw_single_add_self a n ha hn120    have hnt : (State.single a n).terminal = false := by121      obtain ⟨k, rfl⟩ : ∃ k, n = k + 2 := ⟨n - 2, by omega⟩122      rfl123    have hs : (State.single a n).Valid := ⟨ha, by omega⟩124    have hlaw := (state_law_unfold _ hs hnt).1 a n rfl125    rw [hB, hlaw]; rw [hlaw] at hreg126    have hsub : (Expr.sub (Expr.const 1) (returnWeight n)).rational =127        1 - (returnWeight n).rational := by128      rw [Expr.rational_sub (x := Expr.const 1) trivial (wf_returnWeight n), Expr.rational_const]129      simp130    rw [lawCoef_lawScale, Expr.rational_inv, hsub] at hreg ⊢131    have hne := one_sub_rational_returnWeight_ne_zero n hn132    have hlam : (returnWeight n).rational =133        (RatFunc.X : RatFunc ℚ) ^ (-(tri n : ℤ)) * RatFunc.X ^ (1 : ℤ) := by134      rw [rational_returnWeight n, zpow_neg, zpow_natCast, zpow_one,135        mul_comm]136    rw [← hreg, if_neg (by omega), add_zero, ← mul_assoc, hqp, hqp, ← map_mul, ← hlam,137      scalar_eq_algebraMap,138      ← mul_assoc, ← map_mul, ← one_add_mul, ← map_one (algebraMap (RatFunc ℚ) Coef), ← map_add]139    congr 2140    field_simp141    ring142 143/-- **Reciprocal operator equation.** Applying reciprocal substitution and the dilation to the144operator equation: `Φ(S(B_aᵛ)) = ρ(U_{a,a}†) S(G_aᵛ)`. -/145private theorem gaussPhi_dilate_recipSer_clusterSer (a : ℕ) (ha : 0 < a) :(9.4)146    gaussPhi (dilate (recipSer (clusterSer a))) =147      qact (qdagger (crossingQ a a)) (dilate (recipSer (eulerSer 0 a))) := by148  have hB : clusterSer a = qact (crossingQ a a) (gaussPhi (eulerSer 0 a)) :=149    PowerSeries.ext fun n ↦ coeff_clusterSer_eq_coeff_qact a n ha150  have hv : recipSer (clusterSer a) =151      qactRecip (qrecip (crossingQ a a)) (gaussPhiInv (recipSer (eulerSer 0 a))) := by152    rw [hB, (recipSer_qact _ _), (recipSer_gaussPhi (eulerSer 0 a))]153  have hconj := gaussPhi_qactRecip_gaussPhiInv (crossingQ a a)154    (fun c h ↦ crossingQ_symm a a c h ha ha) (recipSer (eulerSer 0 a))155  rw [← hv] at hconj156  rw [(gaussPhi_dilate (recipSer (clusterSer a))), hconj,157    (dilate_codilate (qact (qdagger (crossingQ a a))158      (dilate (recipSer (eulerSer 0 a)))))]159 160/-- If `U_{a,a} U_{a,a}† ≡ 1` through degree `n`, then `ρ(U_{a,a}) Φ(S(B_aᵛ)) ≡ S(G_aᵛ)`161through degree `n`. -/162private theorem qact_gaussPhi_dilate_recipSer_scongr (a n : ℕ) (ha : 0 < a)(9.4)163    (hU : QCongr n (qmul (crossingQ a a) (qdagger (crossingQ a a))) qone) :164    SCongr n (qact (crossingQ a a) (gaussPhi (dilate (recipSer (clusterSer a)))))165      (dilate (recipSer (eulerSer 0 a))) := by166  rw [gaussPhi_dilate_recipSer_clusterSer a ha, ← qact_qmul]167  simpa only [qact_qone] using hU.qact_scongr (dilate (recipSer (eulerSer 0 a)))168 169/-! ### The induction on cluster degree -/170 171/-- Inductive step: if `G_b ≡ S(B_bᵛ)` through degree `n - 1` for all `b > 0`, then172`G_a ≡ S(B_aᵛ)` through degree `n` (`n ≥ 2`). -/173private theorem cluster_reciprocity_step (n : ℕ) (hn : 2 ≤ n)Proof of monic/cluster reciprocity174    (ih : ∀ a : ℕ, 0 < a → SCongr (n - 1) (eulerSer 0 a) (dilate (recipSer (clusterSer a))))175    (a : ℕ) (ha : 0 < a) :176    SCongr n (eulerSer 0 a) (dilate (recipSer (clusterSer a))) := by177  have hQ := qcongr_crossingQ_mul_qdagger (n / 2) (fun b hb ↦178    (SCongr.mono (ih b hb) (by omega)))179    n (by omega) a a ha ha180  have h2 := qact_gaussPhi_dilate_recipSer_scongr a n ha hQ n le_rfl181  have hD : ∀ m : ℕ, m < n → PowerSeries.coeff m182      (eulerSer 0 a - dilate (recipSer (clusterSer a))) = 0 := fun m hm ↦ by183    rw [map_sub, sub_eq_zero]184    exact ih a ha m (by omega)185  have lead := coeff_qact_gaussPhi_of_lt (crossingQ a a) (crossingQ_zero_zero a a) _ n hD186  rw [(gaussPhi_sub (eulerSer 0 a) (dilate (recipSer (clusterSer a)))),187    (qact_sub (crossingQ a a) _ _), map_sub, map_sub,188    ← coeff_clusterSer_eq_coeff_qact a n ha, h2] at lead189  have h4 := coeff_pPow_sub_of_scongr n (by omega) (RatFunc.X : RatFunc ℚ)⁻¹ _ _190    (constantCoeff_eulerSer 0 a)191    (by rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply,192      coeff_zero_dilate_recipSer_clusterSer]) (ih a ha)193  rw [← clusterSer_eq_pPow, ← dilate_recipSer_eulerSer_eq_pPow] at h4194  set δ := PowerSeries.coeff n (eulerSer 0 a) -195    PowerSeries.coeff n (dilate (recipSer (clusterSer a)))196  have key : scalar ((RatFunc.X : RatFunc ℚ)⁻¹ - (RatFunc.X : RatFunc ℚ) ^ (-(tri n : ℤ))) * δ =197      0 := by198    have : scalar ((RatFunc.X : RatFunc ℚ)⁻¹ - (RatFunc.X : RatFunc ℚ) ^ (-(tri n : ℤ)))199        = scalar (RatFunc.X : RatFunc ℚ)⁻¹ - qpow (-(tri n : ℤ)) :=200      AddMonoidAlgebra.single_sub (R := RatFunc ℚ) _ _ _201    rw [this, sub_mul, ← h4, ← lead, sub_self]202  have hδ := eq_zero_of_scalar_mul_eq_zero (X_inv_sub_X_zpow_neg_tri_ne_zero n hn) key203  intro m hm204  rcases Nat.lt_or_ge m n with h | h205  · exact ih a ha m (by omega)206  · obtain rfl : m = n := by omega207    exact sub_eq_zero.mp hδ208 209/-- **Cluster reciprocity.** For every `a > 0`, the Euler transform `G_a` agrees with the210dilated reciprocal cluster series `S(B_aᵛ)` in every degree `≤ n`. -/211theorem cluster_reciprocity (n a : ℕ) (ha : 0 < a) :Proof of monic/cluster reciprocityTheorem 9.3212    SCongr n (eulerSer 0 a) (dilate (recipSer (clusterSer a))) := by213  induction n using Nat.strong_induction_on generalizing a with214  | _ n ih =>215    by_cases h : n ≤ 1216    · exact (SCongr.mono (cluster_reciprocity_one a) h)217    · exact cluster_reciprocity_step n (by omega) (fun a ha ↦ ih (n - 1) (by omega) a ha) a ha218 219/-! ### Coefficient forms and Theorem R -/220 221/-- **Affine reciprocity.** The global monic law is the reciprocal of the root law:222`F_global(q) = F_{S(1;n)}(1/q)` as elements of `Coef`. -/223theorem lawCoef_globalLaw_false_eq_recipCoef (n : ℕ) (hn : 0 < n) :Theorem 1.2Lemma 9.2224    lawCoef (globalLaw false n) = recipCoef (lawCoef (rootLaw n)) := by225  have h1 := (cluster_reciprocity n 1 one_pos) n le_rfl226  rw [coeff_eulerSer,227    (coeff_dilate (recipSer (clusterSer 1)) n),228    (coeff_recipSer (clusterSer 1) n)] at h1229  obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩230  rw [(coeff_succ_clusterSer 1 m)] at h1231  rw [show rootLaw (m + 1) = stateLaw (.single 1 (m + 1)) by simp [rootLaw]]232  refine scalar_mul_left_cancel (pow_ne_zero (m + 1) (RatFunc.X_ne_zero (K := ℚ))) ?_233  rw [← qpow_natCast, ← h1, lawCoef_globalLaw_false, ← mul_assoc, mul_comm (qpow _),234    qpow_neg_mul_qpow, one_mul]235 236/-- **Projective self-reciprocity.** The normalised global projective law `R_n` is invariant237under reciprocal substitution: `R_n(1/q) = R_n(q)` as elements of `Coef`. -/238theorem recipCoef_lawCoef_globalLaw_true (n : ℕ) :Theorem 1.2Lemma 9.2239    recipCoef (lawCoef (globalLaw true n)) = lawCoef (globalLaw true n) := by240  set B := clusterSer 1 with hBdef241  have hB1 : PowerSeries.constantCoeff B = 1 := (constantCoeff_clusterSer 1)242  have hG : eulerSer 0 1 = pPow RatFunc.X B := by simp [eulerSer, hBdef]243  have hQ : eulerSer 1 1 = pPow (RatFunc.X + 1) B := by simp [eulerSer, hBdef]244  -- Step 1: `B ᵛ = S⁻¹ G_1`.245  have hGd : eulerSer 0 1 = dilate (recipSer B) :=246    PowerSeries.ext fun m ↦ cluster_reciprocity m 1 one_pos m le_rfl247  have hrB : recipSer B = codilate (pPow RatFunc.X B) := by248    rw [← hG, hGd, (codilate_dilate (recipSer B))]249  -- Step 2: `Q_1 ᵛ = S⁻¹ Q_1`.250  have hX : (RatFunc.X : RatFunc ℚ) ≠ 0 := RatFunc.X_ne_zero251  have hrQ : recipSer (pPow (RatFunc.X + 1) B) = codilate (pPow (RatFunc.X + 1) B) := by252    rw [(recipSer_pPow (RatFunc.X + 1) B hB1), map_add,253      recipRat_X, map_one, hrB,254      ← (codilate_pPow ((RatFunc.X)⁻¹ + 1) (pPow RatFunc.X B) (constantCoeff_pPow RatFunc.X B)),255      (pPow_pPow ((RatFunc.X)⁻¹ + 1) RatFunc.X B)]256    congr 2257    field_simp258    ring259  -- Step 3: read off the coefficient of `xⁿ`.260  have hcQ := congrArg (PowerSeries.coeff n) hrQ261  rw [(coeff_recipSer (pPow (RatFunc.X + 1) B) n),262    (coeff_codilate (pPow (RatFunc.X + 1) B) n),263    ← hQ, coeff_eulerSer] at hcQ264  have hNrec := recipRat_projectiveNormalizer n265  have hDne := projectiveNormalizer_rational_ne_zero n266  set D := (projectiveNormalizer n).rational267  set R := lawCoef (globalLaw true n)268  have hP : patternSum 1 1 n n = scalar D * R := by269    rw [show R = _ from lawCoef_globalLaw_true n, ← mul_assoc,270      ← (scalar_mul D D⁻¹), mul_inv_cancel₀ hDne,271      scalar_one, one_mul]272  have hqp : qpow (-(n : ℤ)) = scalar ((RatFunc.X ^ n)⁻¹) := by273    simp [qpow, zpow_neg, zpow_natCast]274  rw [hP, map_mul, (recipCoef_scalar D), hNrec,275    hqp, ← mul_assoc, ← (scalar_mul _ D)] at hcQ276  exact (scalar_mul_left_cancel (mul_ne_zero (inv_ne_zero (pow_ne_zero _ hX)) hDne)) hcQ277 278/-- **Theorem R (reciprocity).** For `n > 0` and every factorization type `σ`:279the universal monic density is the root-law coefficient with `q ↦ 1/q` substituted,280`A_{n,σ}(q) = B_{n,σ}(1/q)` (where `B_{n,σ}` is the coefficient of `σ` in the root law281`rootLaw n`), and the universal projective density is self-reciprocal,282`R_{n,σ}(1/q) = R_{n,σ}(q)`; both as identities of rational functions in `q`.283 284The certified form also assumed `ValidType σ` and `typeDegree σ = n`, which the proof does not use.285The hypothesis `0 < n` is used (`rootLaw 0` is defined separately). -/286theorem recip_main (n : ℕ) (hn : 0 < n) (σ : FactorType) :Theorem 1.2Remark 1.3Corollary 10.3287    (monicExpr n σ).rational =288      ((lawCoeff (rootLaw n) σ).subst (.inv .var)).rational ∧289    (projectiveExpr n σ).rational =290      ((projectiveExpr n σ).subst (.inv .var)).rational := by291  have hv : (State.single 1 n).Valid := ⟨Nat.one_pos, hn⟩292  have hr : rootLaw n = stateLaw (State.single 1 n) := by293    unfold rootLaw; rw [if_neg hn.ne']294  refine ⟨?_, ?_⟩295  · rw [← coeff_lawCoef_globalLaw_false, lawCoef_globalLaw_false_eq_recipCoef n hn, hr,296      coeff_recipCoef_lawCoef _ (lawWf_stateLaw (State.single 1 n) hv) σ]297  · rw [← coeff_lawCoef_globalLaw_true, ← recipCoef_lawCoef_globalLaw_true n,298      coeff_recipCoef_lawCoef _ (lawWf_globalLaw true n) σ]299    rfl300 301end SurfaceBlowup