# PP296 full-function sign around the recorded witness

This directory is a research audit that can be vendored as
`pp296/negative_interval/`. It uses the seven `1e-9` rational zero boxes
from sibling `../independent_mpfr/boxes.json` in that package, with
`../independent_zero_eval/boxes.json` as the working-directory fallback
(SHA-256
`1e6ba12da49c05a78b2d0bcc807270ed3ba08fc388e2a8133f00763eab09bc58`).
The independently replayed local boxes and 80–90 rectangle have seven zeros
in total; see sibling `../independent_mpfr/REPLAY_SUMMARY.json` in the
package. The analytic full-function bound comes from sibling
`../Astra_followup_as_received.md`,
sections 1 and 3–4.  These are explicit prerequisites to this arithmetic
audit.

## Result

For every real `x` in the closed interval `[7139.83, 7140.28]`, the entire
Davenport–Heilbronn folded sum satisfies

* `G_16589(x) < -2.57845315144859809e-7` (a strict outward decimal upper
  enclosure); therefore `W_16589(x)<0` because
  `W_k(x)=(2k−1)!/(4x)^k G_k(x)` has a positive prefactor.
* `G_16588(x) > 7.62752058031253466e-6` (a strict outward decimal lower
  enclosure); therefore the adjacent rung is positive throughout the *same*
  interval.

The decimal endpoints are exact rationals: `713983/100` and `178507/25`.
The two calculations each partition the interval into 450 closed cells of
width `1/1000`.  Adjacent cells share endpoints, so their union is the full
closed interval.  The resulting receipts are `uniform_negative_receipt.json`
and `uniform_adjacent_receipt.json`.

This is a **specified negative rung**, plus an adjacent-rung statement on
one `x` interval.  It does not establish the first negative rung over all
`x` or certify every earlier rung.  Exploratory floating scans did not find
a smaller negative candidate, but they are neither exhaustive nor a proof.

## Arithmetic proof

For each of the seven upper-half-plane roots `rho`, put
`q=rho(1−rho)` and `R_x(q)=4xq/(x+q)^2`.  The source uses 256-bit dyadic
intervals rounded outward after every basic operation.  Rational box
endpoints and rational `x` cells are exact inputs.  For a cell `[a,b]` with
midpoint `m` and radius `r`, the exact derivative is

`dR_x(q)/dx = 4q(q−x)/(x+q)^3`.

Interval differentiation encloses the derivative of the *complete seven-root
sum* on `[a,b]`.  If `D` is that interval and `V` encloses the sum at `m`,
the mean value theorem gives the uniform seven-root bounds
`V.hi + r max(|D.lo|,|D.hi|)` and
`V.lo − r max(|D.lo|,|D.hi|)`.  Each cell assertion is made using exact
`Fraction` comparisons, before decimal formatting.

For all omitted roots, the analytic shifted-resolvent identity gives
`M = sum Re(6+q)^{-1} = F'(3)/(5F(3)) < 1/3`.  With the coarse strip
`|Re(rho)−1/2|<3/2`, let `y=(Im rho)^2`,
`g_x(y)=4x(y+5/2)/(x+y−2)^2`, and `h_{k,x}(y)=(y+13)g_x(y)^k`.
Then `|R_x(q)|^k <= h_{k,x}(y) Re(6+q)^{-1}`.  For the entire x interval,
`h` increases on `0<=y<=6400` and decreases on `y>=8100`: the latter
follows from exact checks of `A(8100)<0`, `A'(8100)<0`, and
`A''=2(1−k)<0`, where

`A(y)=(y+5/2)(x+y−2)−k(y+13)(y+7−x)`.

Thus the outside-window absolute sum is strictly less than
`max(h_{k,x}(6400),h_{k,x}(8100))/3`.  Each cell takes the maximum in `x`
of the two endpoint kernels analytically: `g_x(y)` increases up to
`x=y−2` and decreases thereafter.  The integer power is evaluated with
outward dyadic rounding.  This uniform outside bound is added for the
negative proof and subtracted for the positive proof.

## Replay

From this directory, with the bundled Python or any Python 3.10+:

```powershell
python certify_uniform.py --lo 7139.83 --hi 7140.28 --step 0.001
python certify_adjacent.py --lo 7139.83 --hi 7140.28 --step 0.001
```

No third-party package or network access is used.  Each command recomputes
all 450 cells and overwrites only its receipt in this directory.  A failed
strict sign assertion stops the run.  The receipts include SHA-256 hashes
of the input boxes, arithmetic module, and producer sources.  As a single
point cross-check, run

```powershell
python certify_interval.py --xlo 7140.06626 --xhi 7140.06626
```

It gives the original seven-box/full-function upper bound
`−1.79602775115900318e−6` at `k=16589`.