Hailey Collet · HaileyCollet@gmail.com

This continues the research behind the single-compensating-prime proof and quartic boundary. It gives c = 0.125139, or the exact zero-free half-plane Re(s) > 0.874861.

The theorem covers every complex Dirichlet character of nonzero modulus, the Riemann zeta function, and the stated finite-order Hecke family over the Eisenstein field. The principal poles are excluded, and the boundary is strict.

The argument combines earlier moment estimates and source machinery with Gao’s local refinement, extends the required density range, and supplies a common probe for the final zero-exclusion argument. The paper follows the completed Lean construction, including its source normalization, choice order and full error estimate.

Formalization and verification

The unconditional endpoint and the Dirichlet, zeta and Hecke declarations compile in Lean 4.34.1 with only the standard axioms. The complete clean rebuild passed for all 3,695 source modules, with no submitted objects reused. The original Dirichlet, zeta and Hecke proof closures passed Comparator and all three kernels: Lean, NanoDa and con-ron. The bundled Candidate also passed a fresh 194-module compilation, the canonical Dirichlet Comparator and all three kernels.

Both local replays used a documented native judge adapter because this host refused the standard nested namespace setup. They retained the trusted Comparator, protected inputs and official per-kernel sandboxes. The verification record describes those checks and their limits. The separate protected check of the submitted commit is running in PR #42; consult the PR for its current status.

Authorship and sources

I initiated and directed the research, chose the targets and sources, and organized the assembly and checking of the argument. The detailed mathematical derivations and substantial drafting were AI-assisted. Astra and GPT-6.1 Sol performed the Lean formalization; I commissioned and coordinated it. I am the sole human author; this does not attribute every derivation produced within the project to me personally.

The proof credits OpenAI’s original seven-eighths framework, Akash Levy’s weighted-numerator work, Gao’s local refinement and the earlier AI-assisted work in this research program. Read the detailed contribution and attribution account, including my research questions, source integration and coordination, with the original proof work distinguished from later research and catalogue design. The paper and new code are available under Apache-2.0, with upstream attribution and licenses retained.