%======================================================================
\section{The Lean statements}\label{s:statement}

The results of [U1] that we formalize are stated by the following theorems. We then give the main definitions in Lean
syntax, with mathematical symbols for readability. All names are in the namespace \lean{U1}.

\begin{theorem}[formal]\label{thm:formal}
The seventeen theorems of Table~\ref{tab:formal} take no hypotheses, and for each of them \lean{\#print axioms} lists
\lean{propext}, \lean{Classical.choice} and \lean{Quot.sound} and nothing else. They formalize the two assertions of
Theorem~\ref{thm:main}, the infinite-volume form of the area law ([U1, Remark 8.1]), Corollaries 1.3 and 1.4 of [U1],
each in a form relative to the area law of the $U(1)$ model and in a weaker form, Fr\"ohlich's comparison (Proposition 9.1) and the eight results of
[U1, Appendix~E]; the seventeenth, \lean{setting\_realized}, checks the definition of the realized weights of
Proposition E.6.
\end{theorem}

\begin{table}[ht]
\centering\small
\begin{tabular}{lll}
\toprule
{[U1]} & statement & theorem\\
\midrule
Theorem 1.2, first assertion & \lean{AreaLaw} & \lean{Main.thm\_1\_2}\\
Theorem 1.2, second assertion & \lean{AreaLawExplicit} & \lean{Main.thm\_1\_2\_explicit}\\
Remark 8.1 & & \lean{Main.rem\_8\_1}\\
Corollary 1.3, relative form & \lean{Cor13} & \lean{Main.cor\_1\_3\_rel}\\
Corollary 1.3, weaker form & & \lean{Main.cor\_1\_3}\\
Corollary 1.4, relative form & \lean{Cor14} & \lean{Main.cor\_1\_4\_rel}\\
Corollary 1.4, weaker form & & \lean{Main.cor\_1\_4}\\
Proposition 9.1 & \lean{Prop91} & \lean{Main.prop\_9\_1}\\
Lemma E.1 & \lean{LemmaE1} & \lean{lem\_E\_1}\\
Theorem E.2 & \lean{TheoremE2} & \lean{thm\_E\_2}\\
Lemma E.3 & \lean{LemmaE3} & \lean{lem\_E\_3}\\
Corollary E.4 & \lean{CorollaryE4} & \lean{cor\_E\_4}\\
Proposition E.6 & \lean{PropositionE6} & \lean{prop\_E\_6}\\
Theorem E.8 & \lean{TheoremE8} & \lean{thm\_E\_8}\\
Proposition E.10 & \lean{PropositionE10} & \lean{prop\_E\_10}\\
Proposition E.12 & \lean{PropositionE12} & \lean{prop\_E\_12}\\
realized weights of Proposition E.6 & \lean{RealizedWeightSpec} & \lean{setting\_realized}\\
\bottomrule
\end{tabular}
\caption{The seventeen theorems of Theorem~\ref{thm:formal} and the statements they prove. The names of the first eight
rows are in the namespace \lean{U1} (theorems in \lean{U1/MainTheorem.lean}), those of the last nine in
\lean{U1.AppendixE} (statements in \lean{U1/AppendixE/Statements.lean}, theorems in
\lean{U1/AppendixEMain.lean}).}\label{tab:formal}
\end{table}

\paragraph{Lattice and model.} Sites are points of $\mathbb Z^3$. Bonds, plaquettes and cubes carry their orientations and
incidence numbers, and the boundary maps satisfy $\partial\partial=0$ (\lean{bd1\_bd2}). A box is a product of three integer
intervals; \lean{Box.complex} is the finite $2$-complex of its bonds and plaquettes. The angle group is
$\mathbb T=\mathbb R/2\pi\mathbb Z$. On $\mathbb T^E$, with $E$ the set of bonds of a finite complex, \lean{FinComplex.wilsonExp} is the expectation for the probability measure
proportional to $\prod_p e^{\beta\cos\theta_p}\,d\theta$, and the expectation of a constant is that constant (\lean{wilsonExp\_const}).
The Villain measure at coupling $t$ has the Villain weight $\tilde v_t(\theta_p)$ in place of $e^{\beta\cos\theta_p}$, where
$\tilde v_t(\theta)=\sum_{n\in\mathbb Z}e^{-n^2/(2t)}e^{in\theta}=(2\pi t)^{1/2}\sum_{m\in\mathbb Z}e^{-t(\theta-2\pi m)^2/2}$.
A rectangle \lean{C : Rect} lies in a coordinate plane and has sides \lean{C.R}, \lean{C.T}; the loop that [U1] calls $C$, its
boundary, is \lean{C.chain},
traversed first along the side of length \lean{C.R} (\lean{Rect.chain\_eq\_loop}). For a box \lean{B : Box} (the box $\Lambda$ of [U1]), the predicate \lean{C.InBox B} says
$\Lambda\supseteq C$. Then \lean{B.wilsonLoop \(\beta\) C.chain} is $\langle\cos\theta_C\rangle^W_{\Lambda,\beta}$ with free boundary
conditions.

In Lean, the first assertion of Theorem~\ref{thm:main} reads

\begin{alltt}
def AreaLawAt (\(\beta\) \(\sigma\) : \(\mathbb{R}\)) (R\(\sb1\) : \(\mathbb{N}\)) (c : \(\mathbb{R}\)) : Prop :=
  \(\forall\) C : Rect, R\(\sb1\) \(\le\) C.R \(\to\) R\(\sb1\) \(\le\) C.T \(\to\) \(\forall\) B : Box, C.InBox B \(\to\)
    B.wilsonLoop \(\beta\) C.chain \(\le\) Real.exp (-\(\sigma\) * C.R * C.T + c * (C.R + C.T))

def AreaLaw : Prop :=
  \(\exists\) c : \(\mathbb{R}\), \(\forall\) \(\beta\) : \(\mathbb{R}\), 0 < \(\beta\) \(\to\) \(\exists\) \(\sigma\) : \(\mathbb{R}\), 0 < \(\sigma\) \(\wedge\) \(\exists\) R\(\sb1\) : \(\mathbb{N}\), AreaLawAt \(\beta\) \(\sigma\) R\(\sb1\) c
\end{alltt}

and the second reads

\begin{alltt}
def AreaLawExplicit : Prop :=
  \(\exists\) c : \(\mathbb{R}\), \(\forall\) K : \(\mathbb{R}\), Kstar < K \(\to\) \(\exists\) \(\beta\sb0\) : \(\mathbb{R}\), 0 < \(\beta\sb0\) \(\wedge\)
    \(\exists\) \(\sigma\) : \(\mathbb{R}\) \(\to\) \(\mathbb{R}\), \(\exists\) R\(\sb1\) : \(\mathbb{R}\) \(\to\) \(\mathbb{N}\),
    (\(\forall\) \(\beta\), \(\beta\sb0\) \(\le\) \(\beta\) \(\to\)
      1.35e-4 * (1/4) * 1.6e-19 * (K * \(\beta\)) ^ (-(1:\(\mathbb{R}\))/2)
        * Real.exp (-2.49436 * (K * \(\beta\))) \(\le\) \(\sigma\) \(\beta\)) \(\wedge\)
    \(\forall\) \(\beta\), 0 < \(\beta\) \(\to\) AreaLawAt \(\beta\) (\(\sigma\) (max \(\beta\) \(\beta\sb0\))) (R\(\sb1\) (max \(\beta\) \(\beta\sb0\))) c
\end{alltt}

with \lean{Kstar} $=377.38$. We compare these statements with [U1]. In the order of the quantifiers, the perimeter constant
$c$ comes before $\beta$, and before $K$ in the second assertion, as in [U1]. For the first assertion alone this is no
restriction, as [U1] notes after Theorem 1.2: a constant $c$ that depends on $\beta$ can be replaced by $c=0$ if $\sigma$ is
halved and $R_1$ is enlarged. In the second assertion it is a restriction, since there halving $\sigma$ would also halve the explicit lower bound on the
string tension. The statements are also
uniform in the box, since \lean{AreaLawAt} quantifies over all rectangles with
$\min(R,T)\ge R_1$ and all boxes that contain them, with free boundary conditions, so no infinite-volume limit and no other boundary
condition enters the statement. In the explicit string tension, the constants are those of [U1, Theorem 1.2] with
$c_g=\frac14$ and $c_L=1.6\cdot10^{-19}$ substituted, and for $\beta<\beta_0(K)$ the bound holds with the values chosen at
$\beta_0(K)$, as in Theorem~\ref{thm:main}. Finally, as in [U1], the second assertion implies the first with the same $c$;
\lean{AreaLawExplicit.toAreaLaw} proves this with $K=378$.

For the corollaries, \lean{U1.Cor13} states Corollary 1.3 relative to the area law: for every closed subgroup
$G\subseteq U(n)$ that contains the scalars and every $\beta>0$, the area law of the $U(1)$ model at coupling $2n\beta$ with
constants $(\sigma,R_1,c)$ implies $|\langle\mathrm{Tr}\,U_C\rangle|\le2n\exp(-\sigma RT+c(R+T))$ for the $G$ model at $\beta$. The
Higgs field $\varphi$ may take values in any probability space, enters through a homomorphism $\rho$ of $G$ that is trivial on the scalars,
and has any nonnegative integrable weight $h$ with positive integral. Similarly, \lean{U1.Cor14} states Corollary 1.4: in every finite box
the $SU(2)$ model with a unit adjoint Higgs field converges, as the hopping coupling $\kappa\to\infty$, to the $U(1)$ Wilson
model in the sense of expectations of continuous gauge-invariant functions (Proposition 9.3), and the area law of the $U(1)$
model at $\beta$ with constants $(\sigma,R_1,c)$ gives the same area law for the limits of the Wilson loops of the $SU(2)$
model (Corollary 9.4). With \lean{thm\_1\_2}, \lean{Cor13} gives Corollary 1.3 with the constants
$\sigma(2n\beta)$, $R_1(2n\beta)$ and $c$, which depend on $G$ only through $n$, and \lean{Cor14} gives Corollary 1.4 with
the constants $\sigma(\beta)$, $R_1(\beta)$ and $c$. \lean{Cor13.of\_areaLaw} and
\lean{Cor14.of\_areaLaw} combine \lean{Cor13} and \lean{Cor14} with \lean{AreaLaw} into the weaker forms
\lean{Main.cor\_1\_3}, in which $\sigma$ and $R_1$ are chosen after $G$, and \lean{Main.cor\_1\_4}, in which the limit
model has an area law with its own $\sigma$ and $R_1$, not necessarily those of the $U(1)$ model.

The following formal statements are more general than those of [U1], but the paper's proofs cover them.
\begin{itemize}
\item \lean{U1.Prop91} includes the Higgs weight of Corollary 9.2. It holds, as Proposition 9.1 does, on every finite
$2$-complex whose plaquettes are attached along closed edge paths and for every closed edge path $\ell$, and it allows every
Higgs weight $h$ that \lean{U1.Cor13} allows. With weight $1$ it is Proposition 9.1, and on a box it is the first assertion of Corollary 9.2, which [U1]
states on boxes only.
\item In Corollaries 1.3 and 9.2 the map $\rho$ is any group homomorphism trivial on the scalars, whereas the paper has a
representation, and only the composite $(U,\varphi)\mapsto h((\rho(U_e))_e,\varphi)$ needs to be measurable and integrable. The
paper's proof uses only $\rho(zU)=\rho(U)$ for scalar $z$.
\end{itemize}

\paragraph{Appendix E.} Each of the eight results of [U1, Appendix~E] is a closed proposition in
\lean{U1/AppendixE/Statements.lean}. The statements are typed on objects of Section~2 of [U1] that the main formalization defines: finite
$2$-complexes, the Villain weights $\tilde v_t$, the Wilson expectation, the frozen expectation and the Bessel functions
$I_\nu$. The setting of the appendix is defined on top of them: the Fourier coefficients $c_k(w)$ for normalized Haar measure
on $\mathbb T$, plaquette weights, weights of Ginibre type, Villain mixtures with couplings at most $\tau$, the Gibbs
expectations $\langle\cdot\rangle_{X,w}$, the dual sums $\hat Z(n)$ of [U1, Lemma E.1], realized weights, and the boundary of
the unit cube with its outward normals. The following conventions differ from the statements in [U1] without adding hypotheses, and those on $\tau$ and on the face $p_0$ make some
statements slightly stronger. The coupling bound $\tau$ of a Villain mixture may be any real number. For $\tau<0$ there is no Villain mixture,
and for $\tau=0$ the bounds $e^{-\kappa k^2/(2\tau)}$ of Theorem E.2(a), with $\kappa>0$ determined by the complex and the
loop, read $e^0=1$, since division by zero gives $0$ in Lean. Theorem E.8 and Proposition E.12 hold at every face $p_0$ of the
cube, whereas the paper fixes one. Theorem E.8 does not assume $t>0$, since the condition $e^{-1/(2t)}=15/16$ forces it. In Proposition E.6 the weights
of Ginibre type are the normalized exponentials $e^f/\int e^f\,d\varphi/2\pi$ with $f=\sum_{j\le J}\lambda_j\cos j\varphi$, all $\lambda_j\ge0$, and one
cutoff $J$ for all plaquettes; every finite family of plaquette weights of Ginibre type has this form
(\lean{exists\_ginibreWeight\_family}). \S\ref{s:appE} maps the statements to the paper.

The audit of the main results (\S\ref{s:audits}) checks these statements against those of [U1]. Besides the comparison, the audit checks that no statement is true for a
definitional reason: the expectations are normalized and take no junk values, such as the value $0$ that Lean gives to a division by zero, under the hypotheses of the statements. As the partition function is
positive (\lean{integral\_wilsonWeight\_pos}), no expectation degenerates. The statements involve only the definitions of the
models; in particular, no parameter of the proof, such as the constants $\lambda_{\mathrm{PV}}$, $\mu$ and $\kappa_S$ of \S\ref{s:numerics} or the construction, enters a
statement. Throughout the library, each Lean theorem that corresponds to a result of [U1] cites it by its number there, in its docstring.
Some Lean names use the number of the result's LaTeX label instead, for instance \lean{Thm761OfRegSpec} for Theorem 7.57
(label \lean{thm:7.61}); the file \lean{LABELS.tsv} of the archive lists the labels with the numbers the results carry in [U1]. The file
\lean{blueprint/BLUEPRINT.md} maps the definitions and results of [U1] that the statements, the chain and the interface
\lean{U1.R0} of \S\ref{s:arch} involve, among them those of Sections 2 and 9, to their Lean names, and \lean{blueprint/APPENDIX\_E.md} does the same for
Appendix~E.