Quantum Hamming Bound

This file proves the quantum Hamming bound for non-degenerate quantum error-correcting codes. It formalizes the n-qubit Pauli error model and the Knill–Laflamme error correction conditions.

Main results

• card_pauliErrorsLe: The number of Pauli strings of weight ≤ t on n qubits equals ∑ j ∈ Finset.range (t + 1), n.choose j * 3 ^ j.
• quantum_hamming_bound_raw: For an [[n, k]] non-degenerate quantum code correcting t errors, (∑ j, C(n,j) * 3^j) * 2^k ≤ 2^n.
• quantum_hamming_bound: The standard form ∑ j, C(n,j) * 3^j ≤ 2^(n-k).

References

• Knill, Laflamme (1997): Theory of quantum error-correcting codes.

inductive PauliBasis : Type

The four-element type indexing the single-qubit Pauli matrices: identity I, bit-flip X, bit-phase-flip Y, and phase-flip Z.

• I : PauliBasis
• X : PauliBasis
• Y : PauliBasis
• Z : PauliBasis

instance instDecidableEqPauliBasis : DecidableEq PauliBasis

Equations

• instDecidableEqPauliBasis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instFintypePauliBasis : Fintype PauliBasis

Equations

• instFintypePauliBasis = { elems := { val := ↑PauliBasis.enumList, nodup := PauliBasis.enumList_nodup }, complete := instFintypePauliBasis._proof_1 }

def instInhabitedPauliBasis.default : PauliBasis

Equations

• instInhabitedPauliBasis.default = PauliBasis.I

instance instInhabitedPauliBasis : Inhabited PauliBasis

Equations

• instInhabitedPauliBasis = { default := instInhabitedPauliBasis.default }

def sigmaI : Matrix (Fin 2) (Fin 2) ℂ

The 2×2 identity matrix over ℂ (Pauli I).

Equations

• sigmaI = !![1, 0; 0, 1]

def sigmaX : Matrix (Fin 2) (Fin 2) ℂ

The bit-flip Pauli matrix X = [[0,1],[1,0]] over ℂ.

Equations

• sigmaX = !![0, 1; 1, 0]

def sigmaY : Matrix (Fin 2) (Fin 2) ℂ

The bit-phase-flip Pauli matrix Y = [[0,−i],[i,0]] over ℂ.

Equations

• sigmaY = !![0, -Complex.I; Complex.I, 0]

def sigmaZ : Matrix (Fin 2) (Fin 2) ℂ

The phase-flip Pauli matrix Z = [[1,0],[0,−1]] over ℂ.

Equations

• sigmaZ = !![1, 0; 0, -1]

def PauliBasis.toMatrix : PauliBasis → Matrix (Fin 2) (Fin 2) ℂ

Maps each Pauli basis element to its corresponding 2×2 matrix.

Equations

• PauliBasis.I.toMatrix = sigmaI
• PauliBasis.X.toMatrix = sigmaX
• PauliBasis.Y.toMatrix = sigmaY
• PauliBasis.Z.toMatrix = sigmaZ

def PauliString (n : ℕ) : Type

An n-qubit Pauli string: a function assigning a Pauli basis element to each of the n qubits.

Equations

• PauliString n = (Fin n → PauliBasis)

instance instFintypePauliString (n : ℕ) : Fintype (PauliString n)

Equations

• instFintypePauliString n = inferInstanceAs (Fintype (Fin n → PauliBasis))

def support {n : ℕ} (p : PauliString n) : Finset (Fin n)

The support of a Pauli string: the set of qubit indices where the operator is not identity.

Equations

• support p = {i : Fin n | p i ≠ PauliBasis.I}

def weight {n : ℕ} (p : PauliString n) : ℕ

The weight of a Pauli string: the number of non-identity tensor factors.

Equations

• weight p = (support p).card

def pauliMatrix {n : ℕ} (p : PauliString n) : Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ

The 2^n × 2^n matrix for an n-qubit Pauli string, given as a tensor product of single-qubit Pauli matrices.

Equations

• pauliMatrix p i j = ∏ k : Fin n, (p k).toMatrix (i k) (j k)

def PauliErrorsLe (n t : ℕ) : Finset (PauliString n)

The finset of all n-qubit Pauli strings of weight at most t.

Equations

• PauliErrorsLe n t = {p : PauliString n | weight p ≤ t}

inductive PauliNZ : Type

A 3-element type for non-identity single-qubit Pauli operators, used in counting arguments.

• X : PauliNZ
• Y : PauliNZ
• Z : PauliNZ

instance instDecidableEqPauliNZ : DecidableEq PauliNZ

Equations

• instDecidableEqPauliNZ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instFintypePauliNZ : Fintype PauliNZ

Equations

• instFintypePauliNZ = { elems := { val := ↑PauliNZ.enumList, nodup := PauliNZ.enumList_nodup }, complete := instFintypePauliNZ._proof_1 }

instance instInhabitedPauliNZ : Inhabited PauliNZ

Equations

• instInhabitedPauliNZ = { default := instInhabitedPauliNZ.default }

def instInhabitedPauliNZ.default : PauliNZ

Equations

• instInhabitedPauliNZ.default = PauliNZ.X

def PauliNZ.toBasis : PauliNZ → PauliBasis

Embeds a non-identity Pauli into the full Pauli basis.

Equations

• PauliNZ.X.toBasis = PauliBasis.X
• PauliNZ.Y.toBasis = PauliBasis.Y
• PauliNZ.Z.toBasis = PauliBasis.Z

theorem PauliNZ.toBasis_ne_I (a : PauliNZ) : a.toBasis ≠ PauliBasis.I

def mkWithSupport {n : ℕ} (S : Finset (Fin n)) (f : ↥S → PauliNZ) : PauliString n

Constructs a Pauli string with support exactly S and non-identity assignments given by f.

Equations

• mkWithSupport S f i = if h : i ∈ S then (f ⟨i, h⟩).toBasis else PauliBasis.I

theorem support_mkWithSupport {n : ℕ} (S : Finset (Fin n)) (f : ↥S → PauliNZ) : support (mkWithSupport S f) = S

def pauliStringsExactSupport {n : ℕ} (S : Finset (Fin n)) : Finset (PauliString n)

The finset of Pauli strings with support exactly equal to S.

Equations

• pauliStringsExactSupport S = {p : PauliString n | support p = S}

theorem card_pauliStringsExactSupport {n : ℕ} (S : Finset (Fin n)) : (pauliStringsExactSupport S).card = 3 ^ S.card

theorem card_pauliErrorsLe (n t : ℕ) : (PauliErrorsLe n t).card = ∑ j ∈ Finset.range (t + 1), n.choose j * 3 ^ j

Clean Quantum Hamming counting identity.

@[reducible, inline]

abbrev Hn (n : ℕ) : Type

The n-qubit Hilbert space ℂ^(2^n), realized as a Euclidean space indexed by Fin n → Fin 2.

Equations

• Hn n = EuclideanSpace ℂ (Fin n → Fin 2)

def Code (n : ℕ) : Type

An n-qubit quantum code: a subspace of the Hilbert space Hn n.

Equations

• Code n = Submodule ℂ (Hn n)

noncomputable def pauliOp {n : ℕ} (p : PauliString n) : Hn n →ₗ[ℂ] Hn n

The linear operator on Hn n given by acting with the Pauli string p.

Equations

• pauliOp p = Matrix.toLin' (pauliMatrix p)

noncomputable def pauliOpAdjoint {n : ℕ} (p : PauliString n) : Hn n →ₗ[ℂ] Hn n

The adjoint (Hermitian conjugate) of the Pauli operator for p.

Equations

• pauliOpAdjoint p = Matrix.toLin' (pauliMatrix p).conjTranspose

instance instFiniteDimensionalComplexSubtypeHnMemSubmodule (n : ℕ) (C : Submodule ℂ (Hn n)) : FiniteDimensional ℂ ↥C

noncomputable def codeProj {n : ℕ} (C : Submodule ℂ (Hn n)) : Hn n →ₗ[ℂ] Hn n

The orthogonal projection from Hn n onto the code subspace C, viewed as an endomorphism.

Equations

• codeProj C = ↑(C.subtypeL.comp C.orthogonalProjection)

@[simp]

theorem codeProj_apply {n : ℕ} (C : Submodule ℂ (Hn n)) (x : Hn n) : (codeProj C) x = ↑(C.orthogonalProjection x)

theorem codeProj_mem {n : ℕ} (C : Submodule ℂ (Hn n)) (x : Hn n) : (codeProj C) x ∈ C

theorem codeProj_eq_self_of_mem {n : ℕ} {C : Submodule ℂ (Hn n)} {x : Hn n} (hx : x ∈ C) : (codeProj C) x = x

theorem codeProj_idempotent {n : ℕ} (C : Submodule ℂ (Hn n)) (x : Hn n) : (codeProj C) ((codeProj C) x) = (codeProj C) x

def KnillLaflamme (n : ℕ) (C : Submodule ℂ (Hn n)) (t : ℕ) : Prop

The Knill–Laflamme quantum error correction condition: for all Pauli errors E, F of weight ≤ t, the code projection satisfies Π_C ∘ E† ∘ F ∘ Π_C = α_{E,F} • Π_C for some scalar.

Equations

• KnillLaflamme n C t = ∀ (E F : PauliString n), weight E ≤ t → weight F ≤ t → ∃ (α : ℂ), codeProj C ∘ₗ pauliOpAdjoint E ∘ₗ pauliOp F ∘ₗ codeProj C = α • codeProj C

def IsNondegenerate (n : ℕ) (C : Submodule ℂ (Hn n)) (t : ℕ) : Prop

A code is non-degenerate if it satisfies the Knill–Laflamme condition with all off-diagonal terms zero: for distinct errors E ≠ F of weight ≤ t, Π_C ∘ E† ∘ F ∘ Π_C = 0.

Equations

• IsNondegenerate n C t = (KnillLaflamme n C t ∧ ∀ (E F : PauliString n), weight E ≤ t → weight F ≤ t → E ≠ F → codeProj C ∘ₗ pauliOpAdjoint E ∘ₗ pauliOp F ∘ₗ codeProj C = 0)

noncomputable def ErrorSphere (n t : ℕ) (C : Submodule ℂ (Hn n)) : Submodule ℂ (Hn n)

The error sphere: the span of all images E(C) over Pauli strings E of weight ≤ t. This is the subspace that must fit inside Hn n to derive the Hamming bound.

Equations

• ErrorSphere n t C = (PauliErrorsLe n t).sup fun (E : PauliString n) => Submodule.map (pauliOp E) C

theorem error_subspaces_orthogonal {n t : ℕ} {C : Submodule ℂ (Hn n)} (h_nondeg : IsNondegenerate n C t) (E F : PauliString n) (hE : weight E ≤ t) (hF : weight F ≤ t) (h_neq : E ≠ F) : Submodule.map (pauliOp E) C ⟂ Submodule.map (pauliOp F) C

theorem error_sphere_dimension {n t : ℕ} {C : Submodule ℂ (Hn n)} (h_nondeg : IsNondegenerate n C t) : Module.finrank ℂ ↥(ErrorSphere n t C) = (PauliErrorsLe n t).card * Module.finrank ℂ ↥C

theorem finrank_Hn (n : ℕ) : Module.finrank ℂ (Hn n) = 2 ^ n

The n-qubit Hilbert space Hn n has complex dimension 2^n.

theorem quantum_hamming_bound_raw (n k t : ℕ) (C : Submodule ℂ (Hn n)) (h_dim : Module.finrank ℂ ↥C = 2 ^ k) (h_nondeg : IsNondegenerate n C t) : (∑ j ∈ Finset.range (t + 1), n.choose j * 3 ^ j) * 2 ^ k ≤ 2 ^ n

Quantum Hamming bound (raw form): for a non-degenerate [[n, k]] quantum code correcting t errors, the total dimension of the error sphere does not exceed the ambient space.

theorem quantum_hamming_bound (n k t : ℕ) (C : Submodule ℂ (Hn n)) (h_dim : Module.finrank ℂ ↥C = 2 ^ k) (h_nondeg : IsNondegenerate n C t) (hkn : k ≤ n) : ∑ j ∈ Finset.range (t + 1), n.choose j * 3 ^ j ≤ 2 ^ (n - k)

Quantum Hamming bound: a non-degenerate [[n, k]] quantum code correcting t errors satisfies ∑ j ∈ Finset.range (t + 1), C(n, j) * 3^j ≤ 2^(n - k).