A Symplectic Proof of the Quantum Singleton Bound

TL;DR

This paper provides a symplectic linear-algebraic proof of the Quantum Singleton Bound for stabiliser codes, emphasizing algebraic structure and formal verification compatibility.

Contribution

It introduces a symplectic vector space approach and formalisation in Lean4, offering a new, algebraic perspective on the quantum Singleton Bound.

Findings

Derives the bound $k + 2(d-1) extless n$ using symplectic vector spaces.

Provides a formal Lean4 proof of the algebraic argument.

Avoids entropy-based methods, focusing on algebraic and geometric reasoning.

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.