%======================================================================
\section{Appendix E of [U1]}\label{s:appE}

Appendix~E of [U1] is formalized in \lean{U1/AppendixE/} and \lean{U1/AppendixEMain.lean}, in the namespace
\lean{U1.AppendixE}. These files are in the import closure of the root module, so the audits
and the build cover them. The formalization follows the proofs of the appendix.
Table~\ref{tab:formal} gives each result with its closed statement in \lean{U1/AppendixE/Statements.lean} and the theorem
that proves it. The remarks E.5, E.7, E.9 and E.11 are not results, and the numerical values quoted after Theorem E.8 are
not formalized.

\subsection{What the appendix reuses}
The appendix uses the definitions of the main formalization. The
Gibbs expectation of the appendix is the expectation of Section~2 (\lean{gibbsExp\_eq\_gexp}), and with the Wilson weight on
every plaquette it is the Wilson expectation of Theorem~\ref{thm:main} (\lean{gibbsExp\_wilsonW}). The dual formula of
Lemma E.1 is proved for general plaquette weights with the character integrals and Fourier series of the dual
representation (\lean{U1/Dual/}), by the steps that give the Villain case. Theorem E.2(b) and Proposition E.6(a) use the
Ginibre framework of Section~2 (\lean{U1/Correlation/}): the admissibility of $e^{\lambda\cos\varphi}$ and Ginibre's order,
composed with $\varphi\mapsto j\varphi$ and with products, give the monotonicity in every coefficient $\lambda_{p,j}$. Corollary
E.4, Proposition E.6 and the certificate below use the modified Bessel functions $I_\nu$ and their series (\lean{U1/Special/}).

\subsection{Where the proofs take other routes}
At three steps the formal proofs differ from those in [U1].
\begin{itemize}
\item Lemma E.3 is proved without Poisson summation on the lattice. With $g(y)=e^{-\|y\|^2}$ and its periodization
$G(y)=\sum_{m\in\Gamma}g(m+y)$, the Gaussian convolution identity and the unfolding of the integral over a fundamental domain $F$
of $\Gamma$ give $c\sum_{m\in\Gamma}e^{-\|m+x\|^2/2}=\int_FG(z)G(x-z)\,dz$ with $c>0$. Since $G$ is even, the Cauchy--Schwarz
inequality bounds the right side by its value at $x=0$. The lemma is also proved for discrete subgroups that are not of full
rank, with the factor $e^{-\|x-Px\|^2/2}$ for an orthogonal projection $P$ onto a subspace containing $\Gamma$.
\item In Theorem E.2(a), the plaquettes with coupling $t_p=0$ are handled directly instead of by the limit $s\downarrow0$. The
cycles that contribute form a coset of the sublattice of cycles vanishing on these plaquettes, and the form of Lemma E.3
with a projection factor applies to it.
\item In Proposition E.12, Poisson summation for the one-dimensional theta functions comes from Mathlib's summation formula
for quadratic exponentials. For the ratio $R_d$ of theta functions that [U1] uses, with $d$ frozen faces, it gives
$(1-3q)/(1+q)\le R_d\le1$ with $q=e^{-2\pi^2\tau/(6-d)}\le e^{-\pi^2\tau/3}$, in place of
the bound $(1-2\varrho)/(1+2\varrho)$ of [U1], and the conclusion for $\tau\ge3$ is the same.
\end{itemize}

\subsection{The kernel decision for Theorem E.8}
On the boundary of the cube the cycles are the multiples of the sum of the
faces (\lean{mem\_cycles2\_cube\_iff}); the cell counts, the incidences and $\partial\partial=0$ of the cube are decided by the
kernel. Lemma E.1 then gives the closed form $\mathcal W(x)=(A_C+xB_C)/(A_0+xB_0)$ of [U1] for the loop around $p_0$ as a function of the coefficient $x=c_1$ of the weight on $p_0$, so $\mathcal W'$ has the sign of
$S=A_0B_C-A_CB_0$, and the derivative with every face perturbed has the sign of a second number $U$. Both are series in the
coefficients $c_k$ of the weight, homogeneous of degree $11$. A soundness lemma (\lean{cube\_signs\_of\_bounds}) turns rational
enclosures of $c_k$ for $k\le H+2$, together with a geometric bound on the remaining coefficients, into rational upper bounds
for $S$ and $U$; here $H=4$.
\begin{itemize}
\item For the Villain weight, $c_k=(15/16)^{k^2}$ is rational, and $(h+6)^2\ge36+12h$ gives the geometric bound
$c_{6+h}\le c_6(15/16)^{12h}$ for $h\ge0$.
\item For the Wilson weight $w^W_8$, homogeneity allows $c_k=I_k(8)$. Sixteen terms of the series
$I_k(8)=\sum_{m\ge0}4^{2m+k}/(m!\,(m+k)!)$ and a geometric remainder enclose $I_k(8)$, and $I_{k+1}(8)\le4I_k(8)/(k+1)$ gives the
geometric bound.
\end{itemize}
As for Watson's integral, the kernel decides (\lean{decide +kernel}) that the resulting rational
upper bounds are negative. The bounds give $S\le-0.277$ and $U\le-0.325$ for the Villain weight and $S\le-0.2529\,I_0(8)^{11}$ and
$U\le-0.2958\,I_0(8)^{11}$ for the Wilson weight. The margins are large, so the low truncation suffices.