\documentclass{amsart}
\usepackage[margin=1in]{geometry}

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{booktabs}
\usepackage[hyphens]{url}
\usepackage{verbatim}

\ifdefined\Umathchar
  \def\DeclareUnicodeCharacter#1#2{%
    \catcode"#1=\active
    \begingroup\lccode`\~="#1\lowercase{\endgroup\def~}{#2}%
  }
\fi

\DeclareUnicodeCharacter{00AC}{\ensuremath{\neg}}
\DeclareUnicodeCharacter{00D7}{\ensuremath{\times}}
\DeclareUnicodeCharacter{02E2}{\ensuremath{^{\mathrm{s}}}}
\DeclareUnicodeCharacter{03B5}{\ensuremath{\varepsilon}}
\DeclareUnicodeCharacter{2080}{\ensuremath{_0}}
\DeclareUnicodeCharacter{2081}{\ensuremath{_1}}
\DeclareUnicodeCharacter{2082}{\ensuremath{_2}}
\DeclareUnicodeCharacter{2083}{\ensuremath{_3}}
\DeclareUnicodeCharacter{208A}{\ensuremath{_+}}
\DeclareUnicodeCharacter{2113}{\ensuremath{\ell}}
\DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}}
\DeclareUnicodeCharacter{211D}{\ensuremath{\mathbb{R}}}
\DeclareUnicodeCharacter{2124}{\ensuremath{\mathbb{Z}}}
\DeclareUnicodeCharacter{2192}{\ensuremath{\to}}
\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}}
\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}}
\DeclareUnicodeCharacter{2208}{\ensuremath{\in}}
\DeclareUnicodeCharacter{220F}{\ensuremath{\prod}}
\DeclareUnicodeCharacter{2211}{\ensuremath{\sum}}
\DeclareUnicodeCharacter{2212}{\ensuremath{-}}
\DeclareUnicodeCharacter{2223}{\ensuremath{\mid}}
\DeclareUnicodeCharacter{2224}{\ensuremath{\nmid}}
\DeclareUnicodeCharacter{2227}{\ensuremath{\wedge}}
\DeclareUnicodeCharacter{2228}{\ensuremath{\vee}}
\DeclareUnicodeCharacter{224D}{\ensuremath{\asymp}}
\DeclareUnicodeCharacter{2260}{\ensuremath{\neq}}
\DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}}
\DeclareUnicodeCharacter{2264}{\ensuremath{\le}}
\DeclareUnicodeCharacter{2265}{\ensuremath{\ge}}
\DeclareUnicodeCharacter{226A}{\ensuremath{\ll}}
\DeclareUnicodeCharacter{230A}{\ensuremath{\lfloor}}
\DeclareUnicodeCharacter{230B}{\ensuremath{\rfloor}}
\DeclareUnicodeCharacter{2A7D}{\ensuremath{\leqslant}}
\DeclareUnicodeCharacter{2A7E}{\ensuremath{\geqslant}}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{statement}[theorem]{Statement}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\title[The coprimality convention in a theorem of Halupczok]{Making the coprimality convention explicit in a mean value theorem of Halupczok for the ternary Goldbach problem}
\author{Steve Hubbard}
\address{Independent Researcher}

\begin{document}
\sloppy

\begin{abstract}
Theorem 1.2 of Halupczok (2013) is a Bombieri-Vinogradov type mean value theorem for the ternary Goldbach problem with one prime in an arithmetic progression and two primes in short intervals. Her proof works with residue classes $a \bmod q$ coprime to the modulus, as stated on p.~344 of her paper, and this convention needs to be written explicitly into the statement because the printed product and the prime sum differ at $a = q = 3$, where the prime sum is $0$ for $X_1 > 3$ while the printed product is at least $9/16$ for odd $n$. We give two closely related explicit formulations, Formulation~A and Formulation~B, show that Formulation~A implies Formulation~B, and prove both assuming two cited inputs, Hypothesis~H1 and Hypothesis~H2, or alternatively Theorems~2.1 and~2.3 of her paper, which follow from these two inputs. Here Hypothesis~H1 is a uniform reading of a printed remark of Perelli, Pintz and Salerno, supported by a reading of the proof, and Hypothesis~H2 is assembled from displays of Perelli and Pintz and is not a numbered statement. The supplement of Theorem~1.2 with a maximum over $a$ is not covered. The later results of Halupczok's paper use only coprime residue classes and are unaffected. The main results of this note have been checked by computer.
\end{abstract}

\maketitle

\section{Introduction}

In \cite{H} (preprint \cite{H-arXiv}), Halupczok proves a Bombieri-Vinogradov type mean value theorem for the ternary Goldbach problem, extending classical mean value results to the ternary setting in which one prime is restricted to an arithmetic progression $p_1 \equiv a \pmod q$ and two primes lie in short intervals. We warmly credit and thank Halupczok for this work: her paper supplies the structure of the argument and quotes the two deep inputs, and our proof follows her proof of Theorem~1.2, with the changes listed in Section~\ref{sec:differences}.

\begin{theorem}[Main theorem of this note]\label{thm:main}
Assume Hypothesis~H1 and Hypothesis~H2, the two cited inputs described in Section~3.1. Then Formulation~A of Section~3, the coprime form of JTNB Theorem~1.2, holds, and Formulation~B of Section~3, the form over all $q \le Q$ with main term $0$ when $(a, q) > 1$, holds. Alternatively, Formulation~A and Formulation~B follow from the paper's own quoted Theorems 2.1 and 2.3.
\end{theorem}

The numbering of the preprint \cite{H-arXiv} and the published paper \cite{H} correspond as follows:
\begin{center}
\footnotesize
\begin{tabular}{@{}lll@{}}
\toprule
arXiv:1212.4406 v1 \cite{H-arXiv} & JTNB 2013 \cite{H} & JTNB page \\
\midrule
Theorem 2 & Theorem 1.2 & pp.~333 to 334 \\
Theorem 2, last line & Theorem 1.2, last line & p.~334 \\
Theorem 3 & Theorem 2.1 & p.~338 \\
Theorem 5 & Theorem 2.3 & p.~339 \\
Corollary 4 & Corollary 1.4 & p.~334 \\
\bottomrule
\end{tabular}
\end{center}

In the proof of Theorem~1.2, Halupczok works with residue classes coprime to the modulus, stating on \cite[p.~344]{H} that ``we used $(q, a) = 1$ in the last step, what we can assume w.l.o.g., else (4.2) holds true clearly''. Our change is to carry that convention into the theorem statement: for $(a, q) > 1$ and $1 \le q \le X_1$ the inner ternary prime sum vanishes while the printed Euler product $T(n, q, a)$ need not vanish, as for $a = q = 3$, so the statement needs the convention to be true as written. Section~3 writes the convention in two ways: by restricting the outer sum to moduli coprime to $a$, Formulation~A, and by setting the main term to $0$ for the other moduli, Formulation~B, just as display (1.1) of \cite[p.~335]{H} does for the binary singular series $S(r, q, a)$. All later results of \cite{H} apply Theorem~1.2 only to residue classes coprime to the modulus and are unaffected.

We state plainly that the binary Goldbach conjecture remains open and that this note makes no progress on it. The ternary Goldbach problem was settled by Helfgott in 2013 \cite{Helfgott}, which this note does not use.

\section{The printed statement and the coprimality convention}

We first recall JTNB Theorem 1.2 as printed in \cite[pp.~333 to 334]{H}. Suppose that
\[
  X_1 \ge Y_1 \gg X_1^{3/5 + \varepsilon_1}, \qquad
  X_2 \ge Y_2 \gg X_2^{7/12 + \varepsilon_2},
\]
\[
  Y_2^{1/3 + \varepsilon} \ll Y_1 \ll Y_2 \asymp n - X_1 - Y_1 - X_2 - Y_2 \ge 0,
\]
with $n$ odd, and
\[
  Q \ll Y_1 X_1^{-1/2} L^{-B}, \qquad
  Q \ll Y_1^{3/2} (n - X_1)^{-1/2},
\]
where $L = \log Y_2$ and $B = B(A)$. The printed conclusion asserts that for any fixed integer $a$ with $a \le n - X_1 - Y_1$,
\[
  \sum_{q \le Q} \left| \sum_{\substack{p_1 + p_2 + p_3 = n \\ p_i \in [X_i, X_i + Y_i],\ i = 1, 2 \\ p_1 \equiv a \pmod q}} \log p_1 \log p_2 \log p_3 - T(n, q, a) Y_1 Y_2 \right| \ll Y_1 Y_2 L^{-A},
\]
where $[X, X + Y]$ denotes the set of integers $m$ satisfying $X < m \le X + Y$. The theorem ends with a supplement: if $Q \ll Y_1^{1/2}$ is assumed instead of $Q \ll Y_1^{3/2} (n - X_1)^{-1/2}$, then $\max^*_{a(q)}$ can be inserted after the sum over $q$; this supplement is not covered here. In the printed statement, the singular series $T(n, q, a)$ is $1/\varphi(q)$ times the product over all primes $p$ of a local factor equal to $1 - 1/(p - 1)^2$ if $p \mid n$ and $p \nmid q$, or if $p \nmid n - a$ and $p \mid q$; equal to $1 + 1/(p - 1)^3$ if $p \nmid n$ and $p \nmid q$; and equal to $p/(p - 1)$ otherwise. Written out as a displayed formula, this is
\begin{equation}\label{eq:T-def}
  T(n, q, a) = \frac{1}{\varphi(q)} \prod_{p}
  \begin{cases}
    1 - \dfrac{1}{(p - 1)^2} & \text{if } (p \mid n \text{ and } p \nmid q) \text{ or } (p \nmid n - a \text{ and } p \mid q), \\[8pt]
    1 + \dfrac{1}{(p - 1)^3} & \text{if } p \nmid n \text{ and } p \nmid q, \\[8pt]
    \dfrac{p}{p - 1} & \text{otherwise.}
  \end{cases}
\end{equation}

Whereas the binary singular series $S(r, q, a)$ of display (1.1) of \cite[p.~335]{H} is explicitly set to $0$ when $(a, q) > 1$, the printed definition \eqref{eq:T-def} of $T(n, q, a)$ gives the Euler product directly, and the coprimality convention is stated in the proof on \cite[p.~344]{H}:
\begin{quote}
``we used $(q, a) = 1$ in the last step, what we can assume w.l.o.g., else (4.2) holds true clearly''.
\end{quote}

\begin{remark}[Why the convention is stated]\label{rem:convention}
An explicit statement must specify what happens when $(a, q) > 1$. For example, with $a = q = 3$ and $X_1 > 3$, the prime sum is empty and equal to $0$ (as holds whenever $1 \le q \le X_1$ and $(a, q) \neq 1$, since any prime $p_1 \equiv a \pmod q$ divides $(a, q) \le q \le X_1$), while the printed product $T(n, 3, 3)$ in \eqref{eq:T-def} is positive for every odd $n$, as shown below. The convention $(q, a) = 1$, as used in the proof on \cite[p.~344]{H}, is what makes the two sides match.

Let $n$ be odd and take $q = a = 3$ in \eqref{eq:T-def}, so $\varphi(3) = 2$. At $p = 2$ we have $2 \nmid n$ and $2 \nmid 3$, so the local factor is $1 + 1/(2-1)^3 = 2$. At $p = 3$ we have $3 \mid q$: if $3 \nmid n$ then $3 \nmid n - 3$ and the factor is $1 - 1/4 = 3/4$; if $3 \mid n$ then $3 \mid n - 3$, neither of the first two cases applies, and the factor is $3/2$. At each prime $p \ge 5$ we have $p \nmid q$, so the factor is $1 - (p-1)^{-2}$ if $p \mid n$ and $1 + (p-1)^{-3}$ otherwise; in both cases it is at least $1 - (p-1)^{-2} > 0$. Since $\sum_p (p-1)^{-2} < \infty$, the product converges absolutely, and
\[
  T(n, 3, 3) = \tfrac{1}{2} \cdot 2 \cdot f_3 \prod_{p \ge 5} f_p \ \ge\ \tfrac{3}{4} \prod_{p \ge 5} \Bigl(1 - \frac{1}{(p-1)^2}\Bigr) \ \ge\ \tfrac{3}{4} \prod_{m \ge 4} \Bigl(1 - \frac{1}{m^2}\Bigr) = \tfrac{3}{4} \cdot \tfrac{3}{4} = \tfrac{9}{16},
\]
where $f_p$ is the local factor at $p$ and $f_3 \ge 3/4$. The second inequality holds because the numbers $p - 1$ with $p \ge 5$ prime are distinct integers $m \ge 4$ and every factor $1 - m^{-2}$ lies in $(0, 1)$. The last product follows from the telescoping identity $\prod_{m=2}^{M} (1 - m^{-2}) = (M+1)/(2M)$, which gives $\prod_{m \ge 2} (1 - m^{-2}) = 1/2$ and hence $\prod_{m \ge 4} (1 - m^{-2}) = \frac{1/2}{(3/4)(8/9)} = 3/4$. So $T(n, 3, 3) \ge 9/16 > 0$ for every odd $n$.
\end{remark}

\section{The explicit formulations and proof sketch}

There are two natural and closely related ways to write the coprimality convention into the statement of JTNB Theorem 1.2. We state the two explicit formulations below; Theorem~\ref{thm:main} proves both, assuming the two cited inputs described in Section 3.1.

\begin{statement}[Formulation A, the coprime reading]\label{thm:formulationA}
Assume the hypotheses of JTNB Theorem 1.2. Then for any fixed integer $a$ with $a \le n - X_1 - Y_1$,
\[
  \sum_{\substack{q \le Q \\ (a, q) = 1}} \left| \sum_{\substack{p_1 + p_2 + p_3 = n \\ p_i \in [X_i, X_i + Y_i],\ i = 1, 2 \\ p_1 \equiv a \pmod q}} \log p_1 \log p_2 \log p_3 - T(n, q, a) Y_1 Y_2 \right| \ll Y_1 Y_2 L^{-A}.
\]
\end{statement}

\begin{statement}[Formulation B, the zeroed reading]\label{thm:formulationB}
Assume the hypotheses of JTNB Theorem 1.2 together with the additional hypothesis $Q \le X_1$. Define
\[
  T_0(n, q, a) =
  \begin{cases}
    T(n, q, a) & \text{if } (a, q) = 1, \\
    0 & \text{otherwise,}
  \end{cases}
\]
analogously to $S(r, q, a)$ in display (1.1) of \cite[p.~335]{H}. Then for any fixed integer $a$ with $a \le n - X_1 - Y_1$,
\[
  \sum_{q \le Q} \left| \sum_{\substack{p_1 + p_2 + p_3 = n \\ p_i \in [X_i, X_i + Y_i],\ i = 1, 2 \\ p_1 \equiv a \pmod q}} \log p_1 \log p_2 \log p_3 - T_0(n, q, a) Y_1 Y_2 \right| \ll Y_1 Y_2 L^{-A}.
\]
\end{statement}

Unconditionally, Formulation~A implies Formulation~B: when $Q \le X_1$, every modulus $1 \le q \le Q$ with $(a, q) \neq 1$ satisfies $q \le X_1$, so both the ternary prime sum and $T_0(n, q, a)$ are equal to $0$. The hypothesis $Q \le X_1$ has no other role. It is not a true addition to the hypotheses of JTNB Theorem~1.2: when the threshold $Y_0$ for $Y_1, Y_2$ is chosen after the implied constants $c$, taking $Y_0 \ge \max(e, c_6^2)$ gives $X_1 \ge Y_1 \ge Y_0$, $\log Y_2 \ge 1$ and $Q \le c_6 Y_1 X_1^{-1/2} \le c_6 X_1^{1/2} \le X_1$, where $c_6$ is the implied constant in $Q \ll Y_1 X_1^{-1/2} L^{-B}$. So a form of Formulation~B without $Q \le X_1$ follows at once, at the cost of a larger $Y_0$. Statement~\ref{thm:formulationB} keeps $Q \le X_1$ as an explicit hypothesis so that the implication from Formulation~A to Formulation~B holds directly.

\subsection{The main theorem and the two cited inputs}

To state the main result, we first describe the two cited analytic inputs on which Halupczok's proof rests. Because \cite{H} itself quotes two auxiliary theorems from the literature (JTNB Theorems 2.1 and 2.3), our argument replaces each quoted theorem by a deduction from its printed source:

\begin{enumerate}
\item \textbf{First cited input (Hypothesis H1).} JTNB Theorem 2.1 (arXiv Theorem 3, \cite[p.~338]{H}) is deduced from Hypothesis~H1, proved as an implication. Here Hypothesis~H1 represents the printed \textsc{Remark} of Perelli, Pintz and Salerno \cite[p.~530]{PPS}, with their display (2) \cite[p.~529]{PPS}, in its uniform reading: one implied constant for all $x^{3/5}(\log x)^D \le y \le x$. Their printed \textsc{Theorem} \cite[p.~530]{PPS} reads:
\begin{quote}
``The estimate (2) holds if $\psi \leqslant \theta - 1/2$ and $\theta > 3/5$.''
\end{quote}
Immediately below it, their printed \textsc{Remark} \cite[p.~530]{PPS} reads:
\begin{quote}
``Indeed, as it is clear from the proof, we obtain (2) if (3) holds and $y \geqslant x^{3/5}(\log x)^C$, $C = C(A)$'',
\end{quote}
where (3) is $\psi \leqslant \theta - 1/2$.

\begin{remark}[On the uniform reading of the Remark of Perelli, Pintz and Salerno]
The uniform reading was checked by reading the proof in \cite[pp.~531 to 538]{PPS}: every implied constant in that proof is either absolute or depends on $A$ only, with the sole exception of $\delta = \delta(\theta)$ in display (5) on p.~531, which is taken from Huxley and Iwaniec \cite{HI} for small $Q$. It can be taken absolute: at $\theta = 3/5$ the range $\psi < 3\theta - 7/4 - \varepsilon = 1/20 - \varepsilon$ quoted on \cite[p.~530]{PPS} gives $\delta = 1/40$, and for larger $y$ one covers $(z, z + h]$ by at most $y x^{-3/5} + 1$ windows of length $x^{3/5}$, with $x$ replaced by $2x$, and adds the bounds. That range is taken from \cite{PPS}; \cite{HI} itself was not read. So the uniform reading of Hypothesis~H1 rests on this reading of the printed proof, which this note takes as a hypothesis rather than reproving.
\end{remark}

\item \textbf{Second cited input (Hypothesis H2).} JTNB Theorem 2.3 (arXiv Theorem 5, \cite[p.~339]{H}) is deduced from Hypothesis~H2, proved as an implication. Here Hypothesis~H2 is the Goldbach analogue of Theorem 3 of Perelli and Pintz \cite[p.~44]{PP}. It is not a numbered statement of that paper: Perelli and Pintz treat only the Goldbach problem \cite[p.~41]{PP}, and their numbered Theorem~3 is the $2k$-twin analogue of that argument \cite[p.~44]{PP}; the bound below is the Goldbach argument at general $Y$. Specifically, the Goldbach mean square bound follows from their displays (1) and (3) on p.~44, which reduce it to displays (4) and (5); they prove (4) for $N^{7/12 + \varepsilon} \le Y \le N$ in \S4 (p.~45) and (5) for $Y \ge Y_0(A, \varepsilon)$ and $H \ge Y^{1/3 + \varepsilon}$ in \S5 (p.~46), with $H = Y^{1/3 + \varepsilon}$ chosen on p.~44. On p.~339 of \cite{H}, Halupczok writes ``it can be shown (cp.\ [11, Thm.~3])'' and ``The proof in [11] can be adapted'', so JTNB Theorem 2.3 is her stated adaptation. We note clearly that this is a weaker citation than a numbered theorem.
\end{enumerate}

Concretely, Hypothesis~H2 is the hypothesis that for $\varepsilon, A > 0$, $N^{7/12 + \varepsilon} \le Y \le N$ and $H = Y^{1/3 + \varepsilon}$, the sum over $N < 2n \le N + H$ of $|R^*(2n) - M^*(2n)\mathfrak{S}(2n)|^2$ is $\ll H Y^2 L^{-A}$ with $L = \log N$, with $R^*$ and $M^*$ as on p.~43 of \cite{PP} and $\mathfrak{S}$ as on p.~41 of \cite{PP}. So Hypothesis~H2 is the conclusion of that argument at general $Y$, the case Perelli and Pintz treat and Halupczok adapts on p.~339 of \cite{H}, and it is taken as a hypothesis rather than reproved from displays (1), (3), (4) and (5) of \cite{PP}.

The two hypotheses match their printed sources as follows:
\begin{center}
\footnotesize
\begin{tabular}{@{}p{0.17\textwidth}p{0.39\textwidth}p{0.38\textwidth}@{}}
\toprule
Hypothesis & Printed source and range of $q$ & Steps behind the reading \\
\midrule
Hypothesis H1 & Display (2) of \cite[p.~529]{PPS}: sum over $q \le Q$ with $y = x^\theta$ and $Q = x^\psi (\log x)^{-B}$; condition (3), $\psi \leqslant \theta - 1/2$; Remark, p.~530, for $y \geqslant x^{3/5} (\log x)^C$, with $q \le Q \le y x^{-1/2} (\log x)^{-B}$. & Take $\psi = \theta - 1/2$, and $D$ for $C(A)$. The maxima over $a$, $h$, $z$ become choices $a(q)$, $h(q)$, $z(q)$. One constant for all $y$, by Remark~3.3. \\[4pt]
Hypothesis H2 & No $q$: a mean square over $N < 2n \le N + H$. Displays (1), (3), (4), (5), pp.~44 to 46 of \cite{PP}, at $N^{7/12 + \varepsilon} \le Y \le N$, $H = Y^{1/3 + \varepsilon}$. & Reduction by (1) and (3); (4) in \S4; (5) in \S5; each read in the Goldbach setting at general $Y$. \\
\bottomrule
\end{tabular}
\end{center}

\subsection{Proof sketch of Formulation A}

The proof of Formulation~A follows the argument of \cite{H} in four steps, except that her Lemma~2.1 is not used:
\begin{enumerate}
\item Substitute $2k_1 = n - p_1$. The ternary sum splits into a binary part and a main term part.
\item \emph{Binary part:} Bound the binary part using Theorem 5 of \cite{H-arXiv} (JTNB Theorem 2.3, \cite[p.~339]{H}), which provides a mean square bound for the binary Goldbach count in short intervals, combined with Cauchy-Schwarz over $q$ and a divisor moment bound.
\item \emph{Main term part:} Apply Theorem 3 of \cite{H-arXiv} (JTNB Theorem 2.1, \cite[p.~338]{H}), the Perelli-Pintz-Salerno Bombieri-Vinogradov theorem in short intervals. The binary singular series $S$ is expanded over squarefree moduli $s$ and truncated at $s \le L^D$; the congruences $p_1 \equiv a \pmod q$ and $p_1 \pmod s$ are combined via the Chinese remainder theorem, with Theorem 3 applied at modulus $\operatorname{lcm}(q, s)$; and the Euler product of the resulting main term is identified with $T(n, q, a)$, where the singular series tail bound holds unconditionally by taking $\sigma = 1/12$ and $D = 12(A + 3)$.
\item \emph{Non-coprime moduli:} For Formulation~B, the moduli $q \le Q$ with $(a, q) \neq 1$ are handled as in Section~2 and after Statement~\ref{thm:formulationB}.
\end{enumerate}

\subsection{Differences from the printed statement}\label{sec:differences}

Formulations~A and~B in this note differ from JTNB Theorem~1.2 as follows:
\begin{itemize}
\item the coprime restriction of Formulation~A, or $T_0$ in Formulation~B;
\item the hypothesis $Q \le X_1$ in Formulation~B, discussed after Statement~\ref{thm:formulationB};
\item the exponent $B$ may depend on $\varepsilon, \varepsilon_1, \varepsilon_2$ as well as on $A$;
\item $C$ and $Y_0$ may depend on the hypothesis constants and on $a$;
\item her Lemma~2.1 is replaced by Cauchy-Schwarz and a divisor moment, as in step 2 above;
\item the supplement with $\max^*$ is not covered.
\end{itemize}

\subsection{Relation to the rest of Halupczok's paper}

The later results of \cite{H} are unaffected. In particular, Corollary~4 of \cite{H-arXiv}, which is Corollary~1.4 of \cite[p.~334]{H}, sieves primes satisfying $p_1 \equiv -2 \pmod{\text{odd } d}$, which is always a coprime residue class, and the supplement taking a maximum over $a$ restricts to reduced residues only. We follow the statement of Corollary~1.4, since its proof on p.~345 prints $p_2 + 2$ where the statement has $p_1 + 2$. A reading of the rest of \cite{H} finds no subsequent result that invokes a non-coprime residue class $a$.

\begin{remark}[On the strength of the formulation]
For $(a, q) > 1$, a prime $p_1 \equiv a \pmod q$ must divide $(a, q)$, so $p_1 \le q$; hence for $q \le X_1$ no such prime lies in $(X_1, X_1 + Y_1]$ and the prime side vanishes. With the printed singular series $T(n, q, a)$, the Euler product need not vanish for these moduli $q$, and it is positive for $a = q = 3$, so an explicit statement incorporates either the restriction $(a, q) = 1$ or the convention $T_0(n, q, a)$.
\end{remark}

\section{Verification}\label{sec:formal}

The main results of this note are checked in Lean~4 with Mathlib, solely by the Lean kernel. The entry at the commit cited in \cite{Repo} pins \texttt{leanprover/lean4:v4.35.0-rc3} with Mathlib \texttt{v4.35.0-rc3} \cite{Mathlib}. All declarations reside in the namespace \texttt{LeanLab.Halupczok2012}, and file paths below are given relative to the folder \texttt{entries/halupczok2012} of \cite{Repo} at commit \texttt{12f09bfeca2ae00988fa039e2e82c6de4d147108}. On related work, the \texttt{PrimeNumberTheoremAnd} project \cite{PNT} aims to formalize the Prime Number Theorem with classical error term in Lean, and it hosts the Integrated Explicit Analytic Number Theory network; our setting is much narrower, checking one mean value statement for the ternary problem while taking its two deep analytic inputs as hypotheses.

\subsection{Encoding conventions}

Each statement of the paper becomes a Lean proposition, a \texttt{Prop}: Formulation~A is \texttt{Theorem2}, Formulation~B is \texttt{Theorem2Zeroed}, JTNB Theorem~2.1 (arXiv Theorem~3) is \texttt{Theorem3}, and JTNB Theorem~2.3 (arXiv Theorem~5) is \texttt{Theorem5} (the last line supplement of JTNB Theorem~1.2 and Corollary~1.4, arXiv Corollary~4, are not formalized). Hypothesis~H1 and Hypothesis~H2 enter as explicit Lean hypothesis arguments (\texttt{Prop}) named \texttt{PPS1984Remark} and \texttt{PP1993Goldbach}, so that \texttt{theorem2\_U1510 (hR : PPS1984Remark) (hPP : PP1993Goldbach) : Theorem2} and \texttt{theorem2Zeroed\_U1510} prove Formulations~A and~B from the two inputs with no new axiom, and \texttt{theorem2\_U1462} and \texttt{theorem2Zeroed\_U1462} prove them from \texttt{Theorem3} and \texttt{Theorem5}. A full formalization of Hypothesis~H1 and Hypothesis~H2 would require Lean proofs of \cite[pp.~531 to 538]{PPS} and of the reduction by displays (1) and (3), display (4) as in \S4 and display (5) as in \S5 of \cite{PP} in the Goldbach setting, together with a check that the Lean \texttt{ppR}, \texttt{ppM} and \texttt{S} match $R^*$, $M^*$ and $\mathfrak{S}$ of \cite{PP}.

In the Lean encoding of asymptotic hypotheses and conclusions:
\begin{itemize}
\item Each $\ll$ in a hypothesis is encoded as a universally quantified positive constant ($c : \text{\texttt{Fin 7}} \to \mathbb{R}$ and $c_7 : \mathbb{R}$); for example, $Y_1 \gg X_1^{3/5 + \varepsilon_1}$ appears in \texttt{Thm2Hyp} as \texttt{c 0 * X1 \^{} (3 / 5 + ε1) ≤ Y1};
\item Each $\ll$ in a conclusion is encoded as an existential constant $C$, such as \texttt{≤ C * Y1 * Y2 * Real.log Y2 \^{} (-A)};
\item The phrase ``sufficiently large'' is encoded as an existential threshold $Y_0$ (or $x_0$, $N_0$);
\item The constants $C$ and $Y_0$ may depend on $A$, the exponents $\varepsilon, \varepsilon_1, \varepsilon_2$, the hypothesis constants $c, c_7$, and the fixed integer $a$;
\item The exponent $B$ is existentially quantified after $A$ and the exponents, so the Lean $B$ may depend on the exponents, while the printed $B$ depends on $A$ only;
\item The sum \texttt{ternSum} runs over ordered pairs of primes $(p_1, p_2)$ with $p_3 = n - p_1 - p_2$ prime and asks for no distinctness, so a repeated prime counts just as in Halupczok's sum, which carries no such condition;
\item In \texttt{Theorem2Zeroed}, $Q \le X_1$ is kept as an explicit hypothesis; the deduction of $Q \le X_1$ from \texttt{Thm2Hyp} for $Y_0 \ge \max(e, c_6^2)$ in Section~3 is by hand, not in Lean.
\end{itemize}
Every hypothesis sign of \texttt{Thm2Hyp} and \texttt{Theorem2} was checked against the JTNB page image of p.~333, those of \texttt{Theorem3} and \texttt{Theorem5} against pp.~338 and 339, and those of \texttt{PPS1984Printed} and \texttt{PPS1984Remark} against \cite[p.~530]{PPS}.

Halupczok's symbols and the Lean names match as follows:
\begin{center}
\footnotesize
\begin{tabular}{@{}ll@{}}
\toprule
In \cite{H} and this note & Lean \\
\midrule
$T(n, q, a)$, $T_0(n, q, a)$ & \texttt{T n q a}, \texttt{T0 n q a} \\
inner ternary prime sum & \texttt{ternSum n X1 Y1 X2 Y2 q a} \\
hypotheses of JTNB Theorem~1.2 & \texttt{Thm2Hyp}, with the second bound on $Q$ stated apart \\
implied constants in the hypotheses & \texttt{c : Fin 7 → ℝ} and \texttt{c7} \\
implied constant, large enough & \texttt{C}, \texttt{Y0} \\
$L = \log Y_2$ & \texttt{Real.log Y2} \\
$\mathfrak{S}$, $R^*$, $M^*$ & \texttt{S}, \texttt{ppR}, \texttt{ppM} \\
\bottomrule
\end{tabular}
\end{center}

\subsection{Lean declarations and statements}

In the four-step proof of Section~3.2, the substitution $2k_1 = n - p_1$ is \texttt{ternSum\_eq}; the binary part bound is \texttt{binaryPart}, proved assuming \texttt{Theorem5} only; the main term reduction comprises \texttt{crtStep}, \texttt{mainTermMV\_of\_inputs}, and \texttt{singSeriesTails\_holds} (proved unconditionally with no cited input, taking $\sigma = 1/12$ and $D = 12(A + 3)$); and in the module \texttt{NonCoprime} of \cite{Repo}, the vanishing of non-coprime prime sums for $1 \le q \le X_1$ is \texttt{ternSum\_noncoprime} (by way of \texttt{prime\_cong\_noncoprime}), which gives the unconditional implication \texttt{theorem2Zeroed\_of\_theorem2}.

From \path{LeanLab/Halupczok2012/U1510Final.lean}, the headline theorems are:
{\tiny
\begin{verbatim}
theorem theorem2Zeroed_U1510 (hR : PPS1984Remark) (hPP : PP1993Goldbach) :
    Theorem2Zeroed :=
  theorem2Zeroed_U1496 (theorem3_of_uniform (uniform_of_remark hR)) hPP

theorem theorem2_U1510 (hR : PPS1984Remark) (hPP : PP1993Goldbach) : Theorem2 :=
  theorem2_U1496 (theorem3_of_uniform (uniform_of_remark hR)) hPP

theorem theorem3_of_remark (hR : PPS1984Remark) : Theorem3 :=
  theorem3_of_uniform (uniform_of_remark hR)

theorem theorem5_of_PP1993 (hPP : PP1993Goldbach) : Theorem5 :=
  theorem5_of_PP hPP
\end{verbatim}
}

From \texttt{LeanLab/Halupczok2012/U1462Tails.lean}, the reductions from JTNB Theorems 2.1 and 2.3 (\texttt{Theorem3} and \texttt{Theorem5}) are:
{\tiny
\begin{verbatim}
theorem theorem2Zeroed_U1462 (h3 : Theorem3) (h5 : Theorem5) : Theorem2Zeroed
theorem theorem2_U1462 (h3 : Theorem3) (h5 : Theorem5) : Theorem2
\end{verbatim}
}

From \texttt{LeanLab/Halupczok2012/Statements.lean}, the elementary prime-in-progression lemma is:
{\tiny
\begin{verbatim}
theorem prime_cong_noncoprime {p1 q d : ℕ} {a : ℤ} (hp : p1.Prime) (hd : d.Prime)
    (hc : (p1 : ℤ) ≡ a [ZMOD q]) (hdq : d ∣ q) (hda : (d : ℤ) ∣ a) : p1 = d
\end{verbatim}
}

From \texttt{LeanLab/Halupczok2012/Statements.lean}, the definitions of the singular series \texttt{T} matching \eqref{eq:T-def}, the ternary prime sum \texttt{ternSum}, the hypothesis bundle \texttt{Thm2Hyp}, and Formulation~A (\texttt{Theorem2}) are:
{\tiny
\begin{verbatim}
noncomputable def T (n q : ℕ) (a : ℤ) : ℝ :=
  (1 / (Nat.totient q : ℝ)) * ∏' p : Nat.Primes,
    (if ((p : ℕ) ∣ n ∧ ¬ (p : ℕ) ∣ q) ∨ (¬ ((p : ℕ) : ℤ) ∣ (n - a) ∧ (p : ℕ) ∣ q) then
        1 - 1 / ((p : ℝ) - 1) ^ 2
      else if ¬ (p : ℕ) ∣ n ∧ ¬ (p : ℕ) ∣ q then 1 + 1 / ((p : ℝ) - 1) ^ 3
      else (p : ℝ) / ((p : ℝ) - 1))

noncomputable def ternSum (n : ℕ) (X1 Y1 X2 Y2 : ℝ) (q : ℕ) (a : ℤ) : ℝ :=
  ∑ x ∈ ((range (n + 1)) ×ˢ (range (n + 1))).filter (fun x =>
      x.1.Prime ∧ x.2.Prime ∧ x.1 + x.2 ≤ n ∧ (n - x.1 - x.2).Prime ∧
      X1 < x.1 ∧ (x.1 : ℝ) ≤ X1 + Y1 ∧ X2 < x.2 ∧ (x.2 : ℝ) ≤ X2 + Y2 ∧ (x.1 : ℤ) ≡ a [ZMOD q]),
    Real.log x.1 * Real.log x.2 * Real.log ((n - x.1 - x.2 : ℕ) : ℝ)

def Thm2Hyp (ε ε1 ε2 B : ℝ) (c : Fin 7 → ℝ) (n : ℕ) (X1 Y1 X2 Y2 Q : ℝ) : Prop :=
  Odd n ∧ Y1 ≤ X1 ∧ c 0 * X1 ^ (3 / 5 + ε1) ≤ Y1 ∧ Y2 ≤ X2 ∧ c 1 * X2 ^ (7 / 12 + ε2) ≤ Y2 ∧
  c 2 * Y2 ^ (1 / 3 + ε) ≤ Y1 ∧ Y1 ≤ c 3 * Y2 ∧
  0 ≤ (n : ℝ) - X1 - Y1 - X2 - Y2 ∧ c 4 * Y2 ≤ (n : ℝ) - X1 - Y1 - X2 - Y2 ∧
  (n : ℝ) - X1 - Y1 - X2 - Y2 ≤ c 5 * Y2 ∧
  1 ≤ Q ∧ Q ≤ c 6 * Y1 * X1 ^ (-(1 / 2) : ℝ) * Real.log Y2 ^ (-B)

def Theorem2 : Prop :=
  ∀ A ε ε1 ε2 : ℝ, 0 < A → 0 < ε → 0 < ε1 → 0 < ε2 → ∃ B : ℝ, 0 < B ∧
  ∀ c : Fin 7 → ℝ, (∀ i, 0 < c i) → ∀ c7 : ℝ, 0 < c7 → ∀ a : ℤ, ∃ C Y0 : ℝ,
  ∀ (n : ℕ) (X1 Y1 X2 Y2 Q : ℝ), Y0 ≤ Y1 → Y0 ≤ Y2 → Thm2Hyp ε ε1 ε2 B c n X1 Y1 X2 Y2 Q →
    Q ≤ c7 * Y1 ^ (3 / 2 : ℝ) * ((n : ℝ) - X1) ^ (-(1 / 2) : ℝ) → (a : ℝ) ≤ (n : ℝ) - X1 - Y1 →
    ∑ q ∈ (Icc 1 ⌊Q⌋₊).filter (fun q : ℕ => Int.gcd a (q : ℤ) = 1),
      |ternSum n X1 Y1 X2 Y2 q a - T n q a * Y1 * Y2| ≤ C * Y1 * Y2 * Real.log Y2 ^ (-A)
\end{verbatim}
}

From the module \texttt{NonCoprime} of \cite{Repo}, the zeroed singular series \texttt{T0}, the vanishing of non-coprime prime sums, Formulation~B (\texttt{Theorem2Zeroed}), and the unconditional implication from Formulation~A to Formulation~B are:
{\tiny
\begin{verbatim}
noncomputable def T0 (n q : ℕ) (a : ℤ) : ℝ := if Int.gcd a q = 1 then T n q a else 0

theorem ternSum_noncoprime {n q : ℕ} {a : ℤ} {X1 Y1 X2 Y2 : ℝ} (hq : 1 ≤ q)
    (hg : Int.gcd a q ≠ 1) (hqX : (q : ℝ) ≤ X1) : ternSum n X1 Y1 X2 Y2 q a = 0

def Theorem2Zeroed : Prop :=
  ∀ A ε ε1 ε2 : ℝ, 0 < A → 0 < ε → 0 < ε1 → 0 < ε2 → ∃ B : ℝ, 0 < B ∧
  ∀ c : Fin 7 → ℝ, (∀ i, 0 < c i) → ∀ c7 : ℝ, 0 < c7 → ∀ a : ℤ, ∃ C Y0 : ℝ,
  ∀ (n : ℕ) (X1 Y1 X2 Y2 Q : ℝ), Y0 ≤ Y1 → Y0 ≤ Y2 → Thm2Hyp ε ε1 ε2 B c n X1 Y1 X2 Y2 Q →
    Q ≤ c7 * Y1 ^ (3 / 2 : ℝ) * ((n : ℝ) - X1) ^ (-(1 / 2) : ℝ) → (a : ℝ) ≤ (n : ℝ) - X1 - Y1 →
    Q ≤ X1 →
    ∑ q ∈ Icc 1 ⌊Q⌋₊, |ternSum n X1 Y1 X2 Y2 q a - T0 n q a * Y1 * Y2|
      ≤ C * Y1 * Y2 * Real.log Y2 ^ (-A)

theorem theorem2Zeroed_of_theorem2 (h : Theorem2) : Theorem2Zeroed
\end{verbatim}
}

The two cited inputs Hypothesis~H1 (\texttt{PPS1984Remark}) and Hypothesis~H2 (\texttt{PP1993Goldbach}) are defined in \texttt{LeanLab/Halupczok2012/U1495PPS.lean} and \texttt{U1496PP.lean}. They are formulated as Lean hypotheses passed as explicit arguments, not as axioms:
{\tiny
\begin{verbatim}
noncomputable def psiAP (z : ℝ) (q : ℕ) (a : ℤ) : ℝ :=
  ∑ n ∈ (Ioc 0 ⌊z⌋₊).filter (fun n : ℕ => (n : ℤ) ≡ a [ZMOD q]),
    ArithmeticFunction.vonMangoldt n

noncomputable def ppsTerm (z h : ℝ) (q : ℕ) (a : ℤ) : ℝ :=
  |psiAP (z + h) q a - psiAP z q a - h / q.totient|

def PPS1984Remark : Prop :=
  ∀ A : ℝ, 0 < A → ∃ D B : ℝ, 0 < B ∧ ∃ C x0 : ℝ, ∀ x y Q : ℝ, x0 ≤ x →
    x ^ (3 / 5 : ℝ) * Real.log x ^ D ≤ y → y ≤ x →
    Q ≤ y * x ^ (-(1 / 2) : ℝ) * Real.log x ^ (-B) →
    ∀ (a : ℕ → ℤ) (h z : ℕ → ℝ), (∀ q, Int.gcd (a q) q = 1) →
    (∀ q, 0 < h q ∧ h q ≤ y) → (∀ q, x / 2 < z q ∧ z q ≤ x) →
    ∑ q ∈ Icc 1 ⌊Q⌋₊, ppsTerm (z q) (h q) q (a q) ≤ C * y * Real.log x ^ (-A)

def PP1993Goldbach : Prop :=
  ∀ ε A : ℝ, 0 < ε → 0 < A → ∃ C N0 : ℝ, ∀ N Y : ℝ, N0 ≤ N → N ^ (7 / 12 + ε) ≤ Y → Y ≤ N →
    ∑ k ∈ kRange (N / 2) (Y ^ (1 / 3 + ε) / 2),
        (ppR (2 * k) N Y - S (2 * k) * ppM (2 * k) N Y) ^ 2 ≤
      C * Y ^ (1 / 3 + ε) * Y ^ 2 * Real.log N ^ (-A)
\end{verbatim}
}
Here \texttt{ppR} is $R^*(2n, N, Y)$, the sum over $h + k = 2n$ with $N - Y < h \le N$ and $k \le Y$ of $\Lambda(h)\Lambda(k)$ (\cite[p.~43]{PP}); \texttt{ppM} is $M^*(2n, N, Y)$, the corresponding count with weight $1$; and \texttt{S} is the binary singular series $\mathfrak{S}$ of \cite[p.~41]{PP} and of Halupczok's display (1.2), \cite[p.~335]{H}.

\subsection{Build, axiom audit, and status summary}

From \texttt{entries/halupczok2012} at the cited commit, \texttt{lake exe cache get} followed by \texttt{lake build LeanLab.Halupczok2012.U1510Final SolutionHalupczok2012} builds successfully, 8976 jobs. The axiom audit lines are verbatim:
{\tiny
\begin{verbatim}
'LeanLab.Halupczok2012.theorem2Zeroed_U1510' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'LeanLab.Halupczok2012.theorem2_U1510' depends on axioms:
  [propext, Classical.choice, Quot.sound]
\end{verbatim}
}
The theorems \texttt{theorem3\_of\_remark}, \texttt{theorem5\_of\_PP1993}, \texttt{theorem2Zeroed\_U1462}, \texttt{theorem2\_U1462}, \texttt{ternSum\_noncoprime} and \texttt{theorem2Zeroed\_of\_theorem2} have the same three axioms.

Table~\ref{tab:status} summarizes the verification status of each input and step in the argument.

\begin{table}[htbp]
\centering
\caption{Verification status of inputs and steps. Kernel: checked by the Lean kernel. Cited: a Lean hypothesis taken from the literature. Hand: done by hand or by reading, not in Lean.}\label{tab:status}
\footnotesize
\begin{tabular}{@{}p{0.46\textwidth}p{0.49\textwidth}@{}}
\toprule
Input or step & Status \\
\midrule
\texttt{PPS1984Remark}, printed Remark p.~530, uniform reading & Cited, Lean hypothesis; uniform reading is Hand, pp.~531 to 538 \\[4pt]
\texttt{PP1993Goldbach}, unnumbered Goldbach analogue of PP1993 Theorem 3 & Cited, Lean hypothesis; from displays (1), (3), (4), (5), pp.~44 to 46 \\[4pt]
JTNB Theorem 2.1 from \texttt{PPS1984Remark} & Kernel, \texttt{theorem3\_of\_remark} \\[4pt]
JTNB Theorem 2.3 from \texttt{PP1993Goldbach} & Kernel, \texttt{theorem5\_of\_PP1993} \\[4pt]
singular series truncation and Euler product & Kernel, no cited input, \texttt{singSeriesTails\_holds} \\[4pt]
Formulation A, coprime reading of Theorem 1.2 & Kernel from the two inputs, \texttt{theorem2\_U1510} \\[4pt]
Formulation B, all $q$ with $T_0$ and $Q \le X_1$ & Kernel from the two inputs, \texttt{theorem2Zeroed\_U1510} \\[4pt]
Formulation A implies Formulation B & Kernel, unconditional, \texttt{theorem2Zeroed\_of\_theorem2} \\[4pt]
non-coprime prime sums vanish for $q \le X_1$ & Kernel, unconditional, \texttt{ternSum\_noncoprime} \\[4pt]
$T(n, 3, 3) \ge 9/16$ for odd $n$ & Hand, Remark~2.1 \\[4pt]
a form of Formulation B without $Q \le X_1$ & Hand, Section~3 \\[4pt]
later results of \cite{H} unaffected & Hand, Section~3.4 and a reading of \cite{H} \\[4pt]
hypothesis signs against the page images & Hand, Section~4.1 \\
\bottomrule
\end{tabular}
\end{table}

\section{Data availability}

The formalization is archived in the Palomar registry under entry \texttt{PALOMAR-2026-10-28-000026}, version~1 \cite{Palomar}, available at \url{https://palomar-registry.org/entry.html?id=PALOMAR-2026-10-28-000026&version=1}. The registered theorems are \texttt{theorem2Zeroed\_U1510}, \texttt{theorem2\_U1510}, \texttt{theorem3\_of\_remark}, and \texttt{theorem5\_of\_PP1993}, with \texttt{PPS1984Remark} and \texttt{PP1993Goldbach} as Lean hypotheses. Palomar's mechanical check passed with no warnings.

The public Lean source code is available under the Apache-2.0 license in the repository \url{https://github.com/sthubbar/goldbach-lean} in the folder \texttt{entries/halupczok2012} at commit \texttt{12f09bfeca2ae00988fa039e2e82c6de4d147108} \cite{Repo}, and it builds by the command in Section~\ref{sec:formal}.

\subsection*{Use of AI}
Steve Hubbard designed the research program and directed this work. AI tools, Claude and Gemini, were used to write the Lean code and draft the text. AI tools also compared the statements with the sources and carried out the reading of the proof in Remark~3.3. The author takes full responsibility for the content.

\begin{thebibliography}{99}

\bibitem[H]{H}
K.~Halupczok, \emph{Goldbach's problem with primes in arithmetic progressions and in short intervals}, J.~Th\'eor.\ Nombres Bordeaux \textbf{25} (2013), no.~2, 331 to 351, doi:10.5802/jtnb.839. Pages used: Theorem 1.2 pp.~333 to 334; Theorem 2.1 p.~338; Theorem 2.3 p.~339; displays (1.1) and (1.2) p.~335; the proof sentence on $(q, a) = 1$ p.~344.

\bibitem[H-arXiv]{H-arXiv}
K.~Halupczok, \emph{Goldbach's problem with primes in arithmetic progressions and in short intervals}, preprint, arXiv:1212.4406, v1, 18 Dec 2012.

\bibitem[PPS]{PPS}
A.~Perelli, J.~Pintz and S.~Salerno, \emph{Bombieri's theorem in short intervals}, Ann.\ Scuola Norm.\ Sup.\ Pisa Cl.\ Sci.\ (4) \textbf{11} (1984), no.~4, 529 to 539, numdam ASNSP\_1984\_4\_11\_4\_529\_0. Pages used: display (2) p.~529; THEOREM and REMARK p.~530; proof pp.~531 to 538, display (5) p.~531.

\bibitem[PP]{PP}
A.~Perelli and J.~Pintz, \emph{On the exceptional set for Goldbach's problem in short intervals}, J.~London Math.\ Soc.\ (2) \textbf{47} (1993), 41 to 49, doi:10.1112/jlms/s2-47.1.41. Pages used: introduction p.~41; $R^*$ and $M^*$ p.~43; displays (1), (3), (4), (5) and Theorem 3 p.~44; \S4 p.~45; \S5 p.~46.

\bibitem[HI]{HI} M.~N.~Huxley and H.~Iwaniec, \emph{Bombieri's theorem in short intervals}, Mathematika \textbf{22} (1975), 188 to 194.

\bibitem[Helfgott]{Helfgott}
H.~A.~Helfgott, \emph{Major arcs for Goldbach's problem}, preprint, arXiv:1305.2897, 2013; see also \emph{Minor arcs for Goldbach's problem}, preprint, arXiv:1205.5252, 2012.

\bibitem[Palomar]{Palomar}
Palomar registry entry \texttt{PALOMAR-2026-10-28-000026}, version 1, \url{https://palomar-registry.org/entry.html?id=PALOMAR-2026-10-28-000026&version=1}.

\bibitem[Repo]{Repo}
S.~Hubbard, \emph{goldbach-lean}, \url{https://github.com/sthubbar/goldbach-lean}, \texttt{entries/halupczok2012}, commit \texttt{12f09bfeca2ae00988fa039e2e82c6de4d147108}.

\bibitem[PNT]{PNT}
\texttt{PrimeNumberTheoremAnd}, \url{https://github.com/AlexKontorovich/PrimeNumberTheoremAnd}.

\bibitem[Mathlib]{Mathlib}
The mathlib Community, \emph{The Lean mathematical library}, \url{https://github.com/leanprover-community/mathlib4}, version \texttt{v4.35.0-rc3}.

\end{thebibliography}

\end{document}