TCSLib

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\),

\[ k + 2(d-1) \; \le \; n. \]

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

Definition 14.1 Symplectic form
✓
#

For \(u = (x,z), v = (x',z') \in V = \mathbb {F}_p^n \times \mathbb {F}_p^n\),

\[ \omega (u,v) \; =\; \sum _{i=0}^{n-1}(x_i z'_i - z_i x'_i). \]
Lemma 14.2 Additivity of the symplectic form in the first argument
✓
#

Let \(p\) be prime and work over the space \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) equipped with the symplectic form \(\omega (u,v) = \sum _{i=0}^{n-1}(x_i z'_i - z_i x'_i)\), where \(u = (x,z)\) and \(v = (x',z')\). Then for all \(x, y, z \in V\),

\[ \omega (x + y, z) = \omega (x, z) + \omega (y, z). \]

Fix a prime \(p\) and a natural number \(n\), and let \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\), where \(\mathbb {F}_p = \mathbb {Z}/p\mathbb {Z}\). Equip \(V\) with the symplectic form \(\omega (u,v) = \sum _{i=0}^{n-1}(x_i z'_i - z_i x'_i)\) for \(u = (x,z)\) and \(v = (x',z')\). Then \(\omega \) is additive in its second argument: for all \(x, y, z \in V\),

\[ \omega (x,\, y + z) = \omega (x,y) + \omega (x,z). \]

Let \(p\) be prime and work over the prime field \(\mathbb {F}_p\), with \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) carrying the symplectic form \(\omega \) given by \(\omega (u,v) = \sum _{i=0}^{n-1}(x_i z'_i - z_i x'_i)\) for \(u=(x,z)\) and \(v=(x',z')\). Then for every scalar \(c \in \mathbb {F}_p\) and all \(x, y \in V\),

\[ \omega (c\, x,\, y) \; =\; c\, \omega (x, y), \]

where \(c\, x\) denotes the coordinatewise scalar multiplication of \(x\) by \(c\).

Let \(p\) be a prime, and equip \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) with the symplectic form \(\omega (u,v) = \sum _{i=0}^{n-1}(x_i z'_i - z_i x'_i)\), where \(u = (x,z)\) and \(v = (x',z')\). Then for every scalar \(c \in \mathbb {F}_p\) and all \(x, y \in V\),

\[ \omega (x, c\, y) \; =\; c\, \omega (x, y), \]

where \(c\, y\) denotes componentwise scalar multiplication.

Lemma 14.3 Antisymmetry of the symplectic form
✓
#

Fix a prime \(p\) and an integer \(n\), and equip \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) with the bilinear form \(\omega (u,v) = \sum _{i=0}^{n-1}(x_i z'_i - z_i x'_i)\), where \(u = (x,z)\) and \(v = (x',z')\). Then \(\omega \) is antisymmetric: for all \(u, v \in V\),

\[ \omega (u,v) = -\, \omega (v,u). \]
Lemma 14.4 Nondegeneracy of the symplectic form
✓
#

Let \(p\) be a prime and \(n \ge 0\), and let \(\omega \) be the symplectic form on \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\). If a vector \(u \in V\) satisfies \(\omega (u,v) = 0\) for every \(v \in V\), then \(u = 0\).

Definition 14.5 Bundled bilinear form
✓
#

\(\omega \) packaged as a LinearMap.BilinForm.

14.3 Support, weight, and isotropic subspaces

Definition 14.6 Support and weight
✓
#

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)|\).

Lemma 14.7 Weight bound
✓
#

Fix a prime \(p\) and a natural number \(n\), and let \(v \in \mathbb {F}_p^n \times \mathbb {F}_p^n\). Then the weight \(\mathrm{wt}(v)\) satisfies \(\mathrm{wt}(v) \le n\).

Definition 14.8 Support submodule
✓
#

For \(C \subseteq \mathrm{Fin}\, n\), the support submodule \(V_C = \{ v \in V \mid \mathrm{supp}(v) \subseteq C\} \).

Lemma 14.9 Dimension of the support submodule
✓
#

Fix a prime \(p\) and an integer \(n\), and let \(V = \mathbb {F}_p^{\, n} \times \mathbb {F}_p^{\, n}\) be the space of pairs of coordinate vectors over the prime field \(\mathbb {F}_p\). For a subset \(C \subseteq \{ 1, \dots , n\} \), let \(V_C \subseteq V\) be the support submodule consisting of those pairs \((u, w)\) for which \(u_i = 0\) and \(w_i = 0\) at every index \(i \notin C\). Then \(V_C\) has dimension \(\dim _{\mathbb {F}_p}(V_C) = 2\lvert C\rvert \) over \(\mathbb {F}_p\).

Definition 14.10 Symplectic orthogonal complement
✓
#

For a submodule \(S \le V\), \(S^{\perp _\omega } = \{ v \in V \mid \forall s \in S,\; \omega (v,s) = 0\} \).

Lemma 14.11 Dimension of the symplectic orthogonal complement
✓
#

Let \(p\) be a prime and equip the \(2n\)-dimensional space \(V = \mathbb {F}_p^{\, n} \times \mathbb {F}_p^{\, n}\) over the prime field \(\mathbb {F}_p\) with the symplectic form \(\omega \big((x,z),(x',z')\big) = \sum _{i=1}^{n}(x_i z'_i - z_i x'_i)\). Then for every subspace \(S \le V\), its symplectic orthogonal complement \(S^{\perp _\omega } = \{ v \in V \mid \omega (v,s) = 0 \text{ for all } s \in S\} \) has dimension

\[ \dim _{\mathbb {F}_p} S^{\perp _\omega } = 2n - \dim _{\mathbb {F}_p} S. \]
Definition 14.12 Isotropic submodule
✓
#

\(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

Definition 14.13 Quantum code distance
✓
#

\(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).

Lemma 14.14 Code distance is at most the block length
✓
#

Fix a prime \(p\) and a natural number \(n\), and let \(V = \mathbb {F}_p^{\, n} \times \mathbb {F}_p^{\, n}\) carry the symplectic form \(\omega \bigl((x,z),(x',z')\bigr) = \sum _{i} (x_i z'_i - z_i x'_i)\). For every \(\mathbb {F}_p\)-subspace \(S \le V\), the associated code distance \(d(S)\) — the least weight \(\mathrm{wt}(v) = |\mathrm{supp}(v)|\) attained by a vector \(v\) lying in the symplectic orthogonal complement \(S^{\perp _\omega }\) but not in \(S\) — satisfies \(d(S) \le n\).

Definition 14.15 Erasure correctability
✓
#

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\).

Lemma 14.16 Erasure correction below the code distance
✓

Let \(p\) be prime and let \(S\) be an \(\mathbb {F}_p\)-subspace of the symplectic space \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\), with code distance \(d(S)\) and symplectic orthogonal complement \(S^{\perp _\omega }\). If \(E \subseteq \{ 0,\dots ,n-1\} \) is a set of erased coordinates with \(|E| \lt d(S)\), then \(E\) is correctable for \(S\): every \(v \in V_E \cap S^{\perp _\omega }\) already lies in \(S\).

Proof ▶

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.

Definition 14.17 Logical dimension
✓
#

\(k(S) = n - \dim (S)\).

14.5 Key lemma: two disjoint correctable sets

Lemma 14.18 Two disjoint correctable erasures bound the logical dimension
✓

Work in the symplectic space \(V = \mathbb {F}_p^{\, n} \times \mathbb {F}_p^{\, n}\) over the prime field \(\mathbb {F}_p\), equipped with the symplectic form \(\omega \), and let \(S \le V\) be an isotropic submodule, so that \(\omega (u,v) = 0\) for all \(u, v \in S\). Suppose \(A, B \subseteq \{ 0, 1, \dots , n-1\} \) are two disjoint sets of coordinates, each correctable for \(S\): every vector of \(S^{\perp _\omega }\) supported on \(A\) lies in \(S\), and likewise every vector of \(S^{\perp _\omega }\) supported on \(B\) lies in \(S\). Then the logical dimension \(k(S) = n - \dim S\) satisfies

\[ k(S) \; \le \; \bigl|\{ 0, 1, \dots , n-1\} \setminus (A \cup B)\bigr| \; =\; n - |A| - |B|. \]
Proof ▶

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

Theorem 14.19 Quantum Singleton bound
✓

Let \(p\) be prime and work in the symplectic space \(V = \mathbb {F}_p^{\, n} \times \mathbb {F}_p^{\, n}\) equipped with the form \(\omega \). If \(S \le V\) is an isotropic subspace, so that \(\omega (u,v) = 0\) for all \(u, v \in S\), then its logical dimension \(k(S) = n - \dim (S)\) and its distance \(d(S)\) satisfy

\[ k(S) + 2\bigl(d(S) - 1\bigr) \; \le \; n . \]
Proof ▶

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

Definition 14.20 Prime field \(\mathbb {F}_p\)
✓
#

The prime field \(\mathrm{GF}(p)\), realized as \(\mathbb {Z}/p\mathbb {Z}\) via ZMod.

Definition 14.21 Symplectic vector space
✓
#

The ambient space \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) of pairs of coordinate vectors.

Lemma 14.22 Evaluation of the bundled symplectic form
✓
#

Fix a prime \(p\) and an integer \(n\), and set \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\), equipped with the alternating bilinear form

\[ \omega \big((x,z),(x',z')\big) \; =\; \sum _{i=1}^{n}\big(x_i z'_i - z_i x'_i\big), \qquad (x,z),(x',z') \in V. \]

Let \(B \colon V \times V \to \mathbb {F}_p\) be the bilinear form on \(V\) obtained by bundling \(\omega \). Then \(B\) agrees with \(\omega \) on every pair of arguments: for all \(u, v \in V\) one has \(B(u,v) = \omega (u,v)\).

Definition 14.23 Restriction to coordinates in \(C\)
✓
#

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\).

Definition 14.24 Extension from coordinates in \(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.

Lemma 14.25 Restriction inverts extension on coordinates in \(C\)
✓

Fix a prime \(p\), a natural number \(n\), and a subset \(C \subseteq \{ 0,1,\dots ,n-1\} \) of coordinates, and let \(V_C\) denote the support submodule of \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) consisting of vectors whose support lies in \(C\). Let \(E \colon (C \to \mathbb {F}_p) \times (C \to \mathbb {F}_p) \to V_C\) be the extension map, which sends a pair \((f,g)\) to the vector agreeing with \(f\) and \(g\) on \(C\) and equal to zero off \(C\), and let \(R \colon V_C \to (C \to \mathbb {F}_p) \times (C \to \mathbb {F}_p)\) be the restriction map, which sends a vector supported on \(C\) to its two component functions restricted to \(C\). Then \(R \circ E\) is the identity: for every pair \(x = (f,g)\) of functions \(f, g \colon C \to \mathbb {F}_p\) one has \(R(E(x)) = x\).

Lemma 14.26 Extension recovers a vector supported on \(C\)
✓

Fix a prime \(p\) and a subset \(C \subseteq \{ 1,\dots ,n\} \) of coordinates, and let \(V_C \subseteq \mathbb {F}_p^n \times \mathbb {F}_p^n\) be the submodule of pairs of vectors whose support is contained in \(C\). Then extending back the coordinate functions of a supported vector recovers that vector exactly: for every \(x \in V_C\), applying the restriction map \(V_C \to (C \to \mathbb {F}_p) \times (C \to \mathbb {F}_p)\) and then the extension-by-zero map back into \(V_C\) returns \(x\). Equivalently, the extension map is a left inverse of the restriction map.

Definition 14.27 Isomorphism \(V_C \cong (\mathbb {F}_p^C)^2\)
✓

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.

Definition 14.28 Restriction map \(r_E\)
✓
#

The linear map \(r_E : V \to V_E\) that zeroes out the coordinates of a vector outside \(E\), keeping those in \(E\) unchanged.

Definition 14.29 Intersection \(S_M = S \cap V_M\)
✓
#

For a submodule \(S \le V\) and \(M \subseteq \mathrm{Fin}\, n\), the submodule \(S_M = S \cap V_M\).

Definition 14.30 Intersection \(S^{\perp }_M = S^{\perp _\omega } \cap V_M\)
✓

The submodule \(S^{\perp }_M = S^{\perp _\omega } \cap V_M\).

Definition 14.31 Supportable logical operators count \(g(M)\)
✓

\(g(S,M) = \dim _{\mathbb {F}_p}(S^{\perp }_M) - \dim _{\mathbb {F}_p}(S_M)\).

Lemma 14.32 Kernel of the coordinate restriction map
✓
#

Fix a prime \(p\) and let \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\). For a subset \(E \subseteq \{ 1,\dots ,n\} \), let \(r_E \colon V \to V_E\) be the restriction map that keeps the coordinates indexed by \(E\) and sets all others to zero. Then the kernel of \(r_E\) is the support submodule \(V_{E^c}\) consisting of those vectors whose support lies in the complement \(E^c = \{ 1,\dots ,n\} \setminus E\); that is, \(r_E\) annihilates exactly the vectors that vanish on every coordinate in \(E\).

Definition 14.33 Complement of \(E\)
✓
#

\(E^c = \mathrm{Fin}\, n \setminus E\), the complement finset of \(E\).

Lemma 14.34 Complement as set difference
✓
#

Let \(E \subseteq \mathrm{Fin}\, n\) be a finite subset. Then its complement equals the set difference of the whole space and \(E\); that is, \(E^c = \mathrm{Fin}\, n \setminus E\).

Lemma 14.35 Rank of a restricted subspace of \(\mathbb {F}_p^n \times \mathbb {F}_p^n\)
✓

Fix a prime \(p\) and an integer \(n \ge 0\), and let \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\). For a set \(E\) of coordinates, let \(r_E \colon V \to V\) be the restriction map that leaves each coordinate in \(E\) unchanged and sets every coordinate outside \(E\) to zero, and for a set \(C\) of coordinates let \(V_C \le V\) be the subspace of vectors supported on \(C\). Then for every subspace \(S \le V\),

\[ \dim _{\mathbb {F}_p} r_E(S) \; =\; \dim _{\mathbb {F}_p} S \; -\; \dim _{\mathbb {F}_p}\! \bigl(S \cap V_{E^c}\bigr), \]

where \(E^c\) denotes the complement of \(E\) among the \(n\) coordinates.

Lemma 14.36 Symplectic form is unchanged by restricting the second argument
✓

Fix a prime \(p\) and an integer \(n\), and work in the space \(V = \mathbb {F}_p^{\, n} \times \mathbb {F}_p^{\, n}\) equipped with the symplectic form \(\omega \). Let \(M \subseteq \{ 0, 1, \dots , n-1\} \) be a set of coordinates, and let \(v \in V_M\), so that every coordinate of \(v\) lying outside \(M\) vanishes. Then for every \(s \in V\),

\[ \omega (v, s) = \omega (v, r_M(s)), \]

where \(r_M(s)\) is the vector obtained from \(s\) by zeroing out all coordinates outside \(M\).

Definition 14.37 Restriction as an endomorphism of \(V\)
✓

The composition \(r_E^V : V \to V\) of \(r_E\) with the inclusion \(V_E \hookrightarrow V\).

Lemma 14.38 Restriction on the left argument of the symplectic form
✓

Let \(p\) be prime, \(\mathbb {F}_p\) the field with \(p\) elements, and let \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) carry the symplectic form \(\omega \big((x,z),(x',z')\big) = \sum _{i=0}^{n-1}(x_i z'_i - z_i x'_i)\). For a subset \(M \subseteq \{ 0,\dots ,n-1\} \), let \(r_M : V \to V\) be the endomorphism that keeps the coordinates indexed by \(M\) and sets all others to zero, and let \(V_M \subseteq V\) be the subspace of vectors whose support is contained in \(M\). Then for every \(s \in V\) and every \(v \in V_M\),

\[ \omega \big(r_M(s),\, v\big) = \omega (s, v). \]
Lemma 14.39 Non-degeneracy of the symplectic form on a support submodule
✓

Let \(p\) be a prime, let \(n\) be a natural number, and let \(M \subseteq \{ 0,1,\dots ,n-1\} \) be a subset of coordinates. Write \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) for the symplectic space equipped with the form \(\omega \big((x,z),(x',z')\big) = \sum _{i=0}^{n-1}(x_i z'_i - z_i x'_i)\), and let \(V_M \subseteq V\) be the support submodule of those vectors whose coordinates outside \(M\) all vanish. If \(v \in V_M\) satisfies \(\omega (v,w) = 0\) for every \(w \in V_M\), then \(v = 0\).

Lemma 14.40 Left restriction is invisible to the symplectic form on the support submodule
✓

Fix a prime \(p\) and a natural number \(n\), and let \(M \subseteq \{ 0,1,\dots ,n-1\} \) be a set of coordinates. For every \(s \in V\) and every \(v \in V_M\) (that is, every \(v\) supported on \(M\)),

\[ \omega \bigl(r_M^V(s),\, v\bigr) = \omega (s, v). \]

In words: applying the restriction endomorphism \(r_M^V\), which zeroes out the coordinates outside \(M\), to the left argument of the symplectic form leaves the value unchanged whenever the right argument is supported on \(M\).

Lemma 14.41 Restricting to a support before taking the symplectic complement
✓

Fix a prime \(p\) and work in the symplectic space \(V = \mathbb {F}_p^{\, n} \times \mathbb {F}_p^{\, n}\) equipped with the form \(\omega \big((x,z),(x',z')\big) = \sum _{i=0}^{n-1}(x_i z'_i - z_i x'_i)\), and for a subset \(M \subseteq \{ 0,\dots ,n-1\} \) let \(V_M\) be the submodule of vectors whose support lies in \(M\) and let \(r_M \colon V \to V\) be the map that zeroes every coordinate outside \(M\) and fixes those in \(M\). Then for every \(\mathbb {F}_p\)-subspace \(S \le V\),

\[ S^{\perp _\omega } \cap V_M \; =\; \big(r_M(S)\big)^{\perp _\omega } \cap V_M, \]

where \(r_M(S)\) denotes the image of \(S\) under \(r_M\) and \((\cdot )^{\perp _\omega }\) the orthogonal complement with respect to \(\omega \).

Definition 14.42 Restricted bundled form
✓
#

The symplectic bilinear form \(\mathrm{symB}\) restricted to the subspace \(V_M\).

Definition 14.43 Restricted symplectic form
✓

An abbreviation for \(\mathrm{symB\_ sub}\), the symplectic form viewed as a bilinear form on \(V_M\).

Lemma 14.44 Evaluation of the restricted symplectic form
✓

Fix a prime \(p\) and let \(\omega \) denote the symplectic form on \(V = \mathbb {F}_p^{\, n} \times \mathbb {F}_p^{\, n}\). For a subset \(M \subseteq \{ 0, \dots , n-1\} \) and any two vectors \(x, y\) in the support submodule \(V_M\), the restricted symplectic form evaluated at \((x, y)\) agrees with \(\omega (x, y)\) computed on \(x\) and \(y\) regarded as elements of the ambient space \(V\).

Lemma 14.45 Nondegeneracy of the restricted symplectic form
✓

Let \(p\) be a prime, and equip \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) with the symplectic form \(\omega \big((x,z),(x',z')\big) = \sum _{i=0}^{n-1}(x_i z'_i - z_i x'_i)\). For any subset \(M \subseteq \{ 0,\dots ,n-1\} \), let \(V_M\) be the support submodule consisting of those \((x,z) \in V\) with \(x_i = z_i = 0\) for every \(i \notin M\). Then the restriction of \(\omega \) to \(V_M\) is nondegenerate: if \(u \in V_M\) satisfies \(\omega (u,v) = 0\) for all \(v \in V_M\), then \(u = 0\).

Lemma 14.46 Orthogonal complement of a subspace, intersected with a support submodule
✓

Let \(p\) be a prime and let \(\omega \) be the symplectic form on \(V = \mathbb {F}_p^{\, n} \times \mathbb {F}_p^{\, n}\). For any subset \(M\) of \(\{ 0, 1, \dots , n-1\} \) and any submodule \(S \le V\), the vectors of the support submodule \(V_M\) that are \(\omega \)-orthogonal to every element of \(S\) are exactly the images, under the inclusion \(V_M \hookrightarrow V\), of the vectors of \(V_M\) that are orthogonal to \(r_M(S)\) with respect to the restriction of \(\omega \) to \(V_M\). In symbols, writing \(\iota \colon V_M \hookrightarrow V\) for the inclusion and \(\perp _M\) for orthogonality with respect to the restricted form,

\[ S^{\perp _\omega } \cap V_M \; =\; \iota \! \left( r_M(S)^{\perp _M} \right), \]

where \(r_M(S)\) is the image of \(S\) under the restriction map \(r_M \colon V \to V_M\).

Lemma 14.47 Reflexivity of the restricted symplectic form
✓

Fix a prime \(p\), a natural number \(n\), and a subset \(M \subseteq \{ 0,1,\dots ,n-1\} \), and let \(V_M\) be the associated support submodule of \(V = \mathbb {F}_p^{\, n} \times \mathbb {F}_p^{\, n}\). Then the restriction to \(V_M\) of the symplectic form \(\omega (u,v) = \sum _{i} (x_i z'_i - z_i x'_i)\), where \(u=(x,z)\) and \(v=(x',z')\), is reflexive: for all \(u, v \in V_M\), if \(\omega (u,v) = 0\) then \(\omega (v,u) = 0\).

Lemma 14.48 Dimension of the orthogonal intersection over a coordinate set
✓

Fix a prime \(p\), an integer \(n\), and work in the symplectic space \(V = \mathbb {F}_p^{\, n} \times \mathbb {F}_p^{\, n}\) equipped with the symplectic form \(\omega \big((x,z),(x',z')\big) = \sum _{i} (x_i z'_i - z_i x'_i)\). Let \(M\) be a subset of the coordinate set \(\{ 0,1,\dots ,n-1\} \), let \(V_M \le V\) be the support submodule of vectors whose coordinates vanish outside \(M\), and let \(r_M : V \to V_M\) be the restriction map that zeroes every coordinate outside \(M\). Then for any \(\mathbb {F}_p\)-subspace \(S \le V\), the symplectic orthogonal complement \(S^{\perp _\omega }\) satisfies

\[ \dim _{\mathbb {F}_p}\big(S^{\perp _\omega } \cap V_M\big) \; =\; 2\, \left\lvert M\right\rvert \; -\; \dim _{\mathbb {F}_p}\big(r_M(S)\big). \]

Fix a prime \(p\) and equip \(V = \mathbb {F}_p^{\, n} \times \mathbb {F}_p^{\, n}\) with the symplectic form \(\omega \big((x,z),(x',z')\big) = \sum _{i=0}^{n-1}\big(x_i z'_i - z_i x'_i\big)\). For a set of coordinates \(M \subseteq \{ 0,\dots ,n-1\} \), let \(V_M \le V\) be the subspace of vectors supported on \(M\), and for a subspace \(W \le V\) write \(W_M = W \cap V_M\). Let \(S \le V\) be isotropic, meaning \(\omega (u,v) = 0\) for all \(u,v \in S\), let \(S^{\perp }\) denote its symplectic orthogonal complement, and set \(g(S,M) = \dim _{\mathbb {F}_p}\! \big(S^{\perp }\cap V_M\big) - \dim _{\mathbb {F}_p}(S_M)\). Then, writing \(M^c\) for the complementary set of coordinates,

\[ g(S,M) \; =\; 2\, \left\lvert M\right\rvert + \dim _{\mathbb {F}_p}\! \big(S_{M^c}\big) - \dim _{\mathbb {F}_p}(S) - \dim _{\mathbb {F}_p}(S_M). \]
Lemma 14.50 Double complement in a finite set
✓
#

Fix a natural number \(n\), and for a subset \(E \subseteq \mathrm{Fin}\, n\) write \(E^c = \mathrm{Fin}\, n \setminus E\) for its complement. Then for every subset \(M \subseteq \mathrm{Fin}\, n\), taking the complement twice recovers the original set: \((M^c)^c = M\).

Lemma 14.51 Additivity bound for support-restricted subspaces
✓

Fix a prime \(p\) and an integer \(n\), and let \(S\) be a subspace of the ambient space \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\). For a subset \(M \subseteq \{ 1,\dots ,n\} \) with complement \(M^c\), write \(S_M = S \cap V_M\) and \(S_{M^c} = S \cap V_{M^c}\) for the intersections of \(S\) with the corresponding support subspaces. Then

\[ \dim _{\mathbb {F}_p} S_M + \dim _{\mathbb {F}_p} S_{M^c} \le \dim _{\mathbb {F}_p} S. \]
Lemma 14.52 Dimension formula for the operator count of an isotropic subspace
✓

Let \(p\) be prime, and equip the symplectic space \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) with its standard alternating form \(\omega \). If \(S \le V\) is an isotropic subspace and \(M \subseteq \{ 0,1,\dots ,n-1\} \) is any set of coordinates, then

\[ g(S,M) \; =\; \bigl(2\, \left\lvert M\right\rvert + \dim _{\mathbb {F}_p} S_{M^c}\bigr) \; -\; \bigl(\dim _{\mathbb {F}_p} S + \dim _{\mathbb {F}_p} S_M\bigr), \]

where \(M^c\) is the complement of \(M\) and \(S_{M^c} = S \cap V_{M^c}\) consists of the vectors of \(S\) supported on \(M^c\).

Let \(S\) be an isotropic submodule of the symplectic space \(V=\mathbb {F}_p^n\times \mathbb {F}_p^n\), and let \(M\subseteq \{ 0,\dots ,n-1\} \) be a set of coordinates with complement \(M^c\). Writing \(S_M=S\cap V_M\) and \(S_{M^c}=S\cap V_{M^c}\) for the parts of \(S\) supported on \(M\) and on its complement, one has

\[ g(S,M)+\dim _{\mathbb {F}_p}(S_M)+\dim _{\mathbb {F}_p}(S) \; =\; 2\lvert M\rvert + \dim _{\mathbb {F}_p}(S_{M^c}). \]
Lemma 14.54 A dimension inequality for isotropic subspaces
✓

Let \(p\) be a prime and \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\), equipped with the symplectic form \(\omega \big((x,z),(x',z')\big) = \sum _{i} (x_i z'_i - z_i x'_i)\). For a coordinate subset \(M \subseteq \{ 0,\dots ,n-1\} \), let \(V_M \le V\) be the support submodule of vectors supported on \(M\), and for a subspace \(S \le V\) write \(S_M = S \cap V_M\). If \(S\) is isotropic, that is \(\omega (u,v) = 0\) for all \(u,v \in S\), then

\[ \dim _{\mathbb {F}_p} S + \dim _{\mathbb {F}_p} S_M \; \le \; 2\, \left\lvert M\right\rvert + \dim _{\mathbb {F}_p} S_{M^c}, \]

where \(M^c = \{ 0,\dots ,n-1\} \setminus M\) is the complementary coordinate set.

Lemma 14.55 Cleaning dimension identity for isotropic subspaces
✓

Let \(p\) be prime and let \(S \le V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) be a subspace that is isotropic for the symplectic form \(\omega \), meaning \(\omega (u,v)=0\) for all \(u,v \in S\). Then for every subset \(M \subseteq \{ 0,\dots ,n-1\} \), with complement \(M^c\),

\[ g(S,M) + g(S,M^c) = 2n - 2\dim _{\mathbb {F}_p} S, \]

where \(g(S,M) = \dim _{\mathbb {F}_p}\! \big(S^{\perp }_M\big) - \dim _{\mathbb {F}_p}\! \big(S_M\big)\).

Lemma 14.56 Cardinality of a subset plus its complement
✓
#

Let \(n\) be a natural number and let \(M\) be a subset of the \(n\)-element index set \(\mathrm{Fin}\, n = \{ 0, 1, \dots , n-1\} \). Then the size of \(M\) and the size of its complement \(M^c = \mathrm{Fin}\, n \setminus M\) add up to \(n\):

\[ \left\lvert M\right\rvert + \left\lvert M^c\right\rvert = n. \]
Lemma 14.57 Correctable coordinate sets carry no supportable logical operators
✓

Fix a prime \(p\), let \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) be equipped with the symplectic form \(\omega \big((x,z),(x',z')\big) = \sum _{i} (x_i z'_i - z_i x'_i)\), and let \(S \le V\) be a subspace with symplectic orthogonal complement \(S^{\perp _\omega } = \{ v \in V : \omega (v,s) = 0 \text{ for all } s \in S\} \). Let \(M \subseteq \{ 0,1,\dots ,n-1\} \) be a set of coordinates, write \(V_M\) for the subspace of vectors supported on \(M\), and set \(S_M = S \cap V_M\) and \(S^{\perp }_M = S^{\perp _\omega } \cap V_M\). If \(M\) is correctable for \(S\) — meaning every vector of \(S^{\perp _\omega }\) supported on \(M\) already lies in \(S\), i.e. \(S^{\perp }_M \le S\) — then \(g(S,M) = \dim _{\mathbb {F}_p}(S^{\perp }_M) - \dim _{\mathbb {F}_p}(S_M) = 0\).

Lemma 14.58 Correctable erasure and the count of supportable logical operators
✓

Let \(S\) be an isotropic subspace of the symplectic space \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) (with \(p\) prime), and let \(M \subseteq \{ 0,1,\dots ,n-1\} \) be an erasure set that is correctable for \(S\). Writing \(M^c\) for the complement of \(M\), one has

\[ g(S, M^c) \; =\; 2n - 2\dim _{\mathbb {F}_p} S. \]
Lemma 14.59 Correctable part contributes nothing to the operator count
✓

Let \(p\) be prime and let \(S\) be an \(\mathbb {F}_p\)-subspace of the symplectic space \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\). Suppose \(B\) and \(C\) are disjoint subsets of the coordinate set \(\{ 0,\dots ,n-1\} \), and that \(B\) is correctable for \(S\). Then

\[ g(S,\, B \cup C) \; \le \; 2\lvert C\rvert , \]

where \(g(S,M) = \dim _{\mathbb {F}_p}\! \bigl(S^{\perp }_M\bigr) - \dim _{\mathbb {F}_p}\! \bigl(S_M\bigr)\).

Proof ▶

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.

Lemma 14.60 Full index set gives the whole space
✓

Fix a prime \(p\) and an integer \(n\), and let \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\). Taking \(C\) to be the full index set \(\{ 0,1,\dots ,n-1\} \), the support submodule \(V_C = \{ v \in V \mid \mathrm{supp}(v) \subseteq C\} \) is all of \(V\); that is, \(V_C = V\).

Lemma 14.61 Dimension of the ambient space
✓

Let \(p\) be a prime and \(\mathbb {F}_p\) the field with \(p\) elements, and for a natural number \(n\) set \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\). Then \(V\) is a vector space over \(\mathbb {F}_p\) of dimension

\[ \dim _{\mathbb {F}_p}(V) = 2n. \]
Lemma 14.62 Non-degeneracy of the standard symplectic form
✓
#

Fix a prime \(p\) and an integer \(n\), and let \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) carry the bilinear form

\[ \omega \big((x,z),(x',z')\big) \; =\; \sum _{i=1}^{n}\big(x_i z'_i - z_i x'_i\big) \]

over the prime field \(\mathbb {F}_p\). Then \(\omega \) is non-degenerate: the only vector \(u \in V\) with \(\omega (u,v) = 0\) for every \(v \in V\) is \(u = 0\).

Lemma 14.63 Reflexivity of the symplectic form
✓

Let \(p\) be a prime, \(n\) a natural number, and let \(\omega \) be the bilinear form on \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) given by \(\omega (u,v) = \sum _{i=1}^{n}(x_i z'_i - z_i x'_i)\) for \(u = (x,z)\) and \(v = (x',z')\). Then \(\omega \) is reflexive: for all \(u, v \in V\), if \(\omega (u,v) = 0\) then \(\omega (v,u) = 0\).

Lemma 14.64 Dimension bound for isotropic subspaces
✓

Let \(p\) be a prime and equip the \(2n\)-dimensional space \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\) over \(\mathbb {F}_p\) with the symplectic form \(\omega \big((x,z),(x',z')\big) = \sum _{i=1}^{n} (x_i z'_i - z_i x'_i)\). If \(S \le V\) is an isotropic subspace, meaning \(\omega (u,v) = 0\) for all \(u, v \in S\), then \(\dim _{\mathbb {F}_p} S \le n\).

Let \(p\) be a prime and let \(S\) be a subspace of the symplectic space \(V = \mathbb {F}_p^n \times \mathbb {F}_p^n\). If \(S\) is isotropic and its logical dimension vanishes, \(k(S) = 0\), then the code distance vanishes as well, \(d(S) = 0\).

Lemma 14.66 Existence of two disjoint sets of equal size
✓
#

Let \(n\) and \(t\) be natural numbers with \(2t \le n\). Then there exist two disjoint subsets \(A, B \subseteq \{ 1, \dots , n\} \), each of cardinality \(t\).