Pauli-path energy barrier

For any unit code vector $\psi$, each check has eigenvalue $+1$ by [F2], so [F1] gives $⟨\psi ,H_L\psi ⟩=-L^2(J_e+J_m)=E_{\mathrm{c}\mathrm{o}\mathrm{d}\mathrm{e}}$. For any Pauli prefix $E$ and any check $g$, [F5] gives $gE\psi =\pm Eg\psi =\pm E\psi$. Thus $E\psi$ has a joint check syndrome, and each term of $H_L$ has a fixed expectation on it. The sign pattern depends on $E$ and the checks, not on the choice of code vector $\psi$. Therefore $\epsilon (E)$ is well-defined and independent of that choice.

Every $Q$ in [F3] is a finite tensor product of one-edge Pauli factors $I,X,Y,Z$ from [F4], up to scalar phase. Applying its nonidentity factors one edge at a time gives at least one elementary path, so the set of paths in the Definition is nonempty.

By [F1] and [F2], the energy excess of any prefix is $2J_{e}a+2J_{m}b$, where $a,b\in \{0,\dots ,L^2\}$ count its violated stars and plaquettes. This is a finite set of possible real values. Hence the set of peak excesses over the nonempty path family is a nonempty subset of a finite set, and its minimum exists.