The Steane seven-qubit code as a stabiliser family (CSS from Hamming [7,4])

Category: 3-Local (QM-validity).

Glossary: https://glossary.constraintsurfacedynamics.com/steane-code/ Plain-language, CSD-role and formal statements of the Steane code, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The Steane [[7,1,3]] code, built as the first genuine CSS instance of the Cat-1 stabiliser layer (Mathlib/QuantumInfo/Stabilizer.lean, GK-3; plan specs/steane-plan.md): the parity-check rows of the classical Hamming [7,4] code give three X-type and three Z-type stabiliser generators, and the CSS condition — every row orthogonal to every row, H Hᵀ = 0 over 𝔽₂ — makes the trivial sign function coherent, so the whole GK-3 layer instantiates:

• steane_code_dimension — the stabiliser-family trace is 2⁷/2⁶ = 2: a one-logical-qubit code space, by the general stabProjector_trace.
• ★ The logical states: steaneZero ∝ ∑_{c ∈ C₂} |c⟩ (the row space of H) and steaneOne ∝ ∑_{c ∈ C₂} |c + 1⃗⟩, each stabilised by all sixty-four group elements (steaneZero_stabilised/steaneOne_stabilised), and orthonormal (inner_steaneZero_steaneOne, inner_steaneZero_self, inner_steaneOne_self) — the two-dimensional code space exhibited concretely, matching the trace count.
• ★ The logical operators: X̄ = X^{1⃗} swaps the logical states (logicalX_steaneZero/logicalX_steaneOne), Z̄ = Z^{1⃗} fixes |0̄⟩ and negates |1̄⟩ (logicalZ_steaneZero/logicalZ_steaneOne) — a genuine encoded qubit.
• ★ The distance mechanism: single-qubit errors have nonzero, pairwise-distinct syndromes (steane_syndrome_single_ne_zero, steane_syndrome_single_injective) — the classical Hamming distance-3 property, which via pauliOp_comm (the symplectic commutation criterion) is exactly the statement that every single-qubit X- or Z-error anticommutes with a generator identified by its syndrome. Both error types use the same matrix: the code is CSS-self-dual.

Honest scope. The code space is exhibited (two orthonormal stabilised states) and the error-detection mechanism is stated in syndrome form; the full recovery map, the Knill–Laflamme conditions, and fault-tolerance claims are not attempted (⚠️ RESIDUE(R-003)) — the same posture as the three-qubit modules. The 𝔽₂ facts about the concrete Hamming rows (orthogonality, independence, column distinctness) are closed by decide — kernel-checked finite computation, the right tool for a fixed 7 × 3 matrix.

def CSD.Empirical.QM.QEC.Steane.hammingRow : Fin 3 → Fin 7 → Fin 2

The parity-check rows of the Hamming [7,4] code: column j is the binary expansion of j + 1.

Equations

• CSD.Empirical.QM.QEC.Steane.hammingRow = ![![1, 0, 1, 0, 1, 0, 1], ![0, 1, 1, 0, 0, 1, 1], ![0, 0, 0, 1, 1, 1, 1]]

def CSD.Empirical.QM.QEC.Steane.rowComb (c : Fin 3 → Fin 2) : Fin 7 → Fin 2

An 𝔽₂ combination of the Hamming rows — the row space C₂ (eight elements), the support of the logical states.

Equations

• CSD.Empirical.QM.QEC.Steane.rowComb c j = ∑ i : Fin 3, c i * CSD.Empirical.QM.QEC.Steane.hammingRow i j

def CSD.Empirical.QM.QEC.Steane.allOnes : Fin 7 → Fin 2

The all-ones vector: the logical-X/Z label, a Hamming codeword outside the row space.

Equations

• CSD.Empirical.QM.QEC.Steane.allOnes x✝ = 1

def CSD.Empirical.QM.QEC.Steane.steaneA (x : Fin 6 → Fin 2) : Fin 7 → Fin 2

The X-labels of the stabiliser family: the first three bits of x combine the rows.

Equations

• CSD.Empirical.QM.QEC.Steane.steaneA x = CSD.Empirical.QM.QEC.Steane.rowComb fun (i : Fin 3) => x (Fin.castAdd 3 i)

def CSD.Empirical.QM.QEC.Steane.steaneB (x : Fin 6 → Fin 2) : Fin 7 → Fin 2

The Z-labels: the last three bits of x combine the rows.

Equations

• CSD.Empirical.QM.QEC.Steane.steaneB x = CSD.Empirical.QM.QEC.Steane.rowComb fun (i : Fin 3) => x (Fin.natAdd 3 i)

The 𝔽₂ facts about the Hamming rows (kernel-checked)

theorem CSD.Empirical.QM.QEC.Steane.rowComb_add (c d : Fin 3 → Fin 2) : rowComb (c + d) = rowComb c + rowComb d

Row combinations are additive.

theorem CSD.Empirical.QM.QEC.Steane.bdot_rowComb_rowComb (c d : Fin 3 → Fin 2) : QuantumInfo.bdot (rowComb c) (rowComb d) = 0

The CSS condition: every row combination is orthogonal to every row combination (H Hᵀ = 0 over 𝔽₂).

theorem CSD.Empirical.QM.QEC.Steane.bdot_rowComb_allOnes (c : Fin 3 → Fin 2) : QuantumInfo.bdot (rowComb c) allOnes = 0

Every row combination is orthogonal to the all-ones vector (rows have even weight).

theorem CSD.Empirical.QM.QEC.Steane.bdot_allOnes_allOnes : QuantumInfo.bdot allOnes allOnes = 1

The all-ones vector pairs to 1 with itself (seven is odd).

theorem CSD.Empirical.QM.QEC.Steane.rowComb_eq_zero (c : Fin 3 → Fin 2) (h : rowComb c = 0) : c = 0

The rows are independent: only the trivial combination vanishes.

theorem CSD.Empirical.QM.QEC.Steane.rowComb_ne_allOnes (c : Fin 3 → Fin 2) : rowComb c ≠ allOnes

The all-ones vector is not in the row space: the two logical supports are disjoint cosets.

theorem CSD.Empirical.QM.QEC.Steane.rowComb_injective (c d : Fin 3 → Fin 2) (h : rowComb c = rowComb d) : c = d

The row-combination map is injective (the eight support strings are distinct).

The stabiliser-family axioms, and the GK-3 instantiation

theorem CSD.Empirical.QM.QEC.Steane.steaneA_add (x y : Fin 6 → Fin 2) : steaneA (x + y) = steaneA x + steaneA y

theorem CSD.Empirical.QM.QEC.Steane.steaneB_add (x y : Fin 6 → Fin 2) : steaneB (x + y) = steaneB x + steaneB y

theorem CSD.Empirical.QM.QEC.Steane.steane_sigma_coherent (x y : Fin 6 → Fin 2) : (fun (x : Fin 6 → Fin 2) => 0) (x + y) = (fun (x : Fin 6 → Fin 2) => 0) x + (fun (x : Fin 6 → Fin 2) => 0) y + QuantumInfo.bdot (steaneB x) (steaneA y)

The trivial sign function is coherent: the CSS condition kills the pairing.

theorem CSD.Empirical.QM.QEC.Steane.steane_labels_injective (x : Fin 6 → Fin 2) (hA : steaneA x = 0) (hB : steaneB x = 0) : x = 0

The six generators are independent.

theorem CSD.Empirical.QM.QEC.Steane.steane_code_dimension : ∑ z : Fin 7 → Fin 2, (QuantumInfo.stabProjector steaneA steaneB (fun (x : Fin 6 → Fin 2) => 0) (QuantumInfo.basisState z)).ofLp z = 2

The code space is one logical qubit: the stabiliser-family trace is 2⁷/2⁶ = 2 — the general GK-3 dimension count at the Steane labels.

The logical states

noncomputable def CSD.Empirical.QM.QEC.Steane.steaneZero : QuantumInfo.QReg 7

The logical zero: the uniform superposition over the row space C₂.

Equations

• CSD.Empirical.QM.QEC.Steane.steaneZero = (↑√8)⁻¹ • ∑ c : Fin 3 → Fin 2, QuantumInfo.basisState (CSD.Empirical.QM.QEC.Steane.rowComb c)

noncomputable def CSD.Empirical.QM.QEC.Steane.steaneOne : QuantumInfo.QReg 7

The logical one: the uniform superposition over the coset C₂ + 1⃗.

Equations

• CSD.Empirical.QM.QEC.Steane.steaneOne = (↑√8)⁻¹ • ∑ c : Fin 3 → Fin 2, QuantumInfo.basisState (CSD.Empirical.QM.QEC.Steane.rowComb c + CSD.Empirical.QM.QEC.Steane.allOnes)

theorem CSD.Empirical.QM.QEC.Steane.steaneZero_stabilised (x : Fin 6 → Fin 2) : QuantumInfo.pauliOp (steaneA x) (steaneB x) steaneZero = steaneZero

★ The logical zero is stabilised by every element of the sixty-four-element stabiliser group. Z-type parts act trivially by the CSS orthogonality; X-type parts permute the row space.

theorem CSD.Empirical.QM.QEC.Steane.steaneOne_stabilised (x : Fin 6 → Fin 2) : QuantumInfo.pauliOp (steaneA x) (steaneB x) steaneOne = steaneOne

★ The logical one is stabilised by every element — the coset shifts through.

The logical operators: a genuine encoded qubit

theorem CSD.Empirical.QM.QEC.Steane.logicalX_steaneZero : QuantumInfo.pauliOp allOnes 0 steaneZero = steaneOne

★ X̄ = X^{1⃗} maps |0̄⟩ to |1̄⟩.

theorem CSD.Empirical.QM.QEC.Steane.logicalX_steaneOne : QuantumInfo.pauliOp allOnes 0 steaneOne = steaneZero

★ X̄ maps |1̄⟩ back to |0̄⟩.

theorem CSD.Empirical.QM.QEC.Steane.logicalZ_steaneZero : QuantumInfo.pauliOp 0 allOnes steaneZero = steaneZero

★ Z̄ = Z^{1⃗} fixes |0̄⟩.

theorem CSD.Empirical.QM.QEC.Steane.logicalZ_steaneOne : QuantumInfo.pauliOp 0 allOnes steaneOne = -steaneOne

★ Z̄ negates |1̄⟩: the encoded qubit's phase degree of freedom is real.

Orthogonality: the code space is two-dimensional as exhibited

theorem CSD.Empirical.QM.QEC.Steane.inner_steaneZero_steaneOne : inner ℂ steaneZero steaneOne = 0

The two logical states are orthogonal: their supports are disjoint cosets.

theorem CSD.Empirical.QM.QEC.Steane.inner_basisState (u v : Fin 7 → Fin 2) : inner ℂ (QuantumInfo.basisState u) (QuantumInfo.basisState v) = if v = u then 1 else 0

Basis states are orthonormal (local form).

theorem CSD.Empirical.QM.QEC.Steane.sqrt_eight_inv_sq : (starRingEnd ℂ) (↑√8)⁻¹ * ((↑√8)⁻¹ * 8) = 1

The normalisation constant: (1/√8)·(1/√8)·8 = 1.

theorem CSD.Empirical.QM.QEC.Steane.inner_steaneZero_self : inner ℂ steaneZero steaneZero = 1

The logical zero is a unit vector: the eight support strings are distinct.

theorem CSD.Empirical.QM.QEC.Steane.inner_steaneOne_self : inner ℂ steaneOne steaneOne = 1

The logical one is a unit vector: the coset strings are distinct.

The distance mechanism: single-error syndromes

def CSD.Empirical.QM.QEC.Steane.syndrome (e : Fin 7 → Fin 2) : Fin 3 → Fin 2

The syndrome of an error pattern: its pairing against each Hamming row. Via pauliOp_comm, a nonzero syndrome is exactly anticommutation with the corresponding generator.

Equations

• CSD.Empirical.QM.QEC.Steane.syndrome e i = QuantumInfo.bdot (CSD.Empirical.QM.QEC.Steane.hammingRow i) e

def CSD.Empirical.QM.QEC.Steane.unitErr (j : Fin 7) : Fin 7 → Fin 2

The single-bit error at position j.

Equations

• CSD.Empirical.QM.QEC.Steane.unitErr j i = if i = j then 1 else 0

theorem CSD.Empirical.QM.QEC.Steane.steane_syndrome_single_ne_zero (j : Fin 7) : syndrome (unitErr j) ≠ 0

★ Every single-qubit error is detected: its syndrome is nonzero (every Hamming column is nonzero). By CSS symmetry the same statement covers both X- and Z-type single-qubit errors.

theorem CSD.Empirical.QM.QEC.Steane.steane_syndrome_single_injective (j j' : Fin 7) (h : syndrome (unitErr j) = syndrome (unitErr j')) : j = j'

★ Distinct single-qubit errors are distinguished: the seven columns of the Hamming matrix are pairwise distinct — the distance-3 property that makes single errors correctable, not merely detectable.