\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. \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. The first explicit threshold for Chen's theorem was obtained by Yamada \cite{Yamada}. Unconditionally, the current record is due to Bordignon, Johnston and Starichkova \cite{BJS}, who established 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}. \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. 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} 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.} The unconditional record is $\exp(\exp(32.7))$ by Bordignon, Johnston and Starichkova \cite{BJS}; GRH thresholds indicate how far the explicit sieve method can go when zero-free regions are not the bottleneck; within this framework the optimum is about $13.365$ at $u$ near $1628$ (Section 2.4), so $13.375$ is within $0.01$ of the method's limit and further gains need new ideas in Theorems 5 to 7 or the sieve constants. \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, they prove \[ \pi_2(N) > 4\cdot 10^{-3} U_N \frac{N}{\log^2 N} \] 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$, which is the row $\varepsilon^{-1} = 6100$ of Table 1 of \cite{BS-RJ}, pp.\ 1217 to 1218. This is valid since inequality (2) with $\varepsilon(1500)$ implies it with the larger $1/6100$; the journal itself pairs $\varepsilon(1000) < 1/5235$ with 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; the three pieces of $\mathrm{K3J}$ are $8$ times the main term of Theorem 5, minus $\tfrac12\cdot 8$ times the main term $l_1$ of Theorem 6, minus $\tfrac12$ of the main term of Theorem 7. \subsection{Numerical evaluation at $\log\log X_2 = 13.375$ and $\alpha = 0.00256$} At $\log\log X_2 = 13.375$ and $\alpha = 0.00256$, the relevant numerical values are as follows: \begin{itemize} \item $\log X_2 = e^{13.375} = 643707.69$; Lean proves $e^{13.375} \ge 643700$. \item The binding condition, which is the second part of displays (19), (21), and (25) of \cite{BS-RJ}, is \[ \alpha \log X_2 - 11 \log\log X_2 = 1500.767 \ge 1500 = u. \] At this $X_2$ the condition needs $\alpha \ge 0.0025588$, leaving a slack of $0.00047$ in $\log\log X_2$. \item At $\alpha = 0.00256$, $\varepsilon = 1/8349$, $C_1 = 112$, and $C_2 = 114$, the main-term constant $\mathrm{K3J}$ defined in \eqref{eq:K3J} has the numerical value $\mathrm{K3J} = 1.5960\cdot 10^{-4}$, and the lower bound $\mathrm{K3J} > 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, which come to $6.10\cdot 10^{-6}$, the total with the omitted terms is $1.535054\cdot 10^{-4}$. \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 > \sqrt N + 1$ for $\log\log N \ge 13.375$ by Appendix \ref{app:errors}. \end{proof} \begin{itemize} \item Hence, on GRH and the cited results, \[ \pi_2(N) > 9\cdot 10^{-5} U_N \frac{N}{\log^2 N} > 0 \] for every even $N \ge \exp(\exp(13.375))$, and Lemma \ref{lem:pos} yields $N = p + P_2$. \end{itemize} \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 all parameter conditions required by the lemmas and theorems in \cite{BS-RJ} at $\log\log X_2 = 13.375$ ($\alpha = 0.00256$) and $\log\log X_2 = 13.45$ ($\alpha = 0.0024$). Every 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, 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 $2150$ or more, which gives at least $13.466$. Thus the $6100$ row is the best admissible one and no other row 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 All Lean code was written by AI and 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.2\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 (by hand and \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}; hand 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 (\texttt{scripts/i0088\_numerics.py}, not in Lean) \\ \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 hand-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; as detailed in Appendix \ref{app:transcription}, two AI audits on 28 October 2026 caught missing premises $0 < \varepsilon < 1/63$ and $N$ even in commit \texttt{23bb733} (v1.3) that made \texttt{Thm5J} refutable under GRH, fixed at commit \texttt{2fdf0dc}. 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}. The observation that Corollary 1 needs only $\mathrm{K3J} > 0$ rather than $4\cdot 10^{-3}$ also applies to the Section 5.4 assembly of Bordignon, Johnston and Starichkova \cite{BJS}, which we have not computed. \appendix \section{Derivation of $\mathrm{K3J}$ from \cite{BS-RJ}}\label{app:K3J} All three sifting bounds in Section 5 of \cite{BS-RJ} carry the factor $U_N N/\log^2 N$, and $\mathrm{K3J}$ is the combined main-term coefficient. Before detailing the individual sources, Table \ref{tab:K3J_terms} records the line-by-line assembly with explicit 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}\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}[htbp] \centering \caption{Transcription of the four cited inputs in \texttt{ChenThresholdGRH.lean} at commit \texttt{2fdf0dc}.} \label{tab:transcription} \footnotesize \setlength{\tabcolsep}{3.5pt} \begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.12\textwidth}>{\raggedright\arraybackslash}p{0.12\textwidth}>{\raggedright\arraybackslash}p{0.25\textwidth}>{\raggedright\arraybackslash}p{0.22\textwidth}cc@{}} \toprule Lean name & Journal result & Premises & Conclusion & Status & \shortstack{Human-\\checked} \\ \midrule \texttt{Thm5J} & Theorem 5, p.\ 1228 & \texttt{GRH}; \texttt{LinearSieveT4} $\varepsilon$ $C_1$ $C_2$; $0 \le C_1$, $0 \le 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 & Same as \texttt{Thm5J}, with $0 < \alpha < 1/24$, condition (21) as encoded, $\exp(\exp 10) \le X_2 \le N$, $N$ even & $\sum_{\substack{z\le q 2753$ while Theorems 5--7 as printed allow smaller $z$ (satisfied at our $X_2$ since $\log z = 80463$); and the $U_N$ factor $2$ of Appendix \ref{app:factor2}. \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 the hand 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} \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]}. \end{itemize} \section*{Use of AI} AI, namely Claude by Anthropic, wrote all Lean code and drafted the text; the Lean of Section 3 was written by Claude in the author's lab and checked only by the Lean kernel; AI tools were used for the literature search; the statements, the numbers and the references were checked by independent AI checker passes against the Lean source and the published pages of \cite{BS-RJ}; the author is responsible for the content. \textbf{Checker protocol.} As done for every version, each draft is checked by a fresh AI session that did not write it, which compares every theorem name and statement against the Lean source, every number against the build logs and the public Python script \texttt{i0088\_numerics.py}, and every citation against the journal pages, and reports findings that go into the next round; the Lean itself is checked only by the Lean kernel; the author reads every version and is responsible. No human expert has verified the transcriptions of Theorems 4 to 7. \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 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}, \url{https://palomar-registry.org/entry.html?id=PALOMAR-2026-10-28-000016&version=1}. \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}