Exact indistinguishability in a contractible disk

The basis matrix units $\mathrm{\mid }x⟩⟨y\mathrm{\mid }$ span all operators on the finite register by [F7]. Each is the tensor product of one-qubit matrix units by [F8]. The four identities in [F6] therefore express every global matrix unit as a linear combination of tensor Pauli operators. Hence tensor Paulis span the full operator space. If $O$ is supported on $S$, apply the same expansion to $O_S$ in [F5] and tensor with identity outside $S$; every resulting Pauli term is supported on a subset of $S$.

Consider one tensor Pauli $E$ from this expansion. If it anticommutes with a check $g$, then the commutation fact [F2] and the common-$+1$ code definition [F3] make the projector relation [F4] applicable. It gives $\mathrm{\Pi }E\mathrm{\Pi }=\mathrm{\Pi }gE\mathrm{\Pi }=-\mathrm{\Pi }Eg\mathrm{\Pi }=-\mathrm{\Pi }E\mathrm{\Pi }$, so $\mathrm{\Pi }E\mathrm{\Pi }=0$. If $E$ commutes with all checks, write it as a phase times $X^x{Z}^z$. By [F1] and [F9], $z$ has even incidence at every primal vertex and $x$ has even incidence at every dual vertex. They are therefore primal and dual cycles. Their supports lie among the qubits in $S$; by [F12] both cycles lift to finite square-grid cycles. By [F11], the lifted Z cycle is a sum of square face boundaries and the lifted X cycle is a sum of dual face boundaries. Projecting these finite face chains to the torus gives products of plaquette checks and star checks with exactly the original support labels. Indeed, the quotient is a chain map because the boundary of each unit face maps to the stated four-edge torus boundary by [F13]; repeated image faces cancel in pairs over ${\mathbb{F}}_2$. Thus $E$ differs by a scalar phase from a product of checks, by [F10], and $\mathrm{\Pi }E\mathrm{\Pi }$ is a scalar multiple of $\mathrm{\Pi }$ by [F3] and [F4].

Every term in the Pauli expansion of $O$ from step 1.1 has either zero compression or scalar compression by step 2.1. Summing these finitely many terms gives $\mathrm{\Pi }O\mathrm{\Pi }=c(O)\mathrm{\Pi }$. The code projector is nonzero by [F14], so the scalar can be chosen as the sum of the scalar coefficients of those terms.