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.

翻译：我们给出了一种关于稳定子量子纠错码的量子Singleton界限的辛线性代数证明，并附带该线性代数论证的Lean4形式化。该证明采用有限维辛向量空间的语言来描述泡利算符，并基于距离的擦除可纠正性和清洁引理。利用辛稳定子框架中的维数计数论证，我们推导出任意[[n, k, d]]稳定子码满足约束关系$k + 2(d-1) \le n$。该方法分离了该界限背后的代数结构，避免了基于熵的证明中所需的更复杂的解析技巧，同时十分适合形式化验证。