2 Rem 3: Notation for Stabilizer Codes
Let \(V\) be a finite type. The symplectic inner product of two Pauli operators \(P, Q : \operatorname {PauliOp}(V)\) is defined as
This determines commutation in the full Pauli group: \(P\) and \(Q\) commute if and only if \(\langle P,Q\rangle _{\mathrm{symp}} = 0\).
Two Pauli operators \(P, Q : \operatorname {PauliOp}(V)\) commute (in the full Pauli group, including phases) if their symplectic inner product vanishes:
For any Pauli operator \(P : \operatorname {PauliOp}(V)\),
Unfolding the definition of \(\langle P, P \rangle _{\mathrm{symp}}\), we have
It suffices to show each summand is zero. For each \(v\), by commutativity of multiplication in \(\mathbb {Z}/2\mathbb {Z}\) we have \(P.z_v \cdot P.x_v = P.x_v \cdot P.z_v\), so the summand equals \(P.x_v \cdot P.z_v + P.x_v \cdot P.z_v = 0\) since every element of \(\mathbb {Z}/2\mathbb {Z}\) satisfies \(a + a = 0\). Hence the entire sum is zero.
Every Pauli operator commutes with itself: for any \(P : \operatorname {PauliOp}(V)\),
Unfolding the definition of \(\operatorname {PauliCommute}\), the goal reduces to \(\langle P, P \rangle _{\mathrm{symp}} = 0\), which holds by simplification using the theorem symplecticInner_self.
For any Pauli operators \(P, Q : \operatorname {PauliOp}(V)\),
Unfolding the definitions, both directions amount to showing \(\langle P,Q \rangle _{\mathrm{symp}} = 0 \iff \langle Q,P \rangle _{\mathrm{symp}} = 0\). For each direction, we convert the goal using the fact that at each coordinate \(v\), the summand \(P.x_v \cdot Q.z_v + P.z_v \cdot Q.x_v\) equals \(Q.x_v \cdot P.z_v + Q.z_v \cdot P.x_v\) by ring arithmetic. Hence the two sums are equal, and the equivalence follows.
For any Pauli operator \(Q : \operatorname {PauliOp}(V)\),
By simplification: the identity operator has \(x_v = 0\) and \(z_v = 0\) for all \(v\), so each summand \(1.x_v \cdot Q.z_v + 1.z_v \cdot Q.x_v = 0 \cdot Q.z_v + 0 \cdot Q.x_v = 0\). The sum of zeros is zero.
For any Pauli operator \(P : \operatorname {PauliOp}(V)\),
By simplification: the identity operator has \(x_v = 0\) and \(z_v = 0\) for all \(v\), so each summand \(P.x_v \cdot 0 + P.z_v \cdot 0 = 0\). The sum of zeros is zero.
For any Pauli operator \(Q : \operatorname {PauliOp}(V)\), \(\operatorname {PauliCommute}(1, Q)\).
Unfolding \(\operatorname {PauliCommute}\), the goal is \(\langle 1, Q \rangle _{\mathrm{symp}} = 0\), which holds by simplification.
For any Pauli operator \(P : \operatorname {PauliOp}(V)\), \(\operatorname {PauliCommute}(P, 1)\).
Unfolding \(\operatorname {PauliCommute}\), the goal is \(\langle P, 1 \rangle _{\mathrm{symp}} = 0\), which holds by simplification.
For any Pauli operators \(P, Q, R : \operatorname {PauliOp}(V)\),
Expanding the definitions of the symplectic inner product and multiplication of Pauli operators (where \((P \cdot Q).x_v = P.x_v + Q.x_v\) and \((P \cdot Q).z_v = P.z_v + Q.z_v\) in \(\mathbb {Z}/2\mathbb {Z}\)), the left-hand side becomes
Distributing the sum and applying the distributive law of \(\mathbb {Z}/2\mathbb {Z}\), this equals the sum of the right-hand side terms. The equality of the summands at each coordinate \(v\) follows by ring arithmetic.
For any Pauli operators \(P, Q, R : \operatorname {PauliOp}(V)\),
Expanding the definitions, the left-hand side becomes
Distributing and rearranging the sum, this equals the right-hand side. The equality of summands at each coordinate follows by ring arithmetic.
A stabilizer code on qubits labeled by a finite type \(V\) consists of:
A finite index type \(I\) for stabilizer checks,
A map \(\operatorname {check} : I \to \operatorname {PauliOp}(V)\) assigning a Pauli operator to each check index,
A commutativity condition: for all \(i, j \in I\), \(\operatorname {PauliCommute}(\operatorname {check}(i), \operatorname {check}(j))\).
The stabilizer group \(S\) of a stabilizer code \(C\) is the subgroup of \(\operatorname {PauliOp}(V)\) generated by the set of checks \(\{ \operatorname {check}(i) \mid i \in I\} \):
For any stabilizer code \(C\) and check index \(i \in I\), the check \(\operatorname {check}(i)\) belongs to the stabilizer group:
We apply the fact that the closure of a set contains the set itself. Since \(\operatorname {check}(i)\) is in the range of the check map, it belongs to \(\operatorname {Set.range}(\operatorname {check})\), which is contained in \(\operatorname {Subgroup.closure}(\operatorname {Set.range}(\operatorname {check})) = S\).
A Pauli operator \(P\) is in the centralizer of a stabilizer code \(C\) if it commutes (in the full Pauli group) with every stabilizer check:
The centralizer set of a stabilizer code \(C\) is the set of all Pauli operators in the centralizer:
The identity operator belongs to the centralizer of any stabilizer code \(C\):
Let \(i \in I\) be arbitrary. We need to show \(\operatorname {PauliCommute}(1, \operatorname {check}(i))\). This follows directly from the fact that the identity commutes with any Pauli operator on the left.
For any check index \(i \in I\), the check \(\operatorname {check}(i)\) belongs to the centralizer of \(C\):
Let \(j \in I\) be arbitrary. We need to show \(\operatorname {PauliCommute}(\operatorname {check}(i), \operatorname {check}(j))\). This follows directly from the commutativity condition of the stabilizer code \(C\).
A Pauli operator \(P\) is a non-trivial logical operator of a stabilizer code \(C\) if:
\(P\) is in the centralizer: \(\operatorname {inCentralizer}(C, P)\),
\(P\) is not in the stabilizer group: \(P \notin S\),
\(P\) is not the identity: \(P \neq 1\).
If \(P\) is a non-trivial logical operator of \(C\), then \(P\) is in the centralizer.
This is the first component of the conjunction defining \(\operatorname {isLogicalOp}\).
If \(P\) is a non-trivial logical operator of \(C\), then \(P \notin S\).
This is the first component of the second part of the conjunction defining \(\operatorname {isLogicalOp}\).
If \(P\) is a non-trivial logical operator of \(C\), then \(P \neq 1\).
This is the second component of the second part of the conjunction defining \(\operatorname {isLogicalOp}\).
The code distance of a stabilizer code \(C\) is the minimum weight of a non-trivial logical operator:
If no logical operators exist, this returns \(0\).
The number of physical qubits of a stabilizer code \(C\) on qubit type \(V\) is
The number of stabilizer checks of a stabilizer code \(C\) is
A stabilizer code \(C\) has parameters \([\! [n, k, d]\! ]\) if:
\(|V| = n\) (the number of physical qubits is \(n\)),
\(n - \operatorname {numChecks}(C) = k\) (the number of encoded logical qubits is \(k\)),
\(d(C) = d\) (the code distance is \(d\)).
The weight of the \(i\)-th stabilizer check of a code \(C\) is the weight of the corresponding Pauli operator:
The qubit degree of a qubit \(v \in V\) in a stabilizer code \(C\) is the number of checks that act non-trivially on \(v\):
A stabilizer code \(C\) is a quantum low-density parity-check (qLDPC) code with parameters \((w, c)\) if:
Each check has weight bounded by \(w\): \(\forall \, i \in I,\; \operatorname {checkWeight}(C, i) \leq w\),
Each qubit participates in at most \(c\) checks: \(\forall \, v \in V,\; \operatorname {qubitDegree}(C, v) \leq c\).
The identity operator is not a non-trivial logical operator of any stabilizer code \(C\):
Suppose for contradiction that \(\operatorname {isLogicalOp}(C, 1)\) holds. Decomposing this, we obtain \(h_1\) (centralizer membership), \(h_2\) (not in stabilizer group), and \(h_3 : 1 \neq 1\). But \(h_3\) contradicts reflexivity, so the assumption is false.
For any stabilizer code \(C\), every element of the stabilizer group is in the centralizer:
Let \(P \in S\). We proceed by induction on the proof that \(P\) belongs to the subgroup closure.
Generator case: If \(P = \operatorname {check}(i)\) for some \(i\) (i.e., \(P\) is in the generating set \(\operatorname {Set.range}(\operatorname {check})\)), then we obtain \(i\) such that \(P = \operatorname {check}(i)\), and conclude by the lemma that each check is in the centralizer.
Identity case: If \(P = 1\), then \(\operatorname {inCentralizer}(C, 1)\) holds by the lemma that the identity is in the centralizer.
Multiplication case: If \(P = a \cdot b\) where \(a, b\) are in the closure, and we have by induction that \(\operatorname {inCentralizer}(C, a)\) and \(\operatorname {inCentralizer}(C, b)\), then for any check index \(i\), we need to show \(\operatorname {PauliCommute}(a \cdot b, \operatorname {check}(i))\), i.e., \(\langle a \cdot b, \operatorname {check}(i) \rangle _{\mathrm{symp}} = 0\). By the additivity of the symplectic inner product in the first argument, this equals \(\langle a, \operatorname {check}(i) \rangle _{\mathrm{symp}} + \langle b, \operatorname {check}(i) \rangle _{\mathrm{symp}}\). From the inductive hypotheses, both terms are \(0\), so the sum is \(0 + 0 = 0\).
Inverse case: If \(P = a^{-1}\) and \(\operatorname {inCentralizer}(C, a)\) holds by induction, then since every Pauli operator is its own inverse (\(a^{-1} = a\)), we have \(\operatorname {inCentralizer}(C, a^{-1}) = \operatorname {inCentralizer}(C, a)\), which holds by the inductive hypothesis.
No stabilizer check is a non-trivial logical operator: for any \(i \in I\),
Suppose for contradiction that \(\operatorname {isLogicalOp}(C, \operatorname {check}(i))\) holds. Decomposing this, we obtain the condition that \(\operatorname {check}(i) \notin S\). But this contradicts the lemma that \(\operatorname {check}(i) \in S\).