%======================================================================
\section{Audits}\label{s:audits}

The proof checker does not notice if a statement says less than the paper, if a hypothesis is unsatisfiable, or if a build
depends on files that are not in the repository. The audits check for each of these. Like the referee reports on the written-out proofs, they
were made separately from the writing of the formal proofs. The audit reports are in the
directory \lean{audit/} of the Lean archive and, for the release checks on the audited commit \lean{e8e86d3}, in a separate file of
[repo] (\S\ref{s:stats}).

\subsection{Statements}
The audit of the main results compares each Lean statement of a paper result with its statement in
[U1], clause by clause: quantifiers and their order, ranges of parameters, boundary conditions, normalizations and the
objects quantified over. Deliberate generalizations are recorded as such. Definition 1.1 (the Wilson and Villain measures, the Wilson loop and the area law), both
assertions of Theorem 1.2 (with $\Kstar=377.38$), the infinite-volume form of the area law (Remark 8.1) and
Proposition 9.1 (more general than in [U1]) are faithful, and Corollaries 1.3 and 1.4 in the paper's form are
\lean{U1.Main.cor\_1\_3\_rel} and \lean{U1.Main.cor\_1\_4\_rel} together with \lean{thm\_1\_2}. The statements of Section 2 match the paper, with two restrictions
that no statement of a main theorem involves: Lemma 2.2 is stated without the uniqueness of the mixture $\omega_\beta$, and
Lemma 2.3(d) for couplings on $D$ that are all equal to $s$, as $s\to\infty$. The interfaces restate the results of [U1] that
they cite, field by field. A separate audit finds that the nine closed statements of Appendix~E, those of its eight results and of the realized weights, match the text of [U1] without extra
hypotheses, and Lean probes show that each of their hypotheses is satisfied by the paper's own objects: the Wilson and
Villain weights are plaquette
weights, Villain weights are Villain mixtures, the Wilson weight is of Ginibre type, a one-plaquette complex realizes its
own weight, and $\partial\delta_{p_0}\neq0$ on the cube. Both audits were made against version 3 of [U1]; version 4 states Definition 1.1,
Theorem 1.2, its corollaries and the results of Sections 2, 8 and 9 and of Appendix E with the same mathematical
content.

\subsection{Satisfiable hypotheses}
Every hypothesis structure on the chain from the construction to Theorem 1.2 is inhabited
by closed terms of the library, since the proofs of the main theorems build each interface at the canonical
parameters. These structures are satisfiable because of the guards, and the
probes in \lean{audit/probes/} check the guards as described in \S\ref{ss:guards}; all $38$ probe files compile against the
audited commit.

\subsection{The library}
The release checks build the library from a fresh export of the audited commit and run \lean{\#print axioms} on every
theorem of Theorem~\ref{thm:formal}, with the result stated there.
The source contains no \lean{sorry}, no \lean{axiom} declaration and no \lean{native\_decide}, and no constant of the
library uses \lean{sorryAx}. Every constant stored in the compiled library is replayed through the kernel, which accepts
all of them. The theorems of Theorem~\ref{thm:formal} with all their dependencies, and separately every named constant of
the library with its dependencies, are exported with \lean{lean4export}; both exports contain only the same three
axioms, and two independent kernel implementations, \lean{nanoda} and \lean{lean4lean}, accept both. The report of the
release checks (\S\ref{s:stats}) gives the details.