The Steane code corrects every single-qubit Pauli error

Category: 3-Local (QM-validity). BACKLOG #14(b).

Steane.lean exhibits the code space and the distance mechanism (single-qubit errors have nonzero, pairwise-distinct syndromes); Mathlib/QuantumInfo/StabilizerRecovery.lean turns a detected Pauli error family on a stabiliser code into a recovery channel through the Knill–Laflamme theorem. This file instantiates it:

• SingleErr — the twenty-two single-qubit Paulis (I, and X, Z, XZ on each of the seven qubits), with labels errA, errB; steaneProj — the code projector as a matrix;
• ★ syndrome_pair_ne_zero — the distance-3 mechanism for pairs: two distinct single-qubit Paulis have a product whose X-part or Z-part carries a nonzero syndrome (a 𝔽₂ computation over the 22 × 22 pairs, kernel-checked by decide); steane_detects_pair reads it as anticommutation with one of the six generators (steaneX, steaneZ);
• ★★ steane_knillLaflamme — the Steane code satisfies Knill–Laflamme with c = 1 for the single-qubit Paulis: P Eᵢᴴ Eⱼ P = δᵢⱼ P;
• ★★★ exists_steane_recovery — the recovery channel: one channel R with R (E ρ Eᴴ) = ρ for every single-qubit Pauli E and every code state ρ = P ρ P;
• steaneProj_mulVec_steaneZero / _steaneOne — the logical states are code states, and ★★★ steane_recovery_logical — every single-qubit Pauli error on an encoded qubit a|0̄⟩ + b|1̄⟩ is undone: R (E |ψ̄⟩⟨ψ̄| Eᴴ) = |ψ̄⟩⟨ψ̄|.

Honest scope

⚠️ Pauli errors here; the extension to an arbitrary operator on one qubit (its Pauli expansion, ErrorDiscretization.lean's three-qubit pattern on seven qubits) is SteaneArbitrary.lean (BACKLOG #61, 2026-09-26). No two-qubit error is corrected, at any level (the Steane code does not correct them). The recovery is the channel the Knill–Laflamme construction produces, not the syndrome-measurement circuit; the Σ-side twin (a Σ-flow whose environment marginal is the single-qubit Pauli channel, as Empirical/CSD/QEC/RegisterFlow.lean does for three qubits) is Empirical/CSD/QEC/SteaneFlow.lean (BACKLOG #53, 2026-09-27).

References: A. Steane, Error correcting codes in quantum theory, PRL 77 (1996) 793; Nielsen–Chuang §10.4.2; Empirical/QM/QEC/Steane.lean; Mathlib/QuantumInfo/StabilizerRecovery.lean; specs/steane-plan.md; specs/BACKLOG.md #14.

The single-qubit Paulis and the code projector

@[reducible, inline]

abbrev CSD.Empirical.QM.QEC.Steane.SingleErr : Type

The single-qubit Pauli errors on seven qubits: none is the identity, some (j, 0) the X on qubit j, some (j, 1) the Z, some (j, 2) the XZ (proportional to Y).

Equations

• CSD.Empirical.QM.QEC.Steane.SingleErr = Option (Fin 7 × Fin 3)

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

The X-label of a single-qubit Pauli.

Equations

• CSD.Empirical.QM.QEC.Steane.errA none = 0
• CSD.Empirical.QM.QEC.Steane.errA (some (j, t)) = if t = 1 then 0 else CSD.Empirical.QM.QEC.Steane.unitErr j

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

The Z-label of a single-qubit Pauli.

Equations

• CSD.Empirical.QM.QEC.Steane.errB none = 0
• CSD.Empirical.QM.QEC.Steane.errB (some (j, t)) = if t = 0 then 0 else CSD.Empirical.QM.QEC.Steane.unitErr j

noncomputable def CSD.Empirical.QM.QEC.Steane.steaneProj : Matrix (Fin 7 → Fin 2) (Fin 7 → Fin 2) ℂ

The Steane code projector as a matrix on the register's coordinates.

Equations

• CSD.Empirical.QM.QEC.Steane.steaneProj = QuantumInfo.stabMat CSD.Empirical.QM.QEC.Steane.steaneA CSD.Empirical.QM.QEC.Steane.steaneB fun (x : Fin 6 → Fin 2) => 0

def CSD.Empirical.QM.QEC.Steane.steaneX (r : Fin 3) : Fin 6 → Fin 2

The X-type generator X^{hammingRow r} as a label of the family.

Equations

• CSD.Empirical.QM.QEC.Steane.steaneX r k = if ↑k = ↑r then 1 else 0

def CSD.Empirical.QM.QEC.Steane.steaneZ (r : Fin 3) : Fin 6 → Fin 2

The Z-type generator Z^{hammingRow r} as a label of the family.

Equations

• CSD.Empirical.QM.QEC.Steane.steaneZ r k = if ↑k = ↑r + 3 then 1 else 0

theorem CSD.Empirical.QM.QEC.Steane.steaneA_steaneX (r : Fin 3) : steaneA (steaneX r) = hammingRow r

theorem CSD.Empirical.QM.QEC.Steane.steaneB_steaneX (r : Fin 3) : steaneB (steaneX r) = 0

theorem CSD.Empirical.QM.QEC.Steane.steaneA_steaneZ (r : Fin 3) : steaneA (steaneZ r) = 0

theorem CSD.Empirical.QM.QEC.Steane.steaneB_steaneZ (r : Fin 3) : steaneB (steaneZ r) = hammingRow r

The distance mechanism for pairs

theorem CSD.Empirical.QM.QEC.Steane.syndrome_pair_ne_zero (i j : SingleErr) (h : i ≠ j) : syndrome (errB i + errB j) ≠ 0 ∨ syndrome (errA i + errA j) ≠ 0

★ Two distinct single-qubit Paulis are told apart by the syndromes: the product's X-part or its Z-part has a nonzero syndrome. A 𝔽₂ computation over the 22 × 22 pairs.

theorem CSD.Empirical.QM.QEC.Steane.fin2_eq_one_of_ne_zero {v : Fin 2} (h : v ≠ 0) : v = 1

theorem CSD.Empirical.QM.QEC.Steane.exists_row_of_syndrome_ne_zero {e : Fin 7 → Fin 2} (h : syndrome e ≠ 0) : ∃ (r : Fin 3), QuantumInfo.bdot (hammingRow r) e = 1

A nonzero syndrome names a row pairing to 1.

theorem CSD.Empirical.QM.QEC.Steane.steane_detects_pair (i j : SingleErr) (h : i ≠ j) : ∃ (x : Fin 6 → Fin 2), QuantumInfo.bdot (steaneA x) (errB i + errB j) + QuantumInfo.bdot (steaneB x) (errA i + errA j) = 1

Detection as anticommutation: for distinct single-qubit Paulis, some generator pairs to 1 with the product's labels — the hypothesis of stabMat_knillLaflamme.

Knill–Laflamme and the recovery

theorem CSD.Empirical.QM.QEC.Steane.steane_knillLaflamme : QuantumInfo.KnillLaflamme steaneProj (fun (i : SingleErr) => QuantumInfo.pauliMat (errA i) (errB i)) 1

★★ The Steane code satisfies Knill–Laflamme with c = 1 for the single-qubit Paulis: P Eᵢᴴ Eⱼ P = δᵢⱼ P.

theorem CSD.Empirical.QM.QEC.Steane.exists_steane_recovery : ∃ (R : QuantumInfo.Channel (Fin 7 → Fin 2) (Fin 7 → Fin 2) (Option SingleErr)), ∀ (ρ : Matrix (Fin 7 → Fin 2) (Fin 7 → Fin 2) ℂ), ρ = steaneProj * ρ * steaneProj → ∀ (i : SingleErr), R.apply (QuantumInfo.pauliMat (errA i) (errB i) * ρ * (QuantumInfo.pauliMat (errA i) (errB i)).conjTranspose) = ρ

★★★ The Steane code corrects every single-qubit Pauli error: one recovery channel R undoes each of the twenty-two errors on every code state.

The logical states are code states

theorem CSD.Empirical.QM.QEC.Steane.isCodeProjector_steaneProj : QuantumInfo.IsCodeProjector steaneProj

theorem CSD.Empirical.QM.QEC.Steane.stabProjector_steane_of_stabilised (ψ : QuantumInfo.QReg 7) (hψ : ∀ (x : Fin 6 → Fin 2), QuantumInfo.pauliOp (steaneA x) (steaneB x) ψ = ψ) : QuantumInfo.stabProjector steaneA steaneB (fun (x : Fin 6 → Fin 2) => 0) ψ = ψ

The group average fixes a state fixed by every generator.

theorem CSD.Empirical.QM.QEC.Steane.steaneProj_mulVec_steaneZero : steaneProj.mulVec steaneZero.ofLp = steaneZero.ofLp

theorem CSD.Empirical.QM.QEC.Steane.steaneProj_mulVec_steaneOne : steaneProj.mulVec steaneOne.ofLp = steaneOne.ofLp

noncomputable def CSD.Empirical.QM.QEC.Steane.logicalVec (a b : ℂ) : (Fin 7 → Fin 2) → ℂ

The encoded qubit a|0̄⟩ + b|1̄⟩, as a coordinate vector.

Equations

• CSD.Empirical.QM.QEC.Steane.logicalVec a b = (a • CSD.Empirical.QM.QEC.Steane.steaneZero + b • CSD.Empirical.QM.QEC.Steane.steaneOne).ofLp

theorem CSD.Empirical.QM.QEC.Steane.steaneProj_mulVec_logicalVec (a b : ℂ) : steaneProj.mulVec (logicalVec a b) = logicalVec a b

theorem CSD.Empirical.QM.QEC.Steane.logical_density_eq (a b : ℂ) : Matrix.vecMulVec (logicalVec a b) (star (logicalVec a b)) = steaneProj * Matrix.vecMulVec (logicalVec a b) (star (logicalVec a b)) * steaneProj

The density operator of the encoded qubit is a code state: ρ = P ρ P.

theorem CSD.Empirical.QM.QEC.Steane.steane_recovery_logical : ∃ (R : QuantumInfo.Channel (Fin 7 → Fin 2) (Fin 7 → Fin 2) (Option SingleErr)), ∀ (a b : ℂ) (i : SingleErr), R.apply (QuantumInfo.pauliMat (errA i) (errB i) * Matrix.vecMulVec (logicalVec a b) (star (logicalVec a b)) * (QuantumInfo.pauliMat (errA i) (errB i)).conjTranspose) = Matrix.vecMulVec (logicalVec a b) (star (logicalVec a b))

★★★ Every single-qubit Pauli error on an encoded qubit is undone: for |ψ̄⟩ = a|0̄⟩ + b|1̄⟩ and every single-qubit Pauli E, the recovery channel returns |ψ̄⟩⟨ψ̄| from E |ψ̄⟩⟨ψ̄| Eᴴ.