A Exact classical Euler tails and the remaining simplicity problem
On this page · Permalink · Source line 1
This appendix records the related classical Euler tail program at its stationary-separation checkpoint of 5 October 2026. Its purpose is to state the strongest proved reduction and its exact remaining obligation. The universal simplicity problem below is a separate question from Nishibuchi's Conjecture 3.9, which the congruence results of this paper resolve. It is also separate from the presentation and gluing questions called Native 13.2 and Native 13.3 in the original Paper IX.
The tail results have mathematical proofs, supplemented in the indicated families by complete coefficient certificates and proved bounds for every omitted coefficient. Bounded sampled values support implementation checks; they do not supply the universal quantifiers. The latest continuation did not run Lean. Its mathematical claims must therefore be read with the formal-coverage distinctions in the Lean guide.
A.1 The ordinary Euler packet identity
On this page · Permalink · Source line 19
To distinguish ordinary signed Euler numbers from the generalized numbers of the main text, write
Throughout this appendix, \(v_2(2)=1\) and \(v_2(0)=\infty\). Let \(s_2(n)\) be the number of ones in the binary expansion of the nonnegative integer \(n\). Define
The initial values are \(\beta_0=\kappa_0=1\). For \(m\ge1\), differentiation of \(z\coth z\) gives
The classical dyadic Bernoulli denominator law \(v_2(B_{2m})=-1\) and Legendre's formula yield
The source identity
implies, after multiplication by \(4t^2/\sinh^2(2t)\),
For a retained depth \(M\ge0\), put
An empty tail, \(N\le M\), is exactly zero.
Proposition A.1: Sharp uniform classical truncation bound
For every \(M,N\ge0\),
For each fixed \(M\), equality holds at \(N=M+1\).
Read proof · Read statement and proof side by side · Permalink · Source line 68 · Claim record · Lean coverage · Code · Worked examples
Proof of Proposition A.1
The source \(A(n)\) is a dyadic unit for every nonnegative integer \(n\). Each nonempty summand has \(m\ge M+1\), so (A.2) and integrality of the binomial coefficient give the asserted bound. At \(N=M+1\), only the first omitted summand remains; its binomial coefficient and \(A(0)\) both equal one.
Back to statement · Read statement and proof side by side · Permalink · Source line 75 · Claim record · Lean coverage · Code · Worked examples
Thus later row-dependent cancellation can improve a particular tail, but cannot increase the uniform exponent required to hold at every row.
A.2 A finite carry minimum and an exact all-row factorization
On this page · Permalink · Source line 86
Let \(\mathbb Z_2\langle x\rangle\) denote the restricted power series: their integral coefficients tend to zero dyadically. Extend \(A\) by
The apparent singularity at \(x=-1\) is removable. Since \(v_2(\log9)=3\), its convergent expansion is
It follows coefficientwise that \(\mathscr A\in\mathbb Z_2\langle x\rangle^\times\), \(\mathscr A\equiv1\pmod2\), and \(\mathscr A(N)=A(N)\).
Set \(r=M+1\ge1\) and define
The coefficient valuations tend to infinity. At any nonnegative integer \(x\), terms with \(q>x\) vanish. Cancelling the factorials in (A.3) therefore gives the exact identity
This is a finite rational identity at every original Euler row.
The scalar packet weights have exact valuations
Put
Since \(\lambda_r(0)=0\) and \(\lambda_r(q)\ge3q+1-s_2(r)\), every minimizing address satisfies
In particular \(\mu_r\le0\), and the minimum is found by a finite carry calculation. Reduction of the whole series gives
Its highest degree is \(\max J_r\), with leading coefficient one. Thus the normalization is the actual Gauss normalization.
Theorem A.2: Exact classical tail valuation
For every \(r\ge1\) and \(N\ge r\),
There are unique factors
where \(W_r\in\mathbb Z_2[X]\) is monic of degree \(d_r=\max J_r\) and \(U_r\in\mathbb Z_2\langle X\rangle^\times\) satisfies \(U_r\equiv1\pmod2\). Consequently \(v_2G_r(x)=v_2W_r(x)\) for every \(x\in\mathbb Z_2\), and
Read proof · Read statement and proof side by side · Permalink · Source line 148 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem A.2
Equation (A.5), the exact weight in (A.2), and the digit-sum identity \(v_2\binom{2N}{2r}=v_2\binom Nr\) prove (A.8). The binomial coefficients themselves need not be equal.
For preparation, start from the monic polynomial \(g=\overline G_r\) and its zero-one lift \(W_1\), with \(U_1=1\). Suppose \(G_r-W_kU_k\) is coefficientwise divisible by \(2^k\). Its divided reduction is a finite polynomial because \(G_r\) is restricted. Divide it by \(g\) in \(\mathbb F_2[X]\):
With zero-one coefficient lifts, set \(W_{k+1}=W_k+2^ks\) and \(U_{k+1}=U_k+2^kq\). The error is now divisible by \(2^{k+1}\), the polynomial remains monic of degree \(d_r\), and the unit reduces to one. The sequences converge in the Gauss norm. Uniqueness of quotient and remainder at successive binary digits proves uniqueness of the factors. For \(d_r=0\), take \(W_r=1\). The degree bound follows from (A.6).
Back to statement · Read statement and proof side by side · Permalink · Source line 167 · Claim record · Lean coverage · Code · Worked examples
This theorem reduces every depth to a finite polynomial without discarding the infinite analytic tail. It does not explicitly classify every \(W_r\), decide every repeated root from a fixed precision, or prove that all its dyadic roots are simple.
A.3 Regular walls: exact root emergence
On this page · Permalink · Source line 196
For a wall label \(j\ge1\) and \(0\le q<j\), define
Here \(E_j\) is a carry minimum, not an Euler number. A wall label is regular when \(e_j(q)>0\) for \(1\le q<j\). For \(r=2^L-j\) with \(L>L_j\), put \(\delta=L-L_j\). The carry identities give
where \(U\equiv1\pmod2\). For a regular label, also \(E_j=0\) and \(V\equiv1\pmod2\).
For \(0\le i<j\), let
At \(j=1\) use \(d_0=k_0=t_0=0\). The balls \(B_i\) partition \(\mathbb Z_2\). Indeed a residue represented twice among \(0,\ldots,j-1\) splits into its two children; every other represented residue remains one ball. On each such ball,
Theorem A.3: Regular-wall root law
For every regular label \(j\) and every integer \(\delta\ge1\),
In the second case there is exactly one root \(\alpha_i\) in \(B_i\), it is simple, and \(v_2(\alpha_i-i)=\delta-d_i\). Thus the number of dyadic roots is exactly
Read proof · Read statement and proof side by side · Permalink · Source line 236 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem A.3
If \(\delta<t_i\), the unit perturbation has smaller valuation than the skeleton term throughout \(B_i\), so the valuation is exactly \(\delta\). Otherwise, after the ball substitution and division by \(2^{t_i}\), the coefficientwise reduction is \(y+c\) for a constant \(c\in\mathbb F_2\). A restricted integral series with this reduction is a dyadic isometry: division of its difference by \(y-z\) gives an odd linear coefficient plus even higher contributions. Binary lifting therefore gives its unique root and exact distance law. Evaluating at \(x=i\) gives the stated displacement, since \(G_r(i)=2^\delta V(i)\) has exact valuation \(\delta\). The partition proves exhaustion of the roots.
Back to statement · Read statement and proof side by side · Permalink · Source line 253 · Claim record · Lean coverage · Code · Worked examples
The largest emergence threshold is
For \(j=2^a\), all thresholds equal \(j-1\). There are no roots before that distance and exactly \(j\) simple roots at and after it, within the positive-distance range. The equality and pre-wall cases are also resolved: regular labels \(j\ge2\) have no roots there; \(j=1\) has one simple odd root at equality.
For example, \(j=5\) has \((t_0,\ldots,t_4)=(6,3,4,3,6)\). The exact root counts at distances \(1,2,3,4,5,\ge6\) are \(0,0,2,3,3,5\). The older sufficient stages \(3,5,7\) are not the sharp emergence stages, which are \(3,4,6\). The first irregular label, \(j=17\), has \(V\equiv1+X\pmod2\); the regular-wall theorem does not apply. Complete coefficient certificates close distances \(1\) through \(19\), and the general separation theorem gives all seventeen simple roots for \(\delta\ge20\). Those two kinds of evidence together resolve that family.
A.4 What the later simplicity reductions prove
On this page · Permalink · Source line 287
For a general depth \(r\), call \(j_r=\max J_r\) its true terminal. This definition depends on the actual carry minimum; rewriting the same integer as another wall expression does not change \(j_r\). The universal simplicity target is
The following are completed restricted results of the later continuations. Their family statements include a proof that the indicated label is the true terminal throughout the displayed ranges.
| Depth \(r\) | Odd multiplier range | Outer scales |
|---|---|---|
| \(B2^L-129\) | \(0<B<2^{89}\) | \(L\ge392\) |
| \(B2^L-161\) | \(0<B<2^{932}\) | \(L\ge487\) |
All dyadic roots are simple in both infinite integer families. For arbitrary larger admissible multipliers, a multiple root with true terminal \(129\) can occur only at \(L=515\) and in two necessary multiplier classes modulo \(2^{90}\). With true terminal \(161\), it can occur only at \(L=640\) and in one necessary multiplier class modulo \(2^{935}\). These classes are necessary conditions. The records do not assert existence of a singular ordinary Euler index in them.
For terminal \(161\), the neighboring phases are resolved uniformly: \(L=639\) has exactly one simple root and \(L=641\) exactly three simple roots, for every positive odd multiplier with that true terminal. The middle phase is reduced, before the deeper certificate is applied, to
The \(935\)-bit multiplier condition composes this whole-phase reduction with an inherited \(917\)-bit local parameter certificate. It is neither a new \(935\)-bit reconstruction nor an all-precision interpolation of the undepleted Euler family.
The structural argument also extends beyond lower address one. For a certified true-terminal wall, let \(a\) be its last lower minimizing address, \(k=j_r-a\) the regular complement, and \(t=v_2(k)\). Under the regular lower-address hypotheses of the source theorem, all roots above emerged complement balls are simple. Every root is simple at every wall distance in the band
Equality walls are simple even outside that band. This includes certified terminal-\(258\) walls with \(a=2\), \(k=256\), and \(L\ge777\). For \(a=3\), \(k=4096\), only \(L=16385\) remains a possible critical scale. Outside the band, the theorem gives necessary local valuation conditions; it does not exclude the remaining unit cancellation. Irregular lower addresses need their own prefix analysis.
A.5 The actual stationary discriminant
On this page · Permalink · Source line 351
The current focused obstruction is the admitted ordinary-index family
On its surviving chart define the actual, undepleted function
The complete coefficient theorem gives
Its half derivative is a dyadic isometry. It therefore has a unique critical point \(c_r\in\mathbb Z_2\). Set \(\Phi_r^{\mathrm{act}}=K_r(c_r)\). The earlier independent-undepletion notation for this same scalar is \(\Phi_r(2^{2r-25})\). Excluding a multiple root on the surviving chart is exactly the assertion \(\Phi_r^{\mathrm{act}}\ne0\).
Proposition A.4: Exact quadratic compression
There is a unique preparation
With \(\delta_r=\beta_r^2-\alpha_r\) and \(\tau_r=\mathcal U_r'(c_r)/\mathcal U_r(c_r)\),
The equality includes the zero case.
Read proof · Read statement and proof side by side · Permalink · Source line 380 · Claim record · Lean coverage · Code · Worked examples
Proof of Proposition A.4
The same successive monic polynomial division used in Theorem A.2, started at precision eight, preserves the quadratic and unit reductions of (A.11). Write \(W=Z^2+2\beta_rZ+\alpha_r\) and \(w=W(c_r)\). Stationarity gives \(W'(c_r)=-\tau_rw\), while \(w=\Phi_r^{\mathrm{act}}/\mathcal U_r(c_r)\). The quadratic identity \(\beta_r^2-\alpha_r=W'(c_r)^2/4-W(c_r)\) proves the formula. Since \(\tau_r\in256\mathbb Z_2\), its bracket is a unit.
Back to statement · Read statement and proof side by side · Permalink · Source line 397 · Claim record · Lean coverage · Code · Worked examples
This compression retains the unit-cofactor derivative. It does not assert that \(c_r\), \(\alpha_r\), or \(\beta_r\) is rational or algebraic over \(\mathbb Q\). The remaining arithmetic obligation is therefore
Even this assertion would still leave the terminal-\(129\) and higher-address obligations in the universal target (A.9).
A.6 Approximation reaches every depth; separation remains open
On this page · Permalink · Source line 421
The latest continuation retains the exact Bernoulli undepletion factor
It is a dyadic unit, including \(e_{r,0}=1\). Multiplication by this factor preserves the all-\(q\) error of the shifted Jacobi moment model. Consequently the actual model critical values satisfy, for every \(m\ge25\),
The estimate includes every packet and controls motion of the critical point. There is no ceiling at the undepletion exponent \(2r-25\). For each fixed admitted \(r\) it implies the exact equivalence
Indeed a passing strict test has the same valuation as the limit; conversely any finite limit valuation is eventually smaller than \(L_m\). The existence of a passing depth for every ordinary index is unproved. Nonzero models at every depth are compatible with an exactly zero limit.
The degree-two preparation also reduces the old representative-height cost to a linear cost, about \(2P\) bits at precision \(P\). This remains larger than the \(P\) bits needed for a strict nonzero residue certificate. The fixed rational control \((Z-1/3)^2\) has zero critical value while its least-residue integer discriminant representatives are nonzero at every even \(P\ge6\). Thus a nonzero integer representative alone cannot prove a nonzero dyadic discriminant.
One sufficient new arithmetic input would be an odd-denominator projective quadratic
at a proved precision for every admitted ordinary \(r\). Then \((B^2-AC)/A^2\equiv\delta_r\pmod{2^P}\) cannot vanish modulo \(2^P\). No depth-independent theorem supplying this inequality has been established. The tested recurrence and exterior-contact identities retain balancing terms and do not force a contradiction. Finite exponential models approximate the actual target at every depth, but their order grows with precision, their clearing polynomial has zeros on the actual chart, and their proved construction-specific height cost does not give the required discriminant bound.
A.7 Status and source map
On this page · Permalink · Source line 476
| Claim | Status at this edition |
|---|---|
| Nishibuchi Conjecture 3.9 in its stated parameter range | Resolved in the main paper |
| Sharp uniform ordinary Euler tail exponent \(4M+3\) | Proved, with earlier formal coverage |
| Exact tail factorization and finite polynomial at every depth | Proved; later prose development |
| Regular-wall emergence and indicated integer simplicity families | Proved within their stated hypotheses |
| Actual quadratic compression and unbounded stationary approximation | Proved; no fresh Lean build |
| Nonzero actual stationary discriminant for every admitted index | Open |
| Universal simplicity of every \(G_r\) | Open |
| Native 13.2 presentation invariance and Native 13.3 global/completed gluing | Separate open general programs |
The tail factorization, regular-wall proofs, finite preparation, and coefficient cutoffs are recorded in the preserved sources/euler_v4.md of the regular-address checkpoint. The two integer families and multiplier conditions are proved in its next/terminal129/PROOF.md and next/critical_phases/PROOF.md; local_parameter/RECENTER_PROOF.md supplies the inherited local precision certificate. The higher-address extension is in next/higher_address/regular_address_transversality.md. The stationary checkpoint records the exact discriminant identity in stationary_separation/ordinary/QUADRATIC_COMPRESSION_AND_HEIGHT.md and actual convergence in stationary_separation/root/ACTUAL_LIMIT_AND_SEPARATION.md. Its synthesis and proof reviews retain the failed implications and the precise remaining arithmetic input.
The source archive's evidence/root_scope_inventory.md gives the full checkpoint paths and content hashes used for this appendix. The 2026-10-05 complete-work archive preserves the original layouts and historical releases. Its stored hashes and verification receipts are evidence of integrity and recorded execution; they are not substitutes for a proof of the open assertions above.