EarlyCompletion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIV.FiniteAnalytic
7 import Mathlib.RingTheory.MvPowerSeries.Basic
8 
9 /-!
10 # Early algebraic completion for Paper IV
11 
12 This file supplies formal-power-series counterparts of the early algebraic
13 results that were not included in checkpoint 0.2.0: the covariance
14 characterization of cyclic packets, the transfer and signed addition laws, and
15 the coefficient-level rotational and conjugation symmetries of the signed
16 denominator.
17 
18 The addition laws are identities in two-variable formal power series.  The
19 definition `bivariateExponentialGeneratingSeries` is precisely the formal
20 expansion of an exponential generating series after replacing its variable by
21 `X₀ + X₁`; `separatedExponentialGeneratingSeries` is the separated product in
22 the two variables.  No analytic convergence or pointwise evaluation is used.
23 -/
24 
25 namespace Komorebi.PaperIV
26 
27 open scoped PowerSeries
28 
29 noncomputable section
30 
31 /-! ## Formal covariance -/
32 
33 /-- A formal series is fixed by the `j`th cyclic projector exactly when it has
34 weight `j` under rescaling by a primitive `N`th root of unity. -/
35 theorem cyclicProjector_fixed_iff_rescale_covariant {N j : ℕ} (hN : 0 < N)
36     (hjN : j < N) {omega : ℂ} (homega : IsPrimitiveRoot omega N)
37     (f : ℂ⟦X⟧) :
38     cyclicProjector N j f = f ↔
39       PowerSeries.rescale omega f = PowerSeries.C (omega ^ j) * f := by
40   constructor
41   · intro hfixed
42     ext n
43     have hcoeff := congrArg (PowerSeries.coeff n) hfixed
44     rw [coeff_cyclicProjector, Nat.mod_eq_of_lt hjN] at hcoeff
45     rw [PowerSeries.coeff_rescale, PowerSeries.coeff_C_mul]
46     by_cases hres : n % N = j
47     · have hpow : omega ^ n = omega ^ j := by
48         apply (homega.isOfFinOrder hN.ne').pow_eq_pow_iff_modEq.mpr
49         rw [← homega.eq_orderOf]
50         exact hres.trans (Nat.mod_eq_of_lt hjN).symm
51       rw [hpow]
52     · simp [hres] at hcoeff
53       simp [hcoeff]
54   · intro hcov
55     ext n
56     rw [coeff_cyclicProjector, Nat.mod_eq_of_lt hjN]
57     by_cases hres : n % N = j
58     · simp [hres]
59     · simp only [hres, ↓reduceIte]
60       have hcoeff := congrArg (PowerSeries.coeff n) hcov
61       rw [PowerSeries.coeff_rescale, PowerSeries.coeff_C_mul] at hcoeff
62       have hpow : omega ^ n ≠ omega ^ j := by
63         intro heq
64         have hmodeq :=
65           (homega.isOfFinOrder hN.ne').pow_eq_pow_iff_modEq.mp heq
66         have hmod : n % N = j % N := by
67           simpa only [homega.eq_orderOf, Nat.ModEq] using hmodeq
68         exact hres (by simpa [Nat.mod_eq_of_lt hjN] using hmod)
69       have hzero : (omega ^ n - omega ^ j) * PowerSeries.coeff n f = 0 := by
70         rw [sub_mul, hcoeff, sub_self]
71       exact ((mul_eq_zero.mp hzero).resolve_left (sub_ne_zero.mpr hpow)).symm
72 
73 /-- Range formulation of the formal covariance characterization. -/
74 theorem cyclicProjector_mem_range_iff_rescale_covariant {N j : ℕ} (hN : 0 < N)
75     (hjN : j < N) {omega : ℂ} (homega : IsPrimitiveRoot omega N)
76     (f : ℂ⟦X⟧) :
77     (∃ g : ℂ⟦X⟧, cyclicProjector N j g = f) ↔
78       PowerSeries.rescale omega f = PowerSeries.C (omega ^ j) * f := by
79   rw [← cyclicProjector_fixed_iff_rescale_covariant hN hjN homega]
80   constructor
81   · rintro ⟨g, rfl⟩
82     exact cyclicProjector_idempotent N j g
83   · intro hfixed
84     exact ⟨f, hfixed⟩
85 
86 /-! ## Two-variable exponential-generating series -/
87 
88 /-- The two-variable formal expansion of an EGF after the substitution
89 `X ↦ X₀ + X₁`. -/
90 def bivariateExponentialGeneratingSeries {R : Type*} [CommRing R] [Algebra ℚ R]
91     (a : ℕ → R) : MvPowerSeries (Fin 2) R :=
92   fun d =>
93     a (d 0 + d 1) * algebraMap ℚ R (1 / (d 0).factorial : ℚ) *
94       algebraMap ℚ R (1 / (d 1).factorial : ℚ)
95 
96 @[simp]
97 theorem coeff_bivariateExponentialGeneratingSeries {R : Type*}
98     [CommRing R] [Algebra ℚ R] (a : ℕ → R) (d : Fin 2 →₀ ℕ) :
99     MvPowerSeries.coeff d (bivariateExponentialGeneratingSeries a) =
100       a (d 0 + d 1) * algebraMap ℚ R (1 / (d 0).factorial : ℚ) *
101         algebraMap ℚ R (1 / (d 1).factorial : ℚ) :=
102   rfl
103 
104 /-- The product of two EGFs placed in the two separate formal variables. -/
105 def separatedExponentialGeneratingSeries {R : Type*} [CommRing R] [Algebra ℚ R]
106     (a b : ℕ → R) : MvPowerSeries (Fin 2) R :=
107   fun d =>
108     (a (d 0) * algebraMap ℚ R (1 / (d 0).factorial : ℚ)) *
109       (b (d 1) * algebraMap ℚ R (1 / (d 1).factorial : ℚ))
110 
111 @[simp]
112 theorem coeff_separatedExponentialGeneratingSeries {R : Type*}
113     [CommRing R] [Algebra ℚ R] (a b : ℕ → R) (d : Fin 2 →₀ ℕ) :
114     MvPowerSeries.coeff d (separatedExponentialGeneratingSeries a b) =
115       (a (d 0) * algebraMap ℚ R (1 / (d 0).factorial : ℚ)) *
116         (b (d 1) * algebraMap ℚ R (1 / (d 1).factorial : ℚ)) :=
117   rfl
118 
119 /-! ## Transfer addition -/
120 
121 private theorem transferSectionCoeff_addition {R : Type*} [CommRing R]
122     {N k : ℕ} (hN : 0 < N) (lambda : R) (a b : ℕ) :
123     transferSectionCoeff N k lambda (a + b) =
124       ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
125         if (i + j) % N = k then
126           transferSectionCoeff N i lambda a * transferSectionCoeff N j lambda b
127         else 0 := by
128   rw [Finset.sum_eq_single (a % N)]
129   · rw [Finset.sum_eq_single (b % N)]
130     · simp only [transferSectionCoeff]
131       change (if (a + b) % N = k then lambda ^ (a + b) else 0) =
132         if (a % N + b % N) % N = k then lambda ^ a * lambda ^ b else 0
133       rw [← Nat.add_mod, pow_add]
134     · intro j hj hne
135       have hb : b % N ≠ j := by simpa [eq_comm] using hne
136       simp [transferSectionCoeff, hb]
137     · exact fun hmem => (hmem (Finset.mem_range.mpr (Nat.mod_lt b hN))).elim
138   · intro i hi hne
139     have ha : a % N ≠ i := by simpa [eq_comm] using hne
140     simp [transferSectionCoeff, ha]
141   · exact fun hmem => (hmem (Finset.mem_range.mpr (Nat.mod_lt a hN))).elim
142 
143 /-- Exact bivariate formal-power-series addition law for transfer sections. -/
144 theorem transferSection_addition {R : Type*} [CommRing R] [Algebra ℚ R]
145     {N k : ℕ} (hN : 0 < N) (_hkN : k < N) (lambda : R) :
146     bivariateExponentialGeneratingSeries (transferSectionCoeff N k lambda) =
147       ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
148         if (i + j) % N = k then
149           separatedExponentialGeneratingSeries
150             (transferSectionCoeff N i lambda) (transferSectionCoeff N j lambda)
151         else 0 := by
152   ext d
153   simp only [coeff_bivariateExponentialGeneratingSeries, map_sum]
154   rw [transferSectionCoeff_addition hN]
155   simp only [Finset.sum_mul]
156   apply Finset.sum_congr rfl
157   intro i hi
158   apply Finset.sum_congr rfl
159   intro j hj
160   by_cases hlabel : (i + j) % N = k
161   · simp [hlabel, coeff_separatedExponentialGeneratingSeries]
162     ring
163   · simp [hlabel]
164 
165 /-! ## Signed addition -/
166 
167 private theorem signedSectionCoeff_addition {R : Type*} [CommRing R]
168     {N k : ℕ} (hN : 0 < N) (a b : ℕ) :
169     signedSectionCoeff (R := R) N k (a + b) =
170       ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
171         if (i + j) % N = k then
172           (-1 : R) ^ ((i + j) / N) *
173             signedSectionCoeff (R := R) N i a *
174               signedSectionCoeff (R := R) N j b
175         else 0 := by
176   rw [Finset.sum_eq_single (a % N)]
177   · rw [Finset.sum_eq_single (b % N)]
178     · simp only [signedSectionCoeff]
179       change (if (a + b) % N = k then (-1 : R) ^ ((a + b) / N) else 0) =
180         if (a % N + b % N) % N = k then
181           (-1 : R) ^ ((a % N + b % N) / N) *
182             (-1 : R) ^ (a / N) * (-1 : R) ^ (b / N)
183         else 0
184       rw [← Nat.add_mod]
185       by_cases hres : (a + b) % N = k
186       · simp only [hres, ↓reduceIte]
187         rw [Nat.add_div hN]
188         by_cases hcarry : N ≤ a % N + b % N
189         · simp only [hcarry, ↓reduceIte]
190           have hq : (a % N + b % N) / N = 1 := by
191             apply Nat.le_antisymm
192             · exact Nat.div_le_iff_le_mul hN |>.2 (by
193                 have ha := Nat.mod_lt a hN
194                 have hb := Nat.mod_lt b hN
195                 omega)
196             · exact Nat.le_div_iff_mul_le hN |>.2 (by simpa using hcarry)
197           rw [hq, pow_add, pow_add]
198           ring
199         · simp only [hcarry, ↓reduceIte]
200           have hq : (a % N + b % N) / N = 0 :=
201             Nat.div_eq_of_lt (Nat.lt_of_not_ge hcarry)
202           simp only [hq, pow_zero, mul_one, pow_add]
203           ring
204       · simp only [hres, ↓reduceIte]
205     · intro j hj hne
206       have hb : b % N ≠ j := by simpa [eq_comm] using hne
207       simp [signedSectionCoeff, hb]
208     · exact fun hmem => (hmem (Finset.mem_range.mpr (Nat.mod_lt b hN))).elim
209   · intro i hi hne
210     have ha : a % N ≠ i := by simpa [eq_comm] using hne
211     simp [signedSectionCoeff, ha]
212   · exact fun hmem => (hmem (Finset.mem_range.mpr (Nat.mod_lt a hN))).elim
213 
214 /-- Exact bivariate formal-power-series twisted addition law for signed
215 sections.  Since `i,j < N`, the displayed exponent `(i+j)/N` is the manuscript's
216 carry `⌊(i+j)/N⌋`, hence is either zero or one. -/
217 theorem signedSection_addition {R : Type*} [CommRing R] [Algebra ℚ R]
218     {N k : ℕ} (hN : 0 < N) (_hkN : k < N) :
219     bivariateExponentialGeneratingSeries
220         (signedSectionCoeff (R := R) N k) =
221       ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
222         if (i + j) % N = k then
223           MvPowerSeries.C ((-1 : R) ^ ((i + j) / N)) *
224             separatedExponentialGeneratingSeries
225               (signedSectionCoeff (R := R) N i)
226               (signedSectionCoeff (R := R) N j)
227         else 0 := by
228   ext d
229   simp only [coeff_bivariateExponentialGeneratingSeries, map_sum]
230   rw [signedSectionCoeff_addition hN]
231   simp only [Finset.sum_mul]
232   apply Finset.sum_congr rfl
233   intro i hi
234   apply Finset.sum_congr rfl
235   intro j hj
236   by_cases hlabel : (i + j) % N = k
237   · simp only [hlabel, ↓reduceIte]
238     rw [MvPowerSeries.coeff_C_mul,
239       coeff_separatedExponentialGeneratingSeries]
240     ring
241   · simp only [hlabel, ↓reduceIte, MvPowerSeries.coeff_zero]
242     ring
243 
244 /-! ## Distinguished-denominator symmetries -/
245 
246 /-- Coefficient-level rotational invariance of the signed denominator. -/
247 theorem signedDenominator_rescale_of_pow_eq_one {R : Type*} [CommRing R]
248     [Algebra ℚ R] {N : ℕ} {omega : R}
249     (homega : omega ^ N = 1) :
250     PowerSeries.rescale omega (signedSection (R := R) N 0) =
251       signedSection (R := R) N 0 := by
252   ext n
253   rw [PowerSeries.coeff_rescale, coeff_signedSection]
254   rw [signedSectionCoeff]
255   by_cases hres : n % N = 0
256   · simp only [hres, ↓reduceIte]
257     have hn : n = N * (n / N) := by
258       simpa [hres] using (Nat.div_add_mod n N).symm
259     rw [hn, pow_mul, homega, one_pow, one_mul]
260   · simp [hres]
261 
262 /-- Coefficientwise complex conjugation fixes the signed denominator. -/
263 theorem signedDenominator_map_conj (N : ℕ) :
264     PowerSeries.map (starRingEnd ℂ)
265         (signedSection (R := ℂ) N 0) =
266       signedSection (R := ℂ) N 0 := by
267   ext n
268   rw [PowerSeries.coeff_map, coeff_signedSection]
269   by_cases hres : n % N = 0
270   · simp [signedSectionCoeff, hres]
271   · simp [signedSectionCoeff, hres]
272 
273 end
274 
275 end Komorebi.PaperIV

Back to source controls