back to table · edit · history · where entries came from · files · download
2703 bytes, as of the version from 2026-10-28 15:11 (current). Recorded here, not run.
# Certification of the Gram-point indexing and enclosures
Write a=1/4 and z=a+it/2. The derivative of the continuous phase is
theta'(t) = (Re psi(z) - log(pi))/2.
By the convergent digamma series (DLMF 5.7.6),
Re psi(a+it/2) = -EulerGamma + sum_{k>=0}
[1/(k+1) - (k+a)/((k+a)^2+t^2/4)].
Differentiation on compact real intervals is justified by uniform convergence
of the differentiated series. Each summand contributes positively to the
derivative when t>0, so theta'(t) is strictly increasing for t>0. The generator
checks theta'(7)>0 and theta(7)<-pi with ball arithmetic. Stirling's expansion
(DLMF 5.11.1) gives theta(t) ~ (t/2)log(t/(2*pi))-t/2, hence theta(t) tends to
positive infinity. Therefore theta crosses each n*pi, n>=-1, exactly once
on [7,infinity). This establishes indexing without a root-count assumption
about the zeta function or Gram's law.
The computation uses Newton iterates only to locate a candidate. Taking a
midpoint during Newton iteration discards its enclosure status: no Newton
iterate is claimed to contain the root. A separate step takes the exact dyadic
candidate center c and exact rational radius r=10^(-digits-10). Ball evaluations
at the exact rational endpoints c-r and c+r must certify opposite strict signs
of theta(t)-n*pi. Continuity proves existence inside these endpoints. The
monotonicity argument proves uniqueness; an additional interval evaluation of
theta' on the returned ball must be positive. The returned Sage RealBall is
the outward union of balls containing both endpoints. Thus root uncertainty
is certified independently of convergence or error estimates for Newton.
All calculations use Arb through Sage at numberdb.bits(digits,losing=160)
bits. At 100 digits this is 493 bits. The guard is substantially larger than
the endpoint radius, allowing the signed phase subtraction even at the
largest stored index. Evidence records minimum measured retained accuracy.
Every stored decimal is checked at its actual one-last-place endpoints;
its bracket is certified again from the continuous log-gamma definition.
Controls include theta(0)=0, an independently tabulated nonzero theta(1),
and checks that translating a stored interval by ten last places is rejected.
Independent checks use mpmath's grampoint at 150 and 200 decimal digits, plus
the phase relation formed from Gamma itself and evaluations of zeta on the
critical line. They supplement the enclosure proof; they do not establish it.
Sources: https://dlmf.nist.gov/5.7.E6 and https://dlmf.nist.gov/5.11.E1.
Instruction provenance: agents/runs/20261028T143558Z-build-skills/manifest.json;
both skill hashes are e37efb7e2ededf6c1d7134c673f152f648f26e0267c556aebdf3ec65765d8b4c.