\documentclass[11pt,reqno]{amsart}

\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{booktabs}
\usepackage[margin=1.15in]{geometry}
\usepackage{hyperref}

\DeclareUnicodeCharacter{03B9}{\ensuremath{\iota}}
\DeclareUnicodeCharacter{03B3}{\ensuremath{\gamma}}
\DeclareUnicodeCharacter{03B4}{\ensuremath{\delta}}
\DeclareUnicodeCharacter{03C0}{\ensuremath{\pi}}
\DeclareUnicodeCharacter{2016}{\ensuremath{\Vert}}
\DeclareUnicodeCharacter{211D}{\ensuremath{\mathbb{R}}}
\DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}}
\DeclareUnicodeCharacter{2192}{\ensuremath{\to}}
\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}}
\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}}
\DeclareUnicodeCharacter{2208}{\ensuremath{\in}}
\DeclareUnicodeCharacter{2211}{\ensuremath{\sum}}
\DeclareUnicodeCharacter{2227}{\ensuremath{\land}}
\DeclareUnicodeCharacter{2264}{\ensuremath{\le}}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}

\numberwithin{equation}{section}
\setlength{\emergencystretch}{2em}

\title{Goldbach numbers in intervals of length $4.45 \log^2 x$ under the Riemann Hypothesis}
\author{Steve Hubbard}
\email{sthubbar@gmail.com}
\subjclass[2020]{Primary 11P32; Secondary 11M26, 11N05, 11Y35}
\keywords{Goldbach numbers, short intervals, Riemann Hypothesis, explicit bounds}

\begin{document}

\begin{abstract}
Assuming the Riemann Hypothesis, we prove that for every real $x \ge 3$ the interval $(x, x + 4.45 \log^2 x)$ contains an even integer that is a sum of two odd primes. The proof combines a weighted mean square bound for the Chebyshev prime counting error in short intervals with a piecewise linear weight in a bilinear identity for short interval prime counts. The deduction is checked in Lean 4 conditionally on the explicit formula \texttt{ExplicitA}, the zero sum bound \texttt{HadamardK}, the zero count \texttt{BPTN}, the HSW zero counts, the bound $|\gamma| \ge 14$, and the Goldbach verification to $4 \cdot 10^{18}$, all stated as hypotheses.
\end{abstract}

\maketitle

\section{Introduction}

\begin{theorem}\label{thm:main}
Assume the Riemann Hypothesis. For every real $x \ge 3$ the interval $(x, x + 4.45 \log^2 x)$ contains a Goldbach number, that is, an even integer that is a sum of two odd primes.
\end{theorem}

Assuming the Riemann Hypothesis, K\'atai \cite{Katai1967} and Montgomery and Vaughan \cite{MV1975} proved that for some constant $C > 0$ every interval $(x, x + C \log^2 x)$ with $x$ sufficiently large contains a Goldbach number, and Goldston \cite{Goldston1990} gave a proof comparing the measure of prime-free short intervals with Selberg's mean square bound. Cully-Hugill and Dudek \cite[Theorem 1.3]{CHD2024} made this result explicit with $C = 9696$ for all $x \ge 2$. Chirre and Hagen \cite{ChirreHagen2025} reduced the constant to $C = 123$. The binary Goldbach conjecture itself remains open; the result here concerns Goldbach numbers in short intervals under the Riemann Hypothesis.

Our proof follows the mean square framework of Chirre and Hagen \cite{ChirreHagen2025} and makes three changes. First, in the mean square over $[1, x]$, we replace the sharp cutoff by the smooth weight $W(u) = \min(1, u^{-4})$, which produces the positive kernel $4/(4 + (\gamma_i - \gamma_j)^2)$ and bounds the inner sum over zero ordinates directly by $\log|\gamma_i|$. Second, we bound the diagonal sum using the exact modulus squared of the short interval coefficient, Taylor majorants for $1 - \cos$, and a partition of the scaled mid-range $[1, 139.984375]$ into $2161$ pieces with dyadic rational endpoints, reducing the mean square constant from $2.2258$ in \cite{ChirreHagen2025} to $1.0069$. Third, instead of deducing the theorem directly from the mean square on an interval $[ax, x]$ with $\delta = h/(2x)$ as in \cite[Section 5]{ChirreHagen2025}, we integrate $A(t)A(x - t) = 0$ against the weight $\varphi(t) = 11t/(5x)$ on $[x/64, 5x/11]$ and $\varphi(t) = 1$ on $[5x/11, x/2]$, which produces a nonincreasing weight on the quadratic error term and allows direct Abel summation over $256$ equal steps. The resulting constants are new as far as we know.

In comparison with \cite{ChirreHagen2025}, each of these three changes replaces a step in their argument to tighten the resulting constants. First, the smooth weight $W$ replaces their unweighted mean square expansion on $[1, x]$ and makes every off-diagonal term carry the positive kernel $4/(4 + (\gamma_i - \gamma_j)^2)$, so the inner sum is bounded directly by Lemma \ref{lem:HadamardK}. Second, the exact modulus with the $2161$ certified pieces replaces their bound for $|c_\delta(\gamma)|^2$; together with the smooth weight $W$, this lowers the mean square constant from $2.2258$ in \cite{ChirreHagen2025} to $1.0069$ here. Third, the weight $\varphi$ with $256$ step Abel summation replaces their direct deduction from the unweighted short interval mean square, combining with the smaller mean square constant to reduce the interval length constant from $C = 123$ in \cite{ChirreHagen2025} to $4.45$.

The deduction of Theorem \ref{thm:main} from seven stated hypotheses is checked in Lean 4 with Mathlib as the theorem \texttt{goldbach\_\allowbreak 445\_\allowbreak hsw\_\allowbreak gZ}. Lean checks the smooth mean square bound, the $2161$-piece diagonal certificate, the transfer from $\psi$ to $\theta$, the $256$-step Abel summation in the bilinear identity, and the combination with the finite Goldbach verification conditionally on the seven hypotheses \texttt{ExplicitA}, \texttt{HadamardK}, \texttt{Ordinates14}, \texttt{BPTN}, \texttt{Even\allowbreak Goldbach\allowbreak UpTo}, \texttt{HSWN70}, and \texttt{HSWHead14}. Among these, \texttt{HadamardK} is proved in this paper (Lemma \ref{lem:HadamardK}) but assumed as a hypothesis in Lean, and \texttt{ExplicitA}, \texttt{HadamardK}, and \texttt{BPTN} are assumed under the Riemann Hypothesis. See Table \ref{tab:hypotheses} in Appendix \ref{app:formal} for the full list of hypotheses and their status, and Table \ref{tab:pieces} for representative pieces of the diagonal certificate.

\section{Notation and inputs}

Throughout the paper, $\Lambda(n)$ denotes the von Mangoldt function, $\psi(x) = \sum_{n \le x} \Lambda(n)$, and $\theta(x) = \sum_{p \le x} \log p$, where $p$ runs over primes. Under the Riemann Hypothesis, the nontrivial zeros of the Riemann zeta function $\zeta(s)$ take the form $\rho = 1/2 + i\gamma$ with $\gamma \in \mathbb{R}$. We write $N(T)$ for the number of nontrivial zeros $\rho = \beta + i\gamma$ with $0 < \gamma \le T$, counted with multiplicity. For $\delta > 0$ and $\rho = 1/2 + i\gamma$, we define the short interval coefficient
\begin{equation}\label{eq:cdelta-def}
c_\delta(\rho) = c_\delta(\gamma) = \frac{(1+\delta)^{1/2 + i\gamma} - 1}{1/2 + i\gamma}.
\end{equation}
For $x \ge 2$ and $\delta > 0$, we define the short interval mean squares
\begin{equation}\label{eq:Jpsi-def}
J_\psi(x, \delta) = \int_1^x \bigl(\psi((1+\delta)y) - \psi(y) - \delta y\bigr)^2 \, dy, \qquad J_\theta(x, \delta) = \int_1^x \bigl(\theta((1+\delta)y) - \theta(y) - \delta y\bigr)^2 \, dy.
\end{equation}

We state the inputs used in the formal proof together with their published sources, and we prove the second input, Lemma \ref{lem:HadamardK}, directly.

\begin{lemma}[{\cite[Equation (12.1)]{MV2007}, Hypothesis \texttt{ExplicitA}}]\label{lem:ExplicitA}
Assume the Riemann Hypothesis. For every $\delta > 0$ and almost every $y \ge 2$,
\begin{equation}\label{eq:ExplicitA}
\psi((1+\delta)y) - \psi(y) - \delta y = -\lim_{T \to \infty} \sum_{|\gamma| \le T} c_\delta(\rho) y^{1/2 + i\gamma} + \frac{1}{2}\log\frac{1 - y^{-2}}{1 - ((1+\delta)y)^{-2}}.
\end{equation}
For $y > 0$ and complex $s$, $y^s = \exp(s \log y)$ with the real logarithm.
\end{lemma}

Equation \eqref{eq:ExplicitA} is the difference of von Mangoldt's explicit formula \cite[Equation (12.1)]{MV2007} at $(1+\delta)y$ and $y$ for $y \ge 2$ when neither endpoint is a prime power. In the Lean formalization, \texttt{SmoothT2.\allowbreak ExplicitA} states \eqref{eq:ExplicitA} as the limit of $-\sum_{\rho \in Z_n} c_\delta(\rho) y^\rho$ along truncations $Z_n$, for almost every $y \ge 2$, with $B(y) = \frac{1}{2}\log\frac{1 - y^{-2}}{1 - ((1+\delta)y)^{-2}}$ included as the function \texttt{Bf}; the main theorem assumes it, under RH, for each $0 < \delta \le 10^{-13}$.

\begin{lemma}[{Hypothesis \texttt{HadamardK}}]\label{lem:HadamardK}
Assume the Riemann Hypothesis. For every nontrivial zero ordinate $\gamma$ of $\zeta(s)$ and every finite family of nontrivial zero ordinates $\gamma'$ counted with multiplicity,
\begin{equation}\label{eq:HadamardK}
\sum_{\gamma'} \frac{4}{4 + (\gamma - \gamma')^2} \le \log|\gamma|.
\end{equation}
\end{lemma}

\begin{proof}
Since each summand is positive, it suffices to bound the sum over all nontrivial zero ordinates $\gamma'$ counted with multiplicity, where $\rho' = 1/2 + i\gamma'$. Setting $s = 5/2 + i\gamma$, we have
\begin{equation}\label{eq:Hadamard-sum-id}
\sum_{\gamma'} \frac{4}{4 + (\gamma - \gamma')^2} = 2 \sum_{\gamma'} \operatorname{Re}\frac{1}{s - \rho'}.
\end{equation}
By the partial fraction decomposition of $\xi'(s)/\xi(s)$ \cite[Corollary 10.14]{MV2007},
\[
\frac{\xi'(s)}{\xi(s)} = B + \sum_{\rho} \left(\frac{1}{s - \rho} + \frac{1}{\rho}\right), \qquad \operatorname{Re} B = -\sum_{\rho} \operatorname{Re}\frac{1}{\rho},
\]
we have
\begin{equation}\label{eq:Hadamard-partial}
2\sum_{\gamma'} \operatorname{Re}\frac{1}{s - \rho'} = \operatorname{Re}\frac{\Gamma'}{\Gamma}\!\left(\frac{s}{2} + 1\right) - \log\pi + 2\operatorname{Re}\frac{\zeta'}{\zeta}(s) + 2\operatorname{Re}\frac{1}{s - 1}.
\end{equation}
For $\operatorname{Re} z > 0$, Binet's integral formula gives $\frac{\Gamma'}{\Gamma}(z) = \log z - \frac{1}{2z} - \int_0^\infty f(t)e^{-tz}\,dt$, where $f(t) = \frac{1}{2} - \frac{1}{t} + \frac{1}{e^t - 1}$ satisfies $f(0) = 0$ and $f'(t) = \frac{1}{t^2} - \frac{1}{4\sinh^2(t/2)}$ decreases monotonically from $f'(0) = \frac{1}{12}$ to $0$ on $(0, \infty)$. Integrating by parts twice gives $\int_0^\infty f(t)e^{-tz}\,dt = \frac{1}{12z^2} + \frac{1}{z^2}\int_0^\infty f''(t)e^{-tz}\,dt$, which has modulus at most $\frac{1}{12|z|^2} + \frac{1}{|z|^2}\int_0^\infty (-f''(t))\,dt = \frac{1}{6|z|^2} \le \frac{\operatorname{Re} z}{2|z|^2} = \operatorname{Re}\frac{1}{2z}$ whenever $\operatorname{Re} z \ge \frac{1}{3}$, so $\operatorname{Re}\frac{\Gamma'}{\Gamma}(z) \le \log|z|$. Applying this at $z = \frac{9}{4} + \frac{i\gamma}{2}$ with $|\gamma| \ge 14$ from Lemma \ref{lem:Ordinates14} yields
\begin{equation}\label{eq:digamma-bound}
\operatorname{Re}\frac{\Gamma'}{\Gamma}\!\left(\frac{9}{4} + \frac{i\gamma}{2}\right) \le \log\left|\frac{9}{4} + \frac{i\gamma}{2}\right| \le \log|\gamma| - \log 2 + \frac{81}{8\gamma^2}.
\end{equation}
On the line $\operatorname{Re}(s) = 5/2$, the Dirichlet series for $\zeta'/\zeta$ yields $\operatorname{Re}\frac{\zeta'}{\zeta}(s) \le -\frac{\zeta'}{\zeta}(5/2) = 0.28874\dots < 0.2888$, while $2\operatorname{Re}\frac{1}{s-1} = \frac{3}{9/4 + \gamma^2} < \frac{3}{\gamma^2}$. For $|\gamma| \ge 14$, we obtain
\begin{equation}\label{eq:Hadamard-margin}
-\log(2\pi) + 2(0.2888) + \frac{105}{8 \cdot 14^2} = -1.83787\dots + 0.5776 + 0.06696\dots < -1.1933 < 0,
\end{equation}
so the right-hand side of \eqref{eq:Hadamard-partial} is at most $\log|\gamma| - 1.1933 < \log|\gamma|$; the lemma states the weaker bound $\log|\gamma|$ because that is the form used later.
\end{proof}

\begin{lemma}[{\cite[Chapter XV]{Titchmarsh1986}, Hypothesis \texttt{Ordinates14}}]\label{lem:Ordinates14}
Every nontrivial zero $\rho = \beta + i\gamma$ of $\zeta(s)$ satisfies $|\gamma| \ge 14$.
\end{lemma}

The lowest nontrivial zero has ordinate $\gamma_1 = 14.134725\dots > 14$.

\begin{lemma}[{\cite[Lemma 1]{BPT2022}, Hypothesis \texttt{BPTN}}]\label{lem:BPTN}
For all $T \ge 2\pi e$, the zero counting function $N(T)$ satisfies
\begin{equation}\label{eq:BPTN}
N(T) = \frac{T}{2\pi}\log\frac{T}{2\pi e} + \frac{7}{8} + Q(T),
\end{equation}
where
\begin{equation}\label{eq:BPTN-R}
|Q(T)| \le 0.137\log T + 0.443\log\log T + 1.588 + \frac{0.2}{T}.
\end{equation}
\end{lemma}

We use the constants of Lemma 1 of the published version \cite{BPT2022}. The Lean formalization only uses Lemma \ref{lem:BPTN} for $T \ge 10^{13}$, as counts over both signs of the ordinates.

\begin{lemma}[{\cite[Corollary 1]{Schoenfeld1976}}]\label{lem:SchoenfeldTheta}
Assume the Riemann Hypothesis. For every real $u \ge 599$,
\begin{equation}\label{eq:SchoenfeldTheta}
|\theta(u) - u| < \frac{\sqrt{u}\log^2 u}{8\pi}.
\end{equation}
In particular, for every real $u \ge 10^{16}$,
\begin{equation}\label{eq:theta-1e6}
|\theta(u) - u| \le 10^{-6} u.
\end{equation}
\end{lemma}

Inequality \eqref{eq:theta-1e6} follows immediately from \eqref{eq:SchoenfeldTheta} because $u^{-1/2}\log^2 u$ is decreasing for $u > e^4$ and equals $5.4005\dots \times 10^{-7} \cdot 8\pi < 8\pi \cdot 10^{-6}$ at $u = 10^{16}$. In the Lean formalization, inequality \eqref{eq:SchoenfeldTheta} is not assumed; it is proved under RH for $u \ge 10^{11}$ from the explicit formula and the zero counting bound of Hasanalizade, Shen, and Wong \cite[Corollary 1.2]{HSW2021} (assumed as the hypotheses \texttt{HSWN70} and \texttt{HSWHead14}), together with the numerical fact, taken as the hypothesis \texttt{Ordinates14} in Lean, that every nontrivial zero has ordinate of absolute value at least $14$.

\begin{lemma}[{\cite{OSHP2014}, Hypothesis \texttt{Even\allowbreak Goldbach\allowbreak UpTo}}]\label{lem:GoldbachVerification}
Every even integer $2n$ in the range $4 \le 2n \le 4 \cdot 10^{18}$ is a sum of two primes.
\end{lemma}

\section{The mean square bound}

We bound the mean square on $[1, x]$ of a finite Dirichlet polynomial supported on nontrivial zeros of $\zeta(s)$.

\begin{lemma}\label{lem:smooth-mean-square}
Assume the Riemann Hypothesis. Let $\gamma_1, \dots, \gamma_M$ be a finite family of nontrivial zero ordinates of $\zeta(s)$, let $c_1, \dots, c_M \in \mathbb{C}$, and set
\begin{equation}\label{eq:P-def}
P(y) = \sum_{i=1}^M c_i y^{1/2 + i\gamma_i}.
\end{equation}
For every $x \ge 1$,
\begin{equation}\label{eq:P-L2-bound}
\int_1^x |P(y)|^2 \, dy \le x^2 \sum_{i=1}^M |c_i|^2 \sum_{j=1}^M \frac{4}{4 + (\gamma_i - \gamma_j)^2} \le x^2 \sum_{i=1}^M |c_i|^2 \log|\gamma_i|.
\end{equation}
\end{lemma}

\begin{proof}
Define $W(u) = \min(1, u^{-4})$ for $u > 0$. Since $W(u) \ge 0$ for all $u > 0$ and $W(y/x) = 1$ for $1 \le y \le x$, the substitution $y = xu$ gives
\begin{align}
\int_1^x |P(y)|^2 \, dy &\le \int_0^\infty |P(y)|^2 W(y/x) \, dy \nonumber\\
&= x^2 \sum_{i=1}^M \sum_{j=1}^M c_i \overline{c_j} x^{i(\gamma_i - \gamma_j)} \int_0^\infty u^{1 + i(\gamma_i - \gamma_j)} W(u) \, du.\label{eq:P-W-expand}
\end{align}
For any $\Delta \in \mathbb{R}$, splitting the integral at $u = 1$ yields
\begin{equation}\label{eq:W-Mellin}
\int_0^\infty u^{1 + i\Delta} W(u) \, du = \int_0^1 u^{1 + i\Delta} \, du + \int_1^\infty u^{-3 + i\Delta} \, du = \frac{1}{2 + i\Delta} + \frac{1}{2 - i\Delta} = \frac{4}{4 + \Delta^2}.
\end{equation}
Since $\frac{4}{4 + (\gamma_i - \gamma_j)^2} > 0$ is symmetric in $i$ and $j$, applying $\bigl|c_i \overline{c_j} x^{i(\gamma_i - \gamma_j)}\bigr| \le \frac{1}{2}(|c_i|^2 + |c_j|^2)$ in \eqref{eq:P-W-expand} gives the first inequality in \eqref{eq:P-L2-bound}. Applying Lemma \ref{lem:HadamardK} to the inner sum over $j$ gives the second inequality.
\end{proof}

We next bound the diagonal sum $\sum_\gamma |c_\delta(\gamma)|^2 \log|\gamma|$.

\begin{lemma}[{Theorem \texttt{diag\_\allowbreak u6806}}]\label{lem:diag}
Assume the Riemann Hypothesis; in Lean, Theorem \texttt{diag\_\allowbreak u6806} is conditional on the hypotheses \texttt{BPTN} and \texttt{Ordinates14}. For every $\delta$ in the range $0 < \delta \le 10^{-13}$,
\begin{equation}\label{eq:diag-bound}
\sum_{\gamma} |c_\delta(\gamma)|^2 \log|\gamma| \le C_{\mathrm{diag}} \, \delta \log^2\!\left(\frac{2.0001}{\delta}\right), \qquad C_{\mathrm{diag}} = 1.0068.
\end{equation}
\end{lemma}

\begin{proof}
By symmetry of the nontrivial zeros with respect to the real axis, $\sum_\gamma |c_\delta(\gamma)|^2 \log|\gamma| = 2\sum_{\gamma > 0} |c_\delta(\gamma)|^2 \log\gamma$, and every term has $\gamma \ge 14$ by Lemma \ref{lem:Ordinates14}. Let $\eta = \log(1+\delta)$ and $\Lambda = \log(1/\delta)$. From \eqref{eq:cdelta-def}, the exact modulus squared of $c_\delta(\gamma)$ is
\begin{equation}\label{eq:cdelta-exact}
|c_\delta(\gamma)|^2 = \frac{(1+\delta) + 1 - 2\sqrt{1+\delta}\cos(\gamma\eta)}{1/4 + \gamma^2} = \frac{(\sqrt{1+\delta} - 1)^2 + 2\sqrt{1+\delta}\bigl(1 - \cos(\gamma\eta)\bigr)}{1/4 + \gamma^2}.
\end{equation}
For all real $t$, the alternating Taylor series for $\cos t$ gives the degree-6 majorant (\texttt{one\_\allowbreak sub\_\allowbreak cos\_\allowbreak le})
\begin{equation}\label{eq:cos-taylor6}
1 - \cos t \le \frac{t^2}{2} - \frac{t^4}{24} + \frac{t^6}{720}.
\end{equation}
Write $v = \delta|\gamma|$ for the scaled variable, and set
\[
X = \delta\Lambda^2, \qquad Y = \delta\Lambda, \qquad E = \delta^2(\Lambda + 5)^2.
\]
The certified bound is organized in two cases, split at $\delta = 2^{-188}$.

\emph{Pieces.} The bound on an individual piece is formalized as the lemma \texttt{piece\_\allowbreak sum} in \texttt{LeanLab/\allowbreak ChirreHagen2025/\allowbreak U1263Core.\allowbreak lean}, conditional on \texttt{BPTN} (Lemma \ref{lem:BPTN}) and \texttt{Ordinates14} (Lemma \ref{lem:Ordinates14}). Let $0 < \delta \le 10^{-13}$, let $1 \le A \le B$, let $\log B \le \lambda \le 5$, let $Q \ge 0$, and assume the majorant hypothesis on the piece that $|c_\delta(\gamma)|^2 \le Q\delta^2$ whenever $A/\delta < |\gamma| \le B/\delta$. Then \texttt{piece\_\allowbreak sum} states that for any finite set of zero ordinates,
\begin{equation}\label{eq:piece-bound}
\sum_{A/\delta < |\gamma| \le B/\delta} |c_\delta(\gamma)|^2 \log|\gamma| \le 0.31831\, Q (B - A)\bigl(X + (2\lambda - 1.8)Y + (\lambda^2 - 1.8\lambda)\delta\bigr) + 2QE.
\end{equation}
In the structure of this Lean lemma, the zeros on the piece are counted with Lemma \ref{lem:BPTN}, $\log|\gamma| \le \Lambda + \lambda$ there because $|\gamma| \le B/\delta$ and $\log B \le \lambda$, and the term $2QE$ collects the lower order part of the count.

To obtain $Q$ on a piece $A/\delta < |\gamma| \le B/\delta$, write $t = |\gamma|\log(1+\delta)$ for the phase; the lemma \texttt{phase\_\allowbreak range} gives $A(1 - 10^{-13}) < t \le B$ on the piece. The majorant hypothesis $|c_\delta(\gamma)|^2 \le Q\delta^2$ is established by one of two Lean routes in \texttt{U1263Core.\allowbreak lean}: \texttt{pt\_\allowbreak norm} for pieces nearest $v = 1$, and \texttt{pt\_\allowbreak raw} elsewhere. In \texttt{pt\_\allowbreak norm}, for $0 \le \mathrm{lo} \le A(1 - 10^{-13})$, $Q$ satisfies $2(1 + 10^{-13})\allowbreak(1/2 - \mathrm{lo}^2/24 + B^4/720) + 10^{-26} \le Q$. In \texttt{pt\_\allowbreak raw}, given an upper bound $1 - \cos t \le u$ for $A(1 - 10^{-13}) < t \le B$, $Q$ satisfies
\begin{equation}\label{eq:pt-raw-Q}
\frac{10^{-26} + 2(1 + 10^{-13})u}{A^2} \le Q.
\end{equation}
The bound $u$ in \texttt{pt\_\allowbreak raw} comes from \texttt{hu\_\allowbreak poly}, the degree-6 majorant \eqref{eq:cos-taylor6} after shifting $t$ by $2k\pi$, or from \texttt{U6743.\allowbreak hu\_\allowbreak pi}, the majorant $1 - \cos t \le 2 - s^2/2 + s^4/24$ with $s$ the shift of $t$ by an odd multiple of $\pi$; both use $3.141592 < \pi < 3.141593$. The piece endpoints are dyadic rationals; the piece endpoints and $\lambda$ were chosen by a numerical search and certified piece by piece. Here $\lambda$ is any number with $\log B \le \lambda \le 5$, certified in Lean through a dyadic bound on $\log B$; $Q$ is a rational number at least the \texttt{pt\_\allowbreak raw} or \texttt{pt\_\allowbreak norm} bound. For example, the first piece has $A = 1$, $B = 1.0029296875$, $Q = 0.9194789$, $\lambda = 0.0029296875$, and the last piece has $A = 139.6982421875$, $B = 139.984375$, $Q = 0.0001399$, $\lambda = 4.9456581952875$.

\emph{Case $2^{-188} < \delta \le 10^{-13}$.} On the head range $|\gamma| \le 1/\delta$ the sum is at most $\delta\Lambda^2/\pi \le 0.31831\,X$. On the range $v > 1$ it is at most
\[
0.696652249211\,X + 0.294654626964\,Y + 0.112752623673\,\delta + 785.028327376\,E .
\]
This range consists of $2161$ pieces covering $1 < v \le 139.984375$, each bounded by \eqref{eq:piece-bound}, a further range $139.984375 < v \le 599.734375$, and a tail $v > 599.734375$ bounded by $0.002182674424\,X + 0.027980492816\,Y + 0.089673014185\,\delta$. Table \ref{tab:diag-ranges} lists the coefficients of $X = \delta\Lambda^2$. They sum to $1.014962249211$, and the bound $1.0068\,\delta\log^2(2.0001/\delta)$ follows because $\log(2.0001/\delta) = \Lambda + \log 2.0001$ with $\log 2.0001 \ge 0.6931$, and $\Lambda \le 130.3116699904$ when $\delta > 2^{-188}$; together these absorb the lower order terms.

\emph{Case $\delta \le 2^{-188}$.} The head range is $|\gamma| \le 10^{-20}/\delta$, followed by a dyadic chain of $64$ steps, which gives
\[
1.006510467199\,X - 0.263090165331\,Y + 0.112752623673\,\delta + 924.581825936\,E \le 1.0068\,\delta\log^2(2.0001/\delta).
\]

All of these bounds are certified by exact rational arithmetic and checked in Lean as \texttt{diag\_\allowbreak u6806}, conditional on \texttt{BPTN} and \texttt{Ordinates14}.
\end{proof}

\begin{table}[ht]
\centering
\caption{Coefficients of $\delta\Lambda^2$ in the case $2^{-188} < \delta \le 10^{-13}$ of Lemma \ref{lem:diag}.}\label{tab:diag-ranges}
\begin{tabular}{@{}lll@{}}
\toprule
Range & Method & Coefficient of $\delta\Lambda^2$ \\
\midrule
Head $|\gamma| \le 1/\delta$ & Bound $\delta\Lambda^2/\pi$ & $0.31831$ \\
$1 < v \le 139.984375$ & $2161$ pieces, \eqref{eq:piece-bound} & $0.690304599302$ \\
$139.984375 < v \le 599.734375$ & Certified chain & $0.004164975485$ \\
$v > 599.734375$ & Tail bound & $0.002182674424$ \\
\midrule
Total & & $1.014962249211$ \\
\bottomrule
\end{tabular}
\end{table}

The lower order terms and $\Lambda \le 130.3116699904$ bring the total to $1.0068$ relative to $\delta\log^2(2.0001/\delta)$.

Combining Lemma \ref{lem:ExplicitA}, Lemma \ref{lem:smooth-mean-square}, and Lemma \ref{lem:diag} with the $L^2$ convergence of the truncated explicit formula as proved in \cite[Section 3]{ChirreHagen2025} yields the short interval mean square bound.

\begin{proposition}[{Theorem \texttt{theorem2\_\allowbreak u6806}}]\label{prop:Jpsi}
Assume the Riemann Hypothesis; in Lean, Theorem \texttt{theorem2\_\allowbreak u6806} is conditional on the hypotheses \texttt{ExplicitA}, \texttt{HadamardK}, \texttt{Ordinates14}, and \texttt{BPTN}. For all $x \ge 10^{13}$ and $0 < \delta \le 10^{-13}$,
\begin{equation}\label{eq:Jpsi-bound}
J_\psi(x, \delta) \le J \, \delta \log^2\!\left(\frac{2.0001}{\delta}\right) x^2, \qquad J = 1.0069.
\end{equation}
\end{proposition}

\begin{proof}
Write $V(y) = \psi((1+\delta)y) - \psi(y) - \delta y$ and let
\begin{equation}\label{eq:By-def}
B(y) = \frac{1}{2}\log\frac{1 - y^{-2}}{1 - ((1+\delta)y)^{-2}}
\end{equation}
be the secondary term of Lemma \ref{lem:ExplicitA}, so $V(y) - B(y)$ is the zero sum. By Lemma \ref{lem:ExplicitA}, the $L^2$ limit argument of \cite[Section 3]{ChirreHagen2025}, and Lemmas \ref{lem:smooth-mean-square} and \ref{lem:diag}, we have
\begin{equation}\label{eq:PT-limit}
\int_2^x \bigl(V(y) - B(y)\bigr)^2 \, dy \le 1.0068 \, \delta \log^2\!\left(\frac{2.0001}{\delta}\right) x^2.
\end{equation}
For $y \ge 2$ and $0 < \delta \le 1$, we have $|B(y)| \le \delta$, so $\int_2^x B(y)^2 \, dy \le \delta^2 x$. Since $(u + b)^2 \le (1 + \eta)u^2 + (1 + 1/\eta)b^2$ for every $\eta > 0$, taking $\eta = 10^{-5}$ with $L = \log(2.0001/\delta)$ gives
\begin{equation}\label{eq:V-int-2-x}
\int_2^x V(y)^2 \, dy \le (1 + 10^{-5}) \cdot 1.0068 \, \delta L^2 x^2 + (1 + 10^5)\delta^2 x.
\end{equation}
On $[1, 2]$, since $\psi(y) = 0$ for $y < 2$, the difference $\psi((1+\delta)y) - \psi(y)$ is nonzero only for $y \in [2/(1+\delta), 2)$, an interval of length at most $2\delta$, where it is at most $\log 2$; with $u = \psi((1+\delta)y) - \psi(y) \ge 0$ and $v = \delta y \ge 0$ we have $(u - v)^2 \le u^2 + v^2$, so $\int_1^2 V(y)^2 \, dy \le 2\delta(\log 2)^2 + \frac{7}{3}\delta^2 \le 3\delta$. For $x \ge 10^{13}$ and $0 < \delta \le 10^{-13}$, we have $L \ge \log(2 \cdot 10^{13}) > 30$. Dividing by $\delta L^2 x^2$, the first term is $1.0068(1 + 10^{-5}) = 1.00681007$, the second term is at most $10^5 \cdot 10^{-13} / (900 \cdot 10^{13}) < 10^{-30}$, and the third is at most $3 / (900 \cdot 10^{26}) < 10^{-28}$. The sum is below $1.0069$, so $J_\psi(x, \delta) \le 1.0069 \, \delta L^2 x^2$.
\end{proof}

We now pass from $J_\psi(X, \delta)$ to $J_\theta(X, \delta)$.

\begin{lemma}\label{lem:transfer}
Let $X \ge 5 \cdot 10^{17}$ and $0 < \delta \le 10^{-13}$ satisfy $\delta \sqrt{X} < 1$. If $J_\psi(X, \delta) \le J \delta \log^2(2.0001/\delta) X^2$, then
\begin{equation}\label{eq:Jtheta-bound}
J_\theta(X, \delta) \le c \, \delta \log^2\!\left(\frac{2.0001}{\delta}\right) X^2, \qquad c = 1.001 J + 0.0019.
\end{equation}
\end{lemma}

\begin{proof}
Write $D(y) = (\psi - \theta)((1+\delta)y) - (\psi - \theta)(y) \ge 0$ and $u = \psi((1+\delta)y) - \psi(y) - \delta y$, so $\theta((1+\delta)y) - \theta(y) - \delta y = u - D(y)$. Applying $(u - D)^2 \le (1 + \eta)u^2 + (1 + 1/\eta)D^2$ with $\eta = 0.001$ gives $J_\theta(X, \delta) \le 1.001 J_\psi(X, \delta) + 1001 \int_1^X D(y)^2 \, dy$. For every $y$ in the integral, $1 \le y \le X$ and $\delta\sqrt{X} < 1$ give $\delta\sqrt{y} < 1$. By definition, $D(y)$ is the sum over integers $k \ge 2$ of $\log p$ over primes $p$ with $p^k \in (y, (1+\delta)y]$. For each such $k$, the condition $p^k \in (y, (1+\delta)y]$ means $p \in (y^{1/k}, ((1+\delta)y)^{1/k}]$, and the interval $(y^{1/k}, ((1+\delta)y)^{1/k}]$ has length at most $\delta y^{1/k}/k \le \frac{1}{2}\delta\sqrt{y} < 1$, so it holds at most one prime; only $k$ with $2^k \le (1+\delta)y$ contribute, at most $\log((1+\delta)y)/\log 2$ values of $k$, each giving $\log p \le \log((1+\delta)y)$, so $D(y) \le \log^2((1+\delta)y)/\log 2 \le \log^2((1+\delta)X)/\log 2$. By Fubini's theorem, $\int_1^X D(y)\,dy \le \delta X (\psi - \theta)((1+\delta)X)$. Multiplying the pointwise bound by the $L^1$ bound and using $(\psi - \theta)((1+\delta)X) \le 2\sqrt{(1+\delta)X}\,\log((1+\delta)X)$ gives
\[
1001 \int_1^X D(y)^2 \, dy \le 1001 \, \delta X \frac{\log^2((1+\delta)X)}{\log 2} \cdot 2\sqrt{(1+\delta)X}\,\log((1+\delta)X).
\]
For $X \ge 5 \cdot 10^{17}$ and $0 < \delta \le 10^{-13}$, the numerical check
\[
1001 \cdot \frac{\log^2((1+\delta)X)}{\log 2} \cdot 2\sqrt{(1+\delta)X}\,\log((1+\delta)X) \le 0.0019 \, \log^2\!\left(\frac{2.0001}{\delta}\right) X
\]
holds because $\log((1+\delta)X)\log^2((1+\delta)X)/\sqrt{X}$ decreases on $X \ge 5 \cdot 10^{17}$ while $\log(2.0001/\delta)$ is minimal at $\delta = 10^{-13}$, which shows that $1001 \int_1^X D(y)^2 \, dy \le 0.0019 \, \delta \log^2(2.0001/\delta) X^2$ and proves \eqref{eq:Jtheta-bound}.
\end{proof}

With $J = 1.0069$ from Proposition \ref{prop:Jpsi}, this gives $c = 1.0098069$.

\section{The bilinear argument}

To prove Theorem \ref{thm:main}, we split the range of $x$ at $2 \cdot 10^{18}$. For $3 \le x \le 2 \cdot 10^{18}$, the interval length satisfies $4.45\log^2 x \ge 4.45\log^2 3 > 5.36$, so $(x, x + 4.45\log^2 x)$ contains an even integer $2n$ in $[6, 4 \cdot 10^{18}]$, which is a sum of two odd primes by Lemma \ref{lem:GoldbachVerification}. The analytic argument runs for $x \ge 1.1 \cdot 10^{18}$, where $\log x \ge 41$. The two ranges $3 \le x \le 2 \cdot 10^{18}$ and $x \ge 1.1 \cdot 10^{18}$ overlap, so every $x \ge 3$ is covered, and all $x$ with $3 \le x < 1.1 \cdot 10^{18}$ are handled by Lemma \ref{lem:GoldbachVerification} alone, with no analytic input.

Let $x \ge 1.1 \cdot 10^{18}$ and fix $H$ with $4 \le H \le 61.5$. Put $h = H\log^2 x$ and $\delta = h/x$, so $0 < \delta \le 10^{-13}$ and $\delta\sqrt{x} < 1$. Let
\begin{equation}\label{eq:AE-def}
A(t) = \theta((1+\delta)t) - \theta(t), \qquad E(t) = A(t) - \delta t.
\end{equation}
As observed by Goldston \cite[p.~285]{Goldston1990}, if no Goldbach number lies in $(x, x + h]$, then for every $t \in [x/64, x/2]$ the intervals $(t, (1+\delta)t]$ and $(x - t, (1+\delta)(x - t)]$ cannot both contain an odd prime, and since $t \ge x/64 > 10^{16} > 2$, we have
\begin{equation}\label{eq:AA-zero}
A(t) A(x - t) = 0 \qquad \text{for all } t \in [x/64, x/2].
\end{equation}
We weight \eqref{eq:AA-zero} by the continuous piecewise linear function
\begin{equation}\label{eq:phi-weight}
\varphi(t) = \begin{cases}
\dfrac{11t}{5x}, & \dfrac{x}{64} \le t \le \dfrac{5x}{11}, \\[8pt]
1, & \dfrac{5x}{11} \le t \le \dfrac{x}{2}.
\end{cases}
\end{equation}
Substituting $A(t) = \delta t + E(t)$ and $A(x - t) = \delta(x - t) + E(x - t)$ into $0 = \int_{x/64}^{x/2} \varphi(t) A(t) A(x - t) \, dt$ gives the weighted identity
\begin{equation}\label{eq:bilinear-identity}
\delta^2 \int_{x/64}^{x/2} \varphi(t) t(x - t) \, dt + \delta \int_{x/64}^{x/2} \varphi(t)\bigl(t E(x - t) + (x - t) E(t)\bigr) \, dt = -\int_{x/64}^{x/2} \varphi(t) E(t) E(x - t) \, dt.
\end{equation}

By the arithmetic-geometric mean inequality, for every $t \in [x/64, x/2]$ we have
\begin{equation}\label{eq:AM-GM}
\bigl|\varphi(t) E(t) E(x - t)\bigr| \le \frac{1}{2} E(t)^2 + \frac{1}{2}\varphi(t)^2 E(x - t)^2.
\end{equation}
Integrating \eqref{eq:AM-GM} over $t \in [x/64, x/2]$ and substituting $u = x - t$ in the second term yields
\begin{equation}\label{eq:quadratic-weight-int}
\int_{x/64}^{x/2} \bigl|\varphi(t) E(t) E(x - t)\bigr| \, dt \le \int_{x/64}^{63x/64} w(u) E(u)^2 \, du,
\end{equation}
where the combined weight $w(u)$ on $[x/64, 63x/64]$ is
\begin{equation}\label{eq:w-def}
w(u) = \begin{cases}
\dfrac{1}{2}, & \dfrac{x}{64} \le u \le \dfrac{6x}{11}, \\[8pt]
\dfrac{121}{50}\left(1 - \dfrac{u}{x}\right)^2, & \dfrac{6x}{11} \le u \le \dfrac{63x}{64}.
\end{cases}
\end{equation}
At the junction $u = 6x/11$, both expressions in \eqref{eq:w-def} equal $1/2$. Thus $w(u)$ is positive, continuous, and nonincreasing on $[x/64, 63x/64]$.

\begin{proof}[Proof of Theorem \ref{thm:main}]
Assume $x \ge 1.1 \cdot 10^{18}$, fix $H$ with $4 \le H \le 61.5$, put $h = H\log^2 x$ and $\delta = h/x$, and suppose that no Goldbach number lies in $(x, x + h]$. Evaluating the main term on the left-hand side of \eqref{eq:bilinear-identity} with $\varphi(t)$ from \eqref{eq:phi-weight} gives $\delta^2 x^3 M$, where
\begin{align}
M &= \frac{11}{5}\left[\frac{(5/11)^3 - (1/64)^3}{3} - \frac{(5/11)^4 - (1/64)^4}{4}\right] + \left[\frac{(1/2)^2 - (5/11)^2}{2} - \frac{(1/2)^3 - (5/11)^3}{3}\right] \nonumber\\
&= 0.0567215028\dots\label{eq:M-def}
\end{align}
To bound the cross terms in \eqref{eq:bilinear-identity}, write $R(u) = \theta(u) - u$, so $E(u) = R((1+\delta)u) - R(u)$. Substituting $u = x - t$ in $\int_{x/64}^{x/2} \varphi(t) t E(x - t)\,dt$ splits the cross-term integral into four smooth pieces; the first two are written in the variable $t$ and the last two in $u = x - t$: $[x/64, 5x/11]$ with weight $\frac{11}{10} \cdot \frac{2}{x}t(x - t)$, $[5x/11, x/2]$ with weight $x - t$, $[6x/11, 63x/64]$ with weight $\frac{11}{10} \cdot \frac{2}{x}(x - u)^2$, and $[x/2, 6x/11]$ with weight $x - u$. On each piece $[ax, bx]$ with normalized weight $g(u)$, the substitution $v = (1+\delta)u$ transforms $\int_{ax}^{bx} g(u) R((1+\delta)u)\,du$ into $\int_{(1+\delta)ax}^{(1+\delta)bx} \frac{1}{1+\delta}g(\frac{v}{1+\delta}) R(v)\,dv$ with new limits of integration $(1+\delta)ax$ and $(1+\delta)bx$, which gives
\begin{equation}\label{eq:cross-parts}
\begin{aligned}
\int_{ax}^{bx} g(u) E(u)\,du &= \int_{ax}^{bx} \left(\frac{1}{1+\delta}g\!\left(\frac{v}{1+\delta}\right) - g(v)\right) R(v)\,dv \\
&\quad + \left(\int_{bx}^{(1+\delta)bx} - \int_{ax}^{(1+\delta)ax}\right) \frac{1}{1+\delta}g\!\left(\frac{v}{1+\delta}\right) R(v)\,dv.
\end{aligned}
\end{equation}
Since $1 - (1+\delta)^{-k} \le k\delta$ for $k = 1, 2, 3$ and $0 < u \le x$, the interior factor $\bigl|\frac{1}{1+\delta}g(\frac{v}{1+\delta}) - g(v)\bigr|$ is bounded on $[0, x]$ by $2(2 + 3)\delta x = 10\delta x$ for $\frac{2}{x}u(x - u)$, by $(1 + 2)\delta x = 3\delta x$ for $x - u$, and by $2(1 + 4 + 3)\delta x = 16\delta x$ for $\frac{2}{x}(x - u)^2$. Since $u \ge x/64 > 10^{16}$ throughout all four intervals, Lemma \ref{lem:SchoenfeldTheta} gives $|R(v)| \le 10^{-6} v \le 10^{-6} x$ on $[ax, bx]$ of length $(b - a)x$, and $|R(v)| \le 10^{-6} v \le 10^{-6}(1+\delta)x \le 2 \cdot 10^{-6} x$ on the boundary intervals $[bx, (1+\delta)bx]$ and $[ax, (1+\delta)ax]$ of lengths $\delta b x$ and $\delta a x$. Summing the four bounds shows that the left-hand side of \eqref{eq:bilinear-identity} is at least $\delta^2 x^3(M - K)$, where
\begin{align}
K &= \frac{1}{10^6}\Biggl[\frac{11}{10}\biggl(10\Bigl(\frac{5}{11} - \frac{1}{64}\Bigr) + 2\cdot\frac{5}{11} + \frac{2}{64}\biggr) + \biggl(3\Bigl(\frac{1}{2} - \frac{5}{11}\Bigr) + 1 + 2\cdot\frac{5}{11}\biggr) \nonumber\\
&\qquad\quad + \frac{11}{10}\biggl(16\Bigl(\frac{63}{64} - \frac{6}{11}\Bigr) + 2\cdot\frac{63}{64} + 2\cdot\frac{6}{11}\biggr) + \biggl(3\Bigl(\frac{6}{11} - \frac{1}{2}\Bigr) + 2\cdot\frac{6}{11} + 1\biggr)\Biggr] \nonumber\\
&= \frac{1}{10^6}\left(\frac{469}{80} + \frac{45}{22} + \frac{3549}{320} + \frac{49}{22}\right) = 2.122585\dots \cdot 10^{-5} < 2.1226 \cdot 10^{-5}.\label{eq:K-def}
\end{align}

To bound the right-hand side of \eqref{eq:quadratic-weight-int}, take $256$ equal steps
\begin{equation}\label{eq:sj-wj-def}
s_j = \frac{6}{11} + \frac{309j}{180224}, \qquad w_j = \frac{121}{50}(1 - s_j)^2 \qquad \text{for } j = 0, \dots, 256,
\end{equation}
so $s_0 = 6/11$, $s_{256} = 63/64$, and $w_0 = 1/2$. The weight $w(u)$ on $E(u)^2$ in \eqref{eq:w-def} is $1/2$ on $[x/64, 6x/11]$ and at most $w_j$ on $[s_j x, s_{j+1} x]$. Since $s_j x \ge (6/11)x \ge 6 \cdot 10^{17} > 5 \cdot 10^{17}$, $w$ is nonincreasing, and $\int_1^{s_j x} E(u)^2 \, du \le J_\theta(s_j x, \delta) \le c \, \delta \log^2(2.0001/\delta) s_j^2 x^2$ by \eqref{eq:Jtheta-bound}, Abel summation bounds the right-hand side of \eqref{eq:quadratic-weight-int} by $c \, \delta \log^2(2.0001/\delta) x^2 U$, where
\begin{equation}\label{eq:U-def}
U = \sum_{j=1}^{255} (w_{j-1} - w_j) s_j^2 + w_{255} s_{256}^2 = 0.2492140\dots < 0.24922.
\end{equation}

Since $h \ge 2.0001$, we have $\log(2.0001/\delta) \le \log x$. Using $\delta = H\log^2 x / x$ and dividing by $\delta x^2 \log^2 x$, no Goldbach number in $(x, x + h]$ forces $H(M - K) \le c \cdot 0.24922$. Thus it is enough that
\begin{equation}\label{eq:H-criterion}
(1.001 J + 0.0019) \cdot 0.24922 < H(M - K).
\end{equation}
With $J = 1.0069$ from Proposition \ref{prop:Jpsi}, the left-hand side of \eqref{eq:H-criterion} is $0.2516641$, and $H = 4.44$ gives right-hand side $0.2517492$; the smallest $H$ that works is $H_{\min} = 4.43850$. This gives a Goldbach number $n$ with $x < n \le x + 4.44\log^2 x$, and the extra $0.01\log^2 x$ in the theorem gives the strict upper bound in $(x, x + 4.45\log^2 x)$.
\end{proof}

By \eqref{eq:H-criterion}, $H_{\min} = (1.001 J + 0.0019) \cdot 0.24922 / (M - K)$, so $H_{\min}$ is proportional to $c$ and the mean square constant $J$ is the main limiting input; at $J = 1.0069$ the weight scan gives about $4.43$, and the $4.43$ figure is a numerical scan of this weight family at $J = 1.0069$, not a proven lower limit. Lowering the order of the interval length below $\log^2 x$ from the Riemann Hypothesis alone would require an upper bound on the pair correlation of zeros of $\zeta(s)$ that is not known; under the Riemann Hypothesis together with Montgomery's pair correlation conjecture \cite{Montgomery1973}, Goldston \cite{Goldston1990} already reaches $(2 + \epsilon)\log x$.

\section{Numerical verification}

All numerical constants in Lemma \ref{lem:diag}, Proposition \ref{prop:Jpsi}, and the proof of Theorem \ref{thm:main} are certified in the Lean 4 kernel conditionally on the seven hypotheses of \texttt{goldbach\_\allowbreak 445\_\allowbreak hsw\_\allowbreak gZ}. The certification uses finite grids with explicit rational parameters: in Lemma \ref{lem:diag}, the case $2^{-188} < \delta \le 10^{-13}$ uses $2161$ pieces on $1 < v \le 139.984375$, a further range $139.984375 < v \le 599.734375$, and a tail $v > 599.734375$, while the case $\delta \le 2^{-188}$ uses a head range $|\gamma| \le 10^{-20}/\delta$ and a dyadic chain of $64$ steps; in Section 4, the interval $[6/11, 63/64]$ is split into $256$ equal Abel steps in $u/x$. Every constant is a decimal or rational number checked by \texttt{norm\_\allowbreak num} and \texttt{linarith} in the Lean kernel, so no floating point arithmetic enters the certificate and no rounding error analysis is needed; transcendental quantities enter only through certified bounds such as $3.141592 < \pi < 3.141593$, $\log 2.0001 \ge 0.6931$, and dyadic bounds on $\log B$. The Lean build completes successfully in $9183$ jobs with exit code $0$, and \texttt{\#print axioms} for \texttt{goldbach\_\allowbreak 445\_\allowbreak hsw\_\allowbreak gZ}, \texttt{theorem2\_\allowbreak u6806}, and \texttt{goldbach\_\allowbreak 445\_\allowbreak of\_\allowbreak J\_\allowbreak hsw} lists only the standard foundational axioms \texttt{propext}, \texttt{Classical.\allowbreak choice}, and \texttt{Quot.\allowbreak sound}. Table \ref{tab:constants} records the certified parameters and margin checks around $H_{\min} = 4.43850$.

\begin{table}[ht]
\centering
\caption{Certified constants and margin checks for the main theorem.}\label{tab:constants}
\small
\begin{tabular}{@{}lll@{}}
\toprule
Quantity & Certified value & Role in proof \\
\midrule
End of the $2161$ pieces & $139.984375$ & In $v = \delta|\gamma|$, Lemma \ref{lem:diag} \\
Pieces & $2161$ & Dyadic rational endpoints on $1 < v \le 139.984375$ \\
Diagonal constant $C_{\mathrm{diag}}$ & $1.0068$ & Bound in \eqref{eq:diag-bound} for $0 < \delta \le 10^{-13}$ \\
Mean square constant $J$ & $1.0069$ & Bound in \eqref{eq:Jpsi-bound} for $x \ge 10^{13}$ \\
Transfer constant $c$ & $1.0098069$ & $c = 1.001 J + 0.0019$ in \eqref{eq:Jtheta-bound} for $X \ge 5 \cdot 10^{17}$ \\
Abel summation steps & $256$ & Equal steps in $u/x$ from $6/11$ to $63/64$ in \eqref{eq:sj-wj-def} \\
Main term constant $M$ & $0.0567215028\dots$ & Exact integral in \eqref{eq:M-def} with weight $\varphi$ \\
Cross-term constant $K$ & $2.1226 \cdot 10^{-5}$ & Cross-term bound in \eqref{eq:K-def} \\
Abel constant $U$ & $0.2492140\dots < 0.24922$ & Upper bound factor in \eqref{eq:U-def} \\
Minimum admissible $H_{\min}$ & $4.43850$ & Threshold in \eqref{eq:H-criterion}; $4.44$ gives $0.2517492 > 0.2516641$ \\
\bottomrule
\end{tabular}
\end{table}

\appendix
\section{Formal verification}\label{app:formal}

The deduction of Theorem \ref{thm:main} from the seven stated hypotheses is formalized in Lean 4 with Mathlib at \url{https://github.com/sthubbar/lean-lab-preprints}, commit \texttt{74c2d1a}. The diagonal estimate of Lemma \ref{lem:diag} is formalized conditionally on \texttt{BPTN} and \texttt{Ordinates14} as \texttt{diag\_\allowbreak u6806}, the short interval mean square bound of Proposition \ref{prop:Jpsi} conditionally on \texttt{ExplicitA}, \texttt{HadamardK}, \texttt{Ordinates14}, and \texttt{BPTN} as \texttt{theorem2\_\allowbreak u6806}, and the main result Theorem \ref{thm:main} conditionally on all seven hypotheses as \texttt{goldbach\_\allowbreak 445\_\allowbreak hsw\_\allowbreak gZ} in \texttt{LeanLab/\allowbreak Routes/\allowbreak U1508Compose445.\allowbreak lean}.

Lemma \ref{lem:HadamardK} (\texttt{HadamardK}) is proved in this paper from the partial fraction expansion of $\xi'(s)/\xi(s)$ and Binet's formula for the digamma function, but neither ingredient is formalized here, so Lean takes \texttt{HadamardK} as a hypothesis; the Lean proof therefore covers every step from the seven hypotheses to Theorem \ref{thm:main}, and no step of the proof of Lemma \ref{lem:HadamardK}.

The headline theorem is in file \texttt{LeanLab/\allowbreak Routes/\allowbreak U1508Compose445.\allowbreak lean}, namespace \texttt{LeanLab.\allowbreak Routes.\allowbreak U1508}, and has the exact statement:
{\footnotesize
\begin{verbatim}
theorem goldbach_445_hsw_gZ {Z : ℕ → Finset ZIdx}
    (hE : RiemannHypothesis → ∀ δ, 0 < δ → δ ≤ 1 / 10 ^ 13 →
      SmoothT2.ExplicitA gZ Z δ)
    (hH : RiemannHypothesis → SmoothT2.HadamardK gZ)
    (h14 : SmoothT2.Ordinates14 gZ)
    (hB : RiemannHypothesis → Lemma26B.BPTN gZ)
    (hEv : EvenGoldbachUpTo (4 * 10 ^ 18))
    (hN : HSWN70 gZ) (hHd : HSWHead14 gZ) :
    RiemannHypothesis → ∀ x : ℝ, 3 ≤ x →
      ∃ n : ℕ, IsGoldbachNumber n ∧ x < n ∧
        (n : ℝ) < x + 4.45 * Real.log x ^ 2
\end{verbatim}
}
Here \texttt{gZ} is the family of ordinates of the nontrivial zeros of $\zeta(s)$ with multiplicity; \texttt{ExplicitA} states \eqref{eq:ExplicitA} of Lemma \ref{lem:ExplicitA} as the limit of $-\sum_{\rho \in Z_n} c_\delta(\rho) y^\rho$ along truncations $Z_n$, for almost every $y \ge 2$, with $B(y)$ included as the function \texttt{Bf}, assumed under RH for each $0 < \delta \le 10^{-13}$; \texttt{HadamardK} is Lemma \ref{lem:HadamardK}; \texttt{Ordinates14} states that every ordinate has absolute value at least $14$; \texttt{BPTN} is Lemma \ref{lem:BPTN} for $T \ge 10^{13}$; \texttt{HSWN70} and \texttt{HSWHead14} are \cite[Corollary 1.2]{HSW2021} read as counts of ordinates of both signs, for $T \ge 70$ and $T \ge 14$; and \texttt{Even\allowbreak Goldbach\allowbreak UpTo} is Lemma \ref{lem:GoldbachVerification}. The bound \texttt{Schoenfeld\allowbreak Theta} is not a hypothesis of this theorem. Table \ref{tab:hypotheses} lists the status of each hypothesis in the paper and in Lean; the formal verification is conditional on these seven hypotheses, and the main theorem assumes \texttt{ExplicitA}, \texttt{HadamardK}, and \texttt{BPTN} under RH.

\begin{table}[ht]
\centering
\caption{Hypotheses of \texttt{goldbach\_445\_hsw\_gZ} in the paper and in Lean 4.}\label{tab:hypotheses}
\small
\begin{tabular}{@{}llll@{}}
\toprule
Lean hypothesis & Source & In this paper & In Lean 4 \\
\midrule
\texttt{ExplicitA} & \cite[Equation (12.1)]{MV2007}, Lemma \ref{lem:ExplicitA} & Cited & Assumed as hypothesis \\
\texttt{HadamardK} & Lemma \ref{lem:HadamardK} & Proved under RH & Assumed as hypothesis \\
\texttt{Ordinates14} & \cite[Chapter XV]{Titchmarsh1986}, Lemma \ref{lem:Ordinates14} & Cited & Assumed as hypothesis \\
\texttt{BPTN} & \cite[Lemma 1]{BPT2022}, Lemma \ref{lem:BPTN} for $T \ge 10^{13}$ & Cited & Assumed as hypothesis \\
\texttt{HSWN70} & \cite[Corollary 1.2]{HSW2021} for $T \ge 70$ & Cited & Assumed as hypothesis \\
\texttt{HSWHead14} & \cite[Corollary 1.2]{HSW2021} for $T \ge 14$ & Cited & Assumed as hypothesis \\
\texttt{EvenGoldbachUpTo} & \cite{OSHP2014}, Lemma \ref{lem:GoldbachVerification} & Cited & Assumed as hypothesis \\
\bottomrule
\end{tabular}
\end{table}

\subsection*{Structure of the Lean formalization}

The formal proof is organized along the following chain of Lean 4 files and theorems; items 1 to 4 are in \texttt{LeanLab/\allowbreak ChirreHagen2025/} and items 5 and 6 in \texttt{LeanLab/\allowbreak Routes/}:
\begin{enumerate}
\item \texttt{U1263Core.\allowbreak lean} (namespace \texttt{LeanLab.\allowbreak ChirreHagen2025.\allowbreak U1263}) proves \texttt{piece\_\allowbreak sum} (the piece bound \eqref{eq:piece-bound}), \texttt{pt\_\allowbreak raw}, \texttt{pt\_\allowbreak norm}, and \texttt{one\_\allowbreak sub\_\allowbreak cos\_\allowbreak le}, while \texttt{U6743Core.\allowbreak lean} provides \texttt{U6743.\allowbreak hu\_\allowbreak pi}:
{\footnotesize
\begin{verbatim}
lemma piece_sum (hN : BPTN γ) (h14 : Ordinates14 γ) {δ : ℝ} (hδ : 0 < δ)
    (hδ1 : δ ≤ 1 / 10 ^ 13) (A B Q lam : ℝ) (hA : 1 ≤ A) (hAB : A ≤ B)
    (hlam : Real.log B ≤ lam) (hlam5 : lam ≤ 5) (hQ : 0 ≤ Q)
    (hc : ∀ i, A / δ < |γ i| → |γ i| ≤ B / δ →
      ‖cδ γ δ i‖ ^ 2 ≤ Q * δ ^ 2)
    (s : Finset ι) :
    ∑ i ∈ s.filter (fun i => A / δ < |γ i| ∧ |γ i| ≤ B / δ),
      ‖cδ γ δ i‖ ^ 2 * Real.log |γ i|
      ≤ 0.31831 * (Q * (B - A)) * (δ * Real.log (1 / δ) ^ 2
          + (2 * lam - 1.8) * (δ * Real.log (1 / δ))
          + (lam ^ 2 - 1.8 * lam) * δ)
        + 2 * Q * (δ ^ 2 * (Real.log (1 / δ) + 5) ^ 2)

lemma pt_raw ... (A B Q u : ℝ) (hA : 1 ≤ A)
    (hu : ∀ t, A * (1 - 1 / 10 ^ 13) < t → t ≤ B →
      1 - Real.cos t ≤ u)
    (hQ : (1 / 10 ^ 26 + 2 * (1 + 1 / 10 ^ 13) * u) / A ^ 2 ≤ Q) :
    ∀ i, A / δ < |γ i| → |γ i| ≤ B / δ → ‖cδ γ δ i‖ ^ 2 ≤ Q * δ ^ 2
lemma pt_norm ... (A B lo Q : ℝ) (hA : 1 ≤ A) (hlo0 : 0 ≤ lo)
    (hlo : lo ≤ A * (1 - 1 / 10 ^ 13))
    (hQ : 2 * (1 + 1 / 10 ^ 13) *
      (1 / 2 - lo ^ 2 / 24 + B ^ 4 / 720) + 1 / 10 ^ 26 ≤ Q) : ...
lemma one_sub_cos_le (x : ℝ) :
    1 - cos x ≤ x ^ 2 / 2 - x ^ 4 / 24 + x ^ 6 / 720
\end{verbatim}
}
\item The $2161$ pieces on $[1, 139.984375]$ are spread over nine split files \texttt{U6806DiagASpS1.lean} to \texttt{U6806DiagASpS3.lean}, \texttt{U6806DiagBSpS1.lean} to \texttt{U6806DiagBSpS3.lean}, and \texttt{U6806DiagCSpS1.lean} to \texttt{U6806DiagCSpS3.lean}, with $241$, $240$, $240$, $240$, $240$, $240$, $259$, $259$, and $202$ applications of \texttt{piece\_\allowbreak sum}, respectively. Table \ref{tab:pieces} gives three representative pieces exactly as certified in Lean.

The complete list of piece endpoints and majorants is the $2161$ applications of \texttt{piece\_\allowbreak sum} in the nine split files named there, public at the repository and commit already cited, so the full partition can be read from those files; the endpoints were chosen by numerical exploration outside Lean, and the correctness of Lemma \ref{lem:diag} (conditional on \texttt{BPTN} and \texttt{Ordinates14}) does not depend on how they were chosen, because every piece bound is checked in the Lean kernel.
\item \texttt{U6806DiagCSpS3.\allowbreak lean} (namespace \texttt{LeanLab.\allowbreak ChirreHagen2025.\allowbreak U6806}) assembles the diagonal bound \texttt{diag\_\allowbreak u6806}, conditional on \texttt{BPTN} and \texttt{Ordinates14}:
{\footnotesize
\begin{verbatim}
theorem diag_u6806 (hN : BPTN γ) (h14 : Ordinates14 γ) {δ : ℝ}
    (hδ : 0 < δ) (hδ1 : δ ≤ 1 / 10 ^ 13) (s : Finset ι) :
    ∑ i ∈ s, ‖cδ γ δ i‖ ^ 2 * Real.log |γ i|
      ≤ 1.0068 * δ * Real.log (2.0001 / δ) ^ 2
\end{verbatim}
}
\item \texttt{U6806Theorem2Sp.\allowbreak lean} (namespace \texttt{LeanLab.\allowbreak ChirreHagen2025.\allowbreak SmoothT2}) proves the short interval mean square bound \texttt{theorem2\_\allowbreak u6806}:
{\footnotesize
\begin{verbatim}
theorem theorem2_u6806 {γ : ι → ℝ} {Z : ℕ → Finset ι}
    (hE : ∀ δ, 0 < δ → δ ≤ 1 / 10 ^ 13 → ExplicitA γ Z δ)
    (hH : HadamardK γ) (h14 : Ordinates14 γ)
    (hN : Lemma26B.BPTN γ) :
    ∀ x δ : ℝ, 10 ^ 13 ≤ x → 0 < δ → δ ≤ 1 / 10 ^ 13 →
      Jpsi x δ ≤ 1.0069 * δ * Real.log (2.0001 / δ) ^ 2 * x ^ 2
\end{verbatim}
}
\item \texttt{U1505Theta6HSW.\allowbreak lean} (namespace \texttt{LeanLab.\allowbreak Routes.\allowbreak U1505}) proves the bilinear reduction theorem \texttt{goldbach\_\allowbreak 445\_\allowbreak of\_\allowbreak J\_\allowbreak hsw}.
\item \texttt{U1508Compose445.\allowbreak lean} (namespace \texttt{LeanLab.\allowbreak Routes.\allowbreak U1508}) applies \texttt{LeanLab.\allowbreak Routes.\allowbreak U1505.\allowbreak goldbach\_\allowbreak 445\_\allowbreak of\_\allowbreak J\_\allowbreak hsw} to \texttt{SmoothT2.\allowbreak theorem2\_\allowbreak u6806} to obtain the headline theorem \texttt{goldbach\_\allowbreak 445\_\allowbreak hsw\_\allowbreak gZ}.
\end{enumerate}

\begin{table}[ht]
\centering
\caption{Three representative pieces from the $2161$-piece partition of $[1, 139.984375]$.}\label{tab:pieces}
\begin{tabular}{@{}lllll@{}}
\toprule
$A$ & $B$ & $Q$ & $\lambda$ & Majorant \\
\midrule
$1$ & $1.0029296875$ & $0.9194789$ & $0.0029296875$ & \texttt{pt\_norm}, $\mathrm{lo} = 0.99999$ \\
$5.67578125$ & $5.6884765625$ & $0.0111334$ & $1.7905011127125$ & \texttt{pt\_raw} with \texttt{hu\_poly}, $k = 1$ \\
$139.6982421875$ & $139.984375$ & $0.0001399$ & $4.9456581952875$ & \texttt{pt\_raw} with \texttt{hu\_pi}, $k = 22$ \\
\bottomrule
\end{tabular}
\end{table}

Running \texttt{\#print axioms} for \texttt{goldbach\_\allowbreak 445\_\allowbreak hsw\_\allowbreak gZ}, \texttt{theorem2\_\allowbreak u6806}, and \texttt{goldbach\_\allowbreak 445\_\allowbreak of\_\allowbreak J\_\allowbreak hsw} in Lean 4 prints only the standard foundational axioms of Lean and Mathlib: \texttt{propext}, \texttt{Classical.\allowbreak choice}, and \texttt{Quot.\allowbreak sound}. The Lean code was written with AI assistance and checked by the Lean kernel.

\subsection*{Use of AI}
The argument and the text of this paper were developed with AI tools; the main deduction is checked in Lean 4 as described in the appendix.

\subsection*{Data availability}
{\sloppy The Lean source of every theorem named in this paper, with its full import closure and the original build log, is public at \url{https://github.com/sthubbar/lean-lab-preprints}, commit \texttt{74c2d1a}; the headline theorem is in \texttt{LeanLab/Routes/U1508Compose445.lean} and \texttt{Papers/GoldbachRH445.lean} prints its statement and axioms. The README states exactly what the Lean proves and which inputs are hypotheses. The headline theorem is also registered in the Palomar registry as entry PALOMAR-2026-10-28-000002, version 1, \url{https://palomar-registry.org/entry.html?id=PALOMAR-2026-10-28-000002\&version=1}.\par}

\begin{thebibliography}{12}

\bibitem{BPT2022}
R.~P. Brent, D.~J. Platt, and T.~S. Trudgian,
\emph{The mean square of the error term in the prime number theorem},
J. Number Theory \textbf{238} (2022), 740--762.

\bibitem{ChirreHagen2025}
A.~Chirre and M.~Val{\aa}s~Hagen,
\emph{On Goldbach numbers in short intervals},
Research in Number Theory \textbf{12} (2026), article 82, doi:10.1007/s40993-026-00767-6, arXiv:2512.23534.

\bibitem{CHD2024}
M.~Cully-Hugill and A.~W. Dudek,
\emph{An explicit mean-value estimate for the prime number theorem in intervals},
J. Aust. Math. Soc. \textbf{117} (2024), no.~1, 1--15.

\bibitem{Goldston1990}
D.~A. Goldston,
\emph{Linnik's theorem on Goldbach numbers in short intervals},
Glasgow Math. J. \textbf{32} (1990), no.~3, 285--297.

\bibitem{HSW2021}
E.~Hasanalizade, Q.~Shen, and P.-J.~Wong,
\emph{Counting zeros of the Riemann zeta function},
preprint, arXiv:2107.06506, 2021.

\bibitem{Katai1967}
I.~K\'atai,
\emph{A remark on a paper of Ju.~V. Linnik},
Magyar Tud. Akad. Mat. Fiz. Oszt. K\"ozl. \textbf{17} (1967), 99--100.

\bibitem{Montgomery1973}
H.~L. Montgomery,
\emph{The pair correlation of zeros of the zeta function},
in Analytic Number Theory, Proc. Sympos. Pure Math., vol.~24,
Amer. Math. Soc., Providence, R.I., 1973, 181--193.

\bibitem{MV1975}
H.~L. Montgomery and R.~C. Vaughan,
\emph{The exceptional set in Goldbach's problem},
Acta Arith. \textbf{27} (1975), 353--370.

\bibitem{MV2007}
H.~L. Montgomery and R.~C. Vaughan,
\emph{Multiplicative Number Theory. I. Classical Theory},
Cambridge Studies in Advanced Mathematics, vol.~97,
Cambridge University Press, Cambridge, 2007.

\bibitem{OSHP2014}
T.~Oliveira~e~Silva, S.~Herzog, and S.~Pardi,
\emph{Empirical verification of the even Goldbach conjecture and computation of prime gaps up to $4 \cdot 10^{18}$},
Math. Comp. \textbf{83} (2014), no.~288, 2033--2060.

\bibitem{Schoenfeld1976}
L.~Schoenfeld,
\emph{Sharper bounds for the Chebyshev functions $\theta(x)$ and $\psi(x)$. II},
Math. Comp. \textbf{30} (1976), no.~134, 337--360.

\bibitem{Titchmarsh1986}
E.~C. Titchmarsh,
\emph{The Theory of the Riemann Zeta-Function},
2nd ed., revised by D.~R. Heath-Brown,
Oxford University Press, New York, 1986.

\end{thebibliography}

\end{document}