%
\subsection{Full proofs for Appendix~\ref{app:A}}\label{S:I2}

\paragraph{Proof of Proposition~\ref{prop:A.9}, step (3).}
We use the notation of Lemma~\ref{lem:7.53} and Proposition~\ref{prop:A.9}, and we put
$w(\mathcal S):=e^{-(c'/8)\Floc(\mathcal S,N_{\mathcal S})}$.
Since $Z^o\subseteq S_0$ and $11c'/16-\eps\ge c'/8$, steps (1)
and (2) show that the left side of Lemma~\ref{lem:7.53}(a) is at most
$\cP'e^{c_S|S_0|}\sum_\sigma\prod_{\mathcal S}w(\mathcal S)$, the sum over
$\sigma\in\Sigma_{\mathrm{sat}}(S_0)$ and the product over the wall polymers
$\mathcal S$ of $\sigma$. Assigning the disjoint wall polymers of $\sigma$ to
their first cells in $S_0$ bounds the sum by
$\prod_{\Delta\subseteq S_0}\bigl(1+\sum_{\mathcal S\ni\Delta}w(\mathcal S)\bigr)$,
and
\[
\sum_{\mathcal S\ni\Delta}w(\mathcal S)\le6D_Ie^{-(c'/4)\Funit}=\etaseed
\]
under ($\beta3$). Indeed, Lemmas~\ref{lem:7.6}(a) and~\ref{lem:7.26} show that a wall polymer with its walls is determined by its wall
interfaces and their values. These interfaces form a set
connected at Euclidean scale $g$ containing one of the $D_I$ interfaces
within distance $g$ of $\Delta$, so the lattice-animal count of
Lemma~\ref{lem:5.12}, together with $\Floc(\mathcal S)\ge2\Funit\sum_IN_I^2$
from Lemma~\ref{lem:7.32}(a), gives
$\sum_{n\ge1}D_I(eD_I)^{n-1}(3e^{-(c'/4)\Funit})^n$. This gives (a).

In (b),
the terms with $\sigma=(S_0,0)$ and $X\ne S_0$ gain $c_{16}^D$, and those
whose $\sigma$ contains a wall polymer contribute
$(1+\etaseed)^{|S_0|}-1\le\etaseed e^{2|S_0|}$, so the sum without the term
$X=S_0$, $N_X=0$ is at most
$(c_{16}^D+\etaseed)\cP'e^{(c_S+2)|S_0|}=c_{16}\cP'e^{c_2|S_0|}$.

In (c$'$) we have
$\cP'=1$ and $Z^o=\emptyset$, and \eqref{eq:A.core} with $\eps\le c'/8$ and
$c_w=c'/16$ leaves $e^{-(c'/2)\Floc(Z,N_Z)}$.