Steane error correction: final errors lie only on the fault locations

Open

QAlgorithms.GottesmanIntro.steaneEC_claim1

by Goku · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

gottesman-introlecture-notesquantum-information

This is the key claim in the proof that Steane error correction satisfies property EC A (Gottesman intro p.28).

Let $C_1, C_2 \subseteq \mathbb F_2^n$ be binary linear codes with $C_2^{\perp} \subseteq C_1$ , and let $\mathcal C$ be their CSS code, spanned by the states $\sum_{w \in C_2^{\perp}} |u + w\rangle$ for $u \in C_1$ . Steane error correction is applied to a data block in an arbitrary state $|\psi\rangle$ . The state may be entangled with a reference system $R$ , and its incoming error is unrestricted. The procedure runs as follows:

A phase ancilla is prepared in the encoded $|0\rangle = \sum_{w\in C_2^\perp}|w\rangle$ and a bit-flip ancilla in the encoded $|0\rangle+|1\rangle = \sum_{u\in C_1}|u\rangle$ .
A transversal CNOT is applied with the phase ancilla as control and the data as target. Then a transversal CNOT is applied with the data as control and the bit-flip ancilla as target.
The phase ancilla is measured in the Hadamard-rotated basis, giving a word $w_P$ . The bit-flip ancilla is measured in the standard basis, giving $w_B$ .
Classical decoders return $d_P = \mathrm{dec}_P(w_P)$ with the same $C_2$ -syndrome as $w_P$ and $d_B = \mathrm{dec}_B(w_B)$ with the same $C_1$ -syndrome as $w_B$ . Then $Z$ is applied on the qubits of $d_P$ and $X$ on the qubits of $d_B$ . This correction step is error-free.

The faults are arbitrary operators. They may act within $f_P, f_B$ on the prepared ancillas, and within the pairs (data qubit $i$ , ancilla qubit $i$ ) for $i \in g_P$ , resp. $g_B$ , right after the two CNOTs. During the Hadamard and measurement of the phase ancilla they act within $h_P$ , and during the measurement of the bit-flip ancilla within $h_B$ . Put $F = f_P \cup f_B \cup g_P \cup g_B \cup h_P \cup h_B$ . Then for every pair of outcomes $(w_P, w_B)$ the corrected (unnormalized) data–reference state satisfies

|\psi_{\mathrm{final}}\rangle \in V_F \otimes R, \qquad V_F = \operatorname{span}\{E|c\rangle : c \in \mathcal C,\ E \text{ acts only on the qubits in } F\},

and moreover $|F| \le s = |f_P|+|f_B|+|g_P|+|g_B|+|h_P|+|h_B|$ .

In words: after Steane error correction, the data is a codeword (possibly a different logical state) with errors only on the qubits where faults occurred during error correction. This gives EC A when $s \le t$ .

Formalization Note The circuit is the chunk-local definition steaneECOutput. It returns the post-measurement branch for the given outcomes, i.e. the amplitude of the ancillas on $|w_P, w_B\rangle$ . In that branch the map is linear, so the arbitrary fault operators per Kraus branch and the arbitrary incoming vector cover the source's 'no restrictions as to the types of errors'. The hypothesis $s \le t$ of EC A is omitted because the claim's proof never uses it.

Preamble

import Definitions.Def_QAlgorithms_Defs_BinaryStabilizer
import Definitions.Def_QAlgorithms_GottesmanIntro_Ch04_Model
set_option autoImplicit false

Formal statement

namespace QAlgorithms.GottesmanIntro






/-- Gottesman intro p.28, Claim 1 (Steane error correction, proof of EC A): let `C1, C2 ⊆ F_2^n`
be binary linear codes with `C2⊥ ⊆ C1` and let `C` be their CSS code (p.11). Run Steane error
correction (p.27, Figure 3) on an arbitrary incoming data vector `ψ`, possibly entangled with a
reference system `R`, with classical decoders returning an error with the same syndrome as the
measured word (`decP` for `C2`, `decB` for `C1`, p.28). Let the faults be arbitrary operators:
`FP`, `FB` on the prepared phase and bit-flip ancillas, acting within the qubit sets `fP`, `fB`;
`GP`, `GB` at the transversal CNOTs, acting within qubit `i` of the data block and of the
ancilla for `i ∈ gP`, resp. `gB`; `HP`, `HB` during the Hadamard and measurement of the phase
ancilla and the measurement of the bit-flip ancilla, within `hP`, `hB`. Then for every pair of
measurement outcomes the corrected data ⊗ reference state lies in `V_F ⊗ R`, where
`F = fP ∪ fB ∪ gP ∪ gB ∪ hP ∪ hB` and `V_F` is the span of the vectors `E|c⟩` with `c ∈ C` and
`E` acting within `F`: the final state has errors only on the qubits of `F`; and `|F| ≤ s`,
`s = |fP| + |fB| + |gP| + |gB| + |hP| + |hB|`. -/
theorem steaneEC_claim1 {n : ℕ} {R : Type*} [Fintype R] [DecidableEq R]
    (C1 C2 : Submodule (ZMod 2) (Fin n → ZMod 2)) (hC : binDual C2 ≤ C1)
    (decP decB : (Fin n → ZMod 2) → (Fin n → ZMod 2))
    (hdecP : ∀ w : Fin n → ZMod 2, ∀ h ∈ binDual C2, h ⬝ᵥ decP w = h ⬝ᵥ w)
    (hdecB : ∀ w : Fin n → ZMod 2, ∀ h ∈ binDual C1, h ⬝ᵥ decB w = h ⬝ᵥ w)
    (fP fB gP gB hP hB : Finset (Fin n))
    (FP FB HP HB : Matrix (Qubits n) (Qubits n) ℂ)
    (GP GB : Matrix (Qubits n × Qubits n) (Qubits n × Qubits n) ℂ)
    (hFP : ActsWithin fP FP) (hFB : ActsWithin fB FB)
    (hGP : ActsWithinPair gP GP) (hGB : ActsWithinPair gB GB)
    (hHP : ActsWithin hP HP) (hHB : ActsWithin hB HB)
    (ψ : EuclideanSpace ℂ (Qubits n × R)) (wP wB : Fin n → ZMod 2) :
    steaneECOutput C1 C2 decP decB FP FB HP HB GP GB ψ wP wB ∈
        errorSpaceWithRef R (cssCode C1 C2) (fP ∪ fB ∪ gP ∪ gB ∪ hP ∪ hB) ∧
      (fP ∪ fB ∪ gP ∪ gB ∪ hP ∪ hB).card ≤
        fP.card + fB.card + gP.card + gB.card + hP.card + hB.card := by
  sorry

end QAlgorithms.GottesmanIntro

Source

Daniel Gottesman, An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation, 2009, v1, PDF p. 28, §4.4, Claim 1. https://arxiv.org/pdf/0904.2557v1

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Two names in this statement are not part of the provided definition layer: steaneECOutput and ActsWithinPair. Their bodies are not shown, so this read-back states only what their argument signatures reveal and does not unfold them.

Setting. Fix:

a natural number $n$ (the number of physical qubits; $n = 0$ is allowed);
a finite type $R$ with decidable equality, serving as a reference system;
two binary linear codes $C_1, C_2 \subseteq \mathbb{F}_2^n$ , i.e. arbitrary $\mathbb{F}_2$ -subspaces.

For a subspace $C$ , write $C^\perp = \{x \in \mathbb{F}_2^n : c \cdot x = 0 \text{ for all } c \in C\}$ for its dual under the standard dot product over $\mathbb{F}_2$ . The first hypothesis is

C_2^\perp \subseteq C_1 .

Decoders. Two arbitrary maps $\mathrm{dec}_P, \mathrm{dec}_B : \mathbb{F}_2^n \to \mathbb{F}_2^n$ are given. They are assumed to preserve syndromes in the following sense:

for every $w$ and every $h \in C_2^\perp$ : $h \cdot \mathrm{dec}_P(w) = h \cdot w$ ;
for every $w$ and every $h \in C_1^\perp$ : $h \cdot \mathrm{dec}_B(w) = h \cdot w$ .

The identity map satisfies both conditions, so these hypotheses are satisfiable.

Wire sets and operators. Further data:

six arbitrary finite sets of wires $f_P, f_B, g_P, g_B, h_P, h_B \subseteq \{0,\dots,n-1\}$ ;
four $2^n \times 2^n$ complex matrices $F_P, F_B, H_P, H_B$ on $n$ qubits;
two complex matrices $G_P, G_B$ on two $n$ -qubit registers, indexed by $\{0,1\}^n \times \{0,1\}^n$ .

None of these matrices is assumed unitary or normalized.

What "acts within" means. A matrix $E$ on $n$ qubits acts within a set $F$ if there exist:

some $k$ ,
an injective map $w$ from $\{0,\dots,k-1\}$ into the wires, with image contained in $F$ , and
a $2^k \times 2^k$ matrix $M$ ,

such that $E$ equals the embedding of $M$ on wires $w$ . That embedding has entries

E_{y,z} = \begin{cases} M_{y\circ w,\, z\circ w} & \text{if } y_a = z_a \text{ for every wire } a \notin \operatorname{range}(w),\\ 0 & \text{otherwise.}\end{cases}

In words, $E$ is $M$ on the wires $w$ tensored with the identity elsewhere. Because $M$ is arbitrary, the zero matrix and scalar multiples of the identity qualify for any $F$ .

The hypotheses are:

$F_P$ acts within $f_P$ and $F_B$ acts within $f_B$ ;
$H_P$ acts within $h_P$ and $H_B$ acts within $h_B$ ;
$G_P$ satisfies the undisclosed predicate ActsWithinPair with respect to $g_P$ , and $G_B$ with respect to $g_B$ .

Remaining inputs. Also given are an arbitrary vector $\psi \in \mathbb{C}^{\{0,1\}^n \times R}$ and two arbitrary bit vectors $w_P, w_B \in \mathbb{F}_2^n$ . The vector $\psi$ is not assumed to be normalized or to lie in any code space.

Conclusion, first part. Let $\Omega$ be the vector produced by the undisclosed function steaneECOutput, applied to

C_1,\ C_2,\ \mathrm{dec}_P,\ \mathrm{dec}_B,\ F_P,\ F_B,\ H_P,\ H_B,\ G_P,\ G_B,\ \psi,\ w_P,\ w_B .

Let $U = f_P \cup f_B \cup g_P \cup g_B \cup h_P \cup h_B$ . The theorem asserts that $\Omega$ lies in the error space with reference built from the CSS code of $C_1, C_2$ and the wire set $U$ . Unfolded:

The CSS code. For each $u \in C_1$ , the coset state is

|u + C_2^\perp\rangle = \sum_{v \in C_2^\perp} |u+v\rangle,

where $|u+v\rangle$ is the computational basis vector of the bit string $u+v$ . This state is unnormalized. The CSS code $\mathrm{CSS}(C_1,C_2)$ is the complex linear span of these states over all $u \in C_1$ .

The error space. The error space $\mathcal{E}(U)$ is the complex span of all vectors $E c$ such that $E$ is any $n$ -qubit matrix acting within $U$ and $c \in \mathrm{CSS}(C_1,C_2)$ .
The error space with reference. This is the complex span of all product vectors $v \otimes r$ , with $v \in \mathcal{E}(U)$ and $r \in \mathbb{C}^R$ arbitrary. Here $(v\otimes r)_{(z,s)} = v_z\, r_s$ .

So the first part reads:

\Omega \in \operatorname{span}_{\mathbb{C}}\{\, v \otimes r : v \in \mathcal{E}(U),\ r \in \mathbb{C}^R \,\}.

Conclusion, second part. The theorem also asserts

|U| \le |f_P| + |f_B| + |g_P| + |g_B| + |h_P| + |h_B| .

This inequality holds for any six finite sets, independently of every hypothesis.

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Goku · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph