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{Fourth Lean Block Supplement}\label{app:sup4}
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 release continues the unchanged 28-page status-corrected manuscript and the checked third block. It completes the recorded scopes of Theorem 7.2, Corollary 7.3 and Theorem 7.4. All 17 upstream proof files and the three earlier mathematical supplements remain unchanged.
5 
6 \textbf{Seventeen of 24 named items proved in the manuscript now have formal coverage. Seven remain pending.} Three classical inputs and two conjectures are tracked separately. The cumulative project contains \textbf{272 named theorem declarations and 60 explicit definitions across 21 modules}.
7 
8 \begin{center}
9 \begin{tabular}{@{}p{.48\textwidth}>{\raggedright\arraybackslash}p{.18\textwidth}rr@{}}
10 \toprule
11 New module & Scope & Theorems & Defs.\\\midrule
12 \mcode{FiniteMahler} & 7.2 & 19 & 3\\
13 \mcode{PadicDifferenceBounds} & 7.3 & 12 & 2\\
14 \mcode{UnitModeDifferences} & 7.4 & 9 & 0\\
15 \mcode{MahlerExamples} & Exact controls & 13 & 2\\\midrule
16 Total added & Three items & 53 & 7\\\bottomrule
17 \end{tabular}
18 \end{center}
19 The 53 additions include supporting lemmas and examples, not 53 independent discoveries. The classical Gregory--Newton and binomial-difference results are reused from pinned Mathlib. The new modules connect those results to the actual Paper IX coefficient definitions, interpolation scopes, valuation bounds and unit modes.
20 
21 \subsubsection*{Two explicit specification boundaries}
22 A finite sample through $N$ determines $\Delta^s f(n)$ only when $n+s\leq N$. For arbitrary orders, the finite-coefficient identity describes the constructed interpolant, not every unknown continuation of the sample. All three versions are separately checked.
23 
24 The additive valuation is extended to $\ord_p(0)=\infty$. This avoids incorrectly applying Mathlib's finite-valued default at zero to an inequality that must also cover cancellation and identically zero differences.
25 
26 \subsubsection*{Verification status}
27 The fresh cumulative Lean run compiled all 21 modules with warnings as errors, matched all 332 explicit declaration axiom reports, and rejected 12 invalid-proof controls. All 74 infrastructure and release tests passed. Independent exact-rational mirrors are recorded separately from the universal proofs. The archive is also subjected to a fresh-extraction rebuild and integrity audit. Its separate report records that outcome.
28 \par\medskip
29 \pageheading{1. Reconstruction and finite-data scope}{Theorem 7.2; manuscript page 17}
30 Let $R$ be any commutative ring. The implementation uses the actual forward-difference operator
31 \[
32  \Delta_h f(n)=f(n+h)-f(n),\qquad c_r=\Delta_1^r f(0).
33 \]
34 For a full sequence $f:\N\to R$, pinned Mathlib's Gregory--Newton formula gives
35 \[
36  \boxed{f(n)=\sum_{r=0}^{n}c_r\binom nr.}
37 \]
38 The source applies the theorem to these exact definitions. A separate explicit formula relates an $s$-th difference to its original sampled values, so the data dependence is inspectable:
39 \[
40  \Delta_h^s f(n)=\sum_{j=0}^{s}(-1)^{s-j}\binom sj f(n+jh).
41 \]
42 Applying Newton reconstruction to $\Delta_1^s f$ and composing the iterated operators proves
43 \[
44  \boxed{\Delta_1^s f(n)=\sum_{j=0}^{n}c_{s+j}\binom nj.}
45 \]
46 The apparently infinite coefficient sum is finite at each natural argument. Neither continuity nor convergence is needed for these identities.
47 
48 \subsection*{An independently defined interpolant}
49 For a finite coefficient list, define
50 \[
51  I_N(c)(n)=\sum_{r=0}^{N}c_r\binom nr.
52 \]
53 The source proves exact coefficient extraction:
54 \[
55  \Delta_1^s I_N(c)(0)=
56  \begin{cases}c_s,&s\leq N,\\0,&s>N.\end{cases}
57 \]
58 It follows that $I_N(c)$ has the stated shifted-coefficient formula at every order, with zero coefficients beyond $N$. Every difference of order greater than $N$ vanishes. Its coefficients are uniquely determined by its values at $0,\ldots,N$.
59 
60 \subsection*{What the finite sample does and does not determine}
61 For $c_r=\Delta_1^r f(0)$ with $r\leq N$, the source proves
62 \[
63  I_N(c)(n)=f(n)\quad(n\leq N),\qquad
64  \Delta_1^s I_N(c)(n)=\Delta_1^s f(n)\quad(n+s\leq N).
65 \]
66 The condition is essential. The sequences $f(n)=n$ and $g(n)=0$ agree on the sample $\{0\}$, but $\Delta f(0)=1$ and $\Delta g(0)=0$. This is a checked counterexample to unrestricted inference outside the observed stencil.
67 
68 \textbf{Principal targets.}\par
69 \target{Mahler.finite_mahler_reconstruction, Mahler.coefficient_interpolant}\par
70 \target{Mahler.difference_from_coefficients, Mahler.finite_sample_difference}
71 \par\medskip
72 \pageheading{2. Weighted bounds in the actual ring $\Z_p$}{Corollary 7.3; manuscript page 18}
73 Let $p$ be prime. For $x\in\Z_p$, define
74 \[
75  \ord_p(x)=\begin{cases}\infty,&x=0,\\v_p(x),&x\neq0.\end{cases}
76 \]
77 The nonzero branch uses Mathlib's actual $p$-adic valuation. The implementation proves its connection to genuine integral divisibility:
78 \[
79  \boxed{L\leq\ord_p(x)\quad\Longleftrightarrow\quad p^L\mid x
80  \ \text{in }\Z_p,\qquad L\in\N.}
81 \]
82 This is not divisibility in $\Q_p$, where a nonzero scalar can divide any field element. The zero case is proved separately, so zero does not spuriously violate a positive lower bound.
83 
84 The source also proves multiplicativity of this extended order, the nonarchimedean lower bound for addition, and its finite-sum consequence. The natural-number cast is connected to the actual integer binomial valuation.
85 
86 \subsection*{The binomial valuation is retained}
87 Let $f:\N\to\Z_p$, let $c_r=\Delta_1^r f(0)$, and suppose
88 \[
89  w(s+j)\leq\ord_p(c_{s+j})\quad(0\leq j\leq n),
90  \qquad w:\N\to\N\cup\{\infty\}.
91 \]
92 Set
93 \[
94  B_p(w;n,s)=\min_{0\leq j\leq n}
95  \left\{w(s+j)+v_p\!\binom nj\right\}.
96 \]
97 Every binomial in this range is nonzero. The code proves
98 \[
99  \boxed{B_p(w;n,s)\leq\ord_p(\Delta_1^s f(n)).}
100 \]
101 This is the manuscript minimum after the substitution $r=s+j$. Coefficients outside this range have zero binomial multiplier. Weights equal to infinity are allowed, and a completely vanishing difference has order infinity.
102 
103 For a uniform coefficient hypothesis, the simpler conclusion follows:
104 \[
105  \boxed{\inf_{j\geq0} w(s+j)\leq\ord_p(\Delta_1^s f(n)).}
106 \]
107 For each finite $L\leq B_p(w;n,s)$, a separate theorem yields $p^L\mid\Delta_1^s f(n)$ inside $\Z_p$. Another specialization handles arbitrary finite interpolants with infinite weights beyond their degree.
108 
109 \textbf{Principal targets.}\par
110 \target{PadicBounds.nat_le_order_iff, PadicBounds.weighted_difference_bound}\par
111 \target{PadicBounds.weighted_difference_divisibility}\par
112 \target{PadicBounds.coefficient_tail_bound, PadicBounds.interpolant_weighted_bound}
113 \par\medskip
114 \pageheading{3. Unit modes and residue-field reduction}{Theorem 7.4; manuscript page 18}
115 For $u$ in any commutative ring, and every natural step $h$, iteration proves
116 \[
117  \boxed{\Delta_h^s(u^n)=u^n(u^h-1)^s.}
118 \]
119 The proof unfolds the actual forward-difference operator and uses the power multiplication law. No valuation premise or geometric-difference identity is assumed. More generally, a proved divisibility $p^k\mid u^h-1$ implies
120 \[
121  p^{ks}\mid\Delta_h^s(u^n).
122 \]
123 
124 \subsection*{Why a $p$-adic unit supplies one factor of $p$}
125 Now let $u\in\Z_p^\times$. The actual ring homomorphism
126 \[
127  \pi:\Z_p\longrightarrow\mathbb F_p
128 \]
129  sends $u$ to a nonzero unit. Fermat's finite-field theorem therefore gives
130 \[
131  \pi(u)^{p-1}=1,\qquad \pi(u^{p-1}-1)=0.
132 \]
133 Using the proved kernel identity $\ker\pi=p\Z_p$, the source derives
134 \[
135  \boxed{p\mid u^{p-1}-1\quad\text{inside }\Z_p.}
136 \]
137 The conclusion is not supplied as an abstract certificate. It follows from the unit hypothesis and the standard residue-field construction.
138 
139 Combining it with the geometric identity establishes
140 \[
141  \boxed{p^s\mid\Delta_{p-1}^s(u^n),\qquad
142  s\leq\ord_p(\Delta_{p-1}^s(u^n)).}
143 \]
144 These statements hold for every prime, including $p=2$ with step one. Zero differences and order zero are included. Every multiple of the Fermat step satisfies the same lower bound.
145 
146 \subsection*{Finite integral linear combinations}
147 For any finite index set $S$, coefficients $a_i\in\Z_p$ and units $u_i\in\Z_p^\times$, linearity of the actual iterated operator gives
148 \[
149  \Delta_h^s\!\left(\sum_{i\in S}a_i u_i^n\right)
150  =\sum_{i\in S}a_i u_i^n(u_i^h-1)^s.
151 \]
152 At $h=p-1$, the result is divisible by $p^s$. The empty sum is permitted. This does not prove that the general congruential Euler packets of Theorem 7.5 admit such a representation.
153 
154 \textbf{Principal targets.}\par
155 \target{UnitModes.geometric_difference, UnitModes.unit_fermat_divisibility}\par
156 \target{UnitModes.unit_mode_valuation_gain}\par
157 \target{UnitModes.finite_unit_modes_valuation_gain}
158 \par\medskip
159 \pageheading{4. Exact examples and adversarial checks}{The examples use the same definitions as the general results}
160 \subsection*{A polynomial anchor}
161 The actual difference table for $f(n)=n^2$ yields
162 \[
163  (c_0,c_1,c_2,c_3)=(0,1,2,0).
164 \]
165 The finite interpolant therefore reconstructs $I_2(c)(7)=49$. This checks the sign and indexing conventions, not just the names of the defined objects.
166 
167 \subsection*{A sharp binomial-weight improvement}
168 Let
169 \[
170  F(n)=81\binom n1+3\binom n2+3\binom n3+81\binom n4.
171 \]
172 At $n=3$ and $s=1$, the four coefficient valuations are $(4,1,1,4)$, while the binomial valuations are $(0,1,1,0)$. Thus the refined bound is
173 \[
174  B_3(w;3,1)=\min(4,2,2,4)=2,
175 \]
176 stronger than the coefficient-only lower bound one. The source checks both the minimum and the actual result:
177 \[
178  \boxed{\Delta F(3)=180,\qquad\ord_3(180)=2.}
179 \]
180 The valuation equality is proved in the actual completed ring $\Z_3$, with an independent exact integer divisibility check as well.
181 
182 \subsection*{A sharp unit-mode gain}
183 For $p=5$ and $u=2$,
184 \[
185  \Delta_4^2(u^n)\big|_{n=0}=(2^4-1)^2=225.
186 \]
187 The source proves $5^2\mid225$ and $5^3\nmid225$. This example attains the guaranteed gain. No additional uniform power of $p$ is claimed.
188 
189 \subsection*{What fails when hypotheses or conventions are dropped}
190 The nonunit $u=3$ at $p=3$ gives $\Delta_2(u^n)|_{n=0}=8$, with no factor of three. A constant unit has every positive-order difference zero, hence infinite extended valuation. The finite-sample counterexample on page 2 distinguishes a true interpolant identity from an unsupported claim about unknown continuation.
191 
192 The release verifier adds four negative Lean controls: an unrestricted finite-sample inference, zero assigned finite extended valuation, nonunit valuation gain, and an extra unit-mode precision claim. All are required to fail with substantive proof diagnostics. Import errors or timeouts do not qualify as successful rejection tests.
193 
194 \textbf{Source.} The module \mcode{MahlerExamples} contains these exact certificates. Principal target names are listed in the fourth-block ledger.
195 \par\medskip
196 \pageheading{5. Verification record and remaining work}{Evidence is retained separately from conclusions}
197 \subsection*{Cumulative proof checks}
198 Lean 4.34.0-rc2 rebuilt all 21 local modules into a fresh directory with warnings treated as errors. All 272 theorem declarations and 60 explicit definitions matched their expected transitive axiom reports. Only \mcode{propext}, \mcode{Classical.choice} and \mcode{Quot.sound}, or subsets thereof, occurred. All nine dependency pins matched. Twelve invalid-proof controls were rejected.
199 
200 All 74 infrastructure and release tests passed. Historical version-specific tests use immutable metadata snapshots. Current source counts, preserved upstream hashes, exact newly covered manuscript items, remaining items and substantive mathematical boundary cases are checked by the active suite.
201 
202 Ten targeted development runs preceded the cumulative build. Six failed before repair, due to elaboration, coercions, finite-sum normalization, an inferred index type and tactic or linter diagnostics. Those drafts and compiler outputs remain in a separate inactive evidence directory. No failed draft is counted as a passing theorem.
203 
204 \subsection*{Independent exact-rational mirrors}
205 The new standard-library Python program uses repeated difference tables and independently evaluated binomial sums. It passed 2,079 reconstructed values, 15,939 in-range sample differences, 2,600 arbitrary-interpolant differences, 900 weighted cases, 966 unit-mode cases and 350 finite-mode-sum cases. Among the weighted cases, 522 differences were zero. It also rejected 189 out-of-range stencils and 15 nonunit inputs.
206 
207 These are finite tests on rational examples, not executable extraction of Lean functions, a substitute for a universal proof, or a new run of the manuscript's historical experiments.
208 
209 \subsection*{Remaining named items proved in the manuscript}
210 \begin{center}
211 \begin{tabular}{@{}ll@{}}\toprule
212 Item & Remaining formalization\\\midrule
213 6.2 & Finite unit decomposition certificates\\
214 7.5 & Global odd-prime Euler finite-difference theorem\\
215 8.3 & Standard-window residue independence\\
216 8.5 & Uniform standard-window period\\
217 9.1 & Companion-matrix jump theorem\\
218 9.2 & Fibonacci packet recurrence\\
219 10.1 & Arithmetic CRT packet factorization\\\bottomrule
220 \end{tabular}
221 \end{center}
222 The three classical inputs and two conjectures remain separate. Mathlib's pinned compiled cache was reused, not independently rebuilt. No infinite Mahler convergence theorem or prime-independent arithmetic spine is proved here. The original manuscript and three earlier supplements remain unchanged. The finite-data and zero-valuation clarifications accompany them in this release.
223 
224 \textbf{Reproduce.} Run \mcode{bash Run-Portable.sh /path/to/kit}. The report in \path{verification/fourth_release/} records the cumulative build. The separately distributed release audit records archive integrity and fresh-extraction replay.

Back to source controls

Back to Realization Calculus