Stabiliser codes meet Knill–Laflamme: the recovery of a distance-detected error family

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #14(b), the general half.

QuantumInfo/Stabilizer.lean builds the stabiliser group average P on the register and QuantumInfo/KnillLaflamme.lean constructs a recovery channel from the condition P Eᵢᴴ Eⱼ P = cᵢⱼ P. This file connects them for Pauli error families on a stabiliser code:

• pauliMat a b — the Pauli X^a Z^b as a matrix on the register's coordinates, with pauliMat_mulVec identifying it with pauliOp; the Pauli group law pauliMat_mul, the commutation rule pauliMat_comm, and the adjoint pauliMat_conjTranspose ((X^a Z^b)ᴴ = (−1)^{a·b} X^a Z^b) all transported through Matrix.ext_of_mulVec;
• stabMat A B σ — the group average as a matrix; ★ isCodeProjector_stabMat (Hermitian: every signed group element is self-adjoint because coherence forces bdot (B x) (A x) = 0; idempotent by stabProjector_idem), stabMat_ne_zero, and the two-sided absorption genMat_mul_stabMat, stabMat_mul_genMat;
• ★ stabMat_mul_pauliMat_mul_stabMat_eq_zero — a Pauli anticommuting with a generator is killed by the code: P M P = P (G M) P = −P (M G) P = −P M P;
• ★★ stabMat_knillLaflamme — a Pauli error family whose pairwise products are detected (for i ≠ j some generator anticommutes with Eᵢᴴ Eⱼ, i.e. the syndromes differ) satisfies Knill–Laflamme with c = 1: the code is non-degenerate for the family;
• ★★ exists_recovery_stabMat — the recovery channel: R (Eᵢ ρ Eᵢᴴ) = ρ on every code state, for every error of the family. The Steane instance is Empirical/QM/QEC/SteaneRecovery.lean.

Honest scope

⚠️ The detection hypothesis is stated as a syndrome condition on labels, not derived from a distance: a code of distance d detects every Pauli of weight < d, but "weight" and "distance" are not defined here. Degenerate families (products in the stabiliser) are covered by KnillLaflamme.lean but not by this file's c = 1 statement.

References: D. Gottesman, Stabilizer codes and quantum error correction (1997), §3; Nielsen–Chuang Thm 10.8; QuantumInfo/KnillLaflamme.lean; QuantumInfo/Stabilizer.lean; specs/BACKLOG.md #14; specs/steane-plan.md.

Matrices from their action

theorem Matrix.ext_of_mulVec {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M N : Matrix ι ι ℂ} (h : ∀ (v : ι → ℂ), M.mulVec v = N.mulVec v) : M = N

Two matrices with the same action on every vector are equal.

Pauli matrices

noncomputable def QuantumInfo.pauliMat {n : ℕ} (a b : Fin n → Fin 2) : Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ

The Pauli X^a Z^b as a matrix on the register's coordinates: (X^a Z^b) z w = [w = z + a] · (−1)^{b·w}.

Equations

• QuantumInfo.pauliMat a b z w = if w = z + a then QuantumInfo.pauliSign b w else 0

theorem QuantumInfo.add_add_self {n : ℕ} (z a : Fin n → Fin 2) : z + a + a = z

theorem QuantumInfo.pauliMat_mulVec {n : ℕ} (a b : Fin n → Fin 2) (v : (Fin n → Fin 2) → ℂ) : (pauliMat a b).mulVec v = (pauliOp a b (WithLp.toLp 2 v)).ofLp

The Pauli matrix acts as pauliOp.

theorem QuantumInfo.pauliMat_zero {n : ℕ} : pauliMat 0 0 = 1

theorem QuantumInfo.pauliMat_mul {n : ℕ} (a b a' b' : Fin n → Fin 2) : pauliMat a b * pauliMat a' b' = pauliSign b a' • pauliMat (a + a') (b + b')

The Pauli group law in matrix form.

theorem QuantumInfo.pauliMat_comm {n : ℕ} (a b a' b' : Fin n → Fin 2) : pauliMat a b * pauliMat a' b' = signChar (bdot a b' + bdot b a') • (pauliMat a' b' * pauliMat a b)

Commutation in matrix form: the symplectic sign.

theorem QuantumInfo.pauliMat_conjTranspose {n : ℕ} (a b : Fin n → Fin 2) : (pauliMat a b).conjTranspose = pauliSign b a • pauliMat a b

The adjoint of a Pauli: (X^a Z^b)ᴴ = (−1)^{b·a} X^a Z^b.

theorem QuantumInfo.pauliMat_conjTranspose_mul_self {n : ℕ} (a b : Fin n → Fin 2) : (pauliMat a b).conjTranspose * pauliMat a b = 1

A Pauli is unitary: Eᴴ E = 1.

The stabiliser projector as a matrix

noncomputable def QuantumInfo.genMat {n m : ℕ} (A B : (Fin m → Fin 2) → Fin n → Fin 2) (σ : (Fin m → Fin 2) → Fin 2) (x : Fin m → Fin 2) : Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ

The signed group element χ(σx) X^{Ax} Z^{Bx} as a matrix.

Equations

• QuantumInfo.genMat A B σ x = QuantumInfo.signChar (σ x) • QuantumInfo.pauliMat (A x) (B x)

noncomputable def QuantumInfo.stabMat {n m : ℕ} (A B : (Fin m → Fin 2) → Fin n → Fin 2) (σ : (Fin m → Fin 2) → Fin 2) : Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ

The stabiliser group average as a matrix.

Equations

• QuantumInfo.stabMat A B σ = (2 ^ m)⁻¹ • ∑ x : Fin m → Fin 2, QuantumInfo.genMat A B σ x

theorem QuantumInfo.genMat_mulVec {n m : ℕ} (A B : (Fin m → Fin 2) → Fin n → Fin 2) (σ : (Fin m → Fin 2) → Fin 2) (x : Fin m → Fin 2) (v : (Fin n → Fin 2) → ℂ) : (genMat A B σ x).mulVec v = (signChar (σ x) • pauliOp (A x) (B x) (WithLp.toLp 2 v)).ofLp

theorem QuantumInfo.stabMat_mulVec {n m : ℕ} (A B : (Fin m → Fin 2) → Fin n → Fin 2) (σ : (Fin m → Fin 2) → Fin 2) (v : (Fin n → Fin 2) → ℂ) : (stabMat A B σ).mulVec v = (stabProjector A B σ (WithLp.toLp 2 v)).ofLp

The matrix acts as stabProjector.

theorem QuantumInfo.bdot_B_A_eq_zero {n m : ℕ} {A B : (Fin m → Fin 2) → Fin n → Fin 2} {σ : (Fin m → Fin 2) → Fin 2} (hB : ∀ (x y : Fin m → Fin 2), B (x + y) = B x + B y) (hσ : ∀ (x y : Fin m → Fin 2), σ (x + y) = σ x + σ y + bdot (B x) (A y)) (x : Fin m → Fin 2) : bdot (B x) (A x) = 0

Coherence at (x, x) forces bdot (B x) (A x) = 0: every group element is Hermitian.

theorem QuantumInfo.genMat_conjTranspose {n m : ℕ} {A B : (Fin m → Fin 2) → Fin n → Fin 2} {σ : (Fin m → Fin 2) → Fin 2} (hB : ∀ (x y : Fin m → Fin 2), B (x + y) = B x + B y) (hσ : ∀ (x y : Fin m → Fin 2), σ (x + y) = σ x + σ y + bdot (B x) (A y)) (x : Fin m → Fin 2) : (genMat A B σ x).conjTranspose = genMat A B σ x

theorem QuantumInfo.genMat_mul_stabMat {n m : ℕ} {A B : (Fin m → Fin 2) → Fin n → Fin 2} {σ : (Fin m → Fin 2) → Fin 2} (hA : ∀ (x y : Fin m → Fin 2), A (x + y) = A x + A y) (hB : ∀ (x y : Fin m → Fin 2), B (x + y) = B x + B y) (hσ : ∀ (x y : Fin m → Fin 2), σ (x + y) = σ x + σ y + bdot (B x) (A y)) (x : Fin m → Fin 2) : genMat A B σ x * stabMat A B σ = stabMat A B σ

Left absorption: G P = P.

theorem QuantumInfo.stabMat_conjTranspose {n m : ℕ} {A B : (Fin m → Fin 2) → Fin n → Fin 2} {σ : (Fin m → Fin 2) → Fin 2} (hB : ∀ (x y : Fin m → Fin 2), B (x + y) = B x + B y) (hσ : ∀ (x y : Fin m → Fin 2), σ (x + y) = σ x + σ y + bdot (B x) (A y)) : (stabMat A B σ).conjTranspose = stabMat A B σ

theorem QuantumInfo.stabMat_mul_genMat {n m : ℕ} {A B : (Fin m → Fin 2) → Fin n → Fin 2} {σ : (Fin m → Fin 2) → Fin 2} (hA : ∀ (x y : Fin m → Fin 2), A (x + y) = A x + A y) (hB : ∀ (x y : Fin m → Fin 2), B (x + y) = B x + B y) (hσ : ∀ (x y : Fin m → Fin 2), σ (x + y) = σ x + σ y + bdot (B x) (A y)) (x : Fin m → Fin 2) : stabMat A B σ * genMat A B σ x = stabMat A B σ

Right absorption: P G = P.

theorem QuantumInfo.isCodeProjector_stabMat {n m : ℕ} {A B : (Fin m → Fin 2) → Fin n → Fin 2} {σ : (Fin m → Fin 2) → Fin 2} (hA : ∀ (x y : Fin m → Fin 2), A (x + y) = A x + A y) (hB : ∀ (x y : Fin m → Fin 2), B (x + y) = B x + B y) (hσ : ∀ (x y : Fin m → Fin 2), σ (x + y) = σ x + σ y + bdot (B x) (A y)) : IsCodeProjector (stabMat A B σ)

★ The group average is a code projector.

theorem QuantumInfo.stabMat_ne_zero {n m : ℕ} {A B : (Fin m → Fin 2) → Fin n → Fin 2} {σ : (Fin m → Fin 2) → Fin 2} (hA : ∀ (x y : Fin m → Fin 2), A (x + y) = A x + A y) (hB : ∀ (x y : Fin m → Fin 2), B (x + y) = B x + B y) (hσ : ∀ (x y : Fin m → Fin 2), σ (x + y) = σ x + σ y + bdot (B x) (A y)) (hinj : ∀ (x : Fin m → Fin 2), A x = 0 → B x = 0 → x = 0) : stabMat A B σ ≠ 0

The code is nonzero (independent labels).

Detected Paulis are killed by the code

theorem QuantumInfo.stabMat_mul_pauliMat_mul_stabMat_eq_zero {n m : ℕ} {A B : (Fin m → Fin 2) → Fin n → Fin 2} {σ : (Fin m → Fin 2) → Fin 2} (hA : ∀ (x y : Fin m → Fin 2), A (x + y) = A x + A y) (hB : ∀ (x y : Fin m → Fin 2), B (x + y) = B x + B y) (hσ : ∀ (x y : Fin m → Fin 2), σ (x + y) = σ x + σ y + bdot (B x) (A y)) {u v : Fin n → Fin 2} (x : Fin m → Fin 2) (hx : bdot (A x) v + bdot (B x) u = 1) : stabMat A B σ * pauliMat u v * stabMat A B σ = 0

★ A Pauli anticommuting with some generator is killed by the code: P M P = 0.

theorem QuantumInfo.stabMat_knillLaflamme {n m : ℕ} {A B : (Fin m → Fin 2) → Fin n → Fin 2} {σ : (Fin m → Fin 2) → Fin 2} (hA : ∀ (x y : Fin m → Fin 2), A (x + y) = A x + A y) (hB : ∀ (x y : Fin m → Fin 2), B (x + y) = B x + B y) (hσ : ∀ (x y : Fin m → Fin 2), σ (x + y) = σ x + σ y + bdot (B x) (A y)) {ι : Type u_1} [DecidableEq ι] (a b : ι → Fin n → Fin 2) (hsyn : ∀ (i j : ι), i ≠ j → ∃ (x : Fin m → Fin 2), bdot (A x) (b i + b j) + bdot (B x) (a i + a j) = 1) : KnillLaflamme (stabMat A B σ) (fun (i : ι) => pauliMat (a i) (b i)) 1

★★ A detected Pauli error family satisfies Knill–Laflamme with c = 1: for i ≠ j some generator anticommutes with Eᵢᴴ Eⱼ (the labels (aᵢ + aⱼ, bᵢ + bⱼ) pair to 1 with some generator), so the code is non-degenerate for the family.

theorem QuantumInfo.exists_recovery_stabMat {n m : ℕ} {A B : (Fin m → Fin 2) → Fin n → Fin 2} {σ : (Fin m → Fin 2) → Fin 2} (hA : ∀ (x y : Fin m → Fin 2), A (x + y) = A x + A y) (hB : ∀ (x y : Fin m → Fin 2), B (x + y) = B x + B y) (hσ : ∀ (x y : Fin m → Fin 2), σ (x + y) = σ x + σ y + bdot (B x) (A y)) (hinj : ∀ (x : Fin m → Fin 2), A x = 0 → B x = 0 → x = 0) {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a b : ι → Fin n → Fin 2) (hsyn : ∀ (i j : ι), i ≠ j → ∃ (x : Fin m → Fin 2), bdot (A x) (b i + b j) + bdot (B x) (a i + a j) = 1) : ∃ (R : Channel (Fin n → Fin 2) (Fin n → Fin 2) (Option ι)), ∀ (ρ : Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ), ρ = stabMat A B σ * ρ * stabMat A B σ → ∀ (i : ι), R.apply (pauliMat (a i) (b i) * ρ * (pauliMat (a i) (b i)).conjTranspose) = ρ

★★ The recovery channel of a stabiliser code for a detected Pauli error family: every error of the family is undone on every code state, R (Eᵢ ρ Eᵢᴴ) = ρ for ρ = P ρ P.