Dependencies

\(p\) and \(q\) *anticommute* when \(pq = -qp\). Anticommutation with a stabilizer generator is the syndrome signal that detects an error.

Two \(n\)-qubit Pauli operators *anticommute at qubit \(i\)* if their \(i\)-th single-qubit operators are distinct and neither is \(I\). This is the local test whose global parity governs commutation.

\(B_1 = \operatorname {im} \partial _2 \le C_1\): the chains obtained from an \(X\)-check, i.e. the products of stabilizer generators.

The centralizer \(\mathcal{C}(\mathcal{S})\) of a stabilizer group inside \(\mathcal{P}_n\): the Pauli operators commuting with every element of \(\mathcal{S}\). These are exactly the operators that preserve the codespace, so they are the candidates for logical operators.

The \(X\)-type Pauli operator supported on the qubits in a \(1\)-chain: place \(X\) where the chain is \(1\) and \(I\) elsewhere. This is the dictionary between \(\mathbb {F}_2\) linear algebra and \(\mathcal{P}_n\).

The \(Z\)-type counterpart of definition 59, used for the dual side of the CSS code.

The check matrix of a list of \(\mathcal{P}_n\) elements: the matrix over \(\mathbb {F}_2\) whose rows are the symplectic vectors (definition 14) of the listed generators. For a CSS code it is block diagonal, carrying the two classical parity-check matrices \(H_X\) and \(H_Z\) on the diagonal.

An \([[n,k,d]]\) code: a definition 38 bundled with a proof of definition 44. The headline results of this development are inhabitants of this type.

The codespace of \(\mathcal{S}\) is the set of states stabilized by every element of \(\mathcal{S}\) — the simultaneous \(+1\) eigenspace. Logical information is stored here.

\(Z_1 = \ker \partial _1 \le C_1\). Under definition 59 these are exactly the chains whose \(X\) operator commutes with every \(Z\)-check.

The smallest code correcting an arbitrary single-qubit error, and the first non-CSS code in this development: its generators mix \(X\) and \(Z\) on the same qubit, so the CSS machinery does not apply and the distance argument is a direct search over weight-one and weight-two anti-witnesses.

The smallest error-*detecting* code, encoding two qubits with distance two. Its distance is closed by theorem 49.

A generator list is independent when no generator lies in the group generated by the others. The condition only sees the *set* of generators, so a repeated generator is invisible to it and it cannot tie the length of a list to \(n - k\); presentations (definition 40) use the stronger row independence of the check matrix instead.

The \([[144,12,12]]\) gross code as an inhabitant of definition 46 — the headline result of this development.

IBM’s gross code presented as a definition 38 with \(n = 144\) and \(k = 12\).

\(H_1 = Z_1 / B_1\) (definition 54, definition 55). The slogan of the whole framework is *logical operators are homology classes*: nontrivial logical operators correspond to nonzero classes in \(H_1\), and the code distance is the minimum weight of a chain representing a nonzero class.

A code *has distance \(d\)* when every nontrivial logical operator (definition 31) has weight at least \(d\), and some nontrivial logical operator has weight exactly \(d\). Both halves matter: the lower bound is the error-correction guarantee, the witness makes the value exact rather than merely a bound.

The abstract input to the CSS-from-homology machine: a length-three chain complex of \(\mathbb {F}_2\) vector spaces \(C_2 \xrightarrow {\partial _2} C_1 \xrightarrow {\partial _1} C_0\) with \(\partial _1 \partial _2 = 0\), where \(C_1\) is indexed by the physical qubits, \(C_0\) by the \(Z\)-checks and \(C_2\) by the \(X\)-checks. Every topological code in this development is an instance.

The parametric generalized-parity family with exactly two stabilizer generators, the all-\(X\) and all-\(Z\) operators. Distance two for every \(m\), again via theorem 49.

A state \(\psi \) is stabilized by \(g \in \mathcal{P}_n\) when \(g\psi = \psi \), i.e. \(\psi \) is a \(+1\) eigenvector of the unitary definition 5.

A bundled pair of logical \(\overline{X}\) and \(\overline{Z}\) operators for each of the \(k\) encoded qubits, packaged with the proofs that they are logical, are not stabilizers, and anticommute in the right pattern.

A *nontrivial* logical operator is one that acts on the encoded information rather than fixing it. The predicate has two conditions: \(g\) is in the centralizer, and no element of \(\mathcal{S}\) has the same operator part as \(g\).

The second condition is stronger than the familiar \(g \notin \mathcal{S}\) (which it implies, at \(s = g\)) and is what makes the CSS bridge arguments work: with only the weaker condition, \(g\) could differ from a stabilizer by a phase, which is not a nontrivial action on the codespace.

An element of the \(n\)-qubit Pauli group \(\mathcal{P}_n\) is a phase exponent in \(\mathbb {Z}_4\) together with an \(n\)-qubit Pauli operator (definition 3), i.e. a tensor product \(i^a\, P_1 \otimes \cdots \otimes P_n\). Every operator statement in this development is ultimately a statement about elements of \(\mathcal{P}_n\).

An \(n\)-qubit Pauli *operator* is a function \(\mathrm{Fin}\, n \to \{ I,X,Y,Z\} \), i.e. one single-qubit Pauli per qubit. Again this is the phase-free part.

An element of the single-qubit Pauli group \(\mathcal{P}_1 = \{ \, i^a P : a \in \mathbb {Z}_4,\ P \in \{ I,X,Y,Z\} \, \} \), represented as a pair of a phase exponent \(a \in \mathbb {Z}_4\) and an operator \(P\) (definition 1). Splitting the phase off from the operator is what makes the \(n\)-qubit multiplication rule computable.

A Pauli operator is *logical* when it lies in the centralizer definition 26, i.e. it commutes with every stabilizer and therefore maps the codespace to itself.

Multiplication of two phase-free \(n\)-qubit Pauli operators, returning a full group element: multiplying qubitwise produces a Pauli operator together with an accumulated phase in \(\mathbb {Z}_4\), since e.g. \(XZ = -iY\).

The four single-qubit Pauli *operators* \(I\), \(X\), \(Y\), \(Z\), taken without a phase. This is the operator part of a Pauli group element; the phase is tracked separately by definition 2.

The support of \(g \in \mathcal{P}_n\) is the set of qubits on which its operator part is not \(I\).

The unitary matrix \(i^a\, P_1 \otimes \cdots \otimes P_n\) on \((\mathbb {C}^2)^{\otimes n}\) represented by a Pauli group element. This is the semantic anchor of the formalization: it is what makes the syntactic bookkeeping over \(\mathbb {Z}_4 \times \{ I,X,Y,Z\} ^n\) a statement about operators on a Hilbert space.

The weight \(\operatorname {wt}(g)\) of a Pauli group element is the cardinality of its support (definition 8) — the number of qubits it acts on nontrivially. Code distance is a statement about weights.

The soundness map from presentations (definition 40) to stabilizer codes (definition 38): the code whose stabilizer group is the closure of the generators, of size \(2^{n-k}\) by theorem 41. Every concrete code in the library is built this way.

For every \(r \ge 3\), the CSS code built from the classical \([2^r-1, 2^r-1-r, 3]\) Hamming code, packaged with its distance; the Steane code (definition 87) is the case \(r = 3\). The columns of the check matrix are the nonzero vectors of \(\mathbb {F}_2^r\), so theorem 50 applies uniformly in \(r\). \(X\) on the first three qubits (columns \(1, 2, 3\), with \(1 \oplus 2 = 3\)) is the weight-three logical.

The bit-flip repetition code as a stabilizer code, with \(Z_i Z_{i+1}\) generators, packaged with its distance. It has distance one as a *quantum* code — a single phase error \(Z_0\) commutes with every check but anticommutes with the logical \(X^{\otimes n}\) — which is why it appears here as a degenerate reference point rather than as a usable code.

The planar \(L \times L\) rotated surface code, an \([[L^2, 1, L]]\) family. It runs on the same homological machinery as the toric code but with boundary, so \(\dim H_1 = 1\) rather than \(2\).

The rows of the check matrix (definition 18) are linearly independent over \(\mathbb {F}_2\). This is the computable criterion used to discharge the independence obligation of a presentation (definition 40); independent rows are in particular pairwise distinct, so no generator is listed twice.

The nine-qubit Shor code, a repetition code of cat states — historically the first quantum error-correcting code — packaged with its distance. It is degenerate: the two \(X\)-checks cannot tell the three qubits of a block apart, so \(Z_i Z_j\) within a block commutes with every check. It is a stabilizer, though, which is exactly what theorem 51 asks; \(X\) on the first block is the weight-three logical.

The finite data certifying that a bivariate-bicycle complex has no light cycles: an enumeration showing that every nonzero cycle of weight below the target floor would produce an impossible syndrome pattern.

An \([[n,k]]\) stabilizer code: a stabilizer group \(\mathcal{S}\) (definition 21) with \(k \le n\) and exactly \(|\mathcal{S}| = 2^{n-k}\) elements — and nothing else. The definition mentions no generators, so \(k\) is a property of the group (theorem 39); a choice of logical operators is derived data, bundled separately by definition 43. The type carries \(n\) and \(k\), so instantiating it *is* the theorem that the group encodes \(k\) qubits into \(n\).

A presentation of an \([[n,k]]\) code: a list of \(n - k\) phase-zero, pairwise commuting generators whose closure avoids \(-I\) and whose check-matrix rows are linearly independent (definition 19). Row independence rules out a repeated generator, so the length of the list is an honest count.

A definition 38 together with \(k\) pairs of logical operators (definition 34), one per encoded qubit, such that the pairs of distinct qubits commute. This is what the constructions that genuinely need a basis consume — logical Clifford actions, the encoding step of code concatenation — while distance (definition 44) lives on the bare code.

A *stabilizer group* is an abelian subgroup \(\mathcal{S} \le \mathcal{P}_n\) that does not contain \(-I\). The two conditions are exactly what is needed for the common \(+1\) eigenspace to be nonzero: commutativity makes the eigenspace projectors compatible, and excluding \(-I\) rules out the contradiction \(\psi = -\psi \).

The operator \(\sum _{g \in \mathcal{S}} g\), which is \(|\mathcal{S}|\) times the orthogonal projector onto the codespace. Summing over the group is the standard route to showing the codespace is nonzero.

The CSS code built from the classical \([7,4,3]\) Hamming code, with all-\(X\) and all-\(Z\) logical operators, packaged with its distance. The Hamming check matrix has as columns the seven nonzero vectors of \(\mathbb {F}_2^3\), so theorem 50 applies with the same three rows on both sides; \(X\) on qubits \(\{ 3,5,6\} \) is the weight-three logical.

For \(u = (u_X \mid u_Z)\) and \(v = (v_X \mid v_Z)\) in \(\mathbb {F}_2^{2n}\), the symplectic form \(\langle u, v \rangle = u_X \cdot v_Z + u_Z \cdot v_X \in \mathbb {F}_2\).

The linear-algebra shadow of a Pauli operator: an \(n\)-qubit Pauli operator is sent to a vector in \(\mathbb {F}_2^{2n}\), recording in its first \(n\) coordinates which qubits carry an \(X\) component and in its last \(n\) which carry a \(Z\) component (so \(Y\) contributes to both). Products of Paulis become sums of vectors, which is what turns questions about the group \(\mathcal{P}_n\) into linear algebra over \(\mathbb {F}_2\).

The \(L \times L\) square lattice on the torus, packaged as a definition 52: \(C_0\) is spanned by vertices, \(C_1\) by the \(2L^2\) edges (the physical qubits), \(C_2\) by faces, with \(\partial _2\) the face boundary and \(\partial _1\) the edge boundary.

The \(L \times L\) toric code presented as a definition 38 with \(n = 2L^2\) and \(k = 2\).

The natural generating set has \(2L^2\) elements, two more than the \(n - k = 2L^2 - 2\) that a presentation (definition 40) demands, because the vertex checks multiply to the identity and so do the face checks. The packaging therefore uses a *trimmed* list, and the homological identities are what prove the trimmed list generates the same subgroup.

The \([[2L^2, 2, L]]\) toric code as an inhabitant of definition 46, for every \(L \ge 2\).

\(H_1\) of definition 65, i.e. the first homology of the torus with \(\mathbb {F}_2\) coefficients.

\(\varphi : H_1 \to \mathbb {F}_2^2\), \([c] \mapsto (h(c), v(c))\), well defined by theorem 70.

\(h(c) \in \mathbb {F}_2\) counts, modulo two, the vertical edges of the chain \(c\) crossing a fixed horizontal cut of the torus — the number of times \(c\) wraps horizontally.

The vertical counterpart of definition 68.

The data exhibiting one bivariate-bicycle complex as a free double cover of another: a deck transformation \(\sigma \) of order two acting freely, commuting with both boundary maps, with the base recovered as the quotient. The gross \([[144,12,12]]\) code covers the \([[72,12,6]]\) base exactly this way, and the doubling of the distance from \(6\) to \(12\) is what the cover is used to prove.

A Pauli group element whose operator part uses only \(I\) and \(X\), with trivial phase.

A Pauli group element whose operator part uses only \(I\) and \(Z\), with trivial phase. A CSS code is one whose stabilizer is generated by elements each of which is \(X\)-type (definition 47) or \(Z\)-type.

Every nonzero class in the homology of the base bivariate-bicycle complex is represented only by chains of weight at least six, and six is attained.

\(B_1 \le Z_1\).

\(\partial _1(\partial _2 c) = 0\) for every \(c \in C_2\).

A lower bound on the weight of every chain representing a nonzero class in \(H_1\) (and dually) transfers to a lower bound on the weight of every nontrivial logical operator.

\(X(c + c') = X(c) \cdot X(c')\): addition of chains over \(\mathbb {F}_2\) corresponds to multiplication of \(X\)-type Paulis.

Two stabilizer codes (definition 38) on \(n\) qubits with the same stabilizer group encode the same number of logical qubits.

Every stabilizer group has a state in its codespace. A stabilizer code is therefore never vacuous.

Any two elements of \(\mathcal{P}_n\) either commute or anticommute — there is no third case.

Two elements of \(\mathcal{P}_n\) commute if and only if the number of qubits at which they anticommute (definition 10) is even.

Two elements of \(\mathcal{P}_n\) commute if and only if their symplectic vectors are orthogonal under definition 16. This is the bridge that lets the whole theory be done with linear algebra over \(\mathbb {F}_2\): an abelian subgroup becomes a self-orthogonal subspace.

Let a CSS code have \(Z\)-checks and \(X\)-checks supported on the rows of two classical parity-check matrices. If both matrices have nonzero, pairwise distinct columns — both classical codes have distance at least \(3\) — and some nontrivial logical operator of weight \(3\) exists, then the code has distance exactly \(3\).

As theorem 50, except that the checks need not separate every pair of qubits. Suppose both check matrices have nonzero columns; that whenever no \(Z\)-row separates qubits \(i \ne j\), the operator \(X_i X_j\) is a stabilizer; and that whenever no \(X\)-row separates them, \(Z_i Z_j\) is. Then a nontrivial logical operator of weight \(3\) makes the distance exactly \(3\).

If every weight-one Pauli anticommutes with some stabilizer generator, and a weight-two nontrivial logical operator exists, then the code has distance exactly \(2\).

If a code has distance \(d\) then every nontrivial logical operator has weight at least \(d\); equivalently, no undetectable error of weight below \(d\) exists.

\(\dim H_1 = \dim Z_1 - \dim B_1\), so the number of encoded qubits is computed by two rank calculations.

The gross code (definition 84) has distance exactly \(12\), unconditionally.

Pulled back along the cover of definition 78, the base floor gives a weight-six lower bound for every nontrivial logical operator of the gross code.

Every nontrivial gross logical operator falls into one of two sectors, and in each the weight is at least twelve: the *safe* sector, where the two sheets of the cover contribute independently, and the *dangerous* sector, where they do not and a finer argument is needed.

If the rows of the check matrix are linearly independent over \(\mathbb {F}_2\) (definition 19) then the generators are independent in the sense of definition 35.

It suffices to test commutation against a generating set: \(g\) is logical iff it commutes with every generator of \(\mathcal{S}\).

\(-I \notin \mathcal{S}\) for any stabilizer group \(\mathcal{S}\).

The two conditions of definition 31 spelled out as a conjunction, which is the form the concrete distance proofs consume.

Nontriviality only depends on the underlying subgroup, so it transfers between two stabilizer groups with the same carrier.

For a stabilizer group, the Pauli normalizer and the centralizer coincide. This is special to the Pauli group and is the reason the literature uses the two words interchangeably here.

If a Pauli operator is a nontrivial logical operator of the induced CSS code, then its \(X\)-chain and its \(Z\)-chain cannot both be boundaries.

Multiplication on \(\mathcal{P}_n\) is associative. Together with the unit \(I^{\otimes n}\) and the inverse \(g^{-1} = i^{-a}P\) this makes definition 4 a group.

The generators of a presentation (definition 40) of an \([[n,k]]\) code generate a group with exactly \(2^{n-k}\) elements.

From a definition 79 certificate, every nonzero cycle has weight at least six.

A stabilizer group \(\mathcal{S}\) has exactly \(2^r\) elements, where \(r\) is the \(\mathbb {F}_2\)-rank of its symplectic image \(\{ \mathrm{symp}(g) : g \in \mathcal{S}\} \) (definition 14).

\(\mathcal{S} \le \mathcal{C}(\mathcal{S})\).

Definition 14 is injective: a Pauli operator is determined by its symplectic vector. Phases are of course not recorded.

For every \(L \ge 2\) the \(L \times L\) toric code (definition 73) has distance exactly \(L\), so it is an \([[2L^2, 2, L]]\) code.

\(d_X = L\): every nontrivial \(X\)-type logical operator has weight at least \(L\), and a horizontal loop achieves it.

\(d_Z = L\), by the same argument on the dual lattice.

\(\dim _{\mathbb {F}_2} H_1 = 2\) for every \(L \ge 2\), recovering \(H_1(T^2; \mathbb {F}_2) \cong \mathbb {F}_2^2\) and hence \(k = 2\).

\(\varphi \) is a linear isomorphism \(H_1 \cong \mathbb {F}_2^2\): a cycle is a boundary if and only if it wraps trivially in both directions.

Both wrapping numbers vanish on \(B_1\), so they descend to well-defined functions on \(H_1\).

The \(X\) operator of a chain commutes with every \(Z\)-check if and only if the chain is a cycle (definition 54).