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*{Principal results}
2 \addcontentsline{toc}{section}{Principal results}
3 The original external problem is Nishibuchi's Conjecture 3.9 for generalized Euler numbers. Its full parameter range is resolved. If $p$ is prime, $m$ is positive with $m\mid p-1$ or $m=2$, $0\le j<mp$, and $q=\operatorname{lcm}(2,p-1)$, then the original Euler coefficients are $p$-adically integral and
4 \[
5  E_{mpn+qp^r}^{(mp,j)}\equiv E_{mpn}^{(mp,j)}\pmod{p^r}
6  \qquad (r\ge1,\ n\ge r).
7 \]
8 The chapter states the generating function and the conversion between ordinary degree and packet row before using this formula. The normalized coefficient is $C_{N,j}(n)$ and the original coefficient is $E_{Nn}^{(N,j)}=j!C_{N,j}(n)$. The constant coefficient of the original series is $j!$.
9 
10 The strongest common-step conclusion in width four is compact. For $n\ge0$ and $k,H\ge1$,
11 \begin{equation*}
12  \sum_{i=0}^k(-1)^{k-i}\binom ki E_{4(n+iH)}^{(4,j)}
13  \equiv0\pmod{2^{\,v_2(k!)+kv_2(H)+A_j(k)}},
14 \end{equation*}
15 where
16 \[
17  A_0(k)=A_1(k)=k,\qquad
18  A_2(k)=\max\{k+4,\,2k+\lfloor k/2\rfloor+1\},\qquad
19  A_3(k)=k+2.
20 \]
21 There is no starting-row threshold. The exponent is exact in addresses zero and one for every order and positive step. It is exact in address two at every power-of-two order. The proof chapters also give mixed-step forms, the cancellation criterion in addresses zero and one, and exact first-displacement laws.
22 
23 \begin{center}
24 \small
25 \begin{tabularx}{\linewidth}{@{}>{\raggedright\arraybackslash}p{.29\linewidth}>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}p{.21\linewidth}@{}}
26 \toprule
27 Result & Scope & Evidence\\
28 \midrule
29 Nishibuchi Conjecture 3.9 & Every parameter in the original statement, with explicit $n\ge r$ & Inherited Lean proof\\
30 Width-four all-row common-step bound, first differences, least periods and isometry & Every address, row and positive displacement & Inherited Lean proof\\
31 General prime-power inverse transfer and mixed steps & Every prime-power width, with signed steps for odd primes & Written proof and audit\\
32 Factorial gains and exact higher-order families & Four width-four addresses, with stated sharpness scopes & Written proof and audit\\
33 Taylor radii and broader dyadic first differences & Exact radii in addresses $0,1,2$ and stated all-rank cases & Written proof and audit\\
34 Ordinary Euler tail simplicity & Partial families and an explicit remaining discriminant problem & Open in full generality\\
35 \bottomrule
36 \end{tabularx}
37 \end{center}
38 
39 The arithmetic development leads to polynomial lifting, deformation and analytic regularity. The appendices give the detailed continuation arguments and the recovered foundational treatment. Where an earlier formulation is retained for comparison, its hypotheses and proof status remain explicit. The formal companion supplies the exact source map and distinguishes source review from compiler execution. The visual studies supply finite examples and diagrams derived from the theorems.
40 
41 Recorded proof reviews are internal reviews. Formal proof coverage and the scope of each mathematical result are stated separately.
42 \clearpage

Back to source controls

Back to Realization Calculus