\documentclass{amsart} \usepackage[utf8]{inputenc} \usepackage{amsmath,amssymb,amsthm} \usepackage{booktabs} \usepackage[hyphens]{url} \usepackage{verbatim} \sloppy \setlength{\emergencystretch}{6em} % Unicode declarations so raw Lean code in verbatim blocks compiles under pdflatex \DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}} \DeclareUnicodeCharacter{211D}{\ensuremath{\mathbb{R}}} \DeclareUnicodeCharacter{2200}{\ensuremath{\forall}} \DeclareUnicodeCharacter{2203}{\ensuremath{\exists}} \DeclareUnicodeCharacter{2264}{\ensuremath{\le}} \DeclareUnicodeCharacter{2265}{\ensuremath{\ge}} \DeclareUnicodeCharacter{221A}{\ensuremath{\sqrt{}}} \DeclareUnicodeCharacter{03C0}{\ensuremath{\pi}} \DeclareUnicodeCharacter{03B3}{\ensuremath{\gamma}} \DeclareUnicodeCharacter{03B9}{\ensuremath{\iota}} \DeclareUnicodeCharacter{230A}{\ensuremath{\lfloor}} \DeclareUnicodeCharacter{230B}{\ensuremath{\rfloor}} \DeclareUnicodeCharacter{208A}{\ensuremath{_+}} \DeclareUnicodeCharacter{2227}{\ensuremath{\wedge}} \DeclareUnicodeCharacter{21A6}{\ensuremath{\mapsto}} \DeclareUnicodeCharacter{2192}{\ensuremath{\to}} \newtheorem{theorem}{Theorem}[section] \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \title[An explicit prime gap under the Riemann hypothesis]{An explicit prime gap under the Riemann hypothesis, formalized in Lean with its prime power input made elementary} \author{Steve Hubbard} \address{Independent Researcher} \begin{document} \begin{abstract} We report on a Lean 4 formalization of Theorem 2 of Dudek, 2015, as numbered in arXiv v2, which states that if the Riemann hypothesis is true, then for every real $x \ge 2$ there is a prime in the interval $(x - (4/\pi)\sqrt{x}\log x, x]$. In the formalization, Theorem 2 is proved assuming the Riemann hypothesis and one cited explicit zero-counting bound of Hasanalizade, Shen and Wong, arXiv:2107.06506. Four cited inputs of the printed proof are replaced in the formal proof. The two that carry the argument are these: first, the prime power contribution $\psi - \theta$ is required only across the moving window $(x - h, x + h]$ and is proved outright in Lean by an elementary counting argument with no cited input and without assuming the Riemann hypothesis; second, the sum over nontrivial zeros is bounded from the cited Hasanalizade, Shen and Wong zero count for $T \ge 70$ by trading slack between the head and tail sums at the split point $T = 2x/h$. The Riemann hypothesis is open and this note makes no progress on it. \end{abstract} \maketitle \section{The paper} This note documents a formalization in Lean 4 of the main explicit prime gap theorem from A.~W.~Dudek, \emph{On the Riemann hypothesis and the difference between primes}, Int.\ J.\ Number Theory 11, 2015, no.\ 3, 771--778, doi:10.1142/S1793042115500426; preprint arXiv:1402.6417, v2, 20 May 2014 \cite{Dudek}. That paper improves the constant $8/5$ of Ramar\'e and Saouter \cite[Theorem 1]{RaSa} to $4/\pi$. Later work went further: Dudek, Greni\'e and Molteni \cite[Theorem 1.1]{DGM} proved a prime in a symmetric interval of total length $(1 + 4/\log x)\sqrt{x}\log x$, and Carneiro, Milinovich and Soundararajan \cite[Theorem 5]{CMS} proved, under the Riemann hypothesis, that for $x \ge 4$ there is a prime in $[x, x + (22/25)\sqrt{x}\log x]$. Theorem 2 of \cite{Dudek} is therefore not the best known constant, and this note is about the formal record of its proof. It is written for readers who use or check formal proofs in analytic number theory. All theorem, lemma and page numbers of \cite{Dudek} in this note are those of arXiv v2. The journal numbering may differ: \cite{CMS} cites the journal paper with Theorem 1.3 for Theorem 3 of arXiv v2. The primary focus of this note is Theorem 2 of arXiv v2 of \cite{Dudek}: \begin{theorem}[Dudek \cite{Dudek}, Theorem 2 of arXiv v2]\label{thm:dudek} Suppose the Riemann hypothesis is true. Then there is a prime in the interval \[ \left(x - \frac{4}{\pi}\sqrt{x}\log x,\, x\right] \] for all $x \ge 2$. \end{theorem} In addition to Theorem 2, Theorem 1 of \cite{Dudek}, which Dudek quotes from Cram\'er, gives a constant $c > 0$ such that \[ \pi(x + c\sqrt{x}\log x) - \pi(x) > \sqrt{x} \] for all $x \ge 2$, and Dudek's Theorem 3 gives a prime in the interval \[ \left(x - (1 + \varepsilon)\sqrt{x}\log x,\, x\right] \] for all sufficiently large $x$. The same Lean entry also proves Theorems 1 and 3 under the same two hypotheses, with $c = 10^8$ for Theorem 1, whereas the remark of the paper that $c = 3 + \varepsilon$ works for large $x$ is not part of the entry. The purpose of this note is to record which inputs the formal proof took and how they differ from those printed in \cite{Dudek}. No discrepancy was found in the steps of Dudek's argument that were formalized. Theorem 2 is proved assuming the Riemann hypothesis and one cited zero count. The Riemann hypothesis is open and this note makes no progress on it. The binary Goldbach conjecture also remains open and is not treated here. The mathematical content of this note is two observations. The proof uses $\psi - \theta$ only across a short window, where the prime power mass is $O(\log^2 x)$ by counting; this is a simplification of this proof over citing Rosser and Schoenfeld. The zero sum can be closed with a zero count whose constant is too large for the separate head and tail bounds, by trading slack at the split point; this is a convenience forced by the chosen input. Neither is claimed as new. The rest of the Lean entry is formalization work. \subsection*{Outline of the paper's proof} Section 2 of \cite{Dudek} establishes Theorem 2 using a weight $w$ on the open interval $(x - h, x + h)$ together with the integrated Chebyshev function \[ \psi_1(x) = \int_2^x \psi(t)\,dt. \] The argument in Section 2 of \cite{Dudek} proceeds through the following steps: \begin{enumerate} \item \textbf{Explicit formula for $\psi_1$, Lemma 4 of \cite{Dudek}.} For $x > 0$, with $x$ not an integer, \[ \psi_1(x) = \frac{x^2}{2} - \sum_{\rho} \frac{x^{\rho+1}}{\rho(\rho+1)} - x \log(2\pi) + \varepsilon(x), \qquad |\varepsilon(x)| < \frac{12}{5}, \] where the sum runs over the nontrivial zeros $\rho$ of the Riemann zeta function. The printed argument bounds a sum over zeros by $2^{3/2}\sum_\rho 1/|\rho|^2$ and quotes the value of this sum from Davenport \cite{Da}. \item \textbf{Weighted prime-power sum via second differences, Lemma 5 of \cite{Dudek}.} For $x > 0$ and $h > 0$, \[ \sum_{n} \Lambda(n) w(n) = h - \frac{1}{h} \Sigma + \varepsilon(h), \qquad |\varepsilon(h)| < \frac{48}{5h}, \] where $\Lambda$ is the von Mangoldt function and \[ \Sigma = \sum_{\rho} \frac{(x+h)^{\rho+1} - 2x^{\rho+1} + (x-h)^{\rho+1}}{\rho(\rho+1)}. \] \item \textbf{Splitting the sum over zeros.} Writing $\rho = 1/2 + i\gamma$ under the Riemann hypothesis, the sum $\Sigma$ over nontrivial zeros is split at $|\gamma| = \alpha x / h$. To bound the head of the sum, the paper uses a zero count, specifically \[ N(T) < \frac{T \log T}{2\pi} \qquad \text{for } T > 15, \] cited as Corollary 1 of Trudgian, Math.\ Comp.\ 81, 2012 \cite{Tr}. To bound the tail of the sum, the paper uses Lemma 1 (ii) of Skewes \cite{Sk}. \item \textbf{Passing from $\Lambda$ to primes.} To pass from the von Mangoldt function $\Lambda$ to primes, the paper uses, in the paper's words, Theorem 14 and equation 5.5 of its reference [7], Rosser and Schoenfeld, 1962 \cite{RS}, namely the two-sided bound \[ 0.98\sqrt{x} < \psi(x) - \theta(x) < 1.11\sqrt{x} + 3x^{1/3} \qquad \text{for } x \ge 121. \] \item \textbf{Positivity of the lower bound for $x \ge 65000$ and finite verification.} Choosing $\alpha = 2$ and \[ h = \frac{2}{\pi}\sqrt{x}\log x, \] the display at the foot of page 6 of arXiv v2 of \cite{Dudek} states that $\sum_{x - h < p \le x + h} \log p$, the sum of $\log p$ over primes $p$ in $(x - h, x + h]$, exceeds \begin{align*} \operatorname{rhs}(x) &= h - \frac{2}{\pi}\left(\frac{x}{\sqrt{x-h}} + \frac{(x+h)^{3/2}}{x}\right)\log\left(\frac{2x}{h}\right) \\ &\quad - 1.11\sqrt{x+h} - 3(x+h)^{1/3} + 0.98\sqrt{x-h} - \frac{48}{5h}, \end{align*} which is positive for all $x \ge 65000$. Positivity of $\operatorname{rhs}(x)$ guarantees the existence of a prime in $(x - h, x + h]$. Replacing $x + h$ by $x$ then yields Theorem 2 from about $66798.7$, namely \[ 65000 + \frac{2}{\pi}\sqrt{65000}\log 65000. \] The remaining values of $x$ below this threshold were checked by computer in the paper, using Mathematica, with no table printed. \end{enumerate} \section{What the formal proof does} In the Lean 4 formalization \cite{Palomar,Repo}, the main theorem corresponding to Theorem 2 of \cite{Dudek} has the full name \begin{center} {\footnotesize \texttt{LeanLab.PNTPort.ExplicitPsi1.Trivial.theorem2\_of\_RH\_hsw}.} \end{center} Its exact Lean declaration, together with the interval predicate and width function, is as follows: {\footnotesize \begin{verbatim} theorem theorem2_of_RH_hsw (hRH : RiemannHypothesis) (hN : LeanLab.Dudek2014.SigmaH.HSWN70 gZ) : ∀ x : ℝ, 2 ≤ x → LeanLab.Dudek2014.PrimeInDudekInterval x \end{verbatim} } with {\footnotesize \begin{verbatim} def PrimeInDudekInterval (x : ℝ) : Prop := ∃ p : ℕ, p.Prime ∧ x - dudekH x < p ∧ (p : ℝ) ≤ x noncomputable def dudekH (x : ℝ) : ℝ := 4 / π * √x * Real.log x \end{verbatim} } The hypotheses and objects appearing in this statement are defined as follows: \begin{itemize} \item \texttt{RiemannHypothesis} is the standard statement of the Riemann hypothesis from Mathlib \cite{Mathlib}. \item \texttt{gZ} is the family of imaginary parts of the zeros of \texttt{riemannZeta} with real part at least $-1/2$, which are the nontrivial zeros, indexed with multiplicity given by \texttt{analyticOrderNatAt}. \item \texttt{HSWN70 gZ} is the one cited input, included explicitly as a hypothesis to the theorem and never declared as an axiom. \end{itemize} The predicate \texttt{HSWN70} is defined in Lean by: {\footnotesize \begin{verbatim} def HSWN70 (γ : ι → ℝ) : Prop := (∀ T : ℝ, 70 ≤ T → ∀ s : Finset ι, ((s.filter (fun i => |γ i| ≤ T)).card : ℝ) ≤ 2 * (Mt T + Rt T)) ∧ (∀ T t : ℝ, 70 ≤ T → T ≤ t → ∀ s : Finset ι, ((s.filter (fun i => T < |γ i| ∧ |γ i| ≤ t)).card : ℝ) ≤ 2 * ((Mt t + Rt t) - (Mt T - Rt T))) \end{verbatim} } where the main term $\operatorname{Mt}(T)$ and remainder bound $\operatorname{Rt}(T)$ are given by \begin{align*} \operatorname{Mt}(T) &= \frac{T}{2\pi}\log\left(\frac{T}{2\pi e}\right) + \frac{7}{8}, \\ \operatorname{Rt}(T) &= 0.1038 \log T + 0.2573 \log\log T + 10.2425. \end{align*} This hypothesis encodes Corollary 1.2 of Hasanalizade, Shen and Wong, arXiv:2107.06506 \cite{HSW}, which states that \[ \left|N(T) - \frac{T}{2\pi}\log\left(\frac{T}{2\pi e}\right)\right| \le 0.1038 \log T + 0.2573 \log\log T + 9.3675 \qquad \text{for } T \ge e. \] In the Lean formalization, this bound is used only for $T \ge 70$. The Lean definitions add $7/8$ to the main term and $7/8$ to the remainder, so that \[ 9.3675 + \frac{7}{8} = 10.2425. \] Thus $\operatorname{Mt}(T) - \operatorname{Rt}(T)$ is exactly the printed lower bound for $N(T)$, and $\operatorname{Mt}(T) + \operatorname{Rt}(T)$ is the printed upper bound plus $7/4$. The factor $2$ counts ordinates $\gamma$ of both signs, $|\gamma| \le T$ and $T < |\gamma| \le t$, since $N(T)$ counts only $0 < \gamma \le T$. Zeros are counted with multiplicity, the standard reading of $N(T)$, which \cite{HSW} prints as a set count. Consequently, the hypothesis \texttt{HSWN70 gZ} holds for the actual nontrivial zeros of the Riemann zeta function given Corollary 1.2 of \cite{HSW}, ensuring that \texttt{theorem2\_of\_RH\_hsw} is not vacuous. The cited zero count itself is not proved in Lean. \begin{table}[ht] \centering \caption{Comparison between the inputs and verification steps printed in Dudek \cite{Dudek} and those used in the Lean 4 formalization.} \label{tab:comparison} {\small \begin{tabular}{@{}p{0.20\textwidth}p{0.28\textwidth}p{0.44\textwidth}@{}} \toprule Component & Printed paper \cite{Dudek} & Lean 4 formalization \\ \midrule Zero hypothesis & Riemann hypothesis & \texttt{RiemannHypothesis} (Mathlib) \\ Zero count input & Trudgian \cite{Tr}, $T > 15$ & \texttt{HSWN70 gZ} from \cite{HSW}, $T \ge 70$ \\ Prime power step & Cited from \cite{RS} for $x \ge 121$ & \texttt{window\_holds}, proved outright \\ $\psi_1$ error bound & $|\varepsilon(x)| < 12/5$ & \texttt{error\_bound} $\le 2.393 < 12/5$ \\ Sum $\sum_\rho 1/|\rho|^2$ & Value from Davenport \cite{Da} & Not used, the route of \texttt{error\_bound} differs \\ Tail of $\sum 1/\gamma^2$ & Lemma 1 (ii) of Skewes \cite{Sk} & \texttt{tail\_inv\_sq}, from \texttt{HSWN70} \\ Large range & $x \ge 65000$ ($X \gtrsim 66798.7$) & \texttt{rhs\_pos} ($x \ge 65000$), $X \ge 66799$ \\ Small range & Mathematica check (unprinted) & \texttt{small\_range} ($2 \le x < 67001$, kernel) \\ \bottomrule \end{tabular} } \end{table} Table~\ref{tab:comparison} summarizes the relationship between the printed proof in \cite{Dudek} and the formal proof. Four cited inputs of the printed proof are replaced: the zero count of \cite{Tr}, the bound of \cite{RS}, the tail bound of \cite{Sk} and the value from \cite{Da}. The zero count of \cite{HSW} is a choice of input, not a correction; this note does not examine whether the input of \cite{Tr} also suffices. The smaller differences are these. The Lean definition of $\psi_1$ is the sum $\sum_{n \le y} (y - n)\Lambda(n)$, which has the same value as the printed integral for $y \ge 2$. The Lean form of Lemma 5 adds the side condition $h < x$, which holds for $x \ge 65000$. Lemma 4 is proved by its own route, and integer $y$ is allowed. Zeros are counted with multiplicity. We present the mathematics of the prime power step and the zero sum in the following two subsections. \subsection{The prime power step, proved with no cited input} A key observation of the formalization is that the proof of Theorem 2 uses the difference $\psi - \theta$ only through its increment across the window $(x - h, x + h]$. In Lean, this windowed inequality is named \texttt{SchoenfeldWindow} and is proved as the theorem \texttt{LeanLab.PrimePowerWindow.window\_holds}: {\footnotesize \begin{verbatim} def SchoenfeldWindow : Prop := ∀ x : ℝ, 65000 ≤ x → (psiF (x + hD x) - thetaF (x + hD x)) - (psiF (x - hD x) - thetaF (x - hD x)) < 1.11 * √(x + hD x) + 3 * (x + hD x) ^ (1 / 3 : ℝ) - 0.98 * √(x - hD x) \end{verbatim} } where \[ \operatorname{hD}(x) = \frac{2}{\pi}\sqrt{x}\log x. \] The theorem \texttt{window\_holds} is proved outright in Lean, assuming no Riemann hypothesis and using no cited input. A companion lemma, \texttt{schoenfeld\_window\_of}, records that the two-sided bound of Rosser and Schoenfeld \cite{RS} cited in the paper implies \texttt{SchoenfeldWindow}; thus the window form is a logical weakening of the printed input and is all that Dudek's argument requires. \begin{proposition}[\texttt{LeanLab.PrimePowerWindow.window\_holds}]\label{prop:window} For every real $x \ge 65000$, with $h = \operatorname{hD}(x) = (2/\pi)\sqrt{x}\log x$, \[ \bigl(\psi(x+h) - \theta(x+h)\bigr) - \bigl(\psi(x-h) - \theta(x-h)\bigr) < 1.11\sqrt{x+h} + 3(x+h)^{1/3} - 0.98\sqrt{x-h}. \] \end{proposition} The proof goes through the following bound on the mass of the window. \begin{lemma}[\texttt{LeanLab.PrimePowerWindow.mass\_le} with \texttt{diff\_eq}]\label{lem:mass} Let $1 \le a \le b$ be real numbers with $b^{1/3} < a^{1/3} + 1$. Then \[ \bigl(\psi(b) - \theta(b)\bigr) - \bigl(\psi(a) - \theta(a)\bigr) \le \frac{\log b}{2}\bigl(\sqrt{b} - \sqrt{a} + 1\bigr) + \frac{(\log b)^2}{3\log 2}. \] \end{lemma} \begin{proof} Since $\psi(y) = \sum_{n \le y} \Lambda(n)$ and $\theta(y) = \sum_{p \le y} \log p$, the difference $\psi(y) - \theta(y)$ is the sum of $\Lambda(n)$ over non-prime integers $n \le y$. Consequently, the left side of the lemma is precisely the von Mangoldt mass of the prime powers $p^k$ with $k \ge 2$ lying in the interval $(a, b]$. First, the lemma \texttt{sum\_nonprime\_le} bounds the non-prime von Mangoldt mass over a natural-number interval $(A, B]$ with $A \le B$: \[ \sum_{\substack{A < n \le B \\ n \text{ not prime}}} \Lambda(n) \le \sum_{2 \le k \le \log_2 B} \frac{\log B}{k} \cdot \#\{m \in \mathbb{N} : A < m^k \le B\}. \] Indeed, every non-prime $n \in (A, B]$ with $\Lambda(n) \ne 0$ is of the form $n = p^k$ for a prime $p$ and an integer $k \ge 2$ satisfying $k \le \log_2 B$. For such $n$, its von Mangoldt weight satisfies \[ \Lambda(n) = \log p = \frac{\log(p^k)}{k} \le \frac{\log B}{k}, \] and for each fixed exponent $k$, the map $n \mapsto p$ is injective. Second, the lemma \texttt{count\_le} bounds the number of $k$-th powers in the integer interval $(\lfloor a \rfloor, \lfloor b \rfloor]$ for real numbers $0 \le a \le b$: \[ \#\{m \in \mathbb{N} : \lfloor a \rfloor < m^k \le \lfloor b \rfloor\} \le b^{1/k} - a^{1/k} + 1. \] Applying these two bounds separates the prime powers in $(a, b]$ into squares, $k = 2$, and higher powers, $3 \le k \le \log_2 b$: \begin{itemize} \item For $k = 2$, there are at most $\sqrt{b} - \sqrt{a} + 1$ squares in $(a, b]$, each carrying weight $\log p \le \frac{1}{2}\log b$. \item For each $3 \le k \le \log_2 b$, the bound $b^{1/k} < a^{1/k} + 1$ follows from the case $k = 3$ by \texttt{rpow\_sub\_mono}, so there is at most one $k$-th power in $(a, b]$, by \texttt{count\_le\_one}, carrying weight $\log p \le \frac{1}{k}\log b \le \frac{1}{3}\log b$. \end{itemize} There are at most $\log b/\log 2$ exponents $k$, which gives the last term. \end{proof} \begin{proof}[Proof of Proposition \ref{prop:window}] Let $h = \operatorname{hD}(x)$, $a = x - h$, $b = x + h$, $u = x^{1/6}$, $L = \log x$ and $M = \log b$. For all $x \ge 65000$, \[ u \ge 6.34, \qquad L \le 1.5u + 2.32, \qquad L \ge 11, \qquad h \le 0.63662\,u^3 L. \] These give $h \le x/10$, so $0.9x \le a$ and $b \le 1.1x$. Hence $\sqrt{a} \ge 0.948\,u^3$, and $(\sqrt{b} - \sqrt{a})(\sqrt{b} + \sqrt{a}) = 2h$ gives $\sqrt{b} - \sqrt{a} \le 0.6716\,L$. Also $a^{1/3} \ge 0.965\,u^2$ gives $b < (a^{1/3} + 1)^3$, so Lemma \ref{lem:mass} applies. Further $L \le M \le L + 0.1 \le 1.5u + 2.42$. Since $\sqrt{a} \le u^3 \le \sqrt{b}$ and $u^2 \le b^{1/3}$, the target satisfies \[ 1.11\sqrt{b} + 3b^{1/3} - 0.98\sqrt{a} \ge 0.13\,u^3 + 3u^2. \] By Lemma \ref{lem:mass} and $3\log 2 \ge 2.0794$, the window mass is at most \[ \frac{M}{2}(0.6716\,M + 1) + \frac{M^2}{2.0794} \le 0.8168\,M^2 + 0.5\,M. \] Substituting $M \le 1.5u + 2.42$, the proof closes with the polynomial inequality \[ 0.8168\,(1.5u + 2.42)^2 + 0.5\,(1.5u + 2.42) < 0.13\,u^3 + 3u^2 \qquad \text{for } u \ge 6.34, \] which is checked in Lean. \end{proof} \subsection{The zero sum, from the Hasanalizade, Shen and Wong count} The bound on the zero sum $\Sigma$ is formalized as \texttt{LeanLab.Dudek2014.SigmaH.sigmaBd\_of\_hsw}, with conclusion \texttt{SigmaBd}, which is the bound of Section 2.2 of \cite{Dudek} at $\alpha = 2$, on page 5 of the arXiv version: \begin{proposition}[\texttt{LeanLab.Dudek2014.SigmaH.sigmaBd\_of\_hsw}]\label{prop:sigma} Let $\gamma$ be any family of real ordinates satisfying \texttt{HSWN70}, and let $\Sigma$ be the sum of Dudek's Lemma 5 over $\rho = 1/2 + i\gamma$, written \texttt{Zr} in Lean. For every $x \ge 65000$, with $h = \operatorname{hD}(x)$, \[ |\Sigma| \le \left(\frac{2xh}{\pi\sqrt{x-h}} + \frac{4h(x+h)^{3/2}}{2\pi x}\right)\log\left(\frac{2x}{h}\right). \] \end{proposition} This theorem takes no Riemann hypothesis. The hypothesis enters only in \texttt{theorem2\_of\_RH\_hsw}, through \texttt{Zr\_eq\_Zreal}, which identifies the sum over the family \texttt{gZ} with the sum over the nontrivial zeros. The final bound has the same form as the bound in Dudek's paper. The route differs. From the count \texttt{HSWN70}, with its constant $10.2425$, the separate head and tail estimates that would give this form do not both hold near $T = 70$: the tail inequality \[ \sum_{|\gamma| > T} \frac{1}{\gamma^2} \le \frac{\log T}{\pi T} \] needs about $T \ge 170$, while at the split point $T = 2x/h$ with $x \ge 65000$ we only know $T \ge 70$. The formal proof keeps the split at $T = 2x/h$ and trades slack between head and tail through four lemmas: \begin{enumerate} \item \textbf{Head slack, \texttt{head\_count}.} For all $T \ge 70$, the zero count hypothesis \texttt{HSWN70} implies \[ \#\{|\gamma| \le T\} \le \frac{T \log T}{\pi} - \bigl(0.89\,T - 22.25 - 0.502 \log T\bigr), \] so the head count has a positive slack of about $0.89\,T$ below the main term $(T \log T)/\pi$. Indeed, \texttt{HSWN70} gives $\#\{|\gamma| \le T\} \le 2\operatorname{Mt}(T) + 2\operatorname{Rt}(T)$, where \[ 2\operatorname{Mt}(T) = \frac{T \log T}{\pi} - \frac{\log(2\pi) + 1}{\pi}\,T + \frac{7}{4}, \qquad \frac{\log(2\pi) + 1}{\pi} \ge 0.89. \] For $T \ge 70$, the lemma \texttt{Rt\_le} gives $\operatorname{Rt}(T) \le 0.251 \log T + 10.25$, so $2\operatorname{Rt}(T) \le 0.502 \log T + 20.5$, and $7/4 + 20.5 = 22.25$. Write $S(T) = 0.89\,T - 22.25 - 0.502 \log T$ for this slack. \item \textbf{Tail with excess, \texttt{tail\_inv\_sq}.} For $T \ge 70$, partial summation against the second count in \texttt{HSWN70} gives \[ \sum_{|\gamma| > T} \frac{1}{\gamma^2} \le \frac{\log T}{\pi T} + \frac{E(T)}{T^2}, \qquad E(T) = 1.004 \log T + 41.26 - 0.25\,T, \] and the excess $E(T)$ is positive until about $T = 187$. The lemma \texttt{slack} gives $S(T) \ge 0$ and $1.1\,E(T) \le S(T)$ for $T \ge 70$. \item \textbf{Comparison of head and tail weights, \texttt{weight\_ratio}.} Let \[ a = h^2(x-h)^{-1/2} \qquad \text{and} \qquad B = 4(x+h)^{3/2} \] denote the head weight and tail weight, respectively. If $35h \le x$, which is equivalent to $T = 2x/h \ge 70$, then \[ B \le 1.1\,a\,T^2. \] \item \textbf{Combined split bound, \texttt{split\_bound}.} Let $D_i$ denote the second-difference term \[ D_i = \frac{(x+h)^{\rho_i+1} - 2x^{\rho_i+1} + (x-h)^{\rho_i+1}}{\rho_i(\rho_i+1)} \] for the $i$-th zero. Each head term has $\|D_i\| \le a$, by \texttt{second\_diff\_small}, and each tail term has $\|D_i\| \le B/\gamma_i^2$, by \texttt{second\_diff\_large}. The head count and the tail bound give \[ \sum_{i} \|D_i\| \le \left(\frac{T \log T}{\pi} - S(T)\right) a + B\left(\frac{\log T}{\pi T} + \frac{E(T)}{T^2}\right). \] Using $B \le 1.1\,a\,T^2$ and $1.1\,E(T) \le S(T)$, the excess from the tail sum is absorbed into the slack of the head count, which yields \[ \sum_{i} \|D_i\| \le \frac{T \log T}{\pi}\,a + \frac{B \log T}{\pi T}. \] Since $|\Sigma| \le \sum_i \|D_i\|$, substituting $T = 2x/h$, $a = h^2(x-h)^{-1/2}$, and $B = 4(x+h)^{3/2}$, this upper bound equals the displayed formula in \texttt{SigmaBd}. \end{enumerate} \subsection{The rest of the formal proof} The remaining steps of the formalization connect the explicit formula, the positivity of $\operatorname{rhs}(x)$, and the finite prime gap verification to assemble Theorem 2 for all $x \ge 2$: \begin{itemize} \item \textbf{Lemma 4 and Lemma 5, \texttt{lemma4\_Zpatch}.} Lemma 4 of \cite{Dudek} is proved in Lean as \texttt{lemma4\_Zpatch}, combining the explicit formula \texttt{psi1\_formula} and the error estimate \texttt{error\_bound} for all $y > 0$ in the form \[ \left|\psi_1(y) - \left(\frac{y^2}{2} - Z(y) - y \log(2\pi)\right)\right| \le 2.393, \] which is strictly below the printed bound $12/5 = 2.4$. Here $Z(y)$ is the zero sum for $y > 1$; for $y \le 1$ the Lean definition \texttt{Zpatch} takes the value that makes the identity exact, and the proof of Theorem 2 uses $Z$ only for $y > 1$. Lemma 5 of \cite{Dudek} then follows by taking the second difference across $(x-h, x, x+h)$, giving the error bound $48/(5h)$. \item \textbf{Positivity for $x \ge 65000$, \texttt{rhs\_pos}.} The lemma \texttt{rhs\_pos} proves by explicit analytic bounds in Lean that $\operatorname{rhs}(x) > 0$ for every real $x \ge 65000$. \item \textbf{Large range transfer, \texttt{theorem2\_large\_of}.} From the existence of a prime in $(x - \operatorname{hD}(x), x + \operatorname{hD}(x)]$ for all $x \ge 65000$, the theorem \texttt{theorem2\_large\_of} deduces \texttt{PrimeInDudekInterval X} for all $X \ge 66799$ via the intermediate value theorem and monotonicity, since $65000 + (2/\pi)\sqrt{65000}\log 65000$ is about $66798.7$. \item \textbf{Small range verification, \texttt{small\_range}.} The theorem \texttt{small\_range} proves \texttt{PrimeInDudekInterval x} for every real $x$ satisfying $2 \le x < 67001$, with no Riemann hypothesis, by a prime gap scan evaluated by the Lean kernel through \texttt{decide +kernel}. The function \texttt{gapScan} walks the integers of a tier, keeps the last prime seen, and checks $n < \text{last} + g$ at each $n$, so every such $n$ has a prime $p \le n$ with $n - p < g$. Table \ref{tab:gaps} lists the six tiers; the lemma \texttt{gaps\_big} is the last one. Since $g \le \texttt{dudekH}(t)$ at the start $t$ of each tier and \texttt{dudekH} is increasing, the lemma \texttt{tier} gives a prime in the interval. Because the small range $[2, 67001)$ and the large range $[66799, \infty)$ overlap, \texttt{theorem2\_of\_RH\_hsw} covers all $x \ge 2$. \end{itemize} \begin{table}[ht] \centering \caption{The tiers of \texttt{small\_range}. Each integer $n$ in a tier has a prime $p \le n$ with $n - p < g$.} \label{tab:gaps} {\small \begin{tabular}{@{}rrr@{}} \toprule Integers $n$ & Gap $g$ & $\texttt{dudekH}(t)$ at the start $t$, about \\ \midrule $2$ & $1$ & $1.25$ \\ $3$ to $4$ & $2$ & $2.42$ \\ $5$ to $6$ & $2$ & $4.58$ \\ $7$ to $22$ & $4$ & $6.56$ \\ $23$ to $199$ & $14$ & $19.15$ \\ $200$ to $67000$ & $72$ & $95.40$ \\ \bottomrule \end{tabular} } \end{table} \section{Status, cited inputs and data availability} \subsection*{Status of each claim} In Table \ref{tab:status}, Kernel means checked by the Lean kernel at the commit below, Text means argued in this note and not in Lean, and Cited means taken from the source and not proved. \begin{table}[ht] \centering \caption{Status of the claims of this note.} \label{tab:status} {\small \begin{tabular}{@{}p{0.38\textwidth}p{0.26\textwidth}p{0.26\textwidth}@{}} \toprule Claim & Status & Lean name \\ \midrule Theorem \ref{thm:dudek} & Kernel, given \texttt{hRH} and \texttt{hN} & \texttt{theorem2\_of\_RH\_hsw} \\ Proposition \ref{prop:window} & Kernel, no hypothesis & \texttt{window\_holds} \\ Lemma \ref{lem:mass} & Kernel, no hypothesis & \texttt{mass\_le} \\ Proposition \ref{prop:sigma} & Kernel, given \texttt{HSWN70} & \texttt{sigmaBd\_of\_hsw} \\ Lemma 4 in the form with $2.393$ & Kernel, no hypothesis & \texttt{lemma4\_Zpatch} \\ Positivity of $\operatorname{rhs}(x)$ & Kernel, no hypothesis & \texttt{rhs\_pos} \\ Small range & Kernel, no hypothesis & \texttt{small\_range} \\ \texttt{HSWN70 gZ} follows from Corollary 1.2 of \cite{HSW} & Text & none \\ Corollary 1.2 of \cite{HSW} & Cited & hypothesis \texttt{hN} \\ \bottomrule \end{tabular} } \end{table} \subsection*{Cited inputs} Table \ref{tab:inputs} lists every cited input of the printed proof and of the formal proof. Corollary 1.2 of \cite{HSW} was read in arXiv v1. The other four sources were not read for this note; they are quoted as \cite{Dudek} states them, by page of its arXiv v2. \begin{table}[ht] \centering \caption{Cited inputs. Printed statement, page, how the proof uses it, and Lean form.} \label{tab:inputs} {\footnotesize \begin{tabular}{@{}p{0.14\textwidth}p{0.10\textwidth}p{0.29\textwidth}p{0.18\textwidth}p{0.15\textwidth}@{}} \toprule Input & Page & Printed statement & Use & Lean form \\ \midrule Corollary 1.2 of \cite{HSW} & arXiv v1, p.\ 2, display 1.5 & $|N(T) - \frac{T}{2\pi}\log\frac{T}{2\pi e}| \le 0.1038 \log T + 0.2573 \log\log T + 9.3675$ for $T \ge e$ & Used for $T \ge 70$, both signs, $7/8$ added to $\operatorname{Mt}$ and to $\operatorname{Rt}$ & \texttt{HSWN70 gZ} \\ Corollary 1 of \cite{Tr} & \cite{Dudek}, p.\ 5 & $N(T) < T \log T/(2\pi)$ for $T > 15$ & Replaced by \texttt{HSWN70} & none \\ Theorem 14 and 5.5 of \cite{RS} & \cite{Dudek}, p.\ 6 & $0.98\sqrt{x} < \psi(x) - \theta(x) < 1.11\sqrt{x} + 3x^{1/3}$ for $x \ge 121$ & Replaced by the window bound & \texttt{window\_holds} \\ Lemma 1 (ii) of \cite{Sk} & \cite{Dudek}, p.\ 5 & Gives the bound on the tail of the zero sum & Replaced from \texttt{HSWN70} & \texttt{tail\_inv\_sq} \\ Value of $\sum_\rho 1/|\rho|^2$, \cite{Da} & \cite{Dudek}, p.\ 4 & The value of the sum is explicitly known & Not used & none \\ \bottomrule \end{tabular} } \end{table} \subsection*{Data availability} \begin{itemize} \item \textbf{Registry entry:} Palomar registry \texttt{PALOMAR-2026-11-01-000028}, version 1, \url{https://palomar-registry.org/entry.html?id=PALOMAR-2026-11-01-000028&version=1} \cite{Palomar}. \item \textbf{Repository:} \url{https://github.com/sthubbar/goldbach-lean}, directory \texttt{entries/dudek2014}, commit \texttt{da5cf9edad7896290771dfcab8feee2906399e3d} \cite{Repo}. \item \textbf{Toolchain:} Lean and Mathlib version \texttt{v4.35.0-rc3} \cite{Mathlib}. \item \textbf{Build:} in that directory, run \texttt{lake exe cache get}, \texttt{lake build} and \texttt{lake comparator --config=comparator-dudek2014.json}. A fresh public clone of this commit built $9036$ jobs in $1196$ s of wall time on a $2$ core machine. \item \textbf{Axioms and comparator check:} The axioms of the compared theorems are solely the standard Lean foundational axioms \texttt{propext}, \texttt{Quot.sound}, and \texttt{Classical.choice}, with \texttt{0 sorry}. The comparator passed against the challenge file \texttt{ChallengeDudek2014.lean}. \item \textbf{Ported files:} sixteen files under \texttt{LeanLab/PNTPort/StrongPNT} are from the \texttt{PrimeNumberTheoremAnd} project \cite{PNT}, commit \texttt{c39a751132c88b6e8080b74c74023fd95b3d8be0}, Apache-2.0, credited to its contributors. \end{itemize} \medskip \noindent Steve Hubbard designed the research program and directed this work. AI tools, Claude and Gemini, were used to write the Lean code and draft the text. AI agents also did the checks of the Lean against the source, and no human expert has reviewed the mathematics. The author takes full responsibility for the content. \begin{thebibliography}{9} \bibitem[Dudek]{Dudek} A.~W.~Dudek, \emph{On the Riemann hypothesis and the difference between primes}, Int.\ J.\ Number Theory 11 (2015), no.\ 3, 771--778, doi:10.1142/S1793042115500426, arXiv:1402.6417. \bibitem[HSW]{HSW} E.~Hasanalizade, Q.~Shen and P.-J.~Wong, \emph{Counting zeros of the Riemann zeta function}, J.\ Number Theory 235 (2022), 219--241, arXiv:2107.06506. \bibitem[CMS]{CMS} E.~Carneiro, M.~B.~Milinovich and K.~Soundararajan, \emph{Fourier optimization and prime gaps}, arXiv:1708.04122v2, first posted 2017, doi:10.4171/CMH/467. \bibitem[Da]{Da} H.~Davenport, \emph{Multiplicative Number Theory}, Springer, 1980. \bibitem[DGM]{DGM} A.~W.~Dudek, L.~Greni\'e and G.~Molteni, \emph{Primes in explicit short intervals on RH}, Int.\ J.\ Number Theory 12 (2016), no.\ 5, 1391--1407, arXiv:1503.05403. \bibitem[Sk]{Sk} S.~Skewes, \emph{On the difference $\pi(x) - \operatorname{li}(x)$ II}, Proc.\ London Math.\ Soc.\ (3) 5 (1955), 48--70. \bibitem[RS]{RS} J.~B.~Rosser and L.~Schoenfeld, \emph{Approximate formulas for some functions of prime numbers}, Illinois J.\ Math.\ 6, 1962, no.\ 1, 64--94. \bibitem[RaSa]{RaSa} O.~Ramar\'e and Y.~Saouter, \emph{Short effective intervals containing primes}, J.\ Number Theory 98, 2003, no.\ 1, 10--33. \bibitem[Tr]{Tr} T.~S.~Trudgian, \emph{An improved upper bound for the argument of the Riemann zeta-function on the critical line}, Math.\ Comp.\ 81, 2012, no.\ 278, 1053--1061. \bibitem[Palomar]{Palomar} Palomar registry, entry \texttt{PALOMAR-2026-11-01-000028}, version 1, \url{https://palomar-registry.org/entry.html?id=PALOMAR-2026-11-01-000028&version=1}. \bibitem[Repo]{Repo} S.~Hubbard, \texttt{goldbach-lean} repository, directory \texttt{entries/dudek2014}, commit \texttt{da5cf9edad7896290771dfcab8feee2906399e3d}, \url{https://github.com/sthubbar/goldbach-lean}. \bibitem[PNT]{PNT} \texttt{PrimeNumberTheoremAnd}, \url{https://github.com/AlexKontorovich/PrimeNumberTheoremAnd}, commit \texttt{c39a751132c88b6e8080b74c74023fd95b3d8be0}. \bibitem[Mathlib]{Mathlib} The mathlib Community, \emph{The Lean mathematical library}, \url{https://github.com/leanprover-community/mathlib4}, version \texttt{v4.35.0-rc3}. \end{thebibliography} \end{document}