ReciprocalCore.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIV.FormalExponential
7 import KomorebiPaperIV.SectionCycles
8 import Mathlib.RingTheory.PowerSeries.Log
9 
10 /-!
11 # Manuscript-facing reciprocal core
12 
13 This file names the reduced denominator, its formal negative logarithm, and
14 the reciprocal parameter family used in Paper IV.  It closes the semantic gap
15 between the generic family `formalExpFamily L r` and the manuscript's exact
16 specialization `L = -log Delta_N`.
17 -/
18 
19 namespace Komorebi.PaperIV
20 
21 open scoped PowerSeries
22 
23 noncomputable section
24 
25 variable {R : Type*} [CommRing R] [Algebra ℚ R]
26 
27 /-- The reduced denominator `Delta_N(w) = sum (-1)^n w^n / (Nn)!`. -/
28 def reducedDenominator (N : ℕ) : R⟦X⟧ :=
29   PowerSeries.mk fun n =>
30     algebraMap ℚ R ((-1 : ℚ) ^ n / ((N * n).factorial : ℚ))
31 
32 @[simp]
33 theorem coeff_reducedDenominator (N n : ℕ) :
34     PowerSeries.coeff n (reducedDenominator (R := R) N) =
35       algebraMap ℚ R ((-1 : ℚ) ^ n / ((N * n).factorial : ℚ)) := by
36   simp [reducedDenominator]
37 
38 @[simp]
39 theorem constantCoeff_reducedDenominator (N : ℕ) :
40     PowerSeries.constantCoeff (reducedDenominator (R := R) N) = 1 := by
41   rw [← PowerSeries.coeff_zero_eq_constantCoeff]
42   simp
43 
44 /-- The signed denominator in the `z` variable is obtained from the reduced
45 denominator by the substitution `w = z^N`. -/
46 theorem signedSection_zero_eq_expand_reducedDenominator {N : ℕ} (hN : 0 < N) :
47     signedSection (R := R) N 0 =
48       (reducedDenominator (R := R) N).expand N hN.ne' := by
49   ext n
50   rw [coeff_signedSection, PowerSeries.coeff_expand]
51   by_cases hdvd : N ∣ n
52   · have hmod : n % N = 0 := Nat.dvd_iff_mod_eq_zero.mp hdvd
53     have hmul : N * (n / N) = n := Nat.mul_div_cancel' hdvd
54     simp only [hdvd, ↓reduceIte, signedSectionCoeff, hmod]
55     rw [coeff_reducedDenominator, hmul]
56     simp only [div_eq_mul_inv, map_mul, map_pow, map_neg, map_one]
57     ring
58   · have hmod : n % N ≠ 0 := by
59       simpa [Nat.dvd_iff_mod_eq_zero] using hdvd
60     simp [hdvd, signedSectionCoeff, hmod]
61 
62 /-- The formal series `-log Delta_N`, normalized to have constant term zero. -/
63 def negativeLogDenominator (N : ℕ) : R⟦X⟧ :=
64   -PowerSeries.logOf (reducedDenominator (R := R) N)
65 
66 @[simp]
67 theorem constantCoeff_negativeLogDenominator (N : ℕ) :
68     PowerSeries.constantCoeff (negativeLogDenominator (R := R) N) = 0 := by
69   simp [negativeLogDenominator, PowerSeries.constantCoeff_logOf]
70 
71 /-- Exponentiating the formal logarithm of a unit-constant series returns the
72 series.  This bridge is not provided as a named general theorem by the pinned
73 PowerSeries API. -/
74 theorem exp_subst_logOf {f : R⟦X⟧} (hf : f.constantCoeff = 1) :
75     (PowerSeries.exp R).subst (PowerSeries.logOf f) = f := by
76   have hzero : (f - 1).constantCoeff = 0 := by
77     rw [map_sub, map_one, hf, sub_self]
78   let hsub : PowerSeries.HasSubst (f - 1) :=
79     PowerSeries.HasSubst.of_constantCoeff_zero' hzero
80   rw [PowerSeries.logOf_eq]
81   rw [← PowerSeries.subst_comp_subst_apply PowerSeries.HasSubst.log hsub]
82   rw [PowerSeries.subst_exp_log]
83   rw [PowerSeries.subst_add hsub, PowerSeries.subst_X hsub]
84   rw [← PowerSeries.coe_substAlgHom hsub, map_one]
85   ring
86 
87 /-- Formal logarithmic differentiation for a unit-constant series. -/
88 theorem mul_derivative_logOf {f : R⟦X⟧} (hf : f.constantCoeff = 1) :
89     f * PowerSeries.derivative R (PowerSeries.logOf f) =
90       PowerSeries.derivative R f := by
91   have hlog : (PowerSeries.logOf f).constantCoeff = 0 :=
92     PowerSeries.constantCoeff_logOf hf
93   let hsub : PowerSeries.HasSubst (PowerSeries.logOf f) :=
94     PowerSeries.HasSubst.of_constantCoeff_zero' hlog
95   have h := congrArg (PowerSeries.derivative R) (exp_subst_logOf hf)
96   rw [PowerSeries.derivative_subst hsub, PowerSeries.derivative_exp] at h
97   rwa [exp_subst_logOf hf] at h
98 
99 /-- A zero-constant exponential family is `exp (rL)` as a single
100 substitution. -/
101 theorem formalExpFamily_eq_exp_subst {L : R⟦X⟧} (hL : L.constantCoeff = 0)
102     (r : R) :
103     formalExpFamily L r = (PowerSeries.exp R).subst (PowerSeries.C r * L) := by
104   let hLsub : PowerSeries.HasSubst L :=
105     PowerSeries.HasSubst.of_constantCoeff_zero' hL
106   rw [formalExpFamily, PowerSeries.rescale_eq_subst]
107   rw [PowerSeries.subst_comp_subst_apply (PowerSeries.HasSubst.smul_X' r) hLsub]
108   rw [PowerSeries.subst_smul hLsub, PowerSeries.subst_X hLsub]
109   rw [PowerSeries.smul_eq_C_mul]
110 
111 /-- Paper IV's formal reciprocal family `Delta_N(w)^(-r)`. -/
112 def reciprocalSeries (N : ℕ) (r : R) : R⟦X⟧ :=
113   formalExpFamily (negativeLogDenominator (R := R) N) r
114 
115 @[simp]
116 theorem constantCoeff_reciprocalSeries (N : ℕ) (r : R) :
117     PowerSeries.constantCoeff (reciprocalSeries N r) = 1 := by
118   rw [reciprocalSeries, formalExpFamily]
119   change MvPowerSeries.constantCoeff
120       ((PowerSeries.rescale r (PowerSeries.exp R)).subst
121         (negativeLogDenominator N)) = 1
122   rw [PowerSeries.constantCoeff_subst_of_constantCoeff_zero
123     (constantCoeff_negativeLogDenominator N)]
124   rw [← PowerSeries.coeff_zero_eq_constantCoeff, PowerSeries.coeff_rescale]
125   simp
126 
127 @[simp]
128 theorem reciprocalSeries_zero (N : ℕ) :
129     reciprocalSeries (R := R) N 0 = 1 := by
130   exact formalExpFamily_zero (constantCoeff_negativeLogDenominator N)
131 
132 /-- Parameter `-1` recovers the denominator itself. -/
133 theorem reciprocalSeries_neg_one (N : ℕ) :
134     reciprocalSeries (R := R) N (-1) = reducedDenominator N := by
135   rw [reciprocalSeries,
136     formalExpFamily_eq_exp_subst (constantCoeff_negativeLogDenominator N)]
137   rw [negativeLogDenominator]
138   have h := exp_subst_logOf (constantCoeff_reducedDenominator (R := R) N)
139   simpa using h
140 
141 /-- Exact additive parameter law for the manuscript's named reciprocal family. -/
142 theorem reciprocalSeries_add (N : ℕ) (r s : R) :
143     reciprocalSeries N r * reciprocalSeries N s = reciprocalSeries N (r + s) := by
144   exact formalExpFamily_semigroup (constantCoeff_negativeLogDenominator N) r s
145 
146 section Field
147 
148 variable {K : Type*} [Field K] [Algebra ℚ K]
149 
150 /-- Parameter `1` is exactly the formal inverse of `Delta_N`. -/
151 theorem reciprocalSeries_one_eq_inverse (N : ℕ) :
152     reciprocalSeries (R := K) N 1 = (reducedDenominator N)⁻¹ := by
153   apply (PowerSeries.eq_inv_iff_mul_eq_one
154     (by simp : PowerSeries.constantCoeff (reducedDenominator (R := K) N) ≠ 0)).2
155   rw [← reciprocalSeries_neg_one (R := K) N]
156   rw [reciprocalSeries_add, add_neg_cancel, reciprocalSeries_zero]
157 
158 end Field
159 
160 /-- Factorially normalized coefficients `P_{N,n}(r)`. -/
161 def reciprocalCoeff (N n : ℕ) (r : R) : R :=
162   blockCoeff N n (reciprocalSeries N r)
163 
164 /-- Ordinary `w`-coefficient `b_{N,n}(r) = P_{N,n}(r)/(Nn)!`. -/
165 def reciprocalOrdCoeff (N n : ℕ) (r : R) : R :=
166   PowerSeries.coeff n (reciprocalSeries N r)
167 
168 @[simp]
169 theorem reciprocalCoeff_zero_parameter (N : ℕ) :
170     reciprocalCoeff (R := R) N 0 0 = 1 := by
171   simp [reciprocalCoeff, blockCoeff]
172 
173 theorem reciprocalCoeff_zero_parameter_of_pos (N : ℕ) {n : ℕ} (hn : 0 < n) :
174     reciprocalCoeff (R := R) N n 0 = 0 := by
175   simp [reciprocalCoeff, blockCoeff, hn.ne']
176 
177 /-- Exact block-convolution law for `P_{N,n}(r+s)`. -/
178 theorem reciprocalCoeff_addition (N n : ℕ) (r s : R) :
179     reciprocalCoeff N n (r + s) =
180       ∑ q ∈ Finset.range (n + 1),
181         ((N * n).choose (N * q) : R) *
182           reciprocalCoeff N q r * reciprocalCoeff N (n - q) s := by
183   exact reciprocal_block_convolution
184     (constantCoeff_negativeLogDenominator N) N n r s
185 
186 /-- Logarithmic coefficients in the normalization
187 `-log Delta_N = sum kappa_{N,m} X^m / m`.
188 
189 The value at `m = 0` is harmless and is not used by the manuscript.
190 -/
191 def kappaCoeff (N m : ℕ) : R :=
192   (m : R) * PowerSeries.coeff m (negativeLogDenominator (R := R) N)
193 
194 /-- Reduced logarithmic derivative `-Delta_N'/Delta_N`. -/
195 def reducedTangentSeries (N : ℕ) : R⟦X⟧ :=
196   PowerSeries.derivative R (negativeLogDenominator (R := R) N)
197 
198 @[simp]
199 theorem coeff_reducedTangentSeries (N n : ℕ) :
200     PowerSeries.coeff n (reducedTangentSeries (R := R) N) =
201       kappaCoeff N (n + 1) := by
202   rw [reducedTangentSeries, PowerSeries.coeff_derivative, kappaCoeff]
203   simp only [Nat.cast_add, Nat.cast_one]
204   ring
205 
206 /-- Exact formal logarithmic-derivative identity for the reduced denominator. -/
207 theorem reducedDenominator_mul_reducedTangentSeries (N : ℕ) :
208     reducedDenominator (R := R) N * reducedTangentSeries N =
209       -PowerSeries.derivative R (reducedDenominator N) := by
210   rw [reducedTangentSeries, negativeLogDenominator, map_neg]
211   simpa using
212     congrArg Neg.neg
213       (mul_derivative_logOf (constantCoeff_reducedDenominator (R := R) N))
214 
215 /-- Coefficient recurrence obtained from
216 `Delta_N * (-Delta_N' / Delta_N) = -Delta_N'`. -/
217 theorem reducedTangent_coefficient_convolution (N n : ℕ) :
218     (∑ p ∈ Finset.antidiagonal n,
219         PowerSeries.coeff p.1 (reducedDenominator (R := R) N) *
220           kappaCoeff N (p.2 + 1)) =
221       -(PowerSeries.coeff (n + 1) (reducedDenominator N) * (n + 1 : R)) := by
222   have h := congrArg (PowerSeries.coeff (R := R) n)
223     (reducedDenominator_mul_reducedTangentSeries (R := R) N)
224   rw [PowerSeries.coeff_mul, map_neg, PowerSeries.coeff_derivative] at h
225   simpa only [coeff_reducedTangentSeries] using h
226 
227 /-- The generic formal derivative theorem specialized to `Delta_N^(-r)`. -/
228 theorem derivative_reciprocalSeries (N : ℕ) (r : R) :
229     PowerSeries.derivative R (reciprocalSeries N r) =
230       PowerSeries.C r * reciprocalSeries N r *
231         PowerSeries.derivative R (negativeLogDenominator N) := by
232   exact derivative_formalExpFamily (constantCoeff_negativeLogDenominator N) r
233 
234 /-- Finite Newton recurrence specialized to the named reciprocal family. -/
235 theorem reciprocalSeries_coefficient_recurrence (N : ℕ) (r : R) (n : ℕ) :
236     (n + 1 : R) * PowerSeries.coeff (n + 1) (reciprocalSeries N r) =
237       r * ∑ p ∈ Finset.antidiagonal n,
238         PowerSeries.coeff p.1 (reciprocalSeries N r) *
239           ((p.2 + 1 : R) *
240             PowerSeries.coeff (p.2 + 1) (negativeLogDenominator N)) := by
241   exact formalExpFamily_coefficient_recurrence
242     (constantCoeff_negativeLogDenominator N) r n
243 
244 /-- Manuscript Newton recurrence in an equivalent antidiagonal indexing. -/
245 theorem reciprocalOrdCoeff_newton (N : ℕ) (r : R) (n : ℕ) :
246     (n + 1 : R) * reciprocalOrdCoeff N (n + 1) r =
247       r * ∑ p ∈ Finset.antidiagonal n,
248         reciprocalOrdCoeff N p.1 r * kappaCoeff N (p.2 + 1) := by
249   simpa [reciprocalOrdCoeff, kappaCoeff] using
250     reciprocalSeries_coefficient_recurrence (R := R) N r n
251 
252 end
253 
254 end Komorebi.PaperIV

Back to source controls