# Certified values of Hardy Z, T586

The signed real function is Z(t)=exp(i theta(t))*zeta(1/2+i*t), with
continuous theta(t)=Im(logGamma(1/4+i*t/2))-t*log(pi)/2. The log-gamma branch
is analytic in the right half-plane and real on the positive real axis.
Hall, equation (1), fixes the convention. The functional equation makes Z
real and even on the real axis. In particular Z'(0)=0.

## Gram arguments

`gram.py` reuses the root routine attached to live T583. Newton iterations
only locate a candidate. An exact rational interval around that candidate
is accepted after opposite strict signs of theta(t)-n*pi are established at
its endpoints. The digamma series

    Re psi(a+i*b) = -gamma + sum(k>=0) [1/(k+1) - (k+a)/((k+a)^2+b^2)]

with a=1/4 shows that theta'(t) increases for t>0: differentiating each
summand gives a positive term for b>0. Local uniform convergence justifies
this differentiation. The computation certifies theta'(7)>0 and
 theta(7)<-pi; Stirling's expansion gives theta(t) tending to infinity.
Thus every n>=-1 has exactly one root in [7,infinity). The finite endpoint
checks fix the selected roots without a phase-wrap ambiguity. See DLMF
5.7.6 for the digamma series and DLMF 5.11.1 for Stirling's expansion.

## Stationary arguments

`stationary.py` reuses the isolation and refinement logic attached to live
T585, recomputing its entire cover. Exact rational intervals partition
[0,233]. On each ordinary interval either Z' excludes zero, or Z'' excludes
zero and strict endpoint signs of Z' count zero or one root. Opposite signs
and monotonicity prove a unique simple root. Otherwise the interval is
subdivided. The checked cover has 26,196 leaves: 20,945 direct exclusions,
5,150 monotone exclusions, 100 unique-root brackets, and one origin interval.
Exact adjacency checks prove that no gap was left between leaves.

On [0,1/1024], the enclosure of Z'' is strictly positive. Since Z'(0)=0,

    Z'(t)/t = integral(u=0..1) Z''(u*t) du

has a positive analytic extension across t=0. There is no positive root in
that interval. The origin is excluded from the stationary sequence, but is
included separately as an argument of Z. The 100 positive roots through
height 233 are consequently the first 100 distinct positive roots. No
Riemann hypothesis or global one-root-per-zeta-gap assertion is used.

At higher precision, Newton iteration again supplies only a candidate.
Fresh opposite signs at rational endpoints and nonzero Z'' on the entire
bracket certify each refined argument. Every derivative here is with
respect to real height. The FLINT coefficient of degree 1 is Z'; degree 2
must be multiplied by 2 to obtain Z''.

## Values and independent validation

Root enclosures are computed with ten more requested digits than the final
value. FLINT's Hardy jet at 493 working bits for 100-digit output evaluates
the full argument ball, preserving its uncertainty and the sign of Z. No
midpoint-only evaluation is used to claim a bound. Both real and imaginary
parts are checked finite, and the imaginary part must contain zero. The
returned real ball must have at least 353 relative accuracy bits.

The checker first establishes nonzero and zero known-answer controls at the
origin and rejects a reversed-sign control. It then computes
exp(i*theta(t))*zeta(1/2+i*t) through separate log-gamma and zeta calls, with
fresh higher-precision root enclosures. It checks finite, narrow balls,
containment in all written 100-digit decimal intervals, evenness, and the
Gram-point relation Z(g_n)=(-1)^n*zeta(1/2+i*g_n). All 100 stationary argument
brackets also pass endpoint sign checks using the independent product
formula for Z', involving digamma and zeta-prime instead of Hardy jets.
These checks distinguish shared library primitives from an independent
algorithm: separate mpmath root and value calculations at 125 and 155
working decimal digits provide a second-library numerical comparison for
all 303 entries. Their agreement supplements the interval proof, rather
than certifying it. Shifting each stored interval by ten last-place units
in either direction is rejected. The checker is run before filling and
again against the strings read back from the database.

`numerical-evidence.json` gives measured accuracy, sizes, runtime versions,
and actual check outcomes. The complete isolation cover is preserved in the
build artifacts and can be reconstructed by the attached source. Source
reuse is from the website attachments of T583 and T585 fetched 2026-10-28;
no computation depends on their stored decimal values or publication state.

The policy manifest is
`agents/runs/20261028T165752Z-build-skills/manifest.json`, attached as
`skill-manifest.json`. Both skill versions have SHA-256
`e37efb7e2ededf6c1d7134c673f152f648f26e0267c556aebdf3ec65765d8b4c`.