# Release audit

Date: 2026-07-19

## Outcome

No blocking mathematical or implementation defect was found in the
local release audit.

## Mathematical checks

1. The pinned source proposition is parameter-uniform on
   \(0<\eta<\nu/2<1/4\), \(\nu+2\eta<1/2\), and
   \(\nu+\eta<1/2\); the chosen exact rationals satisfy all three.
2. The C1--C8 permanence reductions preserve inequality direction,
   including both halves of C5 and the residue-class floor facts in
   C3.
3. The C11 and C12 coefficient envelopes are valid upper bounds and
   decrease after the certified endpoint.
4. For C13b,
   \(D=2\lfloor\widetilde D/2\rfloor\) satisfies
   \(\widetilde D-2<D\le\widetilde D\). The exponent is decreasing
   in \(D\) throughout that interval, so substituting
   \(W=\widetilde D-2\) is an upper, not lower, envelope.
5. The derivative bound for the C13 envelope retains the negative
   leading term. Its positive remainder decreases and has a directed
   endpoint reserve greater than \(2.90619\cdot10^{-9}\).
6. The \(Y_{47}\) ceiling is handled at the integer digit-length
   level. The proof does not make the false intermediate claim that
   \(L_\dagger\log10\le Y_\dagger\).
7. The exact conversion proves
   \(\lfloor2m/9\rfloor\ge L_\dagger\), and the pinned source proof
   then gives \(p\le10^{\lfloor2m/9\rfloor}\le10^{2m/9}\).

## Reproducibility checks

- Python-FLINT/Arb passes at 256, 384, and 512 bits.
- Julia/Nemo independently retypes the binding formulas and passes at
  384 bits.
- The Nemo major-arc path uses the source's rational lower bound for
  \(c_0\), not the Python error-function evaluation.
- The tagged author code gives a corroborative binding threshold
  \(Y_{\rm required}=7.0621019691\ldots\times10^{31}\), strictly
  below the round directed threshold.
- `verify_all.py` pins local scripts, environments, and transcripts
  and reproduces all retained outputs byte for byte.

## External-review limitation

Two read-only hostile reviews were requested from delegated
`gpt-5.6-sol` agents at high reasoning effort. Both failed before
reading the package because the agent account pool returned HTTP 503
with no available accounts. No external-review result is claimed.
The independent Nemo implementation is a separate computational
reconstruction, not a third-party mathematical review.

## Residual boundary

The release imports the analytic lemmas proved in the hash-pinned
Lehmann v1 manuscript. It audits their specialization and threshold
closure, not the full Drmota--Mauduit--Rivat/Mauduit--Rivat analytic
chain from first principles.
