Correctable errors are closed under linear combinations; weight-t Pauli errors give all t-qubit errors

Open

QAlgorithms.GottesmanIntro.corrects_linearCombination

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

gottesman-introlecture-notesquantum-information

Let $C$ be a quantum code on $n$ qubits, i.e. a linear subspace of $(\mathbb C^2)^{\otimes n}$ . Say that $C$ corrects a set $\mathcal S$ of operators if there is one quantum operation $\mathcal R$ (a trace-preserving map $\rho\mapsto\sum_i R_i\rho R_i^\dagger$ , $\sum_i R_i^\dagger R_i=I$ ) such that for every $E\in\mathcal S$ and every unit vector $|\psi\rangle\in C$ ,

\mathcal R\big(E|\psi\rangle\langle\psi|E^\dagger\big)=\|E|\psi\rangle\|^2\,|\psi\rangle\langle\psi|.

Then:

If $C$ corrects $\{A,B\}$ , then $C$ corrects the whole linear span $\{aA+bB : a,b\in\mathbb C\}$ .
For every $t$ , if $C$ corrects every Pauli operator of weight at most $t$ (a tensor product of $I,X,Y,Z$ with a phase, at most $t$ factors different from $I$ ), then $C$ corrects every operator that acts on at most $t$ qubits. Such an operator has the form $M\otimes I$ for an arbitrary, not necessarily unitary, operator $M$ on a set of at most $t$ qubits.

The theorem reduces error correction to a basis of errors. It is why it suffices to correct the discrete Pauli errors in order to correct arbitrary, even continuous or non-unitary, errors on few qubits.

Formalization Note The factor $\|E|\psi\rangle\|^2$ is forced by trace preservation of $\mathcal R$ . One recovery must serve all errors at once: this is the source's procedure (record the error, measure, invert). With separate recoveries the claim fails.

Preamble

import Definitions.Def_QAlgorithms_Defs_FTCircuit
set_option autoImplicit false

Formal statement

namespace QAlgorithms.GottesmanIntro

open scoped Matrix

open QAlgorithms Stabilizer


/-- Gottesman intro p.4, Theorem 2: for an `n`-qubit quantum code `C`, (1) if `C` corrects the
errors `A` and `B` (with one recovery operation), it corrects every linear combination of `A`
and `B` (all of them with one recovery operation); (2) if `C` corrects all Pauli errors of
weight at most `t`, it corrects all errors acting on at most `t` qubits (arbitrary, not
necessarily unitary, operators; p.5). -/
theorem corrects_linearCombination (n : ℕ) (C : Submodule ℂ (EuclideanSpace ℂ (Qubits n))) :
    (∀ A B : Matrix (Qubits n) (Qubits n) ℂ, Corrects C {A, B} →
      Corrects C (Submodule.span ℂ {A, B} : Set (Matrix (Qubits n) (Qubits n) ℂ))) ∧
    ∀ t : ℕ, Corrects C {M | ∃ P : PauliString n, P.weight ≤ t ∧ M = P.toMatrix} →
      Corrects C {E | ActsOnAtMost t E} := by
  sorry



end QAlgorithms.GottesmanIntro

Source

Daniel Gottesman, An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation, 2009, v1, PDF p. 4, Theorem 2. https://arxiv.org/pdf/0904.2557v1

Read-back

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

Setting. Fix $n\in\mathbb{N}$ and a complex subspace $C\subseteq\mathbb{C}^{\{0,1\}^n}$ (the $n$ -qubit state space).

Correctability. For a set $S$ of $2^n\times 2^n$ complex matrices, " $C$ corrects $S$ " means the following. There exists a single map $R$ from $2^n\times2^n$ matrices to $2^n\times2^n$ matrices that is a Kraus-form channel, meaning $R(\rho)=\sum_j K_j\rho K_j^\dagger$ for finitely many $K_j$ with $\sum_j K_j^\dagger K_j=I$ . This one $R$ must satisfy, for every $E\in S$ and every unit vector $\psi\in C$ ,

R\big(|E\psi\rangle\langle E\psi|\big)=\|E\psi\|^2\,|\psi\rangle\langle\psi|.

The theorem is a conjunction of two statements.

Spans. For all matrices $A,B$ : if $C$ corrects $\{A,B\}$ , then $C$ corrects the entire complex linear span $\{\alpha A+\beta B:\alpha,\beta\in\mathbb{C}\}$ .
From Paulis to local errors. For every $t\in\mathbb{N}$ , suppose $C$ corrects the set of Pauli-string matrices of weight $\le t$ . Then $C$ corrects every matrix acting on at most $t$ qubits.
- Pauli strings. These are the matrices

i^{c}\,\sigma_{1}\otimes\cdots\otimes\sigma_{n}, \qquad c\in\{0,1,2,3\},\ \sigma_q\in\{I,X,Y,Z\},

 where $Y=\begin{pmatrix}0&-i\\ i&0\end{pmatrix}$. Factor $q$ acts on wire $q$.

Weight. The weight of a Pauli string is the number of factors $\sigma_q\ne I$ . The overall phase is unrestricted.
Acting on at most $t$ qubits. $E$ acts on at most $t$ qubits if there are:
- a set $F$ of at most $t$ wires;
- an injective listing $w:\{0,\dots,k-1\}\to\{0,\dots,n-1\}$ with image inside $F$ ;
- an arbitrary (not necessarily unitary) $2^k\times2^k$ matrix $M$ ,
such that $E$ is $M$ placed on wires $w$ and the identity elsewhere. Explicitly, $E_{y,z}=M_{y\circ w,\;z\circ w}$ when $y$ and $z$ agree outside the image of $w$ , and $E_{y,z}=0$ otherwise.

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