9 CSS Codes (Not Yet Formalized)
9.1 Overview
This chapter describes the Calderbank–Shor–Steane (CSS) construction, which builds a quantum stabilizer code from two classical linear codes \(C_Z, C_X \subseteq \mathbb {F}_q^n\) satisfying the orthogonality condition \(C_Z \subseteq C_X^\perp \).
The CSS formalization is not yet present in the Lean library. The symplectic-form machinery used in the quantum Singleton bound (see Chapter 11) provides the underlying linear-algebra foundation.
9.2 Symplectic vector space
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\).
9.3 CSS construction
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)\).
9.4 CSS code parameters
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\)).