Quantum Error Correction in Lean

8 The toric code

The \(L \times L\) square lattice on the torus, read as a chain complex. The \(2L^2\) edges are the qubits; vertices carry the \(Z\)-checks and faces the \(X\)-checks.

Definition 59 The toric chain complex

The \(L \times L\) square lattice on the torus, packaged as a definition 46: \(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.

Definition 60 Toric homology
#

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

Theorem 61 The toric code encodes two qubits

\(\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\).

Proof

By theorem 52 it suffices to compute \(\dim Z_1\) and \(\dim B_1\). Rank-nullity applied to \(\partial _1\) gives \(\dim Z_1 = 2L^2 - \operatorname {rank}\partial _1\), and \(\operatorname {rank}\partial _1 = L^2 - 1\) because the only relation among the vertex checks is that they all multiply to the identity. Dually \(\operatorname {rank}\partial _2 = L^2 - 1\), the kernel of \(\partial _2\) being spanned by the all-ones face chain. Subtracting gives \(2\).

8.1 Wrapping invariants

The homology of the torus is detected by two \(\mathbb {F}_2\)-valued winding numbers, counting how often a chain wraps horizontally and vertically. They are defined on all chains, are unchanged by adding a boundary, and together separate homology classes.

Definition 62 Horizontal wrapping number
#

\(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.

Definition 63 Vertical wrapping number
#

The vertical counterpart of definition 62.

Theorem 64 Wrapping numbers vanish on boundaries

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

Proof

It is enough to check a single face, since \(\partial _2\) is linear and the faces span \(C_2\). A face has exactly two vertical edges, which either both cross the cut or both miss it; either way the count is even.

Definition 65 The wrapping map
#

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

Theorem 66 Wrapping numbers classify homology

\(\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.

Proof

Surjectivity is witnessed by the horizontal and vertical loop chains. Injectivity is the substantive direction: a cycle with \(h = v = 0\) is shown to be a boundary. With theorem 61 giving \(\dim H_1 = 2\), a surjection onto \(\mathbb {F}_2^2\) is automatically injective.

8.2 The code and its distance

The \(L \times L\) toric code presented as a definition 37 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 definition 37 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 natural generating set of the toric code has \(2L^2\) elements, two more than the \(n - k = 2L^2 - 2\) that definition 37 demands: the vertex checks multiply to the identity, and so do the face checks. The packaging therefore uses a trimmed generator list, and the homological identities are what prove the trimmed list generates the same subgroup. Distance proofs stated against the untrimmed stabilizer group are carried across by theorem 33.

Proof

Upper bound: the horizontal loop chain is a cycle with \(h = 1\), hence non-boundary by theorem 66, and has exactly \(L\) edges. Lower bound: a nontrivial class has \(h = 1\) or \(v = 1\); say \(h = 1\). Then the chain meets each of the \(L\) disjoint horizontal cuts an odd number of times, so it contains at least one edge per cut, giving at least \(L\) edges in total.

Proof

The dual complex of definition 59 is again an \(L \times L\) torus lattice with the roles of faces and vertices exchanged, so the argument of theorem 68 applies verbatim to the dual wrapping invariants.

Proof

For a CSS code \(d = \min (d_X, d_Z)\), and both are \(L\) by theorem 68 and theorem 69. The chain-level bounds are moved to Pauli weights by theorem 58, and the result is transported from the hand-built stabilizer group to the packaged code of definition 67 by theorem 33.

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