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 \section{Congruential Euler packets and their arithmetic}
2 \label{sec:arithmetic}
3 
4 Two related constructions run through this section.  The congruential
5 Euler family is indexed by a modulus $N$ and an address $j$.  Its
6 exceptional dyadic member has $N=4$ and four addresses.  The classical
7 signed Euler numbers arise from $N=2$, $j=0$.  Keeping these indices
8 visible distinguishes the four-packet period theorems from the classical
9 edge truncations.
10 
11 \subsection{Original coefficients, normalized packets, and precision}
12 
13 \begin{definition}[Congruential Euler coefficients]\label{def:arith-euler}
14 For $N\ge1$ and $0\le j<N$, define rational coefficients by the formal identity
15 \begin{equation}\label{eq:arith-euler-egf}
16  \sum_{d\ge0}E_d^{(N,j)}\frac{t^d}{d!}
17  =\left(\sum_{n\ge0}\frac{t^{Nn}}{(Nn+j)!}\right)^{-1}.
18 \end{equation}
19 The reciprocal exists because its denominator has constant coefficient
20 $1/j!\ne0$.  Set
21 \[
22  U_{N,j}(n)=E_{Nn}^{(N,j)},\qquad C_{N,j}(n)=\frac{U_{N,j}(n)}{j!}.
23 \]
24 Thus $C_{N,j}(0)=1$ and $U_{N,j}(0)=j!$.  All coefficients outside the
25 multiples of $N$ vanish.
26 \end{definition}
27 
28 The normalized source and its inverse are
29 \begin{equation}\label{eq:arith-kernel}
30  K_{N,j}(t)=j!\sum_{n\ge0}\frac{t^{Nn}}{(Nn+j)!},\qquad
31  \mathcal P_{N,j}(t)=\sum_{n\ge0}C_{N,j}(n)\frac{t^{Nn}}{(Nn)!}.
32 \end{equation}
33 Their product is one.  Clearing factorials in its coefficient of $t^{Nn}$
34 gives the triangular system
35 \begin{equation}\label{eq:arith-triangular}
36  \sum_{q=0}^{n}\binom{Nn+j}{Nq}C_{N,j}(q)=\delta_{n0}.
37 \end{equation}
38 In particular, for $n>0$,
39 \[
40  C_{N,j}(n)=-\binom{Nn+j}{Nn}^{-1}
41        \sum_{q=0}^{n-1}\binom{Nn+j}{Nq}C_{N,j}(q).
42 \]
43 The diagonal binomial coefficient is positive, so this recurrence determines
44 the sequence uniquely.  The Lean construction begins with this recurrence
45 and derives the reciprocal identity from it.  The resulting sequence is
46 then identified with the degree-indexed coefficients of
47 \eqref{eq:arith-euler-egf}, so both descriptions refer to the same family.
48 
49 The relevant declarations are
50 \lean{KomorebiPaperIX.Congruential.triangular_inverse},
51 \lean{KomorebiPaperIX.Congruential.packet_is_actual_inverse}, and
52 \lean{KomorebiPaperIX.NishibuchiCompletion.generalizedEuler_at_packet}.
53 The cleared identity with the original positive-address exponential section
54 is \lean{KomorebiPaperIX.NishibuchiCompletion.original_generating_identity}.
55 
56 \begin{proposition}[A denominator bound for every address]
57 \label{prop:arith-denominator}
58 For $N\ge1$, $0\le j<N$, and $n\in\N$, set
59 \[
60  D_{N,j}(n)=\prod_{r=1}^{n}\binom{Nr+j}{Nr},\qquad D_{N,j}(0)=1.
61 \]
62 Then $D_{N,j}(n)C_{N,j}(n)\in\Z$.
63 \end{proposition}
64 
65 \begin{proof}
66 Proceed by induction in the recurrence \eqref{eq:arith-triangular}.
67 For every $q<n$, the product $D_{N,j}(q)$ divides $D_{N,j}(n-1)$.
68 Multiplying the recurrence by $D_{N,j}(n-1)$ therefore makes every
69 previous term integral.  The diagonal factor completes the product
70 $D_{N,j}(n)$, proving the claim.  At $n=0$, both factors are one.
71 This gives a uniform denominator bound without requiring integrality of
72 the normalized coefficients themselves.  The Lean statements are
73 \lean{KomorebiPaperIX.Congruential.clearing_product} and
74 \lean{KomorebiPaperIX.Congruential.universal_denominator_clearing}.
75 \end{proof}
76 
77 \begin{example}[The Bernoulli boundary address]\label{ex:arith-bernoulli}
78 At $N=2$, the address $j=1$ gives a second classical family.  Define the
79 Bernoulli numbers by
80 \[
81  B(z)=\frac{z}{e^z-1}=\sum_{r\ge0}B_r\frac{z^r}{r!},
82  \qquad B_0=1,\quad B_1=-\frac12.
83 \]
84 All quotients here are regular formal series.  The identity
85 \[
86  2B(z)-B(2z)=\frac{z}{\sinh z}
87             =\sum_{n\ge0}C_{2,1}(n)\frac{z^{2n}}{(2n)!}
88 \]
89 follows by putting the two fractions on a common denominator and using
90 \eqref{eq:arith-euler-egf}.  Comparing even coefficients yields
91 \[
92  C_{2,1}(n)=(2-2^{2n})B_{2n}\qquad(n\in\N).
93 \]
94 This classical derivation restores the boundary example from the original
95 manuscript.  No dedicated Lean bridge for this Bernoulli specialization
96 was identified in the preserved sources.
97 \end{example}
98 
99 \begin{definition}[Differences and valuation conventions]\label{def:arith-precision}
100 For a sequence $f$ and $h,k,n\in\N$, put
101 \[
102  \Delta_h f(n)=f(n+h)-f(n),\qquad
103  \Delta_h^0 f(n)=f(n),\qquad
104  \Delta_h^{k+1}f(n)=\Delta_h^k f(n+h)-\Delta_h^k f(n).
105 \]
106 We use the extended valuation $v_p(0)=+\infty$ in mathematical statements.
107 Thus $v_p(x)\ge L$, including negative integers $L$, means
108 $x=0$ or the ordinary valuation of the nonzero rational $x$ is at least $L$.
109 For integral coefficients and $L\ge0$, it is equivalent to
110 $x\in p^L\Z_p$.  In expressions involving a step multiplier we write
111 $\nu_p(u)=v_p(u)$ for $u>0$ and set $\nu_p(0)=0$.  This finite convention
112 makes the displayed exponents meaningful at step zero, where all
113 positive-order differences vanish.
114 \end{definition}
115 
116 The valuation convention at zero is encoded by
117 \lean{KomorebiPaperIX.GlobalEulerBoundary.precision}.  For $p$-adic
118 congruences, divisibility is interpreted in $\Z_p$. Statements over other
119 coefficient rings specify the ring explicitly.  Field divisibility in
120 $\Q_p$ alone does not encode precision.
121 
122 \subsection{The standard address window and its common reduction}
123 
124 The addresses below the prime have unit diagonal coefficients.  In this
125 window the normalized packets are integral, and their reductions agree
126 at every row.
127 
128 \begin{proposition}[Lucas reduction and address independence]
129 \label{prop:arith-lucas-window}
130 Let $p$ be prime, $m>0$, and $N=mp$.  For $0\le j<p$ and $n,q\in\N$,
131 \[
132  \binom{mpn+j}{mpq}\equiv\binom{mn}{mq}\pmod p.
133 \]
134 Every $C_{mp,j}(n)$ belongs to $\Z_p$.  Its reduction is the unique
135 sequence $\overline C_m:\N\to\F_p$ satisfying
136 \[
137  \sum_{q=0}^{n}\binom{mn}{mq}\overline C_m(q)=\delta_{n0}
138  \quad\text{in }\F_p.
139 \]
140 Consequently, for any two addresses $0\le j,k<p$,
141 \[
142  C_{mp,j}(n)\equiv C_{mp,k}(n)\pmod p\qquad(n\in\N).
143 \]
144 \end{proposition}
145 
146 \begin{proof}
147 Lucas reduction separates the lowest base-$p$ digits, which are $j$ and
148 zero in the upper and lower arguments.  Their binomial contribution is
149 one, leaving the displayed reduced row.  On the diagonal the reduced
150 coefficient is one.  The recurrence \eqref{eq:arith-triangular} therefore
151 constructs an integral packet by successive division by units in $\Z_p$.
152 After reduction, every address satisfies the same triangular system over
153 $\F_p$.  Its diagonal entries are one, so its solution is unique.  This
154 proves both the common reduction and the congruence between addresses.
155 The row reduction is
156 \lean{KomorebiPaperIX.StandardWindow.lucas_row_reduction}.
157 The integral identification and the two reduction statements are
158 \lean{KomorebiPaperIX.WindowIndependence.standard_window_integral},
159 \lean{KomorebiPaperIX.WindowIndependence.coeffPadic_coe},
160 \lean{KomorebiPaperIX.WindowIndependence.residue_independence}, and
161 \lean{KomorebiPaperIX.WindowIndependence.two_window_addresses_congruent}.
162 \end{proof}
163 
164 \subsection{The full Nishibuchi statement and its starting bound}
165 
166 \begin{theorem}[Nishibuchi congruence]\label{thm:arith-nishibuchi}
167 Let $p$ be prime, let $m>0$, and suppose that $m\mid p-1$ or $m=2$.
168 Put $N=mp$ and $q=\operatorname{lcm}(2,p-1)$.  For every $0\le j<N$,
169 all $U_{N,j}(n)$ belong to $\Z_p$.  For $r\ge1$ and $n\ge r$,
170 \begin{equation}\label{eq:arith-nishibuchi}
171  E_{Nn+qp^r}^{(N,j)}\equiv E_{Nn}^{(N,j)}\pmod{p^r}.
172 \end{equation}
173 Thus the positive sufficient starting index $n_0=r$ works uniformly.
174 If $m\mid p-1$, the stronger sufficient condition $r\le mn$ is valid.
175 \end{theorem}
176 
177 This theorem covers the full parameter range and displacement of Conjecture
178 3.9 in the fixed version of Nishibuchi's paper used for the statement
179 comparison.  The corresponding Lean theorem is
180 \lean{KomorebiPaperIX.NishibuchiCompletion.conjecture_3_9}.
181 The stronger divisor-branch threshold is
182 \lean{KomorebiPaperIX.NishibuchiCompletion.divisor_period}.
183 The starting index is sufficient uniformly, although it need not be the
184 earliest one for a given tuple of parameters.
185 
186 We first prove the difference estimates on the divisor branch, then derive
187 the period from a finite Newton expansion.
188 
189 \begin{theorem}[All-address differences on the divisor branch]
190 \label{thm:arith-divisor-base}
191 Let $p$ be prime, $m>0$, $m\mid p-1$, $N=mp$, and $0\le j<N$.
192 Write $h=(p-1)/m$.  For every $u,k,n\in\N$,
193 \begin{align}
194  U_{N,j}(n)&\in\Z_p,\label{eq:arith-divisor-integral}\\
195  \Delta_{uh}^{k}U_{N,j}(n)&\in p^{\min(k,mn)}\Z_p,\label{eq:arith-divisor-bound}\\
196  v_p\bigl(\Delta_{uh}^{k}C_{N,j}(n)\bigr)
197    &\ge\min(k,mn)-v_p(j!).\label{eq:arith-divisor-normalized}
198 \end{align}
199 The factorial correction is part of the normalized statement, including
200 addresses $j\ge p$.
201 \end{theorem}
202 
203 \begin{proof}
204 Work in the Hurwitz integral ring of formal series
205 \[
206  \mathcal H_p=\left\{F\in\Q_p[[t]]:
207             d![t^d]F\in\Z_p\text{ for every }d\right\}.
208 \]
209 For $D=d/dt$, let $B_p=(D^{p^2}-D^p)/p$.  Call $F$ flat if
210 $B_p^sF\in\mathcal H_p$ for every $s\ge0$.
211 We will prove that $j!\mathcal P_{N,j}$ is flat at every address.  The main
212 difficulty is to include the addresses at which the usual unit-pivot
213 argument fails.
214 
215 Set
216 \[
217  H_c(t)=\sum_{n\ge0}\frac{t^{Nn+c}}{(Nn+c)!},\qquad
218  A_c(t)=\sum_{n\ge0}\frac{t^{Nn}}{(Nn+c)!},\qquad
219  R_c(t)=\frac{A_{c-1}(t)}{A_c(t)}\quad(1\le c<N).
220 \]
221 The denominator of this last quotient has nonzero constant coefficient.
222 The section identities give
223 \[
224  R_cH_c=tH_{c-1},\qquad R_c(0)=c,\qquad
225  j!\mathcal P_{N,j}=\mathcal P_{N,0}\prod_{c=1}^{j}R_c.
226 \]
227 Cancellation of consecutive source sections proves the product identity
228 and ties the ratios directly to the family under study.
229 
230 At the singular addresses $c=ap$, $1\le a<m$, use the weighted ring
231 \[
232  \mathcal W_p=\left\{\sum_{d\ge0}a_dT^d:
233           p^{\lfloor d/p\rfloor}a_d\in\Z_p\right\}.
234 \]
235 The key estimate is $R_{ap}(\log(1+T))\in\mathcal W_p$.  Its arithmetic
236 input comes from the cyclic group ring $\Z[\Z/N\Z]$.
237 For its canonical element $x$ and $I=(p,x^{p-1}-1)$, the relation
238 $(x^{p-1})^p=1$ implies $I^p\subseteq(p)I$.  Induction yields
239 $I^q\subseteq(p^{v_p(q!)})$.  Grouping the falling factorial
240 $(x)_d=\prod_{i=0}^{d-1}(x-i)$ into consecutive blocks of length $p$
241 then gives an integral residue-coordinate factor
242 $p^{v_p(\lfloor d/p\rfloor!)}$.  The identity
243 \[
244  v_p(d!)=\lfloor d/p\rfloor+v_p(\lfloor d/p\rfloor!)
245 \]
246 accounts for precisely the weight in $\mathcal W_p$ after dividing by $d!$.
247 Comparison of the section and group-ring recurrences identifies these
248 coordinates with the logarithmically substituted section.
249 
250 To pass from the section to the singular ratio, factor out its initial zero:
251 for $c=ap$, the section has the form
252 \[
253  H_c(\log(1+T))=\frac{T^c}{c!}\,V(T),\qquad V(0)=1,
254  \qquad V\in\mathcal W_p.
255 \]
256 The weight of $c!$ compensates for the coefficient shift by $c$.
257 The weighted ring is closed under inversion of series with constant
258 coefficient one and under $L_T=\log(1+T)(1+T)d/dT$.  With
259 $\ell(T)=\log(1+T)/T$, interpreted by coefficient shifting, differentiation
260 of the displayed factorization gives
261 \[
262  R_c(\log(1+T))=c(1+T)\ell(T)+(L_TV)V^{-1}.
263 \]
264 Since $p\ell(T)\in\mathcal W_p$ and $p\mid c$, both terms are weighted.
265 This is the singular estimate
266 \lean{KomorebiPaperIX.SingularRatioAmice.paper_singular_amice_estimate}.
267 
268 To deduce flatness from the weighted estimate, use
269 $\Theta=(1+T)d/dT$.  Both $\Theta$ and
270 $(\Theta^{p^2}-\Theta^p)/p$ preserve $\mathcal W_p$.
271 For the first operator, its coefficient formula is
272 $(d+1)a_{d+1}+da_d$. Whenever the floor weight rises, the factor $d+1$
273 provides the missing $p$.  For the second operator, the proof uses its
274 full Leibniz correction and the scalar congruence
275 $p^2\mid b^{p^2}-b^p$.  Weighted monomials factor as
276 \[
277  a_dT^d=(p^{\lfloor d/p\rfloor}a_d)
278           (T^p/p)^{\lfloor d/p\rfloor}T^{d\bmod p}.
279 \]
280 The operator preserves these monomials and hence finite weighted
281 polynomials.  Each fixed output coefficient depends on only finitely many
282 input coefficients, which extends the result to the formal series.
283 Substitution $T=e^t-1$ intertwines $D$ with $\Theta$ and maps
284 $\mathcal W_p$ into $\mathcal H_p$, because
285 \[
286  d![t^d]F(e^t-1)=[T^0]\Theta^dF.
287 \]
288 It follows that the singular ratios are flat.  This transfer is proved in
289 \lean{KomorebiPaperIX.WeightedDworkTransfer.singular_ratio_flat}.
290 
291 At a nonsingular address $2\le c<N$ with $p\nmid c$, differentiation of the section
292 identities gives
293 \[
294  tR_c'=R_c(1+R_{c-1}-R_c).
295 \]
296 Writing $q=R_{c-1}-(c-1)$ and $y=R_c-c$, this becomes
297 \[
298  (tD+c)y=cq+yq-y^2.
299 \]
300 On degrees divisible by $p$, the inverse of $tD+c$ divides the degree-$d$
301 coefficient by the unit $d+c$.  Starting with $y_0=0$, form
302 \[
303  y_{s+1}=(tD+c)^{-1}(cq+y_sq-y_s^2).
304 \]
305 Flatness and support are preserved. Indeed, put $E_c=tD+c$ and $C_p=pD^{p^2}-D^p$.
306 The commutator is $[B_p,E_c]=C_p$, and iteration gives
307 \[
308  B_p^rE_cy=E_cB_p^ry+rC_pB_p^{r-1}y.
309 \]
310 For the inverse equation $E_cy=f$, induction on $r$ makes the
311 correction term Hurwitz-integral. Both operators preserve support in
312 degrees divisible by $p$. On that support the degree multiplier $d+c$
313 is a unit, so integrality of $E_cB_p^ry$ implies integrality of
314 $B_p^ry$. Thus the inverse preserves full flatness, as well as support.
315  Since the difference of two right
316 sides factors as $(z-y)(q-z-y)$ and its second factor has zero constant
317 term, agreement with the solution gains one coefficient at each iteration.
318 Consequently $[t^d]y_s=[t^d]y$ for $d\le s$.
319 Every coefficient of $B_p^r y$ can therefore be read from a sufficiently
320 long finite iterate.  The argument is entirely formal.
321 This is the content of
322 \lean{KomorebiPaperIX.RiccatiFlatPropagation.riccati_solution_flat}.
323 
324 The standard window supplies the initial ratio $R_1$.  The weighted
325 estimate handles $p\mid c$, and Riccati propagation handles $p\nmid c$.
326 Flatness is closed under products, so the exact factorization establishes
327 flatness of $j!\mathcal P_{N,j}$.  Extracting its supported Hurwitz coefficients
328 and applying the proved saturation and step-multiple lemmas yields
329 \eqref{eq:arith-divisor-integral}--\eqref{eq:arith-divisor-bound}.
330 
331 Here is the coefficient extraction explicitly. If $a_d=d![t^d]F$,
332 then
333 \[
334  d![t^d]B_p^kF=p^{-k}\Delta_{p(p-1)}^ka_{d+pk}.
335 \]
336 For $F=j!\mathcal P_{N,j}$ and $k\le mn$, take $d=mpn-pk$.
337 Support in multiples of $mp$ turns this into
338 $p^{-k}\Delta_h^kU_{N,j}(n)$, so flatness gives divisibility by $p^k$.
339 For $k>mn$, expand $\Delta_h^{k-mn}$ applied to
340 $\Delta_h^{mn}U_{N,j}(n)$. Every shifted row is at least $n$, so
341 each summand is divisible by $p^{mn}$. Finally
342 $\Delta_{uh}=((I+\Delta_h)^u-I)$, whose $k$th power for $u>0$
343 is an integral combination of powers of $\Delta_h$ of order at least $k$.
344 The case $u=0$ gives zero for $k>0$, and order zero is the original
345 integral coefficient. This proves the bound for all $u$ and $k$.
346 Finally $\Delta_{uh}^kU_{N,j}=j!\Delta_{uh}^kC_{N,j}$ gives
347 \eqref{eq:arith-divisor-normalized}, with the zero case retained.
348 The resulting statements are
349 \lean{KomorebiPaperIX.AllResidueEuler.all_residue_flat},
350 \lean{KomorebiPaperIX.AllResidueEuler.global_unnormalized_bound}, and
351 \lean{KomorebiPaperIX.AllResidueEuler.global_normalized_precision}.
352 \end{proof}
353 
354 \begin{example}[Why the factorial loss is necessary]
355 \label{ex:arith-normalization-loss}
356 Take $p=3$, $m=2$, $N=6$, and $j=3$.  The recurrence gives
357 \[
358  C_{6,3}(1)=-\frac1{84},\qquad
359  C_{6,3}(2)=\frac{703}{5460},\qquad
360  C_{6,3}(2)-C_{6,3}(1)=\frac{64}{455}.
361 \]
362 The last difference has $3$-adic valuation zero.  Here $h=1$, so at
363 $n=1$ the order-one bound without factorial loss would require valuation
364 at least one.  The corrected normalized bound is sharp, since
365 \[
366  v_3\bigl(C_{6,3}(2)-C_{6,3}(1)\bigr)=0=1-v_3(3!).
367 \]
368 Multiplication by $3!$ gives
369 \[
370  U_{6,3}(2)-U_{6,3}(1)=\frac{384}{455},\qquad
371  v_3\bigl(U_{6,3}(2)-U_{6,3}(1)\bigr)=1,
372 \]
373 consistent with the unnormalized theorem.  Thus the factorial correction
374 is already necessary at a single step in the all-address parameter range.
375 These exact values and the refutation of a universal bound without loss
376 are formalized in
377 \lean{KomorebiPaperIX.Normalization.normalized_first},
378 \lean{KomorebiPaperIX.Normalization.normalized_second},
379 \lean{KomorebiPaperIX.Normalization.normalized_difference},
380 \lean{KomorebiPaperIX.Normalization.difference_valuation},
381 \lean{KomorebiPaperIX.Normalization.factorial_loss_is_sharp},
382 \lean{KomorebiPaperIX.Normalization.unnormalized_difference},
383 \lean{KomorebiPaperIX.Normalization.unnormalized_difference_valuation}, and
384 \lean{KomorebiPaperIX.Normalization.universal_no_loss_refuted}.
385 \end{example}
386 
387 \begin{corollary}[A common period in the standard window]
388 \label{cor:arith-window-period}
389 Let $p$ be prime, $m>0$, $m\mid p-1$, and $0\le j<p$.  Put
390 $h=(p-1)/m$.  For every $n\ge1$ and $u\in\N$,
391 \[
392  \overline C_m(n+uh)=\overline C_m(n),\qquad
393  C_{mp,j}(n+uh)\equiv C_{mp,j}(n)\pmod p.
394 \]
395 Thus $h$ is a sufficient period from row one, common to all addresses
396 in the standard window.  It need not be the least period.
397 \end{corollary}
398 
399 \begin{proof}
400 Since $j<p$, the factorial $j!$ is a unit in $\Z_p$.  Also $mn\ge1$.
401 The order-one case of Theorem~\ref{thm:arith-divisor-base} therefore gives
402 valuation at least one for the normalized difference at every step $uh$.
403 This proves the congruence, and Proposition~\ref{prop:arith-lucas-window}
404 identifies its reduction with the equality for $\overline C_m$.
405 The preserved Lean development also proves this period directly from the
406 Hurwitz inverse in characteristic $p$:
407 \lean{KomorebiPaperIX.WindowPeriod.uniform_standard_window_period},
408 \lean{KomorebiPaperIX.WindowPeriod.multiple_period}, and
409 \lean{KomorebiPaperIX.WindowPeriod.standard_window_period_divisibility}.
410 \end{proof}
411 
412 \begin{lemma}[Prime-power period from finite differences]
413 \label{lem:arith-newton-period}
414 Let $R$ be a commutative ring, $p$ a prime, $f:\N\to R$, $h,n\in\N$,
415 and $r\ge1$.  If
416 \[
417  p^{\min(k,r)}\mid\Delta_h^k f(n)\quad\text{for every }k\in\N,
418 \]
419 then $p^r\mid f(n+p^{r-1}h)-f(n)$.
420 \end{lemma}
421 
422 \begin{proof}
423 The finite Newton expansion gives
424 \[
425  f(n+p^{r-1}h)-f(n)
426  =\sum_{k=1}^{p^{r-1}}\binom{p^{r-1}}k\Delta_h^k f(n).
427 \]
428 Terms with $k\ge r$ have the required factor from the difference.
429 For $1\le k<r$, the identity
430 \[
431  k\binom{p^{r-1}}k=p^{r-1}\binom{p^{r-1}-1}{k-1}
432 \]
433 and $v_p(k)<k$ imply
434 $p^r\mid\binom{p^{r-1}}k p^k$ in $\Z$.
435 Mapping that integer divisibility to $R$ proves the claim term by term.
436 The argument includes $r=1$.
437 The declaration is
438 \lean{KomorebiPaperIX.PeriodFromDifferences.prime_power_period}.
439 \end{proof}
440 
441 \begin{proof}[Proof of Theorem~\ref{thm:arith-nishibuchi}]
442 On the divisor branch, $m\mid q$ and the packet step $q/m$ is an integer
443 multiple of $h=(p-1)/m$.  If $r\le mn$, Theorem~\ref{thm:arith-divisor-base}
444 supplies the hypotheses of Lemma~\ref{lem:arith-newton-period}.
445 Its packet displacement is $p^{r-1}q/m$, which converts to the original
446 degree as follows:
447 \[
448  mp\left(n+p^{r-1}\frac qm\right)=mpn+qp^r.
449 \]
450 The choice $n\ge r$ implies $mn\ge r$ because $m\ge1$.
451 
452 For an odd prime, $2\mid p-1$, so the option $m=2$ introduces no further
453 case.  The sole remaining branch is $p=2,m=2,N=4$.  The all-row theorem
454 proved next gives $2^k\mid\Delta_1^kC_{4,j}(n)$ at every row and address.
455 After multiplying by $j!$, Lemma~\ref{lem:arith-newton-period} gives packet
456 period $2^{r-1}$ and degree displacement $4\cdot2^{r-1}=2^{r+1}=qp^r$.
457 It also gives integrality.  Hence the complete statement follows.
458 The formal degree conversion is
459 \lean{KomorebiPaperIX.NishibuchiCompletion.original_degree_shift}.
460 The all-parameter degree theorem is
461 \lean{KomorebiPaperIX.NishibuchiCompletion.full_period_degree}.
462 \end{proof}
463 
464 \subsection{All-row dyadic differences and displacement amplification}
465 
466 For the remainder of the four-packet discussion abbreviate
467 $C_j=C_{4,j}$ and $U_j=U_{4,j}$.  Removing the original row cap requires
468 an unshifted coefficient operator.
469 
470 \begin{theorem}[All-row dyadic higher differences]\label{thm:arith-dyadic-differences}
471 For $0\le j<4$ and all $u,k,n\in\N$,
472 \begin{align}
473  C_j(n)&\in\Z_2,\\
474  \Delta_u^kC_j(n)&\in 2^{k(1+\nu_2(u))}\Z_2,\label{eq:arith-allrow-c}\\
475  \Delta_u^kU_j(n)&\in
476  2^{k(1+\nu_2(u))+v_2(j!)}\Z_2.\label{eq:arith-allrow-u}
477 \end{align}
478 There is no restriction $k\le n$ and no minimum with the row $n$.
479 \end{theorem}
480 
481 \begin{proof}
482 The Hurwitz coefficients of the normalized source $K_{4,j}$ at degrees
483 $4n$ are
484 \[
485  g_j(n)=\binom{4n+j}{4n}^{-1}.
486 \]
487 Their explicit expressions are
488 \[
489  \begin{aligned}
490  g_0(n)&=1,&
491  g_1(n)&=\frac1{4n+1},\\
492  g_2(n)&=\frac1{(4n+1)(2n+1)},&
493  g_3(n)&=\frac3{(4n+1)(2n+1)(4n+3)}.
494  \end{aligned}
495 \]
496 Every denominator is odd.  An affine sequence with even slope satisfies
497 $2^k\mid\Delta_1^k f(n)$ for every $k,n$.  The exact product identity
498 \[
499  \Delta_1^s(fg)(n)=\sum_{i=0}^s\binom si
500           \Delta_1^if(n)\Delta_1^{s-i}g(n+i)
501 \]
502 proves closure of this property under products.  Applying the formula
503 with the factors interchanged to $fg=1$ isolates $f(n+s)\Delta_1^sg(n)$.
504 Multiplication by $f(n+s)^{-1}$ and induction then prove closure under
505 pointwise unit inverses.
506 Thus all four $g_j$ have the property.  The explicit formulas and difference
507 bounds are formalized in
508 \lean{KomorebiPaperIX.DyadicFourKernel.source_coe} and
509 \lean{KomorebiPaperIX.DyadicFourKernel.source_kummer}.
510 
511 For an integer charge $c$, put
512 \[
513  A_c=\frac{D^4-c}{2}.
514 \]
515 A series is flat of charge $c$ when applying any power $A_c^s$ to it gives
516 an element of $\mathcal H_2$.  The required product formula is
517 \begin{equation}\label{eq:arith-charged-product}
518  A_{c+d}(FG)=(A_cF)G+F(A_dG)
519        +2F'G'''+3F''G''+2F'''G'.
520 \end{equation}
521 All middle coefficients are integral.  Derivatives preserve
522 $\mathcal H_2$ and commute with $A_c$.  Induction on the number of
523 iterations in \eqref{eq:arith-charged-product} proves that multiplication
524 adds charges.  If $FG=1$, the same formula yields
525 \[
526  A_{-c}G=-G^2A_cF-G(2F'G'''+3F''G''+2F'''G').
527 \]
528 Induction, starting from the independently established integrality of
529 the reciprocal $G$, proves that inversion negates the charge.
530 Finally $A_{c+2}=A_c-1$, so increasing a charge by two preserves flatness.
531 These are
532 \lean{KomorebiPaperIX.ChargedDworkClosure.B_mul},
533 \lean{KomorebiPaperIX.ChargedDworkClosure.flat_inverse}, and
534 \lean{KomorebiPaperIX.ChargedDworkClosure.flat_charge_shift}.
535 
536 Packing $g_j$ into degrees divisible by four gives $K_{4,j}$.
537 Its source property is precisely charge-one flatness.  Inversion gives
538 charge $-1$, and the charge shift restores charge one for the
539 reciprocal $\mathcal P_{4,j}$.  If $\operatorname{dec}(F)(d)=d![t^d]F$, the exact
540 coefficient identity is
541 \[
542  \operatorname{dec}(A_1^sF)(d)
543        =2^{-s}\Delta_4^s\operatorname{dec}(F)(d).
544 \]
545 At $d=4n$, packing turns the right side into
546 $2^{-s}\Delta_1^sC_j(n)$.  This extraction requires no negative degree
547 and therefore holds at every $n$, including zero.  It proves the unit-step
548 bound \lean{KomorebiPaperIX.DyadicFourAllRows.base_step_bound}.
549 
550 To incorporate $v_2(u)$, expand a displacement using finite Newton
551 coefficients.  For any prime $p$, $u>0$, and $1\le a\le u$,
552 \[
553  p^{v_p(u)+1}\mid\binom ua p^a,
554 \]
555 as follows from $a\binom ua=u\binom{u-1}{a-1}$ and $v_p(a)<a$.
556 Repeated displacement, retaining the remaining base-difference order
557 at each induction step, gives a factor $p^{k(1+v_p(u))}$ from $k$
558 displacements.  This induction is formalized in
559 \lean{KomorebiPaperIX.StepAmplification.repeated_precision}.
560 Applying it with $p=2$ proves \eqref{eq:arith-allrow-c}. Multiplication
561 by $j!$ proves \eqref{eq:arith-allrow-u}.  Zero step and zero order follow
562 from their definitions.  The final statements are
563 \lean{KomorebiPaperIX.DyadicFourFinalStrengthening.normalized_step_bound}
564 and
565 \lean{KomorebiPaperIX.DyadicFourFinalStrengthening.unnormalized_step_bound}.
566 \end{proof}
567 
568 \begin{corollary}[Step-sensitive divisor-branch bound]\label{cor:arith-amplified}
569 Under the hypotheses of Theorem~\ref{thm:arith-divisor-base}, for all
570 $u,k,n\in\N$,
571 \[
572  \Delta_{u(p-1)/m}^{k}U_{mp,j}(n)
573        \in p^{\min(k(1+\nu_p(u)),mn)}\Z_p.
574 \]
575 For $C_{mp,j}$ the corresponding valuation lower bound is
576 $\min(k(1+\nu_p(u)),mn)-v_p(j!)$.
577 \end{corollary}
578 
579 \begin{proof}
580 Apply the same repeated-displacement theorem with the fixed cap $mn$ to
581 \eqref{eq:arith-divisor-bound}.  The argument preserves this cap and
582 improves the contribution from the order of the difference.
583 Division by the fixed factorial gives the rational valuation statement,
584 with the zero case included.
585 These are
586 \lean{KomorebiPaperIX.AllResidueStepAmplification.unnormalized_precision}
587 and
588 \lean{KomorebiPaperIX.AllResidueStepAmplification.normalized_precision}.
589 \end{proof}
590 
591 \begin{corollary}[Dyadic periods from row zero]\label{cor:arith-allrow-period}
592 For $0\le j<4$, $r\ge1$, and $n\ge0$,
593 \[
594  U_j(n+2^{r-1})\equiv U_j(n)\pmod{2^r}.
595 \]
596 For $j=2,3$ and $r\ge2$, $2^{r-2}$ is also a sufficient packet period.
597 The respective original degree displacements are $2^{r+1}$ and $2^r$.
598 \end{corollary}
599 
600 \begin{proof}
601 Use Lemma~\ref{lem:arith-newton-period} and the unit-step case of
602 Theorem~\ref{thm:arith-dyadic-differences}.  At $j=2,3$ the factorial
603 contributes an additional power of two.  The original degree versions are
604 \lean{KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_period_degree}
605 and
606 \lean{KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_half_period_degree}.
607 The next theorem sharpens these sufficient periods to a complete
608 classification.
609 \end{proof}
610 
611 \subsection{Exact displacement valuations and least packet periods}
612 
613 \begin{lemma}[Finite Newton dominance]\label{lem:arith-dominance}
614 Let $f:\N\to\Q$ and write $a_k=\Delta_1^kf(0)$.  Suppose that $c\in\N$,
615 $a_1\ne0$, $v_2(a_1)=c$, and
616 \[
617  v_2(a_k)\ge c+1+\lfloor\log_2k\rfloor\qquad(k\ge2).
618 \]
619 Then for every $n\ge0$ and $T>0$,
620 \[
621  f(n+T)-f(n)\ne0,\qquad
622  v_2\bigl(f(n+T)-f(n)\bigr)=v_2(T)+c.
623 \]
624 \end{lemma}
625 
626 \begin{proof}
627 Finite Newton reconstruction at an arbitrary row gives
628 \[
629  \Delta_1^kf(n)=\sum_{i=0}^{n}\binom ni a_{k+i}.
630 \]
631 The monotonicity of $\lfloor\log_2k\rfloor$ therefore preserves the
632 higher-coefficient bound after translation.  In addition,
633 $\Delta_1f(n)-a_1\in2^{c+1}\Z_2$, so the first difference is nonzero
634 of exact valuation $c$.
635 
636 Now expand the displacement:
637 \[
638  f(n+T)-f(n)=T\Delta_1f(n)
639           +\sum_{k=2}^{T}\binom Tk\Delta_1^kf(n).
640 \]
641 For $1\le k\le T$, the binomial denominator identity implies
642 \[
643  v_2\binom Tk\ge v_2(T)-v_2(k)
644             \ge v_2(T)-\lfloor\log_2k\rfloor.
645 \]
646 Every term of the remaining sum consequently has valuation at least
647 $v_2(T)+c+1$.  Its sum cannot cancel the leading term, which has exact
648 valuation $v_2(T)+c$.  This proves nonvanishing and the claimed valuation
649 using only finite sums.
650 The general theorem is
651 \lean{KomorebiPaperIX.NewtonDominance.exact_displacement}.
652 \end{proof}
653 
654 \begin{theorem}[Exact four-packet displacement law]\label{thm:arith-exact}
655 Set
656 \[
657  (c_0,c_1,c_2,c_3)=(1,1,4,2),\qquad
658  (d_0,d_1,d_2,d_3)=(1,1,5,3).
659 \]
660 For $0\le j<4$, $n\ge0$, and every positive integer $T$,
661 \begin{align*}
662  C_j(n+T)-C_j(n)&\ne0,&
663  v_2\bigl(C_j(n+T)-C_j(n)\bigr)&=v_2(T)+c_j,\\
664  U_j(n+T)-U_j(n)&\ne0,&
665  v_2\bigl(U_j(n+T)-U_j(n)\bigr)&=v_2(T)+d_j.
666 \end{align*}
667 \end{theorem}
668 
669 \begin{proof}
670 The first Newton coefficients, derived from
671 \eqref{eq:arith-triangular}, are
672 \[
673  a_{0,1}=-2,\quad a_{1,1}=-\frac65,\quad
674  a_{2,1}=-\frac{16}{15},\quad a_{3,1}=-\frac{36}{35}.
675 \]
676 Their exact valuations are $c_j$.  Theorem~\ref{thm:arith-dyadic-differences}
677 gives $v_2(a_{j,k})\ge k$ for all orders.  To obtain the stronger
678 logarithmic envelope required by Lemma~\ref{lem:arith-dominance}, only
679 a finite initial segment needs improvement.  The recurrence proves the
680 following exact valuations:
681 \begin{center}
682 \begin{tabular}{cll}\toprule
683 Address $j$ & Further orders $k$ & $v_2(a_{j,k})$ in that order\\\midrule
684 $0$ & $2$ & $3$\\
685 $1$ & $2$ & $3$\\
686 $2$ & $2,3,4,5,6$ & $6,9,13,16,22$\\
687 $3$ & $2,3,4$ & $8,8,15$\\\bottomrule
688 \end{tabular}
689 \end{center}
690 For all subsequent $k$, the elementary inequality
691 $c_j+1+\lfloor\log_2k\rfloor\le k$ completes the envelope.
692 The entries follow by exact rational computation from the defining
693 recurrence, and their valuations are proved in Lean.  Together with the
694 inequality for all subsequent orders, they establish the bound at every
695 order.
696 The uniform envelope is
697 \lean{KomorebiPaperIX.DyadicFourPrefix.tail_precision}.
698 
699 Apply Lemma~\ref{lem:arith-dominance} to $C_j$.  Multiplication by the
700 nonzero factorial $j!$ adds $v_2(j!)$ and preserves nonzeroness.
701 Hence $d_j=c_j+v_2(j!)$, giving the four valuation gains for the original
702 coefficients.
703 The declarations are
704 \lean{KomorebiPaperIX.DyadicFourLeastPeriods.normalized_exact_displacement}
705 and \lean{KomorebiPaperIX.DyadicFourLeastPeriods.exact_displacement}.
706 \end{proof}
707 
708 \begin{corollary}[All positive periods and their least element]
709 \label{cor:arith-least-period}
710 For $r\in\N$ and $0\le j<4$, a positive integer $T$ is a packet period
711 of $U_j$ modulo $2^r$ if and only if
712 \[
713  2^{\max(0,r-d_j)}\mid T.
714 \]
715 Here a packet period means $U_j(n+T)\equiv U_j(n)\pmod{2^r}$ for every
716 $n\ge0$.  Consequently the least positive packet periods are
717 \[
718  \begin{array}{c|cccc}
719  j&0&1&2&3\\\hline
720  \text{least period}&2^{\max(0,r-1)}&2^{\max(0,r-1)}&
721                  2^{\max(0,r-5)}&2^{\max(0,r-3)}.
722  \end{array}
723 \]
724 \end{corollary}
725 
726 \begin{proof}
727 By the exact displacement law, the congruence at any row is equivalent to
728 $v_2(T)+d_j\ge r$.  This is exactly the displayed integer
729 divisibility criterion.  Its least positive solution is the indicated
730 power of two, which also covers $r=0$ and $r\le d_j$.
731 The all-period and least-element statements are
732 \lean{KomorebiPaperIX.DyadicFourLeastPeriods.period_iff_dvd} and
733 \lean{KomorebiPaperIX.DyadicFourLeastPeriods.least_packet_period}.
734 \end{proof}
735 
736 For example, $U_2(n)\equiv2\pmod{32}$ and $U_3(n)\equiv6\pmod8$
737 for every row.  At precision $2^{10}$ the least packet periods are
738 $512,512,32,128$.  A packet displacement $T$ has original degree
739 displacement $4T$, as proved by
740 \lean{KomorebiPaperIX.DyadicFourLeastPeriods.original_degree_exact_displacement}.
741 Minimality here concerns packet shifts.  Shifts of the full degree-indexed
742 sequence, including its zero coefficients off the packet support, require
743 a separate analysis.  The new strengthening chapters determine all repeated-step higher differences in addresses zero and one and a power-of-two-order family in address two. The full exact classification of arbitrary higher-order differences
744 is also a separate question from the first-displacement law.
745 
746 \subsection{Classical odd-length coordinates and their congruence ladder}
747 
748 The classical signed Euler numbers have generating function
749 $\operatorname{sech}t=\sum_{n\ge0}E_{2n}t^{2n}/(2n)!$.
750 They are the $N=2$, $j=0$ member of
751 \eqref{eq:arith-euler-egf}.  The coordinate theorem reconstructs
752 them from finite alternating sums of odd powers.
753 
754 \begin{definition}[Odd-length source and inverse coefficients]
755 \label{def:arith-odd-source}
756 For a positive odd integer $p$, define
757 \[
758  S_d(p)=\sum_{a=0}^{p-1}(-1)^a(2a+1)^d.
759 \]
760 Let $\gamma_m$ be the integral Hurwitz coefficients of $\operatorname{sech}^2$:
761 \[
762  \operatorname{sech}^2t=\sum_{m\ge0}\gamma_m\frac{t^{2m}}{(2m)!},
763  \qquad
764  \gamma_m=\sum_{b=0}^{2m}\binom{2m}{b}E_bE_{2m-b},
765 \]
766 where $E_b=0$ for odd $b$.  Then $\gamma_0=1$.  Define
767 \[
768  T^{\mathrm{odd}}_{p,M}(n)=\sum_{m=0}^{\min(M,n)}
769        \binom{2n}{2m}\gamma_m p^{2m}S_{2(n-m)}(p).
770 \]
771 Here $p$ need only be odd. Primality is needed only to interpret the
772 result as a prime-adic congruence ladder.
773 \end{definition}
774 
775 The source and inverse coefficients are
776 \lean{KomorebiPaperIX.OddPower.source} and
777 \lean{KomorebiPaperIX.EulerCoefficients.inverseEven}. The truncation is
778 \lean{KomorebiPaperIX.OddEuler.truncation}.
779 
780 The same inverse coefficients can be written in the signed zigzag notation
781 of the original manuscript.  Define $Z_r$ by
782 \[
783  \sec t+\tan t=\sum_{r\ge0}Z_r\frac{t^r}{r!}.
784 \]
785 Then
786 \begin{equation}\label{eq:arith-signed-zigzag}
787  \gamma_m=(-1)^m Z_{2m+1}\qquad(m\in\N).
788 \end{equation}
789 Indeed, the odd coefficients come from $\tan t$, whose derivative is
790 $\sec^2t$.  Changing the sign of the squared variable in the even series
791 for $\operatorname{sech}^2t$ gives $\sec^2t$, so its degree-$2m$
792 Hurwitz coefficient is $(-1)^m\gamma_m$.  Differentiation identifies
793 this coefficient with $Z_{2m+1}$, proving the formula.  The Lean bridge is
794 \lean{KomorebiPaperIX.Zigzag.inverse_is_signed_zigzag}. It uses the
795 formal generating-function definition of the zigzag numbers.
796 
797 \begin{theorem}[Classical odd-length reconstruction]
798 \label{thm:arith-odd-reconstruction}
799 For every positive odd integer $p$ and every $n\in\N$,
800 \[
801  E_{2n}=\sum_{m=0}^{n}\binom{2n}{2m}\gamma_m p^{2m}S_{2(n-m)}(p).
802 \]
803 Equivalently, $E_{2n}=\sum_{q=0}^n V_{nq}S_{2q}(p)$ for the lower
804 triangular matrix
805 \[
806  V_{nq}=\binom{2n}{2q}\gamma_{n-q}p^{2(n-q)}\quad(q\le n),
807  \qquad V_{nq}=0\quad(q>n).
808 \]
809 It has $V_{nn}=1$ and $p^{2(n-q)}\mid V_{nq}$ when $q\le n$.
810 \end{theorem}
811 
812 \begin{proof}
813 The exponential generating series of the source is the finite sum
814 \[
815  \mathcal S_p(t)=\sum_{a=0}^{p-1}(-1)^a e^{(2a+1)t}.
816 \]
817 Multiplication by $\cosh t$ telescopes.  Since $p$ is odd,
818 \[
819  \mathcal S_p(t)=\frac{1+e^{2pt}}{2}\operatorname{sech}t.
820 \]
821 Taking its even part gives
822 \[
823  \sum_{n\ge0}S_{2n}(p)\frac{t^{2n}}{(2n)!}
824        =\cosh^2(pt)\operatorname{sech}t.
825 \]
826 Multiplication by the reciprocal $\operatorname{sech}^2(pt)$
827 yields $\operatorname{sech}t$.  The EGF product rule now gives the
828 reconstruction coefficient by coefficient.  Replacing $m$ by $n-q$
829 produces the displayed lower triangular row.  Its diagonal and weights
830 follow from $\gamma_0=1$ and the explicit factor $p^{2(n-q)}$.
831 The source-series identity is
832 \lean{KomorebiPaperIX.OddPower.odd_source_even_egf}. The reconstruction
833 and row statement are
834 \lean{KomorebiPaperIX.OddEuler.odd_euler_reconstruction} and
835 \lean{KomorebiPaperIX.OddEuler.row_action}.
836 \end{proof}
837 
838 \begin{corollary}[Odd-prime truncation ladder]\label{cor:arith-odd-ladder}
839 For every positive odd integer $p$ and all $M,n\in\N$,
840 \[
841  p^{2M+2}\mid E_{2n}-T^{\mathrm{odd}}_{p,M}(n)\quad\text{in }\Z.
842 \]
843 If $M\ge n$, the truncation equals $E_{2n}$ exactly.  In particular,
844 for an odd prime $p$ this is a congruence modulo $p^{2M+2}$ in $\Z_p$.
845 \end{corollary}
846 
847 \begin{proof}
848 Every omitted summand has $m\ge M+1$, hence contains the integer factor
849 $p^{2m}$ divisible by $p^{2M+2}$.  All its other factors are integral.
850 The finite sum of these omitted terms proves the assertion, with the
851 empty-tail case giving exact equality.  These are
852 \lean{KomorebiPaperIX.OddEuler.odd_euler_supercongruence} and
853 \lean{KomorebiPaperIX.OddEuler.full_depth_exact}.
854 \end{proof}
855 
856 The reconstruction and its truncation bound already hold over the integers.
857 For the dyadic construction we use a different source.  Its original bound
858 of $2^{2M+2}$ follows from integral reciprocal coefficients, and the next
859 subsection sharpens that bound to the optimal uniform exponent $4M+3$.
860 
861 \subsection{The optimal classical dyadic edge tower}
862 
863 Return now to the classical signed Euler numbers
864 \[
865  \operatorname{sech}t=\frac1{\cosh t}
866        =\sum_{n\ge0}E_{2n}\frac{t^{2n}}{(2n)!}.
867 \]
868 Thus $E_{2n}=E_{2n}^{(2,0)}$ in the convention
869 \eqref{eq:arith-euler-egf}.  In particular $E_0=1$, $E_2=-1$, and $E_4=5$.
870 The following construction concerns these $N=2$ coefficients, not $C_{4,0}$.
871 
872 \begin{definition}[Dyadic truncation]\label{def:arith-truncation}
873 Define $\beta_m$ by the formal unit-series identity
874 \[
875  \sum_{m\ge0}\beta_m z^{2m}=\left(\frac{z}{\sinh z}\right)^2,
876  \qquad \beta_0=1,
877 \]
878 where the quotient means the inverse of the unit series
879 $(\sinh z/z)^2$.  Define
880 \[
881  A(n)=\frac{3^{2n+2}-1}{4(2n+1)(2n+2)},\qquad
882  S_m(n)=\beta_m2^{2m}\frac{(2n)!}{(2n-2m)!}A(n-m)
883        \quad(0\le m\le n),
884 \]
885 and
886 \begin{equation}\label{eq:arith-tm}
887  T_M(n)=\sum_{m=0}^{\min(M,n)}S_m(n)\qquad(M,n\in\N).
888 \end{equation}
889 \end{definition}
890 
891 These definitions correspond to
892 \lean{KomorebiPaperIX.Dyadic.beta},
893 \lean{KomorebiPaperIX.Dyadic.sourceEven}, and
894 \lean{KomorebiPaperIX.DyadicReconstruction.truncation}.
895 The formal summand uses a falling factorial, and
896 \lean{KomorebiPaperIX.DyadicReconstruction.falling_factorial_fraction}
897 proves its equality with the quotient displayed above.
898 
899 \begin{lemma}[Exact reconstruction and source integrality]
900 \label{lem:arith-reconstruction}
901 For every $n\in\N$,
902 \[
903  E_{2n}=\sum_{m=0}^{n}S_m(n).
904 \]
905 Every $\beta_m$ is $2$-adically integral and every $A(n)$ is a nonzero
906 $2$-adic unit.  If $M\ge n$, then $T_M(n)=E_{2n}$.
907 \end{lemma}
908 
909 \begin{proof}
910 The ordinary kernel coefficients of $(\sinh z/z)^2$, in $z^2$, are
911 \[
912  \frac{2^{2m+1}}{(2m+2)!}.
913 \]
914 Legendre's strict factorial bound
915 $v_2((2m+2)!)<2m+2$ makes them integral.  Their constant coefficient is
916 one.  The coefficient recurrence for its reciprocal therefore
917 proves integrality of every $\beta_m$.
918 For the source factor, lifting the exponent at the even power $2n+2$
919 gives
920 \[
921  v_2(3^{2n+2}-1)=2+v_2(2n+2).
922 \]
923 Its denominator has the same valuation, since $2n+1$ is odd.  Thus
924 $A(n)$ is a nonzero unit.
925 
926 Its exponential generating function is
927 \[
928  \mathcal A(t)=\sum_{n\ge0}A(n)\frac{t^{2n}}{(2n)!}
929              =\frac{\cosh(3t)-\cosh t}{4t^2}.
930 \]
931 The quotients by powers of $t$ are well defined because the required
932 initial coefficients vanish.  The hyperbolic identity
933 \[
934  \mathcal A(t)\cosh t=\left(\frac{\sinh(2t)}{2t}\right)^2
935 \]
936 then gives the exact formal-series product
937 \[
938  \left(\sum_{m\ge0}\beta_m(2t)^{2m}\right)\mathcal A(t)
939        =\operatorname{sech}t.
940 \]
941 Taking the factorial-scaled coefficient of $t^{2n}$ produces the stated
942 finite sum.  Full depth leaves no omitted terms.
943 The relevant declarations are
944 \lean{KomorebiPaperIX.Dyadic.beta_integral},
945 \lean{KomorebiPaperIX.Dyadic.source_valuation},
946 \lean{KomorebiPaperIX.DyadicSeries.dyadic_reconstruction_series}, and
947 \lean{KomorebiPaperIX.DyadicReconstruction.dyadic_reconstruction}.
948 \end{proof}
949 
950 \begin{lemma}[Exact weighted inverse coefficient]\label{lem:arith-kappa}
951 Let $\kappa_m=\beta_m2^{2m}(2m)!$.  For every $m\ge1$,
952 \[
953  \kappa_m=-2^{4m}(2m-1)B_{2m}\ne0,\qquad
954  v_2(\kappa_m)=4m-1,
955 \]
956 where $B_{2m}$ is the usual even Bernoulli number.
957 \end{lemma}
958 
959 \begin{proof}
960 Let $Q(z)=z\coth z$, the regular formal series with constant coefficient
961 one.  The elementary differential identity
962 \[
963  \left(\frac z{\sinh z}\right)^2=Q(z)-zQ'(z)
964 \]
965 and the Bernoulli expansion
966 \[
967  Q(z)=1+\sum_{m\ge1}\frac{2^{2m}B_{2m}}{(2m)!}z^{2m}
968 \]
969 give
970 $\beta_m=-2^{2m}(2m-1)B_{2m}/(2m)!$.
971 Multiplication by $2^{2m}(2m)!$ proves the identity for $\kappa_m$.
972 The Bernoulli denominator theorem gives $v_2(B_{2m})=-1$ for $m>0$: its denominator contains each prime $q$ with $(q-1)\mid 2m$ exactly once, including $2$\cite{DLMF24}.
973 Since $2m-1$ is odd, the valuation is exactly $4m-1$.
974 This also proves nonvanishing.  In Lean, the hyperbolic identity is proved
975 after clearing removable zeros.  The library Bernoulli theorem then
976 determines the valuation of $\kappa_m$.
977 The declarations are
978 \lean{KomorebiPaperIX.DyadicSharpTower.kappa_bernoulli} and
979 \lean{KomorebiPaperIX.DyadicSharpTower.kappa_valuation}.
980 \end{proof}
981 
982 \begin{theorem}[Optimal uniform dyadic tower]\label{thm:arith-sharp-tower}
983 For all $M,n\in\N$,
984 \begin{equation}\label{eq:arith-sharp-tail}
985  E_{2n}-T_M(n)\in2^{4M+3}\Z_2.
986 \end{equation}
987 At the first omitted row $n=M+1$, the error is nonzero and
988 \[
989  v_2\bigl(E_{2M+2}-T_M(M+1)\bigr)=4M+3.
990 \]
991 Thus the exponent $4M+3$ cannot be increased uniformly in the Euler row.
992 \end{theorem}
993 
994 \begin{proof}
995 Rewrite the summand exactly as
996 \[
997  S_m(n)=\kappa_m\binom{2n}{2m}A(n-m).
998 \]
999 For $m>M$, its first factor is divisible by $2^{4m-1}$, the binomial
1000 coefficient is integral, and $A(n-m)$ is a unit.  Hence every omitted
1001 summand is divisible by $2^{4M+3}$.  Summing the finite tail proves
1002 \eqref{eq:arith-sharp-tail}.  If $M\ge n$, the tail is empty and the
1003 statement includes the resulting zero error.
1004 
1005 At $n=M+1$ there is exactly one omitted summand.  Here
1006 $\binom{2n}{2n}=1$ and $A(0)=1$, so the error is $\kappa_{M+1}$.
1007 Lemma~\ref{lem:arith-kappa} gives its exact valuation $4M+3$ and
1008 nonvanishing.  The statements are
1009 \lean{KomorebiPaperIX.DyadicSharpTower.dyadic_supercongruence_sharp},
1010 \lean{KomorebiPaperIX.DyadicSharpTower.first_omitted_error}, and
1011 \lean{KomorebiPaperIX.DyadicSharpTower.first_omitted_error_valuation}.
1012 \end{proof}
1013 
1014 \begin{proposition}[Row-dependent summand weights]\label{prop:arith-row-weight}
1015 For $1\le m\le n$, the summand is nonzero and
1016 \[
1017  v_2(S_m(n))=4m-1+v_2\binom{2n}{2m}.
1018 \]
1019 More generally, if $L\in\N$ satisfies
1020 \[
1021  L\le4m-1+v_2\binom{2n}{2m}\qquad\text{for every }M<m\le n,
1022 \]
1023 then $E_{2n}-T_M(n)\in2^L\Z_2$.
1024 \end{proposition}
1025 
1026 \begin{proof}
1027 Use the same factorization of $S_m(n)$, the nonzero binomial coefficient
1028 for $m\le n$, the exact valuation of $\kappa_m$, and the unit property
1029 of $A(n-m)$.  The tail conclusion follows by addition in $2^L\Z_2$.
1030 These are \lean{KomorebiPaperIX.DyadicSharpTower.summand_valuation} and
1031 \lean{KomorebiPaperIX.DyadicSharpTower.dyadic_supercongruence_row_weight}.
1032 \end{proof}
1033 
1034 The minimum summand weight bounds the tail valuation from below, but
1035 cancellation may raise that valuation. Appendix~\ref{app:root:scope} gives a later exact factorization and finite-polynomial reduction for each fixed depth. A universal explicit root and simplicity classification for that factor remains open.  Uniform optimality follows
1036 from the equality already established at $n=M+1$.
1037 
1038 \subsection{Isometric continuation of the four dyadic packets}
1039 
1040 The exact displacement law also determines the images of the packets
1041 after continuous extension to the dyadic integers.
1042 
1043 \begin{theorem}[Isometric packet bijections]\label{thm:arith-isometry}
1044 For $0\le j<4$, define on natural numbers
1045 \[
1046  f_j(n)=\frac{U_j(n)-j!}{2^{d_j}},\qquad (d_0,d_1,d_2,d_3)=(1,1,5,3).
1047 \]
1048 There is a unique continuous map $\Phi_j:\Z_2\to\Z_2$ whose value at
1049 every $n\in\N$ equals the embedded rational $f_j(n)$.
1050 It is an isometric bijection and $\Phi_j(0)=0$:
1051 \[
1052  |\Phi_j(x)-\Phi_j(y)|_2=|x-y|_2\qquad(x,y\in\Z_2).
1053 \]
1054 In particular, every element of $\Z_2$ has exactly one preimage.
1055 \end{theorem}
1056 
1057 \begin{proof}
1058 For $n>0$, the displacement law at row zero gives
1059 $v_2(U_j(n)-j!)=v_2(n)+d_j$, so $f_j(n)\in\Z_2$.
1060 The value at zero is zero.  Applying the same law to the smaller of two
1061 unequal natural numbers shows
1062 \[
1063  |f_j(n)-f_j(m)|_2=|n-m|_2.
1064 \]
1065 The natural numbers are dense in $\Z_2$, and the target is complete.
1066 The map therefore extends continuously.  The distance identity extends
1067 on the dense product of natural-number points, making the extension
1068 an isometry.  Density also proves uniqueness among all continuous maps
1069 with these prescribed values.
1070 
1071 To prove surjectivity, use compactness.  For an isometry $g$ of a compact
1072 metric space into itself, the sequence of iterates $g^n(x)$ has a
1073 convergent subsequence.  Two sufficiently close iterates, with exponents
1074 $a<b$, yield $d(x,g^{b-a}(x))$ equally small after removing $a$ isometric
1075 iterations.  Since $b-a>0$, the latter point is in the image of $g$.
1076 Thus the image is dense.  It is also compact and hence closed, so it is
1077 the whole space.  Apply this to $\Phi_j$ on $\Z_2$.
1078 
1079 The general ingredients are
1080 \lean{KomorebiPaperIX.DensePadicIsometry.existsUnique_extensionEquiv} and
1081 \lean{KomorebiPaperIX.CompactSelfIsometry.surjective}.
1082 The packet specialization is
1083 \lean{KomorebiPaperIX.DyadicFourIsometry.existsUnique_isometry}.
1084 Uniqueness among continuous maps is
1085 \lean{KomorebiPaperIX.DyadicFourIsometry.unique_continuous}.
1086 \end{proof}
1087 
1088 \begin{corollary}[Exact image of the original coefficients]
1089 \label{cor:arith-affine-image}
1090 The continuous extension of the original sequence is
1091 \[
1092  \widetilde U_j(x)=j!+2^{d_j}\Phi_j(x).
1093 \]
1094 It is injective, its image is exactly $j!+2^{d_j}\Z_2$, and
1095 \[
1096  |\widetilde U_j(x)-\widetilde U_j(y)|_2
1097      =2^{-d_j}|x-y|_2.
1098 \]
1099 Every point of that affine image has exactly one preimage in $\Z_2$.
1100 \end{corollary}
1101 
1102 \begin{proof}
1103 The formula agrees with $U_j$ on every natural number.  Continuity and
1104 the distance equality follow from the corresponding properties of
1105 $\Phi_j$.  Its surjectivity gives precisely the displayed affine image,
1106 and multiplication by the nonzero scalar $2^{d_j}$ preserves injectivity.
1107 The declarations are
1108 \lean{KomorebiPaperIX.DyadicFourIsometry.originalExtension_nat},
1109 \lean{KomorebiPaperIX.DyadicFourIsometry.originalExtension_dist}, and
1110 \lean{KomorebiPaperIX.DyadicFourIsometry.originalExtension_range}.
1111 \end{proof}
1112 
1113 The four rational packet sequences thus extend to bijections onto their
1114 exact dyadic images.  The proof uses density, completeness, and the
1115 displacement law. The strengthening chapters supply the further factorial and Taylor-coefficient argument for analyticity, including exact radii in addresses zero, one and two.  The analytic polynomial solution maps constructed
1116 later rest on separate hypotheses and a separate proof.

Back to source controls

Back to Realization Calculus