14 Quantum Singleton Bound
14.1 Overview
This chapter proves the quantum Singleton bound: for a stabilizer code with logical dimension \(k\) and distance \(d\) on \(n\) qudits over a prime field \(\mathbb {F}_p\),
The proof uses the symplectic vector space \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) with the standard symplectic form, and the key idea of erasure correctability.
14.2 Symplectic vector space
For \(u = (x,z), v = (x',z') \in V = \mathbb {F}_p^n \times \mathbb {F}_p^n\),
\(\omega \) is bilinear: additive and scalar-homogeneous in each argument.
\(\omega (u,v) = -\omega (v,u)\).
If \(\omega (u,v) = 0\) for all \(v\), then \(u = 0\).
\(\omega \) packaged as a LinearMap.BilinForm.
14.3 Support, weight, and isotropic subspaces
The support \(\mathrm{supp}(v) \subseteq \mathrm{Fin}\, n\) consists of coordinates where either component of \(v\) is nonzero; the weight is \(\mathrm{wt}(v) = |\mathrm{supp}(v)|\).
\(\mathrm{wt}(v) \le n\) for all \(v \in V\).
For \(C \subseteq \mathrm{Fin}\, n\), the support submodule \(V_C = \{ v \in V \mid \mathrm{supp}(v) \subseteq C\} \).
\(\dim _{\mathbb {F}_p}(V_C) = 2|C|\).
For a submodule \(S \le V\), \(S^{\perp _\omega } = \{ v \in V \mid \forall s \in S,\; \omega (v,s) = 0\} \).
\(\dim (S^{\perp _\omega }) = 2n - \dim (S)\).
\(S\) is isotropic if \(S \le S^{\perp _\omega }\), i.e. \(\omega (u,v) = 0\) for all \(u,v \in S\).
14.4 Code parameters and erasure correctability
\(d(S) = \min \{ \mathrm{wt}(v) \mid v \in S^{\perp _\omega } \setminus S,\; \mathrm{wt}(v) \neq 0\} \) (or \(0\) if no such \(v\) exists).
\(d(S) \le n\).
An erasure set \(E \subseteq \mathrm{Fin}\, n\) is correctable for \(S\) if every \(v \in V_E \cap S^{\perp _\omega }\) is already in \(S\).
If \(|E| \lt d(S)\), then \(E\) is correctable.
Any \(v \in S^{\perp _\omega } \cap V_E\) outside \(S\) witnesses \(d(S) \le \mathrm{wt}(v)\), while \(v \in V_E\) forces \(\mathrm{supp}(v) \subseteq E\), so \(\mathrm{wt}(v) \le |E| \lt d(S)\) — a contradiction. Used in the Singleton bound to turn the distance hypothesis into two disjoint correctable erasure sets of size \(d(S)-1\). Not proved in Knill–Laflamme (Phys. Rev. A 55, 900); full note: references/informalized/QuantumSingleton.dist_implies_correctable.md.
\(k(S) = n - \dim (S)\).
14.5 Key lemma: two disjoint correctable sets
Let \(S\) be isotropic. If \(A,B \subseteq \mathrm{Fin}\, n\) are disjoint and both correctable, then
By the cleaning identity, \(g(S, \mathrm{univ} \setminus A) = 2(n - \dim S)\) (g_complement_correctable), while \(g(S, B \cup (\mathrm{univ}\setminus (A \cup B))) \le 2\, |\mathrm{univ}\setminus (A \cup B)|\) (g_le_two_card_C); the two argument sets coincide, giving the bound. This is the engine behind Theorem V.1 of Knill–Laflamme (Phys. Rev. A 55, 900), which states the corresponding bound \(n \ge 4e + k\) with proof deferred; the Lean route is a symplectic dimension count with no density matrices.
14.6 Quantum Singleton bound
For any isotropic submodule \(S \le V\),
Choose disjoint erasure sets \(A, B\) of size \(d(S)-1\) (exists_disjoint_finsets_card); both are correctable by dist_implies_correctable, so the two-disjoint-correctable-sets lemma yields \(k(S) \le n - 2(d(S)-1)\). The statement is Theorem V.1 of Knill–Laflamme (Phys. Rev. A 55, 900): an \((n,k)\) \(e\)-error-correcting code satisfies \(n \ge 4e + k\), which with \(d = 2e+1\) is exactly this bound; the paper defers the proof, and the Lean supplies it via the erasure/cleaning argument.
14.7 Additional declarations
The prime field \(\mathrm{GF}(p)\), realized as \(\mathbb {Z}/p\mathbb {Z}\) via ZMod.
The ambient space \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) of pairs of coordinate vectors.
The bundled bilinear form \(\mathrm{symB}\) agrees with \(\omega \): \(\mathrm{symB}(x,y) = \omega (x,y)\) for all \(x,y \in V\).
For \(C \subseteq \mathrm{Fin}\, n\), the linear map \(V_C \to (C \to \mathbb {F}_p) \times (C \to \mathbb {F}_p)\) sending a vector supported on \(C\) to its two component functions restricted to \(C\).
The linear map \((C \to \mathbb {F}_p) \times (C \to \mathbb {F}_p) \to V_C\) that extends a pair of functions on \(C\) to a vector of \(V\) by setting all coordinates outside \(C\) to zero.
For every \(x\), \(\mathrm{restrictToC}_C(\mathrm{extendFromC}_C(x)) = x\).
For every \(x \in V_C\), \(\mathrm{extendFromC}_C(\mathrm{restrictToC}_C(x)) = x\).
The linear equivalence \(V_C \simeq (C \to \mathbb {F}_p) \times (C \to \mathbb {F}_p)\) built from \(\mathrm{restrictToC}\) and \(\mathrm{extendFromC}\) as mutually inverse maps.
The linear map \(r_E : V \to V_E\) that zeroes out the coordinates of a vector outside \(E\), keeping those in \(E\) unchanged.
For a submodule \(S \le V\) and \(M \subseteq \mathrm{Fin}\, n\), the submodule \(S_M = S \cap V_M\).
The submodule \(S^{\perp }_M = S^{\perp _\omega } \cap V_M\).
\(g(S,M) = \dim _{\mathbb {F}_p}(S^{\perp }_M) - \dim _{\mathbb {F}_p}(S_M)\).
\(\ker (r_E) = V_{\mathrm{univ} \setminus E}\), the subspace supported on the complement of \(E\).
\(E^c = \mathrm{Fin}\, n \setminus E\), the complement finset of \(E\).
\(E^c = \mathrm{univ} \setminus E\).
\(\dim _{\mathbb {F}_p}(r_E(S)) = \dim _{\mathbb {F}_p}(S) - \dim _{\mathbb {F}_p}(S \cap V_{E^c})\).
If \(v \in V_M\), then \(\omega (v,s) = \omega (v, r_M(s))\) for all \(s \in V\).
The composition \(r_E^V : V \to V\) of \(r_E\) with the inclusion \(V_E \hookrightarrow V\).
If \(v \in V_M\), then \(\omega (r_M^V(s), v) = \omega (s, v)\) for all \(s \in V\).
If \(v \in V_M\) and \(\omega (v,w) = 0\) for all \(w \in V_M\), then \(v = 0\).
If \(v \in V_M\), then \(\omega (r_M^V(s), v) = \omega (s, v)\) for all \(s \in V\).
\(S^{\perp _\omega } \cap V_M = (r_M^V(S))^{\perp _\omega } \cap V_M\).
The symplectic bilinear form \(\mathrm{symB}\) restricted to the subspace \(V_M\).
An abbreviation for \(\mathrm{symB\_ sub}\), the symplectic form viewed as a bilinear form on \(V_M\).
For \(x,y \in V_M\), \(\mathrm{sym\_ form\_ sub}_M(x,y) = \omega (x,y)\) computed on the underlying vectors.
The restricted symplectic form on \(V_M\) is non-degenerate.
\(S^{\perp _\omega } \cap V_M\) is the image under \(V_M \hookrightarrow V\) of the orthogonal complement of \(r_M(S)\) with respect to the restricted form.
The restricted symplectic form on \(V_M\) is reflexive.
\(\dim _{\mathbb {F}_p}(S^{\perp _\omega } \cap V_M) = 2|M| - \dim _{\mathbb {F}_p}(r_M(S))\).
For isotropic \(S\),
\((M^c)^c = M\).
\(\dim _{\mathbb {F}_p}(S_M) + \dim _{\mathbb {F}_p}(S_{M^c}) \le \dim _{\mathbb {F}_p}(S)\).
For isotropic \(S\),
For isotropic \(S\),
For isotropic \(S\), \(\dim (S) + \dim (S_M) \le 2|M| + \dim (S_{M^c})\).
For isotropic \(S\),
\(|M| + |M^c| = n\).
If \(M\) is correctable for \(S\), then \(g(S,M) = 0\).
If \(S\) is isotropic and \(M\) is correctable, then \(g(S,M^c) = 2n - 2\dim _{\mathbb {F}_p}(S)\).
If \(B\) and \(C\) are disjoint and \(B\) is correctable for \(S\), then \(g(S, B \cup C) \le 2|C|\).
Rank–nullity for the restriction map \(r_C : S^{\perp _\omega } \cap V_{B \cup C} \to V_C\): its kernel consists of vectors supported on \(B\), which correctability of \(B\) absorbs into \(S\), and its range has dimension at most \(\dim V_C = 2|C|\). This is the counting half of the cleaning argument, consumed by the two-disjoint-correctable-sets lemma. Not present in Knill–Laflamme (Phys. Rev. A 55, 900); full note: references/informalized/QuantumSingleton.g_le_two_card_C.md.
\(V_{\mathrm{univ}} = \top \), the entire space \(V\).
\(\dim _{\mathbb {F}_p}(V) = 2n\).
The bundled symplectic form \(\mathrm{symB}\) is non-degenerate.
The bundled symplectic form \(\mathrm{symB}\) is reflexive.
If \(S\) is isotropic, then \(\dim _{\mathbb {F}_p}(S) \le n\).
If \(S\) is isotropic and \(k(S) = 0\), then \(d(S) = 0\).
Whenever \(2t \le n\), there exist disjoint finsets \(A, B \subseteq \mathrm{Fin}\, n\) with \(|A| = |B| = t\).