\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage[T1]{fontenc}
\usepackage{lmodern,amsmath,amssymb,amsthm,mathtools}
\usepackage{booktabs,longtable,array,enumitem,microtype,xcolor}
\usepackage{xurl}
\usepackage[unicode,colorlinks=true,linkcolor=blue!45!black,citecolor=blue!45!black,urlcolor=blue!45!black]{hyperref}
\hypersetup{pdftitle={A 15/16 zero-free half-plane for angular Hecke L-functions over the Eisenstein field},pdfauthor={Troy Winarski},pdfsubject={A mathematical reconstruction of the frozen 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{\frakp}{\mathfrak p}
\newcommand{\fraka}{\mathfrak a}
\newcommand{\frakb}{\mathfrak b}
\newcommand{\frakd}{\mathfrak d}
\newcommand{\frakf}{\mathfrak f}
\newcommand{\frakq}{\mathfrak q}
\newcommand{\frakh}{\mathfrak h}
\newcommand{\frakk}{\mathfrak k}
\newcommand{\frakj}{\mathfrak j}
\newcommand{\supp}{\operatorname{supp}}
\newcommand{\Rea}{\operatorname{Re}}
\newcommand{\Ima}{\operatorname{Im}}
\newcommand{\ee}{\mathrm e}
\newcommand{\dd}{\,\mathrm d}
\newcommand{\abs}[1]{\left|#1\right|}
% Each source identifier is kept intact; semicolon-separated entries get their own lines.
\newcommand{\sourceid}[1]{\mbox{\fontsize{8.5}{10.5}\selectfont\ttfamily\detokenize{#1}}}
\ExplSyntaxOn
\NewDocumentCommand{\src}{m}{
  \par\smallskip
  \group_begin:
  \footnotesize
  \noindent\textit{Source~correspondence.}\par\nobreak
  \seq_set_split:Nnn \l_tmpa_seq { ; } { #1 }
  \seq_map_inline:Nn \l_tmpa_seq {
    \noindent\hspace*{1em}
    \exp_args:Ne \sourceid { \tl_trim_spaces:n { ##1 } }\par\nobreak
  }
  \group_end:
  \smallskip
}
\ExplSyntaxOff
\newcommand{\technical}{\textit{Technical source lemma.}}
\setlength{\emergencystretch}{2em}
\setlist{itemsep=3pt,topsep=5pt}
\numberwithin{equation}{section}
\title{A \(15/16\) zero-free half-plane for angular Hecke \(L\)-functions over the Eisenstein field\\[5pt]
\large A mathematical reconstruction of the frozen Lean proof}
\author{Troy Winarski\\[2pt]
\small Independent researcher\\
\small ORCID: \href{https://orcid.org/0009-0004-5956-3825}{0009-0004-5956-3825}}
\date{21 October 2026}
\begin{document}
\maketitle
\begin{abstract}
We describe the argument recorded in a frozen Lean development for nonvanishing of the unitary angular Hecke \(L\)-functions over \(\mathbb Q(\sqrt{-3})\) in \(\Rea s>15/16\), apart from the principal pole. The family includes imprimitive finite parts and every integer angular type allowed by the unit relation, and hence also real norm twists. The route passes through a mean-square estimate for the actual sextic rows, averaging on sixth powers, a smoothed M\"obius estimate with a totient factor, and Mellin continuation. We explain the angular reflection, the finite energy descent, and the calculation of the exponent. Technical arithmetic lemmas inherited from OAI-003 are stated with their roles and source locations; the longer finite decompositions are described rather than reproduced line by line. This is an expository reconstruction, not a claim of independent human certification. Its purpose is to make the mathematical content, including the source lemmas requiring examination, accessible to a professional reader. The formally verified proof is described here as a \emph{xenoproof}, and the theorem provisionally as a \emph{xenotheorem}; Section~\ref{sec:xeno} defines these terms.
\end{abstract}
\tableofcontents

% BEGIN 01_statement
\section{The statement and the meaning of the family}\label{sec:statement}

Put $K=\mathbb Q(\sqrt{-3})$, $\omega=(-1+\sqrt{-3})/2$, and $\OO=\mathbb Z[\omega]$. Fix the embedding $\iota:K\hookrightarrow\C$ with $\iota(\omega)=\exp(2\pi i/3)$. For a nonzero element $a$ and a nonzero integral ideal $\fraka$, write
\[
 \Nm(a)=|\iota(a)|^2,\qquad \Nm\fraka=|\OO/\fraka|,
 \qquad \alpha(a)=\frac{\iota(a)}{|\iota(a)|}.
\]
The ring $\OO$ is a principal ideal domain, and its unit group has six elements. We extend finite multiplicative characters by zero on nonunits of their residue ring.

\begin{definition}[Admitted angular character]\label{def:character}
An angular character is a triple $\chi=(k,\frakf,\xi)$, where $k\in\Z$, $\frakf$ is a nonzero integral ideal, and $\xi$ is a multiplicative character of $\OO/\frakf$, subject to
\begin{equation}\label{eq:units}
 \alpha(u)^k\xi(u\bmod\frakf)=1\qquad(u\in\OO^\times).
\end{equation}
Set $c_\chi(0)=0$ and $c_\chi(a)=\alpha(a)^k\xi(a\bmod\frakf)$ for $a\ne0$. The associated ideal coefficient is $\chi((a))=c_\chi(a)$.
\end{definition}

The unit equation makes the last definition independent of the generator: replacing $a$ by $ua$ multiplies the proposed value by the left side of \eqref{eq:units}. Multiplicativity follows from that of $\alpha$ and $\xi$. In particular $|\chi(\fraka)|\le1$, and the coefficient is zero if $\fraka$ is not coprime to $\frakf$. ``Every angular type'' below means every triple satisfying \eqref{eq:units}; it does not mean that an arbitrary finite character can be paired with an arbitrary integer.

The condition can be read as a compatibility test on a finite group. On the six units, $\alpha(u)=\iota(u)$ is a sixth root of unity. Thus the restriction of $\xi$ must be the inverse of the restriction of $\alpha^k$. If two units have the same residue modulo $\frakf$, their prescribed values must agree; this is a real restriction on the available pairs $(k,\frakf)$. In particular, if the finite character is principal, compatibility forces $6\mid k$. A nonprincipal finite part can compensate a different unit phase. No choice of a preferred generator is needed for the final ideal character: the equation makes \emph{every} generator give the same value.

Conjugation respects this condition. The conjugate character has data $(-k,\frakf,\overline\xi)$ and coefficient $\overline{c_\chi(a)}$, since $|\alpha(a)|=1$ for $a\ne0$. This explains why conjugation is available for the final family, but does not yet prove that a row estimate involving an additional fixed sextic character is invariant under it. That distinction will determine the order of the proof.
\src{AngularCharacter; AngularFamilyConjugation.LFunction_conjugate}

For $\Rea s>1$ the physical Dirichlet series is
\begin{equation}\label{eq:series}
 L(\chi,s)=\sum_{\fraka\ne0}\frac{\chi(\fraka)}{(\Nm\fraka)^s}
 =\prod_{\frakp}\left(1-\frac{\chi(\frakp)}{(\Nm\frakp)^s}\right)^{-1}.
\end{equation}
Positive real powers use the real logarithm. We use the same notation for its analytic continuation. An imprimitive finite part retains the Euler-factor deletions in \eqref{eq:series}. The principal case is $k=0$ and $\xi=1$, where $1$ denotes the principal finite character, including its zero values on nonunits.

\begin{theorem}[The frozen public statement]\label{thm:main}
For every admitted angular character $\chi$, one has
\[
 L(\chi,s)\ne0\qquad\text{if }\Rea s>\frac{15}{16},
\]
with $s=1$ excluded in the principal case. For $\tau\in\R$, define $\chi_\tau(\fraka)=\chi(\fraka)(\Nm\fraka)^{i\tau}$. Then
\[
 L(\chi_\tau,s)\ne0\qquad\text{if }\Rea s>\frac{15}{16},
\]
with $s=1+i\tau$ excluded in the principal case.
\end{theorem}

There is no angular-order cutoff, finite-conductor bound, or primitivity assumption. There is no assertion on the line $\Rea s=15/16$. The result is qualitative for each character: estimates in this paper may have constants depending on $k$ and $\frakf$. No effective estimate uniform as those parameters grow is asserted. The theorem concerns this family over this field, not all number fields. It asserts neither RH nor GRH, and makes no optimality claim.

\subsection{How to read this reconstruction}
The mathematical route is
\[
\begin{gathered}
\text{actual angular theta reflection}\longrightarrow
\text{quadratic row energy}\longrightarrow
\text{finite energy descent}\\
\Downarrow\\
\text{sextic mean square}\longrightarrow
\text{sixth-power averaging}\longrightarrow
\text{M\"obius cancellation}\\
\Downarrow\\
\text{Mellin identity}\longrightarrow L(\chi,s)\ne0.
\end{gathered}
\]
Sections~\ref{sec:average} and \ref{sec:mellin} give the final deduction in detail. Sections~\ref{sec:reflection}--\ref{sec:descent} explain the machinery supplying its principal input. Reading the final deduction first is a useful way to see exactly what the earlier machinery must prove.

The source is the frozen release identified in Appendix~\ref{sec:concordance}. A source reference after a proposition identifies the formal declaration or module whose mathematics is being described. Some long arithmetic decompositions are explicitly designated technical source lemmas. Their statements and proof mechanisms are exposed here, but their full finite bookkeeping remains in the cited source. Consequently this manuscript is a guide for converting the formal development into an independently checked mathematical proof, rather than a claim that every line of the inherited development has already received a new human proof. The distinction applies to this exposition; it is not an extra hypothesis in the public Lean theorem.

We distinguish three kinds of support. An argument \emph{explained here} is a mathematical deduction supplied in the text, sometimes from a stated technical input. An \emph{inherited formal input} is a theorem about specified objects in the frozen source whose full proof is not reproduced here. A \emph{literature reference} supplies the stated classical background or a separately identified classical result; it does not automatically identify the source's concrete objects. Appendix~\ref{sec:interfaces} collects the interfaces, the hypotheses checked at their uses, and the remaining independent checks. This distinction is especially important for the reflection identity and the quadratic-row estimate.

\subsection{Analytic continuation and its normalization}
The continuation in the source is tied to \eqref{eq:series}, rather than introduced as an abstract function with a functional equation. For $k\ge0$ the elementary identity
\[
 \alpha(a)^k\Nm(a)^{-s}=\iota(a)^k\Nm(a)^{-s-k/2}
\]
turns the problem into the Mellin transform of a polynomial times a Gaussian on the Eisenstein lattice, twisted by a finite residue character. Negative $k$ uses the conjugate polynomial. Poisson summation supplies the theta transformation. Removing the finite Euler factors for an imprimitive character produces the continuation of exactly \eqref{eq:series}. The division by the six units is accounted for when element sums are converted to ideal sums.

For $k\ne0$ the continuation is entire. For $k=0$, $(s-1)L(\chi,s)$ has the holomorphic regularization needed below; for a nonprincipal finite character the function itself is entire and the classical Hecke nonvanishing theorem gives $L(\chi,1)\ne0$. These are statements about the actual family. In the Lean development the connection to the series, the continuation, and this value at one are established by separate declarations, listed in the concordance. The finite-character nonvanishing theorem at one is used only for this boundary case; the improved half-plane is supplied by the argument below.
\src{AngularCharacter; AngularFamilyContinuation.LFunction_eq_series; AngularTypeZeroEntire; AngularNormTwistContinuation}

% END 01_statement


% BEGIN 02_rows
\section{The physical rows and the estimate that is needed}\label{sec:rows}

For the physical mean square and its application in Section~\ref{sec:average}, fix an admitted character $\chi$ of type $k=n$ with $n\in\N$. The reflection in Sections~\ref{sec:reflection}--\ref{sec:descent} is applied to its conjugated coefficient, of type $-n$. The negative types in Theorem~\ref{thm:main} will be obtained at the $L$-function stage in Section~\ref{sec:mellin}.

Let $S$ be a finite set of prime ideals containing the fixed bad primes of the sextic construction, including the primes above $2$ and $3$, and the additional fixed primes required by the conjugate character's reflection conductor. All subsequent sums ``outside $S$'' are restricted to ideals coprime to $\prod_{\frakp\in S}\frakp$.

For a good prime $\frakp$, let $\rho_{\frakp}$ be the sextic residue character, with the choice of the complex sixth roots of unity fixed by the source embedding. It has absolute value one on nonzero residue classes and is zero at zero. For a squarefree ideal outside $S$, set
\begin{equation}\label{eq:row}
 R_{\fraka}(z)=\prod_{\frakp\mid\fraka}\rho_{\frakp}(z\bmod\frakp).
\end{equation}
The empty product is one. The two identities that motivate the construction are
\begin{equation}\label{eq:sixth}
 |R_{\fraka}(z)|\le1,\qquad
 R_{\fraka}(b^6)=\boldsymbol1_{(\fraka,(b))=1}.
\end{equation}
Indeed, a sixth power has sextic character one unless its residue is zero. The same local character has a cubic part $\rho_{\frakp}^2$ and a quadratic part $\rho_{\frakp}^3$. This gives a concrete bridge between cubic Gauss coefficients and a quadratic mean-square estimate.

Let $\mu_K$ be the ideal M\"obius function. Given $W\in C_c^\infty((0,\infty))$ with support in $[a,b]$, $0<a<b$, define
\begin{equation}\label{eq:AZ}
 A_Z(z)=\sum_{\substack{\fraka\text{ outside }S}}
 \mu_K(\fraka)\chi(\fraka)
 W\left(\frac{\Nm\fraka}{Z}\right)R_{\fraka}(z).
\end{equation}
Only squarefree ideals matter. The sum is finite; equivalently one may impose $\Nm\fraka\le D$ for any integer $D\ge bZ$. In particular the coefficients in \eqref{eq:AZ} are the actual M\"obius and character coefficients. They are not an arbitrary independently chosen array for each row $z$.

\begin{proposition}[Physical mean square]\label{prop:ms}
For each fixed admitted $\chi$ with $k=n$, $n\in\N$, and each fixed $W$, there is a fixed set $S$ as above such that for every $\sigma>1/20$ and $\varepsilon>0$ there is $C>0$ satisfying
\begin{equation}\label{eq:ms}
 \sum_{z\in T}|A_Z(z)|^2
 \le C Z^{2+\sigma+\varepsilon}\qquad(Z\ge1)
\end{equation}
for every finite $T\subset\OO\setminus\{0\}$ with $\Nm(z)\le Z^{1+\sigma}$ for all $z\in T$. The constant is independent of $T,Z$, and of the harmless cutoff $D\ge bZ$.
\end{proposition}

The premise called initial canonical density in the intermediate source theorem is discharged by the physical construction. Sections~\ref{sec:reflection}--\ref{sec:descent} explain this discharge. The physical mean-square declaration requires $k=n$, $n\in\N$. Its proof applies the initial-density theorem of type $-n$ to $\overline\chi$, the conjugated base coefficient arising in the square of \eqref{eq:AZ}. No extension of this sextic-row estimate to negative $k$ by conjugation is asserted. Thus its use here does not assume that a formal model is automatically realized by the coefficients of $L(\chi,s)$.
\src{AngularPoissonMoment.physical_outside_mean_square; AngularPoissonMoment.outside_mean_square_of_canonical_density_at_radius; AngularInitialDensity.physical_initial_density; AngularPhysicalSieveEnergy}

\subsection{Why the estimate is useful}
The trivial estimate for one row loses essentially the whole number of ideals, of order $Z$. Proposition~\ref{prop:ms} says that the average square has the scale expected of a square-root cancellation bound, with a small loss. It is a statement about many rows at once; it need not give a good bound at any prescribed row. Sampling the special rows $z=b^6$ will convert this averaged information into cancellation in a single smoothed M\"obius sum.

The count of Eisenstein lattice points in $\Nm(b)\le Y$ is $O(Y)$, because the norm is the square of the Euclidean radius. There are at most six nonzero solutions to $b^6=z$ in the field. Both facts are needed in the Cauchy--Schwarz argument. Treating $b\mapsto b^6$ as injective would omit a genuine multiplicity, even though it would not change the exponent.

\subsection{Notation used in the technical part}
The auxiliary scales have distinct roles: $Z$ is the global scale; $X$ is a column norm scale; $F$ bounds label-ideal norms; $K$ bounds row norms; $m$ is a nonzero element imposing additional coprimality conditions; and $t\in\R$ is a height introduced by Mellin or Fourier separation. These auxiliary coefficients need not themselves be the final unit-invariant ideal character. They are explicit element coefficients obtained from it by residue twists and row twists. The finite orbit used in the descent is closed under the operations that occur there.

% END 02_rows


% BEGIN 03_reflection
\section{Angular reflection: where the infinite type enters}\label{sec:reflection}

\subsection{Completing the cubic coefficient}
Fix the source's multiplicative choice $g(\fraka)$ of primary generators on ideals away from the prime above $3$. Extend $g$ by zero on ideals divisible by that prime, and put $\alpha(0)=0$ for the auxiliary formulas in this section. At a squarefree ideal away from $3$ let
\[
 G_2(\fraka)=\frac1{\sqrt{\Nm\fraka}}
 \sum_{x\bmod\fraka}R_{\fraka}(x)^2\,e_{\fraka}(x),
 \qquad c(\fraka)=\overline{\alpha(g(\fraka))}\,G_2(\fraka),
\]
where $R_{\fraka}$ here uses the same source sextic characters at all primes away from $3$, including the prime above $2$. The additional exclusion of $2$ belongs to the quadratic-row ranges and masks, not to the definition of the unmasked completed sum. The additive character $e_{\fraka}$ comes from the fixed trace pairing and $g(\fraka)$. Its sign and trace convention are those of the pinned source's \texttt{eisTraceModChar}; changing that convention without changing the theta coefficients would change the reflection identity. Set $c(\fraka)=0$ outside the squarefree supported range. For an element coefficient $\Psi$, put
\begin{align*}
 c_\Psi(\fraka)&=c(\fraka)\Psi(g(\fraka)),\\
 b_\Psi(\frakb)&=\frac{\overline{\alpha(g(\frakb))}^{\,3}
                           \Psi(g(\frakb))^3}{\Nm\frakb},
 \qquad V_W(x)=\sqrt{x}\,W(x).
\end{align*}
The completed sum is
\begin{equation}\label{eq:completed}
 T_\Psi(W;X)=\sum_{\fraka,\frakb\ne0}
 \frac{c_\Psi(\fraka)}{\sqrt{\Nm\fraka}}\,
 b_\Psi(\frakb)\,
 V_W\left(\frac{\Nm\fraka(\Nm\frakb)^3}{X}\right).
\end{equation}
Compact support makes this a finite sum for each positive $X$. The cube variable is part of the theta coefficient. It cannot be suppressed merely because the original M\"obius sum is squarefree.

There are two generator conventions in the source, and we keep them separate. The symbol $g$ in these coefficients denotes the fixed multiplicative primary choice. Write $g_0(I)$ for the arbitrary fixed principal generator called \texttt{ConcretePrimeRowBridge.idealGenerator}; it satisfies $(g_0(I))=I$, but is not asserted to be multiplicative. Label and mask representatives below use $g_0$. Changing a label representative by a unit can change an auxiliary row, so the six unit sectors are retained when the source reindexes those labels. The final ideal character is unit-invariant; the auxiliary element rows need not be.

The factors in \eqref{eq:completed} serve different purposes. The $\sqrt{\Nm\fraka}$ in the Gauss normalization removes its natural square-root size. The phase $\overline{\alpha(g(\fraka))}$ matches the order-one differentiated theta coefficient. The factor $(\Nm\frakb)^{-1}$ and the cube in $\Psi(g(\frakb))^3$ encode the cube part of the Fourier index. Finally $V_W=\sqrt{x}W$ is the smoothing normalization that connects the theta expansion to a column sum of size $X$. None of these factors is chosen after reflection to improve an exponent.

For later use its short M\"obius inversion is
\begin{equation}\label{eq:short}
 T_\Psi^{<H}(W;X)=\sum_{\Nm\frakh<H}\mu_K(\frakh)b_\Psi(\frakh)
                   T_\Psi\left(W;\frac{X}{(\Nm\frakh)^3}\right),
\end{equation}
where $\frakh$ denotes a nonzero ideal. This is the quantity called \texttt{shortCompletedSum}. Its complement, with large cube variable, is reopened into smaller-rank states in Section~\ref{sec:descent}.
\src{Arithmetic/IdealMobius.completedT; QuadraticSieve/ProductColumns.shortCompletedSum}

\subsection{Differentiation supplies the angular phase}
The cubic residual theta function has Fourier coefficients related to normalized cubic Gauss sums. Patterson's construction is the classical background \cite{Patterson}; the explicit level-aspect cubic Voronoi framework of Dunn and Radziwi\l\l{} is related background \cite{DR}. Here the precise identities used are the identities reconstructed in the pinned source, with its cusp and trace normalizations. Neither reference is being cited as a theorem directly asserting the angular estimate needed in this paper.

Consider a physical coefficient with type $-n$, $n\ge0$. A Fourier mode of frequency $a$ acquires a factor proportional to $\overline{\iota(a)}$ under an antiholomorphic derivative. Relative to the already differentiated order-one theta coefficient, $n$ further derivatives supply
\begin{equation}\label{eq:derivphase}
 (-2\pi i\,\overline{\vartheta\iota(a)})^n
 =(-2\pi i\,\overline\vartheta)^n
     \alpha(a)^{-n}\Nm(a)^{n/2}.
\end{equation}
Here $\vartheta$ is the fixed nonzero frequency scale. At a completed theta index $a=g(\fraka)g(\frakb)^3$, the radial factor is
\[
 \Nm(a)^{n/2}=\bigl(\Nm\fraka(\Nm\frakb)^3\bigr)^{n/2}.
\]
This is absorbed by the shifted Mellin normalization. The remaining phase is exactly the required angular factor. The total derivative order is $n+1$, not $n$.

Only the finite part $\xi$ is expanded on a residue quotient. If a nonzero $c$ is chosen with $(c)\subseteq(9)\frakf$, finite additive Fourier inversion on $\OO/(c)$ represents the periodic coefficient as a finite sum of additive twists. The factor $\alpha(a)^{-n}$ is supplied by \eqref{eq:derivphase}; it is not a periodic function that can be silently included in that finite Fourier inversion.
\src{AngularCompletedCoefficient; AngularFiniteProjector; AngularHigherProfiles}

\subsection{Reflection at an actual cusp}
A cusp datum $d$ consists of the source's cusp representative and a matrix with lower-left entry $c_d\ne0$. Write $H_d=|c_d|^2$. The differentiated profile at its finite cusp and the corresponding dual profile satisfy, for $v>0$ and integer $r\ge1$,
\begin{equation}\label{eq:cusp}
 \Phi_{r,d}(v)=m_{r,d}v^{-2r}
            \Phi^*_{r,d}\left(\frac1{H_dv}\right),
 \qquad
 m_{r,d}=\frac{\overline{\epsilon_2(\gamma_d)}(-1)^r}{c_d^{2r}}.
\end{equation}
The multiplier $\epsilon_2$ is the actual level-two Kubota character in the source. One cannot replace it by a level-three character by assuming a smaller transformation group. The three cusp scales are $s_j=1,3,3$; their factors remain in the formulas.

At the infinite cusp, every constant Fourier mode is killed by a positive-order horizontal derivative. The differentiated Fourier series has rapid decay. Equation~\eqref{eq:cusp} then transfers this decay to the other endpoint, including the explicit power of $v$ and height $H_d$. The Mellin transform of the differentiated profile is therefore entire; reflection of the integral follows by the substitution $v\mapsto1/(H_dv)$. The finite additive projector is a finite linear combination of these identities, including its zero additive character.

This explains the treatment of the smallest types. For $n=0$ the derivative order is one; for $n=1$ it is two. Both are positive. The argument removes the constant mode before taking the Mellin transform. Thus the absence of an exceptional residue at $k=\pm1$ is based on the physical differentiated cusp profiles, not on a formal cancellation of two gamma symbols alone.
\src{AngularProjectedReflection.datum_reflection; finiteProjector_mellin_reflection; AngularHigherMellin}

\subsection{The shifted Mellin kernel}
Put $a_n=n/2+7/6$, $b_n=n/2+5/6$. The multiplier and its reflected kernel are
\begin{align}
 \mathcal G_n(s)&=\frac{\Gamma(a_n+s)\Gamma(b_n+s)}
                         {\Gamma(a_n-s)\Gamma(b_n-s)},\label{eq:gamma}\\
 \mathcal K_n[V](x)&=\frac1{2\pi i}\int_{(0)}
     \widehat V(-s)\mathcal G_n(s)
          \left(\frac{(2\pi)^4x}{27}\right)^{-s}\dd s,
     \qquad x>0.\label{eq:kernel}
\end{align}
For complex arguments the quotient in \eqref{eq:gamma} is understood using the entire reciprocal gamma function. Poles of the denominator gamma functions are therefore zeros of the multiplier, not poles to cross. The multiplier is holomorphic for $\Rea s>-b_n$ and satisfies
\[
 \mathcal G_n(-s)\mathcal G_n(s)=1
\]
where both sides are defined by nonzero ordinary gamma values. On the imaginary axis $|\mathcal G_n(it)|=1$, by conjugation of the gamma function. On a fixed strip $-1/4\le\Rea s\le A$ it has at most polynomial growth in $|\Ima s|$, with constants allowed to depend on $n,A$.

The Mellin transform of a smooth compactly supported $V$ decays faster than every power on vertical lines. Consequently \eqref{eq:kernel} is absolutely convergent, can be differentiated by $x\,d/dx$, and its contour may be moved to any fixed positive line. For each $A,j\ge0$,
\begin{equation}\label{eq:kerneldecay}
 \left|\left(x\frac d{dx}\right)^j\mathcal K_n[V](x)\right|
 \ll_{n,A,j,V}(1+x)^{-A}.
\end{equation}
The implied constant can be bounded by finitely many Schwartz seminorms of $u\mapsto V(e^u)$. Moving to a small negative line also supplies a positive power of $x$ at zero. These contour arguments use actual integrable majorants; a purely algebraic gamma identity would not be sufficient.
\src{AngularGammaMultiplier; AngularReflectedKernel; AngularKernelContour}

\subsection{What the exact smoothed identity says}
It is useful to display the normalizations that are easy to lose in an informal reflection. Let $B=|\vartheta|=1/\sqrt{27}$, let $B_j=B/s_j$, and let $\Delta\ne0$ be the source's initial derivative scalar. Let $C_{j,z}(h)$ denote the fixed order-one radial Fourier coefficient at the dual cusp. It includes its additive phase. Let $\ell(h)=\Nm(h)$ for $h\ne0$; the source sets $\ell(0)=1$ to totalize the formula, while the differentiated coefficient there is zero. Let $e_j$ denote its additional derivative scalar, whose norm is $|2\pi\vartheta|/s_j$.

Define the explicitly normalized dual expression
\begin{align}
 \mathcal D_{n,d}(V;X)
 ={}&m_{n+1,d}H_d^{n+1}(B/B_j)^{n+2}\nonumber\\
 &\quad\times\sum_{h\in\OO}C_{j,z_d^*}(h)e_j^n\alpha(h)^n
 \mathcal K_n[V]\left(\frac{27B^2B_j^2X\ell(h)}{H_d^2}\right).
 \label{eq:dual}
\end{align}
The zero coefficient is read as zero, regardless of the harmless convention for $\alpha(0)$. If $\widehat\xi_c(h)$ denotes the finite additive Fourier coefficient of the periodic factor, the physical identity is
\begin{equation}\label{eq:physicalreflection}
 \Delta(-2\pi i\overline\vartheta)^n T_{c_\chi}(W;X)
 =\sum_{h\bmod c}\widehat\xi_c(h)\,
            \mathcal D_{n,d(h)}(V_W;X).
\end{equation}
The source defines $C_{j,z}$ and $e_j$ through its fixed cusp Fourier expansion; they are not free coefficients or adjustable constants. Equation~\eqref{eq:physicalreflection} is the technical identity connecting that expansion to \eqref{eq:completed}. Its proof matches the differentiated coefficient using \eqref{eq:derivphase}, reflects each finite additive twist by \eqref{eq:cusp}, applies the Bessel Mellin formula, and shifts the smoothing contour with the bounds just described.

The precise physical interface requires $n\in\N$, $\chi.k=-n$, $c\ne0$, $(c)\subseteq(9)\frakf$, $X>0$, and a smooth $W$ supported in $[a,b]$ with $a>0$. These conditions have direct roles. The integer $n$ gives derivative order $n+1\ge1$; the ideal inclusion makes the finite residue factor well-defined on the chosen quotient; nonzero $c$ makes that quotient finite; and support away from zero gives the Mellin decay used in contour shifting. Such a $c$ exists because the nonzero ideal $(9)\frakf$ contains a nonzero element. For the later physical row family the fixed reflection conductor is constructed to satisfy the corresponding inclusion for each finite residue factor. The cusp identity and the exact Fourier coefficient matching remain inherited formal inputs; the derivative-phase calculation and the role of their hypotheses are explained above.

There is a useful scalar check. After dividing \eqref{eq:dual} by the scalar on the left of \eqref{eq:physicalreflection}, the scalar norm is exactly $s_j^2/|\Delta|$. The height factor cancels, and so does the extra angular-order power. This cancellation concerns that scalar only. The kernel bounds still depend on $n$.
\src{AngularPhysicalSmoothedReflection.completedT_reflection; datumSmoothedDual; dualKernelTerm; datum_normalized_scalar_norm}

% END 03_reflection


% BEGIN 04_energy
\section{From reflection to quadratic energy}\label{sec:energy}

\subsection{The quadratic large-sieve interface}
The quadratic part of a good sextic row is $Q_{\frakk}(a)=R_{\frakk}(a)^3$. Its row ideal $\frakk$ is nonzero, squarefree, and supported away from $2$ and $3$. The relevant classical model is the quadratic large sieve over number fields: for a quadratic Hecke family with fixed reciprocity modulus,
\begin{equation}\label{eq:QLS}
 \sum_{\Nm\fraka\le M}^{*}
 \left|\sum_{\Nm\frakb\le N}^{*}\lambda_{\frakb}\chi_{\frakb}(\fraka)\right|^2
 \ll_{K,\mathfrak c,\varepsilon}(MN)^\varepsilon(M+N)
                 \sum_{\Nm\frakb\le N}^{*}|\lambda_{\frakb}|^2.
\end{equation}
The stars impose squarefreeness and coprimality to the fixed modulus. Goldmakher--Louvel's Theorem~1.1 \cite{GL} gives this form; Heath-Brown's quadratic inequality \cite{HB} is its classical rational-field antecedent. The reciprocity and primitive-product hypotheses of a Hecke family are part of this theorem, not consequences of the symbols merely having modulus one.

The pinned development provides the corresponding concrete Eisenstein quadratic-row inequalities and the product-column consequences needed below. Its matching of the concrete rows, reciprocity classes, masks, and repeated product columns is an arithmetic part of the proof. The citation to \cite{GL} explains the large-sieve framework; it does not by itself verify every normalization and range in this concrete application.

The actual finite-family interface in the pinned source is more useful here than an informal invocation of that citation. If $M,N\ge1$, the maps $i\mapsto I_i$ and $j\mapsto J_j$ are injective, their images are nonzero squarefree ideals away from $2$ and $3$, and $\Nm I_i\le M$, $\Nm J_j\le N$, then for arbitrary \emph{common} coefficients $a_j$ it bounds
\[
 \sum_i\left|\sum_j Q_{J_j}(g(I_i))a_j\right|^2
 \ll_\varepsilon (MN)^\varepsilon(M+N)\sum_j|a_j|^2.
\]
The source proves this through its concrete squared operator norm \texttt{sieveNorm}; the sharp bound for that norm is an inherited formal result. Finite sets supply injective enumerations automatically. Squarefreeness and exclusion of the bad primes are provided by the arithmetic decomposition, not by the analytic kernel. This is the interface used to reach the row orientation in \eqref{eq:productkernel}, through the source's conjugate-transpose and square-part reduction.

For comparison, applying Goldmakher--Louvel directly would require exhibiting a quadratic Hecke family with fixed modulus: primitive characters of trivial infinity type, a finite reciprocity-class system, and the required primitive product property for coprime indices in the same class. Modulus-one values alone do not discharge those conditions. We do not regard this paragraph as a new verification of that identification. The concrete source theorem, including its arithmetic proof, is the inherited input in this exposition; the external theorem is a description of its classical framework, not an extra unproved shortcut.
\src{QuadraticSieve/LogarithmicLoss.sieveNorm_sharp; QuadraticSieve/LogarithmicLoss.finite_family_quadratic_large_sieve; MeanSquare/TransformedColumns.bounded_supported_quadratic_norm}

\subsection{Repeated product columns and square parts}
Here is an arithmetic reduction that can be explained without hiding multiplicity in the notation. On two finite ideal sets $\mathcal A,\mathcal B$, define
\[
 b(I)=\sum_{\substack{(\fraka,\frakb)\in\mathcal A\times\mathcal B\\
                         \fraka\frakb=I}}\beta(\fraka,\frakb).
\]
Grouping by the product is an equality of finite sums. For $I\ne0$, projection onto $\fraka$ injects its product fiber into the divisors of $I$: once $\fraka$ is fixed, ideal cancellation determines $\frakb$. If $|\beta|\le L_0$, this gives $|b(I)|\le L_0\tau_K(I)$. The standard ideal-divisor bound supplies $\tau_K(I)\ll_\delta(\Nm I)^\delta$. All products have norm at most $UB_0$, so this cost is an arbitrarily small power of $UB_0$.

The products need not be squarefree. The inherited supported-column estimate permits any nonzero column ideal whose prime factors avoid $2$ and $3$. Its proof separates $I=A^2I_0$ with $I_0$ squarefree, treats the square factor as a coprimality mask in the quadratic character, and applies the sharp squarefree operator estimate on each fiber. Weighted summation over $A$ gives a small-power loss. In the exact interface, if $\Nm I\le X$, $|b(I)|\le L$, and $K,X\ge1$, then
\[
 \sum_{\substack{\Nm\frakk\le K\\\frakk\ \mathrm{admissible}}}
 \left|\sum_I Q_{\frakk}(g(I))b(I)\right|^2
 \ll_\varepsilon (KX)^\varepsilon(K+X)X L^2.
\]
Products of supported ideals remain supported, so this hypothesis is satisfied. Apply the bound with $X=UB_0$, use the divisor estimate with a smaller loss parameter, and rescale by $L_0$ to obtain the unweighted part of \eqref{eq:productkernel}. Thus collisions of product columns are accounted for before separation of the smooth kernel.
\src{QuadraticSieve/ProductColumns.product_fiber_card; productColumnCoefficient_row_sum; product_quadratic_norm; MeanSquare/TransformedColumns.bounded_supported_quadratic_norm; QuadraticSieve/DivisorBlocks.Supported}

\subsection{Separating the coupled kernel}
Reflection produces weights depending jointly on row and column variables. On compact logarithmic windows the relevant factor has the form
\[
 V_0(r)V_1(u)V_2(v)\,
 \mathcal K_n[V_W]\bigl(R\exp(-2r+u+3v)\bigr).
\]
Extend the one-variable function in $-2r+u+3v$ smoothly beyond the compact range. Fourier inversion represents it as an integral of the product
\[
 e^{-2itr}\,e^{itu}\,e^{3itv}
\]
against a coefficient $g_R(t)\dd t$ (with $2\pi$ absorbed in the Fourier variable). Bounds on two or more derivatives on that compact interval give an integrable Fourier majorant. Equation~\eqref{eq:kerneldecay} yields, for every fixed $A$,
\[
 \int_\R |g_R(t)|\dd t\ll (1+R)^{-A}.
\]
Weighted versions give polynomial-height control. The row dependence is now a factor of absolute value at most one. The remaining coefficients are common to all rows. This is what permits a quadratic large-sieve estimate to be applied under the integral.

For completeness, the analytic inequality used here is just Minkowski in a finite-dimensional Hilbert space:
\[
 \sum_k\left|\int g(t)P_k(t)\dd t\right|^2
 \le\left(\int|g(t)|\dd t\right)^2
       \sup_t\sum_k|P_k(t)|^2.
\]
All sums are finite at this stage and the integral is absolutely controlled. It would not be legitimate to replace the common column coefficients by independent coefficients chosen separately for each $k$.

One resulting estimate, in the source's normalization, is
\begin{align}\label{eq:productkernel}
 &\sum_{\substack{\Nm\frakk\le K\\\frakk\ \mathrm{admissible}}}
 \left|\sum_{\Nm\fraka\le U}\sum_{\Nm\frakb\le B_0}
 Q_{\frakk}(g(\fraka\frakb))\beta(\fraka,\frakb)
 V_0(r_{\frakk})V_1(u_{\fraka})V_2(v_{\frakb})\right.\nonumber\\[-2pt]
 &\hspace{42mm}\left.\cdot\mathcal K_n[V_W]
    (R\exp(-2r_{\frakk}+u_{\fraka}+3v_{\frakb}))\right|^2\nonumber\\
 &\hspace{15mm}\ll (KUB_0)^\varepsilon(K+UB_0)UB_0
                   L_0^2(1+R)^{-2A},
\end{align}
for $|\beta|\le L_0$ and bounded compact windows. The product-column arithmetic theorem handles the possible coincidences $\fraka\frakb=\fraka'\frakb'$; distinct pairs are not assumed to give distinct ideals. The word ``admissible'' in this display retains the squarefree and bad-prime restrictions on the row.
\src{AngularKernelEnergy.completed_smooth_quadratic; Eisenstein/DirichletForm.integrated_product_quadratic; QuadraticSieve/ProductColumns}

\subsection{The actual row family}
For an element coefficient $\Psi$ define a row twist by
\begin{equation}\label{eq:rowtwist}
 \Psi_{m,f,z}(a)=\Psi(a)R_{(a)}(m^6f^4z).
\end{equation}
Here $R_{(a)}$ uses the multiplicative extension of the prime-row values to ideals, agreeing with \eqref{eq:row} on squarefree ideals. A sixth power in the first argument imposes coprimality to $m$; the fourth power in the label and the first power in the row are retained from the finite character identities.

Fix an angular order $n$ and a finite conductor parameter $q$. Let $e_q$ generate the product of the fixed excluded primes required by that conductor. For a nonzero $m$ and squarefree label ideal $\frakf_0$, put
\[
 m_q=me_q,\qquad \frakq=(m_q)\frakf_0.
\]
The ideal $\frakq$ is a moving mask. Its norm must remain visible in every estimate until the state invariant controls it.

\begin{proposition}[Physical completed-row energy]\label{prop:completedenergy}
Fix $n,q,W$ and $\delta,\varepsilon>0$. Uniformly over angular characters of type $-n$ whose finite factor factors through the indicated fixed conductor, over $m\ne0$, squarefree $\frakf_0$, units $u$, $X,K\ge1$, and finite sets of row ideals with $K/2\le\Nm\frakj\le K$, one has
\begin{align}\label{eq:physicalenergy}
 &\sum_{\frakj}\left|T_{(c_\chi)_{m_q,g_0(\frakf_0),u g_0(\frakj)}}(W;X)\right|^2\nonumber\\
 &\hspace{8mm}\ll_{n,q,W,\delta,\varepsilon}
 (\Nm\frakq)^\varepsilon(K\Nm\frakq)^{10\delta+\varepsilon}
 \left(K+\frac{K^2\Nm\frakq}{X}\right).
\end{align}
Every fixed character of type $-n$ admits such a $q$; the source can take $q=\Nm\frakf$ before enlarging it for the finite ray orbit.
\end{proposition}

\begin{proof}[Mechanism of the source proof]
Apply the exact physical reflection \eqref{eq:physicalreflection} to every row twist. Partition the row ideals by their powerful part and by the part supported on the mask. On each such fiber the residual squarefree row map is injective. The residual oscillation is the quadratic row in \eqref{eq:productkernel}; the remaining finite coefficients are constructed from the periodic residue factor and have the required bounded norm.

There are finitely many fixed reflection rays and six local exponent choices at each prime in the factorization. Cauchy--Schwarz over these branches produces a square of the branch count. The variable prime-factor count is bounded by a small power, using $c^{\omega(\fraka)}\ll_{c,\varepsilon}(\Nm\fraka)^\varepsilon$. On a fiber, the quadratic estimate retains an inverse norm factor from the powerful part. Summing the powerful and masked parts with this weight gives the indicated small-power losses and the two scales $K$ and $K^2\Nm\frakq/X$. The fixed ray count and the exact scalar $|4\Delta^{-1}C_{\rm rad}|^2$ in the source have been absorbed into the constant in \eqref{eq:physicalenergy}.

The finite construction is certified by an equality between the reflected row and its proposed fiber expression, before the energy bound is used. Thus the premise ``has an exact completed model'' is proved for the actual coefficients. The arbitrary-member theorem for a model class is not the final premise of this proposition. The detailed local exponent partition and the fiber sum are technical arithmetic source lemmas; this paragraph specifies their function rather than replacing their proof.
\end{proof}
\src{AngularPhysicalFiberData; AngularPhysicalFiberIdentity.completedT_eq_reflectedFiber_idealValue; AngularPhysicalRowEnergy.actual_exactModels; completed_angular_row_energy}

The distinction between fixed and moving parameters matters here. Constants may depend on $n,q,W$. They do not depend on $m,\frakf_0,K,X$ or on the individual rows. The factor $\Nm\frakq$ cannot be called ``fixed conductor'' and absorbed into the constant. It is exactly the factor constrained by the descent geometry in the next section.

The periodicity premise can be discharged without an assumption of primitivity. Take $q=\Nm\frakf\ne0$. The source uses the inclusion of the principal ideal generated by $\Nm\frakf$ in $\frakf$ to show that the finite residue homomorphism factors through the fixed base conductor. The physical fiber theorem also requires nonzero row ideals; this follows from $K/2\le\Nm\frakj$ and $K\ge1$. It requires a squarefree label, a nonzero mask, $X,K\ge1$, and smooth compact support away from zero. These are the hypotheses explicitly retained in Proposition~\ref{prop:completedenergy}. The generic model-to-energy theorem is applied only after the equality of the actual completed row with its reflected fiber has been proved.

For the descent one needs more than a single character. The source takes a common conductor $q=3\Nm\frakf$ for its finite ray orbit. For every allowed base ray twist $\Psi$, it constructs an admitted character $\psi$ of the same angular type whose finite part factors through that conductor, and proves equality of their \emph{masked completed sums}. It does not assert equality of the element coefficients at every element. Equality on the supported primary inputs suffices; the fixed mask kills the remaining inputs. This is the bridge that makes the physical reflection estimate available to every state in the orbit.
\src{AngularPhysicalRowEnergy.finiteResidue_factors_fixedConductor; AngularPhysicalRowEnergy.actual_exactModels; AngularRayOrbit.orbitConductor; AngularRayOrbit.exists_orbit_character; AngularRayOrbit.completed_row_rayChild; AngularSieveModels.actual_canonicalThetaModels}

% END 04_energy


% BEGIN 05_descent
\section{A finite descent, and the return to the original mean square}\label{sec:descent}

The reflection estimate is not yet Proposition~\ref{prop:ms}. It controls completed cubic columns. The original row square produces correlated pairs of such columns, masks, label ideals, and additional height integrals. The role of the finite descent is to control this entire family while preserving its coefficient structure.

\subsection{The energy being propagated}
Choose a finite pool of good primes containing all primes in the relevant supported ideals. For a squarefree ideal $\fraka$ supported in the pool, let $c(\fraka)$ be the normalized cubic coefficient from Section~\ref{sec:reflection}. Let $V$ be a smooth function supported in the logarithmic window $[-A,A]$. A canonical row has the form
\begin{align}\label{eq:canonicalrow}
 P_{\Psi,m,f,V,X}(z)
 =\sum_{\fraka}^{\rm pool}c(\fraka)\Psi(g(\fraka))
 \boldsymbol1_{(\fraka,(m))=1}
 R_{\fraka}(f)^4R_{\fraka}(z)
 V\left(\log\frac{\Nm\fraka}{X}\right).
\end{align}
This is the ideal version of the source's finite subset-of-primes definition. The Chinese remainder and Gauss-factor identities identify the subset coefficient with $c(\fraka)$, including the phase from the chosen generator.

Fix a nonnegative smooth majorant $w$ which is one on $[0,1]$ and zero above $2$. For a finite label set $\mathcal L$, define
\begin{equation}\label{eq:energy}
 \mathcal E(\Psi,m,\mathcal L,V;X,K)
 =\sum_{\frakf_0\in\mathcal L}\sum_{z\ne0}
 w\left(\frac{\Nm(z)}K\right)
 |P_{\Psi,m,g_0(\frakf_0),V,X}(z)|^2.
\end{equation}
The row $z=0$ is excluded. If Poisson summation is performed with that row temporarily included, its square must be subtracted again. This convention is part of the physical energy, not an arbitrary choice of an abstract positive quadratic form. In the source's Fourier convention, the auxiliary height twist on nonzero elements is $\Psi_t(a)=\Psi(a)\exp(2\pi it\log\Nm(a))$; its absolute value does not change. This auxiliary height parameter differs by a factor $2\pi$ from the real norm-twist parameter $\tau$ in Theorem~\ref{thm:main}.
\src{CubicSieve/FirstPassage.secondChildColumn; CubicSieve/LogSeparation.canonicalLogEnergy; RowCompletion/CompletedEnergy.outsideLogEnergy}

The possible base coefficients form a finite orbit: the initial coefficient and its products with the fixed finite ray characters in the source. The orbit has at most seventeen elements. The ray operations in the reopening identities preserve it. The conjugate orientations of the smooth profiles are retained separately; this does not assert that conjugating an arbitrary angular base leaves its angular type unchanged. The mask $m$ is tracked separately; it does not enlarge the supposedly fixed coefficient orbit. Angular reflection supplies the physical estimates for this orbit by choosing one finite conductor large enough for all its residue parts.

\subsection{State invariants and the decreasing integer}
For $Z>1$ and $K\ge1$ put
\begin{equation}\label{eq:rank}
 r=r_Z(K)=\left\lceil\frac{1000\log K}{\log Z}\right\rceil,
 \qquad 0\le r\le3000\quad\text{when }K\le Z^3.
\end{equation}
For $0<\eta\le1/1000$ define
\[
 M_r=e^{3(3000-r)}Z^2,\qquad
 \gamma_r=\frac1{20}-\eta(3000-r).
\]
A state $(\Psi,m,\mathcal L,X,F,K)$ is admissible when
\begin{align}
 &\Psi\text{ lies in the fixed base ray orbit},\quad m\ne0,
       \quad X>0,\quad F,K\ge1,\quad K\le Z^3,\nonumber\\
 &XF\le M_r,\qquad K\Nm(m)\le XFZ^{-\gamma_r},\label{eq:state}\\
 &\frakf_0\in\mathcal L\Longrightarrow
    \frakf_0\ne0,\ \frakf_0\text{ squarefree},\
    (\frakf_0,\textstyle\prod_{\frakp\in S}\frakp)=1,
    \quad\Nm\frakf_0\le F.\nonumber
\end{align}
These are the contents of the source's canonical-state predicate. The initial state has the stronger bounds $XF\le Z^2$ and $K\Nm(m)\le XFZ^{-1/20}$ (with the fixed excluded-prime norm included when choosing the initial mask). The rank-dependent padding allows bounded scale inflation at later stages.

There are two finite budgets. As the rank drops, $M_r$ grows by a factor at least $e^3$ per step, allowing bounded changes of logarithmic bins. At the same time the margin $\gamma_r$ loses $\eta$ per unit by which the rank decreases. The total loss is at most $3000\eta$. If $3000\eta\le1/80$, then $\gamma_r\ge3/80$. After allowing the fixed excluded-prime factor and a dyadic row enlargement, a margin of $1/40$ remains for the short reflected estimate, once $Z$ exceeds a constant depending on those fixed primes. The large threshold $Z\ge e^{9000}$ ensures $M_r\le Z^3$. These numbers are bookkeeping constants; they are not claims of computational practicality.
\src{MeanSquare/UnitRows.CanonicalStateCondition; CubicSieve/ArithmeticBins.fixedDepthRank; CubicSieve/DensityBudgets.canonicalRankMass; canonicalRankMargin}

Each part of the state has a separate purpose. The coefficient condition allows the same fixed collection of reflection estimates at every generation. The nonzero mask gives $\Nm(m)\ge1$, which turns a ratio estimate into a bound on the number of rows. Squarefree labels and their coprimality to the bad primes are the hypotheses of the arithmetic row identities; a mere bound on their norms would not suffice. The mass bound controls the supported column and label scales, whereas the margin controls the product of row size and mask norm. Finally, $K\le Z^3$ bounds the number of generations. No one of these conditions replaces the others.

In a live state, $X\ge1$ and $F\ge1$. Hence $X,F\le XF\le M_r\le Z^3$. This explains why the reopening theorem's separate upper bounds on $X$ and $F$ follow from the state. The common-pool hypothesis is additional: the fixed cutoff must contain every column with norm at most $e^A X$. It is imposed explicitly below, rather than absorbed into the definition of admissibility.

\subsection{The one-step arithmetic lemma}
\begin{lemma}[Reopening at smaller rank]\label{lem:step}
\technical\ Fix the base orbit, excluded primes, $\eta$, and a logarithmic support radius $A$. There are four fixed smooth child profiles, supported in $[-(2A+11),2A+11]$, with the following property. Let the original state be admissible and satisfy $X\ge1$, as required by the reopening theorem. Suppose every admissible state of rank less than $r_Z(K)$, for those child profiles and all real heights $s$, satisfies
\[
 \mathcal E(\Psi'_s,m',\mathcal L',V';X',K')
 \le E(X'F')^2(1+|s|)^{2J},\qquad E\ge1.
\]
Then, for a sufficiently large fixed $Z$ threshold and a common sufficiently large prime pool, the original state satisfies
\begin{equation}\label{eq:step}
 \mathcal E(\Psi_t,m,\mathcal L,V;X,K)
 \le C E(XF)^2Z^{57\eta}(1+|t|)^{2J}.
\end{equation}
Here $J$ is chosen in advance large enough for the finite number of height derivatives required by the reflection and separation estimates. Constants and child profiles do not depend on the later state variables or on the height.
\end{lemma}

\begin{proof}[Structure of the source proof]
M\"obius inversion in the cube variable separates \eqref{eq:short} from the remaining cube scales. The short part is used only when $F<Z^{1/1000}$, with cube cutoff $Z^{1/1000}$; otherwise this part is empty. Proposition~\ref{prop:completedenergy}, together with the state margin, bounds its contribution to the row energy by
\begin{equation}\label{eq:shortenergy}
 C(XF)^2Z^{8\eta-1/40}(1+|t|)^d.
\end{equation}
This follows from the source's more general exponent $\kappa+7\varepsilon-1/40$ by setting $\kappa=\varepsilon=\eta$. The factor $2X$ from completing the row is already included in \eqref{eq:shortenergy}.

For each remaining cube scale, open the product of Gauss coefficients, apply the finite character identities and the second Poisson transformation, and sort terms into logarithmic scale bins. The new label, row, and mask are explicit products of the old prime factors. Cauchy--Schwarz and the finite-fiber multiplicity estimate bound the pushforward energy. Each retained bin has a new state satisfying \eqref{eq:state} and
\begin{equation}\label{eq:rankdrop}
 r_Z(K')+1\le r_Z(K).
\end{equation}
The discarded large-radial bins are controlled by rapid decay of the smooth transform. The two source orientations and conjugation give four child profiles, not profiles chosen separately for each numerical state.

The formal arithmetic reopening theorem bounds the long contribution by
\[
 C E(XF)^2Z^{\eta+17\delta+39\varepsilon}(1+|t|)^{2J}.
\]
Setting $\delta=\varepsilon=\eta$ gives $57\eta$. Taking $2J\ge d$ and using $8\eta-1/40\le57\eta$ absorbs \eqref{eq:shortenergy}. This proves the one-step implication once the finite decomposition and \eqref{eq:rankdrop} have been established.

The exact prime-exponent cases, fiber multiplicities, and scale inequalities in that decomposition are inherited technical source lemmas. They are not consequences of a generic contraction principle. Their mathematical task is to prove that every actual summand is either in the short part, a controlled radial tail, or one of these smaller-rank states, with no uncounted multiplicity. The source locations below identify the closed one-step lemma and the invariant-preserving lemma used inside it.
\end{proof}
\src{RowCompletion/CubicReopening.progressingCanonicalFamily_closed_step; MeanSquare/UnitRows.canonicalStateCondition_retained; AngularSieveDensity.canonicalLog_actual_step}

\subsection{Why a retained child has strictly smaller rank}\label{sec:rankgeometry}
Here is the quantitative content of the arithmetic step. This separates the finite-factorization input from the elementary deduction that it permits. For a long cube bin let $B>0$ be its lower scale, put $B_+=eB$ and $\ell=X/B^3$, and let $q_i\ge1$ ($0\le i\le9$) be the representatives of its ten logarithmic bins. The source calls these numbers \texttt{globalLogRep}. The child scales are
\begin{align*}
 X'&=\frac{\ell}{q_0q_1q_2q_3q_6q_7},&
 F'&=e^4q_1q_4q_6q_7,& K'&=e q_8,\\
 \mathcal D&=B_+Fq_0q_2q_3,&
 m'&=m\,g_0(\mathfrak q_1)g_0(\mathfrak q_2)g_0(\mathfrak q_3).
\end{align*}
The triple of ideals $\mathfrak q_i$ is fixed on the arithmetic fiber; it is distinct from the real bin representatives $q_i$. Its factors are nonzero, so $m'\ne0$. The $q_i$ record norms of the factors in the second-source decomposition. They are not ten free parameters to be optimized.

\paragraph{The inherited geometry interface.}
For a nonempty actual bin with nonzero source frequency, both cube-factor norms at most $B_+$, and retained radial parameter at most $Z^\eta$, the source proves the following implications. Assume
\[
 Z\ge e^{9000},\quad 0\le\eta\le1/1000,\quad
 Z^{1/1000}\le B_+F,\quad K\le Z^3.
\]
In addition to positivity and the required label restrictions, its conclusions include
\begin{align}
 X'F'&\le e^3XF,&
 K'&\le K/\mathcal D\le K Z^{-1/1000},\label{eq:childscales}\\
 \frac{K'\Nm(m')}{X'F'}
 &\le Z^\eta\frac{K\Nm(m)}{e^3XF}.
 \label{eq:childratio}
\end{align}
The finite prime-exponent calculation establishing these inequalities is inherited. Its hypotheses matter: a generic row or an arbitrary tuple of positive scales need not satisfy them. The source's retained-bin construction supplies the radial condition. The long part supplies progress $B_+F\ge Z^{1/1000}$: either the label scale is already large, or the cube variable has passed the short cutoff. The case $Z\ge e^{9000}$ also gives $B_+F\ge e^4$, as required by the pooled-mass estimate.

\paragraph{The elementary closure argument.}
From \eqref{eq:childscales},
\[
 \frac{1000\log K'}{\log Z}
 \le\frac{1000\log K}{\log Z}-1.
\]
Taking ceilings, using $K'\ge1$, gives $r'=r_Z(K')\le r_Z(K)-1$. Thus the decrease is in an integer rank, even when the logarithmic scales themselves are real. Since $r'\le r-1\le2999$,
\[
 e^3M_r\le M_{r'},\qquad \gamma_{r'}+\eta\le\gamma_r.
\]
The first inequality and \eqref{eq:childscales} imply $X'F'\le M_{r'}$. For the margin, \eqref{eq:childratio} gives
\[
 \frac{K'\Nm(m')}{X'F'}
 \le e^{-3}Z^{\eta-\gamma_r}
 \le Z^{-\gamma_{r'}}.
\]
Also $K'\le K\le Z^3$. The remaining closure assertions concern the actual factors: the new label is nonzero and squarefree, remains outside the bad primes, and has norm at most $F'$; the new coefficient is one of the allowed ray twists. These are proved by the retained-state source lemma, not by the scalar inequalities alone. This is precisely where a proposed replacement of the actual arithmetic rows by unrestricted coefficients would break the argument.
\src{MeanSquare/CanonicalTailBounds.globalRetained_canonical_geometry; CubicSieve/ScaleCaps.globalPooledColumnScale; CubicSieve/ScaleCaps.globalPooledLabelScale; CubicSieve/DensityBudgets.canonical_retained_unpadded_closure; CubicSieve/DensityBudgets.canonicalRankMass_child; CubicSieve/DensityBudgets.canonicalRankMargin_padding; MeanSquare/UnitRows.canonicalStateCondition_retained}

\subsection{Both terminal cases, by elementary counting}\label{sec:terminals}
We explain the terminal estimate rather than treating it as an unexplained base case. Put $M=\sup|V|$ and let $\|w\|_\infty$ denote the fixed row majorant's supremum. The local normalized Gauss-factor bound and the coefficient-orbit bound give absolute value at most one for the arithmetic coefficient of each column in \eqref{eq:canonicalrow}; the height twist also has absolute value at most one. This coefficient bound is the inherited input in the following elementary argument.

The support of $V$ forces $\Nm\fraka\le e^A X$. If $e^A X<1$, there are no nonzero integral-ideal columns, and the energy is zero. Otherwise the Eisenstein ideal-counting bound gives at most $128e^AX$ columns. Thus every row has modulus at most $128e^AXM$. There are at most $128F$ label ideals and at most $128(2K)$ lattice points in the row disk $\Nm(z)\le2K$. Restricting these sets can only reduce the resulting upper bound. Consequently
\begin{equation}\label{eq:elementaryterminal}
 \mathcal E\le
 2\cdot128^4\|w\|_\infty(e^AM)^2 X^2FK.
\end{equation}
The source uses the zeroth Schwartz seminorm in place of the displayed supremum. The constants $128$ are convenient counting bounds, not sharp lattice asymptotics. The bound is independent of the finite pool: counting supported ideals never introduces a factor equal to the size of that pool.

It remains to explain why each terminal condition supplies $K\le F$. If $r_Z(K)=0$, then $K\le1$ by the definition of the ceiling; admissibility gives $K=1\le F$. If $0<X\le1$, use the reserved margin. For $3000\eta\le1/40$ we have $\gamma_r\ge1/40$, and hence
\[
 K\le K\Nm(m)\le XFZ^{-1/40}\le XF\le F.
\]
Here the first inequality uses $m\ne0$, and the second uses the state. This also works when the rank is positive. In either case \eqref{eq:elementaryterminal} yields $\mathcal E\le C_{A,V}(XF)^2$. Notice that $X\le1$ does not by itself make the energy zero: the support window may still contain ideals of norm at least one. That is why the counting argument, rather than an empty-sum assertion, is needed.
\src{CubicSieve/CanonicalLogEnergy.canonicalLogEnergy_terminal; canonicalSmoothedEnergy_uniform_row_bound; canonicalLogEnergy_subunit; canonicalTerminalConstant; Eisenstein/BarrierPotential.CanonicalStateCondition.terminal_energy; RowCompletion/CompletedEnergy.outsideLogEnergy_terminal_constant}

\subsection{Closing the induction without a circular supremum}
\begin{proposition}[Finite energy bound]\label{prop:finiteenergy}
For each $\varepsilon>0$ and fixed initial support window, the physical canonical energy satisfies
\begin{equation}\label{eq:finiteenergy}
 \mathcal E(\Psi_t,m,\mathcal L,V;X,K)
 \ll (XF)^2Z^\varepsilon(1+|t|)^d
\end{equation}
throughout the admissible states, with the prescribed common prime pool. The exponent $d$ and the constant are chosen before the state variables.
\end{proposition}
\begin{proof}
First apply the source's terminal estimate. For a fixed smooth $V$ supported in $[-A,A]$, there exists $C_{\rm term}\ge0$ such that, for every admissible state with base coefficient of absolute value at most one, every cutoff $D$, and every real height $t$,
\[
 \mathcal E(\Psi_t,m,\mathcal L,V;X,K)\le C_{\rm term}(XF)^2
 \quad\text{if }r_Z(K)=0\ \text{or }X\le1,
\]
provided $Z>1$, $\eta\ge0$, and $3000\eta\le1/40$. The constant depends only on $A,V$; it is uniform in the state, height, and cutoff. This is the source's terminal lemma for both cases, including $0<X\le1$ at positive rank. In its small-$X$ branch, the state invariant and the nonzero mask give $K\le F$, which is the hypothesis used in the elementary terminal energy bound. This branch does not require rank zero.
\src{RowCompletion/CompletedEnergy.outsideLogEnergy_terminal_constant; Eisenstein/BarrierPotential.CanonicalStateCondition.terminal_energy}

At rank zero, $K=1$, so the terminal estimate starts the induction. At each later rank, first stop if $X\le1$ and use the same estimate. In every remaining state $X>1$, hence $X\ge1$ as required by Lemma~\ref{lem:step}. Assuming the result at every smaller rank, that lemma multiplies the normalized bound by at most a constant times $Z^{57\eta}$. Induction to rank $r$ therefore gives
\[
 \mathcal E\le C_{r,V}Z^{57\eta r}(XF)^2(1+|t|)^{d_r}.
\]
Only the four child profiles at each of finitely many levels occur. Their constants and height exponents can be chosen recursively and maximized over those finite lists. The recursive support radii are $A_0=A$, $A_{j+1}=2A_j+11$. Choose the finite prime-pool cutoff $D$ before starting, with
\[
 D\ge e^{A_{3000}}Z^3.
\]
All supported ideals at every level then fit in that pool. Its size is not absorbed into a constant that depends on $D$; the preceding estimates are uniform in that cutoff.

Choose $\eta>0$ so small that
\[
 \eta\le1/1000,\quad 3000\eta\le1/80,
       \quad 171000\eta\le\varepsilon.
\]
Since $r\le3000$, the factor $Z^{57\eta r}$ is at most $Z^\varepsilon$. The finitely bounded range of $Z$ below the fixed large threshold is treated by the elementary counting bound and included in the constant. This proves \eqref{eq:finiteenergy}. No assertion that an infinite supremum is finite is used to initiate the argument.
\end{proof}
\src{AngularSieveDensity.outsideLogEnergy_finite_rank; outsideLogEnergy_small_power}

\subsection{Paired density and its quantifiers}
After the first Poisson transformation of the original row square, the finite arithmetic expansion produces paired child rows. Their label norms are bounded by $F$, row norms by $K$, and their column scale by $X$. Write $M$ for the norm of the full initial mask, including the fixed excluded primes. The initial geometry is
\begin{equation}\label{eq:initialgeometry}
 XF\le Z^2,\qquad KM\le XFZ^{-1/20}.
\end{equation}
The paired density is an integral of these two child-row arrays against the source's absolutely integrable logarithmic separation densities. The two sides have the conjugate orientations forced by the original square. Apply Cauchy--Schwarz to the pair, use \eqref{eq:finiteenergy} for each oriented energy, and choose enough decay in the separation densities to integrate the resulting height polynomial. This bounds that paired density by
\begin{equation}\label{eq:density}
 C Z^\varepsilon(XF)^2.
\end{equation}

The order of choices in this assertion is essential. Given $\varepsilon>0$, a polynomial scale cap $P\in\N$, and a support radius $A\ge0$, first choose the needed height degree $J$. After the two smooth profiles are fixed, choose $C,C_{\rm pool}$ and an integer $E\ge P$. The estimate then holds for all $Z\ge1$, all $D\ge C_{\rm pool}Z^E$, all ray choices, all finite label-row sets, and all $X,F,K\ge1$ with $X,F,K,M\le Z^P$ satisfying \eqref{eq:initialgeometry}. Labels are squarefree, outside the excluded primes, and rows are nonzero. The profiles are smooth, compactly supported in $[-A,A]$. This is the mathematical content of the predicate named \texttt{HasInitialCanonicalDensityAtRadius}. It is uniform over the subsequent finite arrays and scales; it is not just a bound for one selected configuration.
\src{AngularInitialDensity.HasInitialCanonicalDensityAtRadius; hasInitialCanonicalDensityAtRadius_of_theta}

More explicitly, project the finite set of label--row pairs onto its label set $\mathcal L$. For either orientation, enlarge the row set to the entire majorized disk. This is legitimate because the sum of squared moduli is nonnegative, every original row is nonzero, and $w=1$ on its disk. The finite Cauchy--Schwarz inequality bounds a paired sum by the product of the square roots of these two energies. After integrating the separation variables, the source's density lemma gives a constant of the form
\[
 6(C_1+C_2)\left(\int_\R d_0(t)\dd t\right)^3
 Z^\varepsilon(XF)^2,
\]
where $d_0$ is the fixed nonnegative \texttt{firstLogDensity} of order zero and $C_1,C_2$ are the two energy constants. The density is defined with sufficient height decay before this comparison; the power $(1+|t|)^d$ is therefore integrable against the chosen separation weights. No supremum over unbounded heights is taken without that weight.

The actual initial state is built for each of the two coefficients \texttt{secondRayMinus} and \texttt{secondRayPlus}. Its mask is the product of the selected outside primes. The extra fixed excluded-prime norm in $M$ makes the stated initial geometry strong enough for this state and the later reflection estimate. The label hypotheses give precisely nonzero squarefree ideals, coprimality outside $S$, and the bound $\Nm\frakf_0\le F$. The large-$Z$ branch uses the descent; below the fixed threshold $Z_0$, elementary counting bounds the density by a constant times $K(XF)^2$, and $K\le Z_0^3$ absorbs this extra factor. The source can choose $E=\max(P,3)$ and $C_{\rm pool}=\exp(A_{3000})$. Thus the constant is chosen before $D$, the array, and the scales in both branches.
\src{AngularInitialDensity.outsideCanonicalDensity; AngularInitialDensity.hasInitialCanonicalDensityAtRadius_of_theta; RowCompletion/DensityTransfer.initialCanonicalState; RowCompletion/DensityTransfer.densityChildEnergy_from_canonical_heights}

\subsection{Proof of the physical mean-square estimate}
\begin{proof}[Source reduction completing Proposition~\ref{prop:ms}]
Let $\chi$ have type $k=n$ with $n\in\N$, as in Proposition~\ref{prop:ms}. Let $H=Z^{1+\sigma}$ and fix $\varepsilon>0$. Apply the physical initial-density theorem of type $-n$ to $\overline\chi$. This is the conjugated physical element coefficient required by the row-square source identity. Set
\[
 \eta=\min(1,\varepsilon/100),\qquad
 \nu=(\sigma-1/20)/3>0.
\]
In the finite first/second Poisson expansion, partition the nonzero source at radial parameter $Z^\nu$. The retained range satisfies the initial geometry needed for \eqref{eq:density}, because $2\nu\le\sigma-1/20$. The retained contribution is bounded by
\[
 C_1HZ^{35\eta},
\]
and the high-radial tail by $C_2Z^{-1}$. Since $35\eta\le\varepsilon$ and $H\ge1$, their sum is at most $CHZ^\varepsilon$.

The full Poisson comparison has the sign-sensitive form
\begin{equation}\label{eq:poissoncomparison}
 Z^{-1}\sum_{z\in T}|A_Z(z)|^2
 \le |\mathcal S_{\ne0}|+\Rea\mathcal S_0+|\mathcal T|
                 -|G_{\varnothing}|^2.
\end{equation}
Here $\mathcal S_{\ne0}$ is the nonzero second source just bounded, $\mathcal S_0$ is its zero-frequency contribution, and $\mathcal T$ is the truncation remainder. The separate zero-source and tail estimate gives $\Rea\mathcal S_0+|\mathcal T|\le C_3H$. The final negative term is the removed zero-row square. It may now be dropped for an upper bound; it was not silently omitted when deriving the source identity. Multiplying by $Z$ gives \eqref{eq:ms}.

The original definition may have used a smaller cutoff $D\ge bZ$ than the common pool needed by \eqref{eq:density}. Enlarge it to the maximum of $D$ and $\lceil C_{\rm pool}Z^E\rceil$. This does not change \eqref{eq:AZ}, since the added ideals lie outside the support of $W(\Nm\fraka/Z)$. Apply the uniform source estimate at the enlarged cutoff and return to the unchanged sum. This proves uniformity in the original cutoff.

The two Poisson source identities and the radial partition estimates are additional technical source lemmas. The bound \eqref{eq:poissoncomparison} specifies their exact task and the sign of the correction. The argument here shows how their quantitative conclusions, together with the finite descent, imply the physical mean-square statement, rather than leaving a density hypothesis in that statement.
\end{proof}
\src{AngularNonzeroSource.nonzero_source_bound; AngularPoissonMoment.outside_mean_square_of_canonical_density_at_radius; AngularPoissonMoment.physical_outside_mean_square; AngularInitialDensity.physical_initial_density; AngularIdealRow}

% END 05_descent


% BEGIN 06_average
\section{Sixth-power averaging and the exponent 15/16}\label{sec:average}

Fix an admitted $\chi$ of type $k\ge0$ and the set $S$ supplied by Proposition~\ref{prop:ms}. This sign restriction is retained throughout this section. Define the ideal totient ratio
\[
 d(\fraka)=\prod_{\frakp\mid\fraka}\left(1-\frac1{\Nm\frakp}\right)
\]
and the smoothed sum
\begin{equation}\label{eq:FZ}
 F_W(Z)=\sum_{\fraka\text{ outside }S}
 \mu_K(\fraka)\chi(\fraka)d(\fraka)
 W\left(\frac{\Nm\fraka}{Z}\right).
\end{equation}

\begin{lemma}[Averaging identity]\label{lem:average}
There is a fixed smooth nonnegative radial test function $V$, supported in $[1/2,1]$, with $|V|\le1$ and nonzero zero-frequency radial Fourier coefficient $v_0$, such that for $Y\ge1$,
\begin{equation}\label{eq:average}
 B(Z,Y):=\sum_{b\in\OO}V\left(\frac{\Nm(b)}Y\right)A_Z(b^6)
       =Yv_0F_W(Z)+\mathcal R(Z,Y),
\end{equation}
where for every $\varepsilon>0$,
\begin{equation}\label{eq:R}
 |\mathcal R(Z,Y)|\ll_{\chi,W,V,S,\varepsilon}Z^{1+\varepsilon}.
\end{equation}
The estimate is uniform in $Y\ge1$ and in any cutoff $D\ge bZ$ used to define $A_Z$.
\end{lemma}

\begin{proof}[Explanation of the averaging identity and error]
Interchange the two finite sums and use \eqref{eq:sixth}. For a fixed squarefree $\fraka$ the inner sum is over $b$ coprime to $\fraka$. Inclusion--exclusion gives
\[
 \boldsymbol1_{(\fraka,(b))=1}
 =\sum_{\frakd\mid\fraka}\mu_K(\frakd)\boldsymbol1_{b\in\frakd}.
\]
Poisson summation on the ideal lattice $\frakd$ has zero-frequency term $Yv_0/\Nm\frakd$. Its divisor sum is exactly $Yv_0d(\fraka)$. The fixed normalization of $v_0$ includes the covolume of $\OO$; it is not assumed to be one.

The radial Poisson estimate used in the source bounds the nonzero-frequency remainder for each ideal lattice by a fixed seminorm of $V$, uniformly in the dilation after the zero mode is separated. Summing the inclusion--exclusion remainder costs at most $2^{\omega(\fraka)}$. For every $\varepsilon>0$ this is $O_\varepsilon((\Nm\fraka)^\varepsilon)$. Finally $|\chi|\le1$, $W$ is bounded, $\Nm\fraka\le bZ$ on its support, and the number of ideals of norm at most $bZ$ is $O(bZ)$. These observations give \eqref{eq:R}. All zero modes are retained in the main term before estimating the remainder.

The uniformity in the ideal lattice can also be understood geometrically in this field. Write $\frakd=(d)$ and $b=dc$. Radiality gives
\[
 \sum_{b\in\frakd} V\left(\frac{\Nm(b)}Y\right)
 =\sum_{c\in\OO}V\left(\frac{\Nm(c)}t\right),
 \qquad t=Y/\Nm\frakd.
\]
Thus all ideal lattices reduce to one fixed lattice with a positive dilation parameter; their rotations do not affect the test. For $t<1$ the support in $[1/2,1]$ makes this sum zero, while the main term $tv_0$ is bounded. For $t\ge1$, Poisson summation and rapid Fourier decay give a bounded remainder after the main term. This explains why no uncontrolled shape constant depending on $\frakd$ appears. The pinned radial Poisson lemma supplies the exact normalization and seminorm bound used in the source.
\end{proof}
\src{AngularSixthPower.average_remainder_small_power; Mellin/SixthPowerAverage.totient_sum_normalized_bound}

\begin{lemma}[Cauchy--Schwarz with multiplicity]\label{lem:cauchy}
Let $T_Y=\{b^6:b\ne0,\ \Nm(b)\le Y\}$. Then
\begin{equation}\label{eq:cauchy}
 |B(Z,Y)|^2\le768Y\sum_{z\in T_Y}|A_Z(z)|^2.
\end{equation}
\end{lemma}
\begin{proof}
There are at most $128Y$ nonzero Eisenstein elements in the disk used by the source's lattice bound. Cauchy--Schwarz, followed by $|V|\le1$, bounds the left side by $128Y$ times the sum of $|A_Z(b^6)|^2$ over that disk. Each nonzero value has at most six preimages, since $X^6-z$ has degree six over a field. This proves the stated bound. The constant $768$ is $128\cdot6$, not an exponent loss.
\end{proof}
\src{Mellin/SixthPowerAverage.average_tsum_cauchy}

\begin{proposition}[Smoothed M\"obius cancellation]\label{prop:mobius}
For the fixed $\chi$ of nonnegative angular type and $S$ above, and every $\varepsilon>0$,
\begin{equation}\label{eq:mobius}
 F_W(Z)\ll_{\chi,W,S,\varepsilon} Z^{15/16+\varepsilon}
 \qquad(Z\ge1).
\end{equation}
\end{proposition}
\begin{proof}
Apply Proposition~\ref{prop:ms} with
\begin{equation}\label{eq:parameters}
 \sigma=\frac1{20}+\frac{6\varepsilon}{5},\qquad
 Y=Z^{7/40+\varepsilon/5}.
\end{equation}
Then $Y^6=Z^{1+\sigma}$, so every element of $T_Y$ lies in the permitted row disk and is nonzero. Thus
\[
 \sum_{z\in T_Y}|A_Z(z)|^2\ll Z^{41/20+11\varepsilon/5}.
\]
Multiplying by $Y$ in \eqref{eq:cauchy} and taking a square root gives
\[
 |B(Z,Y)|\ll Z^{89/80+6\varepsilon/5}.
\]
The error in \eqref{eq:R} is at most this scale for $Z\ge1$. Divide \eqref{eq:average} by $Y|v_0|$ and use
\[
 \frac{89}{80}-\frac7{40}=\frac{15}{16},\qquad
 \frac{6\varepsilon}{5}-\frac{\varepsilon}{5}=\varepsilon.
\]
This proves \eqref{eq:mobius}. More precisely the divided error has exponent $33/40+4\varepsilon/5$, which is smaller than the asserted exponent. The proof only needs the weaker comparison made above.
\end{proof}
\src{AngularSeedFifteenSixteenthsMomentRisk.outside_totient_moebius_bound}

This calculation also explains where the numerical boundary comes from. With an available row radius $Z^{1+\sigma}$, sixth-power sampling allows $Y=Z^{(1+\sigma)/6}$. Ignoring arbitrarily small losses, the square-root bound after division by $Y$ has exponent
\[
 \frac{2+\sigma}{2}-\frac{1+\sigma}{12}
 =\frac{11+5\sigma}{12}.
\]
At the limiting admissible value $\sigma=1/20$ this is $15/16$. The strict inequality in the mean-square hypothesis is the reason for retaining $\varepsilon$ and obtaining an open zero-free half-plane. This identity is an explanation of the chosen parameters, not an assertion of optimality of the full method.

% END 06_average


% BEGIN 07_mellin
\section{From cancellation to the actual \texorpdfstring{$L$}{L}-function}\label{sec:mellin}

\subsection{A Mellin transform that is holomorphic beyond absolute convergence}
Until the final conjugation step, let $\chi$ have nonnegative angular type, as in Proposition~\ref{prop:mobius}, with its corresponding $S$. Write $\beta=15/16$ and
\[
 \widehat W(s)=\int_0^\infty W(x)x^{s-1}\dd x,\qquad
 M_W(s)=\int_0^\infty F_W(Z)Z^{-s-1}\dd Z.
\]
The first function is entire. The second is holomorphic for $\Rea s>\beta$. To justify this, $F_W(Z)$ vanishes for sufficiently small positive $Z$, since a nonzero ideal has norm at least one. On each compact subset of $\Rea s>\beta$, choose $\varepsilon>0$ smaller than the distance from that compact set to the boundary. Proposition~\ref{prop:mobius} gives an integrable majorant at infinity, also after multiplication by any fixed power of $\log Z$. It justifies differentiation under the integral and establishes holomorphy locally throughout the open half-plane.

For $\Rea s>2$, absolute convergence permits termwise integration. The change of variables $x=\Nm\fraka/Z$ gives
\begin{equation}\label{eq:mellinidentity}
 M_W(s)=\widehat W(s)D_S(s),\qquad
 D_S(s)=\sum_{\fraka\text{ outside }S}
 \frac{\mu_K(\fraka)\chi(\fraka)d(\fraka)}{(\Nm\fraka)^s}.
\end{equation}
The source uses the safe half-plane $\Rea s>2$ for this initial identity. There is no need to optimize it: any nonempty open region of absolute convergence suffices for the identity theorem.
\src{AngularWeightedMellin; AngularSeedFifteenSixteenthsMellinRisk}

\subsection{Restoring the damping and the excluded primes}
The Dirichlet series in \eqref{eq:mellinidentity} is not $1/L(\chi,s)$. Its local factor at a prime outside $S$ is
\[
 1-d_{\frakp}x_{\frakp},\qquad
 x_{\frakp}=\chi(\frakp)(\Nm\frakp)^{-s},\qquad
 d_{\frakp}=1-(\Nm\frakp)^{-1}.
\]
Define
\begin{align}
 E_S(s)&=\prod_{\frakp\in S}(1-x_{\frakp}),\label{eq:ES}\\
 H_S(s)&=\prod_{\frakp\notin S}
       \frac{1-x_{\frakp}}{1-d_{\frakp}x_{\frakp}}.\label{eq:HS}
\end{align}
Both are holomorphic for $\Rea s>0$, and there $H_S$ is nonzero. Here is a direct verification of the infinite-product assertion. On $\Rea s\ge\delta>0$,
\[
 |1-d_{\frakp}x_{\frakp}|\ge1-2^{-\delta}>0
\]
and
\begin{equation}\label{eq:localcorrection}
 \frac{1-x_{\frakp}}{1-d_{\frakp}x_{\frakp}}-1
 =-\frac{x_{\frakp}}{\Nm\frakp(1-d_{\frakp}x_{\frakp})}.
\end{equation}
Its absolute value is at most $(1-2^{-\delta})^{-1}(\Nm\frakp)^{-1-\delta}$. The sum converges, by the convergence of the Dedekind zeta series to the right of one. Thus the product converges normally on compact subsets. Each numerator is nonzero there as well, since $|x_{\frakp}|<1$; absolute convergence of the perturbations of one gives nonvanishing of the product. The finite factor $E_S$ is entire and is also nonzero on $\Rea s>0$.

In the initial region of absolute convergence,
\begin{equation}\label{eq:eulerrestore}
 E_S(s)H_S(s)D_S(s)L(\chi,s)=1.
\end{equation}
This identity checks the direction of the correction factor: it is $(1-x)/(1-dx)$, not its reciprocal. Combining \eqref{eq:mellinidentity} and \eqref{eq:eulerrestore} gives
\begin{equation}\label{eq:centralanalytic}
 E_S(s)H_S(s)M_W(s)L(\chi,s)=\widehat W(s)
 \qquad(\Rea s>2).
\end{equation}
\src{AngularFiniteRestoration; AngularWeightedMellin}

\subsection{Choosing a test function at the point of interest}
It is unnecessary, and generally incorrect, to assume a single compactly supported $W$ has a zero-free Mellin transform throughout the half-plane. For a prescribed $s_0=\sigma_0+it_0$, choose a nonnegative nonzero $\phi\in C_c^\infty((1,2))$ and put
\[
 W_{s_0}(x)=x^{-it_0}\phi(x).
\]
Then
\begin{equation}\label{eq:nonzeroW}
 \widehat W_{s_0}(s_0)=\int_1^2\phi(x)x^{\sigma_0-1}\dd x>0.
\end{equation}
This is an elementary pointwise construction of the nonvanishing test needed in the proof. The constants in the M\"obius estimate are allowed to depend on this $W_{s_0}$. No uniformity in $s_0$ is required for qualitative nonvanishing.

\begin{proof}[Proof of Theorem~\ref{thm:main}, given Proposition~\ref{prop:ms}]
First let $k>0$. Every factor on the left side of \eqref{eq:centralanalytic} is holomorphic on $\Rea s>\beta$, as is the right side. The identity theorem extends \eqref{eq:centralanalytic} from $\Rea s>2$ to that connected half-plane. At any proposed zero $s_0$, use $W_{s_0}$ as above. The left side would be zero, whereas \eqref{eq:nonzeroW} shows that the right side is nonzero. This is a contradiction.

For $k=0$, use the holomorphic regularization $L^{\mathrm{reg}}(\chi,s)$ agreeing with $(s-1)L(\chi,s)$ away from the pole in the region at issue. Multiply the initial identity by $s-1$ and extend
\begin{equation}\label{eq:regularized}
 E_SH_SM_W L^{\mathrm{reg}}(\chi,s)=(s-1)\widehat W(s)
\end{equation}
holomorphically to $\Rea s>\beta$. If $s_0\ne1$, its right side is nonzero for $W=W_{s_0}$, so $L(\chi,s_0)\ne0$. At $s_0=1$, a nonprincipal finite character is covered by the independent classical theorem $L(\chi,1)\ne0$. In the principal case that point is the stated pole exception.

This proves the assertion for $k\ge0$. Now let $k<0$. The character $\overline\chi$ has type $-k>0$, so the result just proved gives $L(\overline\chi,\overline s)\ne0$ whenever $\Rea s>\beta$. The actual continuation satisfies, for $k\ne0$,
\[
 L(\overline\chi,s)=\overline{L(\chi,\overline s)}.
\]
Evaluating this identity at $\overline s$ gives $L(\overline\chi,\overline s)=\overline{L(\chi,s)}$, hence $L(\chi,s)\ne0$. This extends nonvanishing of the actual $L$-function; it makes no claim about transporting the sextic-row mean square to negative type. Complex conjugation preserves real parts, the principal condition, and the point $1$. Thus every admitted integer type, including $\pm1$, is covered.

Finally, on the initial half-plane of absolute convergence,
\[
 L(\chi_\tau,s)=L(\chi,s-i\tau).
\]
The equality extends to the continuations. Since $\Rea(s-i\tau)=\Rea s$, the same bound follows, and the principal pole moves from $1$ to $1+i\tau$.
\end{proof}
\src{AngularSeedFifteenSixteenthsNonvanishingRisk.physical_seed_nonnegative; AngularSeedFifteenSixteenthsNonvanishingRisk.physical_seed_all_types; AngularFamilyConjugation.LFunction_conjugate; AngularFamilyConjugation.conjugate_nonzero_iff; AngularSeedFifteenSixteenthsFullFamilyRisk.physical_seed; physical_seed_norm_twist}

Notice that this argument never divides by a globally nonvanishing $\widehat W$. It extends a holomorphic identity and selects the test function at the final point. It also restores both the totient damping and the excluded Euler factors before identifying the physical $L$-function. These are necessary parts of the proof of the public statement.

% END 07_mellin


% BEGIN 08_review
\section{Mathematical status, imported material, and verification scope}\label{sec:status}

\subsection{What is explained here and what is inherited}
The final mathematical implication is fully displayed: Proposition~\ref{prop:ms} gives Proposition~\ref{prop:mobius} by the sixth-power average, and the latter gives Theorem~\ref{thm:main} by the holomorphic identity \eqref{eq:centralanalytic}. This includes the actual ideal series, finite Euler restoration, the totient correction, the pointwise nonvanishing test, the principal pole, type zero at one, conjugation, and real norm twists.

The technical source lemmas behind Proposition~\ref{prop:ms} are also indispensable. They include the exact cubic theta coefficient and cusp identities, the concrete quadratic-row estimate, the physical fiber decomposition, the progressing canonical reopening identity and rank drop, and the Poisson source identities with their radial tail bounds. Sections~\ref{sec:reflection}--\ref{sec:descent} state their interfaces, definitions, quantitative budgets, and proof mechanisms. A full independent proof of all their prime-exponent cases and analytic normalizations is not supplied by merely reading the final exponent calculation. This manuscript does not present those omitted finite calculations as already checked by a human referee.

The paper uses ordinary Fourier and Mellin analysis, Poisson summation on ideal lattices, gamma-function identities and estimates, finite character orthogonality, reciprocity, ideal counting, and the classical analytic theory of Hecke $L$-functions. In the formal development these are mathematical dependencies with proofs or previously established library results, not new analytic axioms added for the public theorem. The nonstandard organization into canonical states and a finite rank is explained in Section~\ref{sec:descent}; it is an arithmetic induction with explicit invariants. No separate published theorem is being cited as a substitute for that induction.

\subsection{How the literature is used}
Patterson \cite{Patterson} supplies the historical cubic-theta setting. Dunn--Radziwi\l\l{} \cite{DR} supplies related modern work on cubic Gauss sums and level-aspect Voronoi summation. Their main prime asymptotic is conditional on GRH; this paper does not invoke that conditional asymptotic or their GRH-dependent dispersion estimate. The quadratic large-sieve literature \cite{HB,GL} supplies the framework for \eqref{eq:QLS}. The precise concrete-row and angular adaptations are identified with the pinned formal source rather than attributed to those articles.

OAI-003 and the angular extension cited below are source developments. This document does not describe them as peer-reviewed journal publications. A reader must distinguish the question ``does a published theorem have these hypotheses?'' from ``does the concrete source verify those hypotheses?'' and from ``does the formal declaration express the intended analytic object?'' The source references and the frozen comparison evidence are provided to make those questions checkable.

\subsection{What the recorded Lean checks establish}
The frozen release records a native Windows check of fifteen selected theorem targets, including the public $15/16$ statements. The source import closure contains 134 angular modules. The receipt reports statement comparison, an axiom audit, recursive proof-dependency replay in a fresh Lean kernel environment, and a quotient-primitives postcheck. The permitted axioms are
\[
 \texttt{propext},\qquad\texttt{Classical.choice},\qquad\texttt{Quot.sound}.
\]
The negative controls rejected an unproved solution, a changed endpoint, and a widened pole exception. The latter two controls changed definitions of the public proposition, and recursive definition comparison detected them.

The replay uses the same Lean implementation, not an independently implemented kernel. The comparison fixtures were produced from the declared theorem types and definition bodies; they are not an independently authored analytic specification. Challenge fixtures contain intentionally unproved theorem placeholders and are not solution proofs. The source-closure count is not a claim that every unrelated declaration in all 134 files was freshly replayed: the fresh replay follows the recursive dependencies of the selected targets.

Clean portable reproduction and Linux replay remain pending. The release did not perform a clean portable source rebuild of all dependencies, and its Windows driver does not exercise Linux Landlock. No independent human referee report is asserted. The original development and its receipts belong to one auditor's workflow; the separate AI-assisted review is described below. No new Lean replay was performed for this publication edit. The present exposition is a reconstruction: its equations, notation changes, prose explanations, and citations are not themselves certified by Lean. The PDF itself is not Lean-verified.

The stronger $0.8748389$ theorem remains unfinished and is explicitly excluded from this paper. That investigation is not an input to the statements reconstructed here. No detector/count contraction for that stronger target is assumed in the $15/16$ public theorem. Conversely, the $15/16$ replay does not verify a stronger boundary.

\subsection{Separate review of the frozen package}
The separate review reported the following distinct verdicts:
\begin{itemize}[label=\(\bullet\)]
\item Mathematical soundness: \textbf{INCONCLUSIVE}.
\item Scope fidelity: \textbf{ACCEPTED} for the stated unit-compatible angular model.
\item Imported inputs: \textbf{INCONCLUSIVE}.
\item Verification evidence: \textbf{ACCEPTED} within the reviewed execution scope.
\end{itemize}
No decisive defect was found in the portion examined. The review was AI-assisted, not an independent human referee report. It reused the pinned compiler, checker, and dependency cache and was not a clean-room reproduction. It performed new native checking, statement comparison, an axiom audit, kernel replay, a quotient postcheck, a negative control, and fresh compilation of the five public source modules. It did not independently reconstruct the complete inherited reflection, spectral, and recursion machinery. In particular, its two \textbf{INCONCLUSIVE} verdicts are neither acceptance nor rejection of those mathematical questions.

\subsection{Publication and AI provenance}
The public GitHub source/evidence archive is identified in Appendix~\ref{sec:concordance}. The frozen evidence package is the formal certification artifact for the recorded checks; this explanatory manuscript is not that artifact. The execution limits described above continue to apply. This manuscript is prepared for submission to Hexagon; publication there would not constitute peer review.

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.

\subsection{Xenoproof and xenotheorem terminology}\label{sec:xeno}
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 the present epistemic status of the proof, not its origin, length, or use of artificial intelligence.

We use \emph{xenotheorem} for a theorem for which the only currently known proof is a xenoproof. Both terms are provisional epistemic classifications. A xenoproof may cease to be a xenoproof after successful humanization, and a xenotheorem ceases to be a xenotheorem if a sufficiently human-understood proof is developed or identified.

At the time of this publication, the author knows of no independently human-understood proof of this exact $15/16$ angular-Hecke theorem. It is therefore presented provisionally as a xenotheorem.

The purpose of the terminology is to distinguish formal mathematical correctness from human mathematical understanding. These terms do not alter the theorem's scope or the separate review verdicts above.

\subsection{Questions for an independent mathematical reading}
An independent reader can separate three conclusions: whether the mathematical implication is sound, whether the imported results are invoked with their actual hypotheses, and whether the public statement has the claimed scope. Checking the exact source correspondence is a fourth, formalization-specific question. None follows automatically from the others.

For the mathematical reading, the relevant objects are the concrete character \eqref{eq:series}, the actual row \eqref{eq:AZ}, the completed sum \eqref{eq:completed}, the physical reflection \eqref{eq:physicalreflection}, and the canonical energy \eqref{eq:energy}. For quantitative consistency, the relevant choices are the moving mask in \eqref{eq:physicalenergy}, the invariant \eqref{eq:state}, the rank drop \eqref{eq:rankdrop}, the common prime pool, the strict radius $\sigma>1/20$, and the final parameters \eqref{eq:parameters}. For the analytic conclusion, the relevant identities are \eqref{eq:eulerrestore} and \eqref{eq:regularized}. These references give an audit route without treating any component as exempt from scrutiny.

% END 08_review

\appendix

% BEGIN 09_concordance
\section{Frozen source and declaration concordance}\label{sec:concordance}

The angular source described here is publicly released on GitHub. The frozen verification release has tag \texttt{v15-16-2026-10-18} in the repository
\begin{center}\small\url{https://github.com/TheRealDubb/angular-hecke-15-16-xenoproof}.\end{center}
Its exact Git commit is
\begin{center}\small\path{67bb5d2df315fe5ebe7b6ffe0eb4529ffef225de}.\end{center}
Reference~\cite{Angular} links the public release and the source at this commit. The tagged package provides the frozen Lean source, proof exports, pinned OAI-003 source, hashes, and native Windows verification evidence. The proof exports and pinned OAI-003 source are separate release assets bound to the commit by their recorded hashes. The release record reports that the Git bundle was verified and the source ZIP matched the commit.

Later explanatory README edits on \texttt{main} are distinct from the frozen tagged verification release and are not part of its verified theorem package. The public repository is the source/evidence archive; this scholarly manuscript is an explanatory reconstruction. Clean portable reproduction and Linux replay remain pending.

The inherited OAI-003 source is pinned at
\begin{center}\small\path{adc7f1241b42e322a6451854ab7e4b4c146bf78a}\end{center}
in \url{https://github.com/openai/math}. The recorded Lean version is 4.34.1, revision
\begin{center}\small\path{5045d0056413266e57c625dcd7c365b10e377c52},\end{center}
with mathlib revision
\begin{center}\small\path{d13f23b723b8a846827a245b89c10fc7d3f11612}.\end{center}
The exact dependency and executable hashes are in the release's \texttt{DEPENDENCY\_PINS.json}. Its original comparator toolchain file names 4.34.0, while the native build receipt records an explicit 4.34.1 Windows executable. This provenance difference is retained in the release rather than silently described as a tested portable build.

\subsection{The exact endpoint declaration}
In the namespace
\begin{center}\small\path{OAI.SevenEighths.Angular.FifteenSixteenthsFullFamilyRisk},\end{center}
the theorem \texttt{physical\_seed} takes an \texttt{AngularCharacter}, a complex $s$, and exactly the two mathematical hypotheses
\[
 (15:\R)/16<\Rea s,\qquad
 (\chi.k=0\ \Longrightarrow\ \chi.\mathrm{residue}=1\ \Longrightarrow\ s\ne1).
\]
Its conclusion is
\[
 \texttt{FamilyContinuation.LFunction}\ \chi\ s\ne0.
\]
The corresponding \texttt{physical\_seed\_norm\_twist} has $s\ne1+i\tau$ in the pole condition and concludes nonvanishing of \texttt{NormTwist.LFunction}. The retained research suffix \texttt{Risk} is part of the frozen declaration name, not an additional mathematical hypothesis.

\subsection{Reading the source without relying on this paper's notation}
The release's \texttt{SOURCE\_CLOSURE.json} maps every angular module name to its exact relative file and SHA-256 hash. Angular files are under \texttt{snapshot/outputs/ANGULAR\_LEAN/}; inherited modules are under the pinned OAI \texttt{NumberTheory/DirichletL/} tree. The following list uses short module names so that it remains stable across local directory layouts.

\begin{longtable}{@{}p{0.25\textwidth}p{0.70\textwidth}@{}}
\toprule
Mathematical content & Source modules or declarations\\\midrule
\endhead
Admitted family & \sourceid{AngularCharacter}\newline\sourceid{AngularFamilyContinuation.LFunction_eq_series}.\\[5pt]
Type zero; twists & \sourceid{AngularTypeZeroEntire.LFunction_one_ne_zero}\newline\sourceid{AngularNormTwistContinuation}\newline\sourceid{AngularFamilyConjugation}.\\[5pt]
Angular coefficient & \sourceid{AngularCompletedCoefficient}\newline\sourceid{AngularFiniteProjector}\newline\sourceid{AngularHigherProfiles}.\\[5pt]
Cusp reflection & \sourceid{AngularProjectedReflection}\newline\sourceid{AngularPhysicalSmoothedReflection.completedT_reflection}.\\[5pt]
Shifted kernel & \sourceid{AngularGammaMultiplier}\newline\sourceid{AngularReflectedKernel}\newline\sourceid{AngularKernelContour}\newline\sourceid{AngularKernelEnergy}.\\[5pt]
Physical row energy & \sourceid{AngularPhysicalFiberData}\newline\sourceid{AngularPhysicalFiberIdentity}\newline\sourceid{AngularPhysicalRowEnergy.completed_angular_row_energy}.\\[5pt]
Short energy & \sourceid{AngularShortEnergy}\newline\sourceid{AngularSieveDensity.canonicalShortState_from_certificate}.\\[5pt]
State and rank & \sourceid{MeanSquare/UnitRows.CanonicalStateCondition}\newline\sourceid{CubicSieve/ArithmeticBins.fixedDepthRank}\newline\sourceid{CubicSieve/DensityBudgets}.\\[5pt]
One-step reopening & \sourceid{RowCompletion/CubicReopening.progressingCanonicalFamily_closed_step}\newline\sourceid{AngularSieveDensity.canonicalLog_actual_step}.\\[5pt]
Finite induction & \sourceid{AngularSieveDensity.outsideLogEnergy_finite_rank}\newline\sourceid{outsideLogEnergy_small_power}.\\[5pt]
Density and source & \sourceid{AngularInitialDensity}\newline\sourceid{AngularNonzeroSource}\newline\sourceid{AngularPoissonMoment}.\\[5pt]
Sixth-power average & \sourceid{AngularSixthPower}\newline\sourceid{Mellin/SixthPowerAverage}\newline\sourceid{AngularSeedFifteenSixteenthsMomentRisk.outside_totient_moebius_bound}.\\[5pt]
Mellin and Euler factors & \sourceid{AngularWeightedMellin}\newline\sourceid{AngularFiniteRestoration}\newline\sourceid{AngularSeedRegularization}\newline\sourceid{AngularSeedFifteenSixteenthsMellinRisk}.\\[5pt]
Public conclusion & \sourceid{AngularSeedFifteenSixteenthsNonvanishingRisk}\newline\sourceid{AngularSeedFifteenSixteenthsFullFamilyRisk}\newline\sourceid{AngularSeedFifteenSixteenthsStatementRisk}.\\
\bottomrule
\end{longtable}

The primary evidence files are the release's \texttt{THEOREM\_SCOPE.md}, \texttt{VERIFICATION\_STATUS.md}, \texttt{SOURCE\_CLOSURE.json}, and the public-bundle replay receipt, log, verified manifest, and negative-control record under \path{evidence/windows/public15_16/}. Hashes establish which files were checked; they are not an independent proof of the semantic identification with the intended analytic theorem.

% END 09_concordance


% BEGIN 11_interfaces
\section{Interfaces and the remaining independent mathematical checks}\label{sec:interfaces}

This appendix records the dependency contracts used in the exposition. The source names refer to the frozen files located by Appendix~\ref{sec:concordance}; they do not refer to a later development with similar names. Each entry specifies what is needed, how the present application supplies it, and what has not been independently reconstructed here. Routine finite-sum rearrangements and the elementary inequalities proved in the text are not additional imported hypotheses.

\subsection{The physical character and analytic continuation}
\paragraph{Needed interface.}
An admitted triple defines a bounded multiplicative ideal coefficient and the series \eqref{eq:series}. Its continuation agrees with that series on the initial half-plane. Nonzero type has an entire continuation. At type zero, a holomorphic regularization agrees with $(s-1)L$ off $1$, and the nonprincipal character has $L(\chi,1)\ne0$. Conjugation and real norm twists preserve the series identifications used in Section~\ref{sec:mellin}.

\paragraph{Hypotheses and application.}
The field and embedding are fixed; the modulus is nonzero; the finite character is extended by zero; and the unit equation is imposed in the definition of the family. Generator independence and the bounded norm are explained in Section~\ref{sec:statement}. The comparison at negative type uses $k\ne0$, as required by the cited conjugation theorem. The type-zero argument distinguishes a nonprincipal finite part from the principal one at $s=1$. An imprimitive character retains its deleted Euler factors, which are nonzero at $1$; it is never replaced by a primitive character without that correction.

\paragraph{Support and remaining check.}
Unit descent, conjugation of the initial series, and the vertical-shift identity are explained here. The theta construction of the actual continuation, its agreement with the series, and the type-zero nonvanishing theorem at one are inherited formal mathematics. The latter uses the classical finite-order Hecke input; it is not supplied by the $15/16$ argument. An independent check must identify this precise continuation and the imprimitive factors, rather than checking only a function named $L$.
\src{AngularCharacter; AngularFamilyContinuation.LFunction_eq_series; AngularTypeZeroEntire.LFunction_one_ne_zero; AngularFamilyConjugation.LFunction_conjugate; AngularNormTwistContinuation; AngularSeedRegularization}

\subsection{The completed coefficients and exact angular reflection}
\paragraph{Needed interface.}
The Fourier coefficient at the actual cubic theta cusps must equal the completed coefficient in \eqref{eq:completed}, with its primary phase, cube weight, trace character, and order-one derivative scalar. Positive-order differentiation must give \eqref{eq:derivphase} and \eqref{eq:cusp}; smoothing must then give \eqref{eq:physicalreflection} with exactly the kernel \eqref{eq:kernel}.

\paragraph{Hypotheses and application.}
The reflected character has type $-n$ with $n\in\N$. A nonzero denominator $c$ satisfies $(c)\subseteq(9)\frakf$; the finite quotient is finite. The test is smooth and supported in a positive compact interval; $X>0$. These conditions are stated at the physical identity in Section~\ref{sec:reflection}. The total derivative order is $n+1\ge1$, so the constant mode is removed even for $n=0$. Each cusp datum is the actual finite-twist datum, not an arbitrary matrix with a formally chosen multiplier.

\paragraph{Support and remaining check.}
The phase calculation, the effect of the positive derivative, the shifted gamma quotient, and the contour-decay mechanism are explained here. The precise Fourier coefficient formula, the level-two transformation identity, all cusp scales, and the physical Mellin/Bessel identification are inherited formal inputs. A literature description of cubic theta functions does not establish these normalizations. The independent task is to verify these identities for the stated functions, including the zero additive twist and convergence at both ends of the Mellin integral.
\src{Arithmetic/IdealMobius.completedT; AngularCompletedCoefficient; AngularHigherProfiles; AngularProjectedReflection.datum_reflection; AngularProjectedReflection.finiteProjector_mellin_reflection; AngularPhysicalSmoothedReflection.completedT_reflection; AngularGammaMultiplier; AngularKernelContour}

\subsection{Quadratic energy and actual physical models}
\paragraph{Needed interface.}
The concrete quadratic operator estimate and its supported-product-column consequence must hold for common coefficients. The reflected physical row must equal its finite fiber expression before that estimate is used. This supplies Proposition~\ref{prop:completedenergy} and the theta-model estimate needed for the short part of a canonical state.

\paragraph{Hypotheses and application.}
The squarefree quadratic indices avoid $2$ and $3$ and have bounded norm; finite set indexing is injective. General supported products are treated by square-part decomposition and product fibers, as described in Section~\ref{sec:energy}. The kernel separation gives a single column array for each integration parameter. Physical characters have type $-n$, a finite part factoring through fixed $q\ne0$, a nonzero moving mask, a squarefree label, and nonzero row ideals in the stated dyadic range. The mask norm remains in the bound. The actual-model identity is supplied by the physical fiber construction; it is not an assumption left on the public character.

The ray-orbit application uses \texttt{exists\_orbit\_character}: every allowed raw ray twist has the same masked completed sum as an admitted character of the same type. Fixed-shell models then give dyadic models at all positive rescaled column sizes. The height twist is placed in the smooth test, where it preserves the support. This discharges the model predicate in the short-energy theorem, including cube-rescaled sizes below one.

\paragraph{Support and remaining check.}
Product multiplicity, common-coefficient separation, and the role of the conductor and mask are explained here. The sharp concrete quadratic norm, the exact finite fiber identity, branch counting, the weighted sum over powerful parts, and the conversion to dyadic models remain inherited formal inputs. Goldmakher--Louvel is cited for the classical framework; it is not asserted to apply to an arbitrary angular row family. Checking the concrete arithmetic identifications and any literature hypotheses used inside the inherited proof remains necessary for independent certification.
\src{QuadraticSieve/LogarithmicLoss.finite_family_quadratic_large_sieve; MeanSquare/TransformedColumns.bounded_supported_quadratic_norm; QuadraticSieve/ProductColumns.product_quadratic_norm; AngularKernelEnergy.completed_smooth_quadratic; AngularPhysicalFiberIdentity.completedT_eq_reflectedFiber_idealValue; AngularPhysicalRowEnergy.actual_exactModels; AngularPhysicalRowEnergy.completed_angular_row_energy; AngularSieveModels.actual_fixedShellModels; AngularSieveModels.actual_canonicalThetaModels; AngularShortEnergy}

\subsection{The complete state, terminals, and reopening}
\paragraph{Needed interface.}
The state is exactly \eqref{eq:state}, together with its coefficient, positivity, and label conditions. A retained long bin must produce a state with the same conditions and smaller rank. The short part has \eqref{eq:shortenergy}, and the long part plus the smaller-rank bounds gives \eqref{eq:step}. The terminal estimate applies whenever rank is zero \emph{or} $X\le1$.

\paragraph{Hypotheses and application.}
The prime pool consists of distinct nonzero prime ideals, pairwise coprime, away from $3$ and with odd residue characteristic; these follow from the outside-prime construction and $S$ containing the fixed bad primes. Its primary generators have nonzero norm. The base coefficient has norm at most one and the fixed ray operations preserve the permitted coefficient class. The budgets require $0<\eta\le1/1000$, $3000\eta\le1/80$, $Z\ge e^{9000}$, and $2\Nm(e_S)\le Z^{1/80}$, where $e_S$ is the fixed excluded-prime generator. The last condition is met above a fixed threshold because $S$ is fixed.

Reopening is applied only after the two terminal tests, so $X>1$. The mass bound then gives $X,F\le Z^3$. The cutoff satisfies $D\ge e^AX$ at that generation. The retained nonzero-frequency bins satisfy progress and the radial cap, giving \eqref{eq:childscales}--\eqref{eq:childratio}. Section~\ref{sec:rankgeometry} derives the strict rank decrease and both numerical invariants from those inequalities; Section~\ref{sec:terminals} proves the terminal counting argument. Choosing the common pool for the largest recursive support window preserves the cutoff hypothesis at every depth.

\paragraph{Support and remaining check.}
The scalar closure and the finite induction are explained here, including the order of choices of the height degree, child profiles, and constants. The full arithmetic partition, local exponent identities, finite fibers, radial-tail estimates, and the inequalities at the retained-bin interface remain inherited. Independent checking must show that every actual term is included with its multiplicity, not merely verify that a hypothetical child with those inequalities would contract. The exact source declarations are given throughout Section~\ref{sec:descent}.
\src{MeanSquare/UnitRows.CanonicalStateCondition; MeanSquare/UnitRows.canonicalStateCondition_retained; MeanSquare/CanonicalTailBounds.globalRetained_canonical_geometry; RowCompletion/CubicReopening.progressingCanonicalFamily_closed_step; AngularSieveDensity.canonicalShortState_from_certificate; AngularSieveDensity.canonicalLog_actual_step; AngularSieveDensity.outsideLogEnergy_finite_rank; CubicSieve/CanonicalLogEnergy.canonicalLogEnergy_terminal}

\subsection{Paired density and the physical mean square}
\paragraph{Needed interface.}
Uniform canonical energy bounds for the two oriented coefficients must control the actual paired density for every finite array satisfying \eqref{eq:initialgeometry}. The original row square must satisfy \eqref{eq:poissoncomparison}, with a retained-source bound, a radial-tail bound, and the stated zero-source correction. Together these yield Proposition~\ref{prop:ms} without a remaining density premise.

\paragraph{Hypotheses and application.}
The density quantifiers and positive scale bounds are given in Section~\ref{sec:descent}. The projected labels are admissible; all rows are nonzero and lie in their disk. The full initial mask includes the fixed excluded norm. The two ray coefficients lie in the permitted orbit. For a physical character of type $k=n\ge0$, the required base is the coefficient of its conjugate, of type $-n$; \texttt{physical\_initial\_density} supplies it. Strict $\sigma>1/20$ permits the positive radial cutoff parameter. An enlarged pool is harmless because the original $W$ support makes added columns vanish.

\paragraph{Support and remaining check.}
The Cauchy--Schwarz transfer, quantifier order, cutoff enlargement, and final exponent comparison are explained here. The exact first and second Poisson identities, the interpretation of their source arrays, the zero-frequency calculation, and the uniform radial estimates remain inherited formal inputs. In particular, dropping the final nonpositive term is legitimate only after it has been included with the correct sign in the identity.
\src{RowCompletion/DensityTransfer.densityChildEnergy_from_canonical_heights; AngularInitialDensity.hasInitialCanonicalDensityAtRadius_of_theta; AngularInitialDensity.physical_initial_density; AngularNonzeroSource.nonzero_source_bound; AngularPoissonMoment.outside_mean_square_of_canonical_density_at_radius; AngularPoissonMoment.physical_outside_mean_square}

\subsection{Sixth powers, damping, and the final analytic implication}
\paragraph{Needed interface.}
The ideal-lattice Poisson remainder must give \eqref{eq:R} uniformly in $Y\ge1$. Lattice counting and the at-most-six multiplicity give \eqref{eq:cauchy}. The resulting cancellation gives a holomorphic Mellin transform on $\Rea s>15/16$, and the Euler identity must concern the actual series rather than an unrelated reciprocal model.

\paragraph{Hypotheses and application.}
The averaging test is fixed, smooth, nonnegative, supported away from zero, and has nonzero zero-frequency coefficient. The column coefficients have absolute value at most a fixed bound and are supported at norm $O(Z)$. The sixth-power image lies in the permitted nonzero row disk for the chosen $Y$. The continuation uses an $\varepsilon$ smaller than the distance of a compact subset to the boundary, not one fixed $\varepsilon$ throughout the whole half-plane. The local Euler correction is normally convergent for $\Rea s>0$, and its denominator is nonzero there. At each proposed zero a new smooth test supplies \eqref{eq:nonzeroW}. Type zero at $1$ uses the separately stated classical nonvanishing input, with only the principal pole excluded.

\paragraph{Support and remaining check.}
Sections~\ref{sec:average}--\ref{sec:mellin} explain these deductions, including the multiplicity, exponent arithmetic, Euler-factor orientation, and point-dependent test. The uniform ideal-lattice remainder and its source normalizations are inherited; their required conclusion is explicitly stated in Lemma~\ref{lem:average}. The analytic continuation inputs are those in the first entry of this appendix. No theorem for negative-type sextic rows is used. No statement on the boundary, growing conductor, growing angular order, or the earlier stronger target follows from this argument.
\src{AngularSixthPower.average_remainder_small_power; Mellin/SixthPowerAverage.average_tsum_cauchy; AngularSeedFifteenSixteenthsMomentRisk.outside_totient_moebius_bound; AngularWeightedMellin; AngularFiniteRestoration; AngularSeedFifteenSixteenthsNonvanishingRisk.physical_seed_all_types; AngularSeedFifteenSixteenthsFullFamilyRisk.physical_seed_norm_twist}

\subsection{What this revision does and does not certify}
The revision preserves the nonnegative-type restriction at the physical mean-square stage and makes both terminal cases explicit. It adds the retained-child scalar closure, elementary terminal count, product-column reduction, ray-orbit realization, and dependency interfaces. These are explanatory and source-correspondence improvements, not a new kernel replay or an independent proof of every inherited arithmetic lemma.

The separate review verdicts remain those in Section~\ref{sec:status}: mathematical soundness and imported inputs are \textbf{INCONCLUSIVE}. A complete human certification would require the independent checks listed above. The earlier Track~2B objective sought a signed recursive estimate yielding a boundary below $0.8749570194201$; the present strict $15/16=0.9375$ statement has a different family scope and does not complete that objective. The unfinished $0.8748389$ campaign is also excluded.

% END 11_interfaces


% BEGIN 10_references
\clearpage
\phantomsection
\addcontentsline{toc}{section}{References}
\begin{thebibliography}{9}
\raggedright

\bibitem{Patterson}
S.~J. Patterson,
\emph{A cubic analogue of the theta series},
Journal f\"ur die reine und angewandte Mathematik \textbf{296} (1977), 125--161.
\href{https://doi.org/10.1515/crll.1977.296.125}{doi:10.1515/crll.1977.296.125}.
Classical background for the cubic theta function.

\bibitem{HB}
D.~R. Heath-Brown,
\emph{A mean value estimate for real character sums},
Acta Arithmetica \textbf{72} (1995), no.~3, 235--275.
\href{https://doi.org/10.4064/aa-72-3-235-275}{doi:10.4064/aa-72-3-235-275}.
Classical quadratic large-sieve background.

\bibitem{GL}
L. Goldmakher and B. Louvel,
\emph{A quadratic large sieve inequality over number fields},
Mathematical Proceedings of the Cambridge Philosophical Society
\textbf{154} (2013), no.~2, 193--212.
\href{https://doi.org/10.1017/S0305004112000370}{doi:10.1017/S0305004112000370}.
Author version: \url{https://arxiv.org/abs/1112.1642}.
Theorem~1.1 is the fixed-modulus quadratic Hecke-family inequality discussed in Section~\ref{sec:energy}.

\bibitem{DR}
A. Dunn and M. Radziwi\l\l,
\emph{Bias in cubic Gauss sums: Patterson's conjecture},
Annals of Mathematics \textbf{200} (2024), no.~3, 967--1057.
\href{https://doi.org/10.4007/annals.2024.200.3.3}{doi: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.

\bibitem{OAI}
OpenAI, \emph{OAI-003 source development}, repository \texttt{openai/math},
revision \path{adc7f1241b42e322a6451854ab7e4b4c146bf78a}.
\url{https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a}.
Pinned source material; no peer-reviewed publication status is asserted here.

\bibitem{Angular}
T. Winarski,
\emph{Angular Hecke $15/16$ frozen source and native Windows verification evidence},
public GitHub repository \texttt{TheRealDubb/angular-hecke-15-16-xenoproof},
release \texttt{v15-16-2026-10-18}, commit
\path{67bb5d2df315fe5ebe7b6ffe0eb4529ffef225de}.
\href{https://github.com/TheRealDubb/angular-hecke-15-16-xenoproof/releases/tag/v15-16-2026-10-18}{Tagged release and evidence assets};
\href{https://github.com/TheRealDubb/angular-hecke-15-16-xenoproof/tree/67bb5d2df315fe5ebe7b6ffe0eb4529ffef225de}{source at the frozen commit}.
Source closure, exact theorem scope, dependency pins, and replay evidence as specified in Appendix~\ref{sec:concordance}. This source/evidence release is distinct from later explanatory README edits on \texttt{main}; no independent human certification is asserted.
\end{thebibliography}

% END 10_references

\end{document}