# Independent PP296 zero evaluator

This directory provides a separate, validated evaluation route for the
Davenport–Heilbronn function in PP296. It uses **MPFR directed rounding**
through pinned `gmpy2==2.3.1`, exact rational Bernoulli coefficients, and an
explicit Euler–Maclaurin remainder. It does not call Arb, `python-flint`,
`acb.zeta`, or another Hurwitz-zeta implementation.

Run from this directory with Python 3.14:

```text
python replay.py --scope negative
python replay.py --scope all
```

`replay.py` installs the pinned dependency into local `deps/` if needed.
It first runs `selftest.py`, which catches loss of directed precision in
unary operations, checks an exact complex reciprocal, and compares two
independent Euler–Maclaurin truncations at the same nontrivial point.
`negative` checks the seven local zero boxes and the enclosing 80–90
rectangle. `all` additionally isolates 179 candidate zeros below 260,
checks the symmetric base rectangle by an exact functional-equation path,
checks twelve 20-unit strips, and writes
`REPLAY_SUMMARY.json`. All receipts are machine-readable JSON. The large
contour receipts retain every accepted rational segment, its full image
enclosure, and its endpoint argument increment. The receipts and replay
summary record source hashes and arithmetic runtime versions.

## Exact function

\[
f(s)=5^{-s}\sum_{r=1}^4a_r\zeta(s,r/5),\qquad
(a_1,a_2,a_3,a_4)=(1,\kappa,-\kappa,-1),
\]

where \(\kappa=(\sqrt{10-2\sqrt5}-2)/(\sqrt5-1)\). Since the four
coefficients sum to zero, the Hurwitz pole residues cancel at \(s=1\),
so \(f\) is entire. None of the evaluated contours crosses a pole in an
individual Hurwitz summand. The completed-function Gamma prefactor has no
zeros or poles in the tested rectangles.

## Enclosure and proof method

`mpfr_em.py` evaluates each Hurwitz term with `N` finite terms and `M`
Euler–Maclaurin corrections. For \(\sigma+2M>1\), it adds the absolute
remainder bound

\[
|R_M|\leq \frac{|B_{2M}|}{(2M)!}|(s)_{2M}|
 \frac{(N+a)^{1-\sigma-2M}}{\sigma+2M-1}.
\]

The periodic Bernoulli polynomial satisfies
\(\sup_x|B_{2M}(x)|=|B_{2M}|\), by its absolutely convergent Fourier
series. The code bounds every factor over the input rectangle with
directed MPFR arithmetic. For the first derivative, differentiating the
remainder integral adds at most
\(\sum_{j=0}^{2M-1}|s+j|^{-1}+\log(N+a)+(\sigma+2M-1)^{-1}\)
times the value remainder bound. The implementation uses lower bounds on
each \(|s+j|\); it refuses a region crossing such a zero.

For a rational square centered at \(c\) with coordinate half-width \(r\),
the Rouché check is

\[
|f(c)|+\sqrt2 r\sup_{z\in B}|f'(z)-f'(c)|
<r|f'(c)|.
\]

The right side is a lower bound on the linear function
\(f'(c)(z-c)\) on the square boundary. The left side bounds the
difference from \(f(z)\). Hence each passing square contains exactly one
simple zero. For the 260 census, the 179 squares are also pairwise
disjoint.

For a contour segment \(a\to b\), the code encloses the whole path image
by \(f(m)+f'([a,b])(z-m)\), where \(m=(a+b)/2\). An accepted image rectangle
excludes zero. Convexity then permits homotopy to the straight polygon
edge between the actual endpoint values. The endpoint ratio has positive
real part, and directed `atan(Im/Real)` bounds its argument increment.
Their sum encloses a unique integer multiple of \(2\pi\).

The symmetric base rectangle is checked by `certify_symmetric_base.py`.
It certifies the open path from \(3/2\) to \(3/2+20i\) to \(1/2+20i\),
then reconstructs the full count using the exact functional equation,
real-coefficient conjugation, and a directed enclosure of the completed
Gamma factor's endpoint phase. See `BASE_SHORTCUT_PROOF.md` and
`DH_FUNCTIONAL_EQUATION_NOTE_2026-09-30.md` for the analytic derivation.
The 12 upper strips and all 179 local squares must match the enclosing
count before the below-260 census is complete.

The 169 squares centered on \(\Re s=1/2\) are invariant under
\(\rho\mapsto1-\overline\rho\), an exact symmetry from the functional
equation and real coefficients. Their unique zeros therefore lie exactly
on the critical line. The other ten certified squares form five mirrored
pairs. The 179 region count and 179 disjoint local zeros exclude additional
zeros below 260 within the analytically established vertical strip
\(-2/5<\Re s<7/5\).

## Scope

These files address the PP296 **zero census** and the specified 80–90
negative-witness window. The tail bound above 260 and the analytic kernel
inequality belong to separate checks. This evaluator alone does not prove
a first failing rung, the Riemann hypothesis, or any global zero claim.