\documentclass[10pt,reqno]{amsart}

\usepackage{amsmath,amssymb,amsthm}
\usepackage{booktabs}
\usepackage{array}
\usepackage{url}
\usepackage[margin=1in]{geometry}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\renewcommand{\thetheorem}{M}
\newtheorem*{propA}{Proposition A}
\newtheorem*{thmB}{Theorem B}
\newtheorem*{thmC}{Theorem C}
\newtheorem*{thmD}{Theorem D}
\newtheorem*{thmE}{Theorem E}
\newtheorem*{saouterlemma1}{Lemma 1 \normalfont(Saouter \cite{Saouter1998}, page 864; from Theorem 5 of Brillhart, Lehmer, and Selfridge \cite{BLS1975})}
\newtheorem*{saouterthm1}{Theorem 1 \normalfont(Saouter \cite{Saouter1998}, page 864)}
\newtheorem*{saouterlemma2}{Lemma 2 \normalfont(Saouter \cite{Saouter1998}, page 864)}
\newtheorem*{saouterthm2}{Theorem 2 \normalfont(Saouter \cite{Saouter1998}, page 864)}
\newtheorem*{prothlemma}{Proth's Criterion \normalfont(\texttt{Proth.proth})}

\theoremstyle{remark}
\newtheorem*{remark}{Remark}

\title[Saouter's Primality Criterion in Lean and a 25 Rung Route]{Saouter's primality criterion in Lean, a ladder constant, and a 25 rung route to odd Goldbach up to $10^{20}$}
\author{Steve Hubbard}
\address{Independent Researcher}

\begin{document}
\sloppy

\begin{abstract}
This note gives Lean proofs, with no hypothesis, of the primality criterion of Saouter's paper, Lemma 1 for every even $F$, Theorems 1 and 2, and it records the reading of the constant on page 865 under which the formula agrees with the rest of the paper; separately, given the published even Goldbach computation to $4\cdot 10^{18}$ as an explicit hypothesis, a ladder of 25 Proth primes reaches $10^{20}$ in the Lean kernel. The binary Goldbach conjecture remains open and this note makes no progress on it. The ternary Goldbach theorem for all odd numbers is Helfgott's (\texttt{arXiv:1312.7748}), and it is not formalized here and not used.
\end{abstract}

\maketitle

\section{Introduction and Main Statements}

We formalize in Lean 4, with no hypothesis, Saouter's Lemma 1 for every even $F$ and Theorems 1 and 2, record the reading of the constant on page 865 matching his ladder formula, and deduce ternary Goldbach up to $10^{20}$ from the published $4\cdot 10^{18}$ even Goldbach bound via a ladder of 25 Proth primes.

\begin{theorem}[Main statements]
\textup{(a)} Lemma 1 of Saouter holds for every even $F$, and Saouter's Theorems 1 and 2 hold, in Lean with no hypothesis; \textup{(b)} assuming every even integer from $4$ to $4\cdot 10^{18}$ is a sum of two primes, every odd integer from $7$ to $10^{20}$ is a sum of three primes, in Lean. See Theorems B, C and E for detail.
\end{theorem}

The binary Goldbach conjecture remains open, and this note makes no progress on it. The ternary Goldbach theorem for all odd numbers is Helfgott's \cite{Helfgott2013}, \texttt{arXiv:1312.7748}, and it is not formalized here and not used.

To place the present formalization in the context of prior work, the primary references are Saouter's own verification to $10^{20}$ \cite{Saouter1998} using the even Goldbach input $4\cdot 10^{11}$ from Sinisalo \cite{Sinisalo1993} and a prime ladder of about $250\cdot 10^6$ rungs, together with the subsequent work of Helfgott and Platt \cite{HelfgottPlatt2013}, who verified the ternary Goldbach conjecture up to $8.875\cdot 10^{30}$, far past this range, by the same ladder idea with Proth primes. The range $10^{20}$ is therefore not a new result. What the entry supplies is a short kernel-checked derivation.

We state the exact scope and limits of this verification at the outset:
\begin{itemize}
\item Saouter's ladder of about $250\cdot 10^6$ rungs is not reverified; only the 100 values of Table 1 of \cite{Saouter1998} and the starting and ending primes ($138412033$ and $100000000209366024193$) are checked in the Lean kernel.
\item The 25-rung route is a different ladder built on a larger even Goldbach input ($4\cdot 10^{18}$, from Oliveira e Silva, Herzog, and Pardi \cite{OSP2014}) and does not check Saouter's computation.
\item In Saouter \cite{Saouter1998}, the formula on page 865 reads $N = 5\cdot 2^{23}\cdot k + 1258213$ as printed, and is read as $N(k) = 5\cdot 2^{23}\cdot k + 12582913$ with one digit $9$ restored. The paper's method, table, starting and ending primes, and result all stand.
\end{itemize}
This note is for readers of Saouter's paper and of later ladder computations, and for those who want the primality criterion in a form that a proof assistant accepts.

\section{Saouter's Method and Primality Criteria}

In \cite{Saouter1998} (pages 863 to 866), Saouter verifies the odd Goldbach conjecture up to $10^{20}$. The method on page 863 reduces the ternary problem on bounded intervals to the binary problem via a chain of primes: if $N$ is odd, $p$ is prime, and $N - p$ is a sum of two primes, then $N = p + (N - p)$ is a sum of three primes. Given the even Goldbach verification up to $4\cdot 10^{11}$ by Sinisalo \cite{Sinisalo1993}, one exhibits a strictly increasing sequence of primes
\[
p_0 < p_1 < \dots < p_P
\]
such that $p_0 < 4\cdot 10^{11}$, each consecutive step satisfies $p_{i+1} - p_i < 4\cdot 10^{11}$, and $p_P > 10^{20}$. With step size bounded by $4\cdot 10^{11}$, at least $250\cdot 10^6$ primes are needed to reach $10^{20}$.

To test primes rapidly at this scale without factoring $N - 1$ in full, Saouter uses a special case of the primality criteria of Brillhart, Lehmer, and Selfridge \cite{BLS1975}. We record the statements from page 864 of \cite{Saouter1998}.

\begin{saouterlemma1}
Let $N = RF + 1$ be odd with $F$ even, the factorization of $F$ known, and $\gcd(R, F) = 1$. Suppose an integer $a$ satisfies
\[
a^{N-1} \equiv 1 \pmod{N}
\quad\text{and}\quad
\gcd\bigl(a^{(N-1)/p} - 1,\, N\bigr) = 1
\]
for every prime $p$ dividing $F$. Write $R = 2Fs + r$ with $0 \le r < 2F$. If $N < 2F^3$, then $N$ is prime if and only if $s = 0$ or $r^2 - 8s$ is not a perfect square.
\end{saouterlemma1}

Specializing $F$ to a power of $2$ eliminates all odd prime factors of $F$ and reduces the Lucas-type hypotheses to a single modular exponentiation:

\begin{saouterthm1}
Let $N = 2^{22}R + 1$ with $N < 10^{20}$ and $R$ odd, and suppose there is some integer $a$ with
\[
a^{(N-1)/2} \equiv -1 \pmod{N}.
\]
Write $R = 2\cdot 2^{22}s + r$ with $0 \le r < 2\cdot 2^{22}$. Then $N$ is prime if and only if $s = 0$ or $r^2 - 8s$ is not a perfect square. The size condition of Lemma 1 holds since $2\cdot (2^{22})^3 > 10^{20}$.
\end{saouterthm1}

To avoid searching for a base $a$ at each candidate, Saouter fixes $a = 5$ by restricting the residue class of $N$ modulo $10$:

\begin{saouterlemma2}
A prime $N$ of the form $10k + 3$ satisfies
\[
5^{(N-1)/2} \equiv -1 \pmod{N},
\]
by Euler's criterion and quadratic reciprocity.
\end{saouterlemma2}

\begin{saouterthm2}
Let $N = 2^{22}R + 1$ with $N < 10^{20}$, $N \equiv 3 \pmod{10}$ and $R$ odd, and suppose $5^{(N-1)/2} \equiv -1 \pmod{N}$. Write $R = 2\cdot 2^{22}s + r$ with $0 \le r < 2\cdot 2^{22}$. Then $N$ is prime if and only if $s = 0$ or $r^2 - 8s$ is not a perfect square.
\end{saouterthm2}

The ladder generation algorithm on page 864 of \cite{Saouter1998} proceeds as follows:
\begin{enumerate}
\item Start at $p_0 = 138412033 = 33\cdot 2^{22} + 1$, which is the least prime satisfying both $N = 2^{22}R + 1$ ($R$ odd) and $N \equiv 3 \pmod{10}$.
\item From the current prime rung, step up by $95360\cdot 2^{22}$, which is the largest multiple of $10\cdot 2^{22}$ below $4\cdot 10^{11}$.
\item Test the candidate for primality using Theorem 2; on a composite candidate, step down by $10\cdot 2^{22}$ repeatedly until a prime is reached.
\end{enumerate}

In Section 4, page 865 of \cite{Saouter1998}, the ending prime of the ladder is reported as
\[
100000000209366024193,
\]
and Table 1 gives the initial 100 values of the parameter $k$ for the ladder primes, where the formula on page 865 reads $N = 5\cdot 2^{23}\cdot k + 1258213$.

\section{Proposition A: The Formula Constant on Page 865}

We begin by recording the arithmetic relationship between the formula as printed on page 865 and the candidate family defined on page 864.

\begin{propA}
Let
\[
N(k) = 5\cdot 2^{23}\cdot k + 12582913
\quad\text{and}\quad
N'(k) = 5\cdot 2^{23}\cdot k + 1258213,
\]
where $N'(k)$ is the formula as printed on page 865 of \cite{Saouter1998}. Then:
\begin{enumerate}
\item[\textup{(1)}] Since $12582913 = 3\cdot 2^{22} + 1$ and $5\cdot 2^{23} = 10\cdot 2^{22}$, we have
\[
N(k) = 2^{22}(10k + 3) + 1,
\]
so $N(k) \equiv 3 \pmod{10}$ and the cofactor $R = 10k + 3$ is odd for every natural number $k$.
\item[\textup{(2)}] At $k = 3$ and $k = 2384185796007$, the formula $N(k)$ gives
\begin{align*}
N(3) &= 138412033 = 33\cdot 2^{22} + 1,\\
N(2384185796007) &= 100000000209366024193 = 2^{22}\cdot 23841857960073 + 1,
\end{align*}
which are the starting and ending primes of \cite{Saouter1998}, with $23841857960073$ odd.
\item[\textup{(3)}] For the printed form $N'(k)$, evaluation at $k = 3$ gives the composite number
\[
N'(3) = 127087333 = 19\cdot 6688807,
\]
$N'(k) \bmod 2^{22}$ is never $1$ for any natural number $k$, and $N(k) = N'(k) + 11324700$.
\item[\textup{(4)}] Every one of the 100 printed values of $k$ in Table 1 of \cite{Saouter1998} gives a prime $N(k)$, with largest consecutive step $399968829440 = 95360\cdot 2^{22}$ by script.
\end{enumerate}
\end{propA}

\begin{proof}
Since $2^{22} = 4194304$, direct multiplication yields
\[
3\cdot 2^{22} + 1 = 3\cdot 4194304 + 1 = 12582912 + 1 = 12582913.
\]
Consequently, for any natural number $k$,
\[
N(k) = 5\cdot 2^{23}\cdot k + 12582913 = 2^{22}(10k) + 2^{22}\cdot 3 + 1 = 2^{22}(10k + 3) + 1.
\]
Because $2^{22} = (2^4)^5\cdot 2^2 \equiv 6\cdot 4 = 24 \equiv 4 \pmod{10}$, we have
\[
N(k) \equiv 4(10k + 3) + 1 \equiv 12 + 1 \equiv 3 \pmod{10},
\]
and $10k + 3 = 2(5k + 1) + 1$ is odd.

Substituting $k = 3$ into $N(k)$ gives $10(3) + 3 = 33$ and
\[
N(3) = 33\cdot 2^{22} + 1 = 138412033.
\]
Substituting $k = 2384185796007$ gives $10k + 3 = 23841857960073$, which is odd, and
\[
N(2384185796007) = 2^{22}\cdot 23841857960073 + 1 = 100000000209366024193.
\]
In contrast, for $N'(k) = 5\cdot 2^{23}\cdot k + 1258213$, the difference is constant:
\[
N(k) - N'(k) = 12582913 - 1258213 = 11324700.
\]
Since $5\cdot 2^{23}\cdot k = 10k\cdot 2^{22}$ is a multiple of $2^{22}$, we have $N'(k) \equiv 1258213 \pmod{2^{22}}$, which is never congruent to $1 \pmod{2^{22}}$ for any $k$. At $k = 3$, $N'(3) = 138412033 - 11324700 = 127087333 = 19\cdot 6688807$. Finally, each of the 100 values $N(k)$ for $k$ in Table 1 is checked prime in the Lean kernel via Theorem 2 (\texttt{Table1Thm2.\allowbreak table1\_\allowbreak prime\_\allowbreak thm2}), each consecutive step is below $4\cdot 10^{11}$ (\texttt{Table1.\allowbreak table1\_\allowbreak gaps}), and by script the largest consecutive step is $399968829440 = 95360\cdot 2^{22}$.
\end{proof}

Thus the formula on page 865 is read with constant $12582913 = 3\cdot 2^{22} + 1$, with one digit $9$ restored; note that $12582913 = 7\cdot 1797559$ is itself composite, as it is only the constant term $N(0)$ corresponding to $k = 0$ rather than a rung of the ladder (which starts at $k = 3$). By script, 9 of the 100 values $N'(k)$ are prime, and a rerun of the paper's algorithm starting from $138412033$ reproduces Table 1 of \cite{Saouter1998} exactly. No other change to \cite{Saouter1998} is needed.

\section{Formalization of the Primality Criteria in Lean}

We now turn to the Lean formalization of Lemma 1, Theorems 1 and 2, Lemma 2, and the Table 1 checks. Note also that Lemma 8 of Ramar\'e and Saouter \cite{RamareSaouter2003} restates Lemma 1 with the factor argument.

\begin{thmB}[\texttt{BLS.lemma1}]
Lemma 1 of Section 2 holds for every even $F$.
\end{thmB}

\begin{proof}
Let $N = RF + 1$ satisfy the hypotheses of Lemma 1. By Pocklington's order argument applied to each prime power $p^e \parallel F$, the conditions $a^{N-1} \equiv 1 \pmod{N}$ and $\gcd(a^{(N-1)/p} - 1, N) = 1$ imply that the multiplicative order of $a$ modulo any prime factor $q$ of $N$ is divisible by $F$. By Fermat's little theorem, $F \mid (q - 1)$, which puts every prime factor $q$ of $N$ in the residue class $1 \pmod{F}$. Since products of integers congruent to $1 \pmod{F}$ remain congruent to $1 \pmod{F}$, every positive divisor of $N$ is congruent to $1 \pmod{F}$. Moreover, since $F$ is even and $\gcd(R, F) = 1$, $R$ must be odd; because $R = 2Fs + r$ and $2Fs$ is even, the remainder $r$ is also odd.

Suppose first that $N$ is composite. Then $N$ factors as a product of two integers above $1$,
\[
N = (uF + 1)(vF + 1)
\]
with integers $u, v \ge 1$. Expanding the product gives
\[
RF + 1 = uvF^2 + (u + v)F + 1,
\]
and dividing by $F$ yields
\[
R = uvF + u + v.
\]
From the strict inequality $uvF^2 < (uF + 1)(vF + 1) = N < 2F^3$, dividing by $F^2$ gives $uv < 2F$. Since $u, v \ge 1$, we have $(u - 1)(v - 1) \ge 0$, so
\[
u + v \le uv + 1 \le 2F.
\]
Because $R$ is odd and $F$ is even, the term $uvF$ is even, whence $u + v = R - uvF$ is odd. Since $2F$ is even and $u + v$ is odd, the weak inequality $u + v \le 2F$ forces the strict inequality
\[
u + v < 2F.
\]
Furthermore, since $u + v$ is odd, one of $u, v$ is even and the other is odd, so their product $uv$ is even. We may therefore write
\[
R = 2F\left(\frac{uv}{2}\right) + (u + v)
\quad\text{with}\quad
0 < u + v < 2F.
\]
By uniqueness of the quotient $s$ and remainder $r$ in Euclidean division of $R$ by $2F$, we obtain
\[
s = \frac{uv}{2} \ge 1
\quad\text{and}\quad
r = u + v.
\]
Consequently,
\[
r^2 - 8s = (u + v)^2 - 4uv = (u - v)^2,
\]
which is a perfect square.

Conversely, suppose that $s \ge 1$ and $r^2 - 8s = t^2$ for an integer $t \ge 0$. Since $r$ is odd, $r^2$ is odd, so $t^2 = r^2 - 8s$ is odd, which implies that $t$ is odd. Therefore $r + t$ and $r - t$ are both even, and
\[
u = \frac{r + t}{2}, \qquad v = \frac{r - t}{2}
\]
are integers satisfying
\[
u + v = r \qquad\text{and}\qquad uv = \frac{r^2 - t^2}{4} = \frac{8s}{4} = 2s > 0.
\]
Since $uv = 2s > 0$ and $u + v = r > 0$, both $u$ and $v$ are strictly positive integers ($u, v \ge 1$). Multiplying the factors $uF + 1 > 1$ and $vF + 1 > 1$ gives
\[
(uF + 1)(vF + 1) = uvF^2 + (u + v)F + 1 = 2sF^2 + rF + 1 = (2Fs + r)F + 1 = RF + 1 = N,
\]
which shows that $N$ is composite. Thus $N$ is prime if and only if $s = 0$ or $r^2 - 8s$ is not a perfect square.
\end{proof}

\begin{thmC}
Saouter's Theorem 1 (for both a natural base and an integer base), Lemma 2, and Theorem 2 (in both directions) hold in Lean with no hypothesis; Lemma 2 shows that the hypothesis on $5$ holds for every prime $N \equiv 3 \pmod{10}$, so the test rejects no prime of this class, and the form \texttt{Thm2.\allowbreak theorem2\_\allowbreak if} keeps the hypothesis on $5$ and replaces $N < 10^{20}$ by $N < 2\cdot(2^{22})^3$, for the direction from the square test to primality. The Lean names are \texttt{Thm1.\allowbreak theorem1}, \texttt{Thm1.\allowbreak theorem1\_\allowbreak int}, \texttt{Paper.\allowbreak lemma2}, \texttt{Thm2.\allowbreak theorem2}, and \texttt{Thm2.\allowbreak theorem2\_\allowbreak if}.
\end{thmC}

\begin{proof}
Let $F = 2^{22}$ and $N = 2^{22}R + 1$ with $R$ odd. Then $\gcd(R, 2^{22}) = 1$, and the only prime dividing $F$ is $p = 2$. From the congruence $a^{(N-1)/2} \equiv -1 \pmod{N}$, squaring both sides yields the Fermat condition $a^{N-1} \equiv 1 \pmod{N}$. Moreover, for the unique prime divisor $p = 2$ of $F$, we have $a^{(N-1)/2} - 1 \equiv -2 \pmod{N}$, so
\[
\gcd\bigl(a^{(N-1)/2} - 1,\, N\bigr) = \gcd(-2, N) = 1
\]
because $N = 2^{22}R + 1$ is odd. The size threshold of Lemma 1 is
\[
2F^3 = 2\cdot (2^{22})^3 = 2^{67} = 147573952589676412928 > 10^{20},
\]
so Lemma 1 applies directly to establish Theorem 1.

For Lemma 2 (\texttt{Paper.\allowbreak lemma2}), if $N = 10k + 3$ is prime, then $N$ is odd and $N \equiv 3 \pmod{5}$. Since $5 \equiv 1 \pmod{4}$, quadratic reciprocity and Euler's criterion give
\[
5^{(N-1)/2} \equiv \left(\frac{5}{N}\right) = \left(\frac{N}{5}\right) = \left(\frac{3}{5}\right) = -1 \pmod{N}.
\]
Theorem 2 is Theorem 1 at $a = 5$. Lemma 2 shows that the hypothesis on $5$ holds for every prime $N \equiv 3 \pmod{10}$, so the test rejects no prime of this class. The form \texttt{Thm2.\allowbreak theorem2\_\allowbreak if} keeps the hypothesis on $5$ and replaces $N < 10^{20}$ by $N < 2\cdot(2^{22})^3$, for the direction from the square test to primality.
\end{proof}

\subsection*{Deviation and Range Remark on the Final Prime}
We record one point regarding the range of Theorem 2 as stated on page 864 of \cite{Saouter1998}. The ending prime of Saouter's ladder is
\[
N = 100000000209366024193 > 10^{20},
\]
so it lies outside the range $N < 10^{20}$ stated in Theorem 2, as it must in order for the ladder to cross $10^{20}$. However, it lies well below the Lemma 1 bound
\[
2\cdot (2^{22})^3 = 2^{67} = 147573952589676412928,
\]
so the primality criterion still applies. In Lean, \texttt{Thm2.\allowbreak last\_\allowbreak prime} uses the wider form \texttt{Thm2.\allowbreak theorem2\_\allowbreak if} with hypothesis $N < 2\cdot (2^{22})^3$. Specifically, for $N = 100000000209366024193$, the parameters are
\begin{align*}
R &= 23841857960073,\\
s &= 2842170,\\
r &= 7960713,\\
r^2 - 8s &= 63372928731009,
\end{align*}
and $r^2 - 8s = 63372928731009$ is not a square since it lies strictly between $7960711^2$ and $7960712^2$.

\begin{thmD}
All 100 rungs $N(k)$ from Table 1 of \cite{Saouter1998}, together with the starting prime $138412033$ and the ending prime $100000000209366024193$, are checked prime in the Lean kernel by the criterion of Theorem 2 using one modular power each. Among the 100 rungs of Table 1, 11 have $s = 1$ and the rest have $s = 0$, by script. The 100 Table 1 rungs begin at $138412033$, are strictly rising, and have every consecutive step strictly below $4\cdot 10^{11}$, with largest step $399968829440 = 95360\cdot 2^{22}$ by script. The Lean names are \texttt{Table1Thm2.\allowbreak table1\_\allowbreak prime\_\allowbreak thm2}, \texttt{Thm2.\allowbreak first\_\allowbreak prime}, \texttt{Thm2.\allowbreak last\_\allowbreak prime}, \texttt{Table1.\allowbreak table1\_\allowbreak head}, and \texttt{Table1.\allowbreak table1\_\allowbreak gaps}.
\end{thmD}

\begin{proof}
Each rung is checked in the Lean kernel via \texttt{decide +kernel} applied to Theorem 2 (\texttt{Table1Thm2.\allowbreak table1\_\allowbreak prime\_\allowbreak thm2}, \texttt{Thm2.\allowbreak first\_\allowbreak prime}, and \texttt{Thm2.\allowbreak last\_\allowbreak prime}), and the ordering and step bounds on the 100 rungs are checked directly in \texttt{Table1.\allowbreak table1\_\allowbreak head} and \texttt{Table1.\allowbreak table1\_\allowbreak gaps}.
\end{proof}

\section{The 25-Rung Proth Ladder to $10^{20}$}

Separately from the verification of Saouter's criteria and Table 1, we construct a 25-rung ladder of Proth primes that derives the ternary Goldbach range up to $10^{20}$ from the published even Goldbach range $4\cdot 10^{18}$.

\begin{thmE}
Assuming every even integer from $4$ to $4\cdot 10^{18}$ is a sum of two primes, every odd integer from $7$ to $10^{20}$ is a sum of three primes. The Lean statement \texttt{ProthLadder.\allowbreak ternaryGoldbachUpTo\_\allowbreak 1e20\_\allowbreak of\_\allowbreak even} proves \texttt{EvenGoldbachUpTo (4 * 10 \textasciicircum{} 18)} $\to$ \texttt{TernaryGoldbachUpTo (10 \textasciicircum{} 20)}, where the hypothesis \texttt{EvenGoldbachUpTo (4 * 10 \textasciicircum{} 18)} is passed as an explicit argument, never declared as an axiom, and it is not proved here.
\end{thmE}

\begin{proof}
We check the ladder primes by Proth's theorem (\texttt{Proth.\allowbreak proth}): if $0 < k < 2^{m+1}$, $N = k\cdot 2^{m+1} + 1$, and there is a natural number $a$ such that
\[
a^{k\cdot 2^m} \equiv -1 \pmod{N},
\]
then $N$ is prime.

We take $m + 1 = 34$, so each of the 25 rungs has the form
\[
N = k\cdot 2^{34} + 1
\]
with $0 < k < 2^{34}$ and witness base $a$ as listed in Table~\ref{tab:proth-rungs}. The starting rung in Table~\ref{tab:proth-rungs} is
\[
3999998442578378753 = 232830553\cdot 2^{34} + 1,
\]
and the ending rung is
\[
99999983948045221889 = 5820765157\cdot 2^{34} + 1.
\]

\begin{table}[htbp]
\centering
\small
\caption{The 25 Proth prime rungs $N = k\cdot 2^{34} + 1$ and witness bases $a$ for Theorem E.}
\label{tab:proth-rungs}
\begin{tabular}{@{}rr@{\hspace{2.5em}}rr@{}}
\toprule
$k$ & $a$ & $k$ & $a$ \\
\midrule
$232830553$  & $3$  & $3259628295$ & $13$ \\
$465661177$  & $3$  & $3492458899$ & $3$  \\
$698491779$  & $5$  & $3725289523$ & $3$  \\
$931322415$  & $7$  & $3958120159$ & $3$  \\
$1164153045$ & $7$  & $4190950765$ & $3$  \\
$1396983685$ & $3$  & $4423781383$ & $3$  \\
$1629814317$ & $11$ & $4656612025$ & $3$  \\
$1862644839$ & $5$  & $4889442663$ & $5$  \\
$2095475355$ & $7$  & $5122273297$ & $3$  \\
$2328305925$ & $7$  & $5355103933$ & $3$  \\
$2561136565$ & $3$  & $5587934515$ & $3$  \\
$2793967113$ & $5$  & $5820765157$ & $3$  \\
$3026797689$ & $5$  &              &      \\
\bottomrule
\end{tabular}
\end{table}

Let $B = 4\cdot 10^{18}$. In Lean, the chain relation (\texttt{Ladder.\allowbreak Step2}, checked for our sequence in \texttt{ProthLadder.\allowbreak rungs\_\allowbreak chain}) checks that, starting from $3$ followed by the 25 rungs, each step strictly rises and has difference at most $B - 2$, with largest step
\[
3999999971586736128.
\]
The reach lemma (\texttt{ProthLadder.\allowbreak rungs\_\allowbreak reach}) checks that the ending rung plus $B = 4\cdot 10^{18}$ satisfies
\[
99999983948045221889 + 4\cdot 10^{18} = 103999983948045221889 \ge 10^{20}.
\]
The single-interval covering step (\texttt{Ladder.\allowbreak ternary\_\allowbreak step}) establishes that if $p$ is an odd prime, $n$ is odd, and
\[
p + 4 \le n \le p + B,
\]
then $n - p$ is even and satisfies $4 \le n - p \le B$; by \texttt{EvenGoldbachUpTo B}, $n - p$ is a sum of two primes, so $n = p + (n - p)$ is a sum of three primes. Since each consecutive step in the chain is at most $B - 2$, and since $B$ is even and $p$ is odd, $p + B$ is odd, and $p' + 4 \le p + B + 2$, so the odd integers covered from $p'$ continue directly after those covered from $p$. Induction along the chain (\texttt{Ladder.\allowbreak ternary\_\allowbreak of\_\allowbreak ladder2}), starting at $p = 3$ (which covers odd $n$ from $3 + 4 = 7$ to $3 + B$), therefore covers every odd integer $n$ from $7$ to $10^{20}$.
\end{proof}

\subsection*{Sanity Instance and Rung Count Comparison}
To confirm that the definitions and ladder induction have no hidden vacuity, the formalization includes a sanity instance with no hypothesis (\texttt{ProthLadder.\allowbreak ternaryGoldbachUpTo\_\allowbreak 293\_\allowbreak vacuity}): applying the exact same ladder lemma with $B = 100$ and prime rungs $97$ and $193$, where \texttt{ProthLadder.\allowbreak evenGoldbachUpTo\_\allowbreak 100} is proved directly in the kernel, yields \texttt{TernaryGoldbachUpTo 293} with nothing assumed.

The rung count comparison (with the second quotient in \texttt{Paper.\allowbreak rung\_\allowbreak count}) is:
\[
\frac{10^{20}}{4\cdot 10^{18}} = 25,
\qquad\text{against}\qquad
\frac{10^{20}}{4\cdot 10^{11}} = 250\cdot 10^6
\quad\text{in Saouter \cite{Saouter1998}.}
\]
This saving comes entirely from the larger even Goldbach input $4\cdot 10^{18}$, which is the published computation of Oliveira e Silva, Herzog, and Pardi \cite{OSP2014}, and not from any new idea. The ladder structure is Saouter's \cite{Saouter1998} and the use of Proth primes is that of Helfgott and Platt \cite{HelfgottPlatt2013}, Section 3.

\section{Cited Input, Verification Status, and Data Availability}

\subsection{Differences from the source}
We list the differences between the Lean formalization and \cite{Saouter1998}:
\begin{enumerate}
\item[\textup{(a)}] the constant on page 865, read as in Proposition A;
\item[\textup{(b)}] the last prime, as in the remark on the final prime;
\item[\textup{(c)}] Lean states the base as a natural number and as an integer, the paper as an integer;
\item[\textup{(d)}] the 25 rung ladder starts at $3$ and uses steps at most $B - 2$, the paper starts at $p_0$ and asks steps below $4\cdot 10^{11}$;
\item[\textup{(e)}] Lemma 2 is stated in \texttt{ZMod p}.
\end{enumerate}
The Section 3 sentence ``No other change'' means no other change to the formula. In addition, in Lean $s$ and $r$ are the natural number quotient and remainder of $R$ by $2F$; $(N-1)/2$ is natural division of $2^{22}R$ by $2$, exact since $2^{22}R$ is even; \texttt{IsSquare} is taken over the integers, so a negative $r^2 - 8s$ is not a square, matching ``not a perfect square''; and the case $F = 0$ of \texttt{BLS.\allowbreak lemma1} is empty since $N < 2F^3$ does not hold.

\subsection{Input Table}
There is one cited input in Theorem E, and none elsewhere in this note. Table~\ref{tab:input} records its bibliographic details, printed wording, normalization, and Lean representation. It is a computation, cited as such and never stated as proved.

\begin{table}[htbp]
\centering
\small
\caption{External cited input used in Theorem E (and nowhere else).}
\label{tab:input}
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.24\textwidth}>{\raggedright\arraybackslash}p{0.70\textwidth}@{}}
\toprule
Field & Specification \\
\midrule
Source & T. Oliveira e Silva, S. Herzog, and S. Pardi \cite{OSP2014}, \emph{Empirical verification of the even Goldbach conjecture and computation of prime gaps up to $4\cdot 10^{18}$}, Math. Comp. 83, no. 288, 2014, 2033 to 2060. \\
\addlinespace
Printed statement & Abstract, page 2033: the conjecture is ``confirmed to be true for all even numbers not larger than $4\cdot 10^{18}$''. \\
\addlinespace
Normalization & Inclusive at $4\cdot 10^{18}$, for all even integers $n$ with $n \ge 4$. \\
\addlinespace
Lean form & \texttt{EvenGoldbachUpTo N}, defined as: for all $n$, \texttt{Even n}, $4 \le n$, $n \le N$, \texttt{IsGoldbachSum n}, instantiated at $N = \texttt{4 * 10 \textasciicircum{} 18}$. \\
\addlinespace
Role in Lean & Explicit hypothesis in \texttt{ProthLadder.\allowbreak ternaryGoldbachUpTo\_\allowbreak 1e20\_\allowbreak of\_\allowbreak even}; never an axiom. \\
\bottomrule
\end{tabular}
\end{table}

\subsection{Verification Status Table}
Every claim in this note is classified into one of four categories: \textbf{Kernel} (checked by the Lean 4 kernel), \textbf{Script} (checked by external script and not used in any Lean proof), \textbf{Hand} (a statement checked by hand in this note and not in Lean), or \textbf{Cited} (external published computation). Table~\ref{tab:status} gives the mapping.

\begin{table}[htbp]
\centering
\small
\caption{Verification status of all claims and components (categories: Kernel, Script, Hand, Cited).}
\label{tab:status}
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.42\textwidth}>{\raggedright\arraybackslash}p{0.38\textwidth}>{\raggedright\arraybackslash}p{0.12\textwidth}@{}}
\toprule
Claim or Component & Lean Module / Identifier or Reference & Status \\
\midrule
Proposition A: identities for $N(k)$ and $N'(k)$, $N(3) = 138412033$, $N(2384185796007) = 100000000209366024193$, that $N'(3)$ is composite, $N'(k)\bmod 2^{22} \ne 1$, $N(k) - N'(k) = 11324700$ & \texttt{Paper}, \texttt{Table1.\allowbreak printed\_\allowbreak three\_\allowbreak composite} & Kernel \\
\addlinespace
Proposition A: leastness of $p_0 = 138412033$ (text, not used in proofs); count that 9 of 100 values $N'(k)$ are prime; rerun of Saouter's algorithm from $138412033$ reproducing Table 1; largest Table 1 step $399968829440 = 95360\cdot 2^{22}$; count that 11 of the 100 Table 1 rungs have $s = 1$ & External check scripts & Script \\
\addlinespace
Theorem B: Saouter's Lemma 1 for every even $F$ & \texttt{BLS.\allowbreak lemma1} & Kernel \\
\addlinespace
Theorem C: Saouter's Theorem 1 (natural and integer base), Lemma 2, and Theorem 2 (both directions and $N < 2\cdot(2^{22})^3$ form) & \texttt{Thm1.\allowbreak theorem1}, \texttt{Thm1.\allowbreak theorem1\_\allowbreak int}, \texttt{Paper.\allowbreak lemma2}, \texttt{Thm2.\allowbreak theorem2}, \texttt{Thm2.\allowbreak theorem2\_\allowbreak if} & Kernel \\
\addlinespace
Theorem D: primality of all 100 Table 1 rungs, starting prime $138412033$, and ending prime $100000000209366024193$; ordering and step bound below $4\cdot 10^{11}$ & \texttt{Table1Thm2.\allowbreak table1\_\allowbreak prime\_\allowbreak thm2}, \texttt{Thm2.\allowbreak first\_\allowbreak prime}, \texttt{Thm2.\allowbreak last\_\allowbreak prime}, \texttt{Table1.\allowbreak table1\_\allowbreak head}, \texttt{Table1.\allowbreak table1\_\allowbreak gaps} & Kernel \\
\addlinespace
Theorem E: implication from $\texttt{EvenGoldbachUpTo (4 * 10 \textasciicircum{} 18)}$ to $\texttt{TernaryGoldbachUpTo (10 \textasciicircum{} 20)}$, Proth criterion, 25 rungs, chain, reach, ladder step, induction, sanity check to $293$, and $10^{20}/(4\cdot 10^{11}) = 250\cdot 10^6$ & \texttt{ProthLadder.\allowbreak ternaryGoldbachUpTo\_\allowbreak 1e20\_\allowbreak of\_\allowbreak even}, \texttt{Proth.\allowbreak proth}, \texttt{Ladder.\allowbreak Step2}, \texttt{ProthLadder.\allowbreak rungs\_\allowbreak chain}, \texttt{ProthLadder.\allowbreak rungs\_\allowbreak reach}, \texttt{Ladder.\allowbreak ternary\_\allowbreak step}, \texttt{Ladder.\allowbreak ternary\_\allowbreak of\_\allowbreak ladder2}, \texttt{ProthLadder.\allowbreak ternaryGoldbachUpTo\_\allowbreak 293\_\allowbreak vacuity}, \texttt{ProthLadder.\allowbreak evenGoldbachUpTo\_\allowbreak 100}, \texttt{Paper.\allowbreak rung\_\allowbreak count} & Kernel \\
\addlinespace
$12582913 = 7\cdot 1797559$, by multiplication; $N'(3) = 19\cdot 6688807$; $10^{20}/(4\cdot 10^{18}) = 25$ & Checked by hand in this note & Hand \\
\addlinespace
Even Goldbach verification up to $4\cdot 10^{18}$ (hypothesis of Theorem E) & Oliveira e Silva, Herzog, and Pardi \cite{OSP2014} & Cited \\
\addlinespace
Saouter's full ladder of about $250\cdot 10^6$ rungs (with Sinisalo's $4\cdot 10^{11}$ input \cite{Sinisalo1993}); Helfgott and Platt's verification to $8.875\cdot 10^{30}$ \cite{HelfgottPlatt2013}; Helfgott's ternary Goldbach theorem \cite{Helfgott2013} & \cite{Saouter1998}, \cite{Sinisalo1993}, \cite{HelfgottPlatt2013}, \cite{Helfgott2013} (not reverified) & Cited \\
\bottomrule
\end{tabular}
\end{table}

The proofs printed in this note are written for the reader; the Lean proofs are the check.

\subsection{Data Availability and Build Reproduction}
All Lean names in this note are under the namespace \texttt{GoldbachLean.\allowbreak Saouter1998}. The Lean 4 formalization is publicly available under the Apache-2.0 license:
\begin{itemize}
\item \textbf{Repository:} \url{https://github.com/sthubbar/goldbach-lean}
\item \textbf{Folder:} \texttt{entries/saouter1998}
\item \textbf{Full commit hash:} \texttt{39d1ce6db8b634233ed29c2aa3e3dcf1218400dc}
\item \textbf{Palomar Registry listing:} \texttt{PALOMAR-2026-11-02-000012} version 1, available at \url{https://palomar-registry.org/entry.html?id=PALOMAR-2026-11-02-000012&version=1} (note that Palomar is a listing and not peer review).
\item \textbf{Toolchain:} Lean and Mathlib \texttt{v4.35.0-rc3}.
\item \textbf{Build instruction:} Running \texttt{lake build} inside \texttt{entries/saouter1998} completes in $57\text{ s}$ in a cloud build with cached Mathlib.
\item \textbf{Audit file and foundations:} All main statements are collected and compared in \texttt{ChallengeSaouter1998.lean}, which exports 19 theorems. The proofs depend only on the Lean axioms \texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.sound}. Every finite primality and arithmetic check uses \texttt{decide +kernel} and never \texttt{native\_decide}; each rung verification costs one modular power on numbers below $2^{67}$.
\end{itemize}

\medskip
\noindent
Steve Hubbard designed the research program and directed this work. AI tools, Claude, Codex, Gemini and Antigravity, were used to write the Lean code and draft the text. AI agents also did the checks of the Lean against the source, and no human expert has reviewed the mathematics. The author takes full responsibility for the content.

\begin{thebibliography}{9}

\bibitem{BLS1975}
J. Brillhart, D. H. Lehmer, and J. L. Selfridge,
\emph{New primality criteria and factorizations of $2^m \pm 1$},
Math. Comp. \textbf{29} (1975), no. 130, 620--647.

\bibitem{Helfgott2013}
H. A. Helfgott,
\emph{The ternary Goldbach conjecture is true},
\texttt{arXiv:1312.7748}, 2013.

\bibitem{HelfgottPlatt2013}
H. A. Helfgott and D. J. Platt,
\emph{Numerical verification of the ternary Goldbach conjecture up to $8.875\cdot 10^{30}$},
Exp. Math. \textbf{22} (2013), 406--409.

\bibitem{OSP2014}
T. Oliveira e Silva, S. Herzog, and S. Pardi,
\emph{Empirical verification of the even Goldbach conjecture and computation of prime gaps up to $4\cdot 10^{18}$},
Math. Comp. \textbf{83} (2014), no. 288, 2033--2060.

\bibitem{RamareSaouter2003}
O. Ramar\'e and Y. Saouter,
\emph{Short effective intervals containing primes},
J. Number Theory \textbf{98} (2003), 10--33.

\bibitem{Saouter1998}
Y. Saouter,
\emph{Checking the odd Goldbach conjecture up to $10^{20}$},
Math. Comp. \textbf{67} (1998), no. 222, 863--866, \texttt{doi:10.1090/S0025-5718-98-00928-4}.

\bibitem{Sinisalo1993}
M. K. Sinisalo,
\emph{Checking the Goldbach conjecture up to $4\cdot 10^{11}$},
Math. Comp. \textbf{61} (1993), no. 204, 931--934.

\end{thebibliography}

\end{document}