Since the boundary map \(\partial \) is linear, we have \(\partial (\gamma + \gamma ') = \partial \gamma + \partial \gamma '\). Unfolding the boundary condition, \(\partial \gamma = S_Z(s)|_V\) and \(\partial \gamma ' = S_Z(s)|_V\). Thus \(\partial (\gamma + \gamma ') = S_Z(s)|_V + S_Z(s)|_V\). By extensionality, for each vertex \(v\), this equals \(S_Z(s)|_V(v) + S_Z(s)|_V(v) = 0\) since we work over \(\mathbb {Z}/2\mathbb {Z}\) where \(a + a = 0\).

By the characterization of the kernel as \(\{ x \mid \partial x = 0\} \), this follows directly from the fact that \(\partial (\gamma + \gamma ') = 0\).

By extensionality, we verify for each qubit \(q\) in the extended system \(V \oplus E(G)\). For vertex qubits \(q = \operatorname {inl}(v)\), the X-component is \(0\) by definition of \(\operatorname {deformedOpExt}\). For edge qubits \(q = \operatorname {inr}(e)\), the X-component is also \(0\) by definition. Hence \(\operatorname {xVec} = 0\).

This follows directly from the fact that \(\widetilde{\operatorname {ext}}(P, \gamma ) \cdot \widetilde{\operatorname {ext}}(P, \gamma ) = \mathbf{1}\) applied with \(P = \mathbf{1}\) and \(\gamma = \delta \).

Unfolding the definitions of \(\tilde{s}\) and \(\operatorname {pureZEdgeOp}\), we apply the multiplication law for deformed operator extensions: \(\widetilde{\operatorname {ext}}(s, \gamma ) \cdot \widetilde{\operatorname {ext}}(\mathbf{1}, \gamma + \gamma ') = \widetilde{\operatorname {ext}}(s \cdot \mathbf{1}, \gamma + (\gamma + \gamma '))\). Since \(s \cdot \mathbf{1} = s\) and \(\gamma + (\gamma + \gamma ') = \gamma '\) (the latter because \(\gamma + \gamma = 0\) in \(\mathbb {Z}/2\mathbb {Z}\), so \(\gamma + (\gamma + \gamma ') = (\gamma + \gamma ) + \gamma ' = 0 + \gamma ' = \gamma '\)), we obtain \(\widetilde{\operatorname {ext}}(s, \gamma ')\). The result follows by symmetry.

Since addition in \(\mathbb {Z}/2\mathbb {Z}\) is commutative, \(\gamma ' + \gamma = \gamma + \gamma '\). The result then follows from the previous theorem.

We first show that \(\delta \) satisfies the boundary condition for the identity operator: since \(\partial \delta = 0\) and \(S_Z(\mathbf{1})|_V = 0\) (the identity has no Z-support on vertices), we have \(\partial \delta = S_Z(\mathbf{1})|_V\). The result then follows from the theorem that \(\widetilde{\operatorname {ext}}(P, \gamma )\) commutes with \(A_v\) whenever the boundary condition holds.

Expanding the symplectic inner product and splitting the sum over vertices and edges: for the vertex sum, each term vanishes because both operators have zero X-component and zero Z-component on vertices (the pure-Z edge operator has identity on vertices, and the flux operator is pure Z on edges with zero X on vertices). For the edge sum, each term vanishes because both operators have X-component equal to zero on edges (the pure-Z edge operator has \(\operatorname {xVec} = 0\) everywhere, and the flux operator is pure Z-type). Hence the symplectic inner product is zero.

Unfolding the definitions of \(\operatorname {deformedOriginalChecks}\) and \(\operatorname {deformedCheck}\), we expand the symplectic inner product and split the sum over vertices and edges. For the vertex sum: the pure-Z edge operator has \(\operatorname {xVec} = 0\) and \(\operatorname {zVec} = 0\) on vertices, so each vertex term vanishes. For the edge sum: the deformed operator extension has \(\operatorname {xVec} = 0\) on edges, and the pure-Z edge operator also has \(\operatorname {xVec} = 0\) on edges, so each edge term vanishes. Hence the total symplectic inner product is zero.

We take \(B = \operatorname {pureZEdgeOp}(\gamma _j + \gamma '_j)\). Then:

1. The equality \(\tilde{s}_j(\gamma '_j) = \tilde{s}_j(\gamma _j) \cdot B\) follows from the deformed check difference theorem.

2. The pure Z-type property \(\operatorname {xVec}(B) = 0\) follows from the fact that pure-Z edge operators have no X-support.

3. The boundary condition \(\partial (\gamma _j + \gamma '_j) = 0\) follows from the path difference kernel theorem, using the boundary conditions \(\partial \gamma _j = S_Z(s_j)|_V\) and \(\partial \gamma '_j = S_Z(s_j)|_V\) stored in both data and data\('\).

This follows directly from the deformed check difference theorem applied to the original check \(s_j\) with edge-paths \(\gamma _j\) (from data) and \(\gamma '_j\) (from data\('\)).

This follows from the path difference kernel membership theorem, using the boundary conditions stored in data and data\('\).

This holds by reflexivity: the Gauss’s law checks \(A_v\) do not depend on the edge-path data at all, so both sides are definitionally equal.

This holds by reflexivity: the flux checks \(B_p\) do not depend on the edge-path data at all, so both sides are definitionally equal.

We proceed by cases on the check index \(a\):

• Case \(a = \operatorname {gaussLaw}(v)\): The result follows from the theorem that the pure-Z edge operator commutes with Gauss’s law operators when \(\partial \delta = 0\).

• Case \(a = \operatorname {flux}(p)\): The result follows from the theorem that the pure-Z edge operator commutes with flux operators.

• Case \(a = \operatorname {deformed}(j)\): The result follows from the theorem that the pure-Z edge operator commutes with deformed original checks.

Unfolding the definition of deformed check, we compute the symplectic inner product by splitting the sum over vertices and edges. For the vertex sum: both deformed checks have the same X-vector and Z-vector on vertices (both coming from \(s\)), so the contribution is \(\sum _{v \in V} (s^X_v \cdot s^Z_v + s^Z_v \cdot s^X_v)\). Since multiplication in \(\mathbb {Z}/2\mathbb {Z}\) is commutative, each term is \(s^X_v \cdot s^Z_v + s^X_v \cdot s^Z_v = 0\) (as \(a + a = 0\) in characteristic 2). For the edge sum: both deformed operator extensions have X-component equal to \(0\) on edges, so each term \(0 \cdot z + z' \cdot 0 = 0\). Hence the total symplectic inner product is zero.

This is the deformed check difference theorem applied with the roles of \(\gamma \) and \(\gamma '\) swapped: \(\tilde{s}(\gamma ) = \tilde{s}(\gamma ') \cdot \operatorname {pureZEdgeOp}(\gamma ' + \gamma )\).