A 7/8 zero-free half-plane for angular Hecke L-functions over the Eisenstein field

Primarily AI-generated textHuman understanding: some partsmath.NT — Number Theorymath.CV — Complex Variables

Contributed by Troy Winarski ↗

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 LL-functions over Q(−3)\mathbb{Q}(\sqrt{-3}) in the strict half-plane ℜ(s)>7/8\Re(s)>7/8, 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 15/1615/16 result for the same angular family. The proof compares two estimates for a single normalized physical probe: a low bound with exponent 3/16+ω3/16+\omega and an approximation by a reciprocal Mellin signal with error exponent βn−11/16−σ\beta_n-11/16-\sigma, where βn\beta_n is the supremum of the real parts of zeros within a finite angular cap. Crucially, the positive saving σ\sigma 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

This work arose from an AI-assisted research program investigating extensions of OpenAI Math Family 003. The project first produced a Lean-verified numerical extension of the original Family 003 zero-free region using the same finite-order Hecke and Dirichlet setting; that development and its verification evidence are publicly archived on GitHub. The investigation was then extended in a different direction, from finite-order characters to unit-compatible angular Hecke characters over Q(sqrt{-3})), including nonzero angular type. An initial Lean-verified theorem established the zero-free region Re(s)>23/24 for this angular family and was publicly released with frozen source and verification evidence. Further AI-assisted mathematical analysis, proof development, and Lean formalization strengthened the earlier result to the present strict $\Re(s)>7/8$ zero-free theorem for the full unit-compatible angular Hecke family over the Eisenstein field, including all admissible integer angular orders, primitive and imprimitive finite parts, real unitary norm twists, and the stated principal-pole exceptions. The result subsequently passed a separate AI-assisted mathematical audit and a clean source-build and native Lean kernel-replay verification of its repaired public proof closure. AI systems were used extensively for mathematical exploration, formal proof development, source reconstruction, and auditing. The human contributor directed the research, selected research goals, evaluated intermediate results and scope, and is responsible for the claims and presentation of this submission. The formal source, frozen verification evidence, and public development history are linked separately through the associated GitHub repositories. https://github.com/TheRealDubb/family-003-extension-xenoproof https://github.com/TheRealDubb/angular-hecke-23-24 https://github.com/TheRealDubb/angular-hecke-15-16-xenoproof https://github.com/TheRealDubb/angular-hecke-7-8-xenoproof

Tools used

OpenAI
CodexVersion GPT 6 Astra - Extra High

References

  1. 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
  2. T. Winarski, Eisenstein angular Hecke LL-functions: 7/87/8 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
  3. T. Winarski, A 15/1615/16 zero-free half-plane for angular Hecke LL-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
  4. 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
  5. 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
  6. 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
  7. 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

  1. v1Submitted by Troy WinarskiInitial depositCurrentOct 31, 2026