Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Symplectic Proof of the Quantum Singleton Bound

Frederick Dehmel, Shilun Li

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.

A Symplectic Proof of the Quantum Singleton Bound

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.
Paper Structure (14 sections, 8 theorems, 25 equations)

This paper contains 14 sections, 8 theorems, 25 equations.

Table of Contents

  1. Motivation
  2. Contributions
  3. Introduction
  4. Conventions and symplectic model
  5. Support, restriction, and distance
  6. Erasure correctability
  7. Cleaning lemma and the dimension identity
  8. A symplectic consequence of correctable erasure
  9. Quantum Singleton bound
  10. Conclusion
  11. Lean4 formalisation and code index
  12. Repository and permalinks
  13. Pointers to core definitions
  14. Pointers to key lemmas and the main theorem

Key Result

Lemma 1

If $u\in V$ satisfies $\langle u,v\rangle = 0$ for all $v\in V$, then $u=0$.

Theorems & Definitions (26)

  • Remark 1: Field convention
  • Definition 1: Standard symplectic form
  • Lemma 1: Nondegeneracy
  • proof
  • Definition 2: Support and weight
  • Definition 3: Support subspace
  • Lemma 2: Dimension of a support subspace
  • proof
  • Definition 4: Restriction map
  • Definition 5: stabiliser subspace and distance
  • ...and 16 more