%======================================================================
\section{Certified numerics}\label{s:numerics}

The proof uses numerical constants in three ways: the threshold $\Kstar=377.38$ and the explicit string tension of the second
assertion; the value $\vCb=(-\Delta_{\mathbb Z^3})^{-1}(0,0)$ of the lattice Green's function at the origin, half of Watson's integral; and the many inequalities between constants in the
supplement of [U1] and in the written-out proofs. We certify all of them in Lean, in \lean{U1/Numerics/} or, for some claims of the written-out proofs, where they are used; \S\ref{s:appE} uses the same method for the sign conditions
of Theorem E.8.

\subsection{The threshold}
Lemma 2.6 bounds the density $\delta=e^{-c_\delta(K)\beta}$ of frozen plaquettes through a saddle-point exponent
$c_\delta^{\mathrm{sp}}(K)$, and the Peierls estimate of Section 5 needs $c_\delta(K)/(2K)>6\pi^2\vCb=14.96613\ldots$; the
number $14.9662$ below is this value rounded up. We certify the values of $c_\delta^{\mathrm{sp}}(K)/(2K)$ quoted in Lemma 2.6 through a
parametrization $K=e^t/(2t)$, rational brackets for the saddle point and Taylor bounds on $\exp$ checked by \lean{norm\_num}.
In particular $c_\delta^{\mathrm{sp}}(K)/(2K)\ge14.9663$ for $K\ge377.38$, and the root of $c_\delta^{\mathrm{sp}}(K)/(2K)=14.9662$ is
unique and lies in $[377.36345,377.36355]$. In the proof of the qualitative assertion, $\Kstar$ enters only through the contour bound, which the library proves
for every $K>\Kstar$.

\subsection{Watson's integral}
The bounds
\[
0.2527310098586\le\vCb\le0.2527310098631
\]
reduce to two inequalities between rational numbers, one for each bound, each built from a head of the series expansion of
$\vCb$ and a bound on its tail. Both
are decided by the kernel (\lean{decide +kernel}), which adds no axiom; the resulting theorem is \lean{U1.Numerics.vCb0\_bounds}, and it gives
$2.494355087\le\pi^2\vCb\le2.494355088$ (\lean{U1.Numerics.pi\_sq\_vCb0\_bounds}). The explicit string tension and the
statements for large $\beta$ use these bounds.

\subsection{The symbolic constants}
The paper leaves some constants symbolic, among them the parameters $\mu$ and $\kappa_S$ of
Sections 6 and 7 (item 12 of [U1, S1.1.1]) and the Pauli--Villars parameter $\lambda_{\mathrm{PV}}$ (item 13), and states the conditions
they must satisfy. In the formal
proof we fix them, together with the parameter $C$ of Theorem 6.5 (not the loop $C$):
\[
C=\tfrac14,\qquad\mu=4401,\qquad\kappa_S=7,\qquad\lambda_{\mathrm{PV}}=\lambda_\star(\kappa_S,\mu):=e^{-(\kappa_S+\mu/2+6)}=e^{-2213.5},
\]
and take $\theta_0=\frac1{100}$, $\eta_H=0.62$, $p_4=15$ and $c_\lambda=\frac1{24}$ from the paper. We choose the constants in an
order in which each condition concerns only constants already chosen: the absolute constants and the heat-kernel constants;
then $c_{10}=\frac79r_C$, with $r_C=\kappa_0/2\approx2.8\cdot10^{-183}$, and $c''_{10}=2200$, which is certified admissible (the
least admissible value is about $2137.3$); then $\mu=1+2c''_{10}$; then $\kappa_S$; then $\lambda_{\mathrm{PV}}$; and finally
$\beta$ large. This order is not circular, because no condition bounds $\mu$ or $\kappa_S$ from above, and $c''_{10}$ involves none
of $\mu$, $\kappa_S$, $\lambda_{\mathrm{PV}}$ and $\beta$. Each condition has a certificate in \lean{U1/Numerics/}, most of them in \lean{U1/Numerics/StageC/};
for example, \lean{c10pp\_certificate} certifies the condition of Lemma A.6 on $c''_{10}$, which with $\mu=1+2c''_{10}$
gives that of Proposition B.7, and \lean{T730\_global} certifies condition (7.30), which is the binding condition on $\kappa_S$.

\subsection{The constants of the written-out proofs}
In the six written-out proofs of Sections 6 and 7 and their appendices,
every numerical claim is inventoried with its location, its kind (arithmetic, parametric over a stated range, definitional or analytic)
and whether it holds as written. The arithmetic and parametric claims, except the two figures of a numerical experiment
described below, are also checked independently in 50-digit arithmetic. Lean lemmas in \lean{U1/Numerics/StageC/} certify $563$
claims, among them $96$ of the $98$ arithmetic and $465$ of the $516$ parametric ones; the other parametric and analytic
claims are proved where they are used, and the two remaining arithmetic claims, figures of a numerical experiment reported in a
remark, are checked against its recorded run. Of the $1677$ claims,
nine fail as written: seven roundings in the last digits, one wrong digit and one equality that holds only as an inequality.
Six more cannot be checked from the documents alone. All fifteen are corrected or resolved in the documents, without changing any conclusion. The inventory, with the status of each claim and the lemma
that certifies it where there is one, is the file \lean{U1/Numerics/StageC/CLAIMS.md} of the archive.