\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{211D}{\ensuremath{\mathbb{R}}}
\DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}}
\DeclareUnicodeCharacter{2192}{\ensuremath{\to}}
\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}}
\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}}
\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}

\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 from explicit analytic inputs, stated as hypotheses, is checked in Lean 4.
\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, a degree-6 Taylor majorant for $1 - \cos$, and a geometric partition of the scaled mid-range $[1, 139.984375]$ into $2161$ pieces, 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.

\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 six 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}
\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.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 set of nontrivial zero ordinates $\gamma'$,
\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 zeros $\rho' = 1/2 + i\gamma'$ counted with multiplicity. Setting $s = 5/2 + i\gamma$, we have
\begin{equation}\label{eq:Hadamard-sum-id}
\sum_{\rho'} \frac{4}{4 + (\gamma - \gamma')^2} = 2 \sum_{\rho'} \operatorname{Re}\frac{1}{s - \rho'}.
\end{equation}
By the partial fraction decomposition of $\xi'(s)/\xi(s)$ \cite[Corollary 10.14]{MV2007},
\begin{equation}\label{eq:Hadamard-partial}
2\sum_{\rho'} \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|$.
\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}, together with the numerical fact, taken as a hypothesis in Lean, that every nontrivial zero has ordinate of absolute value at least $14$.

\begin{lemma}[\cite{OSHP2014}]\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\_u6806}}]\label{lem:diag}
Assume the Riemann Hypothesis. 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$ satisfies the degree-6 majorant
\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.} Let $0 < A < B$ and suppose that $Q\delta^2$ majorizes $|c_\delta(\gamma)|^2$ for $A/\delta < |\gamma| \le B/\delta$; such a $Q$ follows from \eqref{eq:cdelta-exact} and a Taylor majorant of $1 - \cos$ such as \eqref{eq:cos-taylor6} on the piece. With $\lambda$ the piece parameter, Lemma \ref{lem:BPTN} gives
\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}
The piece endpoints are dyadic rationals. 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\_u6806}.
\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\_u6806}}]\label{prop:Jpsi}
Assume the Riemann Hypothesis. 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)$. 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$. By Fubini's theorem, $\int_1^X D(y)\,dy \le \delta X (\psi - \theta)((1+\delta)X)$. When $\delta\sqrt{y} < 1$, every interval $(y^{1/k}, ((1+\delta)y)^{1/k}]$ with $k \ge 2$ has length at most $\frac{1}{2}\delta\sqrt{y} < 1$ and contains at most one prime, so $D(y) \le \log^2((1+\delta)y)/\log 2$. Multiplying this pointwise bound by the $L^1$ bound and using $(\psi - \theta)((1+\delta)X) \le 2\sqrt{(1+\delta)X}\,\log((1+\delta)X)$ shows that $1001 \int_1^X D(y)^2 \, dy \le 0.0019 \, \delta \log^2(2.0001/\delta) X^2$ for $X \ge 5 \cdot 10^{17}$ and $0 < \delta \le 10^{-13}$. Thus, if $J_\psi(X, \delta) \le J \delta \log^2(2.0001/\delta) X^2$, then for $X \ge 5 \cdot 10^{17}$, $0 < \delta \le 10^{-13}$, and $\delta \sqrt{X} < 1$, we have
\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}
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$.

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)$, changing variables $v = (1+\delta)u$ in $\int_{ax}^{bx} g(u) R((1+\delta)u)\,du$ gives
\begin{equation}\label{eq:cross-parts}
\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 + \left(\int_{bx}^{(1+\delta)bx} - \int_{ax}^{(1+\delta)ax}\right) g(u) R((1+\delta)u)\,du.
\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((1+\delta)u)| \le 10^{-6}(1+\delta)u \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\\
&= 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}

At $J = 1.0069$, this family of piecewise linear weights cannot go much below about $4.43$. 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, 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} were certified by rational arithmetic over finite grids and verified inside the Lean 4 kernel. In Lemma \ref{lem:diag}, the range $1 < v \le 139.984375$ of the scaled variable $v = \delta|\gamma|$ is split into $2161$ pieces with dyadic rational endpoints, each bounded by \eqref{eq:piece-bound} with the explicit zero count from Lemma \ref{lem:BPTN}. In Section 4, the interval $[6/11, 63/64]$ for $u/x$ is partitioned into $256$ equal steps; the main term $M$ in \eqref{eq:M-def}, the cross-term bound $K$ in \eqref{eq:K-def}, and the Abel summation factor $U$ in \eqref{eq:U-def} are evaluated by exact rational arithmetic. 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}
\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}

The deduction of Theorem \ref{thm:main} from the inputs in Section 2 is formalized in Lean 4 with Mathlib in the files \texttt{ChirreHagen2025/U6806Theorem2Sp.lean} and \texttt{Routes/U1508Compose445.lean}. The diagonal estimate of Lemma \ref{lem:diag} is formalized as \texttt{diag\_u6806}, the short interval mean square bound of Proposition \ref{prop:Jpsi} as \texttt{theorem2\_u6806}, and the main result Theorem \ref{thm:main} as \texttt{goldbach\_445\_hsw\_gZ} in \texttt{U1508Compose445.lean}. The Lean formalization takes \texttt{SmoothT2.HadamardK} as a hypothesis, whereas the paper proves it in Lemma \ref{lem:HadamardK}.

The headline theorem in Lean 4 has the following statement:
\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{EvenGoldbachUpTo} is Lemma \ref{lem:GoldbachVerification}. The bound \texttt{SchoenfeldTheta} 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 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}
\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}

Running \texttt{\#print axioms goldbach\_445\_hsw\_gZ} in Lean 4 prints only the standard foundational axioms of Lean and Mathlib: \texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.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}
The Lean files are available from the author on request. A public release with a commit hash is in preparation.

\begin{thebibliography}{11}

\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{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}