A Symplectic Proof of the Quantum Singleton Bound
Frederick Dehmel, Shilun Li
quant-ph
Feb 21, 2026 · v3
cs.IT
TL;DR
Formalizes in Lean 4 the symplectic linear-algebraic proof of the Quantum Singleton Bound, including the cleaning dimension identity and the main theorem.
Abstract
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.
Problem
The Quantum Singleton Bound k+2(d-1) ≤ n for [[n,k,d]] stabiliser codes is usually proved with entropy or no-cloning arguments. The question is whether it can be derived purely within the symplectic linear-algebraic stabiliser framework and machine-checked.
Approach
Pauli operators are modelled as vectors in a 2n-dimensional symplectic space over a prime field, and a stabiliser code as an isotropic subspace. The proof combines distance-based erasure correctability, the cleaning dimension identity g(M)+g(M^c)=2k, and a lemma that two disjoint correctable sets bound k by the size of the remaining positions. The full linear-algebraic development is formalised in Lean 4.
Results
A self-contained dimension-counting proof of k+2(d-1) ≤ n is given. The authors describe its Lean 4 formalisation as, to their knowledge, the first formalisation of the Quantum Singleton Bound.
