HEXAGONbeta

A 15/16 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 Variablesmath.LO — Logic

Contributed by Troy Winarski ↗

Version 1 / Oct 22, 2026 / CC BY 4.0

Abstract

We describe the argument recorded in a frozen Lean development for nonvanishing of the unit-compatible angular Hecke L-functions over Q(−3)\mathbb Q(\sqrt{-3}) in the strict half-plane ℜ(s)>15/16\Re(s)>15/16, apart from the genuine principal pole. The family includes imprimitive finite parts, every integer angular type allowed by the unit relation, and real unitary norm twists. The proof route passes through a mean-square estimate for the actual sextic rows, sixth-power averaging, a smoothed Möbius estimate with a totient factor, and Mellin continuation. We reconstruct the angular reflection, quadratic energy estimate, finite descent, and the calculation producing the 15/1615/16 exponent, while identifying the technical source lemmas inherited from OAI-003 that remain to be independently reconstructed. The theorem is formally verified in Lean and the frozen source/evidence package has undergone statement comparison, axiom audit, recursive kernel replay, quotient postchecking, and separate AI-assisted review. This manuscript is an expository reconstruction rather than a claim of independent human certification. We describe the formally verified proof as a xenoproof, and the theorem provisionally as a xenotheorem, to distinguish formal mathematical correctness from 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 analysis and formalization strengthened that result to the present strict Re(s)>15/16 theorem for the same angular Hecke family, including real unitary norm twists and the stated principal-pole exception. 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

Tools used

OpenAI
CodexVersion GPT 6 Astra - Extra High

References

  1. S. J. Patterson, A cubic analogue of the theta series , Journal für die reine und angewandte Mathematik 296 (1977), 125--161. doi:10.1515/crll.1977.296.125 (https://doi.org/10.1515/crll.1977.296.125). Classical background for the cubic theta function.DOI
  2. D. R. Heath-Brown, A mean value estimate for real character sums , Acta Arithmetica 72 (1995), no. 3, 235--275. doi:10.4064/aa-72-3-235-275 (https://doi.org/10.4064/aa-72-3-235-275). Classical quadratic large-sieve background.DOI
  3. L. Goldmakher and B. Louvel, A quadratic large sieve inequality over number fields , Mathematical Proceedings of the Cambridge Philosophical Society 154 (2013), no. 2, 193--212. doi:10.1017/S0305004112000370 (https://doi.org/10.1017/S0305004112000370). Author version: https://arxiv.org/abs/1112.1642. Theorem 1.1 is the fixed-modulus quadratic Hecke-family inequality discussed in Section sec:energy .DOI
  4. A. Dunn and M. Radziwiłł, Bias in cubic Gauss sums: Patterson's conjecture , Annals of Mathematics 200 (2024), no. 3, 967--1057. doi:10.4007/annals.2024.200.3.3 (https://doi.org/10.4007/annals.2024.200.3.3). Related cubic theta and Voronoi framework. Its GRH-conditional prime asymptotic is not an input to the argument here.DOI
  5. OpenAI, OAI-003 source development , repository openai/math , revision adc7f1241b42e322a6451854ab7e4b4c146bf78a . https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a. Pinned source material; no peer-reviewed publication status is asserted here.link
  6. T. Winarski, Angular Hecke 15/1615/16 frozen source and native Windows verification evidence , public GitHub repository TheRealDubb/angular-hecke-15-16-xenoproof , release v15-16-2026-10-18 , commit 67bb5d2df315fe5ebe7b6ffe0eb4529ffef225de . Tagged release and evidence assets (https://github.com/TheRealDubb/angular-hecke-15-16-xenoproof/releases/tag/v15-16-2026-10-18); source at the frozen commit (https://github.com/TheRealDubb/angular-hecke-15-16-xenoproof/tree/67bb5d2df315fe5ebe7b6ffe0eb4529ffef225de). Source closure, exact theorem scope, dependency pins, and replay evidence as specified in Appendix sec:concordance . This source/evidence release is distinct from later explanatory README edits on main ; no independent human certification is asserted.link

Version history

  1. v1Submitted by Troy WinarskiInitial depositCurrentOct 22, 2026