%======================================================================
\section{The parts of the formal proof, by section of [U1]}\label{s:parts}

We follow the paper's sections. For each part we give the Lean directory, the main results and the points where the formal
proof differs from the paper's. The library has $887$ files and $221{,}290$ lines of Lean. More than half of it, $502$ files
and $122{,}175$ lines in \lean{U1/StageC/}, formalizes the two expansion stages of Sections 6--7 and their
appendices.

\subsection{Sections 2, 8 and 9: the comparison, the chain and the corollaries}
The lattice, the models and the expectations are defined in \lean{U1/Basic/} and \lean{U1/Model/}, and the statements of
Section 2 are in \lean{U1/Reduction/}, which also proves Propositions 2.9 and 2.10; the directories named next hold the
other proofs. Section 9 and the correlation inequalities of Section 2 (Theorem 2.1, Lemma 2.3)
are both in \lean{U1/Correlation/}; the inequalities are proved through positive kernels and the doubling map
$(a,b)\mapsto(a+b,a-b)$ on compact abelian groups. The modified Bessel functions of real order and the mixture of Hartman and Watson [HW74]
behind Lemma 2.2 are in \lean{U1/Special/}, together with the lattice Coulomb and Yukawa kernels. Lemma 2.4 and Theorem 2.5
are in \lean{U1/Annealed/}, the dual representation and the frozen limit (Lemmas 2.7, 2.8) in \lean{U1/Dual/}, and Lemma 2.6
and the threshold $\Kstar$ in \lean{U1/Numerics/}. Cubical chains on boxes, used for
Propositions 2.9 and 2.10 and in Section 5, are in \lean{U1/Cubical/}.

The chain of Section 8 and its infinite-volume form (Remark 8.1) are formalized in \lean{U1/Chain.lean}, and its variants
for the other main results and the later interfaces in the other files \lean{U1/Chain*.lean}. In Section 9, the comparison behind Proposition 9.1 says that, for any phases $\psi_p$, couplings
$|J'_p|\le J_p$ and every $\alpha$, the expectation of $\cos(\theta_\ell-\alpha)$ in the $U(1)$ model with weights
$e^{J'_p\cos(\theta_p-\psi_p)}$ is at most that of $\cos\theta_\ell$ in the model with weights $e^{J_p\cos\theta_p}$. The
formal proof checks the positivity behind it one plaquette at a time, so plaquettes with the same edge vector up to sign need not be
combined, as they are in [U1]. The proof of Proposition 9.1 gives the constants $n$ and $n\beta$, but
the Lean statement uses the constants $2n$ and $2n\beta$ of [U1], which follow by monotonicity in $\beta$. Proposition 9.3 uses a unitary gauge
chosen for each fixed Higgs configuration, so no measurable section is needed. The limit $\kappa\to\infty$ is a
concentration argument on $SU(2)$ that uses only the invariance of Haar measure, its full support and Fubini's theorem.

\subsection{Sections 3--4: the regularization}
In Lean, the construction of Section 3 is a function from frozen sets to slit domains (\lean{U1/Regularization/}, and
\lean{U1/Geometry/} for the geometry). The grid of the construction is a product of one-dimensional partitions, and its properties (G1)--(G5) follow
from one-dimensional facts in each direction. Both phases of the construction are iterations to a fixed point, with explicit
bounds on the number of steps. For its submodular cut functionals, the smallest minimizers are intersections of all minimizers. We formalize the analysis of
Section 4 for every grid that satisfies (G1)--(G5). The
isoperimetric bounds of Theorem 4.5 and Lemma 4.11 use the discrete Loomis--Whitney inequality [LW49, Theorem 2], which we
prove by slicing and the Cauchy--Schwarz inequality (\lean{U1/Geometry/LoomisWhitney.lean}). In the cut rule of
Definition 3.18, the selection of a fragmented pair is a parameter of the construction (the list of findings in [repo] has an entry on Definition 3.18:
any order fixed before $D$ works). Finally, \lean{U1.consMaps\_regSpec} proves Theorems 3.20 and 3.21 for every valid run of the construction.

\subsection{Section 5: the contour bound}\label{ss:mincut}
Theorem 5.1 is formalized in \lean{U1/MinCut/}, with its cubical lemmas in \lean{U1/Cubical/} and its counts of
lattice animals in \lean{U1/Trees/}. For the outputs of the construction it is proved by
\lean{U1.MinCut.thm\_5\_1\_of\_regSpec} in the form that the chain uses, the moment bound of (5.1). The proof of
\lean{U1.MinCut.thm\_5\_1} gives the tail bound of (5.1) with the sharper counting factor $2^{4|C|+2}$,
but the theorem is stated with the factor $2^{4|C|+5}$ of [U1]. We formalize the separators, the
Leaf Lemma, the charges and the classes of Subsections 5.4--5.6 for every selection of the cut rule.

\subsection{Section 6: Stage 1}
The first stage, a Mayer expansion to the Debye scale (\lean{U1/StageC/S6/}), controls the Debye-screened Coulomb gas on the
slit domain. The ingredients of this stage are the expansion with the forest formula and its coefficients, the screening mass, heat-kernel bounds on the slit
graph, the depletion estimates, and the Yukawa and Coulomb kernels of \lean{U1/Special/}. We state and prove the heat-kernel
bound (HK2) of Theorem 6.8 for the tail mass at a fixed time, a form implied by the exit-time form of [U1]. Appendix D, the only
place where (HK2) is applied, needs only this form.

\subsection{Section 7: Stage 2}
The second stage follows the paper's subsections.
\begin{itemize}
\item Subsections 7.0--7.5 and Appendix C (\lean{U1/StageC/S70/}): the expansion of G\"opfert and Mack [GM82, App.~E] on the slit
domain, walls and their tension, the collar, wall fields and classes, Proposition 7.22 and Theorem 7.27.
\item Subsection 7.6 and Appendix B (\lean{U1/StageC/S76/}): the bounds at a fixed configuration, with the per-cell form of
[BF80, (9.824)] (Proposition B.7).
\item Subsections 7.7--7.9 and Appendix A (\lean{U1/StageC/S77/}): the tree form of the activities, the link sum, the
Kirkwood--Salsburg system in the class algebra of [U1], a Beurling (weighted $\ell^1$) algebra, the proof that frozen flux costs area, and the deterministic area law
(Theorem 7.57).
\item The assembly described in \S\ref{s:arch}: \lean{U1/StageC/Assembly/}, and the position bound in
\lean{U1/StageC/Seed1/}.
\item Gaussian calculus (\lean{U1/Gaussian/}); tree-graph bounds, Kruskal's identity, the Beurling algebra and the polymer gas
(\lean{U1/Trees/}, \lean{U1/Cluster/}).
\end{itemize}

As an example of the analytic work, take Proposition 7.53, which shows that frozen flux costs area. The long wall fields are integer
fields on the bonds that vanish inside the cells of the expansion, are constant on each interface between cells and have
zero sum around every short closed walk; their classes $[N]$, the sums around closed walks, form a group
$\Gamma_{\mathrm{long}}$. For $r$ in it, $Z_r$ is the partition
function at fixed class $r$, $Z=Z_0$, and $\mathrm A(r)$ is the least $\ell^1$ norm of an integer field on the bonds whose
sums around the cycles of the slit graph are those of $r$; the proposition states $Z_r\le e^{-\sigma'\mathrm A(r)}Z$, where
$\sigma'$ is the tension $\sigma_V$ of Theorem 7.57 (\S\ref{s:arch}). In [U1], each configuration of class $r\neq0$ contains
an irreducible family of wall polymers of class $r$, one in which no nonempty subfamily has class $0$. Put
$\omega=e^{\sigma'\mathrm A}$ and $C_{\mathrm{FF}}=\sup_s\omega(s)Z_s/Z$. A union bound over these families and the
re-expansion of each as a seed (Theorems 7.27(c) and 7.49) leave partition functions $Z_s$ at shifted classes $s$, each at
most $C_{\mathrm{FF}}Z/\omega(s)$. Since $\omega(r)\le\omega(r-s)\,\omega(s)$, the weight $\omega(r-s)$ of the shift is left
over; Theorem 7.49(a) and the bound of Lemma 7.48 on the extensions of a seed absorb it, and with that of Proposition
7.52 on the sum over
families this gives $\omega(r)Z_r/Z\le\frac2{31}C_{\mathrm{FF}}$ for $r\neq0$. As $\omega(0)Z_0/Z=1$, it
follows that $C_{\mathrm{FF}}\le\max(1,\frac2{31}C_{\mathrm{FF}})$, and since $C_{\mathrm{FF}}$ is finite (Proposition
7.47), $C_{\mathrm{FF}}=1$, which is the proposition. The formal
version, \lean{prop\_7\_57} in \lean{U1/StageC/S77/FrozenFlux.lean} (named after the label \lean{prop:7.57}), is stated for any abelian group with a weight
$\omega\ge1$ such that $\omega(0)=1$ and $\omega(s+t)\le\omega(s)\omega(t)$, under the hypotheses that $Z_s\ge0$ (Lemma 7.42)
and $\sum_s\omega(s)Z_s<\infty$ (Proposition 7.47) and, over abstract types of families and extensions, Theorem 7.49(a),
the union bound with the re-expansion and the two bounds. The sums in these hypotheses take values in $[0,\infty]$, so
they need no summability hypotheses of their own. The last step is a separate lemma (\lean{le\_of\_sup\_bound}). The theorem
\lean{frozen\_flux} in \lean{U1/StageC/S77/AreaLawInput.lean} applies \lean{prop\_7\_57} to a structure whose fields are the objects of
Sections 7.1--7.8 for one output of the construction and the properties of these objects that the proof uses, and the
assembly in \lean{U1/StageC/Assembly/} fills these fields.

\subsection{What the interfaces had to make precise}\label{ss:guards}
The interfaces of Stage C had to state the inputs of Sections 6--7 in a form that the outputs of the construction actually
satisfy. The paper states several of them more generally than its proof uses them, and a formal interface that demands the
general form can be unsatisfiable. We call the restrictions that
make such an interface satisfiable guards; the following examples show the kind of precision that was needed.

Theorem 7.57 bounds the Villain loop $W_{G'}(C)$ on the slit domain $G'$ in terms of its minimal cut area $A_{G'}(C)$. The
paper proves it by a case split: either some bond of the slit graph crosses the rectangle, or none does. Only
in the first case is the seed set $X_1$ of the expansion nonempty. An interface that asked for Stage C data on every output
would be unsatisfiable, since data with $X_1=\emptyset$ would force $W_{G'}(C)\le0$, while $W_{G'}(C)>0$. The formal
interface therefore asks for the data only on crossing outputs, and on the others the bound is proved directly, from
$W_{G'}(C)=1$ and $A_{G'}(C)=0$.

The bounds of Section 7 are stated for every mass in a band, but their inputs exist only at the actual screening mass of
Section 6. The interface for Theorem 7.57 asks for them only at the one mass where the chain uses them. Similarly, the
position bound of Proposition B.7 needs a per-cell constant that does not depend on the Villain coupling $\tau$: its formal
statement fixes the constants outside the quantifier over $\tau$, and it is proved that each factor of the per-cell constant, measured in units of the screening mass, is bounded
uniformly in $\tau$ at the canonical point.

The other guards are of the same kind. The per-run fields are required only for valid runs, for loops of
at least the minimal length, for frozen sets inside the box and for crossing outputs; the seed bound with the loop present only for seeds
that contain $X_1$; and some hypotheses of the lemmas leading to Proposition B.7 are bounded quantifiers, which in the unbounded
form could not hold. Guards also appear in earlier sections: the rooted minimizers of the contour bound lie in the box and have
the loop $C$ as their boundary, as the paper's minimizers do, and on the output of the construction the map from sites to the $\mathcal U$-cells, the unions of cells from which the
polymers of the expansion are built, is onto (\lean{Construction.outWallGeom\_ucell\_surjective}). The audit of satisfiable
hypotheses (\S\ref{s:audits}) records these guards. Its probes, Lean files kept outside the library and compiled against it, show for each guard that it is needed or that the
objects of the proof satisfy it, except for the guards on the length of the loop and on the frozen sets, which [U1] itself
imposes, and the one on minimizers, which holds by the definition of the rooted minimizers.

\subsection{The appendices and the supplement}
Appendices A, B and C, which carry [BF80, Section 9.1], [BF80, Section 9.8] and [GM82, Appendix E] over to slit domains,
are formalized with the subsections of Section 7 listed above. Appendix D (heat kernel, coarse-to-fine transfer
and covariance bounds on slit domains) is formalized with Section 6, and the constants of the supplement are in
\lean{U1/Numerics/} (\S\ref{s:numerics}).