Pith. sign in

REVIEW 2 major objections 5 minor 1 cited by

The paper derives the Quantum Singleton Bound k+2(d−1)≤n for stabiliser codes from a symplectic dimension identity, and offers a machine-checked formalization.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-02 21:53 UTC pith:DHDVURCZ

load-bearing objection A clean but non-novel symplectic re-derivation of the Singleton bound; the Lean4 formalisation is the real contribution, but the paper has a genuine edge-case gap in Remark 3 and ships no code. the 2 major comments →

arxiv 2602.20186 v3 pith:DHDVURCZ submitted 2026-02-21 quant-ph cs.ITmath.IT

A Symplectic Proof of the Quantum Singleton Bound

Frederick Dehmel , Shilun Li This is my paper
classification quant-ph cs.ITmath.IT MSC 81P7015A6394B65 PACS 03.67.Pp
keywords Quantum Singleton Boundstabiliser codessymplectic vector spacecleaning lemmaerasure correctiondimension countingformal verificationquantum error correction
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper seeks to establish the Quantum Singleton Bound — the trade-off k+2(d−1)≤n between encoded qubits, distance, and block length — for stabiliser quantum codes using only linear algebra over a symplectic vector space. It argues that a code of distance d corrects erasures of any d−1 positions, and that two disjoint correctable regions force all 2k logical degrees of freedom onto the remaining n−2(d−1) positions. A dimension count then gives k≤n−2(d−1), with no use of entropy, no-cloning, or channel theory. The same argument is formalised in a proof assistant, giving what the authors claim is the first machine-checked proof of the bound.

Core claim

The central claim is Theorem 1: every stabiliser code over a prime field with parameters [[n,k,d]] satisfies k+2(d−1)≤n. The argument rests on two algebraic facts. First, any set of at most d−1 positions is a correctable erasure, meaning the subspace of logical operators supported there is contained in the stabiliser. Second, for any subset M of positions, the count of logical operators supportable on M plus the count supportable on its complement equals 2k — the cleaning dimension identity. With two disjoint correctable sets of size d−1, the identity implies all 2k logical operators can be represented on the complement of their union, a space of dimension 2(n−2(d−1)), so k≤n−2(d−1).

What carries the argument

The central object is the 2n-dimensional symplectic vector space over a prime field whose vectors are Pauli operators modulo phases; a stabiliser code is an isotropic subspace S, and the quotient S⊥/S is the logical operator space. The load-bearing identity is g(M)+g(M^c)=2k, where g(M) counts logical operators (modulo stabilisers) supportable on M. Because erasure correctability of M is equivalent to g(M)=0, the identity converts correctability into the statement that all logical operators live on the complement; the final dimension count is performed by restricting logical operators to the complement of two disjoint correctable sets and showing the restriction is injective.

Load-bearing premise

The proof assumes that a set of positions is a correctable erasure exactly when no nontrivial logical operator is supported inside it — the inclusion S⊥∩V_E⊆S — and every subsequent step passes through that identification.

What would settle it

Find a stabiliser code and a set E of at most d−1 positions for which physical erasure correction succeeds but the inclusion S⊥∩V_E⊆S fails, or vice versa; such a counterexample would break the first lemma and the dimension argument that follows. A small exhaustive search over prime fields, or an explicit counterexample in the formalised model, would settle it.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • The Quantum Singleton Bound for stabiliser codes follows from symplectic dimension counting alone, without entropy inequalities or the no-cloning theorem.
  • The cleaning dimension identity g(M)+g(M^c)=2k holds for every isotropic subspace and every partition of the positions, providing a reusable algebraic lemma for other code-parameter bounds.
  • The formalised proof gives a machine-checked certificate of the linear-algebraic argument, claimed to be the first such certificate for the Quantum Singleton Bound.
  • The proof extends to stabiliser codes over non-prime fields by the same dimension identities, as the authors note.
  • The argument indicates that for additive codes the Singleton bound is a purely dimension-theoretic fact about the symplectic form, not a statistical property of quantum states.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same two-disjoint-correctable-sets template might prove other coding bounds by replacing the distance condition with a different weight function and counting logical degrees of freedom on smaller complements.
  • Because the cleaning identity is a pure statement about isotropic subspaces, it may transfer to related settings such as subsystem codes or quantum memories, where different physical constraints replace the distance threshold.
  • A future automated search over small fields and lengths could stress-test the proof's edge cases, especially the regime n<2(d−1) where the paper handles the bound trivially.
  • The formalisation points toward a broader programme of machine-checking coding-theoretic impossibility results, since the symplectic framework keeps proofs in the discrete linear-algebraic language proof assistants handle well.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper presents an algebraic proof of the Quantum Singleton Bound k + 2(d-1) ≤ n for stabiliser codes over prime fields, using only the symplectic structure of the Pauli group. The argument defines stabiliser codes as isotropic subspaces S of F_p^{2n}, introduces a commutant-based notion of correctable erasure, proves the cleaning dimension identity g(M)+g(M^c)=2k, and then combines two disjoint correctable erasures to conclude k ≤ n-2(d-1). A Lean4 formalisation of the linear-algebraic development is also claimed. For the case n ≥ 2(d-1), the proof is correct and the lemmas are sound. The paper's treatment of the complementary case n < 2(d-1) in Remark 3 is logically inverted and leaves a genuine gap in the proof of Theorem 1 as stated.

Significance. If the proof is completed, the paper gives an elegant, fully algebraic derivation of a fundamental bound, avoiding entropic machinery, and is accompanied by what appears to be a substantial machine-checked formalisation. The cleaning dimension identity and the erasure-correctability argument are cleanly presented and are of independent pedagogical value. However, the paper's central claim "for any [[n,k,d]] stabiliser code" is not fully established by the written proof because of the n < 2(d-1) edge case. The gap is repairable with existing ingredients, and the main mathematical idea is sound, but the manuscript as it stands overstates its completeness and its formalisation coverage.

major comments (2)
  1. [§9, Theorem 1 and Remark 3] The proof of Theorem 1 chooses disjoint A,B with |A|=|B|=d-1, which requires n ≥ 2(d-1). Remark 3 claims that when n < 2(d-1), the right-hand side n-2(d-1) is non-positive and hence the inequality k ≤ n-2(d-1) is automatically satisfied because k ≥ 0. This is backwards: if n-2(d-1) < 0, then k ≤ n-2(d-1) is false for every k ≥ 0. The theorem would be false if such a code existed. The paper does not prove that no such code exists. The gap is fixable: since d ≤ n for any code with k>0, one may choose A of size d-1; then both A and A^c have size at most d-1, so both are correctable by Lemma 4, and Lemma 5 gives 2k = g(A)+g(A^c) = 0, forcing k=0. Thus for k>0 no code with n < 2(d-1) exists, and the bound holds vacuously (with k=0 requiring a convention on distance). This repair uses only lemmas already proved, but as written Theorem 1 is not established for all n.
  2. [Appendix A and Contributions] The formalisation index lists `lemma exists disjoint finsets card` as a helper for the final step, but no formal counterpart of the n < 2(d-1) elimination is listed. If the Lean theorem `quantum singleton bound` only states the bound under the hypothesis n ≥ 2(d-1), then the claims in the abstract and Contributions that the formalisation covers "the Quantum Singleton Bound" and the "main theorem" for any [[n,k,d]] stabiliser code are overbroad. The formal statement and the paper's Theorem 1 must be aligned, either by adding the edge-case argument in Lean or by explicitly stating the theorem with the missing hypothesis.
minor comments (5)
  1. [§4, Remark 1] The main theorem is proved only for prime fields F_p. The Discussion says extension to F_q is straightforward, but the abstract and introduction should state this scope limitation explicitly to avoid implying the full generality of the quantum Singleton bound for all stabiliser codes.
  2. [§6, Definition 6] The equivalence of the commutant condition S^⊥ ∩ V_E ⊆ S with the standard Knill–Laflamme erasure-correction condition is asserted with citations. A short explanatory paragraph deriving this equivalence from the stabiliser error-correction conditions would make the paper more self-contained.
  3. [§7, Lemma 5] In the proof, after choosing S_0, it would help to state explicitly that S_M and S_M^c are linearly independent because they have disjoint supports, so the direct sum decomposition is well-defined.
  4. [§8, Lemma 6] The displayed definition of the induced map has a typo: "L− →VC/r_C(W)" should be "L → V_C/r_C(W)", and the partition statement "A B C" should read "A, B, C".
  5. [§9, Remark 3] Even after the edge-case argument is corrected, the wording should be revised: the correct statement is that no stabiliser code with k>0 exists in this regime, not that the inequality is automatic.

Circularity Check

0 steps flagged

No significant circularity: the derivation is self-contained and does not reduce to its inputs.

full rationale

The paper gives a direct linear-algebraic derivation of the Quantum Singleton Bound for stabiliser codes. The load-bearing identification of erasure correctability with the commutant inclusion S^⊥ ∩ V_E ⊆ S is a standard quoted equivalence ([KL97, NC10]), and it is used as an input, not derived from the target bound. Lemma 4 follows immediately from the definition of distance, Lemma 5 (cleaning dimension identity) is proved inside the paper by a dimension count following Preskill, and Lemma 6 uses only correctability of two disjoint sets plus the cleaning identity. Theorem 1 then combines these with an explicit choice of disjoint sets of size d−1. No fitted parameter is renamed as a prediction, no author's prior result is invoked as a uniqueness theorem, and the formalisation is offered as independent machine-checked evidence. The only notable issue is not circularity: Remark 3 mishandles the n < 2(d−1) regime by claiming the bound is automatically satisfied when the right-hand side is non-positive, whereas the inequality k ≤ n−2(d−1) would be impossible for nonnegative k in that regime; this is a correctness gap in case coverage, not a circular step. Because the central derivation is not equivalent to its inputs and does not rely on self-citation in a load-bearing way, the circularity score is 0.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

The proof introduces no free parameters and no new entities. It rests on the standard symplectic model of stabiliser codes and on the unproved algebraic characterisation of correctable erasures.

axioms (3)
  • domain assumption Stabiliser codes are modelled by an isotropic subspace S of (F_p^{2n}, ⟨·,·⟩) with dim S = n−k; Pauli weight and code distance are read off from S^⊥\S.
    The symplectic model is standard and cited to [CRSS97, CRSS98, Got97]; the paper adopts it rather than proving it (Sections 4–5).
  • domain assumption A subset E is correctable exactly when S^⊥ ∩ V_E ⊆ S.
    Definition 6 asserts equivalence with the Knill–Laflamme conditions and cites [KL97, NC10]; no proof of the equivalence is given, yet every later lemma uses it.
  • standard math Standard finite-dimensional linear algebra over F_p: rank-nullity, orthogonal complement dimension dim U + dim U^⊥ = dim V in a nondegenerate symplectic space, quotient dimensions.
    Used throughout Lemmas 3, 5, and 6 without statement as axioms.

pith-pipeline@v1.3.0-alltime-deepseek · 7872 in / 19669 out tokens · 167890 ms · 2026-08-02T21:53:02.887633+00:00 · methodology

0 comments
read the original 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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Entanglement-Rank Duality in Quadratic Phase Quantum States

    quant-ph 2026-05 unverdicted novelty 7.0

    Entanglement purity in quadratic-phase states over finite fields is exactly determined by the rank of the phase matrix, with AME states existing precisely when all bipartition submatrices have full rank.

Reference graph

Works this paper leans on

9 extracted references · 8 linked inside Pith · cited by 1 Pith paper

  1. [5]

    Nonbinary stabilizer codes over finite fields.IEEE Trans

    [KKKS06] Avanti Ketkar, Andreas Klappenecker, Santosh Kumar, and Pradeep Kiran Sarvepalli. Nonbinary stabilizer codes over finite fields.IEEE Trans. Inform. Theory, 52(11):4892– 4914, 2006.arXiv:quant-ph/0508070. [KL97] Emanuel Knill and Raymond Laflamme. Theory of quantum error-correcting codes. Phys. Rev. A, 55(2):900–911,

    Pith/arXiv arXiv 2006

  2. [7]

    [Rai98] Eric M. Rains. Quantum weight enumerators.IEEE Trans. Inform. Theory, 44(4):1388– 1394, 1998.arXiv:quant-ph/9612015. [Rai99] Eric M. Rains. Nonbinary quantum codes.IEEE Trans. Inform. Theory, 45(6):1827– 1832, 1999.arXiv:quant-ph/9703048. [RCPK18] Narayanan Rengaswamy, Robert Calderbank, Henry D. Pfister, and Swanand Kadhe. Synthesis of logical Cl...

    Pith/arXiv arXiv 1998

  3. [1964]

    [Ste96] Andrew M. Steane. Multiple-particle interference and quantum error correction.Proc. R. Soc. Lond. A, 452:2551–2577, 1996.arXiv:quant-ph/9601029. [Wil09] Mark M. Wilde. Logical operators of quantum codes.Phys. Rev. A, 79:062322,

    Pith/arXiv arXiv 1996

  4. [1997]

    [CRSS98] A

    arXiv:quant-ph/9605005. [CRSS98] A. Robert Calderbank, Eric M. Rains, Peter W. Shor, and Neil J. A. Sloane. Quantum error correction via codes over GF(4).IEEE Trans. Inform. Theory, 44(4):1369–1387, 1998.arXiv:quant-ph/9608006. [CS96] A. Robert Calderbank and Peter W. Shor. Good quantum error-correcting codes exist. Phys. Rev. A, 54(2):1098–1105, 1996.arX...

    Pith/arXiv arXiv 1998

  5. [1999]

    Entropic proofs of Singleton bounds for quantum error-correcting codes.IEEE Trans

    [GHW22] Markus Grassl, Felix Huber, and Andreas Winter. Entropic proofs of Singleton bounds for quantum error-correcting codes.IEEE Trans. Inform. Theory, 68(6):3942–3950, 2022.arXiv:2010.07902. [Got97] Daniel Gottesman.Stabilizer codes and quantum error correction. PhD thesis, Califor- nia Institute of Technology, 1997.arXiv:quant-ph/9705052. [Gra21] Mar...

    Pith/arXiv arXiv 2022

  6. [2001]

    Bennett, David P

    9 [BDSW96] Charles H. Bennett, David P. DiVincenzo, John A. Smolin, and William K. Wootters. Mixed-state entanglement and quantum error correction.Phys. Rev. A, 54(5):3824– 3851, 1996.arXiv:quant-ph/9604024. [BPT10] Sergey Bravyi, David Poulin, and Barbara Terhal. Tradeoffs for reliable quantum infor- mation storage in 2D systems.Phys. Rev. Lett., 104:050...

    Pith/arXiv arXiv 1996

  7. [2009]

    [ZBS+23] Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying

    arXiv:0903.5256. [ZBS+23] Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. CoqQ: Foundational verification of quantum programs.Proc. ACM Program. Lang., 7(POPL):833–865,

    Pith/arXiv arXiv

  8. [2021]

    Efficient formal verification of quantum error correcting programs.Proc

    [HFP+25] Yingte Huang, Li Feng, Anya Paykin, Robert Rand, Yuxiang Deng, and Mingsheng Ying. Efficient formal verification of quantum error correcting programs.Proc. ACM Program. Lang., 9(PLDI), 2025.arXiv:2504.07732. [HRH+21] Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. A verified optimizer for quantum circuits.Proc. ACM Progra...

    arXiv 2025

  9. [2022]

    10 [LZZ+19] Junyi Liu, Bohua Zhan, Shuling Zhu, Shenggang Ying, Tao Feng, and Mingsheng Ying

    arXiv:2204.04699. 10 [LZZ+19] Junyi Liu, Bohua Zhan, Shuling Zhu, Shenggang Ying, Tao Feng, and Mingsheng Ying. Formal verification of quantum algorithms using quantum Hoare logic. InProc. CA V 2019, volume 11562 ofLNCS, pages 187–207,

    Pith/arXiv arXiv 2019