E.11 Nishibuchi conjecture completion
On this page · Permalink · Source line 1
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.
1. The complete external statement
On this page · Permalink · Source line 3
For \(N>0\) and \(0\le j<N\), use the original unnormalized convention
The existing packet convention satisfies \({\mathcal E}_{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.
Theorem E.1
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 \({\mathcal E}_{Nn}^{(N,j)}\) is \(p\)-adically integral. For every \(r\ge1\),
In particular, the positive sufficient threshold \(n_0=r\) works uniformly in all allowed parameters.
Permalink · Source line 12 · Claim record · Lean coverage · Code · Worked examples
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.
Principal declaration KomorebiPaperIX.NishibuchiCompletion.conjecture_3_9
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 \({\mathbb Z}_p\) is used in the proof.
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.
2. The missing dyadic branch
On this page · Permalink · Source line 31
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\).
The new proof establishes a higher-difference estimate for every one of its four addresses:
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 \({\mathbb Z}_2\) divisibility theorem and a valuation theorem for the original rational sequence are included.
An explicit source instead of an assumed regularity condition
On this page · Permalink · Source line 41
Let \(g_j(n)=\binom{4n+j}{4n}^{-1}\). Its four formulas are
Every denominator is odd. The code constructs the actual unit inverses in \({\mathbb Z}_2\) and proves these identities against the original binomial coefficients, including \(n=0\).
Define a Kummer sequence over a commutative ring by
The exact discrete product rule
is proved by induction. It proves closure under products. Applied to \(fg=1\), the same formula isolates \(\Delta_1^s g(n)f(n+s)\); induction and multiplication by \(g(n+s)\) prove closure under actual pointwise inverses.
An affine sequence whose slope is divisible by \(a\) satisfies \({\mathcal P}_a\). Consequently the four displayed source sequences satisfy \({\mathcal P}_2\). No numerical interpolation or finite set of samples is used in that deduction.
Source modules: KummerSequences, DyadicFourKernel.
3. The dyadic differential operator and reciprocity
On this page · Permalink · Source line 71
The operator required here is
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\).
Write \(\mathcal H_{\mathrm{int}}\) for the subring of \({\mathbb Q}_2[[t]]\) whose factorial-scaled coefficients belong to \({\mathbb 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\).
Pack \(g_j\) into degrees divisible by four and form its actual EGF. The formal coefficient identity is
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}\).
For a packed coefficient sequence \(e\), the exact extraction formula is
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\).
Identity with the original rational coefficients
On this page · Permalink · Source line 94
The integral lift is constructed from the decoded coefficients of the actual reciprocal. The code proves
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.
Source modules: CubicDworkAlgebra, CubicDworkClosure; DyadicFourDwork and DyadicFourCongruences.
4. From differences to the exact external period
On this page · Permalink · Source line 105
Let \(f\) take values in a commutative ring and suppose
The proved finite Newton expansion is
For \(k\ge r\), the difference already supplies \(p^r\). For \(1\le k<r\), the code proves the integer divisibility
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\).
Divisor branch
On this page · Permalink · Source line 121
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:
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\).
Exceptional branch
On this page · Permalink · Source line 128
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
The \(p=2,m=1\) branch is also checked using \(q=2\), not an incorrectly substituted \(q=p-1=1\).
An exact arithmetic check, not an optimality claim
On this page · Permalink · Source line 135
The independent rational recurrence gives \(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.
Source modules: PeriodFromDifferences, NishibuchiCompletion, ConjectureExamples.
5. Verification, provenance, and boundary
On this page · Permalink · Source line 142
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.