This holds by definitional equality (reflexivity), since \(\operatorname {deformedCheck}\) is defined as \(\operatorname {deformedOpExt}\).

This follows directly from the theorem that the deformed operator extension commutes with Gauss’s law when the boundary condition holds.

This follows directly from the self-inverse property of the deformed operator extension.

This follows directly from the commutation of Gauss’s law operators (Theorem 117).

This follows directly from the commutation of flux operators (Theorem 118).

This follows directly from the Gauss–flux commutation theorem (Theorem 120).

By the commutativity of Pauli commutation (i.e., \([A, B] = 0 \Leftrightarrow [B, A] = 0\)), it suffices to show that \(\tilde{s}_j\) commutes with \(A_v\). This follows directly from the theorem that the deformed operator extension commutes with Gauss’s law when the boundary condition holds, which is guaranteed by the deformed code data.

We unfold the definitions of the deformed original checks, deformed check, and flux checks, and express the Pauli commutation condition in terms of the symplectic inner product. We decompose the sum over the extended qubit system \(V \oplus E(G)\) into the vertex part and the edge part using \(\operatorname {Fintype.sum\_ sum\_ type}\).

Vertex part: We show that

For each vertex \(v\), by the definitions of \(\operatorname {deformedOpExt}\) and \(\operatorname {fluxOp}\), we have \(z_{B_p}(v) = 0\) and \(x_{B_p}(v) = 0\) on vertex qubits, so each summand vanishes. By summing zero terms, the vertex contribution is \(0\).

We rewrite using \(0 + (\text{edge sum}) = (\text{edge sum})\).

Edge part: We show that

For each edge \(e\), by the definitions of \(\operatorname {deformedOpExt}\) and \(\operatorname {fluxOp}\), the deformed check has \(x_{\tilde{s}_j}(e) = 0\) on edge qubits (no \(X\)-support on edges), and the flux operator has \(x_{B_p}(e) = 0\) (pure \(Z\)-type). Thus each summand vanishes, and the edge contribution is \(0\).

We unfold the definitions of the deformed original checks and deformed check, and express the Pauli commutation condition via the symplectic inner product. We decompose the sum over \(V \oplus E(G)\) into the vertex and edge parts.

Edge part: We show that

For each edge \(e\), by the definition of \(\operatorname {deformedOpExt}\), both deformed checks have \(x_{\tilde{s}_k}(e) = 0\) on edge qubits. Thus each summand vanishes and the edge sum is \(0\).

Vertex part: We show that

From the hypothesis, the original checks \(s_i\) and \(s_j\) commute, i.e., \(\langle s_i, s_j \rangle _{\mathrm{symp}} = 0\). Since the deformed operator extension on vertex qubits agrees with the original operator, the vertex sum equals the symplectic inner product of the original checks, which is \(0\) by hypothesis. We use convert to match the goal with the hypothesis \(h_{ij}\).

Combining both parts: the total symplectic inner product is \(0 + 0 = 0\).

We proceed by case analysis on the check indices \(a\) and \(b\).

Case \(a = \operatorname {gaussLaw}(v)\):

• If \(b = \operatorname {gaussLaw}(w)\): by Gauss–Gauss commutation.

• If \(b = \operatorname {flux}(p)\): by Gauss–flux commutation.

• If \(b = \operatorname {deformed}(j)\): by Gauss–deformed commutation.

Case \(a = \operatorname {flux}(p)\):

• If \(b = \operatorname {gaussLaw}(v)\): by commutativity of Pauli commutation and Gauss–flux commutation.

• If \(b = \operatorname {flux}(q)\): by flux–flux commutation.

• If \(b = \operatorname {deformed}(j)\): by commutativity of Pauli commutation and deformed–flux commutation.

Case \(a = \operatorname {deformed}(i)\):

• If \(b = \operatorname {gaussLaw}(v)\): by commutativity of Pauli commutation and Gauss–deformed commutation.

• If \(b = \operatorname {flux}(p)\): by deformed–flux commutation.

• If \(b = \operatorname {deformed}(j)\): by deformed–deformed commutation.

This follows directly from the fact that every Pauli operator is self-inverse (\(P \cdot P = \mathbf{1}\)).

This follows directly from the self-inverse property of Pauli operators.

This follows from the self-inverse property of the deformed check applied to \(s_j\) and \(\gamma _j\).

We proceed by case analysis on \(a\):

• If \(a = \operatorname {gaussLaw}(v)\): by self-inverse property of Gauss’s law checks.

• If \(a = \operatorname {flux}(p)\): by self-inverse property of flux checks.

• If \(a = \operatorname {deformed}(j)\): by self-inverse property of deformed original checks.

This follows directly from the fact that the Gauss’s law operator has zero \(Z\)-vector.

This follows directly from the fact that the flux operator has zero \(X\)-vector.

We convert the goal to the statement of the Gauss’s law product theorem and apply it directly.

We unfold the definitions of the flux checks and Pauli operator weight.

First, we establish that \(B_p\) has no \(X\)-support: \(\operatorname {supportX}(B_p) = \emptyset \), which follows from the fact that flux operators are pure \(Z\)-type.

Next, we characterize the \(Z\)-support of \(B_p\). By extensionality, for each qubit \(q\) in the extended system \(V \oplus E(G)\):

• If \(q = \operatorname {inl}(v)\) for some vertex \(v\): the \(Z\)-component of \(\operatorname {fluxOp}\) is \(0\) on vertices, so \(q \notin \operatorname {supportZ}(B_p)\). No edge maps to a vertex under \(\operatorname {inr}\), confirming both directions of the equivalence.

• If \(q = \operatorname {inr}(e)\) for some edge \(e\): \(q \in \operatorname {supportZ}(B_p)\) if and only if \(e \in p\). In the forward direction, if \(e \notin p\) then by definition of \(\operatorname {fluxOp}\) the \(Z\)-component is \(0\), a contradiction. In the reverse direction, if \(e \in p\) then the \(Z\)-component is \(1 \neq 0\).

Thus \(\operatorname {supportZ}(B_p) = \operatorname {inr}(\{ e \in E(G) : e \in p\} )\), i.e., it is the image of the set of edges in the cycle under the embedding \(\operatorname {inr}\).

Since \(\operatorname {support}(B_p) = \operatorname {supportX}(B_p) \cup \operatorname {supportZ}(B_p) = \emptyset \cup \operatorname {supportZ}(B_p) = \operatorname {supportZ}(B_p)\), the weight equals \(|\operatorname {supportZ}(B_p)|\). Since \(\operatorname {inr}\) is injective, \(|\operatorname {inr}(\{ e \in E(G) : e \in p\} )| = |\{ e \in E(G) : e \in p\} |\).