9 The final congruence in the original Euler convention
On this page · Visual guide: Reading the conclusion at the right strength · Permalink · Source line 1326
The preceding bounds can be stated as one uniform congruence without suppressing the address normalization. This is the strengthened formula for the four-address family, valid from the first row.
Corollary 9.1: Final common-step congruence
Let \(j\in\{0,1,2,3\}\), \(n\geq0\), and \(k,H\geq1\). Define
Then
For \(j=0,1\), this displayed exponent is the exact valuation for every \(n,k,H\) in the stated range. For \(j=2\), the exact positive power-of-two-order valuations are given by Theorem 6.3, with one added bit.
Read proof · Visual guide: The final rank-four congruence · Read statement and proof side by side · Permalink · Source line 1333 · Claim record · Lean coverage · Code · Worked examples
Proof of Corollary 9.1
The left side is \(j!\Delta_H^kC_j(n)\). At addresses zero and one, \(v_2(j!)=0\) and the exact homogeneous formula gives the exponent. At address two, \(v_2(2!)=1\); the maximum of (5.1) and (5.2) yields \(\max(k+4,2k+\lfloor k/2\rfloor+1)\) after removing the common \(v_2(k!)+k v_2(H)\). At address three, the one-bit normalized offset and \(v_2(3!)=1\) give \(k+2\).
Back to statement · Read statement and proof side by side · Permalink · Source line 1354 · Claim record · Lean coverage · Code · Worked examples
For mixed steps the same corollary holds with \(k v_2(H)\) replaced by \(\sum_\nu v_2(H_\nu)\) and the binomial stencil replaced by \(j!\Delta_{H_1}\cdots\Delta_{H_k}C_j(n)\). At addresses zero and one, exactness is then governed by the parity classification in Theorem 6.1. At first order these bounds are exact in every address, with original valuation offsets \((1,1,5,3)\); the least periods are those in (7.5).
9.1 Proof coverage and remaining questions
On this page · Permalink · Source line 1374
The results in these sections are mathematical theorems with detailed proofs and preserved audit evidence. Their formal status must be read statement by statement. The recovered Paper IX release already contains Lean results for the rank-four threshold-free homogeneous bound, the sharp first-difference laws, the least periods, and the dyadic isometry and image conclusions. Those inherited results should not be described as missing merely because the earlier short completion supplement did not include their later modules.
The all-rank dyadic and general prime-power transfer proof presented here, the factorial improvements, the mixed leading-parity classification, the Bernoulli power-order sharpness, the all-rank lower-half exact laws, the complete rank-eight extension, and the exact Taylor-radius arguments have not received new Lean formalization in this strengthening. A mathematical audit and an exact computation are neither a Lean compilation nor external peer review. The separate Lean guide records the recovered formal declarations and any fresh release checks without extending their coverage to these new claims.
The completed external statement is Nishibuchi's Conjecture 3.9 in its prescribed parameter family and coefficient normalization. These stronger congruences enlarge its dyadic branch and remove its starting threshold there. They do not settle every Euler problem. In particular, the following questions remain separate:
a complete exact higher-difference law at all non-power-of-two orders in address two;
complete higher-difference valuations and the exact ordinary Taylor radius in address three;
a classification of the upper-half dyadic addresses having an exact first-difference metric law at arbitrary larger ranks;
the distinct universal simplicity or nonvanishing question for the later Euler-tail residuals, and the original native Paper IX conjectures beyond the completed external statement.
The exact counterexamples above rule out the naive universal upper-half isometry, and mixed cancellations rule out unconditional baseline sharpness for arbitrary stencils. No global historical-priority or novelty assertion is made for these strengthened statements.