%======================================================================
\section{Architecture}\label{s:arch}

An interface is a Lean structure or proposition that collects the
results passed from one part of the proof to another. The passage from one interface to the next is always a proved
theorem, and hypotheses enter only as arguments of theorems, never as global assumptions.

The first interface is the structure \lean{U1.R0}. For one deterministic construction, it packages the results of [U1] on which
the chain of its Section 8 relies:
\begin{itemize}
\item the construction: for each rectangle $C$ a box $\Lambda^\circ$ with $C\subset\Lambda^\circ\setminus\partial\Lambda^\circ$
(Lemma 3.3(e)) and, for each set $D$ of frozen plaquettes in $\Lambda^\circ$ off its boundary, a hole set and a set of frozen plaquettes that
contains $D$ (property (R1) of Theorem 3.20);
\item the screening mass $\tilde m$, with $m_D/2\le\tilde m\le2m_D$ for large $\tau$, where $m_D$ is the Debye mass;
\item Theorem 7.57, the area law on every output of the construction, with its error term $\eta_S\to0$;
\item Theorem 5.1, the contour bound, for all large $K$, with its error term $\eta_T\to0$.
\end{itemize}
For example, the field that carries Theorem 7.57 reads, with line breaks of our own,

\noindent\begin{minipage}{\linewidth}
\begin{alltt}
  thm_7_61 : \(\forall\) \(\tau\), tau0 \(\le\) \(\tau\) \(\to\) \(\forall\) C : Rect,
    loopScale r0 (mt \(\tau\)) \(\le\) C.R \(\to\) loopScale r0 (mt \(\tau\)) \(\le\) C.T \(\to\)
    \(\forall\) D \(\subseteq\) (box \(\tau\) C).intPlaqs,
      (box \(\tau\) C).slitW (frozen \(\tau\) C D) (holes \(\tau\) C D) \(\tau\) C.flat \(\le\)
        Real.exp (-sigmaV r0 (mt \(\tau\)) \(\tau\) *
            (((box \(\tau\) C).minCutArea (frozen \(\tau\) C D) C.chain : \(\mathbb{R}\))
              - etaS \(\tau\) * C.R * C.T) + cN * (C.R + C.T))
\end{alltt}
\end{minipage}

Here \lean{box}, \lean{frozen} and \lean{holes} are fields of the same structure that give the construction, \lean{slitW} is the
Villain loop on the slit domain, computed from the flat rectangle \lean{C.flat} that the loop bounds, and \lean{minCutArea} is
the minimal cut area of the loop. Of the other names, \lean{tau0} is the threshold in $\tau$ of Theorem 7.57, \lean{r0} the fine side $r_0$ of a
coarse cell, \lean{mt} the screening
mass $\tilde m$, \lean{loopScale r0 (mt \(\tau\))} the lower bound $R_1$ on the sides, \lean{intPlaqs} the set of interior
plaquettes of the box, and \lean{sigmaV}, \lean{etaS} and \lean{cN} are the constants $\sigma_V$, $\eta_S$ and $c_N$ of
Theorem 7.57. The field
thus says that, on the slit domain $G'(D)$ built from $D$, $W_{G'(D)}(C)\le\exp(-\sigma_V[A_{G'(D)}(C)-\eta_SRT]+c_N(R+T))$ for all $\tau\ge\tau_0$, all rectangles
with $\min(R,T)\ge R_1$ and all $D$. The chain of Section 8 uses the field as it stands, without knowing how the
construction produces its objects.

\lean{U1.area\_law\_of\_R0 : U1.R0 \(\to\) U1.AreaLaw} formalizes Section 8. It covers the chain (1.4)--(1.8) at one coupling, the
choice of constants $\sigma=(1-\eta_T-\eta_S)\sigma_V$ and $c=c_N+10$, with $\sigma_V$ and $c_N$ from Theorem 7.57, the bound $4|C|+4\le10(R+T)$ and the case of
small $\beta$ in Remark 8.1, by monotonicity in $\beta$. It uses no numerical value of $\Kstar$ or of $\vCb$, which is half of Watson's integral, only $0<\vCb<\infty$.

The next interface, \lean{U1.R1}, is \lean{U1.R0} without the construction, which becomes data
(\lean{ConstructionMaps}) with a specification (\lean{ConstructionSpec}). For the construction of Sections 3--4 the
specification is proved (\lean{U1.consMaps\_spec}); \lean{U1.R1Cons} is \lean{U1.R1} for this construction.

In \lean{U1.R2} only the screening mass is kept. Theorems 7.57 and 5.1 for the outputs of the
construction become the propositions \lean{U1.Thm761OfRegSpec K r\(\sb0\) \(\tilde{m}\)} and \lean{U1.Thm51OfRegSpec K}, and the
properties of the construction needed in Sections 5--7 become a third, \lean{U1.RegSpec K}. Here \lean{K} is the list of
parameters of the construction (\lean{Construction.ConsParams}), not the constant $K$ of Theorem~\ref{thm:main}. \lean{U1.RegSpec K} says that every valid run of the construction satisfies \lean{Construction.RunSpec}, which collects
Theorems 3.20 and 3.21 in the form the later sections require. A run is the construction applied to one rectangle $C$ and one
frozen set $D$ at given $r_0$, $\tilde m$ and $\tau$; it is valid (\lean{Construction.Valid}) if its scales, defined in
Definition~3.1, satisfy $L_c\ge4$ for the block scale $L_c$ and $\ell\ge308L_c$ for the removal scale $\ell$, and its
rectangle has sides at least the fine block scale $L=r_0L_c$. The canonical point
\lean{U1.R2.canon} fixes $r_0=1$ and the screening mass \lean{Gas.mtCanon lamPV}, with $\lambda_{\mathrm{PV}}=e^{-2213.5}$
(\S\ref{s:numerics}). The bounds on this mass are proved in \lean{mtCanon\_lamPV\_bounds}. All three propositions
are proved:
\begin{itemize}
\item \lean{U1.RegSpec K} by \lean{U1.consMaps\_regSpec} (Sections 3--4);
\item \lean{U1.Thm51OfRegSpec K} by \lean{U1.MinCut.thm\_5\_1\_of\_regSpec} (Section 5), and its form for every $K>\Kstar$ by
\lean{U1.MinCut.thm51Kstar\_of\_regSpec};
\item \lean{U1.Thm761OfRegSpec} at the canonical point by the chain described next.
\end{itemize}

The part of the formalization in \lean{U1/StageC/} covers Sections 6--7 and Appendices A--D of [U1] and the assembly
described here. We call it Stage C, after its directory, which is named after the third stage of the work, not after a
stage of the proof in [U1]. For the third proposition, a family of Stage C data (\lean{U1.StageC.S77.StageCFamily}), the inputs of
Sections 7.7--7.9 for the outputs of the construction, gives Theorem 7.57 on every output. The fields of these data are assembled from the results of Sections 6--7 and
Appendix B into an explicit list: scalar constants, a threshold in $\tau$, and for every valid run of the construction at
large $\tau$ the per-run fields. In turn, all fields of the list are produced from one bound per run: the position bound of
Proposition B.7 (Step 4 of its proof in Section S4.7 of [U1]), which bounds the sum over positions of the activity $Q$ by a product of masses per cell times the
exponential of the fractions of the localized energy $F_1^{\mathrm{loc}}$ returned by Lemma B.8. This bound is proved for every valid run at the canonical point and all large $\tau$
(\lean{U1.StageC.Seed1.qMassRun\_HK}). The theorem \lean{U1.area\_law\_of\_qmass} and its variants turn it into the main
theorem and its corollaries, which \lean{U1/MainTheorem.lean} obtains by applying them.

\begin{table}[ht]
\centering\small
\begin{tabular}{p{0.22\textwidth}p{0.38\textwidth}p{0.3\textwidth}}
\toprule
interface & content & proved by\\
\midrule
\lean{R0} & construction, screening mass, Thm 7.57, Thm 5.1 & \lean{R1.toR0}\\
\lean{R1Cons} & \lean{R1} at the construction of Sections 3--4 & \lean{consMaps\_spec}, \lean{R2.toR1Cons}\\
\lean{R2} & screening mass; with the three propositions below it gives \lean{R1Cons} & \lean{R2.canon}, \lean{mtCanon\_lamPV\_bounds}\\
\lean{RegSpec K} & Theorems 3.20, 3.21 on every valid run & \lean{consMaps\_regSpec}\\
\lean{Thm51OfRegSpec K} & Theorem 5.1 on the outputs & \lean{MinCut.thm\_5\_1\_of\_regSpec}\\
\lean{Thm761OfRegSpec} & Theorem 7.57 on the outputs & \lean{StageC.Assembly.} \lean{leaf\_of\_qmass} with \lean{Seed1.qMassRun\_HK}\\
\bottomrule
\end{tabular}
\caption{The interfaces of the formal proof and the theorems that discharge them.}\label{tab:interfaces}
\end{table}

Table~\ref{tab:interfaces} lists the interfaces. We use them because they make the dependency graph of the proof explicit
and checkable. We formalize the chain of
Section 8 and the corollaries against \lean{U1.R0}, while the parts of the proof are formalized independently against fixed
statements. However, if the hypotheses of an interface are unsatisfiable, all theorems derived from it are vacuous; the main
theorems, which take no hypotheses, discharge every interface on their chain, as the audit of satisfiable hypotheses in
\S\ref{s:audits} records.