← All papers
A Symplectic Proof of the Quantum Singleton Bound
quant-ph
Feb 21, 2026 · v2
cs.IT
TL;DR
Gives a symplectic linear-algebraic proof of the Quantum Singleton Bound with a Lean4 formalization of the argument.
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
Standard proofs of the Quantum Singleton Bound for stabiliser codes rely on entropy or the no-cloning theorem, which are heavier than needed and less suited to formal verification.
Approach
The authors model Pauli operators as a finite-dimensional symplectic vector space and derive the bound k+2(d-1)<=n from distance-based erasure correctability and a dimension-counting cleaning lemma, avoiding entropic machinery. They give the first Lean4 formalisation of the full linear-algebraic development, including the symplectic form, stabiliser codes, the cleaning dimension identity, and the main theorem.
Results
A self-contained symplectic proof of the Quantum Singleton Bound for [[n,k,d]] stabiliser codes together with its Lean4 formalisation.