Realization Calculus

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Included manuscript sections

• verification_summary.tex

Read the typeset paper

1 \clearpage\subsection{Nishibuchi conjecture completion}\label{app:sup11}
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*{1. The complete external statement}
4 For $N>0$ and $0\le j<N$, use the original unnormalized convention
5 \[
6  \sum_{d\ge0}\EE_d^{(N,j)}\frac{t^d}{d!}
7  =\left(\sum_{n\ge0}\frac{t^{Nn}}{(Nn+j)!}\right)^{-1}.
8 \]
9 The existing packet convention satisfies
10 $\EE_{Nn}^{(N,j)}=j!C_{N,j}(n)$. The formalization defines the degree-indexed coefficients through the actual factorial-scaled series coefficients, proves their packet identification, and checks the cleared generating identity with the original exponential section.
11 
12 \begin{theorem}
13 Let $p$ be prime, $m>0$, and assume $m\mid p-1$ or $m=2$. Put $N=mp$ and $q=\operatorname{lcm}(2,p-1)$. Every $\EE_{Nn}^{(N,j)}$ is $p$-adically integral. For every $r\ge1$,
14 \[
15 \boxed{\EE_{Nn+qp^r}^{(N,j)}\equiv\EE_{Nn}^{(N,j)}\pmod{p^r}
16        \qquad(0\le j<N,\ n\ge r).}
17 \]
18 In particular, the positive sufficient threshold $n_0=r$ works uniformly in all allowed parameters.
19 \end{theorem}
20 
21 This is the parameter range and displacement of Nishibuchi's Conjecture 3.9 in arXiv:2605.10677v2. The explicit threshold also establishes the suggested bound $n_0\le r$. The original paper already proves the $p=2,m=2,j=0$ period as a special case, with all starting rows. This extension does not claim that special case as a new discovery.
22 
23 \textbf{Principal declaration}\par
24 \code{KomorebiPaperIX.NishibuchiCompletion.conjecture_3_9}
25 
26 The theorem type includes only the stated arithmetic hypotheses. There is no assumed congruence, weighted estimate, or flatness certificate. Precision is the zero-safe predicate $x=0$ or $v_p(x)\ge r$. Its connection to genuine ideal divisibility in $\Z_p$ is used in the proof.
27 
28 \textbf{Claim boundary.} This establishes a sufficient threshold and a period, not the earliest starting index, the least period, or a pointwise optimal valuation formula. The correspondence with the externally written statement is a mathematical review of definitions and quantifiers, not an automated semantic-equivalence theorem. The two native conjectures in Paper IX remain unchanged and unproved.
29 
30 \par\medskip
31 \subsubsection*{2. The missing dyadic branch}
32 For odd primes, the extra option $m=2$ already divides $p-1$. Therefore the only allowed family outside the preceding all-residue theorem is $p=2,m=2$, with $N=4$.
33 
34 The new proof establishes a higher-difference estimate for every one of its four addresses:
35 \[
36 \boxed{v_2\!\left(\Delta_u^k C_{4,j}(n)\right)\ge\min(k,n)
37        \qquad(0\le j<4).}
38 \]
39 All natural $u,k,n$ are allowed, including zero step, zero order and zero differences. The same bound holds for $j!C_{4,j}(n)$. Both a genuine $\Z_2$ divisibility theorem and a valuation theorem for the original rational sequence are included.
40 
41 \subsection*{An explicit source instead of an assumed regularity condition}
42 Let $g_j(n)=\binom{4n+j}{4n}^{-1}$. Its four formulas are
43 \[
44 \begin{aligned}
45  g_0(n)&=1,\\
46  g_1(n)&=(4n+1)^{-1},\\
47  g_2(n)&=((4n+1)(2n+1))^{-1},\\
48  g_3(n)&=3((4n+1)(2n+1)(4n+3))^{-1}.
49 \end{aligned}
50 \]
51 Every denominator is odd. The code constructs the actual unit inverses in $\Z_2$ and proves these identities against the original binomial coefficients, including $n=0$.
52 
53 Define a Kummer sequence over a commutative ring by
54 \[
55 \PP_a(f)\quad\Longleftrightarrow\quad
56  a^k\mid\Delta_1^k f(n)\ \text{for all }k,n.
57 \]
58 The exact discrete product rule
59 \[
60 \Delta_1^s(fg)(n)=\sum_{i=0}^s\binom si
61      \Delta_1^i f(n)\,\Delta_1^{s-i}g(n+i)
62 \]
63 is proved by induction. It proves closure under products. Applied to $fg=1$, the same formula isolates
64 $\Delta_1^s g(n)f(n+s)$. Induction and multiplication by $g(n+s)$ prove closure under actual pointwise inverses.
65 
66 An affine sequence whose slope is divisible by $a$ satisfies $\PP_a$. Consequently the four displayed source sequences satisfy $\PP_2$. No numerical interpolation or finite set of samples is used in that deduction.
67 
68 \textbf{Source modules:} \code{KummerSequences}, \code{DyadicFourKernel}.
69 
70 \par\medskip
71 \subsubsection*{3. The dyadic differential operator and reciprocity}
72 The operator required here is
73 \[
74 \boxed{B_4=\frac{D^8-D^4}{2},\qquad D=\frac{d}{dt}.}
75 \]
76 It is not the preceding $p=2$ specialization $(D^4-D^2)/2$. It is also not an ordinary derivation. The new algebra module proves the actual product formula, including the middle derivative sums whose coefficients are $\binom 8i/2$ and $\binom 4i/2$.
77 
78 Write $\mathcal H_{\mathrm{int}}$ for the subring of $\Q_2[[t]]$ whose factorial-scaled coefficients belong to $\Z_2$. Flatness means $B_4^sF\in\mathcal H_{\mathrm{int}}$ for every $s$. The proof of multiplicative and reciprocal closure is induction on $s$, using the full product correction. It separately proves that the actual reciprocal has integral Hurwitz coefficients when $F(0)=1$.
79 
80 Pack $g_j$ into degrees divisible by four and form its actual EGF. The formal coefficient identity is
81 \[
82 G_j(t)=\sum_{n\ge0}g_j(n)\frac{t^{4n}}{(4n)!}
83        =j!\sum_{n\ge0}\frac{t^{4n}}{(4n+j)!}.
84 \]
85 Its inverse is therefore the original normalized packet EGF. The source Kummer property gives flatness of $G_j$. The proved reciprocal closure gives flatness of $G_j^{-1}$.
86 
87 For a packed coefficient sequence $e$, the exact extraction formula is
88 \[
89 \bigl(U^8-U^4\bigr)^k\operatorname{pack}_4(e)(4n-4k)
90  =\Delta_1^k e(n),\qquad k\le n.
91 \]
92 Here $U$ is the coefficient shift. The nonnegative extraction index is why the first estimate covers $k\le n$. The existing saturation lemma extends it to all $k$ with exponent $\min(k,n)$, and the step-multiple lemma extends step one to every natural $u$.
93 
94 \subsection*{Identity with the original rational coefficients}
95 The integral lift is constructed from the decoded coefficients of the actual reciprocal. The code proves
96 \[
97  \operatorname{coe}(e_j(n))=C_{4,j}(n)\quad\text{in }\Q_2,
98 \]
99 and proves that the coefficient map commutes with every difference stencil. Multiplying by $j!$ yields the unnormalized family. The valuation result is not divisibility in a field.
100 
101 \textbf{Source modules:} \code{CubicDworkAlgebra}, \code{CubicDworkClosure};\par
102 \code{DyadicFourDwork} and \code{DyadicFourCongruences}.
103 
104 \par\medskip
105 \subsubsection*{4. From differences to the exact external period}
106 Let $f$ take values in a commutative ring and suppose
107 \[
108  p^{\min(k,r)}\mid\Delta_h^k f(n)\qquad\text{for every }k.
109 \]
110 The proved finite Newton expansion is
111 \[
112  f(n+p^{r-1}h)-f(n)=
113  \sum_{k=1}^{p^{r-1}}\binom{p^{r-1}}k\Delta_h^k f(n).
114 \]
115 For $k\ge r$, the difference already supplies $p^r$. For $1\le k<r$, the code proves the integer divisibility
116 \[
117  p^r\mid\binom{p^{r-1}}k p^k.
118 \]
119 It follows from $k\binom{p^{r-1}}k=p^{r-1}\binom{p^{r-1}-1}{k-1}$ and $v_p(k)<k$. Thus every summand is divisible by $p^r$, including the endpoint $r=1$.
120 
121 \subsection*{Divisor branch}
122 For $m\mid p-1$, the preceding all-residue theorem provides the needed differences as soon as $r\le mn$. With $q=\operatorname{lcm}(2,p-1)$, the required packet step $q/m$ is proved to be an integer multiple of $(p-1)/m$. The degree conversion is checked exactly:
123 \[
124  mp\left(n+p^{r-1}\frac qm\right)=mpn+qp^r.
125 \]
126 This retains the stronger sufficient condition $r\le mn$ on the divisor branch. The uniform choice $n\ge r$ implies it for every positive $m$.
127 
128 \subsection*{Exceptional branch}
129 For $p=2,m=2$, $q=2$ and the packet displacement is $2^{r-1}$. The new dyadic bound supplies the hypothesis when $n\ge r$, and
130 \[
131  4\bigl(n+2^{r-1}\bigr)=4n+2^{r+1}.
132 \]
133 The $p=2,m=1$ branch is also checked using $q=2$, not an incorrectly substituted $q=p-1=1$.
134 
135 \subsection*{An exact arithmetic check, not an optimality claim}
136 The independent rational recurrence gives
137 $C_{4,1}(1)=-1/5$ and $C_{4,1}(2)=121/45$. Their difference is $26/9$, of $2$-adic valuation one. This agrees with the new bound at $n=k=u=1$. The source also contains universal instantiations of the degree-indexed theorem at all four dyadic addresses and at an odd singular address.
138 
139 \textbf{Source modules:} \code{PeriodFromDifferences}, \code{NishibuchiCompletion}, \code{ConjectureExamples}.
140 
141 \par\medskip
142 \subsubsection*{5. Verification, provenance and boundary}
143 The release has 79 active modules: 70 unchanged baseline modules and nine new modules. Its inventory contains 836 named theorem declarations, 162 explicit definitions and two abbreviations. The transitive audit includes all 1,000 of these declarations. The increase of 83 named theorems includes supporting lemmas and examples, not 83 independent discoveries.
144 
145 \input{parts/verification_summary.tex}
146 
147 \subsection*{Reproduction}
148 The portable runtime is the pinned Linux x86-64 Lean 4.34.0-rc2 kit. It is not duplicated inside this source archive. From the extracted release, run
149 \begin{verbatim}
150 bash Run-Portable.sh /path/to/Komorebi_Portable_Lean_4.34.0-rc2
151 \end{verbatim}
152 The launcher checks file hashes, runs 25 extension-infrastructure tests and the new exact-arithmetic regressions, then builds every module in a new output directory and audits every registered declaration. It also compiles an explicit statement contract and negative controls. The final check verifies the released snapshot again.
153 
154 The source-policy scan excludes proof placeholders and additional project axioms. Compiler errors, timeouts, missing imports and invalid negative-control preludes are not accepted as successful theorem verification. Failed development snapshots are retained separately from active proof sources.
155 
156 \subsection*{Limits of the completion claim}
157 The pinned Mathlib compiled cache is reused, not rebuilt from source. No independent third-party checker or peer review was run. The original numerical experiment suite and Papers I--VIII were not rerun. Prior verification evidence is retained as historical evidence and is not relabeled as fresh testing. The original Paper IX manuscript still requires cumulative supplements and amendments. This extension is not a rewritten primary manuscript.
158 
159 The external Conjecture 3.9 is distinct from Paper IX's native Conjectures 13.2 and 13.3. Those two remain unproved. The present result does not assert least periods, earliest thresholds, or an optimal exponent for every individual parameter tuple. It makes no historical-priority claim relative to other unpublished work.
160 
161 \subsection*{Reference}
162 Yuta Nishibuchi. \emph{$p$-adic Congruences of Generalized Euler Numbers and Relations to Even Zeta Values}. arXiv:2605.10677v2, revised 1 June 2026. Definition 2.1, Conjecture 3.9 and Proposition 3.10. The version identifier is fixed for the statement comparison.

Back to source controls

Back to Realization Calculus