The Steane code under independent noise: the code-capacity failure bound and the threshold

Category: 3-Local (Empirical, QM twin). BACKLOG #51, the part (c) of row 14 (R-003): the sentence link 12 of docs/FROM-POSTULATES-TO-QUANTUM-COMPUTERS.md lacked.

Each of the seven qubits independently suffers an error with probability at most p — any per-qubit noise alphabet, read through a map to the single-qubit Paulis — and the recovery channel of SteaneRecovery.lean is applied. The recovery undoes every single-qubit Pauli (exists_steane_recovery), so the encoded state is restored unless two or more qubits are hit; by the union bound over pairs (measure_pi_two_or_more_le) that has probability at most C(7, 2) p² = 21 p². Concatenation replaces p by 21 p² at every level (concatMeasure_concatBad_le), so k levels give (21 p)^{2^k} / 21: below p when p ≤ 1/21, and tending to 0 when p < 1/21 — the code-capacity threshold of the Steane code.

• patA, patB, patErr — the Pauli labels and the error operator of an error pattern;
• exists_singleErr_of_card_le_one — a pattern with at most one error is a single-qubit Pauli;
• ★★ steane_codeCapacity_failure_le — the failure bound: for every code state ρ, the probability that the recovery does not return ρ is at most 21 p²;
• ★ steane_concatBad_le — the bad patterns of the k-fold concatenated Steane code have probability at most (21 p)^{2^k} / 21; ★ steane_threshold — below p < 1/21 that bound tends to 0.

Honest scope

⚠️ Code capacity, level one quantum. The quantum statement is at level 1: an encoded block whose pattern has at most one error is restored exactly. At higher levels the theorem is the pattern recursion of the code-capacity argument (the probability that two or more sub-blocks are bad); the concatenated quantum recovery — decode each block, correct the resulting block errors with the next level's code, which corrects an arbitrary error on one block because the Paulis span the operators of a qubit — landed 2026-09-27 in SteaneConcat.lean (BACKLOG #86), so the quantum statement now holds at every level: one recovery channel per level restores every code state from every pattern with isBad 7 k x = false, exactly when the error is unitary (exists_concat_recovery_unitary), and the patterns it excludes are exactly the concatBad 7 k bounded here. Its span step is landed (SteaneArbitrary.lean, #61, 2026-09-26): an arbitrary error on one qubit is corrected. The circuit-level threshold theorem is BACKLOG #62, whose first rung landed 2026-09-28 (#62 (a), SteaneFaultyGate.lean): faulty gates on a transversal gadget, where one faulty location is a weight-one error after the ideal gadget, together with the circuit's union bound and level count (Mathlib/Probability/CircuitThreshold.lean). Its (b) and (e) landed the same day (the transversal X̄, Z̄ and Hadamard as the code's logical gates; the polylogarithmic overhead). Its (f) landed too (the transversal CNOT across two blocks). Extended rectangles — faults inside the recovery gadget — and the simulation theorem are still open there.

References: A. Steane, Error correcting codes in quantum theory, PRL 77 (1996); E. Knill, R. Laflamme, W. Zurek, Science 279 (1998); Empirical/QM/QEC/SteaneRecovery.lean; Mathlib/Probability/CodeCapacityThreshold.lean; specs/BACKLOG.md #51; specs/steane-plan.md.

def CSD.Empirical.QM.QEC.Steane.patA {α : Type u_1} (err : α → Option (Fin 3)) (x : Fin 7 → α) : Fin 7 → Fin 2

The X-label of an error pattern: 1 at the qubits carrying X or XZ.

Equations

• CSD.Empirical.QM.QEC.Steane.patA err x i = match err (x i) with | none => 0 | some t => if t = 1 then 0 else 1

def CSD.Empirical.QM.QEC.Steane.patB {α : Type u_1} (err : α → Option (Fin 3)) (x : Fin 7 → α) : Fin 7 → Fin 2

The Z-label of an error pattern: 1 at the qubits carrying Z or XZ.

Equations

• CSD.Empirical.QM.QEC.Steane.patB err x i = match err (x i) with | none => 0 | some t => if t = 0 then 0 else 1

noncomputable def CSD.Empirical.QM.QEC.Steane.patErr {α : Type u_1} (err : α → Option (Fin 3)) (x : Fin 7 → α) : Matrix (Fin 7 → Fin 2) (Fin 7 → Fin 2) ℂ

The error operator of a pattern: the Pauli with the pattern's labels.

Equations

• CSD.Empirical.QM.QEC.Steane.patErr err x = QuantumInfo.pauliMat (CSD.Empirical.QM.QEC.Steane.patA err x) (CSD.Empirical.QM.QEC.Steane.patB err x)

theorem CSD.Empirical.QM.QEC.Steane.exists_singleErr_of_card_le_one {α : Type u_1} (err : α → Option (Fin 3)) (x : Fin 7 → α) (hx : {i : Fin 7 | err (x i) ≠ none}.card ≤ 1) : ∃ (e : SingleErr), patA err x = errA e ∧ patB err x = errB e

A pattern with at most one error is a single-qubit Pauli (or the identity).

theorem CSD.Empirical.QM.QEC.Steane.steane_codeCapacity_failure_le {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure ν] (err : α → Option (Fin 3)) {p : ENNReal} (hν : ν {a : α | err a ≠ none} ≤ p) : ∃ (R : QuantumInfo.Channel (Fin 7 → Fin 2) (Fin 7 → Fin 2) (Option SingleErr)), ∀ (ρ : Matrix (Fin 7 → Fin 2) (Fin 7 → Fin 2) ℂ), ρ = steaneProj * ρ * steaneProj → (MeasureTheory.Measure.pi fun (x : Fin 7) => ν) {x : Fin 7 → α | R.apply (patErr err x * ρ * (patErr err x).conjTranspose) ≠ ρ} ≤ 21 * p ^ 2

★★ The code-capacity failure bound for the Steane code. Under independent per-qubit noise of rate at most p (any alphabet, read through err to the single-qubit Paulis), for every code state ρ the probability that the recovery channel does not return ρ is at most C(7, 2) p² = 21 p²: the recovery undoes every pattern with at most one error, and two or more errors strike with probability at most 21 p².

theorem CSD.Empirical.QM.QEC.Steane.steane_concatBad_le (ν : MeasureTheory.Measure Bool) [MeasureTheory.IsProbabilityMeasure ν] {p : ℝ} (hp : 0 ≤ p) (hν : ν {b : Bool | b = true} ≤ ENNReal.ofReal p) (k : ℕ) : ↑(concatMeasure 7 ν k) (concatBad 7 k) ≤ ENNReal.ofReal ((21 * p) ^ 2 ^ k / 21)

★ The concatenated Steane code: the bad patterns of k levels have probability at most (21 p)^{2^k} / 21 under independent per-qubit noise of rate at most p.

theorem CSD.Empirical.QM.QEC.Steane.steane_threshold {p : ℝ} (hp : 0 ≤ p) (h : p < 1 / 21) : Filter.Tendsto (fun (k : ℕ) => (21 * p) ^ 2 ^ k / 21) Filter.atTop (nhds 0)

★ The threshold of the Steane code, code-capacity form: below p < 1/21, the bound on the bad patterns of the k-fold concatenated code tends to 0 as k → ∞.