HypergeometricCompletion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIV.SectionCycles
7 import Mathlib.Data.Nat.Factorial.BigOperators
8 import Mathlib.RingTheory.Polynomial.Pochhammer
9 import Mathlib.RingTheory.PowerSeries.Expand
10 
11 /-!
12 # Hypergeometric coefficient completion for Paper IV
13 
14 This file proves the factorial/Pochhammer normalization behind the
15 hypergeometric form of the transfer sections.  The proof is elementary and
16 coefficient-level: it groups each factorial block into the `N` rational
17 parameters `(j+a+1)/N`, for `0 ≤ a < N`.
18 
19 The full parameter lattice contains one parameter equal to `1` when `j < N`.
20 Its Pochhammer symbol is `q!`; deleting that entry therefore gives exactly the
21 usual denominator-parameter list for the manuscript's ordinary
22 `₀F_{N-1}`.  We package the ordinary hypergeometric coefficient directly as a
23 formal power series, avoiding analytic convergence claims and the regularized
24 Gamma normalization used by Mathlib's analytic generalized hypergeometric
25 function.
26 -/
27 
28 namespace Komorebi.PaperIV
29 
30 open scoped PowerSeries
31 
32 noncomputable section
33 
34 /-- Product of the `N` Pochhammer factors in the full residue-parameter
35 lattice.  For `j < N`, the factor indexed by `N-j-1` is `(1)_q = q!`. -/
36 def residuePochhammerProduct (N j q : ℕ) : ℚ :=
37   ∏ a ∈ Finset.range N,
38     (ascPochhammer ℚ q).eval (((j + a + 1 : ℕ) : ℚ) / (N : ℚ))
39 
40 private theorem scaled_parameter_step_product {N : ℕ} (hN : 0 < N)
41     (j q : ℕ) :
42     (N : ℚ) ^ N *
43         ∏ a ∈ Finset.range N,
44           (((j + a + 1 : ℕ) : ℚ) / (N : ℚ) + (q : ℚ)) =
45       ((j + N * q + 1).ascFactorial N : ℚ) := by
46   have hNq : (N : ℚ) ≠ 0 := by exact_mod_cast hN.ne'
47   simp_rw [show ∀ a : ℕ,
48       ((j + a + 1 : ℕ) : ℚ) / (N : ℚ) + (q : ℚ) =
49         ((j + N * q + 1 + a : ℕ) : ℚ) / (N : ℚ) by
50     intro a
51     field_simp
52     push_cast
53     ring]
54   rw [Finset.prod_div_distrib]
55   simp only [Finset.prod_const, Finset.card_range]
56   field_simp
57   rw [Nat.ascFactorial_eq_prod_range, Nat.cast_prod]
58 
59 /-- Exact factorial split used in the proof of the hypergeometric form:
60 `(Nq+j)! = j! N^(Nq) ∏ₐ ((j+a+1)/N)_q`. -/
61 theorem factorial_eq_residuePochhammerProduct {N : ℕ} (hN : 0 < N)
62     (j q : ℕ) :
63     (j.factorial : ℚ) * (N : ℚ) ^ (N * q) *
64         residuePochhammerProduct N j q =
65       ((N * q + j).factorial : ℚ) := by
66   induction q with
67   | zero => simp [residuePochhammerProduct]
68   | succ q ih =>
69       rw [residuePochhammerProduct]
70       simp_rw [ascPochhammer_succ_right, Polynomial.eval_mul,
71         Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_natCast]
72       rw [Finset.prod_mul_distrib]
73       rw [Nat.mul_succ, pow_add]
74       change
75         (j.factorial : ℚ) * ((N : ℚ) ^ (N * q) * (N : ℚ) ^ N) *
76             (residuePochhammerProduct N j q *
77               ∏ a ∈ Finset.range N,
78                 (((j + a + 1 : ℕ) : ℚ) / (N : ℚ) + (q : ℚ))) =
79           (((N * q + N) + j).factorial : ℚ)
80       calc
81         _ = ((j.factorial : ℚ) * (N : ℚ) ^ (N * q) *
82               residuePochhammerProduct N j q) *
83             ((N : ℚ) ^ N *
84               ∏ a ∈ Finset.range N,
85                 (((j + a + 1 : ℕ) : ℚ) / (N : ℚ) + (q : ℚ))) := by ring
86         _ = ((N * q + j).factorial : ℚ) *
87             ((j + N * q + 1).ascFactorial N : ℚ) := by
88               rw [ih, scaled_parameter_step_product hN]
89         _ = (((N * q + N) + j).factorial : ℚ) := by
90               norm_cast
91               simpa [add_assoc, add_comm, add_left_comm] using
92                 Nat.factorial_mul_ascFactorial (N * q + j) N
93 
94 /-- The coefficient of the ordinary `₀F_{N-1}` after retaining the full
95 parameter lattice.  The unique `(1)_q=q!` factor is already present in
96 `residuePochhammerProduct`, so no additional factorial occurs here. -/
97 def residueZeroFCoeff (N j q : ℕ) : ℚ :=
98   (residuePochhammerProduct N j q)⁻¹
99 
100 /-- Formal hypergeometric series in the compressed variable. -/
101 def residueZeroFSeries (N j : ℕ) : ℚ⟦X⟧ :=
102   PowerSeries.mk fun q => residueZeroFCoeff N j q
103 
104 @[simp]
105 theorem coeff_residueZeroFSeries (N j q : ℕ) :
106     PowerSeries.coeff q (residueZeroFSeries N j) =
107       residueZeroFCoeff N j q := by
108   simp [residueZeroFSeries]
109 
110 /-- Coefficient form of the manuscript's hypergeometric identity.  It states
111 that the `q`th compressed hypergeometric term, including `j!` and `N^(Nq)`,
112 is exactly the factorial denominator of the transfer section. -/
113 theorem residueZeroFCoeff_normalization {N : ℕ} (hN : 0 < N)
114     (j q : ℕ) :
115     (j.factorial : ℚ)⁻¹ * ((N : ℚ) ^ (N * q))⁻¹ *
116         residueZeroFCoeff N j q =
117       (((N * q + j).factorial : ℚ))⁻¹ := by
118   rw [residueZeroFCoeff]
119   rw [← mul_inv, ← mul_inv]
120   rw [factorial_eq_residuePochhammerProduct hN]
121 
122 /-- The omitted manuscript parameter is exactly `1`. -/
123 theorem residueParameter_eq_one {N j : ℕ} (hN : 0 < N) (hjN : j < N) :
124     (((j + (N - j - 1) + 1 : ℕ) : ℚ) / (N : ℚ)) = 1 := by
125   have hindex : j + (N - j - 1) + 1 = N := by omega
126   rw [hindex]
127   norm_num [show (N : ℚ) ≠ 0 by exact_mod_cast hN.ne']
128 
129 /-- The Pochhammer factor at the omitted parameter is `q!`. -/
130 theorem omitted_residuePochhammer_eq_factorial {N j : ℕ} (hN : 0 < N)
131     (hjN : j < N) (q : ℕ) :
132     (ascPochhammer ℚ q).eval
133         (((j + (N - j - 1) + 1 : ℕ) : ℚ) / (N : ℚ)) =
134       (q.factorial : ℚ) := by
135   rw [residueParameter_eq_one hN hjN]
136   exact ascPochhammer_eval_one ℚ q
137 
138 /-- Exact formal-power-series version of the manuscript's hypergeometric
139 formula, over the rational coefficient field.  The right side is
140 
141 `(λX)^j / j! · ₀F_{N-1}(; A_{N,j}; (λX)^N / N^N)`,
142 
143 with `residueZeroFSeries` carrying the ordinary hypergeometric coefficients.
144 -/
145 theorem transferSection_eq_residueZeroFSeries {N j : ℕ} (hN : 0 < N)
146     (hjN : j < N) (lambda : ℚ) :
147     transferSection N j lambda =
148       PowerSeries.C (lambda ^ j * (j.factorial : ℚ)⁻¹) *
149         (PowerSeries.X ^ j *
150           (PowerSeries.rescale
151               (lambda ^ N * ((N : ℚ) ^ N)⁻¹)
152               (residueZeroFSeries N j)).expand N hN.ne') := by
153   ext n
154   rw [coeff_transferSection, PowerSeries.coeff_C_mul]
155   rw [PowerSeries.coeff_X_pow_mul']
156   by_cases hres : n % N = j
157   · have hjle : j ≤ n := by
158       rw [← hres]
159       exact Nat.mod_le n N
160     have hn : n = N * (n / N) + j := by
161       calc
162         n = N * (n / N) + n % N := (Nat.div_add_mod n N).symm
163         _ = N * (n / N) + j := by rw [hres]
164     have hsub : n - j = N * (n / N) := by omega
165     have hdvd : N ∣ n - j := ⟨n / N, hsub⟩
166     have hdiv : (n - j) / N = n / N := by
167       rw [hsub, Nat.mul_div_cancel_left _ hN]
168     simp only [transferSectionCoeff, hres, ↓reduceIte, hjle,
169       PowerSeries.coeff_expand, hdvd, hdiv, PowerSeries.coeff_rescale,
170       coeff_residueZeroFSeries]
171     calc
172       lambda ^ n * (1 / (n.factorial : ℚ)) =
173           lambda ^ (N * (n / N) + j) *
174             (((N * (n / N) + j).factorial : ℚ))⁻¹ := by
175               rw [← hn]
176               simp only [one_div]
177       _ = (lambda ^ j * (j.factorial : ℚ)⁻¹) *
178           ((lambda ^ N * ((N : ℚ) ^ N)⁻¹) ^ (n / N) *
179             residueZeroFCoeff N j (n / N)) := by
180               symm
181               calc
182                 _ = lambda ^ (N * (n / N) + j) *
183                     ((j.factorial : ℚ)⁻¹ *
184                       ((N : ℚ) ^ (N * (n / N)))⁻¹ *
185                         residueZeroFCoeff N j (n / N)) := by
186                           simp only [mul_pow, inv_pow, ← pow_mul]
187                           ring
188                 _ = _ := by rw [residueZeroFCoeff_normalization hN]
189   · by_cases hjle : j ≤ n
190     · have hzero : ¬N ∣ n - j := by
191         intro hdvd
192         apply hres
193         calc
194           n % N = ((n - j) + j) % N := by rw [Nat.sub_add_cancel hjle]
195           _ = ((n - j) % N + j % N) % N := Nat.add_mod _ _ _
196           _ = j := by
197             rw [Nat.dvd_iff_mod_eq_zero.mp hdvd, zero_add,
198               Nat.mod_eq_of_lt hjN, Nat.mod_eq_of_lt hjN]
199       simp [transferSectionCoeff, hres, hjle, PowerSeries.coeff_expand, hzero]
200     · simp [transferSectionCoeff, hres, hjle]
201 
202 end
203 
204 end Komorebi.PaperIV

Back to source controls