量子Singleton界限的一个辛证明
A Symplectic Proof of the Quantum Singleton Bound
AI总结：
本文通过辛线性代数方法证明稳定子量子纠错码的量子Singleton界限，并给出Lean4形式化验证，核心是利用辛空间中的距离可擦除性和清洗引理进行维度计数。
摘要：
我们给出了稳定子量子纠错码的量子Singleton界限的一个辛线性代数证明，以及该线性代数论证的Lean4形式化。该证明以有限维辛向量空间的语言表述，用于建模Pauli算子，并依赖于基于距离的可擦除性和清洗引理。通过在辛稳定子框架内进行维度计数论证，我们推导出任意$[[n, k, d]]$稳定子码满足$k + 2(d-1) \le n$。这种方法隔离了界限背后的代数结构，避免了基于熵的证明中出现的更复杂的分析机制，同时非常适合形式化验证。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
