Quantum Error Correction in Lean

10 Code instances

The remaining codes exercise the same machinery on smaller or differently shaped examples. The \([[5,1,3]]\) code is the interesting outlier: its generators mix \(X\) and \(Z\) on the same qubit, so it is not CSS, the homological route is unavailable, and its distance is settled instead by a direct search over weight-one and weight-two anti-witnesses.

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 45 applies with the same three rows on both sides; \(X\) on qubits \(\{ 3,5,6\} \) is the weight-three logical.

Definition 82 The Shor \([[9,1,3]]\) code

The stabilizer group of the nine-qubit Shor code, a repetition code of cat states — historically the first quantum error-correcting code.

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 parametric generalized-parity family with exactly two stabilizer generators, the all-\(X\) and all-\(Z\) operators. Distance two for every \(m\), again via theorem 44.

The bit-flip repetition code as a stabilizer code, with \(Z_i Z_{i+1}\) generators. It has distance one as a *quantum* code — phase errors are undetectable — which is why it appears here as a degenerate reference point rather than as a usable code.