\documentclass[11pt,a4paper]{article} \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage[margin=27mm,headheight=14pt]{geometry} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage{microtype,booktabs,array,enumitem} \usepackage{needspace} \usepackage[hidelinks]{hyperref} \usepackage{doi} \usepackage{fancyhdr} \setlength{\parindent}{1.2em} \setlength{\parskip}{0pt} \setlength{\emergencystretch}{1.5em} \allowdisplaybreaks[1] \numberwithin{equation}{section} \newtheorem{theorem}{Theorem}[section] \newtheorem{proposition}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newcommand{\R}{\mathbb R} \newcommand{\C}{\mathbb C} \newcommand{\N}{\mathbb N} \newcommand{\eps}{\varepsilon} \newcommand{\ii}{\mathrm i} \newcommand{\dd}{\,\mathrm d} \newcommand{\pos}[1]{\left(#1\right)_+} \newcommand{\MT}{\mathrm{MT}} \DeclareMathOperator{\supp}{supp} \DeclareMathOperator{\Iso}{Iso} \DeclareMathOperator{\Tr}{Tr} \DeclareMathOperator{\spanop}{span} \DeclareMathOperator{\Proj}{Proj} \pagestyle{fancy} \fancyhf{} \fancyhead[L]{\small C. Kim} \fancyhead[R]{\small Isolated zeros of the Riemann zeta function} \fancyfoot[C]{\thepage} \renewcommand{\headrulewidth}{0.3pt} \title{An Explicit Lower Bound for the Proportion of\\ Isolated Zeros of the Riemann Zeta Function} \author{Cheolmin Kim\\[3pt] \small Independent Researcher, Republic of Korea} \date{11 November 2026\\[4pt] \small Preprint v0.4 --- not peer reviewed} \hypersetup{pdftitle={An Explicit Lower Bound for the Proportion of Isolated Zeros of the Riemann Zeta Function}, pdfauthor={Cheolmin Kim},pdfsubject={Preprint v0.4; unconditional isolated-zero proportion}} \begin{document} \maketitle \begin{abstract} We study isolation in the full sequence of nontrivial zeros of the Riemann zeta function with positive ordinate, counted with multiplicity. For every fixed $01$ and $c>0$, define \begin{equation}\label{eq:B-definition} \begin{split} B_0(X,c)=\#\bigg\{n\ge2:\;&0<\gamma_n\le X,\\[-2pt] &\min(\gamma_{n+1}-\gamma_n,\gamma_n-\gamma_{n-1}) >\frac{2\pi c}{\log X}\bigg\}. \end{split} \end{equation} A repeated ordinate creates a zero gap. The upper neighbor of the last zero counted by $N(X)$ is still taken from the infinite sequence, and the condition $n\ge2$ excludes its first member. These conventions ensure that $B_0(X,c)$ tests isolation in the full array rather than in a selected subset. Every counted zero is simple and lies on the critical line, since a zero off the critical line has a distinct reflection mate $1-\overline\rho$ at the same ordinate. Simplicity alone, however, gives no control of the two neighboring gaps. \subsection*{Background} Pair correlation has long been used to obtain lower bounds for the proportion of simple zeros. Assuming the Riemann hypothesis, Montgomery \cite{Montgomery1973} showed that at least two thirds of the zeros are simple. Montgomery and Taylor improved the proportion to $\frac32-\frac1{\sqrt2}\cot(1/\sqrt2)=0.67250\ldots$ by optimizing the test kernel \cite{Montgomery1975}; see also Cheer and Goldston \cite[Section~2]{CheerGoldston1993} for an account of this method. Baluyot, Goldston, Suriajaya and Turnage-Butterbaugh \cite{BGSTB2024} subsequently established an unconditional version of Montgomery's pair-correlation theorem. The same numerical constant was later obtained unconditionally for zeros that are simple and lie on the critical line, by Alp\"oge and Furman \cite[Theorem~A]{AlpogeFurman2026} and, by a different argument, Lamzouri \cite[Theorem~1.1]{LamzouriSimple2026}. Isolation is a stronger condition: a simple zero can still have an arbitrarily close neighbor. In 2024, Gonek and Sahay \cite[Section~1]{GonekSahay2024} noted that no unconditional result was known even for infinitely many pairs of consecutive gaps meeting the threshold $2\pi c/\log T$ with a single fixed $c>0$. Lamzouri \cite[Theorem~1.1]{Lamzouri2026} answered this question with a positive proportion: for the counting function \eqref{eq:B-definition}, he proved the unconditional lower bound $0.6552\ldots$ for sufficiently small fixed $c$, and $0.50875$ at $c=1/6$. Ang\'on, Ross, Tang and Zhao \cite[Theorem~1]{AngonRossTangZhao2026} also obtained lower proportions for two, three and four consecutive gaps, including $0.3450014\ldots$ for two consecutive gaps each at least $2\pi c/\log X$, for every fixed $01/2$, put $y=(\beta-1/2)\log X/(2\pi)$, and write $v_+=\max(v,0)$. The isolation inequality involves the positive part of the deficit $H_f(y)$ defined in \eqref{eq:transfer-defect}. In place of a bound $[H_f(y)]_+\le\alpha(f)y$, we use $[H_f(y)]_+\le\ell(y-a)_+$ with $a=6/5$ and $\ell=663/1000$. This majorant charges the positive deficit only for normalized displacement beyond $a$. Every zero remains in the counted array, and the pair-energy term is retained. The gap loss is controlled separately and uniformly in the test density. \Needspace{9\baselineskip} A positive real shift in Young's mollified second moment \cite[Lemma~3]{Young2010} gives the matching truncated moment: \[ \limsup_{X\to\infty}\frac1{N(X)} \sum_{\substack{0<\gamma\le X\\\beta>1/2}}(y-a)_+ \le D_P(a,\theta)=\frac{\log m_P(2\pi a,\theta)}{4\pi}. \] The fixed inputs and the functions $m_P$, $D_P$ are specified in \eqref{eq:fixed-parameters}--\eqref{eq:D-definition}. Positive real shifts already lie in Young's complex-shift formula; the same main term also occurs in Conrey's Gaussian formulation \cite[\S5, Proposition, p.~11]{Conrey1989}. The distinction between truncated and untruncated displacement is quantitatively important. Conrey's explicit untruncated estimate \cite[Theorem~3]{ConreyBAMS1989} gives the constant $0.0806$ used by Lamzouri. The density estimate in \cite[Theorem~2]{ConreyBAMS1989} has an unspecified implied constant and by itself does not give an explicit truncated cost. For the fixed inputs below, $m_P\approx1.000618744$ and $D_P\approx0.0000492228663$. Thus the new penalty is $\ell D_P\approx0.0000326347603$, compared with approximately $0.0173$ in the earlier estimate, while the pair-energy constant is unchanged. The smaller off-line penalty provides the numerical gain in the small-gap lower bound; stating the explicit range $01/2), \end{equation} write \begin{equation}\label{eq:MT-cost} C_{\mathrm{MT}}=\frac12+\frac{1}{\sqrt2}\cot(1/\sqrt2). \end{equation} The proof establishes the more informative bound \begin{equation}\label{eq:quantitative-bound} \liminf_{X\to\infty}\frac{B_0(X,c)}{N(X)} \ge 2-C_{\mathrm{MT}}-\ell D_P(a,\theta)-6\pi^2c^2 \qquad \left(00.67246806299>0.672468. \] Within this pair-energy method, $2-C_{\mathrm{MT}}$ is the value reached when the off-line and gap costs vanish. \subsection*{Comparison with other counting results} Knausg{\aa}rd \cite[Theorem~1.3]{Knausgard2026} gives the computer-assisted lower bound $1669159/2478195=0.673538\ldots$ for zeros that are simple and lie on the critical line. The simple-zero results of Alp\"oge--Furman, Lamzouri \cite{LamzouriSimple2026}, and Knausg{\aa}rd do not require a positive lower bound on both neighboring gaps in the full zero array. By contrast, the two-gap result of Ang\'on, Ross, Tang and Zhao \cite[Theorem~1]{AngonRossTangZhao2026} concerns consecutive gaps and thus directly relates to two-neighbor isolation, up to endpoint conventions; it uses non-strict inequalities and a much larger gap range. Theorem~\ref{thm:main} improves the lower proportion in its much smaller fixed-gap range. \subsection*{Conventions} All sums over zeta zeros include multiplicity unless they are explicitly over distinct support points or distinct conjugate pairs. We use the standard analyticity and functional equation of $\zeta$, its absolutely convergent Dirichlet series in $\Re s>1$, polynomial growth on fixed vertical strips, Jensen's formula, and \[ N(X)=\frac{X}{2\pi}\log\frac{X}{2\pi} -\frac{X}{2\pi}+O(\log X). \] All asymptotic statements involving a test function are for that function fixed before the height tends to infinity. \section{A shifted moment and a global displacement bound} \label{sec:young-boundary} We derive the truncated displacement estimate used in the isolation bound. Young's formula first controls the mollified zeta function on a short horizontal shift of the critical line. Jensen's inequality and Littlewood's lemma convert that mean square into a sum of zero displacements; the last step expresses every displacement using the same final height $X$. Throughout this section $P$ is any fixed real polynomial with $P(0)=0$ and $P(1)=1$, and $0<\theta<1/2$ is fixed. We specialize to \eqref{eq:fixed-parameters}--\eqref{eq:P-definition} only in the numerical application. All estimates in this section are unconditional. \subsection{The external shifted-moment formula} For $U>1$, put $L_U=\log U$, $M=U^\theta$, and \begin{equation}\label{eq:young-A} A_U(t)=\sum_{n\le M}\frac{\mu(n)}{n^{1/2+it}} P\!\left(\frac{\log(M/n)}{\log M}\right). \end{equation} Here and below a sum with $n\le M$ is over positive integers, whether or not $M$ is an integer. \Needspace{14\baselineskip} \begin{theorem}[Young's shifted-moment input]\label{thm:young-input} Let $w_U$ be a real smooth function satisfying \[ 0\le w_U\le1,\qquad \operatorname{supp}w_U\subset[U/4,2U], \qquad w_U^{(j)}(t)\ll_j (U/\log U)^{-j}\quad(j\ge0). \] For every fixed $R>0$, uniformly for complex $|\alpha|,|\beta|\le R/\log U$, \begin{align} &\int_{\R}w_U(t)\zeta(1/2+\alpha+it) \zeta(1/2+\beta-it)|A_U(t)|^2\,dt \notag\\ &\hspace{25mm} =c_U(\alpha,\beta)\int_{\R}w_U(t)\,dt +O_{P,\theta,R,w}(U/\log U),\label{eq:young-shifted-input} \end{align} where \begin{equation}\label{eq:young-main-external} \begin{split} c_U(\alpha,\beta)=1+\frac1\theta \left.\frac{\partial^2}{\partial x\,\partial y} \left\{M^{-\beta x-\alpha y} \int_0^1\!\int_0^1 U^{-v(\alpha+\beta)}P(x+u)P(y+u)\,du\,dv\right\} \right|_{x=y=0}. \end{split} \end{equation} The dependence on $w$ is through fixed bounds for its scaled derivatives; it is uniform over a family satisfying those bounds. \end{theorem} This is \cite[Lemma~3, equations (3.1)--(3.3)]{Young2010}, with $T$ renamed $U$. Young's mollifier, evaluated on his reference line, is exactly \eqref{eq:young-A}; its value there is independent of the auxiliary reference-line shift. The complex-shift statement permits positive real $\alpha$ and $\beta$ directly. Although an intermediate formula in \cite[Lemma~6]{Young2010} first assumes $|\alpha+\beta|\gg1/\log U$, the proof removes that restriction by analyticity and the maximum-modulus principle; the displayed Lemma~3 has no such restriction. We use that lemma, including its uniformity, as an external analytic theorem. For $0\le\delta\le R/\log U$, define \begin{equation}\label{eq:shifted-F} \begin{split} \sigma&=\frac12+\delta,\qquad r_U=\delta\log U,\\ \psi_{U,\delta}(s) &=\sum_{n\le M}\mu(n)n^{-s+\delta} P\!\left(1-\frac{\log n}{\log M}\right),\qquad F_{U,\delta}(s)=\zeta(s)\psi_{U,\delta}(s). \end{split} \end{equation} In particular $\psi_{U,\delta}(\sigma+it)=A_U(t)$. On putting $\alpha=\beta=\delta$ in \eqref{eq:young-main-external}, the factor depending on $x,y$ is $e^{-\theta r_U(x+y)}$. Differentiating the polynomial product therefore gives \[ \left.\partial_x\partial_y \{e^{-\theta r_U(x+y)}P(x+u)P(y+u)\}\right|_{x=y=0} =\bigl(P'(u)-\theta r_UP(u)\bigr)^2. \] Integration in $v$ now proves \begin{equation}\label{eq:young-positive-moment} \int_{\R}w_U(t)|F_{U,\delta}(\sigma+it)|^2\,dt =m_P(r_U,\theta)\int_{\R}w_U(t)\,dt+O(U/\log U). \end{equation} The function $m_P$ is given by \eqref{eq:moment-cost}, with the continuous value \[ m_P(0,\theta)=1+\frac1\theta\int_0^1P'(u)^2\,du. \] It is smooth for $r_U\ge0$, is at least $1$, and is bounded together with its first derivative on each fixed compact interval. Thus $\log m_P$ is Lipschitz on such an interval. For comparison with the earlier formulation in \cite[\S5, Proposition, p.~11]{Conrey1989}, first take $r_U>0$ and set $t=\theta r_U$. The same main term can be written as \begin{equation}\label{eq:conrey-young-algebra} \frac{\displaystyle\int_0^1(P'+tP)^2\,du -e^{-2r_U}\displaystyle\int_0^1(P'-tP)^2\,du}{2t} =1+\frac{1-e^{-2r_U}}{2t}\int_0^1(P'-tP)^2\,du. \end{equation} Indeed, $2\int_0^1PP'\,du=P(1)^2-P(0)^2=1$, so the difference between the two integrals without the exponential factor is $2t$. Thus \eqref{eq:conrey-young-algebra} identifies the two forms of the existing main term, with the sign and normalization of the positive shift made explicit. Both sides extend continuously to $r_U=0$. \subsection{From a smooth moment to an unweighted logarithmic integral} Littlewood's lemma uses an unweighted integral of $\log|F|$ on a vertical segment. A smooth plateau first bounds the mean square on that segment, and Jensen's inequality then supplies the logarithmic integral with the required constant. \begin{lemma}[Plateau and Jensen]\label{lem:plateau-jensen} For the function in \eqref{eq:shifted-F}, uniformly for $0\le r_U\le R$, \begin{align} \int_{U/2}^{U}|F_{U,\delta}(\sigma+it)|^2\,dt &\le\frac U2m_P(r_U,\theta)+O(U/\log U), \label{eq:unweighted-square}\\ \int_{U/2}^{U}\log|F_{U,\delta}(\sigma+it)|\,dt &\le\frac U4\log m_P(r_U,\theta)+O(U/\log U). \label{eq:unweighted-log} \end{align} The logarithmic integral is a locally integrable improper integral when the vertical segment contains zeros. \end{lemma} \begin{proof} Choose a fixed smooth function $\chi$ with $0\le\chi\le1$, $\chi(v)=0$ for $v\le0$, and $\chi(v)=1$ for $v\ge1$. For $\Delta=U/\log U$, take \[ w_U(t)=\chi\!\left(\frac{t-U/2+\Delta}{\Delta}\right) \chi\!\left(\frac{U+\Delta-t}{\Delta}\right). \] Then $w_U=1$ on $[U/2,U]$, its support is contained in $[U/2-\Delta,U+\Delta]\subset[U/4,2U]$ for large $U$, and $\int w_U=U/2+O(\Delta)$. All scaled derivative bounds are fixed. Enlarging a nonnegative integral and applying \eqref{eq:young-positive-moment} proves \eqref{eq:unweighted-square}. The function $F_{U,\delta}$ is analytic near this high vertical segment and is not identically zero. A zero of order $k$ contributes $k\log|t-t_0|$ plus a bounded function locally, so its logarithm is integrable. Jensen's inequality for the concave logarithm, applied to $|F|^2$ on an interval of length $U/2$, gives \[ \int_{U/2}^{U}\log|F(\sigma+it)|\,dt \le\frac U4\log\!\left(\frac2U \int_{U/2}^{U}|F(\sigma+it)|^2\,dt\right). \] The same inequality follows by first replacing $|F|^2$ by $|F|^2+\varepsilon$ and passing to the limit. Since $m_P\ge1$ and is bounded on $[0,R]$, the logarithm of the error in \eqref{eq:unweighted-square} is $O(1/\log U)$. This proves \eqref{eq:unweighted-log}. The factor $U/4$ includes both the interval length and $\log|F|=\tfrac12\log|F|^2$. \end{proof} \subsection{Horizontal arguments of the mollified zeta function} The horizontal edges in Littlewood's identity require a bound on a continuous argument of $F$. The following lemma obtains it from Jensen's formula and also counts the mollifier zeros needed when a rectangle boundary is moved past a zero ordinate. \begin{lemma}[Uniform horizontal-boundary bound] \label{lem:horizontal-argument} Keep $P,\theta,R$ fixed and let $F=F_{U,\delta}$ be as in \eqref{eq:shifted-F}. For sufficiently large $U$, \begin{equation}\label{eq:right-edge} F(2+it)=1+O_{P,\theta,R}(1/\log U) \quad\hbox{uniformly for real }t. \end{equation} Suppose $U/3\le t\le3U/2$ and $2/5\le b\le\sigma$. If $F$ has no zero on $[b,2]+it$, continue its argument from the principal value at $2+it$ along that segment. Then \begin{equation}\label{eq:horizontal-arg-bound} \sup_{b\le x\le2}|\arg F(x+it)|\ll_{P,\theta,R}\log U. \end{equation} The constant does not depend on the distance of $t$ from an ordinate of a zero. Moreover, every box \[ \sigma\le\Re s\le2,\qquad |\Im s-t_0|\le1, \qquad U/3\le t_0\le3U/2, \] contains $O_{P,\theta,R}(\log U)$ zeros of $F$, with multiplicity. \end{lemma} \begin{proof} Write $B=\max_{[0,1]}|P|$ and $D=\max_{[0,1]}|P'|$. For $n\le M$ we have $\delta\log n\le R\theta$ and \begin{align*} \left|n^\delta P\!\left(1-\frac{\log n}{\log M}\right)-1\right| &\le B|n^\delta-1| +\left|P\!\left(1-\frac{\log n}{\log M}\right)-P(1)\right|\\ &\le\left(BRe^{R\theta}+\frac D\theta\right) \frac{\log n}{\log U}. \end{align*} Comparison with the absolutely convergent Dirichlet series for $1/\zeta(2+it)$ gives \[ \left|\psi_{U,\delta}(2+it)-\frac1{\zeta(2+it)}\right| \ll\frac1{\log U}\sum_{n\ge1}\frac{\log n}{n^2} +\sum_{n>M}\frac1{n^2} \ll\frac1{\log U}. \] The bound $|\zeta(2+it)|\le\zeta(2)$ proves \eqref{eq:right-edge}. In particular, for large $U$, $\Re F(2+it)\ge3/4$, the principal logarithm is continuous along the whole right edge, and $|\log F(2+it)|\ll1/\log U$. We next give a growth bound on the disks needed for Jensen's formula. For $|z-2|\le3$ and the indicated heights $t$, the numbers $z\pm it$ have real part in $[-1,5]$ and imaginary part of size comparable to $U$. They stay away from the sole pole of $\zeta$. Euler--Maclaurin summation, truncated at $N=\lceil U\rceil$ and with the fourth-order Bernoulli remainder, gives uniformly in this strip \[ |\zeta(s)|\ll U^2. \] For completeness, the finite sum is $O(U^2)$, the integral and the finitely many correction terms are bounded by the same quantity, and the remainder is bounded by a constant times \[ |s(s+1)(s+2)(s+3)| \frac{N^{-\Re s-3}}{\Re s+3} \ll U^{1-\Re s}\ll U^2. \] Also, for $\Re s\ge-1$, \[ |\psi_{U,\delta}(s)| \le B e^{R\theta}\sum_{n\le M}n \ll U^{2\theta}. \] Consequently \begin{equation}\label{eq:F-polynomial-growth} \sup_{|z-2|\le3}|F(z\pm it)|\ll U^{2+2\theta}\ll U^3. \end{equation} This estimate uses no information about the location of zeta zeros. Define the analytic function \[ G_t(z)=\frac12\left(F(z+it)+\overline{F(\overline z+it)}\right). \] The conjugated expression is analytic in $z$; since the coefficients are real it also equals $F(z-it)$. We have $G_t(2)=\Re F(2+it)\ge3/4$ and $|G_t(z)|\ll U^3$ on the radius-three disk. If $n_t(2)$ is the number of zeros of $G_t$ in $|z-2|\le2$, counted with multiplicity, Jensen's formula yields \[ n_t(2)\log(3/2) \le\log\sup_{|z-2|=3}|G_t(z)|-\log|G_t(2)| \ll\log U. \] Zeros on a circular boundary can be handled by a limiting radius. On the real interval, $G_t(x)=\Re F(x+it)$, and $[b,2]$ lies strictly inside the radius-two disk. Hence the real part has $O(\log U)$ zeros there. Let $A(x)$ be the specified continuous argument. Between consecutive zeros of $\Re F(x+it)$ it lies in an open argument interval of length $\pi$, because $F$ stays in one of the two open half-planes. At a zero of the real part the value of $F$ is nonzero by hypothesis, so continuity permits only the same or an adjacent such interval. If the real part has $n$ zeros, this proves \[ |A(x)|\le|A(2)|+(n+1)\pi. \] The right-edge estimate and the zero count prove \eqref{eq:horizontal-arg-bound}. This is a bound on the absolute size of a continuously chosen argument; no bound on its total variation is asserted or required. Finally apply Jensen's formula to $F$ itself, centered at $2+it_0$, using \eqref{eq:right-edge} and \eqref{eq:F-polynomial-growth}. It has $O(\log U)$ zeros in the radius-two disk. The box in the statement is inside that disk, since its maximum distance from the center is at most $\sqrt{(3/2)^2+1}<2$ for large $U$. This counts zeros of the mollifier as well as zeros of $\zeta$; no zeta zero-counting estimate has been applied to the mollifier. \end{proof} \subsection{Littlewood's identity and the four edges} We now combine the logarithmic integral with the boundary estimates. Keeping the mollified function fixed while taking limits of the rectangle edges is essential: the auxiliary left edge may move, but the shift defining the mollifier must stay unchanged. \begin{lemma}[Block displacement estimate]\label{lem:block-displacement} Uniformly for $0\le r_U\le R$, with $\sigma=1/2+r_U/\log U$, \begin{equation}\label{eq:block-displacement} \sum_{U/2<\gamma\le U}(\beta-\sigma)_+ \le\frac{U}{8\pi}\log m_P(r_U,\theta)+O_{P,\theta,R}(U/\log U). \end{equation} The sum is over nontrivial zeta zeros, with multiplicity. \end{lemma} \begin{proof} Fix $U,\delta$ and the analytic function $F=F_{U,\delta}$. First take a rectangle $[b,2]\times[t_1,t_2]$ without boundary zeros, where $b$ is near $\sigma$ and $t_1,t_2$ are near $U/2,U$. There is no pole in this rectangle. With the horizontal arguments continued from the principal argument on the right edge, Littlewood's identity is \begin{equation}\label{eq:littlewood-four-edges} \begin{split} 2\pi\sum_{\rho_F\text{ in the rectangle}} m_{\rho_F}(\Re\rho_F-b) ={}&\int_{t_1}^{t_2}\log|F(b+it)|\,dt -\int_{t_1}^{t_2}\log|F(2+it)|\,dt\\ &+\int_b^2\arg F(x+it_2)\,dx -\int_b^2\arg F(x+it_1)\,dx. \end{split} \end{equation} Here $\rho_F$ ranges over distinct zeros and $m_{\rho_F}$ denotes their order. To verify the signs and the choice of argument, set $u=\log|F|$ and $\phi(x,t)=x-b$. In the distributional sense, $\Delta u=2\pi\sum m_{\rho_F}\delta_{\rho_F}$. Green's identity with $\phi$ gives the left and right logarithmic integrals in \eqref{eq:littlewood-four-edges}. The remaining right edge term is $(2-b)[\arg F(2+it_2)-\arg F(2+it_1)]$. On the top and bottom edges, use $u_t=-v_x$ for a local analytic logarithm $u+iv$ and integrate by parts. Their endpoint terms cancel that right edge term, leaving the displayed top integral minus the bottom integral. This argument uses local logarithms along the edges and the distributional zero masses, so it does not presuppose a logarithm on the interior containing zeros. The horizontal integrals in \eqref{eq:littlewood-four-edges} are $O(\log U)$ by Lemma~\ref{lem:horizontal-argument}. The right logarithmic integral is $O(U/\log U)$ by \eqref{eq:right-edge}. Boundary zeros cause no additional term: keep $F$ fixed, choose zero-free $b<\sigma$ approaching $\sigma$, and choose zero-free heights approaching $U/2$ from below and $U$ from above. The horizontal bound is uniform in these choices. Local factorization at a zero implies convergence of the logarithmic integrals on the vertical edges; a zero on $\Re s=\sigma$ has limiting weight zero. The local zero count in Lemma~\ref{lem:horizontal-argument}, or simply local discreteness followed by a limit, justifies the height choice for $F$, including its mollifier zeros. We obtain the identity with limiting boundaries and the same error bounds. Crucially, changing the auxiliary boundary $b$ in this limiting argument does not change $\delta$ or the mollifier. All zero weights on the left of \eqref{eq:littlewood-four-edges} are nonnegative. A common zero of $\zeta$ and $\psi$ has order equal to the sum of their orders in $F$. We may therefore discard all mollifier zero contributions and retain the zeta zeros. Applying \eqref{eq:unweighted-log} to the remaining left integral gives \[ 2\pi\sum_{U/2\le\gamma\le U}(\beta-\sigma)_+ \le\frac U4\log m_P(r_U,\theta)+O(U/\log U). \] Discarding any contribution at the lower endpoint proves the half-open version \eqref{eq:block-displacement}. \end{proof} \subsection{One normalization at the final height} For a zero $\rho=\beta+i\gamma$ and final height $X$, write \begin{equation}\label{eq:global-horizontal-y} y_{\rho,X}=\frac{\log X}{2\pi}(\beta-1/2). \end{equation} This definition uses the same height $X$ for every zero in the sum. To retain this normalization when summing dyadic blocks, we keep the vertical line fixed and allow the local shift parameter in Young's formula to change from block to block. \begin{proposition}[Global truncated displacement moment] \label{prop:truncated-moment} For every fixed $a>0$, fixed $0<\theta<1/2$, and fixed real polynomial $P$ as above, \begin{equation}\label{eq:global-truncated-moment} \limsup_{X\to\infty}\frac1{N(X)} \sum_{\substack{0<\gamma\le X\\\beta>1/2}} (y_{\rho,X}-a)_+ \le D_P(a,\theta) =\frac{\log m_P(2\pi a,\theta)}{4\pi}. \end{equation} \end{proposition} \begin{proof} Put $L=\log X$, $r=2\pi a$, and fix throughout the argument the line \[ \sigma_X=\frac12+\frac rL. \] Take \[ J=\left\lfloor\frac{\sqrt L}{\log2}\right\rfloor, \qquad U_j=\frac X{2^j}\quad(0\le j0$. For every $02c\text{ for all }x'\in R_1\setminus\{x\}\}, \qquad d=|\mathcal I|. \] Order the remaining points on the real line and split them into maximal consecutive clusters in which successive gaps are at most $2c$. Each cluster has at least two points. A cluster of even size is partitioned into consecutive pairs; a cluster of odd size is partitioned into one consecutive triple and consecutive pairs. Let $G_1,\ldots,G_A$ be the pairs and $T_1,\ldots,T_B$ the triples. The two points in a pair differ by at most $2c$; in a triple each successive gap is at most $2c$ and the extreme gap is at most $4c$. In particular, \begin{equation}\label{eq:group-cardinalities} |R_1|=d+2A+3B,\qquad N=d+2A+3B+\sum_{x\in R_2}m_x+2\sum_{j=1}^qm_j. \end{equation} For these groups put $p_\ell=\sum_{x\in G_\ell}\phi_x$ and $t_\ell=\sum_{x\in T_\ell}\phi_x$, and introduce the finite-dimensional spaces \[ \begin{split} U&=\operatorname{span}\bigl( \{p_\ell\}_{\ell=1}^{A}\cup\{t_\ell\}_{\ell=1}^{B} \cup\{\phi_x:x\in R_2\}\cup\{g_{z_j}\}_{j=1}^{q}\bigr),\\ V&=U+\operatorname{span}\{\phi_x:x\in\mathcal I\}. \end{split} \] Distinct exponential functions $\phi_z$ are linearly independent. Indeed, after dividing on the positive-measure set where $\eta\ne0$, a vanishing combination is an exponential polynomial vanishing on a set with an accumulation point. Its analytic continuation is identically zero, and distinct exponential frequencies then have zero coefficients. The displayed generators use disjoint groups of those frequencies, so \begin{equation}\label{eq:UV-dimensions} D_U:=\dim U=A+B+r+q,\qquad D_V:=\dim V=d+A+B+r+q. \end{equation} Empty spaces and sums are permitted in the argument. The antilinear isometry $Jv(u)=\overline{v(-u)}$ fixes $\phi_x$ for real $x$, as well as $g_z$ and $h_z$. Inner products between $J$-fixed vectors are real. Gram--Schmidt therefore gives a $J$-fixed orthonormal basis $\psi_1,\ldots,\psi_{D_V}$ of $V$ whose first $D_U$ vectors span $U$. The tensors $\psi_k\otimes\psi_k$ are orthonormal. The real numbers \[ \begin{split} \alpha_k&=\langle F,\psi_k\otimes\psi_k\rangle\\ &=\sum_{x\in R_1}\langle\phi_x,\psi_k\rangle^2 +\sum_{x\in R_2}m_x\langle\phi_x,\psi_k\rangle^2\\ &\hspace{8mm}+2\sum_{j=1}^qm_j \bigl(\langle g_{z_j},\psi_k\rangle^2 -\langle h_{z_j},\psi_k\rangle^2\bigr) \end{split} \] satisfy, by Bessel's inequality, $\mathcal S_f(Z)\ge\sum_k\alpha_k^2$. Using $\alpha^2\ge4\alpha-4$ for the first $D_U$ terms and $\alpha^2\ge2\alpha-1$ for the others gives \begin{equation}\label{eq:weighted-Bessel} \mathcal S_f(Z)\ge 2\sum_{k\le D_U}\alpha_k+2\sum_{k\le D_V}\alpha_k-3D_U-D_V. \end{equation} We now bound both partial sums. Put \[ S_0=\sum_{x\in\mathcal I}\|\operatorname{proj}_U\phi_x\|^2, \quad M_*:=\sum_{x\in R_2}m_x+2\sum_{j=1}^qm_j, \quad \kappa_0=\min_{|t|\le2c}K_f(t),\quad \kappa_1=\min_{|t|\le4c}K_f(t). \] A repeated real point contributes exactly its multiplicity in both spaces. For a conjugate pair, Parseval for $g_{z_j}\in U$ and Bessel for $h_{z_j}$ show that its contribution in either space is at least $2m_j(\|g_{z_j}\|^2-\|h_{z_j}\|^2)=2m_j$. For a pair, since its sum $p_\ell$ belongs to either space, the sum of the two squared projection norms is at least \[ \tfrac12\|p_\ell\|^2\ge1+\kappa_0. \] For a triple the analogous bound is \[ \tfrac13\|t_\ell\|^2 \ge1+\tfrac43\kappa_0+\tfrac23\kappa_1. \] The points in $\mathcal I$ contribute $S_0$ in $U$ and exactly $d$ in $V$. Substitution in \eqref{eq:weighted-Bessel} yields the complete cluster inequality \begin{equation}\label{eq:complete-cluster-inequality} \begin{split} \mathcal S_f(Z)\ge{}&4N-3d-4r-4q -4A(2-\kappa_0)\\ &-4B\bigl(3-\tfrac43\kappa_0-\tfrac23\kappa_1\bigr)+2S_0. \end{split} \end{equation} This is the algebra behind \cite[(2.28)]{Lamzouri2026}. For a bound uniform in $f$, use $\cos v\ge1-v^2/2$ and $|u|\le1/2$ in \eqref{eq:kernel-and-Laplace}: \begin{equation}\label{eq:uniform-kernel-local} K_f(t)\ge1-\frac{\pi^2t^2}{2}. \end{equation} Write $e=\pi^2c^2\le1/16$. Then $\kappa_0\ge1-2e$ and $\kappa_1\ge1-8e$. By \eqref{eq:group-cardinalities}, $N\ge d+2A+3B+2(r+q)$. Thus \eqref{eq:complete-cluster-inequality} implies \[ \mathcal S_f(Z)\ge 2N-d+2S_0-8eA+(2-32e)B \ge2N-d+2S_0-4eN. \] The last step uses $2A\le N$ and $2-32e\ge0$. It remains to estimate $S_0$. Split $\mathcal I$ into $\mathcal I_1$, whose points are $c$-isolated from all of $Z$, and $\mathcal I_2=\mathcal I\setminus\mathcal I_1$. Every point of $\mathcal I_2$ is within real-part distance $c$ of a repeated real point or a nonreal conjugate pair; other simple real points are more than $2c$ away. Assign it to one such point or pair. Since distinct elements of $\mathcal I$ differ by more than $2c$, at most one point can be assigned to each repeated real point or each distinct conjugate pair. If $x\in\mathcal I_2$ is assigned to $v\in R_2$, projection on $\phi_v\in U$ and \eqref{eq:uniform-kernel-local} give \[ \|\operatorname{proj}_U\phi_x\|^2 \ge K_f(x-v)^2\ge(1-e/2)^2\ge1-e\ge\tfrac12-e. \] If it is assigned to $z=v+iy$, then $|x-v|\le c$ and \[ \begin{split} \langle\phi_x,g_z\rangle &=\int_I f(u)\cos(2\pi(x-v)u)\cosh(2\pi yu)\,du\\ &\ge(1-e/2)M_f(y),\qquad \|g_z\|^2=\frac{1+M_f(2y)}2. \end{split} \] Cauchy--Schwarz applied to $\phi_v$ and $g_z$ shows that $R(y):=2M_f(y)^2/(1+M_f(2y))\le1$. Hence \[ \begin{split} \|\operatorname{proj}_U\phi_x\|^2 &\ge(1-e/2)^2R(y)\ge R(y)-e\\ &=\frac{1-H_f(y)}2-e \ge\frac{1-[H_f(y)]_+}2-e. \end{split} \] Summing these bounds and using the injectivity of the assignment, \begin{equation}\label{eq:uniform-projection-deficit} S_0\ge\frac{|\mathcal I_2|}{2} -\frac12\sum_{j=1}^q[H_f(\Im z_j)]_+-eN. \end{equation} Consequently \[ \mathcal S_f(Z)\ge2N-|\mathcal I_1| -\sum_{j=1}^q[H_f(\Im z_j)]_+-6eN. \] Since $\operatorname{Iso}_c(Z)\ge|\mathcal I_1|$, this proves \eqref{eq:uniform-finite-isolation}. The two error contributions are $4eN$ from the cluster estimate and $2eN$ from \eqref{eq:uniform-projection-deficit}. \end{proof} \section{Unweighted complex pair correlation and transfer to zeros} \label{sec:pair-transfer} To apply the finite inequality to zeta zeros, we need its unweighted pair energy. The available complex pair-correlation theorem contains a rational weight; the two fixed tests below remove it by an exact identity. For a real, even, integrable function $q$ supported on $[-1,1]$, use $\widehat q(z)=\int_{-1}^1q(u)e^{-2\pi iuz}\,du$, with its entire extension. The unconditional input we need is \cite[Lemma~5, (3.3)--(3.4)]{BGSTB2024}: if $q$ is Lipschitz at zero, then, with $L=\log X$, \begin{equation}\label{eq:BGSTB-input} \begin{split} &\sum_{\substack{\rho,\rho'\\0<\gamma,\gamma'\le X}} \widehat q\!\left(\frac{i(\rho-\rho')L}{2\pi}\right) \frac4{4-(\rho-\rho')^2}\\ &\hspace{12mm}= \frac{XL}{2\pi} \left(q(0)+2\int_0^1u q(u)\,du+O_q(L^{-1/2})\right). \end{split} \end{equation} The sum contains every nontrivial zero in the indicated range, with multiplicity. In particular, the arguments of $\widehat q$ are allowed to be complex. No assertion that the zeros are on the critical line is used. For an even probability density $f\in L^2(I)$ define \begin{equation}\label{eq:pair-cost-functional} C(f)=\int_I f(u)^2\,du +\int_I\int_I |u-v|f(u)f(v)\,du\,dv. \end{equation} The next lemma evaluates the unweighted energy in terms of $C(f)$. \begin{lemma}[Removing the pair weight exactly]\label{lem:unweighted-pair-correlation} Let $f=\eta^2$, where $\eta$ is real, even and belongs to $C_c^\infty((-1/2,1/2))$, with $\int_I\eta^2=1$. Then \begin{equation}\label{eq:unweighted-pair-energy} \frac1{N(X)} \sum_{\substack{\rho,\rho'\\0<\gamma,\gamma'\le X}} K_f\!\left(\frac{i(\rho-\rho')\log X}{2\pi}\right)^2 =C(f)+o_f(1). \end{equation} \end{lemma} \begin{proof} Set $Q=f*f$. Both $Q$ and $Q''$ are fixed, real, even, smooth functions compactly supported in $(-1,1)$, so each separately satisfies the hypotheses of \eqref{eq:BGSTB-input}. Integration by parts gives, for every complex $z$, \[ \widehat Q(z)=K_f(z)^2, \qquad \widehat{Q''}(z)=-4\pi^2z^2K_f(z)^2. \] Writing $\Delta=\rho-\rho'$ and $z=i\Delta L/(2\pi)$, we obtain the exact identity \begin{equation}\label{eq:weight-removal-identity} \left(\widehat Q(z)-\frac{\widehat{Q''}(z)}{4L^2}\right) \frac4{4-\Delta^2}=K_f(z)^2. \end{equation} There is no pole on these zero differences, since $|\Re\Delta|<1$. Apply \eqref{eq:BGSTB-input} to the two fixed tests $Q$ and $Q''$, and only afterwards take the linear combination in \eqref{eq:weight-removal-identity}. The second main term is $O_f(L^{-2})$ after division by $XL/(2\pi)$, and the remaining error is $o_f(1)$. The first main term is \[ Q(0)+2\int_0^1uQ(u)\,du =\int_I f(u)^2\,du+\int_I\int_I|u-v|f(u)f(v)\,du\,dv=C(f), \] where evenness changes $|u+v|$ to $|u-v|$ in the convolution integral. Finally, $N(X)\sim XL/(2\pi)$ proves the lemma. \end{proof} The pair formula now supplies the energy term in the finite inequality. The remaining input is a positive-part first moment of horizontal displacement. The following proposition states the exact majorant and moment assumptions needed for the transfer. \begin{proposition}[Isolation transfer]\label{prop:isolation-transfer} Fix $a>0$, $\ell>0$, $D\ge0$, and a density $f$ as in Lemma~\ref{lem:unweighted-pair-correlation}. Suppose that \begin{equation}\label{eq:transfer-majorant} [H_f(y)]_+\le\ell(y-a)_+\qquad(y\ge0) \end{equation} and that the zeros, with their actual multiplicities, satisfy \begin{equation}\label{eq:transfer-hinge} \limsup_{X\to\infty}\frac1{N(X)} \sum_{\substack{\rho=\beta+i\gamma\\\beta>1/2,\ 0<\gamma\le X}} \left(\frac{(\beta-1/2)\log X}{2\pi}-a\right)_+\le D. \end{equation} Then, for every fixed $01$ form the multiset \begin{equation}\label{eq:global-zero-multiset} Z_X=\left\{-\frac{i(\rho-1/2)\log X}{2\pi}: 0<\Im\rho\le X\right\}. \end{equation} Its cardinality is $N(X)$ and it is conjugation invariant by the functional equation and conjugation symmetry of $\zeta$: $\rho\mapsto1-\overline\rho$ preserves multiplicities. The real part of its point corresponding to $\rho$ is $\gamma\log X/(2\pi)$, and the absolute imaginary part is $|\beta-1/2|\log X/(2\pi)$. This uses one global $\log X$ for all zeros below $X$. Apply Proposition~\ref{prop:finite-isolation} to $Z_X$. Since $K_f$ is even, its energy is the sum in \eqref{eq:unweighted-pair-energy}. Since $H_f$ is even, each distinct nonreal conjugate pair is represented by a distinct right-half-plane zero $\beta>1/2$. The penalty in \eqref{eq:uniform-finite-isolation} can therefore be enlarged to \[ \sum_{\substack{\rho=\beta+i\gamma\\\beta>1/2,\ 0<\gamma\le X}} \left[H_f\!\left(\frac{(\beta-1/2)\log X}{2\pi}\right)\right]_+, \] now with multiplicity. Each representative is inserted once per its original multiplicity; there is no extra factor of two. By \eqref{eq:transfer-majorant} and \eqref{eq:transfer-hinge}, the limsup of this penalty divided by $N(X)$ is at most $\ell D$. We finally compare the finite multiset with the full ordered array. A finite-multiset isolated point has distance greater than $c$ from every other real part, equivalently both available neighboring ordinate gaps exceed $2\pi c/\log X$. Only the final point in the truncation can acquire a new neighbor above $X$, and the convention $n\ge2$ in the definition of $B_0$ can exclude at most the first point. Repeated ordinates do not create further exceptions, because they cannot be isolated even in $Z_X$. Thus \begin{equation}\label{eq:endpoint-isolation-comparison} B_0(X,c)\ge\operatorname{Iso}_c(Z_X)-2. \end{equation} Divide \eqref{eq:uniform-finite-isolation} by $N(X)$, use Lemma~\ref{lem:unweighted-pair-correlation}, and take a liminf. The constant in \eqref{eq:endpoint-isolation-comparison} vanishes, proving \eqref{eq:isolation-transfer-bound}. \end{proof} \section{The fixed numerical certificate and admissible smoothing} \label{sec:certificate} Two numerical statements remain: the value of the final lower bound and the majorant required by Proposition~\ref{prop:isolation-transfer}. Both use only the polynomial and parameter tuple in \eqref{eq:fixed-parameters}--\eqref{eq:P-definition}; no optimization enters the proof. After deriving the elementary formulas, we verify the majorant on a finite covering of $[0,3]$ and estimate the tail analytically. The strict margins then permit an admissible smoothing with the same slope and threshold. \subsection{The transform and energy of the limiting density} Put $I=[-1/2,1/2]$. For an even nonnegative density $f$ supported on $I$ with $\int_I f=1$, use the notation \begin{align*} M_f(y)&=\int_I f(x)\cosh(2\pi yx)\,dx=K_f(iy),\\ H_f(y)&=1-\frac{4M_f(y)^2}{1+M_f(2y)},\\ C(f)&=\int_I f(x)^2\,dx+ \int_I\int_I |x-z|f(x)f(z)\,dx\,dz. \end{align*} These are the transform, projection deficit, and pair-energy constant used in the preceding section. In particular, $M_f(y)\ge1$ for real $y$, so every displayed denominator is positive. Write $M_0=M_{f_0}$ and $H_0=H_{f_0}$ for the density \eqref{eq:MT-density}, which is the Montgomery--Taylor density used in \cite[\S3]{Lamzouri2026}. \begin{lemma}\label{lem:MT-closed-form} For real $y$, \begin{equation}\label{eq:M-closed-form} M_0(y)=\frac{\cosh(\pi y)+ \sqrt2\,\pi y\cot(1/\sqrt2)\sinh(\pi y)} {1+2\pi^2y^2}. \end{equation} Furthermore, \begin{equation}\label{eq:C-closed-form} C(f_0)=C_{\mathrm{MT}} =\frac12+\frac1{\sqrt2}\cot(1/\sqrt2). \end{equation} \end{lemma} \begin{proof} The density is positive on $I$, even, and has integral one. Set $b=\sqrt2$ and $t=2\pi y$. The elementary antiderivative \[ \int e^{tx}\cos(bx)\,dx =\frac{e^{tx}\bigl(t\cos(bx)+b\sin(bx)\bigr)}{t^2+b^2} \] gives \[ \int_{-1/2}^{1/2} e^{tx}\cos(bx)\,dx =\frac{2\bigl(t\sinh(t/2)\cos(b/2) +b\cosh(t/2)\sin(b/2)\bigr)}{t^2+b^2}. \] Division by $b\sin(b/2)$ gives \eqref{eq:M-closed-form}. The formula has no singularity at the origin, and $M_0(0)=1$. For the second identity, define, on $I$, \[ G(x)=f_0(x)+\int_I |x-z|f_0(z)\,dz. \] In the interior of $I$ one has $f_0''=-2f_0$ and $\frac{d^2}{dx^2}\int_I|x-z|f_0(z)\,dz=2f_0(x)$. Consequently $G''=0$. Since $G$ is even, it is constant. At the right endpoint, the unit mass and vanishing first moment of $f_0$ give \[ G(1/2)=f_0(1/2)+\int_I(1/2-z)f_0(z)\,dz =\frac1{\sqrt2}\cot(1/\sqrt2)+\frac12. \] Multiplying the constant identity for $G$ by $f_0$ and integrating proves \eqref{eq:C-closed-form}. \end{proof} \subsection{Exact polynomial inputs and the endpoint value} Every coefficient of $P$ in \eqref{eq:P-definition} is rational. If \[ A=\int_0^1 P'(u)^2\,du,\qquad B=\int_0^1 P(u)^2\,du, \] exact rational integration gives \begin{align} A&=\frac{783057543745087674299266657684417689707279} {419065195577219886170363240902124615327379}, \label{eq:exact-A}\\ B&=\frac{1292604115095627224586630676414215319251379} {9638499498276057381918354540748866152529717}. \label{eq:exact-B} \end{align} These fractions require only rational arithmetic: if $P(u)=\sum_{j=0}^{11}p_ju^j$, use \[ A=\sum_{j,k=1}^{11}\frac{jk\,p_jp_k}{j+k-1},\qquad B=\sum_{j,k=0}^{11}\frac{p_jp_k}{j+k+1}. \] The identity $\int_0^1 PP'=(P(1)^2-P(0)^2)/2=1/2$ then yields, with $k=\theta r=147\pi/125$, \begin{equation}\label{eq:exact-square-expansion} J:=\int_0^1(P'-\theta rP)^2=A-k+k^2B. \end{equation} In particular, the mixed term in this expression has coefficient $-k$, not $-2k$. Substitution of \eqref{eq:exact-square-expansion} into \eqref{eq:moment-cost} gives the exact elementary expression that is evaluated by interval arithmetic. The following intervals are deliberately wider decimal enclosures of the interval outputs. They summarize the fixed-input evaluation; the complete output endpoints are supplied in the accompanying certificate package. \begin{center} \small \begin{tabular}{@{}lll@{}} \toprule Quantity & Lower endpoint & Upper endpoint\\ \midrule $J$ & $0.00457191765729882042$ & $0.00457191765729882043$\\ $m_P(r,\theta)$ & $1.00061874412331700995$ & $1.00061874412331700996$\\ $D_P(a,\theta)$ & $0.00004922286625777224966$ & $0.00004922286625777224967$\\ $C_{\mathrm{MT}}$ & $1.32749929632058835426$ & $1.32749929632058835427$\\ \bottomrule \end{tabular} \end{center} The separately evaluated final expressions satisfy \begin{align} 0.67246806891908274 &<2-C_{\mathrm{MT}}-\ell D_P(a,\theta) <0.67246806891908275, \label{eq:zero-gap-certificate}\\ 0.67246806299732010 &<2-C_{\mathrm{MT}}-\ell D_P(a,\theta)-6\pi^2\,10^{-10} <0.67246806299732011. \label{eq:fixed-gap-certificate} \end{align} Thus the loss at $c=10^{-5}$ is paid before rounding the asserted proportion down to $0.672468$. The remaining margin is greater than $6.2997\times10^{-8}$. \subsection{A finite certificate for the deficit majorant} \begin{proposition}\label{prop:interval-certificate} For the density $f_0$ and constants $a=6/5$, $\ell=663/1000$, \begin{equation}\label{eq:MT-ramp} (H_0(y))_+\le \ell(y-a)_+\qquad(y\ge0). \end{equation} There is strict separation from the relevant comparison functions on each of the compact ranges $[0,1.22]$ and $[1.22,3]$. \end{proposition} \begin{proof} For $i=0,\ldots,29999$, let \[ I_i=\left[\frac{i}{10000},\frac{i+1}{10000}\right]. \] Using \eqref{eq:M-closed-form} and $H_0(y)=1-4M_0(y)^2/(1+M_0(2y))$, the accompanying interval program verifies the following exhaustive list of comparisons at 55 decimal digits of interval precision: \begin{center} \begin{tabular}{@{}lll@{}} \toprule Index range & Covered range & Verified comparison\\ \midrule $0\le i\le12199$ & $[0,1.22]$ & $\sup H_0(I_i)<0$\\ $12200\le i\le29999$ & $[1.22,3]$ & $\sup H_0(I_i)<\inf\ell(I_i-a)$\\ \bottomrule \end{tabular} \end{center} Here $H_0(I_i)$ denotes an interval enclosure of the complete image of the cell, not a set of sampled point values. Endpoints are formed from exact terminating decimal strings, so neighboring cells have identical boundary values. The two ranges contain $12{,}200$ and $17{,}800$ cells, respectively, and their union is $[0,3]$. The first range contains $[0,a]$ and extends beyond $a$. On it, $(H_0)_+=0$, so \eqref{eq:MT-ramp} follows. On the second range, $y>a$ and the second set of comparisons implies the same inequality. For $y\ge3$, positivity of the denominator gives $H_0(y)\le1$, whereas \[ \ell(y-a)\ge\ell(3-a)=\frac{5967}{5000}=1.1934>1. \] This proves the analytic tail without numerical evaluation there. Finally, each comparison in the finite list is strict. The minimum of its finitely many positive separations is positive, which gives the stated compact separation. \end{proof} \begin{remark}[Implementation and reproducibility] The numerical part of Proposition~\ref{prop:interval-certificate} is a computer-assisted finite inequality verification. Its role is limited to the specified elementary functions and fixed cells. The certificate includes the actual source, exact inputs, complete inherited logs, and a separate exact rational check of \eqref{eq:exact-A}--\eqref{eq:exact-square-expansion}. The endpoint comparisons can be checked directly in the supplied code. The first loop tests the sign of the upper interval endpoint after conversion to a Python floating-point number. A finite nonnegative endpoint cannot round to a strictly negative number, so the strict negative test is valid; negative underflow to signed zero would fail the test. The second loop compares interval endpoints directly. Floating-point extrema printed for diagnostic purposes are not used as outward rounded bounds or as the quantitative separation in the smoothing proof. The numerical certificate and its archived replay accompany the source as unchanged companion packages. Each contains a README with the code, exact inputs, and commands needed to reproduce its checks. The replay uses byte-identical interval source; its rational polynomial check is a separate calculation. Earlier manuscript preparation also included a bounded fixed-input check of the rational identities, the transform antiderivative, and the final intervals. This editorial revision inherits those checks and the cell certificate; it does not rerun the complete cell scan. The original logs record precision and successful assertions but omit the original Python, operating-system, and package versions. The later replay and bounded-check environments are recorded separately. Verification therefore relies on the supplied code and interval implementation, without a formal proof-assistant check. \end{remark} \subsection{Smoothing while preserving the majorant} The pair-correlation lemma requires the square of a smooth function supported in the interior of $I$, whereas $f_0$ is positive at the endpoints. We use the strict inequalities in Proposition~\ref{prop:interval-certificate} to approximate $f_0$ within that class while preserving the majorant and its slope $\ell$. \begin{lemma}\label{lem:smooth-ramp} There are even real functions $\eta_\varepsilon\in C_c^\infty((-1/2,1/2))$, with $f_\varepsilon=\eta_\varepsilon^2$ and $\int_I f_\varepsilon=1$, such that \begin{equation}\label{eq:smooth-C-convergence} \|f_\varepsilon-f_0\|_1+\|f_\varepsilon-f_0\|_2\longrightarrow0, \qquad C(f_\varepsilon)\longrightarrow C_{\mathrm{MT}}. \end{equation} For every sufficiently small fixed $\varepsilon>0$, the same majorant holds for all $y\ge0$: \begin{equation}\label{eq:smooth-ramp} (H_{f_\varepsilon}(y))_+\le\ell(y-a)_+. \end{equation} \end{lemma} \begin{proof} Choose even smooth cutoffs $\chi_\varepsilon$ compactly supported in $(-1/2,1/2)$, with $0\le\chi_\varepsilon\le1$, converging pointwise to $1$ at every interior point. Put \[ Z_\varepsilon=\int_I\chi_\varepsilon(x)^2f_0(x)\,dx, \qquad \eta_\varepsilon(x)= \frac{\chi_\varepsilon(x)\sqrt{f_0(x)}}{\sqrt{Z_\varepsilon}}, \qquad f_\varepsilon=\eta_\varepsilon^2. \] The cosine formula defining $f_0$ on $I$ extends to a smooth, strictly positive function on a neighborhood of $I$. Since the cutoffs vanish near the endpoints, the functions above have all the asserted smoothness and symmetry properties after extension by zero. Dominated convergence gives $Z_\varepsilon\to1$ and convergence of $f_\varepsilon$ to $f_0$ in both $L^1(I)$ and $L^2(I)$. For nonnegative unit-mass densities on $I$, the bound $|x-z|\le1$ gives \begin{align*} |C(f_\varepsilon)-C(f_0)| &\le (\|f_\varepsilon\|_2+\|f_0\|_2) \|f_\varepsilon-f_0\|_2 +2\|f_\varepsilon-f_0\|_1. \end{align*} This proves the second convergence in \eqref{eq:smooth-C-convergence}. For any fixed $R>0$, evenness and the integral definition imply \[ \sup_{|y|\le R}|M_{f_\varepsilon}(y)-M_0(y)| \le\cosh(\pi R)\|f_\varepsilon-f_0\|_1\longrightarrow0. \] Because $M_{f_\varepsilon}(y)\ge1$ and $M_0(y)\ge1$, the rational expression defining $H_f$ has a denominator bounded below by $2$. Taking $R=6$ therefore gives uniform convergence $H_{f_\varepsilon}\to H_0$ on $[0,3]$. Let $\delta>0$ be less than the minimum compact separation in Proposition~\ref{prop:interval-certificate}. For sufficiently small $\varepsilon$, uniform convergence makes $\sup_{0\le y\le3}|H_{f_\varepsilon}(y)-H_0(y)|<\delta$. The inequalities $H_{f_\varepsilon}<0$ on $[0,1.22]$ and $H_{f_\varepsilon}<\ell(y-a)$ on $[1.22,3]$ follow. The analytic tail is unchanged, since every nonnegative unit-mass density has $H_f\le1$ and $\ell(3-a)>1$. This proves \eqref{eq:smooth-ramp}. \end{proof} The preceding lemma permits a fixed admissible smoothing to approach the displayed energy constant arbitrarily closely while preserving the entire deficit majorant. The gap-loss estimate in the preceding section is uniform over this family and has coefficient $6\pi^2$. In applying the asymptotic formula, each $\varepsilon$ is fixed before $X\to\infty$. One may then let $\varepsilon\to0$ in the resulting inequality for the liminf. No height-dependent smoothing and no uniformity in the test-function-dependent asymptotic remainder are required. These orders of limits are used explicitly in the final proof below. \section{Completion of the proof and scope}\label{sec:completion} The uniform gap estimate lets us fix $c$ before choosing the test function. We first combine the preceding results in that order to prove the explicit theorem, then explain the weaker existence statement available from a test-dependent gap error. \begin{proof}[Proof of Theorem~\ref{thm:main}] First fix $00$, the certified strict margins and the smoothing argument give \[ [H_{f_\varepsilon}(y)]_+\le\ell(y-a)_+ \qquad (y\ge0). \] The analytic estimates are now applied with this function fixed. Proposition~\ref{prop:truncated-moment}, together with the finite-multiset transfer and the pair-energy formula, yields \begin{equation}\label{eq:smoothed-final} \liminf_{X\to\infty}\frac{B_0(X,c)}{N(X)} \ge 2-C(f_\varepsilon)-\ell D_P(a,\theta)-6\pi^2c^2. \end{equation} The gap term is uniform in $\varepsilon$. The terms denoted $o_{f_\varepsilon}(1)$ have already vanished in the height limit. No uniform rate for those terms is used. The left side of \eqref{eq:smoothed-final} is independent of $\varepsilon$. Letting $\varepsilon\to0$ afterwards, and using $C(f_\varepsilon)\to C_{\mathrm{MT}}$, proves \eqref{eq:quantitative-bound} throughout its stated range. Now suppose $c\le10^{-5}$. The directed interval evaluation supplies \[ 2-C_{\mathrm{MT}}-\ell D_P(a,\theta)>0.6724680689. \] Since $\pi^2<10$, \[ 6\pi^2c^2\le6\pi^2\,10^{-10}<6\cdot10^{-9}. \] Consequently the lower bound is greater than $0.6724680629$ and hence greater than $0.672468$. The more precise certified evaluation at $c=10^{-5}$ is greater than $0.67246806299$. This proves the theorem. Equivalently, it suffices to prove the endpoint $c=10^{-5}$ and use that $B_0(X,c)$ is nonincreasing in $c$. \end{proof} \begin{remark}[A separate existence statement]\label{rem:existential} There exists $c_0>0$ such that the same numerical lower bound holds for every fixed $00$ inside that range so that $A_\varepsilon c_0^2<2\cdot10^{-8}$. For each fixed $0