Quantum Singleton Bound

This file proves the quantum Singleton bound for stabilizer codes over a prime field GF(p).

A stabilizer code is modeled as an isotropic subspace S of the symplectic vector space V = GF(p)^n × GF(p)^n with respect to the standard symplectic form.

Main definitions

• sym_form: The standard symplectic form on V = GF(p)^n × GF(p)^n.
• IsIsotropic S: Predicate asserting S ≤ S^⊥ (S is self-orthogonal).
• code_dist S: The minimum weight of a vector in S^⊥ \ S (the distance of the code).
• code_k S: The number of logical qudits, defined as n - dim(S).

Main results

• quantum_singleton_bound: For an isotropic stabilizer code with distance d and k logical qudits, k + 2 * (d - 1) ≤ n.

References

• Knill, Laflamme, Viola (2000): Theory of quantum error correction for general noise.
• Ashikhmin, Knill (2001): Nonbinary quantum stabilizer codes.

@[reducible, inline]

abbrev F (p : ℕ) [Fact (Nat.Prime p)] : Type

The prime field GF(p), realized as ZMod p.

Equations

• F p = ZMod p

@[reducible, inline]

abbrev V (n p : ℕ) [Fact (Nat.Prime p)] : Type

The symplectic vector space V := F^n × F^n

Equations

• V n p = ((Fin n → F p) × (Fin n → F p))

def sym_form {n p : ℕ} [Fact (Nat.Prime p)] (u v : V n p) : F p

Standard symplectic form on V: sym_form (u, v) = ∑ i, u₁ᵢ v₂ᵢ - u₂ᵢ v₁ᵢ.

Equations

• sym_form u v = ∑ i : Fin n, (u.1 i * v.2 i - u.2 i * v.1 i)

theorem sym_form_add_left {n p : ℕ} [Fact (Nat.Prime p)] (x y z : V n p) : sym_form (x + y) z = sym_form x z + sym_form y z

theorem sym_form_add_right {n p : ℕ} [Fact (Nat.Prime p)] (x y z : V n p) : sym_form x (y + z) = sym_form x y + sym_form x z

theorem sym_form_smul_left {n p : ℕ} [Fact (Nat.Prime p)] (c : F p) (x y : V n p) : sym_form (c • x) y = c * sym_form x y

theorem sym_form_smul_right {n p : ℕ} [Fact (Nat.Prime p)] (c : F p) (x y : V n p) : sym_form x (c • y) = c * sym_form x y

theorem sym_form_swap {n p : ℕ} [Fact (Nat.Prime p)] (u v : V n p) : sym_form u v = -sym_form v u

The symplectic form is antisymmetric: sym_form u v = -sym_form v u.

noncomputable def symB {n p : ℕ} [Fact (Nat.Prime p)] : LinearMap.BilinForm (F p) (V n p)

The standard symplectic form sym_form packaged as a LinearMap.BilinForm.

Equations

• symB = LinearMap.mk₂ (F p) (fun (x y : V n p) => sym_form x y) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem symB_apply {n p : ℕ} [Fact (Nat.Prime p)] (x y : V n p) : (symB x) y = sym_form x y

theorem sym_form_nondegenerate {n p : ℕ} [Fact (Nat.Prime p)] (u : V n p) (h : ∀ (v : V n p), sym_form u v = 0) : u = 0

The symplectic form is non-degenerate: if sym_form u v = 0 for all v, then u = 0.

def supp {n p : ℕ} [Fact (Nat.Prime p)] (v : V n p) : Finset (Fin n)

Support of a vector v in V

Equations

• supp v = {i : Fin n | v.1 i ≠ 0 ∨ v.2 i ≠ 0}.toFinset

def wt {n p : ℕ} [Fact (Nat.Prime p)] (v : V n p) : ℕ

Weight of a vector v in V

Equations

• wt v = (supp v).card

def V_sub {n p : ℕ} [Fact (Nat.Prime p)] (C : Finset (Fin n)) : Submodule (F p) (V n p)

Support subspace V_C

Equations

• V_sub C = { carrier := {v : V n p | ∀ i ∉ C, v.1 i = 0 ∧ v.2 i = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable def restrictToC {n p : ℕ} [Fact (Nat.Prime p)] (C : Finset (Fin n)) : ↥(V_sub C) →ₗ[F p] (↥C → F p) × (↥C → F p)

Equations

• restrictToC C = { toFun := fun (x : ↥(V_sub C)) => match x with | ⟨v, property⟩ => (fun (c : ↥C) => v.1 ↑c, fun (c : ↥C) => v.2 ↑c), map_add' := ⋯, map_smul' := ⋯ }

noncomputable def extendFromC {n p : ℕ} [Fact (Nat.Prime p)] (C : Finset (Fin n)) : (↥C → F p) × (↥C → F p) →ₗ[F p] ↥(V_sub C)

Equations

• One or more equations did not get rendered due to their size.

theorem restrictToC_extendFromC {n p : ℕ} [Fact (Nat.Prime p)] (C : Finset (Fin n)) (x : (↥C → F p) × (↥C → F p)) : (restrictToC C) ((extendFromC C) x) = x

theorem extendFromC_restrictToC {n p : ℕ} [Fact (Nat.Prime p)] (C : Finset (Fin n)) (x : ↥(V_sub C)) : (extendFromC C) ((restrictToC C) x) = x

noncomputable def V_sub_iso {n p : ℕ} [Fact (Nat.Prime p)] (C : Finset (Fin n)) : ↥(V_sub C) ≃ₗ[F p] (↥C → F p) × (↥C → F p)

Equations

• V_sub_iso C = { toFun := ⇑(restrictToC C), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(extendFromC C), left_inv := ⋯, right_inv := ⋯ }

theorem dim_V_sub {n p : ℕ} [Fact (Nat.Prime p)] (C : Finset (Fin n)) : Module.finrank (F p) ↥(V_sub C) = 2 * C.card

def r_E {n p : ℕ} [Fact (Nat.Prime p)] (E : Finset (Fin n)) : V n p →ₗ[F p] ↥(V_sub E)

Restriction map r_E : V -> V_E

Equations

• r_E E = { toFun := fun (v : V n p) => ⟨(fun (i : Fin n) => if i ∈ E then v.1 i else 0, fun (i : Fin n) => if i ∈ E then v.2 i else 0), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[reducible, inline]

abbrev sym_orth {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) : Submodule (F p) (V n p)

Orthogonal complement with respect to the symplectic bilinear form.

Equations

• sym_orth S = symB.orthogonal S

def IsIsotropic {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) : Prop

Isotropic subspace

Equations

• IsIsotropic S = (S ≤ sym_orth S)

noncomputable def code_dist {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) : ℕ

The distance of the stabilizer code defined by S

Equations

• code_dist S = sInf {d : ℕ | ∃ v ∈ sym_orth S, v ∉ S ∧ wt v = d}

def correctable {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (E : Finset (Fin n)) : Prop

Correctable erasure (commutant form)

Equations

• correctable S E = (sym_orth S ⊓ V_sub E ≤ S)

theorem dist_implies_correctable {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (E : Finset (Fin n)) (h : E.card < code_dist S) : correctable S E

An erasure set E is correctable whenever its size is strictly less than the code distance.

def S_M {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (M : Finset (Fin n)) : Submodule (F p) (V n p)

Intersection of S and V_M

Equations

• S_M S M = S ⊓ V_sub M

def S_perp_M {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (M : Finset (Fin n)) : Submodule (F p) (V n p)

Intersection of S^\perp and V_M

Equations

• S_perp_M S M = sym_orth S ⊓ V_sub M

noncomputable def g {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (M : Finset (Fin n)) : ℕ

Supportable logical operators count g(M)

Equations

• g S M = Module.finrank (F p) ↥(S_perp_M S M) - Module.finrank (F p) ↥(S_M S M)

theorem ker_r_E {n p : ℕ} [Fact (Nat.Prime p)] (E : Finset (Fin n)) : LinearMap.ker (r_E E) = V_sub (Finset.univ \ E)

Kernel of r_E is V_{E^c}

def E_c {n : ℕ} (E : Finset (Fin n)) : Finset (Fin n)

Complement of E

Equations

• E_c E = Eᶜ

theorem E_c_eq {n : ℕ} (E : Finset (Fin n)) : E_c E = Finset.univ \ E

theorem dim_map_r_E {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (E : Finset (Fin n)) : Module.finrank (F p) ↥(Submodule.map (r_E E) S) = Module.finrank (F p) ↥S - Module.finrank (F p) ↥(S ⊓ V_sub (E_c E))

Rank-nullity for restriction of S to E

theorem sym_form_r_E {n p : ℕ} [Fact (Nat.Prime p)] (M : Finset (Fin n)) (v : V n p) (hv : v ∈ V_sub M) (s : V n p) : sym_form v s = sym_form v ↑((r_E M) s)

Symplectic form respects restriction

def r_E_V {n p : ℕ} [Fact (Nat.Prime p)] (E : Finset (Fin n)) : V n p →ₗ[F p] V n p

Equations

• r_E_V E = (V_sub E).subtype ∘ₗ r_E E

theorem sym_form_r_E_left {n p : ℕ} [Fact (Nat.Prime p)] (M : Finset (Fin n)) (s v : V n p) (hv : v ∈ V_sub M) : sym_form ((r_E_V M) s) v = sym_form s v

theorem sym_form_nondegenerate_on_V_sub {n p : ℕ} [Fact (Nat.Prime p)] (M : Finset (Fin n)) (v : V n p) (hv : v ∈ V_sub M) (h : ∀ w ∈ V_sub M, sym_form v w = 0) : v = 0

Non-degeneracy on V_sub M

theorem sym_form_left_restrict {n p : ℕ} [Fact (Nat.Prime p)] (M : Finset (Fin n)) (s v : V n p) (hv : v ∈ V_sub M) : sym_form ((r_E_V M) s) v = sym_form s v

Restriction map as an endomorphism of V

theorem orth_inter_eq_orth_map {n p : ℕ} [Fact (Nat.Prime p)] (M : Finset (Fin n)) (S : Submodule (F p) (V n p)) : sym_orth S ⊓ V_sub M = sym_orth (Submodule.map (r_E_V M) S) ⊓ V_sub M

Orthogonal intersection lemma

noncomputable def symB_sub {n p : ℕ} [Fact (Nat.Prime p)] (M : Finset (Fin n)) : LinearMap.BilinForm (F p) ↥(V_sub M)

Symplectic bilinear form restricted to V_sub M.

Equations

• symB_sub M = symB.comp (V_sub M).subtype (V_sub M).subtype

@[reducible, inline]

abbrev sym_form_sub {n p : ℕ} [Fact (Nat.Prime p)] (M : Finset (Fin n)) : LinearMap.BilinForm (F p) ↥(V_sub M)

Equations

• sym_form_sub M = symB_sub M

@[simp]

theorem sym_form_sub_apply {n p : ℕ} [Fact (Nat.Prime p)] (M : Finset (Fin n)) (x y : ↥(V_sub M)) : ((sym_form_sub M) x) y = sym_form ↑x ↑y

theorem sym_form_sub_nondegenerate {n p : ℕ} [Fact (Nat.Prime p)] (M : Finset (Fin n)) : (sym_form_sub M).Nondegenerate

Non-degeneracy of restricted form

theorem orth_inter_eq_orth_sub_image {n p : ℕ} [Fact (Nat.Prime p)] (M : Finset (Fin n)) (S : Submodule (F p) (V n p)) : sym_orth S ⊓ V_sub M = Submodule.map (V_sub M).subtype ((sym_form_sub M).orthogonal (Submodule.map (r_E M) S))

The intersection S^\perp ∩ V_M corresponds to the orthogonal complement of r_M(S) in V_M

theorem sym_form_sub_isRefl {n p : ℕ} [Fact (Nat.Prime p)] (M : Finset (Fin n)) : (sym_form_sub M).IsRefl

The restricted symplectic form is reflexive

theorem dim_orth_inter {n p : ℕ} [Fact (Nat.Prime p)] (M : Finset (Fin n)) (S : Submodule (F p) (V n p)) : Module.finrank (F p) ↥(sym_orth S ⊓ V_sub M) = 2 * M.card - Module.finrank (F p) ↥(Submodule.map (r_E M) S)

Dimension of orthogonal intersection

theorem g_expansion {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (hS : IsIsotropic S) (M : Finset (Fin n)) : g S M = 2 * M.card + Module.finrank (F p) ↥(S_M S (E_c M)) - Module.finrank (F p) ↥S - Module.finrank (F p) ↥(S_M S M)

theorem E_c_E_c {n : ℕ} (M : Finset (Fin n)) : E_c (E_c M) = M

theorem dim_S_M_add_dim_S_M_c_le_dim_S {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (M : Finset (Fin n)) : Module.finrank (F p) ↥(S_M S M) + Module.finrank (F p) ↥(S_M S (E_c M)) ≤ Module.finrank (F p) ↥S

theorem g_formula {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (hS : IsIsotropic S) (M : Finset (Fin n)) : g S M = 2 * M.card + Module.finrank (F p) ↥(S_M S (E_c M)) - (Module.finrank (F p) ↥S + Module.finrank (F p) ↥(S_M S M))

theorem g_add_dims {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (hS : IsIsotropic S) (M : Finset (Fin n)) : g S M + Module.finrank (F p) ↥(S_M S M) + Module.finrank (F p) ↥S = 2 * M.card + Module.finrank (F p) ↥(S_M S (E_c M))

theorem dim_ineq_aux {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (hS : IsIsotropic S) (M : Finset (Fin n)) : Module.finrank (F p) ↥S + Module.finrank (F p) ↥(S_M S M) ≤ 2 * M.card + Module.finrank (F p) ↥(S_M S (E_c M))

theorem cleaning_dimension_identity {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (hS : IsIsotropic S) (M : Finset (Fin n)) : g S M + g S (E_c M) = 2 * n - 2 * Module.finrank (F p) ↥S

Cleaning dimension identity

theorem card_add_compl {n : ℕ} (M : Finset (Fin n)) : M.card + (E_c M).card = n

theorem correctable_implies_g_zero {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (M : Finset (Fin n)) (h : correctable S M) : g S M = 0

theorem g_complement_correctable {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (hS : IsIsotropic S) (M : Finset (Fin n)) (h : correctable S M) : g S (E_c M) = 2 * n - 2 * Module.finrank (F p) ↥S

If M is correctable, g(M^c) = 2k

theorem g_le_two_card_C {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (B C : Finset (Fin n)) (h_disjoint : Disjoint B C) (hB : correctable S B) : g S (B ∪ C) ≤ 2 * C.card

def code_k {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) : ℕ

Number of logical qudits k

Equations

• code_k S = n - Module.finrank (F p) ↥S

theorem two_disjoint_correctable_sets_bound_logical_dimension {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (hS : IsIsotropic S) (A B : Finset (Fin n)) (h_disjoint : Disjoint A B) (hA : correctable S A) (hB : correctable S B) : code_k S ≤ (Finset.univ \ (A ∪ B)).card

Lemma 5: Two disjoint correctable sets bound logical dimension

@[simp]

theorem V_sub_univ_eq_top {n p : ℕ} [Fact (Nat.Prime p)] : V_sub Finset.univ = ⊤

theorem finrank_V {n p : ℕ} [Fact (Nat.Prime p)] : Module.finrank (F p) (V n p) = 2 * n

theorem symB_nondegenerate {n p : ℕ} [Fact (Nat.Prime p)] : symB.Nondegenerate

theorem symB_isRefl {n p : ℕ} [Fact (Nat.Prime p)] : symB.IsRefl

theorem finrank_sym_orth {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) : Module.finrank (F p) ↥(sym_orth S) = 2 * n - Module.finrank (F p) ↥S

theorem finrank_le_n_of_isotropic {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (hS : IsIsotropic S) : Module.finrank (F p) ↥S ≤ n

theorem wt_le_n {n p : ℕ} [Fact (Nat.Prime p)] (v : V n p) : wt v ≤ n

Any vector in V n p has weight at most n.

theorem code_dist_le_n {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) : code_dist S ≤ n

code_dist S ≤ n since all weights are bounded by n.

theorem code_dist_eq_zero_of_code_k_eq_zero {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (hS : IsIsotropic S) (hk : code_k S = 0) : code_dist S = 0

theorem exists_disjoint_finsets_card {n : ℕ} (t : ℕ) (h : 2 * t ≤ n) : ∃ (A : Finset (Fin n)) (B : Finset (Fin n)), Disjoint A B ∧ A.card = t ∧ B.card = t

Choose disjoint finsets A,B of size t inside Fin n, assuming 2t ≤ n.

theorem quantum_singleton_bound {n p : ℕ} [Fact (Nat.Prime p)] (S : Submodule (F p) (V n p)) (hS : IsIsotropic S) : code_k S + 2 * (code_dist S - 1) ≤ n

Quantum Singleton bound: code_k S + 2*(code_dist S - 1) ≤ n.