\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. This is conditional on GRH and on 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. It is not a new method. It is a re-choice of the parameters $u$ and $\alpha$ in their argument. \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 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. Within the formalization, 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 proved in Lean. Theorems 5, 6, 7 and Theorem 4 are transcribed from \cite{BS-RJ} as explicit hypotheses and are not formalized. Full details are given in 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 in full detail: \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 the relation $\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, with proof on p.\ 1229), Theorem 6 (p.\ 1231), Theorem 7 (pp.\ 1234 to 1235), and Lemma 9 (p.\ 1227, the weighted sieve inequality of Chen that bounds $\pi_2(N)$ below by sifting functions, minus $2N^{7/8} + N^{1/3}$), and takes the parameters \[ u = 1000, \quad \alpha_1 = \alpha_2 = \alpha_3 = 10^{-3}, \quad A = 10, \quad \varepsilon_1 = 10^{-20}, \] together with $\varepsilon(1000) < 1/5235$, $C_1 = 113$, and $C_2 = 114$. \item The arXiv version \cite{BS-arXiv}, v1, the only arXiv version, had the threshold $\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 itself needs only that the Section 5.4 combination be positive, not that it exceed $4\cdot 10^{-3}$: the inequality $\pi_2'(N) \ge \pi_2(N) - \sqrt{N} - 1$ from the proof of 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$; see Lemma \ref{lem:pos}. Asking only for a positive constant lets $\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}$ exactly as in the Lean formalization (see Appendix \ref{app:K3J} for its derivation from \cite{BS-RJ}), with $g = e^\gamma$, $\varepsilon = 1/8349$, and $\bar{c}$ the constant of 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 the factor $1 + 5\cdot 10^{-5}$ is the journal's Lemma 11 (p.\ 1228) factor on Theorem 6's $l_1$, p.\ 1231. In words, the three pieces of $\mathrm{K3J}$ are $8$ times the main term of Theorem 5, minus one half of $8$ times the main term $l_1$ of Theorem 6, minus one half 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 Lean proves $\mathrm{K3J} > 10^{-4}$. \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)$ is the number of representations of $N$ as a sum of a prime and a square-free semiprime, which must be read as a square-free integer with at most two prime factors, since $\pi_2(N)$ also counts $N = p + q$ with $q$ prime and the inequality removes only $q = 1$ and $q$ with a repeated prime factor; in the journal's words the $1$ counts the representation $N = p + 1$, if it exists, and $\sqrt N$ bounds the number of integers up to $N$ with two equal prime factors. Hence $\pi_2'(N) > 0$. This inequality holds for every even $N$ and does not use the threshold $\exp(\exp(14))$; Corollary 1 of \cite{BS-RJ} applies it with Theorem 3's constant $4\cdot10^{-3}$, and we apply it with the constant $9\cdot10^{-5}$ of Section 2.2, using Appendix \ref{app:errors} to see that $9\cdot10^{-5}U_N N/\log^2 N > \sqrt N + 1$ for $\log\log N \ge 13.375$. \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} (via the inequality $\pi_2'(N) \ge \pi_2(N) - \sqrt{N} - 1$ from the proof of Corollary 1 of \cite{BS-RJ}, Section 5.5, p.\ 1241, which does not involve the threshold) then gives $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 optimum of this framework with $A = 10$ and $\varepsilon_1 = 10^{-20}$ is about $\log\log X_2 = 13.36525$, at $u$ just above the prime $1627$, with $\alpha = 0.0027829$; at the integer $u = 1628$ it is $13.36582$. Thus $13.375$ is within $0.01$ of what Section 5.4 of \cite{BS-RJ} can give at $A = 10$. These optimizations are numerical only and not formalized; the paper keeps $13.375$, which Lean checks. Table \ref{tab:u_opt} shows the optimal threshold across several choices of $u$. \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; $u = 1500$ is a round value near the optimum, and the finer scan above shows $u = 1628$ is marginally better, $13.36582$ against $13.37261$. For fixed $u = 1500$ and $\log\log X_2 = 13.375$, the admissible window for $\alpha$ is as follows: 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; $0.00256$ is a round value inside it. The bisections are in the public script. 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 with Mathlib v4.35.0. All paths below are relative to the \texttt{LeanLab} repository root, with 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). Every proved Lean theorem named in this paper depends only on the standard axioms \texttt{[propext, Classical.choice, Quot.sound]}. The files contain two \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}. Neither is used by \texttt{chenThreshold13375\_of\_deep\_closed}, which takes $\varepsilon(1500) < 1/8349$ from \texttt{Cert1575.eps1500}. The import closure also contains the statement files \texttt{LeanLab/DERZ1997/Statements.lean} and \texttt{LeanLab/AlmostPrimeSums/Statements.lean} with \texttt{sorry}, which none of the named theorems uses, as their axiom lists show. The file \texttt{LeanLab/BS2022GRH/ChenThresholdGRH.lean} states the threshold proposition: {\footnotesize \begin{verbatim} def ChenThreshold13375 : Prop := GRH → ∀ N : ℕ, Even N → exp (exp 13.375) ≤ (N : ℝ) → ChenSqfreeRep N \end{verbatim} } where \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. The cited leaves are stated in the same file as Lean propositions transcribing the journal: \texttt{Thm5J} (Theorem 5, p.\ 1228), \texttt{Thm6J} (Theorem 6, pp.\ 1231 to 1232), and \texttt{Thm7J} (Theorem 7, pp.\ 1234 to 1235), each taking \texttt{GRH}, \texttt{LinearSieveT4}, \texttt{epsJ u ≤ ε}, $0 < \varepsilon < 1/63$ and \texttt{Even n} as explicit arguments, as in the journal; \texttt{LinearSieveT4 ε C₁ C₂} is Theorem 4, the linear sieve, p.\ 1218, with Table 1, in the ranges used; and \texttt{epsJ} is display (6), p.\ 1221. These are hypotheses, not proved. The file \texttt{LeanLab/BS2022GRH/Cert1575Closed.lean} proves the headline theorem: {\footnotesize \begin{verbatim} theorem chenThreshold13375_of_deep_closed (h5 : Thm5J) (h6 : Thm6J) (h7 : Thm7J) (hT4 : LinearSieveT4 (1 / 8349) 112 114) : ChenThreshold13375 \end{verbatim} } Thus the full step from Theorems 5, 6, 7 and Theorem 4 to the threshold is checked in Lean. The file \texttt{LeanLab/BS2022GRH/JournalMargin.lean} defines \texttt{K3J}: {\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} } The file \texttt{LeanLab/BS2022GRH/JournalPositive.lean} contains the three main-term and parameter results: {\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} } In Lean, $e^\gamma$ is bracketed by $1.7810699 < e^\gamma < 1.7810725$, \texttt{LeanLab.Helfgott2013.GammaFine.exp\_gamma\_gt} and \texttt{exp\_gamma\_lt}, and $\bar{c} < 0.363084$ is \texttt{LeanLab.ChenExplicit.BJS.cbar\_lt}. The file \texttt{LeanLab/BS2022GRH/RangeCheck13375.lean} proves eight range lemmas: \texttt{lemma7\_range}, \texttt{display25\_first}, \texttt{display25\_third}, \texttt{remark1\_H}, \texttt{remark1\_H\_vacuity}, \texttt{mono\_step}, \texttt{mono\_range\_13375}, and \texttt{sieve\_ranges\_13375}. Two of these statements are: {\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} } The proved ingredients assembled by \texttt{chenThreshold13375\_of\_deep\_closed} are as follows: \begin{itemize} \item \texttt{lemma9J\_holds : Lemma9J}, the journal's Lemma 9 (Chen's weighted inequality, p.\ 1227), proved for every $N \ge 2^{24}$ from the lab's \texttt{U7153.lemma10}. \item \texttt{section55\_step}, proving $\pi_2(N) - \sqrt{N} - 1 \le \pi_2'(N)$ (Section 5.5, p.\ 1241), and \texttt{rep\_of\_pi2'}, proving that $0 < \pi_2'(N)$ gives the representation. \item \texttt{Journal.theorem3\_positive\_main}, proving $10^{-4} < \mathrm{K3J}$ at the new parameters. \item \texttt{Cert1567.bracket13375\_holds : Bracket13375}, which proves that for every $N \ge \exp(\exp 13.375)$, \[ \mathrm{K3J} - 10^{-5} \le 8\cdot B_5 - \tfrac12\cdot 8\cdot B_6 - \tfrac12\cdot B_7, \] where $B_5, B_6, B_7$ are the journal's exact brackets of Theorems 5, 6, 7 with every correction factor and error term, at $\alpha = 0.00256$, $A = 10$, $\varepsilon = 1/8349$, $C_1 = 112$, $C_2 = 114$, $\varepsilon_1 = 10^{-20}$, and $X_2 = \exp(\exp 13.375)$. The loss is about $6.2\cdot 10^{-6}$, almost all from the $\mathrm{li}$ factor of Theorem 7. This is why the constant $9\cdot 10^{-5}$ appears: $10^{-4} - 10^{-5}$. It replaces the Python total for the logic; the Python total $1.535054\cdot 10^{-4}$ stays as a numerical cross-check. \item \texttt{Cert1567.mbar\_le}, proving $\bar m(X_2, 10, X_2^{1/8}) \le 40$ at $\log\log X_2 = 13.375$, a weaker bound than the paper's hand bound $6.2325$ but enough inside \texttt{bracket13375\_holds}; and \texttt{Cert1567.li\_factor}, proving that at $\log Y = L/3$ with $L \ge 643700$, $\log Y\cdot(\mathrm{li}\,Y + Y^{1/2}\log Y/(8\pi))/Y \le 1 + 4.6702\cdot 10^{-6}$. \item \texttt{error\_13375}, proving that for $\log N \ge e^{13.375}$, $2N^{7/8} + N^{1/3} + \sqrt{N} + 1 < 3.6\cdot 10^{-5}\cdot N/\log^2 N$; and \texttt{two\_fifths\_le\_UNfull}, proving $U_N \ge 2/5$ in the Lean normalisation below. \item \texttt{X2\_ranges}, \texttt{cond19\_13375}, and \texttt{cond25\_13375}, proving the conditions (19), (21), and (25) at the new parameters. \item \texttt{Cert1575.eps1500}, proving $\varepsilon(1500) < 1/8349$, display (6) (see Appendix \ref{app:eps}). \end{itemize} The Lean leaves use $U_N := 2e^{-\gamma} \prod_{p>2}(1 - (p-1)^{-2}) \prod_{p>2,\, p\mid N}(p-1)/(p-2)$, the normalisation in which the sieve product $V(z) = \prod_{p 10^{-4}$ & \eqref{eq:K3J} and Section 2.2 \\ \addlinespace[3pt] \texttt{bracket13375\_holds} & $8B_5 - 4B_6 - \tfrac12 B_7 \ge \mathrm{K3J} - 10^{-5}$ for $N \ge X_2$ & Appendices \ref{app:K3J} and \ref{app:errors}, with Lemma 9 and Theorems 5, 6, 7 gives $\pi_2(N) > 9\cdot 10^{-5} U_N N/\log^2 N - 2N^{7/8} - N^{1/3}$ \\ \addlinespace[3pt] \texttt{lemma9J\_holds} & Lemma 9 of \cite{BS-RJ} & (A.1) \\ \addlinespace[3pt] \texttt{error\_13375} & Lemma 9 and Section 5.5 error terms $< 3.6\cdot 10^{-5} N/\log^2 N$ & Appendix \ref{app:errors} \\ \addlinespace[3pt] \texttt{section55\_step} and \texttt{rep\_of\_pi2'} & $\pi_2' \ge \pi_2 - \sqrt{N} - 1$ and $\pi_2' > 0$ gives $N = p + P_2$ & Lemma \ref{lem:pos} \\ \addlinespace[3pt] \texttt{eps1500} & $\varepsilon(1500) < 1/8349$ & Appendix \ref{app:eps} \\ \addlinespace[3pt] \texttt{mbar\_le} & $\bar m \le 40$ & Appendix \ref{app:errors} \\ \addlinespace[3pt] \texttt{conditions\_13375}, \texttt{cond19\_13375}, \texttt{cond25\_13375}, \texttt{display25\_first}, \texttt{display25\_third} & parameter ranges & Table \ref{tab:ranges} \\ \addlinespace[3pt] \texttt{chenThreshold13375\_of\_}\allowbreak\texttt{deep\_closed} & the main statement from Theorems 5, 6, 7 and Theorem 4 & Theorem \ref{thm:main} \\ \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, stated in Lean as hypotheses, not proved \\ \addlinespace[3pt] (ii$'$) & Lemma 9 of \cite{BS-RJ} & Lean, \texttt{lemma9J\_holds} \\ \addlinespace[3pt] (iii) & Their hypotheses hold at the new parameters, Table \ref{tab:ranges} & Lean, \texttt{RangeCheck13375.lean}, \texttt{conditions\_13375}, \texttt{cond19\_13375}, \texttt{cond25\_13375}, \texttt{display25\_first}, \texttt{display25\_third}; the remaining rows by hand \\ \addlinespace[3pt] (iv) & $\varepsilon(1500) < 1/8349$ & Lean, \texttt{Cert1575.eps1500}, and Python cross-check (\texttt{scripts/i0088\_numerics.py}; Appendix \ref{app:eps}) \\ \addlinespace[3pt] (v) & Row $6100$ gives $C_1 = 112$, $C_2 = 114$ & read from Table 1 of \cite{BS-RJ} \\ \addlinespace[3pt] (vi) & $\mathrm{K3J} > 10^{-4}$ & Lean, \texttt{theorem3\_positive\_main} \\ \addlinespace[3pt] (vii) & Bracket combination $\ge \mathrm{K3J} - 10^{-5} > 9\cdot 10^{-5}$ & Lean, \texttt{bracket13375\_holds}; Python total $1.535054\cdot 10^{-4}$ as cross-check (Appendix \ref{app:errors}) \\ \addlinespace[3pt] (viii) & Error terms and the remainder of (33) are negligible & Lean, \texttt{error\_13375} and \texttt{bracket13375\_holds}; hand bound in Appendix \ref{app:errors} as cross-check \\ \addlinespace[3pt] (ix) & $\pi_2(N) > \sqrt N + 1$ implies $N = p + P_2$ & Lean, \texttt{section55\_step}, \texttt{rep\_of\_pi2'} (Lemma \ref{lem:pos}) \\ \addlinespace[3pt] (x) & Assembly from (i) to (ix) to $\mathrm{ChenThreshold13375}$ & Lean, \texttt{chenThreshold13375\_of\_}\allowbreak\texttt{deep\_closed} \\ \bottomrule \end{tabular} \end{table} \subsection{Limitations}\label{subsec:limitations} In the Lean formalization, GRH is an explicit hypothesis. Theorems 5, 6, 7 and Theorem 4 of \cite{BS-RJ} are transcribed by hand from the journal and stated as Lean hypotheses (\texttt{Thm5J}, \texttt{Thm6J}, \texttt{Thm7J}, and \texttt{LinearSieveT4}), so a transcription error there would not be caught by Lean. This risk is real: in the version cited by v1.3 of this note, commit \texttt{23bb733}, the three statements omitted the premises $0 < \varepsilon < 1/63$ and $N$ even, and with $\varepsilon = 1$, or with $N$ odd, \texttt{Thm5J} could be refuted under GRH, which made the conditional theorem vacuous. Independent audit passes found both gaps on 28 October 2026; the premises were added at commit \texttt{2fdf0dc}, the headline still builds with only the standard axioms, and a third audit found no further refutation. They are stated with the Lean normalisation of $U_N$ of Section 3, twice the printed one, while the printed factor $(e^{-\gamma}\prod_{p>2}(1-(p-1)^{-2}))^{-1}$ in their negligible error terms is kept as printed; so they are transcriptions in that normalisation, not verbatim copies of the printed statements. Deriving Theorems 5, 6, 7 from GRH through the journal's Lemma 3, Lemma 7, and the linear sieve (Section 4 and Sections 5.1 to 5.3 of \cite{BS-RJ}, the deep part of the argument) is the open step \texttt{theorems567\_of\_inputs}, which is a named \texttt{sorry} not used by \texttt{chenThreshold13375\_of\_deep\_closed}. Formalizing that derivation together with the linear sieve with explicit constants would be needed for a fully formal proof. The observation that Corollary 1 needs only $\mathrm{K3J} > 0$ rather than the printed $4\cdot 10^{-3}$ applies to the Section 5.4 style assembly of Bordignon, Johnston and Starichkova \cite{BJS} as well, but the lab has not computed what it gives there. \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 - \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}\bigl(1 - \frac{1}{(p-1)^2}\bigr)\prod_{p>2,\,p\mid N}\frac{p-1}{p-2}$, twice the printed $U_N$ (numerically, for primes below $10^8$, $V(x)\log x$ divided by the printed $U_N$ is $1.99756$, $1.99992$, and $1.999992$ at $x = 10^4, 10^6, 10^8$ for $N = 2^{20}$, $9699690$, and $10^{12}+2$ alike, and the Lean file \texttt{Verify1565.lean} proves the algebraic identities \texttt{factor\_identity}, \texttt{prod\_identity}, and \texttt{drop\_two}). \item \textbf{Theorem 5} (p.\ 1228). Through Theorem 5 the factor $8$ comes from $V(z)$ with $\log z = \tfrac18\log N$, and the corrected $V(z)$ carries the factor $2$ into the lower bound with $\mathrm{UNfull}$. The printed $(e^{-\gamma}\prod_{p>2}(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). Through Theorem 6, which is an upper bound, the printed statement with the smaller $U_N$ is not what its proof gives; the proof gives the upper bound with $\mathrm{UNfull}$, and the printed $(e^{-\gamma}\prod_{p>2}(1-(p-1)^{-2}))^{-1}$ in the error terms is twice the needed inverse and only weakens them. \item \textbf{Theorem 7} (pp.\ 1234--1235). Through Theorem 7, which is also an upper bound, the printed statement with the smaller $U_N$ is not what its proof gives; the proof gives the upper bound with $\mathrm{UNfull}$. The printed $(e^{-\gamma}\prod_{p>2}(1-(p-1)^{-2}))^{-1}$ in its error terms is likewise 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} Accordingly, the Lean leaves \texttt{Thm5J}, \texttt{Thm6J}, and \texttt{Thm7J} use $\mathrm{UNfull}$, equal to $2$ times the printed $U_N$, and we make no claim that the main theorem of \cite{BS-RJ} is wrong: with the true $U_N$ their Theorem 3 holds as a coefficient statement. Every Section 5.4 bound is a coefficient times $U_N N/\log^2 N$, so $\mathrm{K3J}$ and the threshold $13.375$ do not depend on the normalisation. \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 \begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.16\textwidth}>{\raggedright\arraybackslash}p{0.14\textwidth}>{\raggedright\arraybackslash}p{0.29\textwidth}>{\raggedright\arraybackslash}p{0.22\textwidth}p{0.07\textwidth}@{}} \toprule Lean name & Journal result & Premises & Conclusion & Status \\ \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} \\ \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 to 7 as printed allow smaller $z$, which holds 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*{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}