SectionCycles.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.RingTheory.PowerSeries.Exp
7 
8 /-!
9 # Formal transfer and signed exponential sections
10 
11 This file isolates the exponential-generating coefficient sequences behind
12 Paper IV's transfer sections `E_{N,j}` and signed sections `D_{N,j}`.  The
13 derivative cycles are proved as identities of formal power series, including
14 the minus sign at the signed wraparound.  There are no convergence hypotheses.
15 -/
16 
17 namespace Komorebi.PaperIV
18 
19 open scoped PowerSeries
20 
21 noncomputable section
22 
23 variable {R : Type*} [CommRing R] [Algebra ℚ R]
24 
25 /-- Realize a coefficient sequence as its exponential generating series. -/
26 def exponentialGeneratingSeries (a : ℕ → R) : R⟦X⟧ :=
27   PowerSeries.mk fun n =>
28     a n * algebraMap ℚ R (1 / (n.factorial : ℚ))
29 
30 @[simp]
31 theorem coeff_exponentialGeneratingSeries (a : ℕ → R) (n : ℕ) :
32     PowerSeries.coeff n (exponentialGeneratingSeries a) =
33       a n * algebraMap ℚ R (1 / (n.factorial : ℚ)) := by
34   simp [exponentialGeneratingSeries]
35 
36 /-- Formal differentiation shifts exponential-generating coefficients. -/
37 theorem derivative_exponentialGeneratingSeries (a : ℕ → R) :
38     PowerSeries.derivative R (exponentialGeneratingSeries a) =
39       exponentialGeneratingSeries (fun n => a (n + 1)) := by
40   ext n
41   rw [PowerSeries.coeff_derivative]
42   simp only [coeff_exponentialGeneratingSeries]
43   have hfac :
44       algebraMap ℚ R (1 / ((n + 1).factorial : ℚ)) * (n + 1 : R) =
45         algebraMap ℚ R (1 / (n.factorial : ℚ)) := by
46     have hn : (n + 1 : R) = algebraMap ℚ R (n + 1) := by
47       rw [map_add, map_natCast, map_one]
48     rw [hn, ← map_mul]
49     congr 1
50     rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add_one]
51     field_simp
52   rw [mul_assoc, hfac]
53 
54 /-- Repeated formal differentiation shifts EGF coefficients by the same amount. -/
55 theorem iterate_derivative_exponentialGeneratingSeries (a : ℕ → R) (k : ℕ) :
56     (PowerSeries.derivative R)^[k] (exponentialGeneratingSeries a) =
57       exponentialGeneratingSeries (fun n => a (n + k)) := by
58   induction k with
59   | zero => simp
60   | succ k ih =>
61       rw [Function.iterate_succ_apply', ih, derivative_exponentialGeneratingSeries]
62       apply congrArg exponentialGeneratingSeries
63       funext n
64       congr 1
65       omega
66 
67 /-- Exponential-generating coefficients of the transfer section `E_{N,j}(λz)`. -/
68 def transferSectionCoeff (N j : ℕ) (lambda : R) (n : ℕ) : R :=
69   if n % N = j then lambda ^ n else 0
70 
71 /-- Formal transfer section `E_{N,j}(λX)`. -/
72 def transferSection (N j : ℕ) (lambda : R) : R⟦X⟧ :=
73   exponentialGeneratingSeries (transferSectionCoeff N j lambda)
74 
75 @[simp]
76 theorem coeff_transferSection (N j n : ℕ) (lambda : R) :
77     PowerSeries.coeff n (transferSection N j lambda) =
78       transferSectionCoeff N j lambda n *
79         algebraMap ℚ R (1 / (n.factorial : ℚ)) := by
80   simp [transferSection]
81 
82 omit [Algebra ℚ R] in
83 /-- Away from the wraparound, transfer coefficients shift by one and gain `λ`. -/
84 theorem transferSectionCoeff_succ_of_pos {N j : ℕ} (hN : 0 < N)
85     (hj : 0 < j) (hjN : j < N) (lambda : R) (n : ℕ) :
86     transferSectionCoeff N j lambda (n + 1) =
87       lambda * transferSectionCoeff N (j - 1) lambda n := by
88   unfold transferSectionCoeff
89   have hnmod : n % N < N := Nat.mod_lt n hN
90   have hstep : (n + 1) % N = (n % N + 1) % N :=
91     (Nat.mod_add_mod n N 1).symm
92   by_cases h : n % N = j - 1
93   · have hlt : n % N + 1 < N := by omega
94     have hs : (n + 1) % N = j := by
95       rw [hstep, Nat.mod_eq_of_lt hlt]
96       omega
97     simp only [hs, h, ite_true]
98     rw [pow_succ']
99   · have hs : (n + 1) % N ≠ j := by
100       intro hs
101       apply h
102       by_cases hlt : n % N + 1 < N
103       · have heq : (n + 1) % N = n % N + 1 := by
104           rw [hstep, Nat.mod_eq_of_lt hlt]
105         omega
106       · have heq : n % N + 1 = N := by omega
107         have hzero : (n + 1) % N = 0 := by simp [hstep, heq]
108         omega
109     simp [h, hs]
110 
111 omit [Algebra ℚ R] in
112 /-- At the wraparound, transfer coefficients shift by one and gain `λ`. -/
113 theorem transferSectionCoeff_succ_zero {N : ℕ} (hN : 0 < N)
114     (lambda : R) (n : ℕ) :
115     transferSectionCoeff N 0 lambda (n + 1) =
116       lambda * transferSectionCoeff N (N - 1) lambda n := by
117   unfold transferSectionCoeff
118   have hnmod : n % N < N := Nat.mod_lt n hN
119   have hstep : (n + 1) % N = (n % N + 1) % N :=
120     (Nat.mod_add_mod n N 1).symm
121   by_cases h : n % N = N - 1
122   · have heq : n % N + 1 = N := by omega
123     have hs : (n + 1) % N = 0 := by simp [hstep, heq]
124     simp only [hs, h, ite_true]
125     rw [pow_succ']
126   · have hs : (n + 1) % N ≠ 0 := by
127       intro hs
128       apply h
129       by_cases hlt : n % N + 1 < N
130       · have heq : (n + 1) % N = n % N + 1 := by
131           rw [hstep, Nat.mod_eq_of_lt hlt]
132         omega
133       · omega
134     simp [h, hs]
135 
136 /-- Exponential-generating coefficients of the signed section `D_{N,j}`. -/
137 def signedSectionCoeff (N j : ℕ) (n : ℕ) : R :=
138   if n % N = j then (-1 : R) ^ (n / N) else 0
139 
140 /-- Formal signed section `D_{N,j}`. -/
141 def signedSection (N j : ℕ) : R⟦X⟧ :=
142   exponentialGeneratingSeries (signedSectionCoeff (R := R) N j)
143 
144 @[simp]
145 theorem coeff_signedSection (N j n : ℕ) :
146     PowerSeries.coeff n (signedSection (R := R) N j) =
147       signedSectionCoeff (R := R) N j n *
148         algebraMap ℚ R (1 / (n.factorial : ℚ)) := by
149   simp [signedSection]
150 
151 private theorem succ_div_eq_of_mod_succ_lt {N n : ℕ} (hN : 0 < N)
152     (h : n % N + 1 < N) :
153     (n + 1) / N = n / N := by
154   have hOne : 1 < N := by omega
155   rw [Nat.add_div hN, Nat.div_eq_of_lt hOne, Nat.mod_eq_of_lt hOne]
156   simp [Nat.not_le.mpr h]
157 
158 private theorem succ_div_eq_add_one_of_mod_eq_pred {N n : ℕ} (hN : 0 < N)
159     (h : n % N = N - 1) :
160     (n + 1) / N = n / N + 1 := by
161   by_cases hOne : N = 1
162   · subst N
163     simp
164   · have hOneN : 1 < N := by omega
165     rw [Nat.add_div hN, Nat.div_eq_of_lt hOneN, Nat.mod_eq_of_lt hOneN]
166     simp [show N ≤ n % N + 1 by omega]
167 
168 omit [Algebra ℚ R] in
169 /-- Away from the wraparound, signed coefficients shift without changing sign. -/
170 theorem signedSectionCoeff_succ_of_pos {N j : ℕ} (hN : 0 < N)
171     (hj : 0 < j) (hjN : j < N) (n : ℕ) :
172     signedSectionCoeff (R := R) N j (n + 1) =
173       signedSectionCoeff (R := R) N (j - 1) n := by
174   unfold signedSectionCoeff
175   have hnmod : n % N < N := Nat.mod_lt n hN
176   have hstep : (n + 1) % N = (n % N + 1) % N :=
177     (Nat.mod_add_mod n N 1).symm
178   by_cases h : n % N = j - 1
179   · have hlt : n % N + 1 < N := by omega
180     have hs : (n + 1) % N = j := by
181       rw [hstep, Nat.mod_eq_of_lt hlt]
182       omega
183     have hdiv : (n + 1) / N = n / N :=
184       succ_div_eq_of_mod_succ_lt hN hlt
185     simp [h, hs, hdiv]
186   · have hs : (n + 1) % N ≠ j := by
187       intro hs
188       apply h
189       by_cases hlt : n % N + 1 < N
190       · have heq : (n + 1) % N = n % N + 1 := by
191           rw [hstep, Nat.mod_eq_of_lt hlt]
192         omega
193       · have heq : n % N + 1 = N := by omega
194         have hzero : (n + 1) % N = 0 := by simp [hstep, heq]
195         omega
196     simp [h, hs]
197 
198 omit [Algebra ℚ R] in
199 /-- The signed coefficient wraparound contributes exactly one minus sign. -/
200 theorem signedSectionCoeff_succ_zero {N : ℕ} (hN : 0 < N) (n : ℕ) :
201     signedSectionCoeff (R := R) N 0 (n + 1) =
202       -signedSectionCoeff (R := R) N (N - 1) n := by
203   unfold signedSectionCoeff
204   have hnmod : n % N < N := Nat.mod_lt n hN
205   have hstep : (n + 1) % N = (n % N + 1) % N :=
206     (Nat.mod_add_mod n N 1).symm
207   by_cases h : n % N = N - 1
208   · have heq : n % N + 1 = N := by omega
209     have hs : (n + 1) % N = 0 := by simp [hstep, heq]
210     have hdiv : (n + 1) / N = n / N + 1 :=
211       succ_div_eq_add_one_of_mod_eq_pred hN h
212     simp only [hs, h, ite_true, hdiv, pow_succ]
213     ring
214   · have hs : (n + 1) % N ≠ 0 := by
215       intro hs
216       apply h
217       by_cases hlt : n % N + 1 < N
218       · have heq : (n + 1) % N = n % N + 1 := by
219           rw [hstep, Nat.mod_eq_of_lt hlt]
220         omega
221       · omega
222     simp [h, hs]
223 
224 /-- Formal derivative cycle for the nonzero transfer-section labels. -/
225 theorem derivative_transferSection_of_pos {N j : ℕ} (hN : 0 < N)
226     (hj : 0 < j) (hjN : j < N) (lambda : R) :
227     PowerSeries.derivative R (transferSection N j lambda) =
228       PowerSeries.C lambda * transferSection N (j - 1) lambda := by
229   rw [transferSection, derivative_exponentialGeneratingSeries, transferSection]
230   ext n
231   rw [PowerSeries.coeff_C_mul]
232   simp only [coeff_exponentialGeneratingSeries]
233   rw [transferSectionCoeff_succ_of_pos hN hj hjN]
234   ring
235 
236 /-- Formal derivative cycle at the transfer-section wraparound. -/
237 theorem derivative_transferSection_zero {N : ℕ} (hN : 0 < N) (lambda : R) :
238     PowerSeries.derivative R (transferSection N 0 lambda) =
239       PowerSeries.C lambda * transferSection N (N - 1) lambda := by
240   rw [transferSection, derivative_exponentialGeneratingSeries, transferSection]
241   ext n
242   rw [PowerSeries.coeff_C_mul]
243   simp only [coeff_exponentialGeneratingSeries]
244   rw [transferSectionCoeff_succ_zero hN]
245   ring
246 
247 /-- Formal derivative cycle for the nonzero signed-section labels. -/
248 theorem derivative_signedSection_of_pos {N j : ℕ} (hN : 0 < N)
249     (hj : 0 < j) (hjN : j < N) :
250     PowerSeries.derivative R (signedSection (R := R) N j) =
251       signedSection (R := R) N (j - 1) := by
252   rw [signedSection, derivative_exponentialGeneratingSeries, signedSection]
253   ext n
254   simp only [coeff_exponentialGeneratingSeries]
255   rw [signedSectionCoeff_succ_of_pos hN hj hjN]
256 
257 /-- Formal derivative cycle at the signed wraparound, with the required minus sign. -/
258 theorem derivative_signedSection_zero {N : ℕ} (hN : 0 < N) :
259     PowerSeries.derivative R (signedSection (R := R) N 0) =
260       -signedSection (R := R) N (N - 1) := by
261   rw [signedSection, derivative_exponentialGeneratingSeries, signedSection]
262   ext n
263   simp only [coeff_exponentialGeneratingSeries, map_neg]
264   rw [signedSectionCoeff_succ_zero hN]
265   ring
266 
267 omit [Algebra ℚ R] in
268 /-- Advancing by one full block multiplies transfer coefficients by `λ^N`. -/
269 theorem transferSectionCoeff_add_period {N j : ℕ} (_hN : 0 < N)
270     (lambda : R) (n : ℕ) :
271     transferSectionCoeff N j lambda (n + N) =
272       lambda ^ N * transferSectionCoeff N j lambda n := by
273   unfold transferSectionCoeff
274   have hmod : (n + N) % N = n % N := Nat.add_mod_right n N
275   rw [hmod]
276   by_cases h : n % N = j
277   · simp only [h, ite_true]
278     rw [pow_add]
279     ring
280   · simp [h]
281 
282 omit [Algebra ℚ R] in
283 /-- Advancing by one full block reverses the signed coefficient. -/
284 theorem signedSectionCoeff_add_period {N j : ℕ} (hN : 0 < N) (n : ℕ) :
285     signedSectionCoeff (R := R) N j (n + N) =
286       -signedSectionCoeff (R := R) N j n := by
287   unfold signedSectionCoeff
288   have hmod : (n + N) % N = n % N := Nat.add_mod_right n N
289   have hdiv : (n + N) / N = n / N + 1 := by
290     simpa using Nat.add_mul_div_left n 1 hN
291   rw [hmod, hdiv]
292   by_cases h : n % N = j
293   · simp only [h, ite_true, pow_succ]
294     ring
295   · simp [h]
296 
297 /-- Every formal transfer section satisfies the expected `N`th-order equation. -/
298 theorem iterate_derivative_transferSection {N j : ℕ} (hN : 0 < N)
299     (lambda : R) :
300     (PowerSeries.derivative R)^[N] (transferSection N j lambda) =
301       PowerSeries.C (lambda ^ N) * transferSection N j lambda := by
302   rw [transferSection, iterate_derivative_exponentialGeneratingSeries]
303   ext n
304   rw [PowerSeries.coeff_C_mul]
305   simp only [coeff_exponentialGeneratingSeries]
306   rw [transferSectionCoeff_add_period hN]
307   ring
308 
309 /-- Every formal signed section satisfies `D^(N) = -D`. -/
310 theorem iterate_derivative_signedSection {N j : ℕ} (hN : 0 < N) :
311     (PowerSeries.derivative R)^[N] (signedSection (R := R) N j) =
312       -signedSection (R := R) N j := by
313   rw [signedSection, iterate_derivative_exponentialGeneratingSeries]
314   ext n
315   simp only [coeff_exponentialGeneratingSeries, map_neg]
316   rw [signedSectionCoeff_add_period hN]
317   ring
318 
319 /-- Formal initial data for the transfer basis. -/
320 theorem constantCoeff_iterate_derivative_transferSection {N j k : ℕ}
321     (hkN : k < N) (lambda : R) :
322     PowerSeries.constantCoeff
323         ((PowerSeries.derivative R)^[k] (transferSection N j lambda)) =
324       if k = j then lambda ^ j else 0 := by
325   rw [transferSection, iterate_derivative_exponentialGeneratingSeries]
326   rw [← PowerSeries.coeff_zero_eq_constantCoeff]
327   simp only [coeff_exponentialGeneratingSeries, zero_add, Nat.factorial_zero,
328     Nat.cast_one, one_div]
329   rw [transferSectionCoeff]
330   rw [Nat.mod_eq_of_lt hkN]
331   by_cases h : k = j
332   · subst j
333     simp
334   · simp [h]
335 
336 /-- Formal initial data for the signed basis: the derivative matrix is the identity. -/
337 theorem constantCoeff_iterate_derivative_signedSection {N j k : ℕ}
338     (_hjN : j < N) (hkN : k < N) :
339     PowerSeries.constantCoeff
340         ((PowerSeries.derivative R)^[k] (signedSection (R := R) N j)) =
341       if k = j then 1 else 0 := by
342   rw [signedSection, iterate_derivative_exponentialGeneratingSeries]
343   rw [← PowerSeries.coeff_zero_eq_constantCoeff]
344   simp only [coeff_exponentialGeneratingSeries, zero_add, Nat.factorial_zero,
345     Nat.cast_one, one_div]
346   rw [signedSectionCoeff]
347   rw [Nat.mod_eq_of_lt hkN]
348   by_cases h : k = j
349   · subst j
350     simp [Nat.div_eq_of_lt hkN]
351   · simp [h]
352 
353 end
354 
355 end Komorebi.PaperIV

Back to source controls