\documentclass[11pt]{article} \usepackage[margin=1in]{geometry} \usepackage[T1]{fontenc} \usepackage{lmodern,amsmath,amssymb,amsthm,mathtools} \usepackage{booktabs,longtable,array,enumitem,microtype,xcolor,xurl} \usepackage[unicode,colorlinks=true,linkcolor=blue!45!black,citecolor=blue!45!black,urlcolor=blue!45!black]{hyperref} \hypersetup{pdftitle={A 7/8 zero-free half-plane for angular Hecke L-functions over the Eisenstein field},pdfauthor={Troy Winarski},pdfsubject={A source-grounded reconstruction of the repaired and replayed Lean proof}} \newtheorem{theorem}{Theorem}[section] \newtheorem{proposition}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \newtheorem{remark}[theorem]{Remark} \newcommand{\C}{\mathbb C} \newcommand{\R}{\mathbb R} \newcommand{\Z}{\mathbb Z} \newcommand{\N}{\mathbb N} \newcommand{\OO}{\mathcal O} \newcommand{\Nm}{\mathrm N} \newcommand{\Rea}{\operatorname{Re}} \newcommand{\dd}{\,\mathrm d} \newcommand{\abs}[1]{\left|#1\right|} \newcommand{\src}[2]{\par\smallskip\noindent{\footnotesize\textit{Source correspondence #1.} #2}\par\smallskip} \newcommand{\fid}[1]{\path{#1}} \newcommand{\technical}{\textit{Technical formal input.}} \setlength{\emergencystretch}{3em} \setlist{itemsep=3pt,topsep=5pt} \numberwithin{equation}{section} \title{A \(7/8\) zero-free half-plane for angular Hecke \(L\)-functions over the Eisenstein field\\[5pt] \large The physical detector, a common signal, and finite-cap closure} \author{Troy Winarski\\[2pt]\small Independent researcher\\ \small ORCID: \href{https://orcid.org/0009-0004-5956-3825}{0009-0004-5956-3825}} \date{31 October 2026} \begin{document} \maketitle \begin{abstract} We reconstruct the frozen Lean argument for nonvanishing of the angular Hecke \(L\)-functions over \(\mathbb Q(\sqrt{-3})\) in the strict half-plane \(\Rea s>7/8\), apart from the principal pole. The family includes every unit-compatible integer angular type, all nonzero finite ideal moduli, imprimitive presentations, and real unitary norm twists. The argument uses two bounds for one normalized physical probe: a low estimate with exponent \(3/16+\omega\), and a comparison with a reciprocal Mellin signal with exponent \(\beta_n-11/16-\sigma\). The saving is chosen before the target character. Their combination improves the actual zero supremum at each finite angular cap; induction and conjugation close the full family. We explain the normalization, the analytic implication, and the quantifiers on which this contradiction depends, while identifying the longer arithmetic estimates as technical inputs from the formal source. The separately repaired public import closure has a recorded clean build of 8,213 source modules and fresh native Lean kernel replay. We document the original reproducibility failure, its repair, and the separate AI-assisted audit. This exposition is not itself Lean-verified and is not independent human mathematical certification. The proof is presented as a xenoproof, and the result provisionally as a xenotheorem, in the sense specified in Section~\ref{sec:status}. \end{abstract} \tableofcontents \section{The theorem and the family}\label{sec:statement} Put \(K=\mathbb Q(\sqrt{-3})\), \(\omega_3=(-1+\sqrt{-3})/2\), and \(\OO=\Z[\omega_3]\). Fix the complex embedding with \(\omega_3=e^{2\pi i/3}\). For \(a\ne0\), set \[ \alpha(a)=a/|a|,\qquad \Nm(a)=|a|^2. \] For a nonzero integral ideal \(\mathfrak a\), \(\Nm\mathfrak a=|\OO/\mathfrak a|\). The Eisenstein ring is principal, and its unit group has six elements. \begin{definition}[Admitted character]\label{def:family} An angular character is a triple \(\chi=(k,\mathfrak m,\nu)\), where \(k\in\Z\), \(\mathfrak m\ne0\) is an integral ideal, and \(\nu\) is a multiplicative residue character modulo \(\mathfrak m\), with its prescribed zero extension, such that \begin{equation}\label{eq:unit} \alpha(u)^k\nu(u\bmod\mathfrak m)=1\quad (u\in\OO^\times). \end{equation} Its element coefficient is zero at zero and is \(c_\chi(a)=\alpha(a)^k\nu(a\bmod\mathfrak m)\) otherwise. Its ideal coefficient is \(\chi((a))=c_\chi(a)\), with value zero on the zero ideal. \end{definition} Equation~\eqref{eq:unit} makes the ideal coefficient independent of the generator: \(c_\chi(ua)=c_\chi(a)\). It is multiplicative, has absolute value at most one, and, on nonzero ideals, vanishes precisely at the ideals not coprime to \(\mathfrak m\). The finite part and the angular order are therefore constrained by compatibility; the theorem does not pair arbitrary residue characters with arbitrary integers. In particular, no periodicity of \(\alpha(a)^k\) as a function of the residue class of \(a\) is assumed. \src{C01}{\fid{AngularCharacter.lean}, lines 48--173, especially \fid{elementCoeff_unit_mul}, \fid{idealHom_span}, and \fid{idealHom_zero_iff}.} For \(\Rea s>1\), define \begin{equation}\label{eq:series} L(\chi,s)=\sum_{\mathfrak a\ne0}\chi(\mathfrak a)(\Nm\mathfrak a)^{-s} =\prod_{\mathfrak p}\bigl(1-\chi(\mathfrak p)(\Nm\mathfrak p)^{-s}\bigr)^{-1}. \end{equation} Positive norms use the real logarithm in their complex powers. The source proves absolute convergence and the Euler product on this half-plane. Below it, \(L\) denotes the continuation constructed from the primitive theta function and the exact imprimitive Euler factors, rather than the totalized value of a possibly divergent formal sum. This distinction is part of the statement-to-object comparison. For nonzero angular order the continued function is entire. Type zero uses the separate finite-character identifications at the pole and at one. \src{C02}{\fid{AngularSeries.lean}, lines 19--62; \fid{AngularFamilyContinuation.lean}, \fid{LFunction_eq_series} and \fid{LFunction_differentiable}; \fid{AngularPhysicalPublicStatementCheck.lean}, lines 11--20.} \begin{theorem}[The public statement]\label{thm:main} For every admitted \(\chi=(k,\mathfrak m,\nu)\) and every \(s\in\C\), \[ \Rea s>7/8\quad\Longrightarrow\quad L(\chi,s)\ne0, \] provided that \(s\ne1\) when \(k=0\) and \(\nu\) is principal. For \(\tau\in\R\), the coefficient \(\chi_\tau(\mathfrak a)=\chi(\mathfrak a)(\Nm\mathfrak a)^{i\tau}\) has continuation \(L(\chi,s-i\tau)\) and the same zero-free half-plane, with \(s=1+i\tau\) excluded in the principal case. \end{theorem} Both signs of \(k\), type zero, primitive and imprimitive finite parts, and all nonzero ideal moduli are included. For the alternative coefficient \(\chi(\mathfrak a)(\Nm\mathfrak a)^{-i\tau}\), the shift is \(s+i\tau\) and the exceptional point is \(1-i\tau\). There is no assertion on \(\Rea s=7/8\), no assertion below \(7/8\), and no Gaussian-field theorem. The conclusion is pointwise for the full family. Its proof uses estimates at fixed finite angular caps; it does not assert estimates uniform over unbounded angular order. \src{C03}{\fid{AngularPhysicalFinalAssembly.lean}, lines 117--120; \fid{AngularPhysicalNormTwistNonvanishing.lean}, lines 13--48.} \subsection{What is new in this reconstruction} The previous \(15/16\) exposition~\cite{Previous} followed sixth-power averaging and a smoothed M\"obius estimate into a nonvanishing statement. The present formal assembly has a different decisive implication. It compares one physical probe with one reciprocal signal and contradicts a supremum over actual zeros. The identity \[ \frac{3}{16}+\frac{11}{16}=\frac78 \] locates the new boundary, but the identity alone supplies no zero-free region. The low bound, the high comparison with a common positive saving, the analytic meaning of the signal, and the induction on angular caps are all required. Sections~\ref{sec:probe}--\ref{sec:high} expose the analytic interfaces and their realization by the actual probe. Sections~\ref{sec:mellin} and \ref{sec:closure} give the final mathematical deduction. The long local and energy decompositions remain explicit technical formal inputs, with source locators. This is an expository reconstruction of that dependency chain, not a claim to reproduce all 8,213 modules as a standalone handwritten proof. The supplied claim concordance records the source comparison for the major statements made here. Neither prose nor concordance is a Lean proof. \section{The actual zero supremum and the required quantifiers}\label{sec:sup} For \(n\in\N\), let \begin{align} \mathcal Z_n=\{\Rea s :{}& |k_\chi|\le n,\ 0<\Rea s,\ L(\chi,s)=0,\notag\\[-2pt] &s\ne1\ \text{if }k_\chi=0\text{ and }\nu_\chi=1\},\label{eq:zeros}\\ \beta_n={}&\sup\bigl(\{1/2\}\cup\mathcal Z_n\bigr).\label{eq:beta} \end{align} The characters range over all finite moduli. Nonvanishing from the absolutely convergent Euler product gives \(\beta_n\le1\); the inserted sentinel gives \(\beta_n\ge1/2\). Thus the supremum exists without requiring a zero or requiring that the supremum be attained. By its definition, every character in the cap is zero-free to the right of \(\beta_n\). This is a tautological starting region for reciprocal estimates, not an assumption of the desired bound. \src{C04}{\fid{AngularPhysicalZeroSupremum.lean}, lines 13--56 and 98--115.} The key analytic supplier is the following property: \begin{equation}\label{eq:improvement} \begin{gathered} \forall n>0,\quad \beta_n>7/8\ \Longrightarrow\ \exists\delta_n>0\ \forall\eta\ (k_\eta=-n)\ \forall s,\\ \Rea s>\beta_n-\delta_n\ \Longrightarrow\ L(\eta,s)\ne0. \end{gathered} \end{equation} The order of \(\exists\delta_n\) and \(\forall\eta\) is essential. A separate positive improvement for each character need not move the supremum over all conductors. Conversely, an asymptotic multiplicative constant or threshold depending on \(\eta\) does not prevent~\eqref{eq:improvement}, provided that the continuation boundary is common. The formal cap-closure module first proves a conditional theorem with \eqref{eq:improvement} as an explicit premise, named \fid{NegativeOrderImprovement}. The final assembly then supplies that premise. It is not a new axiom and is not left as a hypothesis of Theorem~\ref{thm:main}. \src{C05}{\fid{AngularPhysicalCapClosure.lean}, lines 38--89; \fid{AngularPhysicalFinalAssembly.lean}, lines 36--113.} \section{One physical probe and its normalization}\label{sec:probe} Fix \(n>0\), provisionally suppose \(\beta_n>7/8\), and put \(\omega=(\beta_n-7/8)/2\). The final assembly first chooses numerical parameters, a fixed finite set \(S\) of excluded primes, a ray modulus and subgroup, and nonzero nonnegative smooth windows. These choices are made before the target \(\eta\) of angular order \(-n\). The exclusions satisfy the source-tail and fixed-bad-prime conditions used in the analytic estimates; they are not an unspecified arbitrary finite set. \subsection{Slots and the exact signed operation} There are an even positive number \(N\) of prime slots, with distinct positive lengths \(\ell_j\) satisfying \begin{equation}\label{eq:lengths} \sum_{j=1}^{N}\ell_j=\frac16,\qquad X=Z^{17/48},\quad Y=Z^{23/48},\quad Y_j=Z^{\ell_j}. \end{equation} The pool \(T_j(Z)\) consists of primes outside \(S\), in the fixed identity ray class, with norms between \(Y_j\) and \(2Y_j\). Canonical generators give the element supports used in the physical formula. Distinct exponents make these annuli disjoint eventually. For each fixed target, their lower endpoints also eventually exceed its finitely many modulus primes; this eventual statement allows a target-dependent threshold. Write \(\mathcal P_{\eta,D}(X,Y,Z)\) for the source's \fid{markedPhysicalProbe}, with mark ideal \(D\), and write \(\mathcal P_{\eta,1}\) for its unmarked version. This is a specified spectral sum, not an arbitrary function selected to meet estimates. In particular its row coefficient, before any absolute value is taken, is \begin{equation}\label{eq:rowcoefficient} c_\eta(a)\,\overline{\Xi(a)}\, \operatorname{recip}(s,a)\,\operatorname{row}_{m}((a)). \end{equation} Here \(\Xi\), the sextic reciprocity phase, and the ideal row are the calibration and arithmetic objects in the source. The actual infinite-order factor \(c_\eta(a)\) remains present. The formal definition sums supported ideals, a Gauss-weighted lattice variable, and a vertical integral on \(\Rea t=4\) with kernel \(Z^t e^{t^2}\). Its normalization includes the calibration scalar, the row norm square root, and the scale of the lattice window. These choices are retained by both subsequent estimates. For a single slot with element \(p\), the exact compensation is \begin{equation}\label{eq:compensation} \overline{c_\eta(p)}\, \mathcal P_{\eta,(p)}(X,Y,Z\Nm p) -(\Nm p)^{-3/2}\mathcal P_{\eta,1}(X/\Nm p,Y/\Nm p,Z). \end{equation} For several slots the source applies its finite tuple compensation operation and sums the resulting expressions with weight \(\prod_j w(\Nm p_j/Y_j)\). Denote this exact result by \(\mathcal I_\eta(Z)\). Equation~\eqref{eq:compensation} explains why replacing the construction by an unsigned amplification, or dropping its conjugate target factor, would change the theorem being estimated. \src{C06}{\fid{AngularPhysicalDetectorPhysicalProbe.lean}, lines 19--117; \fid{AngularPhysicalFinalAssembly.lean}, lines 24--34; \fid{AngularPhysicalPrincipalNormalized.lean}, lines 64--80.} \subsection{The source and prime-mass scalar} Set \begin{equation}\label{eq:mass} M_j(Z)=\sum_{\mathfrak p\in T_j(Z)} w\bigl(\Nm\mathfrak p/Y_j\bigr)(\Nm\mathfrak p)^{-5/6}. \end{equation} The fixed source scalar is \begin{equation}\label{eq:sourceconstant} c_S=\mathcal M W_1(1)\, \mathcal M(\widehat W_0^{\mathrm{rad}})(1/6)\,\frac{R_S^2}{6}, \end{equation} where \(\widehat W_0^{\mathrm{rad}}\) is the source's radial Fourier transform, \(\mathcal M\) is its Mellin transform convention, and \(R_S\) is the principal residue with the fixed prime exclusions. The factor \(1/6\) comes from the pole at \(6z=1\); it is not an adjustable normalization. The normalizer and the probe used in the final assembly are \begin{equation}\label{eq:normalizer} A(Z)=(-1)^N Z^{-1/36}\prod_{j=1}^N M_j(Z),\qquad J_\eta(Z)=\frac{\mathcal I_\eta(Z)}{c_S A(Z)}. \end{equation} Here \(-1/36=-(1/6)/6\), as in \fid{Probe.principalScalar}. The fixed windows make \(c_S\ne0\); the ray-prime mass theorem gives eventual positivity of each \(M_j\). For every positive loss allowance the reciprocal normalizer has the corresponding eventual small-power bound. Such a bound must be paid when passing from an unnormalized estimate to \(J_\eta\). The prime-mass input uses the established boundary nonvanishing and ray-prime asymptotic route in OAI-003. The final audit checks that it does not invoke the new angular \(7/8\) theorem to justify its own normalizer. This is one of the places where source correspondence is more informative than a generic appeal to primes in progressions. \src{C07}{\fid{OAI/NumberTheory/DirichletL/Detector/PrincipalResidueActual.lean}, \fid{residueWeights}; \fid{PrincipalSignalComparison.lean}, \fid{slotMass}; \fid{PrincipalMellinResidues.lean}, \fid{sourceResidueConstant}; \fid{Detector/Basic.lean}, \fid{principalScalar}; \fid{AngularPhysicalLowNormalized.lean}, lines 54--74. Short OAI paths in this paragraph are relative to \fid{OAI/NumberTheory/DirichletL/}. Audit: sections 3--4.} \section{The low estimate and the retained angular machinery}\label{sec:low} \begin{proposition}[Low estimate at the chosen witnesses]\label{prop:low} For the fixed source and slot data above, every positive loss \(\lambda\), and every target \(\eta\) of negative nonzero angular order, the actual normalized probe satisfies \begin{equation}\label{eq:low} J_\eta(Z)=O_\eta\bigl(Z^{3/16+\lambda}\bigr)\qquad(Z\longrightarrow\infty). \end{equation} The constants also depend on the fixed data and on \(\lambda\). The normalizer is nonzero for all sufficiently large \(Z\). \end{proposition} \noindent\technical\ The formal statement retains the ray subgroup's containment of global units, the source exclusions, positive support intervals, smoothness, nonnegativity and nonzeroness of the windows, injectivity of slot lengths, and their sum \(1/6\). These hypotheses are supplied by the fixed witnesses in the final assembly. They are not being replaced by a claim about arbitrary coefficients or arbitrary windows. The final normalization step has a short proof worth making explicit. Use half the desired loss in the unnormalized physical-probe estimate and half in the inverse-normalizer bound: \[ |\mathcal I_\eta(Z)|\le C_1 Z^{3/16+\lambda/2},\qquad |(c_S A(Z))^{-1}|\le C_2 Z^{\lambda/2}. \] Multiplication gives~\eqref{eq:low}. The window-bound reduction first divides each slot window by \(D=\max(1,B)\); restoring all \(N\) windows costs the fixed factor \(D^N\), not another exponent depending on \(Z\). \src{C08}{\fid{AngularPhysicalLowWindowBound.lean}, lines 26--77; \fid{AngularPhysicalLowNormalized.lean}, lines 17--74.} \subsection{What the low bound contains} The input is about the literal angular coefficient. Its dependency route passes from angular reflection and completed coefficients through selected physical energy, a tuple Gram identity, the total Gaussian sum, and the common physical bound. The following interfaces identify the mathematical tasks without pretending that a one-line estimate reproduces their proofs. \begin{longtable}{p{.26\textwidth}p{.66\textwidth}} \toprule Task & Formal interface and retained information\\\midrule\endhead Angular coefficient & \fid{AngularCanonicalCoefficient} and \fid{AngularControlledScalar}: distinguish the finite residue factor from the angular phase; preserve the actual coefficient.\\[4pt] Common Fourier density & \fid{AngularKernelSourceUniform} and \fid{AngularKernelSeparation}: choose the common separating density before the moving arithmetic data, and retain its norm cost.\\[4pt] Completed energy & \fid{AngularFullBudget}: retained and discarded-source terms are combined with the fixed-cusp, mask, scale, and canonical-margin hypotheses.\\[4pt] Physical selection & \fid{AngularPhysicalLowSelectedBound} and \fid{AngularPhysicalLowPhysicalInverseBound}: specialize the energy estimate to the selected physical rows and their normalization.\\[4pt] Gram and Gaussian sum & \fid{AngularPhysicalLowTupleGram} and \fid{AngularPhysicalLowGaussianSum}: retain the actual paired terms before applying bounds and summing the physical rows.\\\bottomrule \end{longtable} For example, the full-budget source bounds the sum of squared literal sector rows by an expression of the form \begin{equation}\label{eq:sector} C(1+|\theta|)^d Z^{F_0-3c_*/16-O_0/2}. \end{equation} This formula is recorded only under the full source hypotheses: matching powerful and mask parts; norm ranges and admissible squarefree/cubic families; canonical margins; cusp congruences and coprimalities; and the stated scale, pool, loss, and tail inequalities. It is not asserted for unrestricted rows. The height degree \(d\) is selected before the arithmetic cusp data; the constant and threshold may then depend on the fixed cusp, and precede the finite indexing families. The term \(O_0/2\) and the squared density norm are among the multiplicity and energy costs checked in the final audit. \src{C09}{\fid{AngularFullBudget.lean}, lines 15--79 and 95--113. Audit: sections 1 and 4, LOW/FULL energy and common-density passages.} The formal reductions use the quadratic and cubic sieve inputs after the required decompositions. The audited quadratic application uses primitive inducing quadratic characters, squarefree good ideals and the fixed reciprocity classes; it does not turn an arbitrary row-dependent mask into a scalar coefficient. The audited cubic application uses primary squarefree Eisenstein variables, with nonsquarefree factors decomposed and paid beforehand. The angular factor is preserved and separated at the appropriate stage rather than declared a finite-order character. These are statements about the reviewed application route; they are not blanket claims about all theorems in the cited literature. The longer reductions remain technical formal inputs to Proposition~\ref{prop:low}. \src{C10}{Final audit, section 3; \fid{PROOF_DOSSIER.md} in the frozen release. Classical provenance: \cite{GL,HB,DR}; formal import graph: \fid{metadata/MODULE_INDEX.json}.} \section{The counted detector and the common positive saving}\label{sec:high} \subsection{The detector is compared with its actual principal pool} Let \(\mathcal I^{\mathrm{pr}}_\eta(Z)\) denote the principal physical pool in the same row decomposition. The detector theorem proves, for the chosen retained parameters \(p\), \begin{equation}\label{eq:detector} \left|\frac{\mathcal I_\eta(Z)-\mathcal I^{\mathrm{pr}}_\eta(Z)}{c_S A(Z)}\right| \le C_{\mathrm{det}}(\Nm\mathfrak m_\eta)^2 Z^{\beta_n-11/16-p.\mathrm{saving}} \end{equation} eventually. The constant \(C_{\mathrm{det}}>0\) is chosen before \(\eta\). The source's explicit factor is the norm of its \emph{presentation modulus} squared, not a silently substituted primitive conductor. The threshold may depend on \(\eta\). The inequality is conditional on the fixed source, profile, ray, and retained-parameter hypotheses in the cited theorem, all of which the final assembly instantiates. \src{C11}{\fid{AngularPhysicalDetectorActualPhysicalContraction.lean}, \fid{actual_conductor_uniform_physical_contraction}, lines 26--61.} The principal pool is not yet the reciprocal signal. It has a separate comparison, and its constant is allowed to depend on the target. Combining these two stages while conflating their quantifiers would overstate the uniformity actually proved. \subsection{Numerical reserves and the order of choices} The source's retained-parameter structure uses a finite even slot family, positive lengths, a small reserve \(0<\rho\le10^{-8}\), and \[ \frac56 r_{\min}\le\ell_j\le\frac1{200}R,\qquad \sum_j\ell_j=\frac16. \] Its numerical parameter-existence theorem supplies such data for every positive requested gap, with \(07/8\) and satisfies \begin{equation}\label{eq:H} |H_\eta(s)-1|\le\frac12. \end{equation} Consequently it is nowhere zero there. Its source definition is \texttt{globalClosedCorrection eta S s 1 (1/6)}, not a freely chosen auxiliary numerator. \src{C13}{\fid{PrincipalMellinResidues.lean}, \fid{source_double_residue}; \fid{AngularPhysicalPrincipalResidueBound.lean}, lines 19--34; \fid{AngularPhysicalPrincipalNormalized.lean}, \fid{actual_ray_principal_comparison}.} Put \(a_{\min}=(5/6)p.r_{\min}\), and define the actual signal saving by \begin{equation}\label{eq:sigma} e_{\mathrm{pr}}=\min(a_{\min}/8,1/2000),\qquad \sigma=\min(p.\mathrm{saving},a_{\min}/4)>0. \end{equation} The principal-pool comparison contributes the two powers \[ Z^{\beta_n-11/16-17/48000+p.\mathrm{normalizerLoss}},\qquad Z^{\beta_n-11/16+e_{\mathrm{pr}}-(7/8)a_{\min}}. \] The parameter budget proves \[ p.\mathrm{normalizerLoss}+\sigma\le17/48000,\qquad e_{\mathrm{pr}}+\sigma\le(7/8)a_{\min}. \] Together with \(\sigma\le p.\mathrm{saving}\), these inequalities allow all three errors, including~\eqref{eq:detector}, to be bounded by the same power. This is the explicit numerical step joining the actual detector to the actual signal. \src{C14}{\fid{AngularPhysicalDetectorActualSignalBudget.lean}, lines 10--69; \fid{AngularPhysicalDetectorActualSignalContraction.lean}, lines 100--132.} \begin{proposition}[Common-signal estimate]\label{prop:high} For the fixed witnesses used in the final assembly there is a \(\sigma>0\), chosen before the target \(\eta\) of order \(-n\), such that \begin{equation}\label{eq:high} J_\eta(Z)-f_\eta(Z) =O_\eta\bigl(Z^{\beta_n-11/16-\sigma}\bigr). \end{equation} Here \(f_\eta\) is the signal of Section~\ref{sec:mellin} for the actual excluded character \(\eta_S\), with correction \(H_\eta\). The low bound in Proposition~\ref{prop:low} applies to this same \(J_\eta\). \end{proposition} The final constant has the form \(C_{\mathrm{det}}(\Nm\mathfrak m_\eta)^2+2C_{\mathrm{pr},\eta}\). Its dependence on the target is compatible with a common saving \(\sigma\). \src{C15}{\fid{AngularPhysicalDetectorActualSignalContraction.lean}, lines 29--65 and 114--132; \fid{AngularPhysicalFinalAssembly.lean}, lines 67--104.} \section{From the common signal to analytic nonvanishing}\label{sec:mellin} Let \(\eta_S\) be the source character obtained by excluding the fixed primes \(S\). Its angular order is still \(-n\ne0\). Put \(c=-11/16\). On the absolute-convergence half-plane define the amplitude \[ \mathcal A_\eta(s)=e^{(s-5/6)^2}\frac{H_\eta(s)}{L(\eta_S,s)}. \] For \(x>0\), the source's inverse Mellin convention gives \begin{equation}\label{eq:signal} f_\eta(x)=\frac1{2\pi}\int_{\R} x^{2+it+c}e^{(2+it-5/6)^2} \frac{H_\eta(2+it)}{L(\eta_S,2+it)}\dd t. \end{equation} This integral is defined on the fixed line \(\Rea s=2\), where nonvanishing already follows from the Euler product. Its construction therefore does not presuppose the improved half-plane. \src{C16}{\fid{AngularPhysicalSignal.lean}, lines 17--24, 56--72, and 92--112; \fid{AngularPhysicalSignalIdentity.lean}, lines 86--94.} \subsection{The Mellin implication in detail} On a vertical line, the Gaussian multiplier has modulus \(e^{(a-5/6)^2-t^2}\). The source proves the associated integrability, continuity on \(x>0\), and rapid decay as \(x\downarrow0\). For the last property, move the line in~\eqref{eq:signal} to any \(\Rea s=B\ge2\); the right-half-plane reciprocal bound and Gaussian decay give \(f_\eta(x)=O(x^{B+c})\) on \(00,\qquad a=\beta_n-\delta=\max(7/8+\omega,\beta_n-\sigma). \end{equation} The triangle inequality gives \(f_\eta(x)=O(x^{a+c})\). Local integrability, this bound at infinity, and rapid decay at zero make \begin{equation}\label{eq:transform} F_\eta(s)=\int_0^\infty f_\eta(x)x^{-s-c}\frac{\dd x}{x} \end{equation} holomorphic for \(\Rea s>a\). For example, on a compact subset of that half-plane, the tail is bounded by \(x^{-1-\epsilon}\) for some \(\epsilon>0\); the same domination after logarithmic factors justifies complex differentiation. The lower endpoint is handled by the arbitrary power decay. Mellin/Fourier inversion identifies \(F_\eta(s)=\mathcal A_\eta(s)\) first on the line used to define the signal and then, by analytic uniqueness, on \(\Rea s>\max(a,1)\). Since \(\eta_S\) has nonzero angular order, its continued \(L\)-function is holomorphic. Hence the product identity \begin{equation}\label{eq:product} L(\eta_S,s)F_\eta(s)=e^{(s-5/6)^2}H_\eta(s) \end{equation} continues to all of \(\Rea s>a\). Here \(a>7/8\), so the right-hand side is nonzero by~\eqref{eq:H}. A zero of \(L(\eta_S,s)\) would make the left-hand side zero, a contradiction. Thus \begin{equation}\label{eq:excludedfree} L(\eta_S,s)\ne0\qquad(\Rea s>\beta_n-\delta). \end{equation} This argument continues a holomorphic product; it does not assume that the reciprocal was already holomorphic in the new strip. \src{C17}{\fid{AngularPhysicalSignal.lean}, \fid{signal_rapidDecayAtZero}, \fid{signal_locallyIntegrable}, and \fid{signalMellin_eq_amplitude_on_line}; \fid{AngularPhysicalSignalIdentity.lean}, lines 29--94; \fid{OAI/NumberTheory/DirichletL/Continuation.lean}, lines 15--75; \fid{OAI/NumberTheory/DirichletL/Supremum.lean}, lines 10--48.} \subsection{Returning from the excluded character} The source proves, first by the series in \(\Rea s>1\) and then by analytic continuation for nonzero order, the exact identity \begin{equation}\label{eq:deletion} L(\eta_S,s)=L(\eta,s)\prod_{\mathfrak p\mid\mathfrak m_{\eta_S}} \bigl(1-\eta(\mathfrak p)(\Nm\mathfrak p)^{-s}\bigr) \qquad(\Rea s>0). \end{equation} Original modulus primes have coefficient zero and contribute factor one. For nonvanishing transfer in the direction needed here, the product identity already suffices: a zero of \(L(\eta,s)\) would be a zero of \(L(\eta_S,s)\). The finite factors are also nonzero for \(\Rea s>0\), by the norm bound on the coefficients. The final source proof uses the first, direct implication. Combining~\eqref{eq:excludedfree} and~\eqref{eq:deletion} establishes~\eqref{eq:improvement}. \src{C18}{\fid{AngularPhysicalAnalyticDeletion.lean}, \fid{factors_eq}, \fid{LFunction_eq_of_mask_nonzero_order}, and \fid{nonzero_of_excluded}; \fid{AngularPhysicalFinalAssembly.lean}, lines 105--113.} \section{Finite-cap closure and the full family}\label{sec:closure} We give the final induction, since it shows precisely why a common margin was needed. At \(n=0\), the source identifies the actual angular type-zero function with the appropriate finite-character continuation. It then invokes the pinned OAI-003 \(7/8\) theorem. Principal type zero excludes its pole; the nonprincipal value at one is included through the separate entire identification. Consequently \(\beta_0\le7/8\). \src{C19}{\fid{AngularPhysicalCapClosure.lean}, lines 16--35; \fid{OAI/NumberTheory/DirichletL/Hecke/Nonvanishing.lean}, public finite-family theorem.} Suppose \(\beta_{n-1}\le7/8\), with \(n>0\). If \(\beta_n>7/8\), the preceding construction supplies \(\delta>0\) for every order \(-n\) character. Conjugation gives the same assertion for order \(+n\), using \[ L(\overline\chi,\overline s)=\overline{L(\chi,s)}, \qquad k_{\overline\chi}=-k_\chi. \] Conjugation preserves the real part of the potential zero. Put \[ d=\min\bigl(\delta,(\beta_n-7/8)/2\bigr)>0. \] Zeros of the top two angular orders have real part at most \(\beta_n-\delta\le\beta_n-d\). Zeros of all smaller orders have real part at most \(7/8<\beta_n-d\). Taking the supremum, including its sentinel, therefore gives \[ \beta_n\le\max(1/2,\beta_n-d)<\beta_n, \] which is impossible. Hence \(\beta_n\le7/8\) for all \(n\). For an arbitrary admitted character choose \(n=|k_\chi|\) and apply the definition of \(\beta_n\). This proves the untwisted statement of Theorem~\ref{thm:main}; the norm-twist identities then prove its remaining assertions. \src{C20}{\fid{AngularPhysicalCapClosure.lean}, lines 45--89; \fid{AngularPhysicalZeroSupremum.lean}, lines 98--115; \fid{AngularPhysicalNormTwistNonvanishing.lean}, lines 13--48.} Three boundaries in this argument should remain distinct. Absolute convergence above one initializes the zero supremum. The correction \(H_\eta\) is controlled on the fixed half-plane above \(7/8\). The Mellin step gives the intermediate boundary \(a=\beta_n-\delta>7/8\), contradicting a proposed cap above \(7/8\). No direct estimate on the boundary line, no attained rightmost zero, and no finite-order replacement of the nonzero angular character are used. \section{Formal verification, the repair, and epistemic status}\label{sec:status} \subsection{The frozen artifact and what was replayed} The reference source is the repaired release frozen at Git commit \begin{center}\small\path{79830bf6a346a6742fde1ace977a8bb805e638e7}\end{center} with tag \fid{v7-8-2026-10-30}. The source and evidence are publicly available in the \href{https://github.com/TheRealDubb/angular-hecke-7-8-xenoproof/releases/tag/v7-8-2026-10-30}{frozen GitHub release}~\cite{Angular}. The public annotated tag resolves to that exact commit. As checked on 31 October 2026, \fid{main} is one documentation commit ahead, changing only \fid{README.md}; these later changes do not modify the tagged theorem or its verified sources. The tag was created on 30 October, and GitHub records the release's publication on 31 October 2026. The present publication pass checked the release page and public tag/comparison metadata. It did not re-download or re-hash the release assets. The exact preserved evidence archive is identified in Appendix~\ref{sec:artifacts}. This paper does not modify the frozen release. The supplied repair report records a successful clean build of 8,213 supplied source modules, including the two public roots, with 191 directly referenced toolchain modules and five packaged elaboration resources. It then records \texttt{leanchecker -{}-fresh -{}-verbose ReplayRoots} exiting with code zero after 1,648.219 seconds. The harness imports both public roots and adds no declaration; the replay checks the combined imported environment in a fresh native Lean kernel environment. This is stronger source/build evidence than the original targeted replay against historical imported objects. Separately, the public proof dependency census records 129,614 constants, no missing, unsafe or partial dependencies, and exactly the axioms \fid{propext}, \fid{Classical.choice}, and \fid{Quot.sound}. Their types were checked against their standard formulations. The number 129,614 describes the public proof dependency census; it is not asserted to be the cardinality of the entire imported environment replayed by the fresh harness. \src{V01}{Repair report, ``New checks performed independently''; \fid{VERIFICATION_RESULT.json}, \fid{KERNEL_REPLAY.json}, \fid{PublicClosureCensus.json} and its log, and \fid{StandardAxiomTypes.json}. These receipt paths are under \fid{evidence/independent_repair/clean_build/}.} The build record preserves a checked resumption: 8,211 successful fresh compilations from the first full attempt were reused only after their exact sources, imports, dependencies, compiler recipes, artifact hashes and logs were checked unchanged. The last two modules were compiled after correction. The report records 20,519 compiled artifact-part hash checks before replay. No author cached objects or historical setup/import-artifact files were admitted to that clean build. The 44,014.80 seconds reported for build attempts are a historical runtime, not an estimate for another machine. The runtime was Lean 4.34.1 at revision \begin{center}\small\path{5045d0056413266e57c625dcd7c365b10e377c52}.\end{center} The replay uses Lean's native kernel, not a separately implemented external kernel. The evidence does not establish Linux execution, official runtime binary-byte provenance, or independent buildability of archived legacy modules outside the public closure. No new Lean build or replay was performed merely to write this manuscript. \subsection{The original failure and the exact repair} The original cold-review package had an inconsistent source/import branch. At \fid{AngularSieveDensity.lean:21}, the declaration referenced \fid{AngularSieveModels.HasCanonicalThetaModels}, which was absent from the final-root environment. Line 34 also referred to the absent \fid{AngularShortEnergy.canonicalShortState_uniform_twist}. Historical successful compilation used a different \fid{AngularShortEnergy} object. Source re-elaboration reproduced the missing-name errors, and unrestricted imported-environment replay failed. An earlier timeout was inconclusive; it must not be confused with this subsequently observed error. The stale declarations did not occur in the actual public theorem's recursive proof dependencies, which passed their separate targeted replay. The defect therefore invalidated the original package's claim to a coherent source build, while the audit did not identify a mathematical failure of the public proof. Both facts belong in the record. The repair removes the import of \fid{AngularSeedNonvanishing} from \fid{AngularNormTwistContinuation}. Its only use there was the last, unused \(23/24\) corollary \fid{physical_seed_all_norm_twists}. The complete statement and proof of that corollary are preserved verbatim in the new \fid{AngularNormTwistSeedContinuation}, which retains the old import. The three public theorem/statement files are byte-identical. Of the 8,229 original Lean sources, 8,228 are byte-identical; the remaining file is split as described. Sixteen old modules leave the public import closure, but remain archived. The moved legacy module is also archived, not independently certified buildable by this repair. All eight retained continuation declarations were compared against the baseline: their types and definition/proof bodies match. \src{V02}{\fid{REPAIR_RECORD.json}; \fid{source_repair.patch}; \fid{SOURCE_PRESERVATION.json}; \fid{clean_build/CONTINUATION_SEMANTICS.json} and its log; final audit section 5 and the repair report. The repair record is at the release root; the patch, preservation file and \fid{clean_build/} directory are under \fid{evidence/independent_repair/}.} The auditor's first removal script itself failed to remove an LF-terminated import because it expected CRLF. The clean build caught that error. Explicit line removal and Lean's header-parser audit corrected it. Failed-attempt logs are retained; source/index snapshots reconstructed after a late evidence copy are labelled as such and matched to recorded hashes. The original compiler receipts are not presented as reconstructed output. This implementation error, its correction, and the checked reuse of successful fresh compilations are part of the evidence, rather than grounds to describe the run as an untouched single-pass build. \subsection{Five separate review verdicts} The final original audit and follow-up repair report give: \begin{center} \begin{tabular}{p{.59\textwidth}cc} \toprule Criterion & Original & Repaired\\\midrule Mathematical soundness & ACCEPT & ACCEPT\\ Statement and scope fidelity & ACCEPT & ACCEPT\\ Imported input applicability & ACCEPT & ACCEPT\\ Coefficients, normalization and uniformity & ACCEPT & ACCEPT\\ Verification evidence and reproducibility & REJECT & ACCEPT\\\bottomrule \end{tabular} \end{center} The first four repaired verdicts retain the baseline audit's detailed reasoning; the follow-up supplies the clean-build and fresh-replay evidence for the fifth. The original reproducibility verdict has not been retrospectively changed. The review combined source inspection, exact algebra, semantic comparison and native-kernel checks. It did not manually reread every foundational helper, all Mathlib sources, or all original Kubota/Patterson papers. These are AI-assisted audit records, not an independent human referee report. \src{V03}{\fid{ANGULAR_HECKE_7_8_FINAL_AUDIT.txt} and \fid{ANGULAR_HECKE_7_8_REPAIR_REPORT.txt}, final verdict tables and scope paragraphs.} \subsection{Authorship, AI assistance, and xenoproofs} AI systems were used extensively in the research, formalization, reconstruction, and auditing. The human author directed the research and is responsible for the submitted manuscript and its claims. AI systems are not listed as human coauthors. A separate AI-assisted reviewer and a fresh kernel replay provide different kinds of evidence; neither is independent human mathematical certification of this exposition or its conceptual account. Following the first paper, we use \emph{xenoproof} for a mathematically verified proof whose correctness can be checked independently while its essential strategy and conceptual structure are not yet adequately understood by human mathematicians. The term describes an epistemic status, not a proof's origin, length, or mere use of AI. A \emph{xenotheorem} is a theorem for which the only currently known proof is a xenoproof. These classifications are provisional: successful humanization can change them. We present this result provisionally in that category, without claiming a survey establishing that no human-understood proof exists elsewhere. This paper exposes the final common-signal deduction in ordinary mathematical language and identifies its technical inputs. That is useful progress toward human understanding, but does not certify the whole analytic development by human examination. The mathematical statements encoded in the source, the correctness of the prose reconstruction, and the suitability of a classical reference at a particular use are separate questions. The source concordance is intended to make those questions answerable. The PDF is not Lean-verified. Submission to Hexagon and hosting the release on GitHub do not themselves constitute mathematical peer review. \appendix \section{Exact source and evidence identifiers}\label{sec:artifacts} Formal module paths in this paper are relative to \fid{lean/} in the frozen release at commit \fid{79830bf6a346a6742fde1ace977a8bb805e638e7}. Short OAI paths are relative to \fid{lean/OAI/NumberTheory/DirichletL/}. The public release URL is \begin{quote}\small\url{https://github.com/TheRealDubb/angular-hecke-7-8-xenoproof/releases/tag/v7-8-2026-10-30}\end{quote} The tag identifies the frozen source, independently of later documentation updates on \fid{main}. The main theorem's full declaration is \begin{quote}\small\path{OAI.SevenEighths.Angular.PhysicalFinalAssembly.LFunction_ne_zero_of_seven_eighths_lt_re}.\end{quote} The two build/replay roots are \fid{AngularPhysicalPublicStatementCheck} and \fid{AngularPhysicalNormTwistNonvanishing}. The exact public type is: \begin{quote}\small\ttfamily theorem LFunction\_ne\_zero\_of\_seven\_eighths\_lt\_re\par \quad ($\chi$ : AngularCharacter) (s : $\C$)\par \quad (hs : (7/8 : $\R$) < s.re)\par \quad (hpole : $\chi$.k = 0 $\to$ $\chi$.residue = 1 $\to$ s $\ne$ 1) :\par \quad FamilyContinuation.LFunction $\chi$ s $\ne$ 0 \end{quote} \noindent This is a typographic transcription; the exact UTF-8 source is \fid{AngularPhysicalFinalAssembly.lean}. The preserved repaired evidence archive is \begin{quote}\small\path{ANGULAR_HECKE_7_8_REPRODUCIBILITY_REPAIRED_2026-10-29.zip}\end{quote} with SHA-256 \begin{quote}\small\path{9c1255008343d73f872cd0875a4efdef224ddd1cb0f65c432b9d3abcc5fd79e0}.\end{quote} The final original audit has SHA-256 \begin{quote}\small\path{808a5ef0bb4f219fac5a4ea67658c10aa70ba9354846bf6935c8d4032224b8a7},\end{quote} and the repair report has SHA-256 \begin{quote}\small\path{496422f8c197f320d48f6f5d682e071262c51585a757c3235a104999b84a05c6}.\end{quote} The manuscript's companion \fid{CLAIM_SOURCE_CONCORDANCE.json} records the compared source files, declarations, hashes, and audit locations. Its integrity receipt checks correspondence of those files to the frozen release; it does not claim that hashes verify a mathematical implication. OAI-003 is pinned to \fid{openai/math} revision \fid{adc7f1241b42e322a6451854ab7e4b4c146bf78a}; Mathlib is pinned to \fid{d13f23b723b8a846827a245b89c10fc7d3f11612}. The remaining dependencies, compatibility patches and actual packaged source hashes are recorded in \fid{metadata/DEPENDENCY_PINS.json} and \fid{metadata/MODULE_INDEX.json}. The source/import graph is larger than the recursive dependency graph of the public proof; the reproducibility repair illustrates why the distinction matters. \section{Reproduction and the reader's checks} The frozen release contains Python tools using only the standard library. The toolchain and compiled objects are not included in its source ZIP. After verifying the source/evidence hashes, the supplied workflow is: \begin{quote}\small\ttfamily python -B tools/rebuild\_from\_source.py -{}-plan\par python -B tools/audit\_source\_imports.py -{}-lean LEAN -{}-build-dir IMPORT\_CHECK\par python -B tools/clean\_build.py -{}-lean LEAN -{}-build-dir BUILD -{}-jobs 1\par python -B tools/replay\_clean\_build.py -{}-lean LEAN -{}-checker CHECKER -{}-build-dir BUILD \end{quote} Use the pinned Windows executables and new directories outside the source tree. \fid{REPRODUCTION.md} and \fid{REPAIR_README.txt} provide the full commands and conditions. The existing recorded run used three scheduled workers; a single worker is shown to limit memory pressure. The first command checks a build plan; it is not a theorem replay. The later commands are substantial computations and were not rerun for this manuscript. For a mathematical reading, the main checks are whether the actual family is identified correctly, whether both bounds concern precisely the same normalized probe, whether the positive saving precedes the target, and whether the Mellin product identity concerns the actual continued \(L\)-function. For a reproduction reading, distinguish source/import consistency, compiled object integrity, native kernel replay, the public proof axiom census, and semantic agreement with the intended statement. None is a substitute for all the others. \begin{thebibliography}{9} \bibitem{OAI} OpenAI, \emph{OAI-003 source development}, repository \href{https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a}{openai/math at the pinned revision}. The formal source and background manuscripts are source artifacts, not journal certification of the angular extension. \bibitem{Angular} T. Winarski, \emph{Eisenstein angular Hecke \(L\)-functions: \(7/8\) zero-free half-plane}, source and evidence release, \fid{v7-8-2026-10-30}, frozen 30 October 2026; published 31 October 2026. \url{https://github.com/TheRealDubb/angular-hecke-7-8-xenoproof/releases/tag/v7-8-2026-10-30}. Commit and evidence archive: Appendix~\ref{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. \bibitem{Previous} T. Winarski, \emph{A \(15/16\) zero-free half-plane for angular Hecke \(L\)-functions over the Eisenstein field: a mathematical reconstruction of the frozen Lean proof}, manuscript dated 21 October 2026. \href{https://github.com/TheRealDubb/angular-hecke-15-16-xenoproof/releases/tag/v15-16-2026-10-18}{Associated frozen source/evidence release}, \fid{v15-16-2026-10-18}. The manuscript date and the earlier source-release date identify distinct artifacts. \bibitem{GL} L. Goldmakher and B. Louvel, \emph{A quadratic large sieve inequality over number fields}, \href{https://arxiv.org/abs/1112.1642v2}{arXiv:1112.1642v2}, 31 May 2012. Definition 1 and Theorem 1.1 are the audited classical comparison points. \bibitem{HB} D. R. Heath-Brown, \emph{Kummer's conjecture for cubic Gauss sums}, \emph{Israel Journal of Mathematics} \textbf{120} (2000), 97--124, \href{https://doi.org/10.1007/s11856-000-1273-y}{doi:10.1007/s11856-000-1273-y}. The audit compares Theorem 2 with the Eisenstein cubic sieve application. \bibitem{DR} A. Dunn and M. Radziwi\l\l, \emph{Bias in cubic Gauss sums: Patterson's conjecture}, \href{https://arxiv.org/abs/2109.07463v3}{arXiv: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. \bibitem{DLMF} NIST Digital Library of Mathematical Functions, \href{https://dlmf.nist.gov/10.43.E19}{equation 10.43.19}, the K-Bessel Mellin integral convention compared in the final audit. \end{thebibliography} \end{document}