The Knill–Laflamme conditions

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #14(a), the first brick of active error correction.

Glossary: https://glossary.constraintsurfacedynamics.com/knill-laflamme/ Plain-language, CSD-role and formal statements of the Knill-Laflamme conditions, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

A code is an orthogonal projector P on a finite-dimensional Hilbert space; a family of error operators E i is correctable on the code when some quantum channel R (the recovery) undoes every error on every code state: R (E i ρ E iᴴ) = λ i • ρ whenever ρ = P ρ P. The Knill–Laflamme condition is the algebraic criterion

P E iᴴ E j P = c i j • P for some matrix c,

and the theorem is that the two are equivalent (Knill–Laflamme 1997; Nielsen–Chuang Thm 10.1):

• ★★ exists_recovery_of_knillLaflamme — the recovery map exists: from the condition, with c Hermitian (KnillLaflamme.isHermitian), diagonalise c = U D U* (Mathlib's Matrix.IsHermitian.spectral_theorem; U = klUnitary); the canonical errors F k = ∑ᵢ U i k • E i satisfy P F kᴴ F l P = d k δ_kl P with d k ≥ 0 (knillLaflamme_canonicalError), so their images of the code are orthogonal; the Kraus operators R k = d k^{−1/2} P F kᴴ (for d k ≠ 0) have R kᴴ R k = d k⁻¹ F k P F kᴴ, orthogonal projectors summing to Q, and 1 − Q completes the channel (recoveryChannel); on a code state R (F k ρ F lᴴ) = d k δ_kl ρ (recoveryChannel_apply), hence R (E i ρ E jᴴ) = c j i • ρ;
• ★ exists_recovery_channel_of_knillLaflamme — for a noise channel 𝓔 with Kraus operators E, R (𝓔 ρ) = ρ on the code: trace preservation makes tr c = 1;
• ★★ knillLaflamme_of_recovery — the converse: if a channel corrects the errors up to scalars, the condition holds. Each R k E i P maps every code vector to a multiple of itself (exists_smul_of_sum_conj_eq: the sandwiched identity ∑ₖ |⟨u, R k E i v⟩|² = λ |⟨u, v⟩|² with u the component of R k E i v orthogonal to v), hence is a scalar on the code (exists_smul_of_forall_smul), and P E iᴴ E j P = ∑ₖ (R k E i P)ᴴ (R k E j P) by trace preservation;
• knillLaflamme_iff — the equivalence;
• ★★ recovery_apply_lin_comb — discretization: the correction property is bilinear in the two error slots and a channel is linear, so a recovery corrects every linear combination of the family, up to the scalar the coefficients give (exists_smul_recovery_apply_of_eq_lin_comb is the existential form). Correcting the four Paulis on a qubit therefore corrects every operator on that qubit.

Honest scope

⚠️ Matrices over ℂ on a finite index type; the code is a projector, not a subspace, and no stabiliser structure is assumed (the stabiliser instances — Steane, BACKLOG #14(b) — are downstream). Degenerate codes are covered (c need not be invertible: d k = 0 errors act as 0 on the code). The recovery is constructed, not shown unique.

References: E. Knill, R. Laflamme, Theory of quantum error-correcting codes, Phys. Rev. A 55 (1997) 900; M. Nielsen, I. Chuang, Quantum Computation and Quantum Information, Thm 10.1; QuantumInfo/Channel.lean; specs/BACKLOG.md #14; specs/steane-plan.md; docs/FROM-POSTULATES-TO-QUANTUM-COMPUTERS.md §10.

Code projectors

structure QuantumInfo.IsCodeProjector {n : Type u_1} [Fintype n] (P : Matrix n n ℂ) : Prop

A code projector: an orthogonal projector P (Hermitian and idempotent).

• conjTranspose_eq : P.conjTranspose = P
• mul_self : P * P = P

theorem QuantumInfo.IsCodeProjector.posSemidef {n : Type u_1} [Fintype n] {P : Matrix n n ℂ} (hP : IsCodeProjector P) : P.PosSemidef

theorem QuantumInfo.IsCodeProjector.trace_pos {n : Type u_1} [Fintype n] {P : Matrix n n ℂ} (hP : IsCodeProjector P) (hP0 : P ≠ 0) : 0 < P.trace

theorem QuantumInfo.IsCodeProjector.smul_injective {n : Type u_1} {P : Matrix n n ℂ} (hP0 : P ≠ 0) {a b : ℂ} (h : a • P = b • P) : a = b

A nonzero matrix determines the scalar multiplying it.

theorem QuantumInfo.IsCodeProjector.nonneg_of_smul_posSemidef {n : Type u_1} [Fintype n] {P : Matrix n n ℂ} (hP : IsCodeProjector P) (hP0 : P ≠ 0) {a : ℝ} (h : (↑a • P).PosSemidef) : 0 ≤ a

A real scalar a with a • P positive semidefinite is nonnegative.

The Knill–Laflamme condition

def QuantumInfo.KnillLaflamme {n : Type u_1} [Fintype n] {ι : Type u_2} (P : Matrix n n ℂ) (E : ι → Matrix n n ℂ) (c : Matrix ι ι ℂ) : Prop

The Knill–Laflamme condition for the errors E on the code P, with matrix c: P E iᴴ E j P = c i j • P.

Equations

• QuantumInfo.KnillLaflamme P E c = ∀ (i j : ι), P * (E i).conjTranspose * E j * P = c i j • P

theorem QuantumInfo.KnillLaflamme.isHermitian {n : Type u_1} [Fintype n] {ι : Type u_2} {P : Matrix n n ℂ} {E : ι → Matrix n n ℂ} {c : Matrix ι ι ℂ} (hP : IsCodeProjector P) (hP0 : P ≠ 0) (hc : KnillLaflamme P E c) : c.IsHermitian

The Knill–Laflamme matrix of a nonzero code is Hermitian.

theorem QuantumInfo.Channel.apply_sum {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_3} {κ : Type u_4} [Fintype m] [Fintype κ] (Φ : Channel n m κ) {α : Type u_5} (s : Finset α) (f : α → Matrix n n ℂ) : Φ.apply (∑ a ∈ s, f a) = ∑ a ∈ s, Φ.apply (f a)

A channel applied to a finite sum.

The recovery channel of an orthogonal error family

noncomputable def QuantumInfo.recoveryOp {n : Type u_1} [Fintype n] {κ : Type u_3} (P : Matrix n n ℂ) (F : κ → Matrix n n ℂ) (d : κ → ℝ) (k : κ) : Matrix n n ℂ

The recovery Kraus operator of the k-th orthogonal error: d k^{−1/2} P F kᴴ, or 0 when d k = 0.

Equations

• QuantumInfo.recoveryOp P F d k = if d k = 0 then 0 else ↑(√(d k))⁻¹ • (P * (F k).conjTranspose)

noncomputable def QuantumInfo.errorImageProj {n : Type u_1} [Fintype n] {κ : Type u_3} (P : Matrix n n ℂ) (F : κ → Matrix n n ℂ) (d : κ → ℝ) (k : κ) : Matrix n n ℂ

The projector d k⁻¹ F k P F kᴴ onto the image of the code under the k-th error.

Equations

• QuantumInfo.errorImageProj P F d k = if d k = 0 then 0 else ↑(d k)⁻¹ • (F k * P * (F k).conjTranspose)

noncomputable def QuantumInfo.recoveryProj {n : Type u_1} [Fintype n] {κ : Type u_3} (P : Matrix n n ℂ) (F : κ → Matrix n n ℂ) (d : κ → ℝ) [Fintype κ] : Matrix n n ℂ

The projector onto the span of all error images: ∑ₖ R kᴴ R k.

Equations

• QuantumInfo.recoveryProj P F d = ∑ k : κ, (QuantumInfo.recoveryOp P F d k).conjTranspose * QuantumInfo.recoveryOp P F d k

noncomputable def QuantumInfo.recoveryKraus {n : Type u_1} [Fintype n] [DecidableEq n] {κ : Type u_3} (P : Matrix n n ℂ) (F : κ → Matrix n n ℂ) (d : κ → ℝ) [Fintype κ] : Option κ → Matrix n n ℂ

The recovery Kraus family: the R k, completed by 1 − ∑ₖ R kᴴ R k.

Equations

• QuantumInfo.recoveryKraus P F d (some k) = QuantumInfo.recoveryOp P F d k
• QuantumInfo.recoveryKraus P F d none = 1 - QuantumInfo.recoveryProj P F d

theorem QuantumInfo.mul_codeProj_eq_zero_of_eq_zero {n : Type u_1} [Fintype n] {κ : Type u_3} [DecidableEq κ] {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} (hP : IsCodeProjector P) (hF : ∀ (k l : κ), P * (F k).conjTranspose * F l * P = if k = l then ↑(d k) • P else 0) {k : κ} (hk : d k = 0) : F k * P = 0

An error with d k = 0 kills the code.

theorem QuantumInfo.recoveryOp_conjTranspose_mul_self {n : Type u_1} [Fintype n] {κ : Type u_3} {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} (hP : IsCodeProjector P) (hd : ∀ (k : κ), 0 ≤ d k) (k : κ) : (recoveryOp P F d k).conjTranspose * recoveryOp P F d k = errorImageProj P F d k

theorem QuantumInfo.errorImageProj_mul {n : Type u_1} [Fintype n] {κ : Type u_3} [DecidableEq κ] {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} (hF : ∀ (k l : κ), P * (F k).conjTranspose * F l * P = if k = l then ↑(d k) • P else 0) (k l : κ) : errorImageProj P F d k * errorImageProj P F d l = if k = l then errorImageProj P F d k else 0

theorem QuantumInfo.errorImageProj_conjTranspose {n : Type u_1} [Fintype n] {κ : Type u_3} {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} (hP : IsCodeProjector P) (k : κ) : (errorImageProj P F d k).conjTranspose = errorImageProj P F d k

theorem QuantumInfo.recoveryProj_eq {n : Type u_1} [Fintype n] {κ : Type u_3} {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} [Fintype κ] (hP : IsCodeProjector P) (hd : ∀ (k : κ), 0 ≤ d k) : recoveryProj P F d = ∑ k : κ, errorImageProj P F d k

theorem QuantumInfo.recoveryProj_mul_self {n : Type u_1} [Fintype n] {κ : Type u_3} [DecidableEq κ] {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} [Fintype κ] (hP : IsCodeProjector P) (hd : ∀ (k : κ), 0 ≤ d k) (hF : ∀ (k l : κ), P * (F k).conjTranspose * F l * P = if k = l then ↑(d k) • P else 0) : recoveryProj P F d * recoveryProj P F d = recoveryProj P F d

theorem QuantumInfo.recoveryProj_conjTranspose {n : Type u_1} [Fintype n] {κ : Type u_3} {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} [Fintype κ] (hP : IsCodeProjector P) (hd : ∀ (k : κ), 0 ≤ d k) : (recoveryProj P F d).conjTranspose = recoveryProj P F d

theorem QuantumInfo.recoveryKraus_tp {n : Type u_1} [Fintype n] [DecidableEq n] {κ : Type u_3} [DecidableEq κ] {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} [Fintype κ] (hP : IsCodeProjector P) (hd : ∀ (k : κ), 0 ≤ d k) (hF : ∀ (k l : κ), P * (F k).conjTranspose * F l * P = if k = l then ↑(d k) • P else 0) : ∑ o : Option κ, (recoveryKraus P F d o).conjTranspose * recoveryKraus P F d o = 1

The recovery Kraus family is trace preserving.

noncomputable def QuantumInfo.recoveryChannel {n : Type u_1} [Fintype n] [DecidableEq n] {κ : Type u_3} [DecidableEq κ] {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} [Fintype κ] (hP : IsCodeProjector P) (hd : ∀ (k : κ), 0 ≤ d k) (hF : ∀ (k l : κ), P * (F k).conjTranspose * F l * P = if k = l then ↑(d k) • P else 0) : Channel n n (Option κ)

The recovery channel of an orthogonal error family.

Equations

• QuantumInfo.recoveryChannel hP hd hF = { kraus := QuantumInfo.recoveryKraus P F d, tp := ⋯ }

theorem QuantumInfo.recoveryOp_mul_mul_codeProj {n : Type u_1} [Fintype n] {κ : Type u_3} [DecidableEq κ] {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} (hF : ∀ (k l : κ), P * (F k).conjTranspose * F l * P = if k = l then ↑(d k) • P else 0) (m k : κ) : recoveryOp P F d m * F k * P = if m = k ∧ d m ≠ 0 then ↑√(d m) • P else 0

theorem QuantumInfo.recoveryOp_conj {n : Type u_1} [Fintype n] {κ : Type u_3} [DecidableEq κ] {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} (hP : IsCodeProjector P) (hd : ∀ (k : κ), 0 ≤ d k) (hF : ∀ (k l : κ), P * (F k).conjTranspose * F l * P = if k = l then ↑(d k) • P else 0) {ρ : Matrix n n ℂ} (hρ : ρ = P * ρ * P) (m k l : κ) : recoveryOp P F d m * (F k * ρ * (F l).conjTranspose) * (recoveryOp P F d m).conjTranspose = if m = k ∧ m = l ∧ d m ≠ 0 then ↑(d m) • ρ else 0

The action of one recovery operator on an error term of a code state.

theorem QuantumInfo.one_sub_recoveryProj_mul {n : Type u_1} [Fintype n] [DecidableEq n] {κ : Type u_3} [DecidableEq κ] {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} [Fintype κ] (hP : IsCodeProjector P) (hd : ∀ (k : κ), 0 ≤ d k) (hF : ∀ (k l : κ), P * (F k).conjTranspose * F l * P = if k = l then ↑(d k) • P else 0) (k : κ) : (1 - recoveryProj P F d) * F k * P = 0

The completion 1 − Q kills every error image of the code.

theorem QuantumInfo.recoveryChannel_apply {n : Type u_1} [Fintype n] [DecidableEq n] {κ : Type u_3} [DecidableEq κ] {P : Matrix n n ℂ} {F : κ → Matrix n n ℂ} {d : κ → ℝ} [Fintype κ] (hP : IsCodeProjector P) (hd : ∀ (k : κ), 0 ≤ d k) (hF : ∀ (k l : κ), P * (F k).conjTranspose * F l * P = if k = l then ↑(d k) • P else 0) {ρ : Matrix n n ℂ} (hρ : ρ = P * ρ * P) (k l : κ) : (recoveryChannel hP hd hF).apply (F k * ρ * (F l).conjTranspose) = if k = l then ↑(d k) • ρ else 0

★ The recovery channel undoes an orthogonal error family on the code: R (F k ρ F lᴴ) = d k δ_kl • ρ for ρ = P ρ P.

Diagonalising the Knill–Laflamme matrix

noncomputable def QuantumInfo.klUnitary {ι : Type u_2} [Fintype ι] [DecidableEq ι] {c : Matrix ι ι ℂ} (hc' : c.IsHermitian) : Matrix ι ι ℂ

The eigenvector unitary of the Knill–Laflamme matrix, as a matrix.

Equations

• QuantumInfo.klUnitary hc' = ↑hc'.eigenvectorUnitary

theorem QuantumInfo.klUnitary_star_mul {ι : Type u_2} [Fintype ι] [DecidableEq ι] {c : Matrix ι ι ℂ} (hc' : c.IsHermitian) : star (klUnitary hc') * klUnitary hc' = 1

theorem QuantumInfo.klUnitary_mul_star {ι : Type u_2} [Fintype ι] [DecidableEq ι] {c : Matrix ι ι ℂ} (hc' : c.IsHermitian) : klUnitary hc' * star (klUnitary hc') = 1

theorem QuantumInfo.eq_klUnitary_mul_diagonal {ι : Type u_2} [Fintype ι] [DecidableEq ι] {c : Matrix ι ι ℂ} (hc' : c.IsHermitian) : c = klUnitary hc' * Matrix.diagonal (RCLike.ofReal ∘ hc'.eigenvalues) * star (klUnitary hc')

noncomputable def QuantumInfo.canonicalError {n : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] {c : Matrix ι ι ℂ} (hc' : c.IsHermitian) (E : ι → Matrix n n ℂ) (k : ι) : Matrix n n ℂ

The canonical errors F k = ∑ᵢ U i k • E i, U the eigenvector unitary of c.

Equations

• QuantumInfo.canonicalError hc' E k = ∑ i : ι, QuantumInfo.klUnitary hc' i k • E i

theorem QuantumInfo.star_klUnitary_mul_mul {ι : Type u_2} [Fintype ι] [DecidableEq ι] {c : Matrix ι ι ℂ} (hc' : c.IsHermitian) : star (klUnitary hc') * c * klUnitary hc' = Matrix.diagonal (RCLike.ofReal ∘ hc'.eigenvalues)

theorem QuantumInfo.knillLaflamme_canonicalError {n : Type u_1} [Fintype n] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {P : Matrix n n ℂ} {E : ι → Matrix n n ℂ} {c : Matrix ι ι ℂ} (hc' : c.IsHermitian) (hc : KnillLaflamme P E c) (k l : ι) : P * (canonicalError hc' E k).conjTranspose * canonicalError hc' E l * P = if k = l then ↑(hc'.eigenvalues k) • P else 0

The canonical errors satisfy the diagonal Knill–Laflamme condition.

theorem QuantumInfo.eq_sum_canonicalError {n : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] {E : ι → Matrix n n ℂ} {c : Matrix ι ι ℂ} (hc' : c.IsHermitian) (i : ι) : E i = ∑ k : ι, star (klUnitary hc' i k) • canonicalError hc' E k

The errors in terms of the canonical ones: E i = ∑ₖ conj(U i k) • F k.

theorem QuantumInfo.knillLaflamme_matrix_apply {ι : Type u_2} [Fintype ι] [DecidableEq ι] {c : Matrix ι ι ℂ} (hc' : c.IsHermitian) (i j : ι) : c j i = ∑ k : ι, klUnitary hc' j k * ↑(hc'.eigenvalues k) * star (klUnitary hc' i k)

The Knill–Laflamme matrix in terms of the eigen-data: c j i = ∑ₖ U j k d k conj(U i k).

The Knill–Laflamme theorem

theorem QuantumInfo.exists_recovery_of_knillLaflamme {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {P : Matrix n n ℂ} {E : ι → Matrix n n ℂ} {c : Matrix ι ι ℂ} (hP : IsCodeProjector P) (hP0 : P ≠ 0) (hc : KnillLaflamme P E c) : ∃ (R : Channel n n (Option ι)), ∀ (ρ : Matrix n n ℂ), ρ = P * ρ * P → ∀ (i j : ι), R.apply (E i * ρ * (E j).conjTranspose) = c j i • ρ

★★ The Knill–Laflamme theorem (recovery exists). If the errors E satisfy the Knill–Laflamme condition on the nonzero code P, there is a channel R with R (E i ρ E jᴴ) = c j i • ρ on every code state ρ = P ρ P; in particular R (E i ρ E iᴴ) = c i i • ρ.

theorem QuantumInfo.exists_recovery_channel_of_knillLaflamme {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {P : Matrix n n ℂ} {c : Matrix ι ι ℂ} (hP : IsCodeProjector P) (hP0 : P ≠ 0) (𝓔 : Channel n n ι) (hc : KnillLaflamme P 𝓔.kraus c) : ∃ (R : Channel n n (Option ι)), ∀ (ρ : Matrix n n ℂ), ρ = P * ρ * P → R.apply (𝓔.apply ρ) = ρ

★ A noise channel satisfying Knill–Laflamme is corrected on the code: for a channel 𝓔 whose Kraus operators satisfy the condition, R (𝓔 ρ) = ρ for every ρ = P ρ P.

Discretization: the recovery corrects the whole span of the errors

theorem QuantumInfo.recovery_apply_lin_comb {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] {P : Matrix n n ℂ} {E : ι → Matrix n n ℂ} {c : Matrix ι ι ℂ} {κ : Type u_3} [Fintype κ] {R : Channel n n κ} (hR : ∀ (ρ : Matrix n n ℂ), ρ = P * ρ * P → ∀ (i j : ι), R.apply (E i * ρ * (E j).conjTranspose) = c j i • ρ) (a : ι → ℂ) {ρ : Matrix n n ℂ} (hρ : ρ = P * ρ * P) : R.apply ((∑ i : ι, a i • E i) * ρ * (∑ i : ι, a i • E i).conjTranspose) = (∑ i : ι, ∑ j : ι, star (a i) * a j * c i j) • ρ

★★ The recovery corrects every linear combination of the error operators, up to the scalar its coefficients give. This is the discretization step: a code that corrects finitely many errors corrects the whole subspace they span, because the correction property is bilinear in the two error slots and the recovery is linear. Correcting the four Paulis on a qubit therefore corrects every operator on that qubit.

theorem QuantumInfo.exists_smul_recovery_apply_of_eq_lin_comb {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] {P : Matrix n n ℂ} {E : ι → Matrix n n ℂ} {c : Matrix ι ι ℂ} {κ : Type u_3} [Fintype κ] {R : Channel n n κ} (hR : ∀ (ρ : Matrix n n ℂ), ρ = P * ρ * P → ∀ (i j : ι), R.apply (E i * ρ * (E j).conjTranspose) = c j i • ρ) {F : Matrix n n ℂ} {a : ι → ℂ} (hF : F = ∑ i : ι, a i • E i) : ∃ (γ : ℂ), ∀ (ρ : Matrix n n ℂ), ρ = P * ρ * P → R.apply (F * ρ * F.conjTranspose) = γ • ρ

The same statement for an error given as a linear combination: if F is a combination of the E i, the recovery returns a multiple of the code state.

The converse: a recovery forces the condition

theorem QuantumInfo.exists_smul_of_forall_smul {n : Type u_1} [Fintype n] [DecidableEq n] {P A : Matrix n n ℂ} (hAP : A * P = A) (h : ∀ (w : n → ℂ), ∃ (α : ℂ), A.mulVec w = α • P.mulVec w) : ∃ (μ : ℂ), A = μ • P

A matrix mapping every vector w to a multiple of P w, and vanishing off the code, is a scalar multiple of P.

theorem QuantumInfo.exists_smul_of_sum_conj_eq {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℂ} {κ : Type u_3} [Fintype κ] (hP : IsCodeProjector P) (A : κ → Matrix n n ℂ) (lam : ℂ) (hA : ∀ (k : κ), A k * P = A k) (h : ∀ (X : Matrix n n ℂ), ∑ k : κ, A k * X * (A k).conjTranspose = lam • (P * X * P)) (k : κ) : ∃ (μ : ℂ), A k = μ • P

Kraus operators of a scalar map on the code are scalars. If ∑ₖ A k X (A k)ᴴ = λ • P X P for every X, and each A k vanishes off the code, then every A k is a scalar multiple of P.

theorem QuantumInfo.knillLaflamme_of_recovery {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} {P : Matrix n n ℂ} {E : ι → Matrix n n ℂ} (hP : IsCodeProjector P) {κ : Type u_3} [Fintype κ] (R : Channel n n κ) (lam : ι → ℂ) (h : ∀ (i : ι) (ρ : Matrix n n ℂ), ρ = P * ρ * P → R.apply (E i * ρ * (E i).conjTranspose) = lam i • ρ) : ∃ (c : Matrix ι ι ℂ), KnillLaflamme P E c

★★ The Knill–Laflamme theorem (the condition is necessary). If a channel R corrects the errors E on the code P up to scalars — R (E i ρ E iᴴ) = λ i • ρ on code states — then the errors satisfy the Knill–Laflamme condition.

theorem QuantumInfo.knillLaflamme_iff {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {P : Matrix n n ℂ} {E : ι → Matrix n n ℂ} (hP : IsCodeProjector P) (hP0 : P ≠ 0) : (∃ (c : Matrix ι ι ℂ), KnillLaflamme P E c) ↔ ∃ (R : Channel n n (Option ι)) (lam : ι → ℂ), ∀ (i : ι) (ρ : Matrix n n ℂ), ρ = P * ρ * P → R.apply (E i * ρ * (E i).conjTranspose) = lam i • ρ

The Knill–Laflamme theorem: the errors E are correctable on the nonzero code P — some channel inverts every error on the code up to a scalar — if and only if they satisfy the Knill–Laflamme condition for some matrix c.

The condition in encoder form

theorem QuantumInfo.isCodeProjector_mul_conjTranspose {n : Type u_1} [Fintype n] {L : Type u_3} [Fintype L] [DecidableEq L] {V : Matrix n L ℂ} (hV : V.conjTranspose * V = 1) : IsCodeProjector (V * V.conjTranspose)

An isometric encoder gives a code projector: P = V Vᴴ for Vᴴ V = 1.

theorem QuantumInfo.mul_conjTranspose_ne_zero {n : Type u_1} [Fintype n] {L : Type u_3} [Fintype L] [DecidableEq L] {V : Matrix n L ℂ} [Nonempty L] (hV : V.conjTranspose * V = 1) : V * V.conjTranspose ≠ 0

The code of an isometric encoder is nonzero as soon as it encodes something.

theorem QuantumInfo.mul_conjTranspose_mul_encoder {n : Type u_1} [Fintype n] {L : Type u_3} [Fintype L] [DecidableEq L] {V : Matrix n L ℂ} (hV : V.conjTranspose * V = 1) : V * V.conjTranspose * V = V

theorem QuantumInfo.conjTranspose_mul_mul_conjTranspose {n : Type u_1} [Fintype n] {L : Type u_3} [Fintype L] [DecidableEq L] {V : Matrix n L ℂ} (hV : V.conjTranspose * V = 1) : V.conjTranspose * (V * V.conjTranspose) = V.conjTranspose

theorem QuantumInfo.knillLaflamme_of_encoder {n : Type u_1} [Fintype n] {ι : Type u_2} {E : ι → Matrix n n ℂ} {c : Matrix ι ι ℂ} {L : Type u_3} [Fintype L] [DecidableEq L] {V : Matrix n L ℂ} (h : ∀ (i j : ι), V.conjTranspose * (E i).conjTranspose * E j * V = c i j • 1) : KnillLaflamme (V * V.conjTranspose) E c

★ Encoder form implies projector form. If the errors are scalar on the encoded qubit, Vᴴ Eᵢᴴ Eⱼ V = cᵢⱼ • 1, they satisfy Knill–Laflamme on the code V Vᴴ. The encoder form is what a concatenation composes: it needs no rank statement relating V Vᴴ to a stabiliser projector, and not even that V is an isometry.

theorem QuantumInfo.encoder_of_knillLaflamme {n : Type u_1} [Fintype n] {ι : Type u_2} {P : Matrix n n ℂ} {E : ι → Matrix n n ℂ} {c : Matrix ι ι ℂ} {L : Type u_3} [DecidableEq L] {V : Matrix n L ℂ} (hP : IsCodeProjector P) (hV : V.conjTranspose * V = 1) (hPV : P * V = V) (hc : KnillLaflamme P E c) (i j : ι) : V.conjTranspose * (E i).conjTranspose * E j * V = c i j • 1

★ Projector form implies encoder form, for an encoder whose columns are code states.

theorem QuantumInfo.encoder_apply_of_eq_one {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} {P : Matrix n n ℂ} {E : ι → Matrix n n ℂ} {c : Matrix ι ι ℂ} {L : Type u_3} [DecidableEq L] {V : Matrix n L ℂ} (hP : IsCodeProjector P) (hV : V.conjTranspose * V = 1) (hPV : P * V = V) (hc : KnillLaflamme P E c) {i₀ : ι} (hi₀ : E i₀ = 1) (j : ι) : V.conjTranspose * E j * V = c i₀ j • 1

The logical action of a single error, for a family containing the identity: the identity's row of the Knill–Laflamme matrix.

def QuantumInfo.EncoderKL {n : Type u_1} [Fintype n] {ι : Type u_2} {L : Type u_3} [DecidableEq L] (V : Matrix n L ℂ) (E : ι → Matrix n n ℂ) : Prop

The Knill–Laflamme condition in encoder form, existential in the scalars: every pair of errors acts on the encoded space as some scalar. This is the form a concatenation carries through its induction, where the scalars themselves are of no interest.

Equations

• QuantumInfo.EncoderKL V E = ∀ (i j : ι), ∃ (γ : ℂ), V.conjTranspose * (E i).conjTranspose * E j * V = γ • 1

theorem QuantumInfo.encoderKL_iff {n : Type u_1} [Fintype n] {ι : Type u_2} {L : Type u_3} [DecidableEq L] {V : Matrix n L ℂ} {E : ι → Matrix n n ℂ} : EncoderKL V E ↔ ∀ (i j : ι), ∃ (γ : ℂ), V.conjTranspose * (E i).conjTranspose * E j * V = γ • 1

theorem QuantumInfo.exists_knillLaflamme_of_encoderKL {n : Type u_1} [Fintype n] {ι : Type u_2} {E : ι → Matrix n n ℂ} {L : Type u_3} [Fintype L] [DecidableEq L] {V : Matrix n L ℂ} (h : EncoderKL V E) : ∃ (c : Matrix ι ι ℂ), KnillLaflamme (V * V.conjTranspose) E c

theorem QuantumInfo.exists_recovery_of_encoderKL {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {E : ι → Matrix n n ℂ} {L : Type u_3} [Fintype L] [DecidableEq L] {V : Matrix n L ℂ} [Nonempty L] (hV : V.conjTranspose * V = 1) (h : EncoderKL V E) : ∃ (c : Matrix ι ι ℂ) (R : Channel n n (Option ι)), ∀ (ρ : Matrix n n ℂ), ρ = V * V.conjTranspose * ρ * (V * V.conjTranspose) → ∀ (i j : ι), R.apply (E i * ρ * (E j).conjTranspose) = c j i • ρ

★★ A recovery from the encoder form: errors that act as scalars on the encoded space are corrected by one channel.

theorem QuantumInfo.smul_eq_one_of_unitary {n : Type u_1} [Fintype n] [DecidableEq n] {κ : Type u_4} [Fintype κ] (R : Channel n n κ) {E ρ : Matrix n n ℂ} (hE : E.conjTranspose * E = 1) {γ : ℂ} (h : R.apply (E * ρ * E.conjTranspose) = γ • ρ) (hρ : ρ.trace ≠ 0) : γ = 1

★ A unitary error is undone exactly: if a recovery returns a code state up to a scalar and the error is unitary, that scalar is 1, because both the error and the channel preserve the trace.