We present a symplectic linear-algebraic proof of the Quantum Singleton Bound for stabiliser quantum error-correcting codes together with a Lean4 formalisation of the linear-algebraic argument. The proof is formulated in the language of finite-dimensional symplectic vector spaces modelling Pauli operators and relies on distance-based erasure correctability and the cleaning lemma. Using a dimension-counting argument within the symplectic stabiliser framework, we derive the bound $k + 2(d-1) \le n$ for any $[[n, k, d]]$ stabiliser code. This approach isolates the algebraic structure underlying the bound and avoids the heavier analytic machinery that appears in entropy-based proofs, while remaining well-suited to formal verification.
We present a symplectic linear-algebraic proof of the Quantum Singleton Bound for stabiliser quantum error-correcting codes together with a Lean4 formalisation of the linear-algebraic argument. The proof is formulated in the language of finite-dimensional symplectic vector spaces modelling Pauli operators and relies on distance-based erasure correctability and the cleaning lemma. Using a dimension-counting argument within the symplectic stabiliser framework, we derive the bound k+2(d−1)≤n for any [[n,k,d]] stabiliser code. This approach isolates the algebraic structure underlying the bound and avoids the heavier analytic machinery that appears in entropy-based proofs, while remaining well-suited to formal verification.
This work introduces a symplectic framework for quantum error correcting codes in which local structure is analyzed through an anticode perspective. In this setting, a code is treated as a symplectic space, and anticodes arise as maximal symplectic subspaces whose elements vanish on a prescribed set of components, providing a natural quantum analogue of their classical counterparts. This framework encompasses several families of quantum codes, including stabilizer and subsystem codes, provides a natural extension of generalized distances in quantum codes, and yields new invariants that capture local algebraic and combinatorial features. The notion of anticodes also naturally leads to operations such as puncturing and shortening for symplectic codes, which in turn provide algebraic interpretations of key phenomena in quantum error correction, such as the cleaning lemma and complementary recovery and yield new descriptions of weight enumerators.
We show that a relatively simple reasoning using von Neumann entropy inequalities yields a robust proof of the quantum Singleton bound for quantum error-correcting codes (QECC). For entanglement-assisted quantum error-correcting codes (EAQECC) and catalytic codes (CQECC), a type of generalized quantum Singleton bound [Brunet al., IEEE Trans. Inf. Theory 60(6):3073–3089 (2014)] was believed to hold for many years until recently one of us found a counterexample [MG, Phys. Rev. A 103, 020601 (2021)]. Here, we rectify this state of affairs by proving the correct generalized quantum Singleton bound, extending the above-mentioned proof method for QECC; we also prove information-theoretically tight bounds on the entanglement-communication tradeoff for EAQECC. All of the bounds relate block lengthnand code lengthkfor given minimum distancedand we show that they are robust, in the sense that they hold with small perturbations for codes which only correct most of the erasure errors of less thandletters. In contrast to the classical case, the bounds take on qualitatively different forms depending on whether the minimum distance is smaller or larger than half the block length. We also provide a propagation rule: any pure QECC yields an EAQECC with the same distance and dimension, but of shorter block length.
This paper presents a complete, constructive derivation of the Steane [[7,1,3]] quantum error-correcting code using a unified framework that bridges GF(4) algebra, binary symplectic representation, and stabilizer formalism. We demonstrate how classical coding theory, finite-field arithmetic, and symplectic geometry naturally converge to form a comprehensive foundation for quantum error correction. Starting from the classical Hamming [7,4,3] code, we provide explicit constructions showing: (1) how GF(4) encodes the Pauli group modulo phases, (2) how the symplectic inner product on F2n2 captures commutativity, (3) how syndrome extraction reduces to binary matrix multiplication, and (4) how transversal Clifford gates emerge from symplectic transformations. The step-by-step derivation encompasses stabilizer construction, centralizer analysis, logical operator identification, code distance verification, and fault-tolerant syndrome measurement via flagged circuits. All results are derived using elementary finite-field and binary linear algebra, ensuring the exposition is self-contained and accessible. We further illustrate how this algebraic framework extends naturally to modern quantum LDPC codes. This work serves as both a pedagogical tutorial for students entering quantum error correction and a unified reference for researchers implementing stabilizer codes in practice
The quantum Hamming bound arises from a direct dimension estimate for exact quantum error-correcting codes. For nondegenerate codes, distinct correctable errors map the code space into orthogonal subspaces, so dimension counting directly gives the bound; degeneracy allows these subspaces to overlap and invalidates the argument. Although linear-programming, asymptotic, and structural approaches have advanced the problem from several directions, the general local-dimension case has remained open. Here we prove the quantum Hamming bound for every local dimension q≥3. Building on the exact two-center Fourier reduction, we develop new overlap estimates for nonbinary Hamming spaces. For q≥4, Jacobi estimates and monotonicity give a uniform gap; qutrits form the boundary case where the gap vanishes and are handled by a filtered correction. This completes the finite-length nonbinary case; together with the existing qubit result, it establishes the quantum Hamming bound for arbitrary local dimension.
Linear programming approaches have been applied to derive upper bounds on the size of classical and quantum codes. In this paper, we derive similar results for general quantum codes with entanglement assistance by considering a type of split weight enumerator. After deriving the MacWilliams identities for these enumerators, we are able to prove algebraic linear programming bounds, such as the Singleton bound, the Hamming bound, and the first linear programming bound. Our Singleton bound and Hamming bound are more general than the previous bounds for entanglement-assisted quantum stabilizer codes. In addition, we show that the first linear programming bound improves the Hamming bound when the relative distance is sufficiently large. On the other hand, we obtain additional constraints on the size of Pauli subgroups for quantum codes, which allow us to improve the linear programming bounds on the minimum distance of quantum codes of small length. In particular, we show that there is no [[27, 15, 5]] or [[28, 14, 6]] stabilizer code. We also discuss the existence of some entanglement-assisted quantum stabilizer codes with maximal entanglement. As a result, the upper and lower bounds on the minimum distance of maximal-entanglement quantum stabilizer codes with length up to 20 are significantly improved.
Quantum error-correcting codes (QECCs) sit between noisy quantum hardware and reliable computation, so the code parameters used in practice must be trustworthy. The single number that summarizes a code's strength is its distance, yet certifying a distance lower bound is NP-hard in general, placing it beyond the reach of pen-and-paper proofs as well as direct proof-assistant scripting. As a result, distance values in the literature come either from non-scaling hand proofs, or from unverified solvers that leave a trust gap exactly where the code is supposed to provide a guarantee. We present Lean-QEC, the first Lean 4 formalization of stabilizer-code theory that delivers end-to-end, machine-checked distance certificates at industrial code sizes. Lean-QEC formalizes the linear algebra of qubit states, the Pauli group, stabilizer codes, the binary symplectic representation, classical coding theory, and the CSS and Bivariate Bicycle families. To break the combinatorial barrier, Lean-QEC translates the distance condition into a Boolean satisfiability formula through a verified reduction. The pipeline scales through a BitVec-flattened encoding that replaces Lean's Matrix representation, and an error-location encoding that reduces the variable count from n to k⌈log2n⌉. With these, we obtain automatically-generated Lean-checked distance proofs for a large range of industrially viable qLDPC codes within the Bivariate Bicycle and Generalized Bicycle families, including [[90, 8, 10]] and [[70, 6, 9]] BB codes, with the formulation scaling up to 144 qubits when performed outside the Lean kernel. The resulting library is reusable and is designed to plug into broader Lean-based efforts toward end-to-end verification of fault-tolerant quantum computation.