ThetaCore.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIV.ReciprocalCore
7 
8 /-!
9 # Scaled reciprocal coupling and theta coefficients
10 
11 This file gives a branch-free formal-series definition of the theta family
12 from Paper IV and proves its exact reconstruction from the named reciprocal
13 coefficients.  The reduced variable is `w = z^N`.
14 -/
15 
16 namespace Komorebi.PaperIV
17 
18 open scoped PowerSeries
19 
20 noncomputable section
21 
22 variable {R : Type*} [CommRing R] [Algebra ℚ R]
23 
24 omit [Algebra ℚ R] in
25 /-- Block coefficients commute with rescaling in the expected way. -/
26 theorem blockCoeff_rescale (N n : ℕ) (a : R) (f : R⟦X⟧) :
27     blockCoeff N n (PowerSeries.rescale a f) = a ^ n * blockCoeff N n f := by
28   rw [blockCoeff, PowerSeries.coeff_rescale, blockCoeff]
29   ring
30 
31 /-- The reduced theta generating series
32 `Delta_N(-u^N w)^(-1) Delta_N(-w)^(-u)`.
33 
34 Because `H_N(z) = Delta_N(-z^N)`, this is exactly the formal version of
35 `H_N(uz)^(-1) H_N(z)^(-u)` after putting `w = z^N`.
36 -/
37 def thetaSeries (N : ℕ) (u : R) : R⟦X⟧ :=
38   PowerSeries.rescale (-u ^ N) (reciprocalSeries N 1) *
39     PowerSeries.rescale (-1) (reciprocalSeries N u)
40 
41 /-- Factorially normalized theta coefficient `Theta_{N,n}(u)`. -/
42 def thetaCoeff (N n : ℕ) (u : R) : R :=
43   blockCoeff N n (thetaSeries N u)
44 
45 @[simp]
46 theorem thetaSeries_zero (N : ℕ) (hN : 0 < N) :
47     thetaSeries (R := R) N 0 = 1 := by
48   simp [thetaSeries, hN.ne']
49 
50 @[simp]
51 theorem thetaCoeff_zero_parameter (N : ℕ) (hN : 0 < N) :
52     thetaCoeff (R := R) N 0 0 = 1 := by
53   rw [thetaCoeff, thetaSeries_zero N hN]
54   simp [blockCoeff]
55 
56 theorem thetaCoeff_zero_parameter_of_pos (N : ℕ) (hN : 0 < N)
57     {n : ℕ} (hn : 0 < n) :
58     thetaCoeff (R := R) N n 0 = 0 := by
59   rw [thetaCoeff, thetaSeries_zero N hN]
60   simp [blockCoeff, PowerSeries.coeff_one, hn.ne']
61 
62 /-- Exact theta reconstruction before extracting the common sign. -/
63 theorem thetaCoeff_reconstruction_unfactored (N n : ℕ) (u : R) :
64     thetaCoeff N n u =
65       ∑ q ∈ Finset.range (n + 1),
66         ((N * n).choose (N * q) : R) *
67           (-u ^ N) ^ q * reciprocalCoeff N q 1 *
68           (-1 : R) ^ (n - q) * reciprocalCoeff N (n - q) u := by
69   rw [thetaCoeff, thetaSeries, blockCoeff_mul]
70   apply Finset.sum_congr rfl
71   intro q hq
72   rw [blockCoeff_rescale, blockCoeff_rescale]
73   simp only [reciprocalCoeff]
74   ring
75 
76 /-- Paper IV's theta reconstruction formula. -/
77 theorem thetaCoeff_reconstruction (N n : ℕ) (u : R) :
78     thetaCoeff N n u =
79       (-1 : R) ^ n *
80         ∑ q ∈ Finset.range (n + 1),
81           ((N * n).choose (N * q) : R) *
82             reciprocalCoeff N q 1 * u ^ (N * q) *
83               reciprocalCoeff N (n - q) u := by
84   rw [thetaCoeff_reconstruction_unfactored, Finset.mul_sum]
85   apply Finset.sum_congr rfl
86   intro q hq
87   have hqn : q ≤ n := Nat.le_of_lt_succ (Finset.mem_range.mp hq)
88   have hsign : (-1 : R) ^ q * (-1 : R) ^ (n - q) = (-1 : R) ^ n := by
89     rw [← pow_add, Nat.add_sub_of_le hqn]
90   rw [neg_pow]
91   have hpow : (u ^ N) ^ q = u ^ (N * q) := by rw [← pow_mul]
92   rw [hpow]
93   calc
94     ((N * n).choose (N * q) : R) *
95           ((-1 : R) ^ q * u ^ (N * q)) * reciprocalCoeff N q 1 *
96           (-1 : R) ^ (n - q) * reciprocalCoeff N (n - q) u =
97         ((-1 : R) ^ q * (-1 : R) ^ (n - q)) *
98           (((N * n).choose (N * q) : R) * reciprocalCoeff N q 1 *
99             u ^ (N * q) * reciprocalCoeff N (n - q) u) := by ring
100     _ = (-1 : R) ^ n *
101           (((N * n).choose (N * q) : R) * reciprocalCoeff N q 1 *
102             u ^ (N * q) * reciprocalCoeff N (n - q) u) := by rw [hsign]
103 
104 /-- For even `N`, the theta generating series also specializes to one at
105 `u = -1`.  This is the formal source of the manuscript's `u + 1` factor. -/
106 theorem thetaSeries_neg_one_of_even (N : ℕ) (hN : Even N) :
107     thetaSeries (R := R) N (-1) = 1 := by
108   rw [thetaSeries, hN.neg_one_pow]
109   rw [← map_mul, reciprocalSeries_add, add_neg_cancel, reciprocalSeries_zero]
110   simp
111 
112 theorem thetaCoeff_neg_one_of_even_of_pos (N : ℕ) (hN : Even N)
113     {n : ℕ} (hn : 0 < n) :
114     thetaCoeff (R := R) N n (-1) = 0 := by
115   rw [thetaCoeff, thetaSeries_neg_one_of_even N hN]
116   simp [blockCoeff, PowerSeries.coeff_one, hn.ne']
117 
118 end
119 
120 end Komorebi.PaperIV

Back to source controls