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{Fifth Lean Block Supplement}\label{app:sup5}
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 fourth block. It completes Proposition 6.2, Corollary 8.3 and Theorem 10.1 in the scopes stated below. All 21 upstream proof files and the four earlier mathematical supplements remain unchanged.
5 
6 \textbf{Twenty of 24 named items proved in the manuscript now have formal coverage. Four remain pending.} Three classical inputs and two conjectures are tracked separately. The cumulative project contains \textbf{333 named theorem declarations and 77 explicit definitions across 28 modules}.
7 
8 \begin{center}
9 \begin{tabular}{@{}p{.43\textwidth}p{.22\textwidth}rr@{}}
10 \toprule
11 New module & Scope & Theorems & Defs.\\\midrule
12 \mcode{UnitTriangular} & Integral solver & 5 & 1\\
13 \mcode{WindowIndependence} & 8.3 & 11 & 3\\
14 \mcode{FiniteUnits} & 6.2, prime powers & 13 & 4\\
15 \mcode{DyadicUnits} & 6.2, sign branch & 10 & 4\\
16 \mcode{UnitRefinement} & Finite compatibility & 4 & 2\\
17 \mcode{CRTPackets} & 10.1 & 5 & 1\\
18 \mcode{FiniteArithmeticExamples} & Exact controls & 13 & 2\\\midrule
19 Total added & Three items & 61 & 17\\\bottomrule
20 \end{tabular}
21 \end{center}
22 The 61 new theorems include supporting lemmas and examples, not 61 independent discoveries. Pinned Mathlib supplies finite-field, unit-group, ideal-power, $p$-adic residue and Chinese-remainder results. The new modules connect these to the actual packet coefficients, explicit finite lifts and existing selectors.
23 
24 \subsubsection*{The specification matters}
25 Rational coefficients are not reduced through an imaginary map $\Q\to\F_p$. The proof first constructs their integral lifts in $\Z_p$ and establishes equality in $\Q_p$. Root representatives are actual units at the requested precision, not unchanged residues that need not satisfy the root equation modulo $p^\ell$.
26 
27 \subsubsection*{Verification status}
28 The fresh cumulative Lean build compiled all 28 modules with warnings treated as errors, matched 410 declaration axiom reports, and rejected all 17 invalid-proof controls. All 103 infrastructure and release tests passed. Independent finite regressions are recorded separately from the proofs. A separate release audit records the archive's fresh-extraction rebuild and integrity checks.
29 \par\medskip
30 \pageheading{1. Integral reduction of the original coefficients}{Corollary 8.3; manuscript pages 19--20}
31 Fix a prime $p$, an integer $m\geq1$ and a window address $0\leq j<p$. The earlier project defines the rational packet coefficients by the actual recurrence
32 \[
33  \sum_{q=0}^{n}\binom{mpn+j}{mpq}C_{mp,j}(q)=\delta_{n0}.
34 \]
35 The previous Lucas theorem proves
36 \[
37  \binom{mpn+j}{mpq}\equiv\binom{mn}{mq}\pmod p,\qquad
38  \binom{mpn+j}{mpn}\equiv1\pmod p.
39 \]
40 The last congruence makes each diagonal entry a unit in the actual completed ring $\Z_p$.
41 
42 \subsection*{First construct the integral solution}
43 For a ring $R$, a triangular row system $T$, right-hand side $b$, and proved unit pivots $d_n=T_{nn}$, define
44 \[
45  s_n=d_n^{-1}\left(b_n-\sum_{q<n}T_{nq}s_q\right).
46 \]
47 The new ring-level solver uses well-founded recursion. Its row identities and unique-solution property are proved. The source also proves compatibility of this solver with ring homomorphisms into fields.
48 
49 Specializing to $R=\Z_p$ constructs $c^{(p)}_{m,j}(n)$. Mapping to $\Q_p$ and comparing with the original rational forward substitution gives
50 \[
51  \boxed{c^{(p)}_{m,j}(n)=C_{mp,j}(n)\quad\text{in }\Q_p.}
52 \]
53 Thus every original standard-window coefficient is $p$-integral, for every row. Integrality is a conclusion, not an additional hypothesis on the coefficients.
54 
55 \subsection*{Then apply the residue map}
56 Independently define $e^{(m,p)}$ over $\F_p$ by the unit-diagonal system
57 \[
58  \sum_{q=0}^{n}\binom{mn}{mq}e^{(m,p)}_q=\delta_{n0}.
59 \]
60 Its recurrence and uniqueness are checked. Applying the actual homomorphism $\pi:\Z_p\to\F_p$ to the integral row, and then Lucas reduction, proves
61 \[
62  \boxed{\pi(c^{(p)}_{m,j}(n))=e^{(m,p)}_n.}
63 \]
64 For $j,k<p$, a separate ideal statement gives
65 \[
66  p\mid c^{(p)}_{m,j}(n)-c^{(p)}_{m,k}(n)\quad\text{inside }\Z_p.
67 \]
68 The formal solver also covers $m=0$. The manuscript uses $m\geq1$. No global finite-difference theorem or period assertion enters this proof.
69 
70 \textbf{Principal targets.}\par
71 \target{WindowIndependence.coeffPadic_coe, .standard_window_integral}\par
72 \target{WindowIndependence.residue_independence, .reduced_unique}\par
73 \target{WindowIndependence.two_window_addresses_congruent}
74 \par\medskip
75 \pageheading{2. Explicit finite prime-power decomposition}{Proposition 6.2; odd-prime branch}
76 Let $p$ be prime, $\ell\geq1$, and
77 \[
78  a\in\bigl(\Z/p^\ell\Z\bigr)^\times.
79 \]
80 Define actual units in the same ring by
81 \[
82  \boxed{\omega_\ell(a)=a^{p^{\ell-1}},\qquad
83  \langle a\rangle_\ell=a\,\omega_\ell(a)^{-1}.}
84 \]
85 The Lean source writes $\ell=L+1$, so zero precision is excluded without truncated natural-number subtraction.
86 
87 \subsection*{The root equation and residue are derived}
88 Euler's unit-group exponent gives
89 \[
90  \omega_\ell(a)^{p-1}
91  =a^{p^{\ell-1}(p-1)}=a^{\varphi(p^\ell)}=1.
92 \]
93 Reduction to the actual field $\F_p$ commutes with powers. Its Frobenius identity gives
94 \[
95  \overline{\omega_\ell(a)}
96  =\bar a^{p^{\ell-1}}=\bar a.
97 \]
98 Consequently,
99 \[
100  \boxed{a=\omega_\ell(a)\langle a\rangle_\ell,\quad
101  \omega_\ell(a)^{p-1}=1,\quad
102  \overline{\langle a\rangle_\ell}=1.}
103 \]
104 The manuscript's finite existence conclusion is obtained directly. The proof does not assume a Hensel lift or an already supplied root representative.
105 
106 \subsection*{Uniqueness requires a lifting argument}
107 The source proves the actual kernel statement
108 \[
109  \bar x=0\quad\Longleftrightarrow\quad p\mid x
110  \quad\text{in }\Z/p^\ell\Z.
111 \]
112 For $x\equiv y\pmod p$, the checked ideal-power lifting theorem gives
113 \[
114  x^{p^{\ell-1}}-y^{p^{\ell-1}}\in(p)^\ell=(0).
115 \]
116 If $w^{p-1}=1$, then $w^p=w$ and hence $w^{p^k}=w$ for every $k$. Therefore two roots with the same residue are equal. The decomposition is unique whenever its second factor reduces to one. Multiplicativity of both factors is also proved.
117 
118 For $p=3,\ell=2,a=2$, the checked values are
119 \[
120  \omega_2(2)=8,\qquad \langle2\rangle_2=7,\qquad
121  8^2=1,\quad8\cdot7=2\quad\text{in }\Z/9\Z.
122 \]
123 The unlifted representative $2$ is not a square root of one modulo nine.
124 
125 \textbf{Principal targets.}\par
126 \target{FiniteUnits.finite_unit_decomposition, .power_lift_congruence}\par
127 \target{FiniteUnits.omega_unique, .decomposition_unique}\par
128 \target{FiniteUnits.omega_mul, .principal_mul}
129 \par\medskip
130 \pageheading{3. Precision compatibility and the dyadic sign}{Finite refinements and Proposition 6.2's dyadic branch}
131 For $1\leq k\leq\ell$, let
132 \[
133  \rho_{\ell,k}:\Z/p^\ell\Z\longrightarrow\Z/p^k\Z
134 \]
135 be the actual reduction homomorphism. It induces a map on units. The explicit construction satisfies
136 \[
137  \boxed{\rho_{\ell,k}(\omega_\ell(a))
138  =\omega_k(\rho_{\ell,k}(a)),}
139 \]
140 \[
141  \boxed{\rho_{\ell,k}(\langle a\rangle_\ell)
142  =\langle\rho_{\ell,k}(a)\rangle_k.}
143 \]
144 The proof uses the exponent factorization
145 $p^{\ell-1}=p^{k-1}p^{\ell-k}$ and the already proved Frobenius invariance of a lifted root. Principal factors also satisfy
146 \[
147  \langle a\rangle_\ell^{\,p^{\ell-1}}=1.
148 \]
149 At precision one the principal factor is exactly one. These are coherent finite certificates. No infinite inverse limit or topological unit-group equivalence is constructed in this release.
150 
151 \subsection*{Why the mod-four branch is separate}
152 Now let $\ell\geq2$ and $a\in(\Z/2^\ell\Z)^\times$. The actual units of $\Z/4\Z$ are exhausted by $1$ and $-1$. Define
153 \[
154  \varepsilon_\ell(a)=
155  \begin{cases}1,&a\equiv1\pmod4,\\-1,&a\equiv3\pmod4,\end{cases}
156  \qquad
157  \langle a\rangle_{2,\ell}=\varepsilon_\ell(a)a.
158 \]
159 The source uses $\ell=L+2$. It proves
160 \[
161  \boxed{a=\varepsilon_\ell(a)\langle a\rangle_{2,\ell},\quad
162  \varepsilon_\ell(a)\in\{1,-1\},\quad
163  \langle a\rangle_{2,\ell}\equiv1\pmod4.}
164 \]
165 The sign is uniquely determined by the residue modulo four, and cancellation gives uniqueness of the principal factor.
166 
167 The checked example $a=3$ modulo eight has sign $7=-1$ and principal factor $5$:
168 \[
169  7\cdot5=3\pmod8,\qquad5=1\pmod4.
170 \]
171 The code separately proves $1=-1$ in $\Z/2\Z$ but $1\neq-1$ in $\Z/4\Z$. Modulo two alone cannot identify the sign. The generic prime-power construction at $p=2$ only asks for a principal residue modulo two and is not silently substituted for this stronger mod-four factorization.
172 
173 \textbf{Principal targets.}\par
174 \target{UnitRefinement.omega_compatible, .principal_compatible, .principal_power}\par
175 \target{DyadicUnits.dyadic_unit_decomposition, .decomposition_unique}
176 \par\medskip
177 \pageheading{4. CRT addresses and the actual packet selectors}{Theorem 10.1; manuscript page 22}
178 Let $a\geq0$, let $M$ be odd, and put $N=2^aM$. Coprimality is derived from oddness:
179 \[
180  \gcd(2^a,M)=1.
181 \]
182 The construction uses the actual Chinese-remainder ring equivalence
183 \[
184  \boxed{\Z/N\Z\ \simeq\ \Z/2^a\Z\times\Z/M\Z.}
185 \]
186 Its bijectivity and component formula are checked. On a natural representative $r$, the components are precisely its reductions modulo the two factors, not arbitrary coordinate labels.
187 
188 \subsection*{The algebraic bridge to projectors}
189 For natural indices $n,r$, the source proves
190 \[
191  n\equiv r\pmod{2^aM}
192  \quad\Longleftrightarrow\quad
193  \bigl(n\equiv r\pmod{2^a}\text{ and }n\equiv r\pmod M\bigr).
194 \]
195 For the original coefficient selector
196 \[
197  (P_{N,r}f)(n)=
198  \begin{cases}f(n),&n\bmod N=r,\\0,&\text{otherwise},\end{cases}
199 \]
200 take the canonical label $0\leq r<N$. The logical equivalence yields the actual equality of sequence operators
201 \[
202  \boxed{P_{N,r}f=
203  P_{2^a,\,r\bmod2^a}\bigl(P_{M,\,r\bmod M}f\bigr).}
204 \]
205 This statement holds for coefficients in any type with zero. A separate theorem lifts the equality coefficientwise to the existing formal power-series selectors over any semiring.
206 
207 The cases $a=0$ and $M=1$ are included. The corresponding one-element residue ring is not excluded. Oddness of $M$ already implies positivity.
208 
209 \subsection*{What is not asserted}
210 CRT factors addresses, not the visibility weights or valuation filtrations associated with those addresses. Nothing in this proof gives an equal-weight decomposition at every prime or an additional analytic convergence theorem.
211 
212 Coprimality cannot be discarded. The distinct classes $0$ and $2$ modulo four both map to $(0,0)$ when both components are reduced modulo two. The source checks this counterexample. It also checks a composite-modulus failure of the Fermat exponent and a coefficient outside the standard window that is not $3$-adically integral.
213 
214 \textbf{Principal targets.}\par
215 \target{CRTPackets.address_bijective, .address_components, .residue_equivalence}\par
216 \target{CRTPackets.packet_factorization, .series_packet_factorization}\par
217 \target{FiniteArithmeticExamples.outside_window_not_integral}
218 \par\medskip
219 \pageheading{5. Verification, regressions and remaining work}{Cumulative release evidence}
220 The fresh build started with an empty output directory under Lean 4.34.0-rc2 and Mathlib revision
221 \[
222  \mcode{aeb72f1e9981b6d35b426b16dca7759be3e7ba06}.
223 \]
224 All nine dependency revisions matched the runtime manifest and repository heads.
225 
226 \begin{center}
227 \begin{tabular}{@{}p{.68\textwidth}r@{}}
228 \toprule
229 Check & Result\\\midrule
230 Modules compiled, warnings treated as errors & 28/28\\
231 Named theorem declarations & 333\\
232 Explicit definitions audited separately & 77\\
233 Expected axiom reports matched & 410/410\\
234 Invalid-proof controls rejected & 17/17\\
235 Infrastructure and release tests & 103 passed\\\bottomrule
236 \end{tabular}
237 \end{center}
238 Dependencies are among \mcode{propext}, \mcode{Classical.choice} and \mcode{Quot.sound}, or subsets thereof. The source scan excludes admitted proofs, new axioms and selected trust bypasses. The five new rejection controls cover root lifting, primality, dyadic signs, integrality and coprimality.
239 
240 \subsection*{Independent finite checks}
241 The exact Python mirrors passed 2,132 standard-window coefficient rows, 1,476 prime-power unit cases, 555 exhaustive root-uniqueness checks, 4,594 precision comparisons and 576 multiplicativity comparisons. The dyadic suite checked 454 decompositions and their uniqueness. CRT covered 1,240 addresses and 6,200 selector cases. Thirteen invalid inputs were rejected.
242 
243 These are independently implemented finite arithmetic checks, not code extracted from Lean or replacements for its universal proofs. Their deterministic mathematical payload is replayed separately from elapsed time in the fresh-extraction release audit.
244 
245 \subsection*{Failures and preservation}
246 Eleven of 18 development checks failed before repair, on lemma interfaces, coercions, finite cases and simplification. Their inactive snapshots and diagnostics are retained. All 21 upstream proof files and four earlier supplements are unchanged. Edition-specific test updates retain archived originals.
247 
248 \subsection*{Four items proved in the manuscript remain pending}
249 \begin{center}
250 \begin{tabular}{@{}lp{.79\textwidth}@{}}
251 7.5 & Global odd-prime Euler finite-difference theorem\\
252 8.5 & Uniform standard-window period\\
253 9.1 & Companion jump theorem\\
254 9.2 & Fibonacci packet recurrence\\
255 \end{tabular}
256 \end{center}
257 Three classical inputs and two conjectures remain separate. Mathlib's cache was reused, not independently rebuilt. Earlier papers and historical experiments were not rerun. The preserved manuscript must be read with the cumulative supplements and amendments.

Back to source controls

Back to Realization Calculus