1 Rem 1: Stabilizer Code Convention
Throughout this work, we consider an \([[n,k,d]]\) quantum low-density parity-check (qLDPC) stabilizer code on \(n\) physical qubits, encoding \(k\) logical qubits with distance \(d\). The code is specified by a set of stabilizer checks \(\{ s_i\} \). A logical operator \(L\) is a Pauli operator that commutes with all stabilizers but is not itself a stabilizer. By choosing an appropriate single-qubit basis for each physical qubit, we ensure that the logical operator \(L\) being measured is a product of Pauli-\(X\) matrices:
where \(\operatorname {supp}(L)\) denotes the set of qubits on which \(L\) acts non-trivially.
The four single-qubit Pauli operators form an inductive type StabPauliType with constructors:
\(I\) — the identity,
\(X\) — the Pauli-\(X\) (bit flip),
\(Y\) — the Pauli-\(Y\),
\(Z\) — the Pauli-\(Z\) (phase flip).
Multiplication of single-qubit Pauli types (ignoring global phase) is defined by the rules:
\(I \cdot p = p\) and \(p \cdot I = p\) for all \(p\),
\(X \cdot X = Y \cdot Y = Z \cdot Z = I\),
\(X \cdot Y = Z\), \(Y \cdot X = Z\), \(Y \cdot Z = X\), \(Z \cdot Y = X\), \(Z \cdot X = Y\), \(X \cdot Z = Y\).
A single-qubit Pauli type \(p\) acts nontrivially if and only if \(p \neq I\). That is, isNontrivial returns true for \(X\), \(Y\), and \(Z\), and false for \(I\).
A single-qubit Pauli type \(p\) is \(X\)-type if \(p \in \{ X, Y\} \); i.e., it involves the \(X\) component.
A single-qubit Pauli type \(p\) is \(Z\)-type if \(p \in \{ Z, Y\} \); i.e., it involves the \(Z\) component.
Two single-qubit Pauli types \(p\) and \(q\) commute if any of the following holds: one of them is \(I\), or \(p = q\). Explicitly, the only anticommuting pairs are \(\{ X,Z\} \), \(\{ X,Y\} \), and \(\{ Y,Z\} \).
For all single-qubit Pauli types \(p\) and \(q\), \(\operatorname {commutes}(p, q) = \operatorname {commutes}(q, p)\).
We case-split on all combinations of \(p\) and \(q\). In each of the \(4 \times 4 = 16\) cases, the equality holds by reflexivity.
A Pauli operator on \(n\) qubits is a structure consisting of:
a function \(\texttt{paulis} : \operatorname {Fin}(n) \to \texttt{StabPauliType}\) assigning a single-qubit Pauli type to each qubit, and
a global phase \(\texttt{phase} \in \mathbb {Z}/4\mathbb {Z}\), where \(0 = +1\), \(1 = +i\), \(2 = -1\), \(3 = -i\).
The identity operator on \(n\) qubits is defined as \(\texttt{paulis}(i) = I\) for all \(i \in \operatorname {Fin}(n)\) and \(\texttt{phase} = 0\).
The support of a Pauli operator \(P\) on \(n\) qubits is the finite set
The \(X\)-type support of a Pauli operator \(P\) is the finite set of qubits where \(P\) acts as \(X\) or \(Y\):
The \(Z\)-type support of a Pauli operator \(P\) is the finite set of qubits where \(P\) acts as \(Z\) or \(Y\):
Two Pauli operators \(P\) and \(Q\) on \(n\) qubits commute (ignoring global phase) if and only if the number of positions where their single-qubit Pauli types anticommute is even:
A Pauli operator \(P\) on \(n\) qubits is purely \(X\)-type if, for every qubit \(i\), \(P.\texttt{paulis}(i) \in \{ I, X\} \).
Given a finite set \(S \subseteq \operatorname {Fin}(n)\), the pure \(X\)-type operator \(\operatorname {pureX}(S)\) is the Pauli operator with
and phase \(0\).
For any finite set \(S \subseteq \operatorname {Fin}(n)\), the operator \(\operatorname {pureX}(S)\) is purely \(X\)-type.
Let \(i\) be an arbitrary qubit. By the definition of \(\operatorname {pureX}\), we split on whether \(i \in S\). If \(i \in S\), then \(\operatorname {pureX}(S).\texttt{paulis}(i) = X\). If \(i \notin S\), then \(\operatorname {pureX}(S).\texttt{paulis}(i) = I\). In both cases the result is in \(\{ I, X\} \), and the claim follows by simplification.
For any finite set \(S \subseteq \operatorname {Fin}(n)\),
By extensionality, it suffices to show that for each \(i\), \(i \in \operatorname {supp}(\operatorname {pureX}(S))\) if and only if \(i \in S\). We unfold the definitions of support and \(\operatorname {pureX}\) and split on whether \(i \in S\). If \(i \in S\), then \(\operatorname {pureX}(S).\texttt{paulis}(i) = X \neq I\), so \(i\) is in the support. If \(i \notin S\), then \(\operatorname {pureX}(S).\texttt{paulis}(i) = I\), so \(i\) is not in the support. Both directions follow by simplification.
For any finite set \(S \subseteq \operatorname {Fin}(n)\),
By extensionality, it suffices to show for each \(i\) that \(i \in \operatorname {xSupp}(\operatorname {pureX}(S))\) if and only if \(i \in S\). We unfold the definitions and split on whether \(i \in S\). If \(i \in S\), then \(\operatorname {pureX}(S).\texttt{paulis}(i) = X\), which is \(X\)-type. If \(i \notin S\), then \(\operatorname {pureX}(S).\texttt{paulis}(i) = I\), which is not \(X\)-type. Both cases follow by simplification using the definition of isXType.
For any finite set \(S \subseteq \operatorname {Fin}(n)\),
By extensionality, it suffices to show for each \(i\) that \(i \notin \operatorname {zSupp}(\operatorname {pureX}(S))\). We unfold the definitions and split on whether \(i \in S\). If \(i \in S\), then \(\operatorname {pureX}(S).\texttt{paulis}(i) = X\), which is not \(Z\)-type. If \(i \notin S\), then \(\operatorname {pureX}(S).\texttt{paulis}(i) = I\), which is also not \(Z\)-type. In both cases the claim follows by simplification using the definition of isZType.
A stabilizer group on \(n\) qubits is a structure consisting of:
a set of generating Pauli operators \(\texttt{generators} \subseteq \texttt{PauliOp}(n)\),
a proof that the generating set is finite,
a proof that all generators mutually commute: for all \(s_1, s_2 \in \texttt{generators}\), \(\operatorname {commutes}(s_1, s_2)\).
An \([[n, k, d]]\) stabilizer code is a structure consisting of:
the number of physical qubits \(n \in \mathbb {N}\),
the number of logical qubits \(k \in \mathbb {N}\),
the code distance \(d \in \mathbb {N}\),
a stabilizer group on \(n\) qubits,
a constraint \(n \geq k\),
a positivity constraint \(d {\gt} 0\).
A Pauli operator \(P\) on \(C.n\) qubits commutes with the stabilizer group of a code \(C\) if and only if it commutes with every generator:
The centralizer of a stabilizer code \(C\) is the set of all Pauli operators on \(C.n\) qubits that commute with all stabilizers:
A Pauli operator \(P\) is in the stabilizer group of code \(C\) if there exists a finite set of generators \(\texttt{gens} \subseteq C.\texttt{stabilizers}.\texttt{generators}\) such that:
if \(\texttt{gens} = \emptyset \) then \(P\) equals the identity, and
\(P\) is one of the generators, or \(P\) is the identity.
(This is a simplified definition; a full treatment would define the group generated by the generators.)
A logical operator for a stabilizer code \(C\) is a structure consisting of:
an underlying Pauli operator \(\texttt{op} : \texttt{PauliOp}(C.n)\),
a proof that \(\texttt{op}\) commutes with all stabilizers,
a proof that \(\texttt{op}\) is not in the stabilizer group.
The support of a logical operator \(L\) is \(\operatorname {supp}(L) := \operatorname {supp}(L.\texttt{op})\).
The \(X\)-type support of a logical operator \(L\) is \(\operatorname {xSupp}(L) := \operatorname {xSupp}(L.\texttt{op})\).
The \(Z\)-type support of a logical operator \(L\) is \(\operatorname {zSupp}(L) := \operatorname {zSupp}(L.\texttt{op})\).
An \(X\)-type logical operator for a stabilizer code \(C\) extends a logical operator with the additional property that the underlying Pauli operator is purely \(X\)-type. This captures the convention
For an \(X\)-type logical operator \(L\), the support equals the \(X\)-type support:
By extensionality, it suffices to show for each qubit \(i\) that \(i \in \operatorname {supp}(L) \Leftrightarrow i \in \operatorname {xSupp}(L)\). We unfold the definitions and use the fact that \(L\) is purely \(X\)-type, so \(L.\texttt{paulis}(i) \in \{ I, X\} \). We consider two cases:
If \(L.\texttt{paulis}(i) = I\), then \(i \notin \operatorname {supp}(L)\) (since \(I = I\)) and \(\texttt{isXType}(I) = \texttt{false}\), so \(i \notin \operatorname {xSupp}(L)\). By simplification, both sides are false.
If \(L.\texttt{paulis}(i) = X\), then \(X \neq I\) so \(i \in \operatorname {supp}(L)\), and \(\texttt{isXType}(X) = \texttt{true}\) so \(i \in \operatorname {xSupp}(L)\). Both directions are verified by the decide tactic.
For an \(X\)-type logical operator \(L\), the \(Z\)-type support is empty:
By extensionality, it suffices to show that no qubit \(i\) belongs to \(\operatorname {zSupp}(L)\). We unfold the definitions and use the purely \(X\)-type property of \(L\), so \(L.\texttt{paulis}(i) \in \{ I, X\} \). We consider two cases:
If \(L.\texttt{paulis}(i) = I\), then \(\texttt{isZType}(I) = \texttt{false}\), so \(i \notin \operatorname {zSupp}(L)\).
If \(L.\texttt{paulis}(i) = X\), then \(\texttt{isZType}(X) = \texttt{false}\), so \(i \notin \operatorname {zSupp}(L)\).
Both cases follow by simplification.
Given a stabilizer code \(C\) and a finite set \(S \subseteq \operatorname {Fin}(C.n)\), together with proofs that \(\operatorname {pureX}(S)\) commutes with all stabilizers and is not in the stabilizer group, we construct an \(X\)-type logical operator with underlying operator \(\operatorname {pureX}(S)\). The purely \(X\)-type property follows from the lemma that \(\operatorname {pureX}(S)\) is purely \(X\)-type.
For a stabilizer code \(C\), a finite set \(S\), and appropriate proofs \(h_1, h_2\),
By simplification using the definitions of fromSupport and LogicalOp.support, together with the lemma that \(\operatorname {supp}(\operatorname {pureX}(S)) = S\).
For an \(X\)-type logical operator \(L\) over a stabilizer code \(C\), the Pauli content of \(L\) on each qubit matches \(\operatorname {pureX}\) applied to its support. That is,
This is the formal statement that \(L = \prod _{v \in \operatorname {supp}(L)} X_v\) (ignoring global phase).
By extensionality, it suffices to show that for each qubit \(i\), \(L.\texttt{op}.\texttt{paulis}(i) = \operatorname {pureX}(\operatorname {supp}(L)).\texttt{paulis}(i)\). We unfold the definitions and split on whether \(i \in \operatorname {supp}(L)\):
If \(i \in \operatorname {supp}(L)\): By the definition of support, \(L.\texttt{paulis}(i) \neq I\). Since \(L\) is purely \(X\)-type, \(L.\texttt{paulis}(i) \in \{ I, X\} \). Because \(L.\texttt{paulis}(i) \neq I\), we conclude \(L.\texttt{paulis}(i) = X\). On the other hand, \(\operatorname {pureX}(\operatorname {supp}(L)).\texttt{paulis}(i) = X\) since \(i \in \operatorname {supp}(L)\).
If \(i \notin \operatorname {supp}(L)\): By the definition of support (filtering and double negation elimination), \(L.\texttt{paulis}(i) = I\). On the other hand, \(\operatorname {pureX}(\operatorname {supp}(L)).\texttt{paulis}(i) = I\) since \(i \notin \operatorname {supp}(L)\).
In both cases the equality holds.
A stabilizer code \(C\) is Low-Density Parity-Check (LDPC) if there exist constants bounding:
Maximum check weight \(w_{\max } \in \mathbb {N}\): for every generator \(s \in C.\texttt{stabilizers}.\texttt{generators}\), \(|\operatorname {supp}(s)| \leq w_{\max }\).
Maximum qubit degree \(\Delta _{\max } \in \mathbb {N}\): for every qubit \(i \in \operatorname {Fin}(C.n)\), the number of generators whose support contains \(i\) is at most \(\Delta _{\max }\).