11 Lem 1: Deformed Code Checks
The operators listed in Definition 4 (Deformed Code) form a valid generating set of commuting checks for a stabilizer code (or subsystem code). Specifically, all six pairwise commutation relations among the Gauss’s law operators \(A_v\), the flux operators \(B_p\), and the deformed checks \(\tilde{s}_j\) are established. The combined checks are shown to be self-inverse, and together they define a valid stabilizer code on the extended qubit system \(V \oplus E(G)\).
For any two vertices \(v, w \in V\), the Gauss’s law operators commute:
i.e., \(\operatorname {PauliCommute}(\operatorname {gaussLawChecks}(G, v),\; \operatorname {gaussLawChecks}(G, w))\) holds. Both \(A_v\) and \(A_w\) are pure \(X\)-type operators, so they commute.
This follows directly from allChecks_pairwise_commute_gaussLaw_gaussLaw.
For any two cycle indices \(p, q \in C\), the flux operators commute:
i.e., \(\operatorname {PauliCommute}(\operatorname {fluxChecks}(G, \mathrm{cycles}, p),\; \operatorname {fluxChecks}(G, \mathrm{cycles}, q))\) holds. Both \(B_p\) and \(B_q\) are pure \(Z\)-type operators, so they commute.
This follows directly from allChecks_pairwise_commute_flux_flux.
Let \(\mathrm{data}\) be a DeformedCodeData for \(G\) and checks, and suppose all original checks pairwise commute, i.e., \(\operatorname {PauliCommute}(\mathrm{checks}(i), \mathrm{checks}(j))\) for all \(i, j \in J\). Then for any \(i, j \in J\), the deformed checks commute:
i.e., \(\operatorname {PauliCommute}(\operatorname {deformedOriginalChecks}(G, \mathrm{checks}, \mathrm{data}, i),\; \operatorname {deformedOriginalChecks}(G, \mathrm{checks}, \mathrm{data}, j))\). On edge qubits both are pure \(Z\)-type; on vertex qubits commutation is inherited from the original checks.
This follows directly from allChecks_pairwise_commute_deformed_deformed.
Assume for every cycle \(c \in C\) and every vertex \(v \in V\), the number of edges in the cycle \(c\) incident to \(v\) is even. Then for any \(v \in V\) and \(p \in C\), the Gauss’s law operator and flux operator commute:
The symplectic inner product counts the overlap of the \(X\)-support of \(A_v\) with the \(Z\)-support of \(B_p\), which is the number of edges in \(p\) incident to \(v\). For a valid cycle, this is always even (\(0\) or \(2\)).
This follows directly from allChecks_pairwise_commute_gaussLaw_flux.
Let \(\mathrm{data}\) be a DeformedCodeData for \(G\) and checks. For any vertex \(v \in V\) and index \(j \in J\), the Gauss’s law operator and deformed check commute:
The boundary condition ensures the anticommutation signs cancel.
This follows directly from allChecks_pairwise_commute_gaussLaw_deformed.
Let \(\mathrm{data}\) be a DeformedCodeData for \(G\) and checks. For any cycle index \(p \in C\) and check index \(j \in J\), the flux operator and deformed check commute:
\(B_p\) is pure \(Z\)-type and acts only on edges; \(\tilde{s}_j\) has no \(X\)-support on edges. Since \(Z\) commutes with \(Z\) and \(B_p\) does not act on vertex qubits, they commute.
By commutativity of the Pauli commutation relation (rewriting via \(\operatorname {pauliCommute\_ comm}\)), the goal reduces to showing \(\operatorname {PauliCommute}(\operatorname {deformedOriginalChecks}(G, \mathrm{checks}, \mathrm{data}, j),\; \operatorname {fluxChecks}(G, \mathrm{cycles}, p))\). This follows directly from allChecks_pairwise_commute_deformed_flux.
Let \(\mathrm{data}\) be a DeformedCodeData for \(G\) and checks. Suppose all cycles satisfy the evenness condition (for every \(c \in C\) and \(v \in V\), the number of edges in cycle \(c\) incident to \(v\) is even), and all original checks pairwise commute. Then for any two check indices \(a, b \in \operatorname {CheckIndex}(V, C, J)\):
This follows directly from allChecks_commute.
Let \(\mathrm{data}\) be a DeformedCodeData for \(G\) and checks. For any check index \(a \in \operatorname {CheckIndex}(V, C, J)\):
This follows directly from allChecks_self_inverse.
The deformed code forms a valid stabilizer code on the extended qubit system \(V \oplus E(G)\). The check index type is \(\operatorname {CheckIndex}(V, C, J) = V \oplus C \oplus J\), and the check function is \(\operatorname {deformedCodeChecks}\). The pairwise commutation of all checks is established by allChecks_commute.
Formally, given a graph \(G\), cycles, original checks, deformed code data \(\mathrm{data}\), the cycle evenness hypothesis, and the hypothesis that original checks pairwise commute, we define:
with index type \(I = \operatorname {CheckIndex}(V, C, J)\) and check map \(\operatorname {deformedCodeChecks}(G, \mathrm{cycles}, \mathrm{checks}, \mathrm{data})\).
The number of physical qubits in the deformed stabilizer code is \(|V| + |E(G)|\):
By simplification using the definition of \(\operatorname {numQubits}\) and the fact that the cardinality of a sum type \(V \oplus E(G)\) equals \(|V| + |E(G)|\) (i.e., \(\operatorname {Fintype.card\_ sum}\)), the result follows.
The number of checks in the deformed stabilizer code is \(|V| + |C| + |J|\):
By simplification using the definition of \(\operatorname {numChecks}\), it suffices to show \(|\operatorname {CheckIndex}(V, C, J)| = |V| + |C| + |J|\). We establish an equivalence \(\operatorname {CheckIndex}(V, C, J) \simeq V \oplus C \oplus J\) by the bijection:
\(\operatorname {gaussLaw}(v) \mapsto \operatorname {inl}(v)\),
\(\operatorname {flux}(p) \mapsto \operatorname {inr}(\operatorname {inl}(p))\),
\(\operatorname {deformed}(j) \mapsto \operatorname {inr}(\operatorname {inr}(j))\),
with left and right inverses verified by case analysis (each case holdsby reflexivity). Applying \(\operatorname {Fintype.card\_ congr}\) with this equivalence, then using \(\operatorname {Fintype.card\_ sum}\) twice and associativity of addition, we obtain the result.
For any vertex \(v \in V\), the Gauss’s law operator \(A_v = \operatorname {gaussLawChecks}(G, v)\) is a member of the stabilizer group of the deformed stabilizer code:
We observe that \(\operatorname {gaussLawChecks}(G, v) = \operatorname {check}(\operatorname {deformedStabilizerCode}(\ldots ), \operatorname {gaussLaw}(v))\). This holds by reflexivity. Rewriting with this identity, the result follows from the fact that every check of a stabilizer code lies in its stabilizer group (check_mem_stabilizerGroup).
For any cycle index \(p \in C\), the flux operator \(B_p = \operatorname {fluxChecks}(G, \mathrm{cycles}, p)\) is a member of the stabilizer group of the deformed stabilizer code:
We observe that \(\operatorname {fluxChecks}(G, \mathrm{cycles}, p) = \operatorname {check}(\operatorname {deformedStabilizerCode}(\ldots ), \operatorname {flux}(p))\). This holds by reflexivity. Rewriting with this identity, the result follows from check_mem_stabilizerGroup.
For any check index \(j \in J\), the deformed check \(\tilde{s}_j = \operatorname {deformedOriginalChecks}(G, \mathrm{checks}, \mathrm{data}, j)\) is a member of the stabilizer group of the deformed stabilizer code:
We observe that \(\operatorname {deformedOriginalChecks}(G, \mathrm{checks}, \mathrm{data}, j) = \operatorname {check}(\operatorname {deformedStabilizerCode}(\ldots ), \operatorname {deformed}(j))\). This holds by reflexivity. Rewriting with this identity, the result follows from check_mem_stabilizerGroup.
For any vertex \(v \in V\), the Gauss’s law operator \(A_v\) lies in the centralizer of the deformed stabilizer code:
Let \(a\) be an arbitrary check index. We observe that \(\operatorname {gaussLawChecks}(G, v) = \operatorname {check}(\operatorname {deformedStabilizerCode}(\ldots ), \operatorname {gaussLaw}(v))\) by reflexivity. Rewriting with this identity, the commutation follows from the checks_commute property of the deformed stabilizer code applied to the indices \(\operatorname {gaussLaw}(v)\) and \(a\).
For any cycle index \(p \in C\), the flux operator \(B_p\) lies in the centralizer of the deformed stabilizer code:
Let \(a\) be an arbitrary check index. We observe that \(\operatorname {fluxChecks}(G, \mathrm{cycles}, p) = \operatorname {check}(\operatorname {deformedStabilizerCode}(\ldots ), \operatorname {flux}(p))\) by reflexivity. Rewriting with this identity, the commutation follows from the checks_commute property of the deformed stabilizer code applied to the indices \(\operatorname {flux}(p)\) and \(a\).
For any check index \(j \in J\), the deformed check \(\tilde{s}_j\) lies in the centralizer of the deformed stabilizer code:
Let \(a\) be an arbitrary check index. We observe that \(\operatorname {deformedOriginalChecks}(G, \mathrm{checks}, \mathrm{data}, j) = \operatorname {check}(\operatorname {deformedStabilizerCode}(\ldots ), \operatorname {deformed}(j))\) by reflexivity. Rewriting with this identity, the commutation follows from the checks_commute property of the deformed stabilizer code applied to the indices \(\operatorname {deformed}(j)\) and \(a\).
For any vertex \(v \in V\), the Gauss’s law check in the deformed stabilizer code is pure \(X\)-type, i.e., its \(Z\)-vector is zero:
This follows directly from gaussLawChecks_pure_X.
For any cycle index \(p \in C\), the flux check in the deformed stabilizer code is pure \(Z\)-type, i.e., its \(X\)-vector is zero:
This follows directly from fluxChecks_pure_Z.
For any check index \(j \in J\) and any edge \(e \in E(G)\), the deformed check in the deformed stabilizer code has no \(X\)-support on the edge qubit \(e\):
This follows directly from deformedOriginalChecks_no_xSupport_on_edges.
The product of all Gauss’s law checks in the deformed stabilizer code equals the logical operator \(L = \prod _{v \in V} X_v\):
By converting using gaussLawChecks_product_eq_logical, the two sides are shown to be equal.