The Steane code corrects an arbitrary error on one qubit

Category: 3-Local (Empirical, QM twin). BACKLOG #61, its discretization step; it closes the gap SteaneRecovery.lean's honest scope named ("Pauli errors only").

★★★ steane_recovery_arbitrary: one channel corrects an arbitrary 2 × 2 error on any one of the seven qubits, returning the code state scaled by tr(MᴴM)/2; and ★★★ steane_recovery_unitary_qubit: for a unitary error that scalar is 1, so the state is restored exactly.

Two steps, and the first is general. In KnillLaflamme.lean, ★★ recovery_apply_lin_comb: the correction property is bilinear in the two error slots and a channel is linear, so a recovery that corrects a family corrects every linear combination of it, up to the scalar the coefficients give. For a stabiliser code the family's Knill–Laflamme matrix is the identity (stabMat_knillLaflamme), so the cross terms vanish and the scalar is ∑ᵢ |aᵢ|².

The second step is the Steane instance. gateOf q M, the 2 × 2 matrix M acting on qubit q of the register, is linear in M (gateOf_add, gateOf_smul) and sends the four Paulis to the four single-qubit Pauli strings of the code's error family (gateOf_one_eq_pauliMat, gateOf_pX_eq_pauliMat, gateOf_pZ_eq_pauliMat, gateOf_pXZ_eq_pauliMat, through eq_add_unitErr_iff and bdot_unitErr). With ErrorDiscretization.lean's pauli_decomposition that gives ★ gateOf_eq_sum_pauliMat: an arbitrary error on one qubit is a combination of the code's own errors, with coefficients read off the entries of M. Summing their squares (sum_singleCoeff_sq) turns ∑ᵢ |aᵢ|² into tr(MᴴM)/2.

• eq_add_unitErr_iff, bdot_unitErr — the label arithmetic of a single-qubit Pauli;
• gateOf_one_eq_pauliMat, gateOf_pX_eq_pauliMat, gateOf_pZ_eq_pauliMat, gateOf_pXZ_eq_pauliMat — the four Paulis at one position as Pauli strings;
• singleCoeff, ★ gateOf_eq_sum_pauliMat, sum_singleCoeff_sq;
• exists_steane_recovery_cross — the recovery with its cross terms, which is what the span step consumes;
• ★★★ steane_recovery_arbitrary, ★★★ steane_recovery_unitary_qubit.

Honest scope

⚠️ One qubit still. This removes the Pauli restriction, not the weight-one restriction: two qubits in error are outside the Steane code's reach at level one, as before. ⚠️ The scalar tr(MᴴM)/2 is the honest statement for a general M: an error that is not unitary is trace-decreasing, and the recovery returns the code state with that weight. Nothing here normalises it away. ⚠️ This is the discretization step of BACKLOG #61, not the row: the concatenated quantum recovery at level k is SteaneConcat.lean (BACKLOG #86, 2026-09-27), which adds the tensor layer over the blocks (Mathlib/QuantumInfo/BlockKron.lean) and the induction. What this file gives that induction is exactly the step it needs: an arbitrary logical error on one block is corrected by the next level up, because the Paulis span the operators of a qubit.

References: E. Knill, R. Laflamme, W. Zurek, Science 279 (1998); M. Nielsen, I. Chuang, Quantum Computation and Quantum Information §10.6; Mathlib/QuantumInfo/KnillLaflamme.lean; Empirical/QM/QEC/SteaneRecovery.lean; Empirical/QM/QEC/ErrorDiscretization.lean; specs/BACKLOG.md #61; specs/steane-plan.md.

The four single-qubit Paulis at one position, as Pauli strings

theorem CSD.Empirical.QM.QEC.Steane.eq_add_unitErr_iff {q : Fin 7} {z w : Fin 7 → Fin 2} : w = z + unitErr q ↔ (∀ (i : Fin 7), i ≠ q → z i = w i) ∧ z q ≠ w q

theorem CSD.Empirical.QM.QEC.Steane.bdot_unitErr (q : Fin 7) (w : Fin 7 → Fin 2) : QuantumInfo.bdot (unitErr q) w = w q

theorem CSD.Empirical.QM.QEC.Steane.gateOf_one_eq_pauliMat (q : Fin 7) : QuantumInfo.Controlled.gateOf q 1 = QuantumInfo.pauliMat 0 0

theorem CSD.Empirical.QM.QEC.Steane.gateOf_pX_eq_pauliMat (q : Fin 7) : QuantumInfo.Controlled.gateOf q pX = QuantumInfo.pauliMat (unitErr q) 0

theorem CSD.Empirical.QM.QEC.Steane.gateOf_pZ_eq_pauliMat (q : Fin 7) : QuantumInfo.Controlled.gateOf q pZ = QuantumInfo.pauliMat 0 (unitErr q)

theorem CSD.Empirical.QM.QEC.Steane.gateOf_pXZ_eq_pauliMat (q : Fin 7) : QuantumInfo.Controlled.gateOf q pXZ = QuantumInfo.pauliMat (unitErr q) (unitErr q)

An arbitrary single-qubit operator is a combination of the four

noncomputable def CSD.Empirical.QM.QEC.Steane.singleCoeff (q : Fin 7) (M : Matrix (Fin 2) (Fin 2) ℂ) : SingleErr → ℂ

The Pauli coefficients of a single-qubit operator, as a function on the error labels: supported on the four labels at the given qubit.

Equations

• CSD.Empirical.QM.QEC.Steane.singleCoeff q M none = (M 0 0 + M 1 1) / 2
• CSD.Empirical.QM.QEC.Steane.singleCoeff q M (some (j, t)) = if j = q then if t = 0 then (M 0 1 + M 1 0) / 2 else if t = 1 then (M 0 0 - M 1 1) / 2 else (M 1 0 - M 0 1) / 2 else 0

theorem CSD.Empirical.QM.QEC.Steane.gateOf_eq_sum_pauliMat (q : Fin 7) (M : Matrix (Fin 2) (Fin 2) ℂ) : QuantumInfo.Controlled.gateOf q M = ∑ i : SingleErr, singleCoeff q M i • QuantumInfo.pauliMat (errA i) (errB i)

★ Discretization on the Steane register: an arbitrary operator on one qubit is a combination of the code's own error family.

The recovery, with its cross terms

theorem CSD.Empirical.QM.QEC.Steane.exists_steane_recovery_cross : ∃ (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 j : SingleErr), R.apply (QuantumInfo.pauliMat (errA i) (errB i) * ρ * (QuantumInfo.pauliMat (errA j) (errB j)).conjTranspose) = 1 j i • ρ

The Steane recovery with the full Knill–Laflamme correction property, cross terms included: the error labels are distinguishable, so the matrix of scalars is the identity.

An arbitrary error on one qubit is corrected

theorem CSD.Empirical.QM.QEC.Steane.sum_singleCoeff_sq (q : Fin 7) (M : Matrix (Fin 2) (Fin 2) ℂ) : ∑ i : SingleErr, ∑ j : SingleErr, star (singleCoeff q M i) * singleCoeff q M j * 1 i j = (star (M 0 0) * M 0 0 + star (M 0 1) * M 0 1 + star (M 1 0) * M 1 0 + star (M 1 1) * M 1 1) / 2

theorem CSD.Empirical.QM.QEC.Steane.steane_recovery_arbitrary : ∃ (R : QuantumInfo.Channel (Fin 7 → Fin 2) (Fin 7 → Fin 2) (Option SingleErr)), ∀ (ρ : Matrix (Fin 7 → Fin 2) (Fin 7 → Fin 2) ℂ), ρ = steaneProj * ρ * steaneProj → ∀ (q : Fin 7) (M : Matrix (Fin 2) (Fin 2) ℂ), R.apply (QuantumInfo.Controlled.gateOf q M * ρ * (QuantumInfo.Controlled.gateOf q M).conjTranspose) = ((star (M 0 0) * M 0 0 + star (M 0 1) * M 0 1 + star (M 1 0) * M 1 0 + star (M 1 1) * M 1 1) / 2) • ρ

★★★ The Steane recovery corrects an arbitrary error on one qubit. For every qubit q and every 2 × 2 matrix M, one channel returns the code state scaled by tr(MᴴM)/2 — the Paulis span the operators of a qubit, and the Knill–Laflamme correction property is bilinear in the two error slots, so correcting the four Paulis corrects the whole continuum.

theorem CSD.Empirical.QM.QEC.Steane.steane_recovery_unitary_qubit : ∃ (R : QuantumInfo.Channel (Fin 7 → Fin 2) (Fin 7 → Fin 2) (Option SingleErr)), ∀ (ρ : Matrix (Fin 7 → Fin 2) (Fin 7 → Fin 2) ℂ), ρ = steaneProj * ρ * steaneProj → ∀ (q : Fin 7), ∀ M ∈ Matrix.unitaryGroup (Fin 2) ℂ, R.apply (QuantumInfo.Controlled.gateOf q M * ρ * (QuantumInfo.Controlled.gateOf q M).conjTranspose) = ρ

★★★ A unitary error on one qubit is undone exactly. The scalar of steane_recovery_arbitrary is tr(MᴴM)/2 = 1 for a unitary block.