%
Part~S4 gives more detailed versions of some of these proofs: those of Section~\ref{S:proofs5} in
Section~\ref{S4-S:S4.2}, those of Section~\ref{S:E2} in Section~\ref{S4-S:S4.3}, those of
Section~\ref{S:F2} in Sections~\ref{S4-S:S4.4} and~\ref{S4-S:S4.5}, those of Section~\ref{S:H2}
in Section~\ref{S4-S:S4.8}, in a version that includes the bounds for every primitive-admissible wall field, and
those of Section~\ref{S:I2} also in Section~\ref{S4-S:S4.8}.

\subsection{Full proofs for Section~\ref{sec:2}}\label{S:proofsA}

\paragraph{Proof of Lemma~\ref{lem:2.3}.}\label{S:lem2.3}
We verify Ginibre's hypothesis \cite{Gi70} for the Villain weights directly. A continuous
function $K$ on $\mathbb T^m\times\mathbb T^m$ is a \emph{positive kernel} if it is a uniform limit
of finite sums $\sum_iu_i(\alpha)u_i(\beta)$ with continuous real $u_i$. Positive kernels form a
cone closed under products and under pullback by homomorphisms $\mathbb T^{m'}\to\mathbb T^m$, and
$\iint s(\alpha)s(\beta)K(\alpha,\beta)\,d\alpha\,d\beta\ge0$ for every continuous real $s$. A
continuous $w:\mathbb T\to\RR$ is \emph{admissible} if $(a,b)\mapsto w(a+b)w(a-b)$ is a positive
kernel, and we write $w_1\preceq w_2$ if $(a,b)\mapsto w_1(a+b)w_2(a-b)-w_1(a-b)w_2(a+b)$ is one.

\emph{Step 1 (Ginibre's argument).} Let $w_p>0$ be admissible, $\mu\propto\prod_pw_p(\theta_p)\,d\theta$,
and $B,B'$ integer vectors. The map $(\alpha,\beta)\mapsto(\alpha+\beta,\alpha-\beta)$ of
$\mathbb T^{E}\times\mathbb T^{E}$ onto itself preserves Haar measure, and
$\prod_pw_p(\theta_p(\alpha)+\theta_p(\beta))\,w_p(\theta_p(\alpha)-\theta_p(\beta))$ is a positive
kernel in $(\alpha,\beta)$. Doubling the variables and using
$\cos(x+y)\pm\cos(x-y)\in\{2\cos x\cos y,\,-2\sin x\sin y\}$ gives $\ex{\cos B\cdot\theta}_\mu\ge0$ and
$\ex{\cos B\cdot\theta\,\cos B'\cdot\theta}_\mu\ge\ex{\cos B\cdot\theta}_\mu\ex{\cos B'\cdot\theta}_\mu$,
as in \cite[Propositions~2, 3]{Gi70}. If moreover $w_q\preceq w_q'$ for one plaquette $q$, with
$w_q'>0$, then the same change of variables in
$\iint(\cos B\cdot\theta'-\cos B\cdot\theta)\,w_q(\theta_q)w_q'(\theta_q')\prod_{p\ne q}w_p(\theta_p)w_p(\theta_p')\,d\theta\,d\theta'$,
symmetrized under $\beta\mapsto-\beta$, shows that replacing $w_q$ by $w_q'$ does not lower
$\ex{\cos B\cdot\theta}$.

\emph{Step 2 (the Villain weights).} Let $t,t_1,t_2>0$. Expanding $\vt_t(a\pm b)$ in Fourier series
and putting $p=n+m$, $r=n-m$ (so $p\equiv r$ mod $2$ and $n^2+m^2=\frac12(p^2+r^2)$) gives
\[
\vt_t(a+b)\vt_t(a-b)=\tfrac12\bigl(c(a)c(b)+\tilde c(a)\tilde c(b)\bigr),\qquad
c(a):=\sum_pe^{-p^2/4t}\cos pa,\quad\tilde c(a):=\sum_p(-1)^pe^{-p^2/4t}\cos pa ,
\]
so $\vt_t$ is admissible. For $t_1\le t_2$, with $\sigma:=\frac1{8t_1}+\frac1{8t_2}$ and
$\kappa:=\frac1{4t_1}-\frac1{4t_2}\ge0$,
\[
\vt_{t_1}(a+b)\vt_{t_2}(a-b)-\vt_{t_1}(a-b)\vt_{t_2}(a+b)
=2\sum_{p\equiv r\ (2)}e^{-\sigma(p^2+r^2)}\sinh(\kappa pr)\,\sin pa\,\sin rb ,
\]
a positive kernel: expand $\sinh(\kappa pr)=\sum_{j\ \mathrm{odd}}\kappa^jp^jr^j/j!$ and
$\one_{p\equiv r}=\frac12(1+(-1)^{p+r})$; the series converges absolutely, as $\sigma-\kappa/2=1/(4t_2)>0$.
Hence $\vt_{t_1}\preceq\vt_{t_2}$. Finally $\vt_t(a-b)-\vt_t(a+b)=2\sum_ne^{-n^2/2t}\sin na\,\sin nb$, so
$1\preceq\vt_t$, and the constant $1$ (a removed plaquette) is admissible.

\emph{Step 3 (conclusion).} Step~1 with $w_p=\vt_{t_p}$ gives (a), with $\ex{\sin\theta_C}=0$ by
$\theta\mapsto-\theta$. Step~1 with $\vt_{t_1}\preceq\vt_{t_2}$, one plaquette at a time, gives (b), and
with $1\preceq\vt_t$ and the admissibility of $1$ it gives (c).

\emph{Step 4 (frozen limits).} For fixed couplings off $D$, the expectation is a
nondecreasing function of the couplings on $D$ with values in $[0,1]$, and
therefore has a limit. This limit inherits monotonicity in the other
couplings. If $D\subseteq D'$ and $s\ge\tau$, then
$t^{\tau,D,s}\le t^{\tau,D',s}$ coordinatewise, so
$\ex{\cos\theta_C}^{V}_{t^{\tau,D,s}}\le\ex{\cos\theta_C}^{V}_{t^{\tau,D',s}}\le g_{X,\tau}(C;D')$,
and $g_{X,\tau}(C;D)\le g_{X,\tau}(C;D')$. Monotonicity in $\tau$ passes to the
limit in the same way.
\qed

\paragraph{Proof of Lemma~\ref{lem:2.8}.}\label{S:lem2.8}
Let $Q_s(k):=\frac1{2\tau}\abs{\one_{F^c}(n_0+\partial k)}^2+\frac1{2s}\abs{\one_F(n_0+\partial k)}^2$,
so that by Lemma~\ref{lem:2.7} the left side of \eqref{eq:2.frozen} at
finite $s$ is $N_s/D_s$ with $N_s:=\sum_ke^{-Q_s(k)}$ and $D_s$ the same sum
for $n_0=0$. We write $k=w'+w$ with $w'\in W'$, $w=\sum_\KK a_\KK\one_\KK\in W$.
Since $\one_{F^c}\partial w=0$,
\[
N_s=\sum_{w'\in W'}e^{-\frac1{2\tau}\abs{\one_{F^c}(n_0+\partial w')}^2}S_s(w'),\qquad
S_s(w'):=\sum_{a\in\ZZ^{\mathcal K_F}}e^{-\frac1{2s}\abs{b+Ba}^2},
\]
with $b:=\one_F(n_0+\partial w')\in\RR^F$ and $Ba:=\partial(\sum_\KK a_\KK\one_\KK)\in\RR^F$.
The matrix $M:=B^{\mathsf T}B$ is positive definite because $\partial$ is
injective. Completing the square, we get $\abs{b+Ba}^2=(a-a_0)\cdot M(a-a_0)+\abs{Pb}^2$
with $a_0:=-M^{-1}B^{\mathsf T}b$ and $P:=1-BM^{-1}B^{\mathsf T}$ the orthogonal
projection onto $(\operatorname{im}B)^\perp$. Poisson summation in $a$ gives
\begin{gather*}
S_s(w')=(2\pi s)^{\abs{\mathcal K_F}/2}(\det M)^{-1/2}\,e^{-\abs{Pb}^2/(2s)}\bigl(1+r_s(w')\bigr),\\
\abs{r_s(w')}\le\rho_s:=\sum_{0\ne m\in\ZZ^{\mathcal K_F}}e^{-2\pi^2s\abs{m}^2/\norm{M}},
\end{gather*}
uniformly in $w'$, and $\rho_s\to0$ exponentially. The prefactor is the same
in $N_s$ and $D_s$ and cancels. In the remaining sums the factor
$e^{-\abs{Pb}^2/(2s)}(1+r_s)$ tends to $1$, is bounded by $2$ for large $s$,
and differs from $1$ by at most $\abs{\one_F(n_0+\partial w')}^2/(2s)+\rho_s$.
If $\one_{F^c}\partial w'=0$ for some $w'\in W'\otimes\RR$, then $w'$ is constant
on each component of the unfrozen graph and vanishes on the component of the
ground, so $w'\in(W\otimes\RR)\cap(W'\otimes\RR)=\{0\}$. Hence
$\abs{\one_{F^c}(n_0+\partial w')}^2\ge c\abs{w'}^2-C$ for some $c>0$, and
$e^{-\frac1{2\tau}\abs{\one_{F^c}(n_0+\partial w')}^2}$ times any polynomial in
$w'$ is summable over $W'$. Dominated convergence gives \eqref{eq:2.frozen},
and the bound on the factor gives the rate $O(1/s)$. Since the summands of
\eqref{eq:2.frozen} are $W$-invariant functions of $k\in\ZZ^{\Lam'_3}$, the
sums do not depend on the complement.
\qed