Realization Calculus

Download original file

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

Read the typeset paper

1 \clearpage\subsection{First Lean Block Supplement}\label{app:sup1}
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 result}
4 This block uses the 28-page \emph{status-corrected} Paper IX manuscript. That PDF is preserved unchanged. The release supplies a first formalization companion, not a completed or rewritten arithmetic paper.
5 
6 \textbf{Seven of 24 named items proved in the manuscript now have Lean coverage in the stated scopes. Seventeen remain pending.} Three classical inputs and two conjectures are registered separately. The development contains \textbf{89 explicit theorem declarations and 22 definitions across eight modules}. Supporting lemmas and concrete instances are included. These are not 89 independent discoveries.
7 
8 \begin{center}
9 \begin{tabular}{@{}p{.15\textwidth}p{.73\textwidth}@{}}
10 \toprule
11 Item & Covered mathematical content\\\midrule
12 1.2 & Residue reconstruction and divisor refinement\\
13 2.1 & Actual unit-EGF coordinate equivalence and transported projectors\\
14 2.2 & Filtered finite coefficient reconstruction, including $\Z_p$\\
15 3.2 & Constructed unique triangular inverse and original section identity\\
16 3.3 & Universal denominator clearing\\
17 8.2 & Lucas standard-window reduction and the diagonal unit\\
18 13.1 & Exact normalization counterexample and sharp factorial loss\\
19 \bottomrule
20 \end{tabular}
21 \end{center}
22 
23 \subsubsection*{The correction is preserved}
24 The normalized packet is not the same object as the packet multiplied by $j!$. The checked recurrence gives
25 \[
26  C_{6,3}(1)=-\frac1{84},\qquad C_{6,3}(2)=\frac{703}{5460},
27 \]
28 \[
29  C_{6,3}(2)-C_{6,3}(1)=\frac{64}{455},\qquad
30  v_3\!\left(\frac{64}{455}\right)=0.
31 \]
32 Thus the unrestricted normalized no-loss claim fails already at a valid one-step parameter instance. Multiplication by $3!$ restores one factor of three in this instance. The general corrected finite-difference theorem is \textbf{not} inferred from this calculation and is not yet formalized here.
33 
34 \subsubsection*{Verification standard}
35 All eight modules passed a fresh cumulative build with compiler warnings treated as errors. The audit resolved all 89 explicit theorems and all 22 explicit definitions. Their transitive axiom dependencies are confined to \mcode{propext}, \mcode{Classical.choice} and \mcode{Quot.sound}, or subsets. Three invalid-proof controls were rejected. The proof, scope, and numerical-regression records remain distinct.
36 \par\medskip
37 \pageheading{1. Residue packets and actual EGF coordinates}{Source items 1.2 and 2.1}
38 For a sequence $a:\N\to R$, define the actual selector
39 \[
40  (P_{N,j}a)(n)=\begin{cases}a(n),&n\bmod N=j,\\0,&\text{otherwise.}\end{cases}
41 \]
42 The source proves idempotence for every selector, orthogonality for distinct standard residue labels, and, when $N>0$,
43 \[
44  \sum_{j=0}^{N-1}P_{N,j}a=a.
45 \]
46 If $N\mid M$ and $M>0$, it also proves
47 \[
48  P_{N,j}a=\sum_{\substack{0\le r<M\\r\bmod N=j}}P_{M,r}a.
49 \]
50 The formal power-series versions are proved coefficientwise for actual \mcode{PowerSeries} objects. There is no finite truncation of the sequence domain in these theorems.
51 
52 \subsection*{A constructed inverse, not an inverse hypothesis}
53 Let $K$ be a characteristic-zero field. Define
54 \[
55  \mathcal E(a)=\sum_{n\ge0}\frac{a_n}{n!}t^n,\qquad
56  \mathcal D(A)_n=n![t^n]A.
57 \]
58 Both inverse laws $\mathcal D\mathcal E=I$ and $\mathcal E\mathcal D=I$ are proved. The ordinary power-series product then yields the binomial convolution
59 \[
60  \mathcal D\bigl(\mathcal E(h)\mathcal E(a)\bigr)_n
61  =\sum_{r=0}^{n}\binom nr h_r a_{n-r}.
62 \]
63 For $h_0=1$, the formal inverse of $H=\mathcal E(h)$ is used to construct a sequence equivalence
64 \[
65  U_H a=\mathcal D(H\mathcal E(a)),\qquad
66  U_H^{-1}a=\mathcal D(H^{-1}\mathcal E(a)).
67 \]
68 The equivalence has proved left and right inverse laws. The inverse's constant coefficient is proved to be one. The associated lower-triangular entries have diagonal one and vanish above the diagonal.
69 
70 For the actual conjugated selectors
71 \[
72  \widehat P_{N,j}=U_HP_{N,j}U_H^{-1},
73 \]
74 idempotence, orthogonality, and finite reconstruction are proved from the constructed maps. No projector identity for the conjugates is inserted as an assumption.
75 
76 \textbf{Formal boundary.} These are formal series and coefficient identities. They do not establish convergence for an analytic EGF. The characteristic-zero field assumption is explicit. Unrestricted factorial division in an arbitrary ring is not asserted.
77 
78 \textbf{Principal targets.}\par
79 \target{ResiduePackets.packet_reconstruction}\par
80 \target{ResiduePackets.packet_refinement}\par
81 \target{EGF.coordinateEquiv, EGF.coordinate_forward, EGF.coordinate_inverse}\par
82 \target{EGF.transported_reconstruction}
83 \par\medskip
84 \pageheading{2. Triangular inversion and denominator control}{Source items 3.2 and 3.3}
85 For a general lower-triangular coefficient array $T$ over a field with nonzero diagonal, the code defines forward substitution by well-founded recursion:
86 \[
87  a_n=\frac{b_n-\sum_{q<n}T_{nq}a_q}{T_{nn}}.
88 \]
89 It proves that this constructed sequence solves every row and that every sequence solving those rows equals it. No existence or uniqueness premise is used.
90 
91 \subsection*{The congruential coefficients}
92 Over $\Q$, specialize to
93 \[
94  T_{nq}=\binom{Nn+j}{Nq},\qquad b_n=\delta_{n0}.
95 \]
96 The diagonal is positive as an integer, hence nonzero. The resulting sequence $C_{N,j}(n)$ satisfies
97 \[
98  C_{N,j}(0)=1,\qquad
99  \sum_{q=0}^{n}\binom{Nn+j}{Nq}C_{N,j}(q)=\delta_{n0}.
100 \]
101 The displayed recurrence in the manuscript and the unique-solution theorem are consequences of this definition.
102 
103 The formalization does not stop at a recurrence. In the variable $z=t^N$, construct
104 \[
105  K_{N,j}(z)=\sum_{n\ge0}\frac{j!}{(Nn+j)!}z^n,\qquad
106  F_{N,j}(z)=\sum_{n\ge0}\frac{C_{N,j}(n)}{(Nn)!}z^n.
107 \]
108 It proves the factorial coefficient identity, then $F_{N,j}K_{N,j}=1$ and therefore $F_{N,j}=K_{N,j}^{-1}$.
109 
110 For $N>0$ and $0\le j<N$, the independently defined original exponential section is
111 \[
112  E_{N,j}(t)=\sum_{d\equiv j\ ({\rm mod}\ N)}\frac{t^d}{d!}.
113 \]
114 Using the actual power-series expansion homomorphism $z\mapsto t^N$, the code proves
115 \[
116  E_{N,j}(t)=\frac{t^j}{j!}K_{N,j}(t^N),\qquad
117  \boxed{F_{N,j}(t^N)E_{N,j}(t)=\frac{t^j}{j!}.}
118 \]
119 Thus the recurrence is connected back to the original normalized EGF definition. The section vanishes at zero when $j>0$. No inverse of that nonunit section is assumed.
120 
121 \subsection*{Universal clearing}
122 Define
123 \[
124  D_{N,j}(n)=\prod_{r=1}^{n}\binom{Nr+j}{Nr},\qquad D_{N,j}(0)=1.
125 \]
126 For every $n$, the code proves $D_{N,j}(n)C_{N,j}(n)\in\Z$. The general proof promotes each earlier clearing denominator to the common product, then cancels the new nonzero diagonal. This is a denominator bound, not a claim that every normalized coefficient is integral.
127 \par\medskip
128 \pageheading{3. Filtered tails and the standard window}{Source items 2.2 and 8.2}
129 \subsection*{Filtration at a finite coefficient row}
130 Let $R$ be any commutative ring. For $w\in\N\cup\{\infty\}$ define
131 \[
132  p^{[w]}=\begin{cases}p^w,&w<\infty,\\0,&w=\infty.\end{cases}
133 \]
134 The infinity convention expresses a vanishing coefficient, not an infinite exponent operation. For any finite index set, every term with weight at least $L$ is divisible by $p^L$. A finite-sum proof yields
135 \[
136  \boxed{p^L\ \bigm|\ 
137  \sum_{r=0}^{n}\binom nr c_rp^{[w(r)]}S_{n-r}
138  -\sum_{\substack{0\le r\le n\\w(r)<L}}
139      \binom nr c_rp^{[w(r)]}S_{n-r}.}
140 \]
141 The result is specialized to actual $p$-adic integers $R=\Z_p$ for prime $p$. Divisibility there is precisely the asserted membership in $p^L\Z_p$.
142 
143 For an individual row the sum is finite, so the proof does not require $w(r)\to\infty$. This is a stronger coefficient-row scope, not a theorem about an infinite limiting process. A supporting lemma also proves a $p^{2M+2}$ tail bound for a sum with visible factors $p^{2m}$. It is not counted as either Euler supercongruence theorem: their generating-function reconstruction identities remain pending.
144 
145 \subsection*{Actual Lucas reduction}
146 For prime $p$, all $m,n,q\in\N$, and $0\le j<p$, the checked binomial congruence is
147 \[
148  \boxed{\binom{mpn+j}{mpq}\equiv\binom{mn}{mq}\pmod p.}
149 \]
150 The proof applies Mathlib's Lucas low-digit reduction to the actual natural binomial coefficients. It does not assume a pre-reduced row. The statement also permits $q>n$. If $m>0$, both binomial coefficients then vanish.
151 
152 Taking $q=n$ gives
153 \[
154  \binom{mpn+j}{mpn}\equiv1\pmod p.
155 \]
156 Nondivisibility by $p$ and invertibility of that diagonal in $\Z/p\Z$ are proved. The separate supporting lemma $p\nmid j!$ for $j<p$ establishes the standard-window factorial-unit condition.
157 
158 \textbf{Dependency boundary.} Lucas' theorem is a named classical input in the manuscript and is reused from the pinned Mathlib library. This block does not independently reconstruct Lucas' full digit theorem. The residue-independence result (8.3), uniform standard-window period (8.5), and the global finite-difference theorem (7.5) remain pending.
159 
160 \textbf{Principal targets.}\par
161 \target{Filtered.padic_filtered_reconstruction}\par
162 \target{StandardWindow.lucas_row_reduction}\par
163 \target{StandardWindow.standard_diagonal_unit}\par
164 \target{StandardWindow.factorial_valuation_zero}
165 \par\medskip
166 \pageheading{4. Sharp normalization boundary}{Source item 13.1}
167 The construction fixes the two coefficient conventions:
168 \[
169  C_{N,j}(n),\qquad \widetilde C_{N,j}(n)=j!\,C_{N,j}(n).
170 \]
171 The witness uses $p=3$, $m=2$, $N=mp=6$, $j=3$, $n=1$ and difference step $h=(p-1)/m=1$. The parameter conditions are checked explicitly, including odd primality, $m\mid p-1$ and $j<N$.
172 
173 The first row gives $84C_{6,3}(1)+1=0$. The second row, evaluated by the same recursive definition, gives $C_{6,3}(2)=703/5460$. Therefore
174 \[
175  \Delta_1 C_{6,3}(1)=\frac{64}{455}\ne0.
176 \]
177 Neither numerator nor denominator is divisible by three, so its actual rational 3-adic valuation is zero. A further theorem negates the universal one-step no-loss statement by applying it to this valid tuple and deriving $1\le0$.
178 
179 For the unnormalized convention,
180 \[
181  \Delta_1\widetilde C_{6,3}(1)=3!\,\frac{64}{455}=\frac{384}{455},
182  \qquad v_3\!\left(\frac{384}{455}\right)=1.
183 \]
184 The factorial's valuation is also proved:
185 \[
186  v_3(3!)=1,\qquad
187  v_3\bigl(\Delta_1C_{6,3}(1)\bigr)
188  =1-v_3(3!)=0.
189 \]
190 This proves sharpness at the displayed normalization boundary. It does not establish the corrected global inequality for all parameters, and does not assert that every nonunit-factorial parameter tuple must violate every no-loss specialization. All valuation calculations here concern nonzero rationals.
191 
192 \subsubsection*{Work remaining in the named proved register}
193 \begin{center}\small
194 \begin{tabular}{@{}p{.19\textwidth}p{.69\textwidth}@{}}
195 \toprule
196 Items & Pending mathematical content\\\midrule
197 4.1--4.3 & Odd-power generating function, Euler reconstruction, odd-prime ladder\\
198 5.1--5.4 & Dyadic inverse and source integrality, reconstruction, weighted ladder\\
199 6.2 & Finite unit-decomposition certificates\\
200 7.2--7.5 & Finite Mahler reconstruction, weighted differences, unit modes, global odd-prime differences\\
201 8.3, 8.5 & Standard-window residue independence and uniform period\\
202 9.1, 9.2 & Companion jumps and Fibonacci packet recurrence\\
203 10.1 & Arithmetic CRT packet factorization\\\bottomrule
204 \end{tabular}\end{center}
205 The two conjectures, 13.2 and 13.3, remain unproved and outside the 24-item register. The 17 pending entries are manuscript proof claims awaiting this project's Lean verification, not conjectures newly created by the formalization process.
206 \par\medskip
207 \pageheading{5. Verification and reproducibility}{Exact source pins, observed checks and retained failures}
208 \begin{center}\small
209 \begin{tabular}{@{}lrr@{}}\toprule
210 Module & Theorems & Definitions\\\midrule
211 ResiduePackets & 8 & 2\\
212 Triangular & 14 & 3\\
213 EGFCoordinates & 21 & 6\\
214 FilteredReconstruction & 7 & 1\\
215 CongruentialEuler & 16 & 7\\
216 ExponentialSection & 5 & 3\\
217 StandardWindow & 6 & 0\\
218 NormalizationBoundary & 12 & 0\\\midrule
219 Total & 89 & 22\\\bottomrule
220 \end{tabular}\end{center}
221 
222 \textbf{Lean run.} All eight modules were compiled into a new empty output directory under Lean 4.34.0-rc2. All nine dependency revisions matched the pinned manifest. Mathlib's revision is\par
223 {\footnotesize\mcode{aeb72f1e9981b6d35b426b16dca7759be3e7ba06}.}
224 
225 The 111 explicit-declaration axiom reports matched the inventory. A false natural equality, an admitted placeholder, and the false normalized bound were all rejected. The placeholder control exercises the warnings-as-errors policy. \mcode{sorryAx} is also excluded by the separate axiom whitelist. The 21 infrastructure and release tests passed.
226 
227 \textbf{Independent exact regressions.} Python integer and rational mirrors passed 120 triangular systems, 45 congruential parameter pairs (495 rows), 120 EGF-coordinate cases, 45 residue-refinement cases, 240 filtered tails, 10,824 Lucas rows, the normalization witness and eight invalid-input controls. These are not executions extracted from Lean or reruns of the original historical numerical package.
228 
229 \textbf{Failures retained.} Of 29 captured development checks, 15 passed and 14 failed before repair. A malformed generic-field draft triggered a release-candidate compiler panic after proof errors. The repaired sources passed the final clean run. Development products were not reused in that run. An earlier cumulative invocation was interrupted before completion and is retained separately. One initial Python scanner-test assertion had the wrong expected whitespace count and was repaired. Its failure log is retained.
230 
231 \textbf{Trust and source boundary.} Mathlib's precompiled dependency cache was reused, not rebuilt from source. No earlier paper was rebuilt. Only the status-corrected primary PDF was recovered for this manuscript baseline, not its original TeX, experiment package, or complete global finite-difference supplement. Formal-to-prose correspondence is a reviewed crosswalk, not an automated semantic-equivalence theorem. Native Windows was not tested.
232 
233 \textbf{Reproduce.} With Python 3.10+ and the separate extracted Linux portable kit:
234 \begin{verbatim}
235 bash Run-Portable.sh /path/to/Komorebi_Portable_Lean_4.34.0-rc2
236 \end{verbatim}
237 The ZIP includes sources, inventories, the unchanged manuscript, this supplement, exact-regression scripts, tests, and successful and failed logs. The large runtime and local build products are not included.

Back to source controls

Back to Realization Calculus