A 7/8 zero-free half-plane for angular Hecke L-functions over the Eisenstein field
Version 1 / Nov 02, 2026 / CC BY 4.0
Abstract
We reconstruct the argument recorded in a frozen Lean development establishing nonvanishing of the unit-compatible angular Hecke -functions over in the strict half-plane , apart from the genuine principal pole. The family includes every admissible integer angular order, all nonzero finite ideal moduli, primitive and imprimitive presentations, and real unitary norm twists. This strengthens the earlier result for the same angular family.
The proof compares two estimates for a single normalized physical probe: a low bound with exponent and an approximation by a reciprocal Mellin signal with error exponent , where is the supremum of the real parts of zeros within a finite angular cap. Crucially, the positive saving is chosen before the target character. Mellin continuation converts these estimates into a strict improvement of the zero supremum. Induction on angular order, together with conjugation, establishes nonvanishing for the full family.
The repaired public proof closure passed a clean compilation of 8,213 Lean modules and fresh native Lean kernel replay. An independent AI-assisted audit recorded five ACCEPT verdicts for the repaired package, following the identification and correction of a reproducibility defect in the original archive. We document the mathematical argument, formal verification evidence, and remaining limitations. This manuscript is an expository reconstruction, not independent human mathematical certification. We describe the formally verified proof as a *xenoproof* and the result provisionally as a *xenotheorem*, distinguishing machine-checkable correctness from established human mathematical understanding.
Provenance statement
Tools used
- OpenAI
- CodexVersion GPT 6 Astra - Extra High
References
- OpenAI, OAI-003 source development , repository openai/math at the pinned revision (https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a). The formal source and background manuscripts are source artifacts, not journal certification of the angular extension.link
- T. Winarski, Eisenstein angular Hecke -functions: zero-free half-plane , source and evidence release, v7-8-2026-10-30 , frozen 30 October 2026; published 31 October 2026. https://github.com/TheRealDubb/angular-hecke-7-8-xenoproof/releases/tag/v7-8-2026-10-30. Commit and evidence archive: Appendix sec:artifacts . The final original audit and repair report are dated 29 October 2026; the recorded fresh replay completed on 30 October UTC, still 29 October in New York.link
- T. Winarski, A zero-free half-plane for angular Hecke -functions over the Eisenstein field: a mathematical reconstruction of the frozen Lean proof , manuscript dated 21 October 2026. Associated frozen source/evidence release (https://github.com/TheRealDubb/angular-hecke-15-16-xenoproof/releases/tag/v15-16-2026-10-18), v15-16-2026-10-18 . The manuscript date and the earlier source-release date identify distinct artifacts.link
- L. Goldmakher and B. Louvel, A quadratic large sieve inequality over number fields , arXiv:1112.1642v2 (https://arxiv.org/abs/1112.1642v2), 31 May 2012. Definition 1 and Theorem 1.1 are the audited classical comparison points.arXiv
- D. R. Heath-Brown, Kummer's conjecture for cubic Gauss sums , Israel Journal of Mathematics 120 (2000), 97--124, doi:10.1007/s11856-000-1273-y (https://doi.org/10.1007/s11856-000-1273-y). The audit compares Theorem 2 with the Eisenstein cubic sieve application.DOI
- A. Dunn and M. Radziwiłł, Bias in cubic Gauss sums: Patterson's conjecture , arXiv:2109.07463v3 (https://arxiv.org/abs/2109.07463v3), 14 May 2024. The cited audit examines the relevant cubic sieve and metaplectic formulas; it does not import a GRH-dependent prime asymptotic into this theorem.arXiv
- NIST Digital Library of Mathematical Functions, equation 10.43.19 (https://dlmf.nist.gov/10.43.E19), the K-Bessel Mellin integral convention compared in the final audit.link
Version history
- v1 · 16 pagesSubmitted by Troy WinarskiInitial depositCurrentOct 31, 2026