back to table · edit · history · where entries came from · files · download
5026 bytes, as of the version from 2026-10-28 16:45 (current). Recorded here, not run.
# Certificate for the first 100 positive stationary points of Hardy Z
The definition is Z(t)=exp(i theta(t)) zeta(1/2+it), with theta(t) the
imaginary part of log-Gamma(1/4+it/2), minus t log(pi)/2. Log-Gamma is the
analytic branch real on the positive real axis. The functional equation
makes Z real and even on the real axis, so Z'(0)=0. The real function is
analytic on the entire real axis. Hall, equation (1), supplies the convention;
FLINT's Hardy Z routine implements it, with null character/group pointers
selecting the Riemann zeta function. FLINT returns Taylor coefficients, so
coefficient 1 is Z' and twice coefficient 2 is Z''.
## Complete finite enumeration
All interval endpoints are exact rationals. At 96 working bits the generator
constructs a covering of [0,233] by 26,196 adjacent closed intervals. Adjacency
is checked with exact rational arithmetic. Overlap at endpoints causes no
counting ambiguity: every nonzero endpoint participating in a root bracket
has a certified nonzero derivative.
On [0,1/1024], the interval evaluation of Z'' is positive, displayed as
[5.5 +/- 0.0428]. Therefore the analytic extension of
Z'(t)/t = integral from u=0 to 1 of Z''(u*t) du
is positive there. This proves that the origin is the only root of Z' on
this initial interval. The origin is not a selected entry.
Each subsequent leaf interval satisfies one of three certificates:
* 20,945 intervals: the enclosure of Z' excludes zero throughout.
* 5,150 intervals: Z'' excludes zero throughout, and Z' has the same strict
sign at both endpoints. Strict monotonicity excludes a root.
* 100 intervals: Z'' excludes zero throughout, and Z' has opposite strict
signs at the endpoints. The intermediate value theorem supplies one root;
strict monotonicity proves uniqueness, and nonzero Z'' proves simplicity.
When neither test succeeds, subdivision continues. Nonfinite or wide balls
never count as a certificate. No unproved global interlacing statement or
Riemann hypothesis enters the argument. There are exactly 100 distinct
positive roots through height 233, all simple. The endpoint 233 is a stopping
boundary for the certified cover, not an extra free mathematical parameter.
The ordered leaf descriptions have SHA-256
7d3f73b0126a8fd09f520f455c6ad39bd84e2a54e1b6a336e1dcedd28a995132
when encoded by generate.py. The raw covering is preserved as coverage.json
in the build artifacts. Running the generator reconstructs it from scratch.
## Enclosures and serialization
The 96-bit cover selects each root's unique coarse bracket. Newton iteration
at 493 bits proposes a midpoint only. A fresh exact rational bracket of
radius 2^(-383) is tested with strict opposite endpoint signs of Z' and a
nonzero Z'' enclosure. Only after these tests is the bracket returned as a
Sage real ball. Every returned root ball has at least 383 relative accuracy
bits. numberdb.to_text serializes them to 100 significant digits, each
written decimal denoting an interval of one last-place unit on either side.
The independent checker tests the endpoints of those actual decimal intervals.
## Independent checks
checks.py differentiates the defining product using separate log-Gamma,
digamma, zeta and zeta-prime calls, without using the generator's Hardy jet
or root iteration. Its endpoint signs certify a root in each serialized
interval at 560 bits. It checks the zero and nonzero known-answer controls
before evaluating the entries. The same checker rejects intervals displaced
by ten last-place units in both directions for every entry.
Separate mpmath calculations at 125 and 155 decimal digits agree inside all
100 stored intervals. These are independent numerical agreement checks;
rigour comes from the interval arguments, not from mpmath's digits. The parity
identities Z(-t)=Z(t) and Z'(-t)=-Z'(t) are checked for all selected entries.
The first two signed critical values agree with Hall's coarse descriptions.
FLINT isolates the first 99 critical-line zeta zeros independently of the
stationary-point cover. The total zero counts are N(233)=98 and N(234)=99,
where N counts all nontrivial zeros with multiplicity up to the given height.
The 99 distinct critical-line roots lie below 234, so this finite comparison
also certifies their simplicity and completeness. The stationary points c_1
and c_2 precede the first zeta zero. For 3 <= j <= 100, the stored interval
lies strictly between gamma_{j-2} and gamma_{j-1}. These are assertions about
the checked finite range only.
## Policy and provenance
The policy manifest is
../20261028T160405Z-build-skills/manifest.json in the archived run and
skill-manifest.json among the attachments. Both archived skill copies have
SHA-256 e37efb7e2ededf6c1d7134c673f152f648f26e0267c556aebdf3ec65765d8b4c.
The bridge hardy_arb.pyx was read from the attached source of T584 and reused;
it does not enumerate stationary points. All selection and root-isolation
logic for this table is in generate.py. No independent critique acceptance
is claimed by this build.