By the definition of \(\operatorname {xCheckIndices}\), membership requires \((\mathtt{check}(i)).\mathtt{zVec} = 0\). Simplifying the filter condition from the membership hypothesis yields the result directly.

By the definition of \(\operatorname {zCheckIndices}\), membership requires \((\mathtt{check}(i)).\mathtt{xVec} = 0\). Simplifying the filter condition yields the result.

This follows directly from the fact that all checks of a stabilizer code pairwise commute.

This follows directly from the pairwise commutation of stabilizer code checks.

We expand the definition of \(\operatorname {PauliCommute}\) as the symplectic inner product. The symplectic inner product \(\langle P, R \rangle = \sum _v (P.\mathtt{xVec}(v) \cdot R.\mathtt{zVec}(v) + P.\mathtt{zVec}(v) \cdot R.\mathtt{xVec}(v))\). Since \(P.\mathtt{zVec} = 0\) and \(R.\mathtt{zVec} = 0\), each term in the sum vanishes, so the sum equals zero.

We expand the symplectic inner product. Since \(P.\mathtt{xVec} = 0\) and \(R.\mathtt{xVec} = 0\), every term \(P.\mathtt{xVec}(v) \cdot R.\mathtt{zVec}(v) + P.\mathtt{zVec}(v) \cdot R.\mathtt{xVec}(v)\) vanishes, so the total sum is zero.

We choose the left disjunct. By the definition of the identity Pauli operator, \((1).\mathtt{zVec} = 0\).

By simplification using the definitions of \(\operatorname {hyperBoundaryMap}\) and \(\operatorname {zCheckIncident}\).

This follows directly from the fact that hypergraph Gauss’s law operators have zero Z-component.

This follows directly from the general result that hypergraph Gauss’s law operators commute.

The result is the conjunction of the two properties established above: mutual commutation (from step1_gauss_commute) and pure X-type (from step1_gauss_pure_X).

Given \(\langle i, h \rangle \) witnessing \(p \sim q\), we decompose \(h\) into the two cases. In each case, swapping the two components of the conjunction gives the witness for \(q \sim p\).

Suppose \(p \sim p\). Then there exists \(i\) such that \(p = \operatorname {inl}(i)\) and \(p = \operatorname {inr}(i)\) (or vice versa), which contradicts \(\operatorname {inl} \neq \operatorname {inr}\).

The cardinality of a sum type is the sum of the cardinalities: \(|\operatorname {Fin}(n)| + |\operatorname {Fin}(n)| = n + n = 2n\).

This holds by definitional equality (reflexivity).

We provide the witness \(\langle i, \operatorname {Or.inl}\langle \operatorname {rfl}, \operatorname {rfl}\rangle \rangle \).

We provide the witness \(\langle i, \operatorname {Or.inr}\langle \operatorname {rfl}, \operatorname {rfl}\rangle \rangle \).

Suppose \(\operatorname {inl}(i) \sim \operatorname {inl}(j)\). Then there exists \(k\) with \(\operatorname {inl}(i) = \operatorname {inl}(k)\) and \(\operatorname {inl}(j) = \operatorname {inr}(k)\) (or vice versa), but \(\operatorname {inl}(j) = \operatorname {inr}(k)\) contradicts \(\operatorname {inl} \neq \operatorname {inr}\).

Suppose \(\operatorname {inr}(i) \sim \operatorname {inr}(j)\). Then there exists \(k\) with \(\operatorname {inr}(i) = \operatorname {inr}(k)\) and \(\operatorname {inr}(j) = \operatorname {inl}(k)\) (or a symmetric case), but \(\operatorname {inr} \neq \operatorname {inl}\) gives a contradiction.

For the forward direction, given \(\langle k, h \rangle \) witnessing adjacency, in the first case \(\operatorname {inl}(i) = \operatorname {inl}(k)\) gives \(i = k\) by injectivity, so \(q = \operatorname {inr}(k) = \operatorname {inr}(i)\). The second case gives \(\operatorname {inl}(i) = \operatorname {inr}(k)\), contradicting \(\operatorname {inl} \neq \operatorname {inr}\). For the reverse direction, if \(q = \operatorname {inr}(i)\) then the result follows from the matching edge lemma.

Analogous to the data adjacency characterization, using the reverse matching edge.

Since \(\operatorname {inl}(i) \sim \operatorname {inr}(i)\), adjacency implies reachability.

From the reachability hypothesis, we obtain a walk from \(p\) to \(q\). We prove by induction on the walk that any walk stays within a single component \(\{ \operatorname {inl}(i), \operatorname {inr}(i)\} \). For the nil walk, \(p = q\) and the component is determined by whether \(p\) is \(\operatorname {inl}(i)\) or \(\operatorname {inr}(i)\). For a cons walk, by the inductive hypothesis the tail of the walk stays in some component \(i\), and the adjacency step must connect to a vertex in the same component (since each vertex is only adjacent to its partner).

This follows from the general result that Gauss’s law operators have zero Z-component.

This is an instance of the general commutation result for Gauss’s law operators.

This is an instance of the general Gauss’s law product theorem.

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

By simplification using the definition of the logical operator.

By simplification using the definition of the logical operator.

By extensionality and simplification using the definition of \(\operatorname {pauliZ}\).

Both operators are pure Z-type (their \(\mathtt{xVec}\) is zero), so they commute by the pure Z commutation lemma.

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

The result is the conjunction of the three properties: commutation, self-inverse, and pure Z-type.

This is an instance of the general result that the entangling circuit transforms Gauss’s law operators to single-qubit \(X\) operators.

This is an instance of the general result that the entangling circuit transforms single-qubit \(X\) operators to Gauss’s law operators.

This is an instance of the general involutivity of the entangling circuit action.

This follows from the general result that the entangling circuit preserves symplectic inner products (and hence commutation), applied symmetrically.

The result is assembled from the three steps: Step 1 uses step1_gauss_commute and step1_gauss_pure_X; Step 2 uses step2_gauss_commute, step2_gauss_pure_X, and step2_cx_transforms_gauss; Step 3 uses step3_edgeZ_commute and step3_edgeZ_self_inverse.

From the CSS property, either \((\mathtt{check}(i)).\mathtt{zVec} = 0\) or \((\mathtt{check}(i)).\mathtt{xVec} = 0\). In the first case, if \(\mathtt{xVec} = 0\) as well, then the check is the identity, contradicting \(\mathtt{check}(i) \neq 1\); otherwise \(i \in \operatorname {xCheckIndices}\). The second case is analogous, yielding \(i \in \operatorname {zCheckIndices}\).

This holds by definitional equality.

This follows directly from the fact that all checks of a stabilizer code pairwise commute.

This holds by definitional equality.

By extensionality, membership in the neighbor finset is equivalent to adjacency, which by the data adjacency characterization is equivalent to \(q = \operatorname {inr}(i)\), i.e., membership in the singleton \(\{ \operatorname {inr}(i)\} \).

By extensionality, membership in the neighbor finset is equivalent to adjacency, which by the ancilla adjacency characterization is equivalent to \(q = \operatorname {inl}(i)\).

Rewriting the degree as the cardinality of the neighbor finset and using the data neighbor set result, \(|\{ \operatorname {inr}(i)\} | = 1\).

Rewriting the degree as the cardinality of the neighbor finset and using the ancilla neighbor set result, \(|\{ \operatorname {inl}(i)\} | = 1\).

We case-split on whether \(v = \operatorname {inl}(i)\) or \(v = \operatorname {inr}(i)\). In the first case we apply data_degree, in the second ancilla_degree.

We split the sum over the sum type \(\operatorname {Fin}(n) \oplus \operatorname {Fin}(n)\). Each data vertex contributes degree 1 and each ancilla vertex contributes degree 1, giving \(n \cdot 1 + n \cdot 1 = 2n\).

By the handshaking lemma, \(2|E| = \sum _v \deg (v) = 2n\).

The result assembles all the previously established properties: Step 1 commutation, Step 2 commutation and CX transformation, Step 3 commutation, the degree bound, and the edge count.