Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \clearpage\subsection{All Residue Completion Supplement}\label{app:sup10}
2 \noindent\textbf{Checkpoint scope.} This complete source body retains the status of its dated original supplement. Earlier pending or partial-coverage labels are historical; the final core records their resolution.\par\medskip
3 \subsubsection*{Scope and final statement}
4 Let $p$ be a prime, let $m>0$ divide $p-1$, put $N=mp$ and $h=(p-1)/m$, and let $0\le j<N$. The original rational packet is defined by
5 \[
6  \sum_{q=0}^{n}\binom{Nn+j}{Nq}C_{N,j}(q)=\delta_{n0},
7  \qquad E_j(n)=j!\,C_{N,j}(n).
8 \]
9 For every $n,k,u\in\N$, the new formal result establishes
10 \[
11  \boxed{E_j(n)\in\Z_p,\qquad
12  \Delta_{uh}^{k}E_j(n)\in p^{\min(k,mn)}\Z_p.}
13 \]
14 Here $\Delta_h f(n)=f(n+h)-f(n)$. The corresponding rational valuation statement is zero-safe:
15 \[
16  \Delta_{uh}^{k}E_j(n)=0\quad\text{or}\quad
17  v_p\bigl(\Delta_{uh}^{k}E_j(n)\bigr)\ge\min(k,mn).
18 \]
19 For the normalized coefficients, the exact correction is retained:
20 \[
21  \boxed{\Delta_{uh}^{k}C_{N,j}(n)=0\quad\text{or}\quad
22  v_p\bigl(\Delta_{uh}^{k}C_{N,j}(n)\bigr)\ge\min(k,mn)-v_p(j!).}
23 \]
24 The manuscript's odd-prime, positive-$u$ theorem is a specialization. The formal statement also includes zero row, zero order, zero multiplier, and the $p=2,m=1$ subcase. This does not assert a different or broader external dyadic conjecture.
25 
26 \begin{center}\begin{tabular}{lrr}\toprule
27 Inventory & Prior v0.9.0 & Current source corpus\\\midrule
28 Named manuscript-proved items covered &23/24&24/24\\
29 Active mathematical modules &57&70\\
30 Explicit theorem declarations &630&753\\
31 Explicit definitions audited separately &128&148\\\bottomrule
32 \end{tabular}\end{center}
33 The 123 added theorem declarations include supporting lemmas and examples. They are not 123 independent discoveries. Three classical inputs and two conjectures remain separately tracked. The original manuscript and all 57 upstream proof modules are preserved unchanged.
34 
35 \textbf{Principal declaration.} \path{KomorebiPaperIX.Theorem75.global_finite_difference} states the integrality and both precision bounds together, for the original coefficient functions. Its hypotheses are primality, $m>0$, $m\mid p-1$ and $j<mp$, not an assumed flatness or weightedness certificate.
36 \par\medskip
37 \subsubsection*{1. Stability of the weighted differential ring}
38 The recovered checkpoint used the actual weighted subring
39 \[
40  \Wp=\left\{F(T)=\sum_{d\ge0}a_dT^d:\
41  p^{\lfloor d/p\rfloor}a_d\in\Z_p\ \text{for every }d\right\}.
42 \]
43 Its coefficient condition is identified with the one in the previously checked singular-Amice development. The failed \mcode{ThetaWeighted} draft is retained separately; the repaired active source checks the complete formal-series statement below.
44 
45 Put
46 \[
47  \Theta=(1+T)\frac{d}{dT},\qquad
48  B_\Theta=\frac{\Theta^{p^2}-\Theta^p}{p}.
49 \]
50 The coefficient formula
51 \[
52  [T^d]\Theta F=(d+1)a_{d+1}+da_d
53 \]
54 proves $\Theta\Wp\subseteq\Wp$. If the floor weight increases between $d$ and $d+1$, then $p\mid d+1$, which compensates for that increase.
55 
56 \textbf{The normalized defect is not assumed to be a derivation.}
57 Its proved product rule contains the two middle Leibniz sums:
58 \[
59  B_\Theta(FG)=(B_\Theta F)G+F(B_\Theta G)+\mathcal B_p(F,G).
60 \]
61 The coefficients of $\mathcal B_p$ are the actual integral quotients
62 $\binom{p^2}{a}/p$ and $\binom pa/p$. Derivative stability and this correction formula show that the elements $F\in\Wp$ satisfying $B_\Theta F\in\Wp$ are closed under the finite ring operations.
63 
64 The scalar input is proved for every natural $b$, including nonunits:
65 \[
66  \boxed{p^2\mid b^{p^2}-b^p\quad\text{in }\Z.}
67 \]
68 Because $\Theta(1+T)^b=b(1+T)^b$, the binomial expansion of $T^p=((1+T)-1)^p$ then proves stability of the divided generator $T^p/p$. For $d=pq+r$, $0\le r<p$, every weighted monomial has the exact factorization
69 \[
70  a_dT^d=(p^qa_d)\left(\frac{T^p}{p}\right)^qT^r.
71 \]
72 The scalar $p^qa_d$ is integral by the actual weight condition. Thus all weighted monomials, and all finite weighted polynomials, satisfy the defect condition.
73 
74 Finally, $[T^d]B_\Theta F$ depends only on coefficients through $d+p^2$. Replacing $F$ by this finite prefix proves the result for the entire formal series, without an analytic convergence assumption:
75 \[
76  \boxed{B_\Theta\Wp\subseteq\Wp,\qquad B_\Theta^s\Wp\subseteq\Wp\ (s\ge0).}
77 \]
78 \textbf{Modules.} \mcode{WeightedAmiceRing}, \mcode{FrobeniusSquare}, \mcode{ThetaWeighted}.
79 \par\medskip
80 \subsubsection*{2. Actual substitution and singular higher differences}
81 Let
82 \[
83  \mathcal E(F)(t)=F(e^t-1),\qquad D=\frac{d}{dt},\qquad
84  B_D=\frac{D^{p^2}-D^p}{p}.
85 \]
86 All substitutions use Mathlib's actual formal exponential, logarithm and substitution maps. The chain rule gives
87 \[
88  D\mathcal E(F)=\mathcal E(\Theta F),\qquad
89  B_D^s\mathcal E(F)=\mathcal E(B_\Theta^sF).
90 \]
91 The implementation also proves the inverse-substitution identity
92 \[
93  \mathcal E\bigl(f(\log(1+T))\bigr)=f(t).
94 \]
95 
96 The relevant integral subring is the \emph{Hurwitz} subring
97 \[
98  \Hp=\{f\in\Q_p[[t]]:\ n![t^n]f\in\Z_p\ \text{for every }n\}.
99 \]
100 It is not coefficientwise integrality of ordinary power-series coefficients. The precise connection is
101 \[
102  n![t^n]\mathcal E(F)=[T^0]\Theta^nF.
103 \]
104 Since every iterate of $\Theta$ preserves $\Wp$, the right side is integral. Therefore $\mathcal E(\Wp)\subseteq\Hp$. Applying the same statement to every $B_\Theta^sF$ proves
105 \[
106  \boxed{f(\log(1+T))\in\Wp\quad\Longrightarrow\quad
107  B_D^sf\in\Hp\text{ for every }s.}
108 \]
109 This is the proved transfer that was missing in the earlier attempt. No weighted Mahler pairing is assumed; the formal differential route supplies an alternative bridge.
110 
111 \subsection*{Application to the actual singular ratios}
112 The preceding v0.9.0 source independently constructs
113 \[
114  H_{N,c}(t)=\sum_{n\ge0}\frac{t^{Nn+c}}{(Nn+c)!},\quad
115  A_c(t)=t^{-c}H_{N,c}(t),\quad R_c=\frac{A_{c-1}}{A_c}.
116 \]
117 The notation $t^{-c}H_{N,c}$ means removing its proved initial zero coefficients. For each $c=ap$, $1\le a<m$, that source proves
118 $R_{ap}(\log(1+T))\in\Wp$. The new transfer consequently proves flatness of the \emph{same} rational ratio after scalar extension to $\Q_p$.
119 
120 The actual ratio is also proved to be an expansion in $t^N$, so its coefficients vanish outside multiples of $N$. Constructed $\Z_p$ lifts and the established coefficient criterion now give, for its literal Hurwitz coefficients $r_a(n)$,
121 \[
122  \boxed{\Delta_{uh}^{k}r_a(n)\in p^{\min(k,mn)}\Z_p.}
123 \]
124 The separate rational precision theorem is obtained through the coefficient-lift equality. Divisibility in the field $\Q_p$ is never substituted for this assertion.
125 
126 \textbf{Modules.} \mcode{WeightedDworkTransfer}, \mcode{SeriesDifferenceBridge}, \mcode{RatioSeriesSupport}.
127 \par\medskip
128 \subsubsection*{3. Nonsingular propagation without an assumed limit}
129 For consecutive original sections, the already defined ratios satisfy
130 \[
131  R_cH_{N,c}=tH_{N,c-1},\qquad H_{N,c}'=H_{N,c-1}.
132 \]
133 Differentiating the first relation, using the relation for $R_{c-1}$, and cancelling a section whose leading coefficient is proved nonzero gives the actual Riccati equation
134 \[
135  \boxed{tR_c'=R_c(1+R_{c-1}-R_c),\qquad 2\le c<N.}
136 \]
137 It is not an equation imposed on a replacement ratio. Write
138 \[
139  q=R_{c-1}-(c-1),\qquad y=R_c-c.
140 \]
141 Both have zero constant coefficient. With $\Lambda_c=tD+c$, the equation becomes
142 \[
143  \boxed{\Lambda_c y=cq+yq-y^2.}
144 \]
145 
146 When $p\nmid c$, define the actual inverse coefficientwise:
147 \[
148  [t^d]\Lambda_c^{-1}f=\frac{[t^d]f}{d+c}.
149 \]
150 On $p$-supported degrees, $d+c$ is a genuine $p$-adic unit. The proof establishes Hurwitz integrality of this solution, its support, both inverse identities, and preservation of full flatness using the earlier all-order Euler commutator theorem. The singular pivots $c=ap$ are never declared to be units.
151 
152 Now define explicit iterations
153 \[
154  y_0=0,\qquad y_{r+1}=\Lambda_c^{-1}(cq+y_rq-y_r^2).
155 \]
156 If $q$ is flat and $p$-supported, every iterate has those properties. The crucial link to the actual ratio is an exact finite-prefix theorem:
157 \[
158  \boxed{[t^d]y_r=[t^d]y\qquad(d\le r).}
159 \]
160 Indeed,
161 \[
162  (cq+zq-z^2)-(cq+yq-y^2)=(z-y)(q-z-y).
163 \]
164 The second factor has zero constant term. Multiplication therefore raises the established agreement prefix by one; coefficientwise division by $d+c$ preserves that prefix.
165 
166 For fixed $s,d$, the coefficient $d![t^d]B_D^sy$ depends only on the coefficients of $y$ through $d+p^2s$. Choosing the matching finite iterate proves its integrality. This establishes flatness of the actual $y$, and hence of $R_c$, without postulating flatness of the solution or invoking an unproved analytic fixed-point theorem.
167 
168 \textbf{Modules.} \mcode{EulerSeriesInverse}, \mcode{RiccatiFlatPropagation}, \mcode{RatioRiccati}.
169 \par\medskip
170 \subsubsection*{4. All-residue assembly and original coefficients}
171 The standard-window source and inverse results supply $R_1$ and $F_{N,0}$. Induction over $1\le c<N$ now has two proved cases. At $p\mid c$, the singular weighted estimate and the new substitution theorem give flatness. At $p\nmid c$, the preceding Riccati propagation applies. Thus every actual ratio $R_c$ is flat.
172 
173 Let $K_j(t)$ be the normalized section kernel with constant coefficient one. The constructed unnormalized Euler series is
174 \[
175  F_{N,j}(t)=j!\,K_j(t)^{-1}.
176 \]
177 The source/inverse identities and the factorial successor identity prove
178 \[
179  F_{N,j+1}=F_{N,j}R_{j+1},\qquad
180  F_{N,j}=F_{N,0}\prod_{c=1}^{j}R_c.
181 \]
182 The product formula is not an assembly hypothesis. Proved flatness of all factors and the original product-closure theorem establish flatness of the full family.
183 
184 Coefficient extraction identifies, literally,
185 \[
186  (Nn)![t^{Nn}]F_{N,j}=j!\,C_{N,j}(n).
187 \]
188 The support outside multiples of $N$ is proved separately. The constructed integral lift therefore represents the original rational coefficient function. The existing saturation criterion and the proved step-multiple argument give the ideal bound at every order, row and multiplier. Multiplication by $j!$ commutes with finite differences, giving precisely the displayed normalization loss.
189 
190 \subsection*{Exact examples outside the standard window}
191 For $(p,m,j)=(3,2,3)$, the source derives
192 \[
193  C_{6,3}(1)=-\frac1{84},\quad C_{6,3}(2)=\frac{703}{5460},\quad
194  C_{6,3}(3)=-\frac{223199}{7980}.
195 \]
196 Consequently,
197 \[
198  \Delta_1^2\bigl(3!C_{6,3}\bigr)(1)=-\frac{1464768}{8645},\qquad
199  v_3\!\left(-\frac{1464768}{8645}\right)=2.
200 \]
201 This attains $\min(2,2\cdot1)=2$. At the regular address $j=4$ beyond the singular boundary, the source likewise proves
202 \[
203  \Delta_1^2\bigl(4!C_{6,4}\bigr)(1)=-\frac{102745512}{2377375},
204 \]
205 and applies the universal exponent-two bound to this actual coefficient function.
206 
207 The earlier no-loss counterexample is retained: $v_3(C_{6,3}(2)-C_{6,3}(1))=0$. Proving the corrected theorem does not make that false normalized claim true.
208 
209 \textbf{Modules.} \mcode{AllRatiosDwork}, \mcode{AllResidueEuler}, \mcode{Theorem75}, \mcode{AllResidueExamples}.
210 \par\medskip
211 \subsubsection*{5. Verification record and claim boundary}
212 Each local module is rebuilt in a fresh output directory, with warnings treated as errors. A live \mcode{\#print axioms} audit checks every registered declaration, permitting only \mcode{propext}, \mcode{Classical.choice} and \mcode{Quot.sound}, or subsets.
213 
214 \begin{center}\begin{tabular}{lr}\toprule
215 Required release check & Inventory\\\midrule
216 Local proof modules &70\\
217 Named theorem declarations &753\\
218 Explicit definitions &148\\
219 Expected axiom reports &901\\
220 Pinned dependency revisions &9\\
221 Deliberate invalid-proof controls &33\\
222 Infrastructure and release tests &235\\\bottomrule
223 \end{tabular}\end{center}
224 The accompanying JSON verification record, not the existence of this table, determines whether the actual run passed. The final package also includes a fresh-extraction replay record, checksums, the declaration inventory and the updated manuscript coverage ledger.
225 
226 The negative controls preserve the earlier rejected false equalities, placeholders, invalid normalizations and unit pivots. Four new controls demand an extra power in the sharp singular example, remove the factorial loss, misuse a composite base, or center a ratio at the wrong constant. An infrastructure timeout or missing import is not an accepted negative result.
227 
228 \subsection*{Independent finite checks}
229 The standard-library Python mirror checks 328 complete residue families for primes $2,3,5,7,11$, including 233 higher-residue families. It checks 4,264 integral unnormalized coefficients, 22,137 normalized and 22,137 unnormalized difference bounds, and 1,640 comparisons with a separately computed ordinary reciprocal. Further checks cover 108 weighted differential iterations, 205 integer Frobenius-square cases and 180 exact Picard agreement prefixes.
230 
231 These are finite exact-arithmetic checks, not extracted Lean code and not substitutes for the universal formal proofs. The old normalization counterexample and the new sharp exponent-two example remain visible.
232 
233 \subsection*{Preservation and limitations}
234 All 57 earlier proof modules and the original 28-page status-corrected manuscript are retained unchanged. The new supplement and amendments give the current proof route. Historical failed drafts and interrupted recovery attempts are retained separately from accepted builds. Historical tests that assert an older unfinished status now read that frozen historical status; current tests require the actual unconditional capstone theorem before accepting completion.
235 
236 The portable Lean and Mathlib versions are pinned. Mathlib's compiled dependency cache is reused, not independently rebuilt. The historical numerical experiment suite and Papers I--VIII are not rerun. The two native conjectures remain unproved. No independent historical-priority assessment is made. Manuscript-to-Lean correspondence remains mathematical review, not a theorem equating natural-language prose with formal types.

Back to source controls

Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation