A Symplectic Proof of the Quantum Singleton Bound

Frederick Dehmel, Shilun Li

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-algebr…