\documentclass[11pt,reqno]{amsart} \usepackage[utf8]{inputenc} \usepackage[T1]{fontenc} \usepackage{amsmath,amssymb,amsthm} \usepackage{booktabs} \usepackage{array} \usepackage{url} \DeclareUnicodeCharacter{03B1}{\ensuremath{\alpha}} \DeclareUnicodeCharacter{03B5}{\ensuremath{\varepsilon}} \DeclareUnicodeCharacter{2081}{\ensuremath{_1}} \DeclareUnicodeCharacter{2082}{\ensuremath{_2}} \DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}} \DeclareUnicodeCharacter{211D}{\ensuremath{\mathbb{R}}} \DeclareUnicodeCharacter{2192}{\ensuremath{\to}} \DeclareUnicodeCharacter{2200}{\ensuremath{\forall}} \DeclareUnicodeCharacter{2264}{\ensuremath{\le}} \DeclareUnicodeCharacter{2227}{\ensuremath{\land}} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma}[section] \theoremstyle{remark} \newtheorem{remark}{Remark} \title{A lower explicit threshold for Chen's theorem under GRH} \author{Steve Hubbard} \address{Independent Researcher} \begin{document} \begin{abstract} Assume the Generalized Riemann Hypothesis (GRH). We show that every even integer $N \ge \exp(\exp(13.375))$ can be written as $N = p + P_2$, where $p$ is a prime and $P_2$ is either a prime or a product of two primes. This result is conditional on GRH and on Theorems 5, 6, 7 and Lemma 9 of Bordignon and Starichkova (Ramanujan J.\ 64, 2024), together with their auxiliary lemmas, Table 1 and display (6) that their Section 5.4 uses, used at new parameter values inside their own Section 5.4. It is not a new method; it is a re-choice of the parameters $u$ and $\alpha$ in their argument, combined with the observation that Chen's theorem itself needs only that the Section 5.4 main-term combination be positive, not that it exceed $4\cdot 10^{-3}$, because the inequality $\pi_2'(N) \ge \pi_2(N) - \sqrt{N} - 1$ from the proof of their Corollary 1 (Section 5.5, p.\ 1241), which does not involve the threshold, gives $N = p + P_2$ as soon as $\pi_2(N) > \sqrt{N} + 1$. In Lean 4 the threshold statement itself is stated with GRH as an explicit hypothesis and proved conditional on the journal's Theorems 5, 6, 7 and the linear sieve Theorem 4 at the constants used; Lemma 9, the Section 5.5 step, $\varepsilon(1500) < 1/8349$ and the Section 5.4 bracket arithmetic are proved in Lean. Theorems 5, 6, 7 and Theorem 4 are not formalized. The linear sieve is used in the printed fixed level form; see Remark \ref{rem:level}. \end{abstract} \maketitle \section{Introduction} In 1973, Chen \cite{Chen} proved that every sufficiently large even integer $N$ can be represented as \[ N = p + P_2, \] where $p$ is a prime and $P_2$ is a prime or a product of two primes. While the binary Goldbach conjecture remains open, and this note makes no progress on it, substantial work has gone into making the threshold for Chen's theorem explicit. Yamada \cite{Yamada} claimed the threshold $\exp(\exp(36))$; \cite{BJS} reports mistakes in that argument. Unconditionally, Bordignon, Johnston and Starichkova \cite{BJS} state Chen's theorem for all even integers $N \ge \exp(\exp(32.7))$. Johnston and Starichkova \cite{JS} proved related explicit results on writing even integers as a prime plus an almost prime. In related formal work, a qualitative Lean 4 formalization of Chen's theorem with an existential, non-explicit threshold is claimed in the unrefereed repository \cite{Lean}. Assuming the Generalized Riemann Hypothesis (GRH), Bordignon and Starichkova lowered the explicit threshold considerably. In the arXiv version \cite{BS-arXiv} (v1, the only arXiv version), they obtained the threshold $\exp(\exp(15.85))$ with lower-bound constant $4\cdot 10^{-4}$. In the published journal version \cite{BS-RJ} (Theorem 3, p.\ 1214), they proved under GRH that \[ \pi_2(N) > 4\cdot 10^{-3} U_N \frac{N}{\log^2 N} \quad\text{for } N > \exp(\exp(14)), \] from which their Corollary 1 (p.\ 1214) gives Chen's theorem for these $N$. We are not aware of a published GRH threshold below $\exp(\exp(14))$. In this note we establish the threshold $\exp(\exp(13.375))$ under GRH by re-choosing the parameters $u$ and $\alpha$ inside Section 5.4 of \cite{BS-RJ}. The note is written for analytic number theorists working on explicit sieve bounds. Its lower bound constant for $\pi_2(N)$ is $9\cdot 10^{-5}$, against $4\cdot 10^{-3}$ in Theorem 3 of \cite{BS-RJ}, so the lower threshold comes at the cost of the constant. \begin{theorem}[Main statement]\label{thm:main} Assume the Generalized Riemann Hypothesis, and assume Theorems 5, 6, 7 and Lemma 9 of Bordignon and Starichkova \cite{BS-RJ}, together with the auxiliary lemmas, Table 1 and display (6) of \cite{BS-RJ} that their Section 5.4 uses, used at new parameter values inside their own Section 5.4, with Theorems 5, 6, 7 read with $U_N$ replaced by twice its printed value, Appendix \ref{app:factor2}, and with Theorem 4 of \cite{BS-RJ} used in its printed fixed level form, Remark \ref{rem:level}. Then every even integer $N \ge \exp(\exp(13.375))$ can be written as $N = p + P_2$, with $p$ a prime and $P_2$ a prime or a product of two primes. \end{theorem} \begin{remark}[Level of the sieve input]\label{rem:level} The induction in the proof of Theorem 4 of \cite{BS-RJ} passes to sifting level $p$ below $z$, so it uses inequality (2) at every level, while the proofs of Theorems 5 to 7 check (2) at level $z$ only. We use Theorem 4 in its printed fixed $z$ form as a hypothesis. We do not claim the printed result is wrong. \end{remark} Lemma 9 is also proved in Lean, Section 3, so the cited inputs actually needed are Theorems 5, 6, 7 and Theorem 4 with Table 1 and display (6). \textbf{What is formally verified.} In Lean 4 the threshold statement is proved with GRH as an explicit hypothesis and Theorems 5, 6, 7 and Theorem 4 of \cite{BS-RJ} as explicit unformalized hypotheses, while Lemma 9, the Section 5.5 step, $\varepsilon(1500) < 1/8349$, and the Section 5.4 bracket arithmetic with all correction factors and error terms are kernel-checked (Section 3). \textbf{Context.} GRH thresholds indicate how far the explicit sieve method can go when zero-free regions are not the bottleneck. Within Table 1 of \cite{BS-RJ} the optimum is about $13.365$ at $u$ near $1628$ (Section 2.4). The sieve table of \cite{BJS}, arXiv v6, which takes $\varepsilon \le 1/74$, has smaller constants, for instance $C_1 = 109$ and $C_2 = 110$ in its row $\varepsilon^{-1} = 2000$, and would give about $13.345$ by the same bracket at $u$ near $1628$. That value is from a script and we have not certified it in Lean. \section{The parameter re-choice in Section 5.4 of \cite{BS-RJ}} Table \ref{tab:glossary} summarizes the notation of \cite{BS-RJ} used throughout this note ($\gamma$ denotes Euler's constant). \begin{table}[htbp] \centering \caption{Glossary of notation from \cite{BS-RJ}.} \label{tab:glossary} \footnotesize \begin{tabular}{@{}p{0.28\textwidth}p{0.42\textwidth}p{0.24\textwidth}@{}} \toprule Symbol & Meaning & Place in \cite{BS-RJ} \\ \midrule $\pi_2(N)$ & representations of $N$ as a prime plus a product of at most two primes & Theorem 3, p.\ 1214 \\ $\pi_2'(N)$ & the same with a square-free semiprime & Section 5.5, p.\ 1241 \\ $U_N$ & $e^{-\gamma}\prod_{p>2}\bigl(1-\frac{1}{(p-1)^2}\bigr)\prod_{p>2,\,p\mid N}\frac{p-1}{p-2}$, as printed; see Appendix \ref{app:factor2} for the factor $2$ & Theorem 3 and Lemma 10 \\ $X_2$ & lower bound for $N$ in Theorems 5 to 7, $N \ge X_2 \ge 4\cdot 10^{18}$ & Theorems 5 to 7 \\ $z, y$ & $z = N^{1/8}$, $y = N^{1/3}$ & Section 5, p.\ 1226 \\ $\mathcal A, \mathcal B$ & sifted sets, $\mathcal A = \{N-p\}$ & p.\ 1227 \\ $A, u$ & parameters of Theorems 5 to 7, $A > 0$, $u \in [400,10^8]$ & Theorems 5 to 7 \\ $\alpha_i$ & level parameters with $D = N^{1/2-\alpha_i}$ & Theorems 5 to 7 \\ $\varepsilon(u)$ & prime-sum error parameter & display (6), p.\ 1221 \\ $C_1(\varepsilon), C_2(\varepsilon)$ & linear sieve constants via inequality (2) of Theorem 4, p.\ 1218 & Table 1, pp.\ 1217--1218 \\ $\varepsilon_1$ & parameter in $(0,1)$ & Theorem 7 \\ $\bar c$ & $\int_{1/8}^{1/3}\frac{\log(2-3\beta)}{\beta(1-\beta)}\,d\beta < 0.363084$ & Lemma 14, p.\ 1237 \\ $\bar m$ & bilinear remainder factor & (31), pp.\ 1239--1240 \\ $M_\varphi$ & upper-bound factor in Lemma 5 & Lemma 5, p.\ 1216 \\ \bottomrule \end{tabular} \end{table} We begin by recording what the paper of Bordignon and Starichkova \cite{BS-RJ} does: \begin{itemize} \item In \cite{BS-RJ}, Theorem 3, p.\ 1214, under GRH, gives the bound displayed in the Introduction for $N > \exp(\exp(14))$. Their Corollary 1 (p.\ 1214) gives Chen's theorem for these $N$, passing from $\pi_2(N)$ to $\pi_2'(N)$ via $\pi_2'(N) \ge \pi_2(N) - \sqrt{N} - 1$ (Section 5.5, p.\ 1241). \item Their Section 5.4, p.\ 1241, combines Theorem 5 (p.\ 1228, proof p.\ 1229), Theorem 6 (p.\ 1231), Theorem 7 (pp.\ 1234--1235), and Lemma 9 (p.\ 1227, Chen's weighted sieve inequality bounding $\pi_2(N)$ below by sifting functions minus $2N^{7/8} + N^{1/3}$), at \[ u = 1000, \quad \alpha_1 = \alpha_2 = \alpha_3 = 10^{-3}, \quad A = 10, \quad \varepsilon_1 = 10^{-20}, \] with $\varepsilon(1000) < 1/5235$, $C_1 = 113$, and $C_2 = 114$. \item The arXiv version \cite{BS-arXiv} (v1) had $\exp(\exp(15.85))$ with constant $4\cdot 10^{-4}$. \end{itemize} All changes in the present note take place inside Section 5.4 of \cite{BS-RJ} (p.\ 1241): \begin{enumerate} \item We choose the parameters \[ u = 1500, \quad \alpha_1 = \alpha_2 = \alpha_3 = 0.00256, \quad A = 10, \quad \varepsilon_1 = 10^{-20}. \] \item From display (6) of \cite{BS-RJ}, p.\ 1221, we have $\varepsilon(1500) < 1/8349$; see Appendix \ref{app:eps} for the computation giving $\varepsilon(1500) = 1/8349.3238$. \item We take $C_1 = 112$ and $C_2 = 114$, the row $\varepsilon^{-1} = 6100$ of Table 1 of \cite{BS-RJ}, pp.\ 1217 to 1218, and apply Theorem 4 with $\varepsilon = 1/8349$. This is valid since $C_1(\varepsilon)$ and $C_2(\varepsilon)$ are decreasing in $1/\varepsilon$, as stated after the sieve table of \cite{BJS}; the journal does the same with $\varepsilon(1000) < 1/5235$ and the row $4500$. \item The key observation is that Chen's theorem needs only that the Section 5.4 combination be positive, not that it exceed $4\cdot 10^{-3}$: the threshold-free inequality $\pi_2'(N) \ge \pi_2(N) - \sqrt{N} - 1$ (Section 5.5, p.\ 1241) gives $N = p + P_2$ once $\pi_2(N) > \sqrt{N} + 1$ (Lemma \ref{lem:pos}), letting $\log\log X_2$ drop to $13.375$. \end{enumerate} \begin{table}[htbp] \centering \caption{Comparison of Section 5.4 parameters in \cite{BS-RJ} and in this note.} \label{tab:params} \begin{tabular}{@{}lcc@{}} \toprule Quantity & \cite{BS-RJ}, \S5.4 & This note \\ \midrule $\log\log X_2$ & $14$ & $13.375$ \\ $u$ & $1000$ & $1500$ \\ $\alpha_1 = \alpha_2 = \alpha_3 = \alpha$ & $10^{-3}$ & $0.00256$ \\ $A$ & $10$ & $10$ \\ $\varepsilon_1$ & $10^{-20}$ & $10^{-20}$ \\ Upper bound on $\varepsilon(u)$ & $\varepsilon(1000) < 1/5235$ & $\varepsilon(1500) < 1/8349$ \\ Table 1 row $\varepsilon^{-1}$ (pp.\ 1217 to 1218) & $4500$ & $6100$ \\ $(C_1, C_2)$ & $(113, 114)$ & $(112, 114)$ \\ \bottomrule \end{tabular} \end{table} \subsection{Definition of the main-term constant $\mathrm{K3J}$} We define $\mathrm{K3J}$ as in the Lean formalization (Appendix \ref{app:K3J}), with $g = e^\gamma$, $\varepsilon = 1/8349$, and $\bar{c}$ from Lemma 14 of \cite{BS-RJ}, p.\ 1237, \[ \bar c = \int_{1/8}^{1/3} \frac{\log(2-3\beta)}{\beta(1-\beta)}\,d\beta < 0.363084, \] by setting \begin{equation}\label{eq:K3J} \begin{aligned} \mathrm{K3J} &= 8\,\Bigl( 2g\log(3-8\alpha)/(4-8\alpha) - \varepsilon C_2\cdot 3\, e^{8\alpha-2}/(4-8\alpha) \Bigr) \\ &\, - \tfrac12\cdot 8\Bigl( (1+5\cdot10^{-5}) \Bigl(\tfrac{g}{4}\bigl(\log 6 + \log\tfrac{3-8\alpha}{3-18\alpha}\bigr)/\bigl(\tfrac12-\alpha\bigr) + \log(8/3)\,\varepsilon C_1 \Bigr) \Bigr) \\ &\, - \tfrac12 \Bigl( 2g/\bigl(\tfrac12-\alpha\bigr) + 3\varepsilon C_1 \Bigr)\,\bar c. \end{aligned} \end{equation} Here $1 + 5\cdot 10^{-5}$ is the Lemma 11 (p.\ 1228) factor on Theorem 6's $l_1$, p.\ 1231; in short, with $M = U_N N/\log^2 N$, Theorems 5, 6, 7 give, in turn, \[ \begin{aligned} S(\mathcal A,\mathbb P,z) &> 8M\bigl(2g\log(3-8\alpha) - 3\varepsilon C_2 e^{8\alpha-2}\bigr)/(4-8\alpha) - \cdots,\\ \textstyle\sum_{z\le q 10^{-4}$ is kernel-checked in Lean as \texttt{theorem3\_positive\_main}, so the positivity margin does not rest on the script. \item With the terms $\mathrm{K3J}$ leaves out, namely the $\mathrm{li}$ factor \[ \frac{\log y\,\bigl(\mathrm{li}(y)+\sqrt{y}\log y/(8\pi)\bigr)}{y} = 1 + \frac{1}{\log y} + \frac{2}{\log^2 y} + \dots \] with $y = X_2^{1/3}$ and the $1/\log^2 N$ terms of Theorems 6 and 7, the total with the omitted terms is $1.535054\cdot 10^{-4}$. Thus $\mathrm{K3J} = 1.5960\cdot 10^{-4}$ is the leading coefficient of $U_N N/\log^2 N$, and the total $1.535054\cdot 10^{-4}$ adds back the $\mathrm{li}$ factor and the $1/\log^2 N$ terms; the difference, $6.10\cdot 10^{-6}$, is almost all the $\mathrm{li}$ factor, which exceeds $1$ and multiplies the subtracted Theorem 7 piece (Table \ref{tab:errors}). \end{itemize} All remaining omitted factors, the remainder of (33), and the power-saving error terms from Lemma 9 and Corollary 1 are bounded explicitly in Appendix \ref{app:errors} and are negligible. \begin{lemma}[positivity suffices]\label{lem:pos} Let $N$ be even. If $\pi_2(N) > \sqrt N + 1$, then $N = p + q$ with $p$ prime and $q > 1$ square-free with at most two prime factors; in particular $N = p + P_2$. \end{lemma} \begin{proof} Section 5.5 of \cite{BS-RJ}, p.\ 1241, shows $\pi_2'(N) \ge \pi_2(N) - \sqrt N - 1$, where $\pi_2'(N)$ counts representations of $N$ as a prime plus a square-free integer $q > 1$ with at most two prime factors, since $\pi_2(N)$ also counts prime $q$ and the subtraction removes only $q = 1$ (at most $1$) and integers up to $N$ with two equal prime factors (at most $\sqrt N$). Thus $\pi_2'(N) > 0$. This threshold-free inequality applies with the constant $9\cdot10^{-5}$ of Section 2.2, since $9\cdot10^{-5}U_N N/\log^2 N - 2N^{7/8} - N^{1/3} > \sqrt N + 1$ for $\log\log N \ge 13.375$ by Appendix \ref{app:errors}. \end{proof} \begin{proof}[Proof of Theorem \ref{thm:main}] Let $N \ge X_2 = \exp(\exp(13.375))$ be even. The parameters of this section satisfy the conditions of Table \ref{tab:ranges}, and $\varepsilon(1500) < 1/8349$, so Theorems 5, 6, 7 apply with $\varepsilon = 1/8349$, $C_1 = 112$, $C_2 = 114$. With the weights of Lemma 9, \eqref{eq:app_lem9}, they give \[ \pi_2(N) > \bigl(8B_5 - 4B_6 - \tfrac12 B_7\bigr) U_N \frac{N}{\log^2 N} - 2N^{7/8} - N^{1/3}, \] where $B_5, B_6, B_7$ are the brackets of Appendix \ref{app:K3J}. Section 3 gives $8B_5 - 4B_6 - \tfrac12 B_7 \ge \mathrm{K3J} - 10^{-5} > 9\cdot 10^{-5}$, so \[ \pi_2(N) > 9\cdot 10^{-5} U_N \frac{N}{\log^2 N} - 2N^{7/8} - N^{1/3}. \] By Appendix \ref{app:errors} the right side exceeds $\sqrt N + 1$, and Lemma \ref{lem:pos} yields $N = p + P_2$. \end{proof} \begin{remark}[Threshold with the printed constant $4\cdot 10^{-3}$ kept]\label{rem:1345} \sloppy With the printed constant $4\cdot 10^{-3}$ kept, the same method at $u = 1500$ and $\alpha = 0.0024$ gives $\exp(\exp(13.45))$, with $\mathrm{K3J} = 5.1803\cdot 10^{-3}$ and total $5.1747\cdot 10^{-3}$ in Python, both above $4\cdot 10^{-3}$, and the binding condition $1517.3 \ge 1500$. The numerical optimum at $u = 1500$ is $13.4239$ at $\alpha = 0.0024375$, so $13.45$ is conservative. The value $13.45$ is checked in Lean in \texttt{LeanLab/BS2022GRH/JournalLower.lean}: \texttt{theorem3\_lower\_main} proves $\mathrm{K3J} > 0.0042$ at $\alpha = 0.0024$, $\varepsilon = 1/8349$, $C_1 = 112$, $C_2 = 114$, and \texttt{conditions\_1345} proves the binding condition at $13.45$; build log \texttt{20261020T0403Z-27388-U1166.log}, axioms \texttt{[propext, Classical.choice, Quot.sound]}. \end{remark} \subsection{Verification of parameter ranges at $13.375$ and $13.45$} Table \ref{tab:ranges} checks the parameter conditions of the lemmas and theorems in \cite{BS-RJ}, as printed at level $z$, at $\log\log X_2 = 13.375$ ($\alpha = 0.00256$) and $\log\log X_2 = 13.45$ ($\alpha = 0.0024$); the question of lower levels is Remark \ref{rem:level}. Each listed condition holds in both columns, and only the first row is tight. \begin{table}[htbp] \centering \caption{Parameter range conditions at $\log\log X_2 = 13.375$ ($\alpha = 0.00256$) and $\log\log X_2 = 13.45$ ($\alpha = 0.0024$).} \label{tab:ranges} \footnotesize \begin{tabular}{@{}p{0.44\textwidth}ccc@{}} \toprule Condition and source in \cite{BS-RJ} & Required & At $13.375$ & At $13.45$ \\ \midrule (19), (21), (25) part 2, $\alpha\log X_2 - 11\log\log X_2 \ge u$ & $1500$ & $1500.767$ & $1517.272$ \\ (19), (21), (25) part 1, $\log X_2 \ge (A+1)/\alpha$ & $4296.9$ / $4583.3$ & $643707.69$ & $693842.31$ \\ (25), $\log X_2 \ge 48(A+4/3)$ & $544$ & $643707.69$ & $693842.31$ \\ (25), $\frac{\log X_2}{48} - \frac{34}{3}\log\log X_2 \ge \log 0.44$ & $-0.821$ & $13258.99$ & $14302.61$ \\ $\alpha_1 < 1/8$, $\alpha_2 < 1/24$, $\alpha_3 < 1/16$ & $< 0.041667$ & $0.00256$ & $0.0024$ \\ Lemma 7, p.\ 1221, $\log z = \log X_2/8 > 2753$ & $2753$ & $80463.46$ & $86730.29$ \\ Theorem 5, $s = 4 - 8\alpha \in [3,4]$ & $[3,4]$ & $3.97952$ & $3.98080$ \\ Theorem 6, $k = 8(1/6 - \alpha) \in [1,2]$ & $[1,2]$ & $1.312853$ & $1.314133$ \\ Remark 1, p.\ 1230, $\log H = \frac{\log X_2}{2} - 11\log\log X_2 \ge \log 10^8$ & $18.42$ & $321706.72$ & $346773.21$ \\ Lemma 11, p.\ 1228, $\log\log X_2 \ge 10$ & $10$ & $13.375$ & $13.45$ \\ Lemmas 12 and 13, $X_2 \ge 4\cdot 10^{18}$ (log form) & $42.83$ & $643707.69$ & $693842.31$ \\ Lemma 14, p.\ 1237, $\log y = \log X_2/3 \ge \log 2657$ & $7.885$ & $214569.23$ & $231280.77$ \\ Proof of Theorem 6, p.\ 1234, $\log y \ge \log 286$ & $5.656$ & $214569.23$ & $231280.77$ \\ Theorems 5 to 7, $400 \le u \le 10^8$ & $u = 1500$ & $1500$ & $1500$ \\ \bottomrule \end{tabular} \end{table} \subsection{Headroom and the active constraint} With $u = 1500$ the binding condition is the second part of (19), (21), and (25): $\alpha\log X_2 - 11\log\log X_2 \ge u$. At $\alpha = 0.00256$ it needs $\log\log X_2 \ge 13.374532$, a slack of $0.00047$. Every other range condition holds with a wide margin (Table \ref{tab:ranges}). The total decreases in $\alpha$, so positivity bounds $\alpha$ from above. At $\log\log X_2 = 13.375$ the admissible window is $0.0025588 \le \alpha < 0.0025649$. The joint optimum at $u = 1500$ is $\log\log X_2 = 13.37261$ at $\alpha = 0.0025649$. Letting $u$ vary, with $\varepsilon(u)$ recomputed by display (6) and the best admissible Table 1 row, the script-only optimum of this framework ($A = 10$, $\varepsilon_1 = 10^{-20}$) is about $\log\log X_2 = 13.36525$ at $u$ just above the prime $1627$ with $\alpha = 0.0027829$ (Table \ref{tab:u_opt}). \begin{table}[htbp] \centering \caption{Optimal $\log\log X_2$ as a function of $u$ ($A = 10$, $\varepsilon_1 = 10^{-20}$, $\varepsilon = \varepsilon(u)$ itself; with $\varepsilon = 1/8349$ the $u = 1500$ entry is $13.37261$).} \label{tab:u_opt} \begin{tabular}{@{}cccc@{}} \toprule $u$ & $1/\varepsilon(u)$ & Table 1 row & Optimal $\log\log X_2$ \\ \midrule $1000$ & $5235.67$ & $4500$ & $13.78977$ \\ $1200$ & $6432.64$ & $6100$ & $13.47933$ \\ $1400$ & $7586.12$ & $6100$ & $13.40351$ \\ $1500$ & $8349.32$ & $6100$ & $13.37258$ \\ $1628$ & about $9236$ & $6100$ & $13.36582$ \\ $2000$ & $11401.89$ & $6100$ & $13.42558$ \\ $2200$ & $12589.97$ & $12200$ & $13.46608$ \\ \bottomrule \end{tabular} \end{table} \textbf{Choice of $u$ and $\alpha$.} The parameters $u = 1500$ and $\alpha = 0.00256$ were found by a grid search over $u$ and $\alpha$ with the Section 5.4 total. Although $u = 1628$ gives $13.36582$, about $0.0068$ below $13.37261$ at $u = 1500$ and $0.0092$ below the headline $13.375$, the headline keeps $u = 1500$ and $13.375$ because every Lean certificate (\texttt{eps1500}, \texttt{bracket13375\_holds}, \texttt{mbar\_le}, \texttt{li\_factor}) is proved at $u = 1500$ and $\log\log X_2 = 13.375$; moving to $u = 1628$ would need new kernel certificates for $\varepsilon(1628)$ and the bracket, for a gain under $0.01$. For fixed $u = 1500$ and $\log\log X_2 = 13.375$, the lower end $0.0025588$ solves $\alpha\log X_2 - 11\log\log X_2 = u$ in closed form and the upper end $0.0025649$ is the zero of the total found by bisection in the public script, with $0.00256$ a round value inside it. Smaller $A$ lowers the binding side, by a separate script, to $13.3644$ for $A = 9$ and $13.3561$ for $A = 8$ at $u = 1500$, but the remainder of (33) grows like $10^{20}/\log^{A-4} N$ and stops being negligible at $A = 8$ unless $\varepsilon_1$ is enlarged; this is not pursued. Table \ref{tab:table1_sens} shows the sensitivity to the choice of row in Table 1 of \cite{BS-RJ} at $u = 1500$ and $\varepsilon = 1/8349$. Rows $63$ to $114$ give a negative total for every $\alpha$. The next row, $12200$ with $C_1 = 112$ and $C_2 = 113$, needs $\varepsilon(u)^{-1} \ge 12200$, hence $u$ of about $2130$ or more, which gives at least $13.448$. Thus the $6100$ row is the best admissible one in Table 1 of \cite{BS-RJ}, and no other row of that table reaches $13.375$. \begin{table}[htbp] \centering \caption{Sensitivity to Table 1 of \cite{BS-RJ} at $u = 1500$, $\varepsilon = 1/8349$.} \label{tab:table1_sens} \begin{tabular}{@{}ccccc@{}} \toprule Row $\varepsilon^{-1}$ & $C_1$ & $C_2$ & Total at $\alpha = 0.00256$, $13.375$ & Best $\log\log X_2$ \\ \midrule $2300$ & $114$ & $116$ & $-1.12\cdot 10^{-3}$ & $13.38861$ \\ $3300$ & $113$ & $115$ & $-4.81\cdot 10^{-4}$ & $13.38058$ \\ $4500$ & $113$ & $114$ & $-3.82\cdot 10^{-4}$ & $13.37932$ \\ $6100$ & $112$ & $114$ & $+1.535\cdot 10^{-4}$ & $13.37261$ \\ \bottomrule \end{tabular} \end{table} \section{Formal verification, Lean 4} \sloppy The Lean code is checked only by the Lean kernel (Lean v4.35.0, Mathlib v4.35.0; file paths, namespaces, and build logs are in Appendix \ref{app:build}). Every proved Lean theorem named here depends only on the standard axioms \texttt{[propext, Classical.choice, Quot.sound]}. The files contain two unused \texttt{sorry}: the open deep step \texttt{theorems567\_of\_inputs} in \texttt{ChenThresholdGRH.lean} (Section \ref{subsec:limitations}) and the superseded placeholder \texttt{Cert1567.eps1500\_cert} in \texttt{Cert1567.lean} (replaced in \texttt{chenThreshold13375\_of\_deep\_closed} by \texttt{Cert1575.eps1500}); unused \texttt{sorry} statements in \texttt{LeanLab/DERZ1997/Statements.lean} and \texttt{LeanLab/AlmostPrimeSums/Statements.lean} lie in the import closure but are used by none of the named theorems, as their axiom lists show. Table \ref{tab:lean_map} maps each Lean file to its theorem names and claims, and Table \ref{tab:status} records the verification chain. The core Lean declarations are: {\footnotesize \begin{verbatim} def ChenThreshold13375 : Prop := GRH → ∀ N : ℕ, Even N → exp (exp 13.375) ≤ (N : ℝ) → ChenSqfreeRep N \end{verbatim} } {\footnotesize \begin{verbatim} theorem chenThreshold13375_of_deep_closed (h5 : Thm5J) (h6 : Thm6J) (h7 : Thm7J) (hT4 : LinearSieveT4 (1 / 8349) 112 114) : ChenThreshold13375 \end{verbatim} } {\footnotesize \begin{verbatim} noncomputable def K3J (α g ε C₁ C₂ cb : ℝ) : ℝ := 8 * (2 * g * log (3 - 8 * α) / (4 - 8 * α) - ε * C₂ * 3 * exp (8 * α - 2) / (4 - 8 * α)) - 1 / 2 * (8 * ((1 + 5e-5) * (g / 4 * (log 6 + log ((3 - 8 * α) / (3 - 18 * α))) / (1 / 2 - α) + log (8 / 3) * ε * C₁))) - 1 / 2 * ((2 * g / (1 / 2 - α) + 3 * ε * C₁) * cb) \end{verbatim} } {\footnotesize \begin{verbatim} theorem theorem3_positive_main : (0.0001 : ℝ) < K3J 0.00256 (exp eulerMascheroniConstant) (1 / 8349) 112 114 LeanLab.ChenExplicit.BJS.cbar theorem conditions_13375 : (1500 : ℝ) ≤ 0.00256 * exp 13.375 - 11 * 13.375 ∧ 11 / 0.00256 ≤ exp (13.375 : ℝ) theorem params_ok_13375 : (0.00256 : ℝ) < 1 / 24 ∧ (400 : ℝ) ≤ 1500 ∧ (1500 : ℝ) ≤ 10 ^ 8 ∧ (0 : ℝ) < K3J 0.00256 (exp eulerMascheroniConstant) (1 / 8349) 112 114 LeanLab.ChenExplicit.BJS.cbar \end{verbatim} } {\footnotesize \begin{verbatim} theorem display25_first : max ((10 + 1) / (0.00256 : ℝ)) (48 * (10 + 4 / 3)) ≤ exp 13.375 theorem sieve_ranges_13375 : (3 : ℝ) ≤ 4 - 8 * 0.00256 ∧ 4 - 8 * (0.00256 : ℝ) ≤ 4 ∧ (1 : ℝ) < 8 * (1 / 6 - 0.00256) \end{verbatim} } Here \texttt{ChenSqfreeRep N} means $N = p + m$ with $p$ prime and $m > 1$ square-free with at most two prime factors, and \texttt{GRH} is the lab's predicate for GRH of Dirichlet $L$-functions. Two further details: \begin{itemize} \item In \texttt{Cert1567.bracket13375\_holds : Bracket13375}, for $N \ge X_2 = \exp(\exp 13.375)$ at $\alpha = 0.00256$, $A = 10$, $\varepsilon = 1/8349$, $C_1 = 112$, $C_2 = 114$, $\varepsilon_1 = 10^{-20}$, the exact Theorem 5--7 brackets $B_5, B_6, B_7$ satisfy \[ \mathrm{K3J} - 10^{-5} \le 8\cdot B_5 - \tfrac12\cdot 8\cdot B_6 - \tfrac12\cdot B_7 \] (loss $\approx 6.1\cdot 10^{-6}$, almost all from the Theorem 7 $\mathrm{li}$ factor, giving $10^{-4} - 10^{-5} = 9\cdot 10^{-5}$; Python cross-check $1.535054\cdot 10^{-4}$). \item In \texttt{JournalPositive.lean}, $1.7810699 < e^\gamma < 1.7810725$ uses \texttt{LeanLab.Helfgott2013.GammaFine.exp\_gamma\_gt} and \texttt{exp\_gamma\_lt}, and $\bar c < 0.363084$ uses \texttt{LeanLab.ChenExplicit.BJS.cbar\_lt}. \end{itemize} \begin{table}[htbp] \centering \caption{Lean files, theorem names, and claims.} \label{tab:lean_map} \footnotesize \begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.28\textwidth}>{\raggedright\arraybackslash}p{0.31\textwidth}>{\raggedright\arraybackslash}p{0.35\textwidth}@{}} \toprule Lean file & Theorem names & Claim \\ \midrule \texttt{ChenThresholdGRH.lean} & \texttt{ChenThreshold13375}, \texttt{Thm5J}, \texttt{Thm6J}, \texttt{Thm7J}, \texttt{LinearSieveT4}, \texttt{epsJ}, \texttt{lemma9J\_holds} (\texttt{Lemma9J} via \texttt{U7153.lemma10}, $N \ge 2^{24}$), \texttt{section55\_step}, \texttt{rep\_of\_pi2'}, \texttt{error\_13375}, \texttt{X2\_ranges}, \texttt{cond19\_13375}, \texttt{cond25\_13375} & Threshold proposition and transcribed leaves; Lemma 9 (A.1); $\pi_2' \ge \pi_2 - \sqrt{N} - 1$ and $\pi_2' > 0 \Rightarrow N = p + P_2$ (Lemma \ref{lem:pos}); $2N^{7/8} + N^{1/3} + \sqrt{N} + 1 < 3.6\cdot 10^{-5} N/\log^2 N$ (Appendix \ref{app:errors}); conditions (19), (21), (25) \\ \addlinespace[3pt] \texttt{U7154UN.lean} & \texttt{UNfull}, \texttt{two\_fifths\_le\_UNfull} & $\mathrm{UNfull} \ge 2/5$ (Appendix \ref{app:factor2}) \\ \addlinespace[3pt] \texttt{Cert1575Closed.lean} & \texttt{chenThreshold13375\_of\_}\allowbreak\texttt{deep\_closed} & Headline assembly of Theorem \ref{thm:main} from \texttt{Thm5J}, \texttt{Thm6J}, \texttt{Thm7J}, and \texttt{LinearSieveT4} \\ \addlinespace[3pt] \texttt{JournalMargin.lean} & \texttt{K3J} & Main-term constant definition \eqref{eq:K3J} \\ \addlinespace[3pt] \texttt{JournalPositive.lean} & \texttt{theorem3\_positive\_main}, \texttt{conditions\_13375}, \texttt{params\_ok\_13375} & $\mathrm{K3J} > 10^{-4}$ (\eqref{eq:K3J}, Section 2.2) and binding parameter conditions at $13.375$ \\ \addlinespace[3pt] \texttt{RangeCheck13375.lean} & \texttt{lemma7\_range}, \texttt{display25\_first}, \texttt{display25\_third}, \texttt{remark1\_H}, \texttt{remark1\_H\_vacuity}, \texttt{mono\_step}, \texttt{mono\_range\_13375}, \texttt{sieve\_ranges\_13375} & Eight parameter-range lemmas for Table \ref{tab:ranges} \\ \addlinespace[3pt] \texttt{Cert1567.lean} & \texttt{bracket13375\_holds}, \texttt{mbar\_le}, \texttt{li\_factor} & $8B_5 - 4B_6 - \tfrac12 B_7 \ge \mathrm{K3J} - 10^{-5}$ (gives $\pi_2(N) > 9\cdot 10^{-5} U_N N/\log^2 N - 2N^{7/8} - N^{1/3}$); $\bar m(X_2,10,X_2^{1/8}) \le 40$; $\frac{\log Y(\mathrm{li}\,Y + Y^{1/2}\log Y/(8\pi))}{Y} \le 1 + 4.6702\cdot 10^{-6}$ at $\log Y = L/3$, $L \ge 643700$ (Appendices \ref{app:K3J}, \ref{app:errors}) \\ \addlinespace[3pt] \texttt{Cert1575.lean}, \texttt{Cert1575Closed.lean} & \texttt{eps1500\_proved}, \texttt{eps1500} & $\varepsilon(1500) < 1/8349$, display (6) (Appendix \ref{app:eps}) \\ \bottomrule \end{tabular} \end{table} \begin{table}[htbp] \centering \caption{Logical chain and verification status.} \label{tab:status} \footnotesize \begin{tabular}{@{}cp{0.44\textwidth}p{0.42\textwidth}@{}} \toprule Step & Statement & Checked by \\ \midrule (i) & GRH & Assumed (explicit hypothesis in Lean) \\ \addlinespace[3pt] (ii) & Theorems 5, 6, 7, Theorem 4 with Table 1 of \cite{BS-RJ} & Cited (explicit hypotheses in Lean, not proved) \\ \addlinespace[3pt] (ii$'$) & Lemma 9 of \cite{BS-RJ} & Kernel (\texttt{lemma9J\_holds}) \\ \addlinespace[3pt] (iii) & Their hypotheses hold at the new parameters, Table \ref{tab:ranges} & Kernel for the named lemmas (\texttt{RangeCheck13375.lean}, \texttt{conditions\_13375}, \texttt{cond19\_13375}, \texttt{cond25\_13375}, \texttt{display25\_first}, \texttt{display25\_third}); Script for the remaining rows (\texttt{scripts/i0088\_numerics.py}) \\ \addlinespace[3pt] (iv) & $\varepsilon(1500) < 1/8349$ & Kernel, script cross-check (\texttt{Cert1575.eps1500}; \texttt{scripts/i0088\_numerics.py} gives $\varepsilon(1500) = 1/8349.3238$, Appendix \ref{app:eps}) \\ \addlinespace[3pt] (v) & Row $6100$ gives $C_1 = 112$, $C_2 = 114$ & Cited (read from Table 1 of \cite{BS-RJ}) \\ \addlinespace[3pt] (vi) & $\mathrm{K3J} > 10^{-4}$ & Kernel (\texttt{theorem3\_positive\_main}, \texttt{exp\_gamma\_gt}, \texttt{exp\_gamma\_lt}, \texttt{cbar\_lt}) \\ \addlinespace[3pt] (vii) & Bracket combination $\ge \mathrm{K3J} - 10^{-5} > 9\cdot 10^{-5}$ & Kernel, script cross-check (\texttt{bracket13375\_holds}, \texttt{li\_factor}; Python total $1.535054\cdot 10^{-4}$ in \texttt{scripts/i0088\_numerics.py}, Appendix \ref{app:errors}) \\ \addlinespace[3pt] (viii) & Error terms and the remainder of (33) are negligible & Kernel, script cross-check (\texttt{error\_13375}, \texttt{mbar\_le} with $\bar m \le 40$, \texttt{bracket13375\_holds}; bound $\bar m < 6.2325$ in Appendix \ref{app:errors}) \\ \addlinespace[3pt] (ix) & $\pi_2(N) > \sqrt N + 1$ implies $N = p + P_2$ & Kernel (\texttt{section55\_step}, \texttt{rep\_of\_pi2'}, Lemma \ref{lem:pos}) \\ \addlinespace[3pt] (x) & Assembly from (i) to (ix) to $\mathrm{ChenThreshold13375}$ & Kernel (\texttt{chenThreshold13375\_of\_}\allowbreak\texttt{deep\_closed}) \\ \addlinespace[3pt] (xi) & $\alpha$-window $[0.0025588, 0.0025649)$, $u$-scan ($13.36525$ near $1627$), and Tables \ref{tab:u_opt}, \ref{tab:table1_sens}, \ref{tab:eps_sens} & Script, not in Lean: the $\alpha$-window by \texttt{scripts/i0088\_numerics.py}; the $u$-scan and the three tables by a separate script, not in the public repository \\ \bottomrule \end{tabular} \end{table} \subsection{Limitations}\label{subsec:limitations} In the Lean formalization, GRH is an explicit hypothesis, and Theorems 5, 6, 7 and Theorem 4 of \cite{BS-RJ} are transcribed as Lean hypotheses (\texttt{Thm5J}, \texttt{Thm6J}, \texttt{Thm7J}, \texttt{LinearSieveT4}), the first three in the $\mathrm{UNfull}$ normalisation of Appendix \ref{app:factor2} (with the printed $(e^{-\gamma}\prod_{p>2}(1-(p-1)^{-2}))^{-1}$ kept in error terms), so a transcription error would not be caught by Lean. No human expert has checked the transcriptions. Commit \texttt{23bb733} lacked the premises $0 < \varepsilon < 1/63$ and $N$ even, which made \texttt{Thm5J} refutable under GRH; commit \texttt{2fdf0dc} added them. Deriving Theorems 5, 6, 7 from GRH through Lemma 3, Lemma 7, and the linear sieve (Section 4 and Sections 5.1--5.3 of \cite{BS-RJ}) is the unused \texttt{sorry} \texttt{theorems567\_of\_inputs}. Full formalization would need Lean proofs of Theorem 4 and of Theorems 5, 6, 7 from GRH. The observation that Corollary 1 needs only $\mathrm{K3J} > 0$ rather than $4\cdot 10^{-3}$ applies in form to the Section 5.4 assembly of Bordignon, Johnston and Starichkova \cite{BJS}, but it does not transfer directly: their unconditional argument has its own inputs, parameters and range conditions in place of the GRH Theorems 5, 6, 7, and here the gain came from positivity together with the binding condition, the second part of (19), (21), (25). We have not computed their assembly nor checked which of their constraints binds, so whether positivity lowers their threshold $\exp(\exp(32.7))$ is open. \appendix \section{Derivation of $\mathrm{K3J}$ from \cite{BS-RJ}}\label{app:K3J} Table \ref{tab:K3J_terms} records the assembly of $\mathrm{K3J}$ term by term, with signs. \begin{table}[htbp] \centering \caption{$\mathrm{K3J}$ terms at $\alpha = 0.00256$, $\varepsilon = 1/8349$, $C_1 = 112$, $C_2 = 114$, $g = e^\gamma$.} \label{tab:K3J_terms} \footnotesize \begin{tabular}{@{}p{0.10\textwidth}p{0.33\textwidth}p{0.25\textwidth}p{0.05\textwidth}p{0.12\textwidth}@{}} \toprule Term & Expression & Source in \cite{BS-RJ} & Sign & Value \\ \midrule $T_5$ main & $8\cdot \frac{2g\log(3-8\alpha)}{4-8\alpha}$ & Theorem 5, p.\ 1228, inner bracket $f(s)$ at $s = 4-8\alpha$ & $+$ & $+7.818059$ \\ \addlinespace[3pt] $T_5$ sieve & $8\cdot \varepsilon C_2\frac{3e^{8\alpha-2}}{4-8\alpha}$ & Theorem 5, p.\ 1228 & $-$ & $-0.011375$ \\ \addlinespace[3pt] $T_6$ main & $\tfrac12\cdot 8(1+5\cdot 10^{-5})\frac{(g/4)(\log 6 + \log\frac{3-8\alpha}{3-18\alpha})}{1/2-\alpha}$ & Theorem 6, pp.\ 1231--1232, display $l_1$; factor $1+5\cdot 10^{-5}$ from Lemma 11, p.\ 1228 & $-$ & $-6.446572$ \\ \addlinespace[3pt] $T_6$ sieve & $\tfrac12\cdot 8(1+5\cdot 10^{-5})\log(8/3)\,\varepsilon C_1$ & Theorem 6, display $l_1$ & $-$ & $-0.052633$ \\ \addlinespace[3pt] $T_7$ main & $\tfrac12\cdot \frac{2g}{1/2-\alpha}\,\bar c$ & Theorem 7, pp.\ 1234--1235, with (29), p.\ 1237, and Lemma 14, p.\ 1237 & $-$ & $-1.300014$ \\ \addlinespace[3pt] $T_7$ sieve & $\tfrac12\cdot 3\varepsilon C_1\,\bar c$ & Theorem 7, pp.\ 1234--1235, with (29), p.\ 1237, and Lemma 14, p.\ 1237 & $-$ & $-0.007306$ \\ \midrule Sum & $\mathrm{K3J}$ & Weights $1, -1/2, -1/2$ from Lemma 9, p.\ 1227 & & $1.58626\cdot 10^{-4}$ \\ \bottomrule \end{tabular} \par\smallskip {\footnotesize Values use $\bar c < 0.363084$; with the exact $\bar c$ the sum is $1.5960\cdot 10^{-4}$, as in Section 2.\par} \end{table} Each piece arises from \cite{BS-RJ} as follows: \begin{itemize} \item By Lemma 9 of \cite{BS-RJ}, p.\ 1227 (Chen's weighted inequality), \begin{equation}\label{eq:app_lem9} \pi_2(N) > S(\mathcal A,\mathbb P,z) - \tfrac12\sum_{z\le q 8\frac{U_N N}{\log^2 N}\Bigl(\Bigl(1-\frac{0.62\log X_2}{X_2^{1/16}}\Bigr) \\ \times\Bigl(\frac{2e^\gamma\log(3-8\alpha_1)}{4-8\alpha_1} - \varepsilon C_2(\varepsilon)\frac{3e^{8\alpha_1-2}}{4-8\alpha_1}\Bigr) - E_5\Bigr), \end{multline} where $E_5$ is a term of order $\log^{-8} N$. The factor $8$ comes from $V(z)$ and $\log z = \tfrac18\log N$ (Lemma 10), together with $|\mathcal A| \ge N/\log N$ (Lemma 11); the inner bracket is $f(s) - \varepsilon C_2 e^2 h(s)$ evaluated at $s = 4 - 8\alpha_1$, where $f(s) = 2e^\gamma\log(s-1)/s$ and $h(s) = 3s^{-1}e^{-s}$ (proof of Theorem 5, p.\ 1229). \item By Theorem 6 of \cite{BS-RJ}, pp.\ 1231 to 1232, \begin{equation}\label{eq:app_thm6} \sum_{z\le q2}(1-(p-1)^{-2})\bigr)^{-1}$, the constant printed in Theorems 5, 6, 7, with $c_G$ of Lemma 13, p.\ 1230. The brackets of \texttt{Thm5J}, \texttt{Thm6J}, \texttt{Thm7J} are \begin{align*} B_5 &= \lambda_-\Bigl(\frac{2g\log(3-8\alpha)}{4-8\alpha} - \varepsilon C_2\frac{3e^{8\alpha-2}}{4-8\alpha}\Bigr) - \frac{T\,c_G(X_2)}{8\lambda_-\log^{A-2}N},\\ B_6 &= l_1 + \frac{l_2}{\log^{A-3}N} + \frac{l_3}{\log^{A-1}N},\\ l_2 &= \frac{c_G(X_2)}{8}\Bigl(0.50007 + \frac{1}{\log X_2}\Bigr)T,\\ l_3 &= \lambda_+\Bigl(\frac{2g}{k} + \varepsilon C_1 e^2 h(k)\Bigr)c_G(X_2), \end{align*} with $l_1$ as in \eqref{eq:app_l1}, and \begin{multline*} B_7 = \Bigl(1+\frac{0.06\log X_2}{X_2^{1/6}}\Bigr)\Bigl(\frac{2g}{\frac12-\alpha}+3\varepsilon C_1\Bigr)(1+\varepsilon_1)\\ \times\frac{\log Y\,\bigl(\mathrm{li}(Y)+\sqrt Y\log Y/(8\pi)\bigr)}{Y}\,\Bigl(\bar c + \frac{36}{\log^2 X_2}\\ + \Bigl(\log\frac83 + \frac{64}{\log^2 X_2}\Bigr)\Bigl(\frac{\log\sqrt{1+\varepsilon_1}}{\log^2 Y - \log^2\sqrt{1+\varepsilon_1}} + \frac{27}{\log^2 X_2}\Bigr)\Bigr)\\ + \frac{T(1+\varepsilon_1)}{\log(1+\varepsilon_1)\log^{A-4}X_2}\Bigl(\frac{0.053\,\bar m(X_2,A,X_2^{1/8})}{(1+\varepsilon_1)^{1/2}} + \frac{0.08\log^{A+1}X_2}{X_2^{1/8}}\Bigr). \end{multline*} \section{The factor $2$ in $U_N$}\label{app:factor2} \textbf{Normalisation used.} The Lean leaves \texttt{Thm5J}, \texttt{Thm6J}, and \texttt{Thm7J} use $\mathrm{UNfull} := 2e^{-\gamma}\prod_{p>2}\bigl(1-(p-1)^{-2}\bigr)\prod_{p>2,\,p\mid N}\frac{p-1}{p-2}$, twice the printed $U_N$ of pp.\ 1214 and 1227 of \cite{BS-RJ}; \texttt{LinearSieveT4}, Theorem 4, does not involve $U_N$. Theorems 5, 6, 7 are applied in this $\mathrm{UNfull}$ normalisation in Lean, and the theorem holds under either reading. Specifically, the threshold proposition \texttt{ChenThreshold13375}, the conclusion of \texttt{chenThreshold13375\_of\_deep\_closed}, does not mention $U_N$ at all (stating that every even $N \ge \exp(\exp 13.375)$ is $p + P_2$), and $\mathrm{K3J}$ is a constant independent of $U_N$. Here $U_N$ enters only as a common positive factor: Theorems 5, 6, 7 give bounds $8B_5$, $8B_6$ and $B_7$ times $U_N N/\log^2 N$, so with the Lemma 9 weights the combination $8B_5 - 4B_6 - \tfrac12 B_7$ multiplies the same $U_N$, and its sign, governed by $\mathrm{K3J}$, does not depend on which normalisation is used, provided Theorems 5, 6, 7 are read in the same one. The last step needs a lower bound on $U_N$ to beat $\sqrt N + 1$ and the error terms: $U_N \ge 0.37$ in the printed normalisation (Appendix \ref{app:errors}) and \texttt{two\_fifths\_le\_UNfull}, $\mathrm{UNfull} \ge 2/5$, in the Lean one; both suffice at $\log\log N \ge 13.375$ with a wide margin. Hence the threshold $13.375$ is the same under either consistent reading, and Lean proves it in the $\mathrm{UNfull}$ reading. Pages 1214 and 1227 of \cite{BS-RJ} print $U_N = e^{-\gamma}\prod_{p>2}\bigl(1 - \frac{1}{(p-1)^2}\bigr)\prod_{p>2,\,p\mid N}\frac{p-1}{p-2}$; that this printed $U_N$ is half the limit of $V(x)\log x$ in Lemma 10 is a lab finding of 27 October 2026, checked on the journal page images. The companion paper \cite{BJS}, arXiv:2207.09452, defines $U_N$ with $2e^{-\gamma}$. We trace the factor $2$ line by line through the five results used in Section 5.4: \begin{itemize} \item \textbf{Lemma 10} (p.\ 1227). Lemma 10 states that $V(x) = \prod_{p2}(1-(p-1)^{-2}))^{-1}$ in the error terms is twice the needed inverse and only weakens them. \item \textbf{Theorem 6} (pp.\ 1231--1232) and \textbf{Theorem 7} (pp.\ 1234--1235). For both upper bounds, the proofs give the bounds with $\mathrm{UNfull}$, and the printed $(e^{-\gamma}\prod_{p>2}(1-(p-1)^{-2}))^{-1}$ in their error terms is twice the needed inverse and only weakens them. \item \textbf{Lemma 9} (p.\ 1227). Through Lemma 9 nothing changes, because Lemma 9 has no $U_N$. \end{itemize} We make no claim that Theorem 3 of \cite{BS-RJ} is wrong: with $\mathrm{UNfull}$ it holds as a coefficient statement. \section{Transcription of the cited inputs}\label{app:transcription} Table \ref{tab:transcription} records the four cited inputs stated in Lean in \texttt{LeanLab/BS2022GRH/ChenThresholdGRH.lean} at public commit \texttt{2fdf0dc}. \begin{table}[p] \centering \caption{Transcription of the four cited inputs in \texttt{ChenThresholdGRH.lean} at commit \texttt{2fdf0dc}.} \label{tab:transcription} \scriptsize \setlength{\tabcolsep}{3.5pt} \begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.11\textwidth}>{\raggedright\arraybackslash}p{0.22\textwidth}>{\raggedright\arraybackslash}p{0.17\textwidth}>{\raggedright\arraybackslash}p{0.21\textwidth}cc@{}} \toprule Lean name & Journal statement, quoted & Premises & Conclusion & Status & \shortstack{Human-\\checked} \\ \midrule \texttt{Thm5J} & Theorem 5, p.\ 1228: ``Assume that GRH holds. Let $\alpha_1, A>0$, $N\ge X_2\ge 4\cdot10^{18}$ \dots\ Then, $S(\mathcal A,\mathbb P,z)>8\frac{U_N N}{\log^2 N}(\dots)$'' & \texttt{GRH}; \texttt{LinearSieveT4} $\varepsilon$ $C_1$ $C_2$; $\mathrm{epsJ}(u) \le \varepsilon$ with $\mathrm{epsJ}$ display (6), p.\ 1221; $0 < \varepsilon < 1/63$; $0 < \alpha < 1/8$; $0 < A$; condition (19); $4\cdot 10^{18} \le X_2 \le N$; $N$ even & $S(\mathcal A,\mathbb P,z) > 8\,\mathrm{UNfull}\frac{N}{\log^2 N}B_5$ & \texttt{MATCH}$^*$ & No \\ \addlinespace[3pt] \texttt{Thm6J} & Theorem 6, pp.\ 1231--1232: ``Assume that GRH holds. Let $\alpha_2, A>0$, $N\ge X_2\ge\exp(\exp(10))$ \dots\ (21) \dots\ then $\sum_{z\le q0$, and $N\ge X_2\ge\exp(\exp(10))$ \dots\ (25) \dots\ Then, we have $S(\mathcal B,\mathbb P,y)\le\frac{U_N N}{\log^2 N}(\dots)$'' & Same as \texttt{Thm5J}, with $0 < \varepsilon_1 < 1$, $0 < \alpha < 1/16$, condition (25), $\exp(\exp 10) \le X_2 \le N$, $N$ even & $S(\mathcal B,\mathbb P,y) \le \mathrm{UNfull}\frac{N}{\log^2 N}B_7$ & \texttt{MATCH}$^*$ & No \\ \addlinespace[3pt] \texttt{Linear\-SieveT4} & Theorem 4, p.\ 1218: ``Suppose that, for some $\epsilon$ such that $0<\epsilon<1/63$, the inequality (2) holds for all $n$ and $1(f(s)-\epsilon C_2(\epsilon)e^2h(s))X-R$''; Table 1, pp.\ 1217--1218 & Linear sieve inequality (2) for sifting weights with $0 < \varepsilon < 1/63$ and the Mertens-type product condition, used at $\varepsilon = 1/8349$, $C_1 = 112$, $C_2 = 114$ & Sifting bounds of Theorem 4 with constants $C_1, C_2$ & \texttt{MATCH}$^*$ & No \\ \bottomrule \end{tabular} \par\smallskip {\footnotesize $^*$ A match up to the deviations listed in Section \ref{subsec:deviations}.\par} \end{table} Quotations are from the journal pages, in this note's notation. No human expert has checked the transcriptions of Theorems 4, 5, 6, 7. Commit \texttt{2fdf0dc} proved that all non-\texttt{GRH}, non-sieve leaf hypotheses hold at the paper's parameters. \subsection{Deviations from the printed statements}\label{subsec:deviations} \begin{itemize} \item \texttt{Thm5J}, \texttt{Thm6J}, \texttt{Thm7J} hold for any $\varepsilon \ge \varepsilon(u)$ and any witness $C_1, C_2$ of \texttt{LinearSieveT4}, in place of $\varepsilon = \varepsilon(u)$ and Table 1. They add $N$ even, and they use $\mathrm{UNfull}$, Appendix \ref{app:factor2}. \item \texttt{LinearSieveT4} has finite support, takes the upper bound for $s \le 3$ and the lower bound for $s \le 4$, and has weak inequalities in place of the printed strict ones. It is read at the one level $z$, Remark \ref{rem:level}. \item Lemma 7 needs $\log z > 2753$ while Theorems 5 to 7 as printed allow smaller $z$; at our $X_2$, $\log z = 80463$. \end{itemize} \section{Omitted terms and error terms}\label{app:errors} Table \ref{tab:errors} summarizes the terms omitted from $\mathrm{K3J}$ and the error terms at $\log X_2 = 643707.69$. \begin{table}[htbp] \centering \caption{Omitted factors and error terms at $\log X_2 = 643707.69$, measured against $U_N N/\log^2 N$.} \label{tab:errors} \footnotesize \begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.36\textwidth}>{\raggedright\arraybackslash}p{0.20\textwidth}>{\raggedright\arraybackslash}p{0.38\textwidth}@{}} \toprule Term & Source in \cite{BS-RJ} & Size against $U_N N/\log^2 N$ \\ \midrule $\mathrm{li}$ factor $\frac{\log y\,(\mathrm{li}(y)+\sqrt{y}\log y/(8\pi))}{y}$ & Theorem 7, Lemma 14 & relative $1/\log y = 4.66\cdot 10^{-6}$, absolute about $6\cdot 10^{-6}$; largest omitted term, included in the total $1.535054\cdot 10^{-4}$ \\ \addlinespace[3pt] $512/(k\log^2 X_2)$ and $64/\log^2 X_2$ in $l_1$; $36/\log^2 X_2$ and $27/\log^2 X_2$ in Theorem 7 & Theorems 6 and 7 & at most $10^{-9}$; included in the total $1.535054\cdot 10^{-4}$ \\ \addlinespace[3pt] $(1 \pm 0.62\log X_2/X_2^{1/16})$, $X_2^{1/8}/(X_2^{1/8}-1)$, $(1+0.06\log X_2/X_2^{1/6})$, $1+\varepsilon_1$ & Theorems 5 to 7 & relative $e^{-40000}$ or $10^{-20}$ \\ \addlinespace[3pt] $E_5$, $l_2/\log^{7} N$, and $l_3/\log^{9} N$ & Theorems 5 and 6 & below $10^{-40}$ \\ \addlinespace[3pt] Remainder of (33) & Section 5.4, p.\ 1241 & $< 1.7\cdot 10^{-15}$ \\ \addlinespace[3pt] $2N^{7/8} + N^{1/3} + \sqrt{N} + 1$ & Lemma 9, Corollary 1 & ratio to $9\cdot 10^{-5}U_N N/\log^2 N$ is $\le 6.01\cdot 10^4\log^2 N\cdot N^{-1/8} < e^{-80425}$ \\ \bottomrule \end{tabular} \end{table} The bounds in the last two rows of Table \ref{tab:errors} are obtained as follows: \begin{itemize} \item From the definition of $U_N$ in Theorem 3 and Lemma 10 of \cite{BS-RJ}, \[ U_N \ge e^{-\gamma}\prod_{p>2}\bigl(1-(p-1)^{-2}\bigr) = 0.5614594836\cdot 0.66016181 \ge 0.370654 > 0.37, \] since the product over $p \mid N$ is at least $1$. \item The journal defines $\bar m$ in (31), pp.\ 1239 to 1240, and bounds $M_\varphi(D^*) \le 1.08$ on p.\ 1240; the bound \[ \bar m(N,10,N^{1/8}) \le 2\cdot 1.08\,\bigl(2/\log 2 + 4e^{-13000}\bigr) < 6.2325 \le 8 \] is ours: every other term of (31) carries $\log^{11} N$ or $\log^{12} N$ times a negative power of $w = N^{1/8}$, below $e^{-13000}$. Consequently, the remainder of (33), p.\ 1241, where the constant $0.053$ is printed in (33), satisfies \begin{multline*} \frac{1+\varepsilon_1}{U_N\log(1+\varepsilon_1)\log^{6}N}\bigl[0.053\,\bar m(1+\varepsilon_1)^{-1/2} + 0.08N^{-1/8}\log^{11}N\bigr] \\ \le 1.0001\cdot\frac{0.053\cdot 8\cdot 10^{20}}{0.37\cdot 7.1\cdot 10^{34}} < 1.7\cdot 10^{-15}. \end{multline*} In Lean, the lemma \texttt{mbar\_le} proves $\bar m \le 40$ at $X_2$ without that estimate, and \texttt{bracket13375\_holds} absorbs the remainder of (33) with that weaker bound. \item From Lemma 9 and Corollary 1, comparing $2N^{7/8} + N^{1/3} + \sqrt N + 1$ against $9\cdot10^{-5}U_N N/\log^2 N$ with $U_N \ge 0.37$ gives a ratio bounded by \[ \frac{2 + N^{-13/24} + N^{-3/8} + N^{-7/8}}{3.33\cdot10^{-5}}\log^2 N\cdot N^{-1/8} \le 6.01\cdot10^4\log^2 N\cdot N^{-1/8}, \] whose logarithm at $\log N = 643707.69$ is $11.0 + 26.75 - 80463.46 < -80425$, and $2\log t - t/8$ decreases for $t > 16$. \end{itemize} \section{The value of $\varepsilon(1500)$}\label{app:eps} By display (6) of \cite{BS-RJ}, p.\ 1221, \begin{equation}\label{eq:eps_def} \varepsilon(u_0) = \exp\Bigl(1.131\cdot10^{-7} + \Bigl(\frac{u_0}{u_0-2}+0.501\Bigr)\sum_{p\ge u_0}p^{-2}\Bigr) - 1. \end{equation} We sum $p^{-2}$ over primes $1500 \le p < 10^9$ with a segmented sieve (in \texttt{scripts/i0088\_numerics.py}), giving $7.96425\cdot10^{-5}$, and bound the tail using $\pi(t) < 1.25506\,t/\log t$ \cite{RS} and partial summation: \begin{align*} \sum_{p \ge X} p^{-2} &= \int_X^\infty t^{-2}\,d\pi(t) \le \int_X^\infty 2\pi(t)\,t^{-3}\,dt \\ &\le 2\cdot 1.25506 \int_X^\infty \frac{dt}{t^2 \log t} \le \frac{2\cdot 1.25506}{X \log X}, \end{align*} the boundary term $-\pi(X)/X^2$ being negative; at $X = 10^9$ this is $1.2113\cdot 10^{-10}$. Hence \[ \varepsilon(1500) = 1.1977018\cdot10^{-4} = 1/8349.3238 < 1/8349, \] with a margin of $4.6\cdot10^{-9}$. The same method gives $\varepsilon(1000) = 1/5235.667 < 1/5235$, matching \cite{BS-RJ}. In Lean, \texttt{Cert1575.eps1500} proves $\varepsilon(1500) < 1/8349$, display (6): the head sum over primes $1501 \le p < 9003001$ of $1/p^2$ is at most $7963599791126110\cdot 10^{-20}$, checked by the kernel with \texttt{decide +kernel} in $11$ windows \texttt{Cert1575W00} to \texttt{Cert1575W10}, no \texttt{native\_decide}, by adding $\lfloor 10^{20}/n^2\rfloor + 1$ over $n \equiv 1, 5 \pmod 6$ coprime to $m!$, with $m = 1499$ or $3000$ below every prime of the window, an upper bound that needs no primality certificate; the tail over $p \ge H = 9003001$ is at most $(C\cdot H - \theta_0)/(16H^2) + C/(16H)$, $C = 89/80$, $\theta_0 = 8191444$, by summation by parts against Chebyshev's $\theta$ with explicit Chebyshev bounds proved in the lab, leaving a margin of about $8.8\cdot 10^{-10}$ in $1 + 1/8349 - e^x$. This kernel proof replaces the Python sum for the logic, and the two agree. The conclusion is not sensitive to this margin: at $\alpha = 0.00256$ and $\log\log X_2 = 13.375$ the total stays positive for every $\varepsilon < 1/8331.07$, and the $6100$ row of Table 1 needs only $\varepsilon < 1/6100$. Table \ref{tab:eps_sens} shows the sensitivity of the total and optimal threshold to $1/\varepsilon$ at $u = 1500$ and row $6100$: the threshold $13.375$ needs $1/\varepsilon(1500)$ above $8331.07$; the computed value is $8349.3238$. \begin{table}[htbp] \centering \caption{Sensitivity to $\varepsilon$ at $u = 1500$, Table 1 row $6100$.} \label{tab:eps_sens} \begin{tabular}{@{}ccc@{}} \toprule $1/\varepsilon$ & Total at $\alpha = 0.00256$, $13.375$ & Best $\log\log X_2$ \\ \midrule $8349$ & $1.5351\cdot 10^{-4}$ & $13.37261$ \\ $8340$ & $7.6548\cdot 10^{-5}$ & $13.37357$ \\ $8331.07$ & $2.4\cdot 10^{-8}$ & $13.37453$ \\ $8300$ & $-2.6751\cdot 10^{-4}$ & $13.37789$ \\ $8000$ & $-2.9576\cdot 10^{-3}$ & $13.41228$ \\ $7000$ & $-1.3590\cdot 10^{-2}$ & $13.56120$ \\ $6100$ & $-2.6139\cdot 10^{-2}$ & $13.77160$ \\ \bottomrule \end{tabular} \end{table} The script numbers in this note use mpmath at $30$ digits with a double precision prime sum and take about $8$ s on a $2$ core PC; they are cross checks only and enter no Lean proof. Table 1 of \cite{BS-RJ} is used as printed, and we claim nothing beyond the source about the rigour of its computation. \section{Build logs and file paths}\label{app:build} Lean files named in Section 3 without a directory lie in \texttt{LeanLab/BS2022GRH/}; other paths are relative to the repository root. Declarations carry the namespace prefix \texttt{LeanLab.BS2022GRH} (sub-namespace \texttt{Journal} for \texttt{JournalMargin.lean}, \texttt{JournalPositive.lean} and \texttt{RangeCheck13375.lean}, \texttt{ChenThresholdGRH} for \texttt{ChenThresholdGRH.lean}, and \texttt{Cert1567}, \texttt{Cert1575} for the certificate files). The build logs are recorded in \texttt{logs/paperB/}: \begin{itemize} \item \texttt{20261020T0802Z-20406-JournalPositive.log}: Build completed successfully, \texttt{EXIT 0}, \texttt{sorry} count $0$; \texttt{theorem3\_positive\_main}, \texttt{conditions\_13375}, and \texttt{params\_ok\_13375} each depend on axioms \texttt{[propext, Classical.choice, Quot.sound]}. \item \texttt{20261020T1303Z-22201.log}, a fresh rebuild by a second run: \texttt{JournalPositive} and \texttt{RangeCheck13375} both \texttt{EXIT 0}, $0$ \texttt{sorry}, and all $11$ theorems depend only on \texttt{[propext, Classical.choice, Quot.sound]}. \item \texttt{20261026T2003Z-2973-U-1561.log} and \texttt{20261027T0004Z-17012-U-1567.log}: each ends with Build completed successfully and \texttt{EXIT 0}. \item \texttt{20261027T0807Z-9485-U-1575.log}: records earlier failed attempts and the final rebuild of \texttt{Cert1575Closed} after a docstring fix, Build completed successfully ($9101$ jobs), \texttt{EXIT 0}, with \texttt{Cert1575.eps1500} and \texttt{chenThreshold13375\_of\_deep\_closed} depending on axioms \texttt{[propext, Classical.choice, Quot.sound]}. \item \texttt{20261028-public-repo-build-after-statement-fix.log}: the build at the public repository after the premise fix, Build completed successfully ($9103$ jobs), \texttt{EXIT 0}. \end{itemize} \section*{Contributions} 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. \section*{Data availability} The Lean source of every theorem named in this paper, with its full import closure, the build logs, and the Python script \texttt{i0088\_numerics.py} with its output, are public at \url{https://github.com/sthubbar/lean-lab-preprints}, commit \texttt{2fdf0dc}; the README states exactly what the Lean proves and what it does not. The build command is \texttt{lake build LeanLab.BS2022GRH.Cert1575Closed Papers.ChenGRH13375}. The conditional threshold theorem, with its four cited inputs as explicit hypotheses, is registered in the Palomar registry of Lean-verified mathematics as \texttt{PALOMAR-2026-10-28-000016}, version 2, \url{https://palomar-registry.org/entry.html?id=PALOMAR-2026-10-28-000016&version=2}. \section*{Acknowledgement} The author thanks M.\ Bordignon and V.\ Starichkova for their paper \cite{BS-RJ}, whose method this note uses unchanged. \begin{thebibliography}{9} \bibitem{BS-RJ} M.~Bordignon and V.~Starichkova, \emph{An explicit version of Chen's theorem assuming the Generalized Riemann Hypothesis}, Ramanujan J.\ \textbf{64} (2024), no.~4, 1213--1242, \url{https://doi.org/10.1007/s11139-024-00866-x}. \bibitem{BS-arXiv} M.~Bordignon and V.~Starichkova, \emph{An explicit version of Chen's theorem assuming the Generalized Riemann Hypothesis}, arXiv:2211.08844, v1, 2022. \bibitem{BJS} M.~Bordignon, D.~R.~Johnston and V.~Starichkova, \emph{An explicit version of Chen's theorem and the linear sieve}, Int.\ J.\ Number Theory \textbf{21} (2025), 2497--2572, \url{https://doi.org/10.1142/S1793042125501192}; arXiv:2207.09452. \bibitem{Chen} J.~R.~Chen, \emph{On the representation of a larger even integer as the sum of a prime and the product of at most two primes}, Sci.\ Sinica \textbf{16} (1973), 157--176. \bibitem{JS} D.~R.~Johnston and V.~V.~Starichkova, \emph{Some explicit results on the sum of a prime and an almost prime}, Acta Math.\ Hungar.\ \textbf{177} (2025), 163--192, \url{https://doi.org/10.1007/s10474-025-01572-w}; arXiv:2208.01229. \bibitem{Lean} subfish-zhou, \emph{goldbach-lean}, \url{https://github.com/subfish-zhou/goldbach-lean}. \bibitem{RS} J.~B.~Rosser and L.~Schoenfeld, \emph{Approximate formulas for some functions of prime numbers}, Illinois J.\ Math.\ \textbf{6} (1962), 64--94. \bibitem{Yamada} T.~Yamada, \emph{Explicit Chen's theorem}, arXiv:1511.03409, 2015. \end{thebibliography} \end{document}