Dependencies

A codeword of length \(n\) over alphabet \(\alpha \) is a function \(c : \mathrm{Fin}\, n \to \alpha \).

Pointwise addition, subtraction, and the all-zero codeword.

A (block) code of length \(n\) over \(\alpha \) is a finite set () of codewords.

A code \(C\) is linear with generator matrix \(G\) (shape \(n\times m\)) if every message \(c':\mathrm{Fin}\, m\to \alpha \) maps to a codeword \(Gc'\in C\), and every codeword in \(C\) arises this way.

Existential version: there exists some \(m\) and generator matrix \(G\) witnessing linearity.

Hamming distance between two codewords, wrapping Mathlib’s .

holds when \(d\) is the minimum Hamming distance of \(C\): there exist distinct codewords at distance exactly \(d\), and no two distinct codewords are closer than \(d\).

The Hamming weight of \(c\) is \(d(c, \mathbf{0})\).

asserts existence of a code of size \(A\) and minimum distance \(d\) that is maximal among all such codes.

The Hamming ball of radius \(l\) around \(c\):

implemented as a .

If a code \(C\) has minimum distance \(d\), then \(d \le n\).

Assuming \(\alpha \) is nontrivial, a code \(C\subseteq \alpha ^n\) with minimum distance \(d\) satisfies

For any center \(c\) and radius \(l\),

If \(C\) has minimum distance \(d\gt 0\), then for distinct \(c_1,c_2\in C\),

Reformulation of the previous lemma as .

Let \(q=|\alpha |\gt 1\). If \(C\subseteq \alpha ^n\) has minimum distance \(d\gt 0\), then

For \(0\lt p\le 1-1/q\) and \(q=|\alpha |\),

For \(q\ge 2\) and \(0\lt p\lt 1\),

Variant using a different exponentiation operator.

For \(x\ge 0\),

For \(0\lt p\lt 1\) and \(q\ge 2\), eventually

For \(q=|\alpha |\) and \(0\lt p\le 1-1/q\),

If \(C\) is linear (witnessed by some generator matrix) and has minimum distance \(d\), then:

• every nonzero codeword in \(C\) has weight at least \(d\);

• some codeword in \(C\) has weight exactly \(d\).

The uniform probability mass function on \(\alpha ^n\), encoded as a function \(\alpha ^n\to \mathbb {R}\) assigning \(1/|\alpha |^n\) to each vector.

For fixed \(x\in \alpha ^k\) and \(v\in \alpha ^n\), the set \(\{ G : Gx=v\} \) is finite.

\(\mu _x(v)\) is the fraction of \(n\times k\) matrices \(G\) satisfying \(Gx=v\).

Utility returning the \(i\)-th row of a matrix as a \(1\times k\) matrix.

If \(x\neq 0\) and \(k\ge 1\), then for a uniformly random \(n\times k\) matrix \(G\) over \(\alpha \), the product \(Gx\) is uniformly distributed over \(\alpha ^n\):

For any nonzero \(x\in \alpha ^k\),

The number of \(n\times k\) matrices that send some nonzero message to a codeword of weight \(\lt d\) is at most

If \(k \le n - \lceil \log _q|B_{d-1}(\mathbf{0})|\rceil - 1\), then there exists a generator matrix \(G\) such that every nonzero message is mapped to a codeword of Hamming weight at least \(d\).

A code \(C\) is \((\rho ,L)\)-list-decodable if every Hamming ball of radius \(\lfloor \rho n\rfloor \) contains at most \(L\) codewords of \(C\).

If the ball volume \(V\) and code size \(M\) satisfy the counting inequality

then there exists a code \(C\) of size \(M\) that is \((p,L)\)-list-decodable.

For \(k\le M\le N\),

For the choice \(r = 1-H_q(\rho )-1/L\), \(M=\lfloor q^{rn}\rfloor \), and \(V=\lfloor q^{H_q(\rho )n}\rfloor \), whenever \(L\lt M\le q^n\),

For any \(q=|\alpha |\), \(0\lt \rho \le 1-1/q\), and \(L\ge 1\), there exist codes of rate \(r = 1-H_q(\rho )-1/L\) that are \((\rho ,L)\)-list-decodable.

A binary codeword of length \(n\) is a function \(\mathrm{Fin}\, n \to \mathrm{Bool}\).

The Hamming weight \(\mathrm{wt}(x) = |\{ i : x_i = 1\} |\); the Hamming distance \(\mathrm{hdist}(x,y) = \mathrm{wt}(x \oplus y)\).

A code \(C \subseteq \{ 0,1\} ^n\) is \((n,d,w)\)-admissible if every pair of distinct codewords has Hamming distance \(\ge d\) and every codeword has weight \(\le w\).

Map \(x \in \{ 0,1\} ^n\) to the vector \(\hat{x}^\alpha _i = (-1)^{x_i} - \alpha \) (with \(\alpha \ge 0\)), viewed in \(\mathbb {R}^n\).

\(\langle \hat{x},\hat{y}\rangle = n - 2\, \mathrm{hdist}(x,y)\).

For \(\alpha \ge 0\), \(\mathrm{hdist}(x,y) \ge d\), and \(\mathrm{wt}(x),\mathrm{wt}(y) \le w\),

If \(n \gt 0\), \(1 \le d\), \(2d \le n\), and \(w \le J_2(n,d)\), then \((n - 2d) + \alpha ^2 n + 2\alpha (2w - n) \le 0\) for the choice \(\alpha = \alpha (n,d)\).

In a finite inner-product space, if a set \(S\) of unit vectors has pairwise non-positive inner products, then one can project away one vector and reduce to a smaller set in the orthogonal complement with the same property.

A set of unit vectors in an \(n\)-dimensional real inner product space with pairwise non-positive inner products has size at most \(2n\).

A finite set of unit vectors in \(\mathbb {R}^n\) with pairwise non-positive inner products has cardinality at most \(2n\).

Let \(C \subseteq \{ 0,1\} ^n\) be a code with minimum distance \(\ge d\) and all weights \(\le w\). For any \(\alpha \ge 0\) with \((n-2d) + \alpha ^2 n + 2\alpha (2w-n) \le 0\),

If \(n \gt 0\), \(1 \le d\), \(2d \le n\), and all codewords of \(C\) have weight \(\le w \le J_2(n,d)\) and minimum distance \(\ge d\), then \(|C| \le 2n\).

Every \((n,d,w)\)-admissible code \(C\) with \(w \le J_2(n,d)\) satisfies \(|C| \le 2n\).

\(A_0(n,d,w)\) is the maximum size of an \((n,d,w)\)-admissible code.

If \(n \gt 0\), \(1 \le d\), \(2d \le n\), and \(w \le J_2(n,d)\), then

For a finite field \(\mathbb {F}_q\) and \(n \in \mathbb {N}\), the symplectic space is the vector space \(V = \mathbb {F}_q^n \times \mathbb {F}_q^n\), equipped with the symplectic form

A subspace \(S \le V\) is isotropic if \(\omega (u,v)=0\) for all \(u,v\in S\).

Classical codes \(C_Z, C_X \le \mathbb {F}_q^n\) satisfy the CSS condition if

Given \(C_Z \perp C_X\), the CSS stabilizer is the subspace of \(V\) generated by the \(X\)-type vectors \((x,0)\) for \(x \in C_Z\) and \(Z\)-type vectors \((0,z)\) for \(z \in C_X\).

The CSS stabilizer is isotropic if and only if the CSS condition holds.

If \(C_Z \perp C_X\), then \(\dim (\mathrm{cssStabilizer}) = \dim (C_Z) + \dim (C_X)\).

The CSS code \(Q(C_Z, C_X)\) encodes \(k = n - \dim (C_Z) - \dim (C_X)\) logical qudits, and has distance \(d = \min (d_Z, d_X)\) where \(d_Z\) (resp. \(d_X\)) is the minimum weight of a vector in \(C_Z^\perp \setminus C_X\) (resp. \(C_X^\perp \setminus C_Z\)).

The four Pauli basis elements \(\{ I,X,Y,Z\} \), represented as an inductive type.

A Pauli string of length \(n\) is a function \(p : \mathrm{Fin}\, n \to \mathrm{PauliBasis}\).

The support \(\mathrm{supp}(p) \subseteq \mathrm{Fin}\, n\) consists of coordinates where \(p(i) \neq I\); the weight is \(\mathrm{wt}(p) = |\mathrm{supp}(p)|\).

The set of all Pauli strings of weight at most \(t\):

The \(n\)-qubit Hilbert space \(\mathcal{H}_n = \ell ^2\! \bigl(\{ 0,1\} ^n,\mathbb {C}\bigr)\), implemented as .

\(\dim _{\mathbb {C}}(\mathcal{H}_n) = 2^n\).

For \(p \in \mathrm{PauliString}\, n\), the associated Pauli operator \(\hat{p} : \mathcal{H}_n \to \mathcal{H}_n\).

A subspace \(C \le \mathcal{H}_n\) satisfies the Knill–Laflamme condition for \(t\)-error correction if for all Pauli strings \(E,F\) with \(\mathrm{wt}(E),\mathrm{wt}(F) \le t\) there exists \(\lambda _{EF}\in \mathbb {C}\) such that \(P_C\, E^\dagger F\, P_C = \lambda _{EF}\, P_C\), where \(P_C\) is the orthogonal projection onto \(C\).

A code is non-degenerate if it satisfies the Knill–Laflamme condition and additionally \(P_C E^\dagger F P_C = 0\) whenever \(E \neq F\).

The error sphere \(\mathrm{ES}(C,t)\) is the subspace \(\bigvee _{\mathrm{wt}(p)\le t} \hat{p}(C)\), i.e. the supremum of the Pauli images of \(C\) over all \(t\)-errors.

If \(C\) is non-degenerate and \(E \neq F\) both have weight \(\le t\), then \(\hat{E}(C) \perp \hat{F}(C)\).

If \(C\) is non-degenerate,

If \(C \le \mathcal{H}_n\) is non-degenerate, then

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 .

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

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

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

Let \(S\) be isotropic. If \(A,B \subseteq \mathrm{Fin}\, n\) are disjoint and both correctable, then

For any isotropic submodule \(S \le V\),