Knill–Laflamme condition for quantum error correction

Open

QAlgorithms.GottesmanIntro.knillLaflamme

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

gottesman-introlecture-notesquantum-information

This is the Knill–Laflamme criterion.

Let $\mathcal H$ be a finite-dimensional Hilbert space, $\mathcal E$ a linear space of operators on $\mathcal H$ (the errors) and $C\subseteq\mathcal H$ a subspace. Say $C$ corrects $\mathcal E$ if there is a quantum operation $\mathcal R$ on $\mathcal H$ (a map $\rho\mapsto\sum_i R_i\rho R_i^\dagger$ with $\sum_i R_i^\dagger R_i=I$ ) such that $\mathcal R(E|\psi\rangle\langle\psi|E^\dagger)=\|E|\psi\rangle\|^2|\psi\rangle\langle\psi|$ for all $E\in\mathcal E$ and all unit vectors $|\psi\rangle\in C$ . Then $C$ corrects $\mathcal E$ if and only if there is a function $c:\mathcal E\to\mathbb C$ such that

\langle\psi|E^\dagger E|\psi\rangle=c(E)\qquad\text{for all }E\in\mathcal E\text{ and all unit vectors }|\psi\rangle\in C.

The criterion turns the existence of a recovery operation into a checkable condition on the code alone. It is the basis of the distance, degeneracy and counting bounds that follow.

Formalization Note The function $c$ is quantified before $|\psi\rangle$ , so it does not depend on the state. Codewords are normalized, following the source's convention of omitted normalization (p.2).

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.6, Theorem 3 (Knill–Laflamme): for a linear space `𝓔` of errors on a
finite-dimensional Hilbert space `H` and a subspace `C` of `H`, `C` is a quantum
error-correcting code correcting `𝓔` iff there is a function `c(E)`, independent of the state,
with `⟨ψ|E†E|ψ⟩ = c(E)` for all `E ∈ 𝓔` and all normalized `|ψ⟩ ∈ C` (eq. (29)). -/
theorem knillLaflamme {ι : Type*} [Fintype ι] [DecidableEq ι]
    (𝓔 : Submodule ℂ (Matrix ι ι ℂ)) (C : Submodule ℂ (EuclideanSpace ℂ ι)) :
    Corrects C (𝓔 : Set (Matrix ι ι ℂ)) ↔
      ∃ c : Matrix ι ι ℂ → ℂ, ∀ E ∈ 𝓔, ∀ ψ ∈ C, ‖ψ‖ = 1 → inner ℂ ψ (act (Eᴴ * E) ψ) = c E := by
  sorry


end QAlgorithms.GottesmanIntro

Source

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

Read-back

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

Setting. Let $\iota$ be a finite index set with decidable equality. Let $\mathcal{E}$ be a complex linear subspace of the $\iota\times\iota$ complex matrices, and let $C$ be a complex subspace of $\mathbb{C}^\iota$ .

Statement. The following are equivalent.

$C$ corrects $\mathcal{E}$ . There is a single Kraus-form channel $R$ with the following property. Here $R(\rho)=\sum_j K_j\rho K_j^\dagger$ for finitely many $\iota\times\iota$ matrices $K_j$ with $\sum_j K_j^\dagger K_j=I$ . For every $E\in\mathcal{E}$ and every unit vector $\psi\in C$ ,

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

Here $|\phi\rangle\langle\phi|$ is the matrix $(a,b)\mapsto\phi_a\overline{\phi_b}$ .

Constant expectation. There is a function $c$ from matrices to $\mathbb{C}$ such that, for every $E\in\mathcal{E}$ and every unit vector $\psi\in C$ ,

\langle\psi,\,E^\dagger E\,\psi\rangle=c(E).

The inner product is conjugate-linear in its first argument.

Condition 2 constrains only the diagonal expectations $\langle\psi,E^\dagger E\psi\rangle$ of single operators $E\in\mathcal{E}$ . It requires these to be independent of the unit codeword $\psi$ . It does not explicitly mention cross terms $\langle\psi_i,E^\dagger F\psi_j\rangle$ .

If $C=\{0\}$ , there are no unit vectors in $C$ , and both sides hold trivially.

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