back to table · edit · history · where entries came from · files · download
5063 bytes, as of the version from 2026-11-01 08:20 (current). Recorded here, not run.
# Numerical methods and proofs for T645
The normalization is R(x)=x sum_{j>=0}(-x)^j/(j! zeta(2j+2)). The sources are
Cisło–Wolf, https://arxiv.org/html/0807.2971, equations (2), (10), (13), and
Paris, https://arxiv.org/html/2107.02800, §1. The source convention is
R(x)=-x S_{2,2}(x). No hypothesis on zeta zeros is needed for these computations.
## Primary enclosure
For x>=0 the absolute j-th term is at most x*x^j/j!, because
0<1/zeta(2j+2)<1. Beyond j=M, the ratios of consecutive majorant terms are
at most x/(M+1). If M+1>x, their sum is therefore bounded by
E_M = x^(M+1)/(M! (1-x/(M+1))).
The generator computes M and E_M with exact rationals, stops when
E_M<10^(-digits-35), and adds the zero-centered ball of radius E_M to the
Arb finite sum. Working precision is bits(digits)+2*ceil(x)+80; the variable
guard accounts for cancellation of exponentially large intermediate terms.
The returned accuracy is checked explicitly. R(0) is exactly zero from its
factor x, not from observed decimal zeros.
For the default selection, 415–613 working bits give at least 406 relative
accuracy bits. M ranges through at most 505. The entire ball, not its midpoint,
is contained inside the decimal's exact rational last-place interval.
## Independent enclosure
The identity 1/zeta(s)=sum mu(n)/n^s, absolutely convergent for s>1, gives
R(x)/x = sum_{n>=1} mu(n)/n^2 exp(-x/n^2).
Evaluate the terms n<=N directly. For n>N, expand exp(-t) only through
k=K-1. This gives
R(x)/x = sum_{n<=N} mu(n)/n^2 exp(-x/n^2)
+ sum_{k=0}^{K-1} (-x)^k/k! A_k + error/x,
A_k = 1/zeta(2k+2) - sum_{n<=N} mu(n)/n^(2k+2).
Taylor's integral remainder on t>=0 is bounded in absolute value by t^K/K!,
since all derivatives of exp(-t) have absolute value <=1 there. Hence
|error| <= x^(K+1)/K! sum_{n>N} n^(-2K-2)
<= x^(K+1)/(K! (2K+1) N^(2K+1)).
The code uses N=16, K=100 and 900-bit ball arithmetic. It evaluates the tail
polynomial by Horner's rule and adds this bound. Its largest tail bound is
about 5.0e-201 at x=100. Every nonzero independent result retains at least
662 relative accuracy bits.
All even zeta inputs in this method are recomputed from
1/zeta(2m) = 2(2m)! / ((2*pi)^(2m) |B_(2m)|),
using DLMF 25.6.2, https://dlmf.nist.gov/25.6. Bernoulli numbers through B_200
are built from B_0=1 and
B_n = -sum_{j=0}^{n-1} binomial(n+1,j) B_j / (n+1)
in exact rational arithmetic. Pi is enclosed independently by
16 atan(1/5)-4 atan(1/239), summing alternating rational arctangent series with
the next-term remainder. The tangent addition formula verifies Machin's
identity; 0<4 atan(1/5)-atan(1/239)<pi/2 selects pi/4. Thus neither Arb zeta
nor the primary series evaluator is used in the independent value calculation.
## Relationships and controls
The EGF check computes 553 coefficients c_k by successive differences of
reciprocal even zeta balls at 1600 bits. From the absolutely convergent Möbius
representation of c_k, |c_k|<=zeta(2)<2. The geometric majorant for the omitted
exponential series, multiplied by 2*x*exp(-x), therefore certifies its tail.
Every EGF enclosure is contained in the proposed or stored interval for R(x).
The exact origin, the limit R(x)/x at the origin, the first three closed forms
for c_k, and the full finite comparison bound in Cisło–Wolf (33) are checked.
The stored T644 coefficient intervals through k=100 are treated as intervals,
not exact input values. No claim about the RH asymptotic criterion is inferred
from finite numerical checks.
Before comparisons, the checker validates the known nonzero rational 1/2,
initial Bernoulli numbers and Möbius values, 1/zeta(2)=6/pi^2, and R(0)=0.
It rejects a wrong rational and a shifted reciprocal-zeta control. Every ball
must be finite and narrow. For each of the 100 decimal rows, moving the
independent value by ten last-place units fails containment. Independent and
primary results also agree when rounded to all 100 stored significant digits.
The displayed Sage program is separately executed over all 101 arguments.
## Evidence and reproducibility
Run `sage -python checks.py` with generate.py, check.py, T644.json and
skill-manifest.json beside it. `sage -python checks.py --stored` performs the
same checks on values read back from T645. A private draft needs a NumberDB
API key. `sage -python generate.py` runs Generator.verify(sample=None).
The runner uses agents/sage.sh for every Sage process; the attached scripts
also work as ordinary Sage programs without the campaign wrapper.
checks-evidence.json records the private checks; stored-checks-evidence.json
records the post-write checks. dry-run.log and snippet-check.log record the
standard dry run and displayed-program execution. The coordinated instructions
are in agents/runs/20261101T075931Z-build-skills/manifest.json, attached as
skill-manifest.json. Both archived skill SHA-256 hashes are
`a2b28d9953264d7b0ca62663785c2952190c5be6d6d3597fd695d9a54d606278`.
The build artifacts are evidence for an independent critique, not its verdict.