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{Eighth Lean Block Supplement}\label{app:sup8}
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 The all-residue Theorem 7.5 remains pending. This release proves its \textbf{full saturated higher-power estimate throughout the standard window}, rather than only a period modulo $p$. For every prime $p$, positive $m\mid p-1$, $0\le j<p$, and natural $n,k,u$, put $h=(p-1)/m$. Then
5 \[
6 \boxed{\quad
7 \Delta_{uh}^{k}C_{mp,j}(n)=0\quad\text{or}\quad
8 v_p\!\left(\Delta_{uh}^{k}C_{mp,j}(n)\right)\ge\min\{k,mn\}.
9 \quad}
10 \]
11 The unnormalized family $j!C_{mp,j}(n)$ satisfies the same bound. Both statements concern the original rational coefficient function, identified with its actual integral $p$-adic lift. They include $p=2$, $k=0$, $n=0$, and the additional harmless case $u=0$.
12 
13 \textbf{Coverage remains 23 of 24 named items proved in the manuscript.} Three classical inputs and two conjectures remain separate. The new result covers every permissible residue when $m=1$, but not the range $p\le j<mp$ when $m>1$.
14 
15 \begin{center}\begin{tabular}{@{}p{.58\textwidth}rr@{}}\toprule
16 New module & Theorems & Definitions\\\midrule
17 \mcode{DworkAlgebra} & 7 & 3\\
18 \mcode{DworkClosure} & 20 & 2\\
19 \mcode{HurwitzDworkClosure} & 15 & 2\\
20 \mcode{ResidueZeroDwork} & 9 & 2\\
21 \mcode{DifferenceStepMultiples} & 5 & 1\\
22 \mcode{EulerDefect} & 4 & 2\\
23 \mcode{StandardWindowDwork} & 14 & 1\\
24 \mcode{StandardWindowPrecision} & 5 & 0\\
25 \mcode{DworkWindowExamples} & 8 & 0\\\midrule
26 Total added & 87 & 13\\\bottomrule
27 \end{tabular}\end{center}
28 The cumulative corpus has \textbf{526 explicit theorem declarations and 107 explicit definitions in 47 modules}. Counts include support lemmas and examples, not independent discoveries. All 38 upstream proof modules and seven earlier supplements are preserved.
29 
30 \par\medskip
31 \pageheading{1. The characteristic-zero product rule}{The normalized defect is not an ordinary derivation}
32 Let $A$ be a commutative algebra over a characteristic-zero field $K$, and let $U$ be an actual $K$-derivation. The source defines
33 \[
34  B=\frac{U^{p^2}-U^p}{p},\qquad
35  M_q(f,g)=\sum_{a=1}^{q-1}\frac{1}{p}\binom qa
36           (U^a f)(U^{q-a}g),\quad q=p,p^2.
37 \]
38 The coefficients of each $M_q$ are proved integral: the middle entries of a prime-power binomial row are divisible by $p$. In Lean they are implemented as natural quotients, with exact division proved before the product identity is used. Induction on derivative order establishes the full Leibniz formula and hence
39 \[
40 \boxed{B(fg)=B(f)g+fB(g)+M_{p^2}(f,g)-M_p(f,g).}
41 \]
42 The middle terms are essential. At $p=3$, $f=t$ and $g=t^2$, the constant coefficient of $B(fg)$ is $-2$, whereas that of $B(f)g+fB(g)$ is zero. This inequality is itself Lean-checked.
43 
44 \subsection*{All orders, without a circular closure assumption}
45 Let $I\subset A$ be a subring stable under $U$. Define
46 \[
47  \operatorname{Bounded}_r(f)\iff B^s f\in I\ (0\le s\le r),
48  \qquad \operatorname{Flat}(f)\iff B^s f\in I\ (s\ge0).
49 \]
50 The definitions contain no product or inverse closure requirement. Since $B$ commutes with $U$, derivatives of a bounded element remain bounded. Induction on $r$ in the displayed product rule then proves closure under multiplication. The finite middle sums use the lower-order induction hypothesis, not the desired next-order conclusion.
51 
52 For an actual inverse $fg=1$, applying the product rule and multiplying by $g$ gives
53 \[
54  B(g)=-g^2B(f)-gM_{p^2}(f,g)+gM_p(f,g).
55 \]
56 If $g\in I$, induction on $r$ proves boundedness of $g$ from boundedness of $f$. At each successor stage the preceding stage supplies boundedness of $g$ needed on the right. Passing to all finite orders proves reciprocal closure for an integral inverse.
57 
58 \textbf{Principal targets.}\par
59 \target{DworkAlgebra.B_mul}\par
60 \target{DworkClosure.bounded_mul, DworkClosure.bounded_inverse}\par
61 \target{DworkClosure.flat_mul, DworkClosure.flat_inverse}
62 
63 \par\medskip
64 \pageheading{2. The actual integral Hurwitz lattice}{Connecting differential expressions to coefficient divisibility}
65 The specialization works inside $\Q_p[[t]]$ and uses factorial-scaled coefficients
66 \[
67  a_f(d)=d![t^d]f,\qquad
68  I_p=\{f\in\Q_p[[t]]:a_f(d)\in\Z_p\text{ for every }d\}.
69 \]
70 The source constructs $I_p$ as a subring. Actual exponential-series multiplication gives
71 \[
72  a_{fg}(d)=\sum_{r=0}^{d}\binom dr a_f(r)a_g(d-r),
73  \qquad a_{Uf}(d)=a_f(d+1).
74 \]
75 These identities prove multiplication and derivative stability of the lattice. Membership does not require ordinary power-series coefficients to lie in $\Z_p$.
76 
77 \subsection*{The reciprocal is integral}
78 For $f\in I_p$ with constant coefficient one, the usual power-series reciprocal is used. Its inverse equation yields the exact coefficient recurrence
79 \[
80  a_{f^{-1}}(d)=\delta_{d0}-\sum_{r=0}^{d-1}
81      \binom dr a_{f^{-1}}(r)a_f(d-r).
82 \]
83 Strong induction proves that all of these coefficients are integral. Combining this construction with the preceding all-order theorem proves flatness of the \emph{actual reciprocal}. No flatness or integrality of that reciprocal is assumed in the normalized-series specialization.
84 
85 \subsection*{The earlier coefficient criterion is recovered exactly}
86 Define the literal coefficient defect
87 \[
88  (\delta a)(d)=a(d+p^2)-a(d+p).
89 \]
90 The new source proves, for every $s,d$,
91 \[
92  a_{B^s f}(d)=p^{-s}(\delta^s a_f)(d).
93 \]
94 For an integral coefficient $x$, it proves the bridge
95 \[
96 \boxed{p^{-s}x\in\Z_p\quad\Longleftrightarrow\quad p^s\mid x\text{ in }\Z_p.}
97 \]
98 Thus the differential definition is equivalent to the existing coefficient-level Dwork criterion. Division occurs in $\Q_p$, while the assertion after division is membership in $\Z_p$. It is not divisibility in the field. Zero coefficients satisfy every finite precision condition.
99 
100 \textbf{Principal targets.}\par
101 \target{HurwitzDworkClosure.integral_inverse}\par
102 \target{HurwitzDworkClosure.flat_product, HurwitzDworkClosure.flat_reciprocal}\par
103 \target{HurwitzDworkClosure.decode_B_iterate}\par
104 \target{HurwitzDworkClosure.normalized_mem_iff, HurwitzDworkClosure.flat_encode_iff}
105 
106 \par\medskip
107 \pageheading{3. A nonsingular Euler-operator argument}{The standard interval without an analytic power-series-in-the-index premise}
108 On Hurwitz coefficients, the actual Euler operator plus $c$ is
109 \[
110  (\Lambda_c a)(d)=(d+c)a(d).
111 \]
112 Direct induction proves its commutator with every defect iterate:
113 \[
114  \delta^s\Lambda_c a
115  =\Lambda_c\delta^s a
116   +sp\bigl(pU^{p^2}-U^p\bigr)\delta^{s-1}a,
117  \qquad s\ge1.
118 \]
119 Suppose $a$ is integral and supported at degrees divisible by $p$, and $p\nmid c$. Every supported pivot $d+c$ is proved to be a unit of $\Z_p$. The defect preserves this support. Induction in the commutator identity therefore proves
120 \[
121  \operatorname{Flat}(\Lambda_c a)\Longrightarrow\operatorname{Flat}(a).
122 \]
123 This is a reflection theorem on the integral supported domain. It does not assume flatness of the proposed preimage, and does not assert invertibility at a singular pivot $p\mid c$.
124 
125 \subsection*{Apply it to the explicit normalized sections}
126 Set $N=mp$ and, for $0\le j<p$, define integral Hurwitz coefficients
127 \[
128  g_j(d)=
129  \begin{cases}
130  \displaystyle\binom{d+j}{d}^{-1},&N\mid d,\\[1mm]
131  0,&N\nmid d.
132  \end{cases}
133 \]
134 The inverse binomial is constructed using the actual unit pivots already proved by Lucas reduction. Its image in $\Q_p$ is proved equal to the displayed reciprocal.
135 
136 For $j=0$, $g_0$ is the literal $N$-divisibility indicator. Because $N\mid p(p-1)$, the two shifts in $\delta g_0$ agree and $\delta g_0=0$. It is flat at every order. The actual binomial identity gives
137 \[
138  \Lambda_{j+1}g_{j+1}=(j+1)g_j.
139 \]
140 As $1\le j+1<p$, the nonsingular reflection theorem inductively proves flatness of every $g_j$ in the standard window. There is no uniform-convergence assumption in this argument.
141 
142 \textbf{Principal targets.}\par
143 \target{EulerDefect.iterated_commutator, EulerDefect.flat_of_euler_flat}\par
144 \target{StandardWindowDwork.kernel_coe, StandardWindowDwork.kernel_euler_step}\par
145 \target{StandardWindowDwork.kernel_flat}
146 
147 \par\medskip
148 \pageheading{4. From these sections to the original Euler packets}{Actual reciprocal, actual rational sequence, every order and step multiple}
149 The factorial-ratio identity is proved coefficient by coefficient:
150 \[
151  \sum_{d\ge0}g_j(d)\frac{t^d}{d!}
152  =j!\sum_{r\ge0}\frac{t^{Nr}}{(Nr+j)!}.
153 \]
154 The right side is precisely the normalized source kernel from the first block, not a replacement family. The earlier rational identity for its reciprocal is transported to $\Q_p[[t]]$. A separate encoding theorem identifies the reciprocal's coefficients with the already constructed $\Z_p$ lifts of the original $C_{N,j}(r)$.
155 
156 All-order reciprocal closure therefore gives flatness of the actual packed Euler coefficient sequence. The earlier coefficient-extraction theorem now has a \emph{proved antecedent} for every $j<p$, and yields
157 \[
158  p^{\min(k,mn)}\mid\Delta_h^k C_{mp,j}(n)\quad\text{in }\Z_p,
159  \qquad h=(p-1)/m.
160 \]
161 A new finite telescoping argument proves the extension to arbitrary natural multiples of $h$. Its first-step identity is
162 \[
163  f(n+uh)-f(n)=\sum_{a=0}^{u-1}\Delta_h f(n+ah).
164 \]
165 Commutation of differences and induction on their order transfer any fixed ideal bound valid on a forward tail. The required precision $\min(k,mn)$ is nondecreasing as the starting row advances. Hence
166 \[
167  \boxed{p^{\min(k,mn)}\mid\Delta_{uh}^{k}C_{mp,j}(n)\quad(0\le j<p).}
168 \]
169 
170 The scalar-extension bridge identifies these differences with the original rational coefficient function. The rational theorem explicitly allows zero differences, avoiding the library's finite valuation convention at zero. Since $j!$ is a unit for $j<p$, both normalized and unnormalized versions have the same precision.
171 
172 \textbf{Scope.} The proof includes all primes, all rows and orders, and all natural step multipliers. For $m=1$, the standard window is the complete allowed residue range. For larger $m$, residues $p\le j<mp$ are not covered by this theorem. The earlier one-power period is not the source of the new higher-power estimate.
173 
174 \textbf{Principal targets.}\par
175 \target{StandardWindowDwork.window_is_reciprocal, StandardWindowDwork.standard_window_flat}\par
176 \target{StandardWindowDwork.standard_window_global_bound}\par
177 \target{StandardWindowPrecision.normalized_window_precision}\par
178 \target{StandardWindowPrecision.unnormalized_window_precision}\par
179 \target{StandardWindowPrecision.modulus_p_complete_family}
180 
181 \par\medskip
182 \pageheading{5. Examples, verification and the remaining gap}{The coverage count is unchanged; the unresolved theorem now has a stronger proved part}
183 The original rational recurrence gives
184 \[
185  C_{6,2}(1)=-\frac1{28},\quad C_{6,2}(2)=\frac{425}{364},\quad
186  C_{6,2}(3)=-\frac{2039759}{2660}.
187 \]
188 Consequently, the new source proves
189 \[
190  \Delta_1^2 C_{6,2}(1)=-\frac{949959}{1235},\qquad
191  v_3\!\left(\Delta_1^2 C_{6,2}(1)\right)=2.
192 \]
193 This attains the bound $\min(2,2\cdot1)=2$. A claim of a third power is rejected. The separate cubic example proves that the normalized differential defect is not an ordinary derivation. Controls also reject an asserted unit pivot at $c=p$ and the prime-power binomial-divisibility formula at a composite base.
194 
195 \subsection*{Recorded checks}
196 The cumulative verifier rebuilds all 47 modules and audits all 633 explicit declarations: 526 theorems and 107 definitions. Warnings are errors, unexpected axiom dependencies are rejected, and 27 deliberately invalid proof controls are tested. The allowed transitive axioms remain \mcode{propext}, \mcode{Classical.choice} and \mcode{Quot.sound}. Exact results, compiler commands and source hashes are in the accompanying machine-readable reports.
197 
198 All 189 infrastructure and release tests passed. Independent exact-arithmetic mirrors checked 3,040 normalized and 3,040 unnormalized bounds in 95 standard-window families, 6,596 source defects and 6,596 reciprocal defects, 75 product identities, 360 inverse-closure cases, 720 Euler commutators and 150 telescoping identities. They are finite Python mirrors, not code extracted from Lean and not substitutes for the universal proofs.
199 
200 Failed development snapshots and diagnostics are preserved separately. Historical source files and earlier supplements remain unchanged. Mathlib's pinned compiled cache is reused, not independently rebuilt. The original historical numerical suite is not rerun. The manuscript-to-formal correspondence remains a mathematical review.
201 
202 \subsection*{What is still unproved}
203 The all-residue Theorem 7.5 requires the additional range $p\le j<mp$. Its supporting prose proof treats singular ratios at $c=p,2p,\ldots,(m-1)p$ through weighted Amice estimates and a dual Mahler pairing, then propagates across the intervening indices. Those actual-family estimates and the full remaining propagation are not supplied by this release. A unit argument at $p\nmid c$ cannot be used at $p\mid c$.
204 
205 \textbf{Release boundary: 23/24 named items proved in the manuscript, with Theorem 7.5 still pending.} The two conjectures remain unproved. The proved standard-window result is an infinite family, but no numerical proportion of the remaining work is inferred from the width of that window.

Back to source controls

Back to Realization Calculus