{"id":"94f64f65-230a-4979-a6a3-c20aff82c872","arxiv_id":"2602.20186","paper_version":3,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The quantum Singleton bound k+2(d−1)≤n for stabilizer codes is derived from erasure correctability and the cleaning lemma, and formalized in Lean4.","lead":"A new proof of the known quantum Singleton bound for stabilizer codes, built on symplectic dimension counting and the cleaning lemma, with a companion Lean4 formalization. The main value is a machine-checked version of a standard coding-theory result, though the mathematics itself is not new.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1 is only proved for n ≥ 2(d−1); Remark 3's handling of n < 2(d−1) is logically inverted, leaving the proof incomplete for that regime.","rationale":"The reader's weakest_assumption pointed to Definition 6 (the commutant-form erasure correctability condition), but that condition is standard and correct: for Pauli stabilizer codes, erasure of E is correctable iff no nontrivial logical operator is supported on E, i.e., S^⊥ ∩ V_E ⊆ S. Lemma 4 and Lemma 6 pass through it validly. The genuinely load-bearing gap is the mishandled n < 2(d−1) edge case. The proof of Theorem 1 only works when n ≥ 2(d−1) because it needs two disjoint sets of size d−1; Remark 3's claim that the bound is automatically satisfied when n−2(d−1)<0 is logically inverted—k ≥ 0 does not make k ≤ negative true. This is a real incompleteness in the proof as written, even though the underlying theorem is true and the gap is patchable. The reader's verdict CONDITIONAL is appropriate, but for this reason, not for the Definition 6 equivalence. Since the reader already assigned CONDITIONAL, our read does not change the verdict.","tokens_in":8106,"tokens_out":18242,"duration_ms":142135,"concrete_test":"Independently verify Remark 3 with a concrete parameter set, e.g., n=3, d=3: the bound requires k≤−1, which is impossible for any k≥0, directly contradicting the remark's assertion that the bound is automatically satisfied. Then check whether the symplectic proof can be patched by showing that if n<2(d−1), the existence of a logical operator of weight d with support A and a correctable complement B=[n]\\A of size n−d forces a contradiction via the cleaning lemma. If no such code exists, the theorem is safe but the paper still needs a valid argument for this case.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The proof of Theorem 1 selects disjoint A,B⊆[n] with |A|=|B|=d−1, which requires n≥2(d−1). Remark 3 attempts to cover n<2(d−1) but argues that since k≥0, the bound k≤n−2(d−1) is automatically satisfied when the RHS is non-positive. This is backwards: if n−2(d−1)<0, then k≤n−2(d−1) is false for every k≥0, so the theorem's inequality is not automatically satisfied; rather, such a code would violate the bound. The correct resolution is that no [[n,k,d]] stabilizer code with k≥1 can have n<2(d−1), but the paper does not prove this. Thus the proof as written does not establish the theorem for all stabilizer codes. The formalisation cannot fill this gap, as Appendix A lists `exists disjoint finsets card` only for the n≥ case.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":8347,"tokens_out":7046,"duration_ms":62641,"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":[{"comment":"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.","section":"§9, Theorem 1 and Remark 3"},{"comment":"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.","section":"Appendix A and Contributions"}],"minor_comments":[{"comment":"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.","section":"§4, Remark 1"},{"comment":"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.","section":"§6, Definition 6"},{"comment":"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.","section":"§7, Lemma 5"},{"comment":"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\".","section":"§8, Lemma 6"},{"comment":"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.","section":"§9, Remark 3"}],"recommendation":"major_revision","confidential_remarks":"The core algebraic argument is correct in the n ≥ 2(d-1) regime, and the flaw in Remark 3 is genuinely load-bearing for the stated theorem. However, the gap is local and can be closed with a short argument already implicit in the paper's lemmas, so rejection is not warranted. I recommend major revision, with the authors required to fix the edge case in both the informal proof and the formalisation claim."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe headline: this is a clean, self-contained symplectic re-derivation of a long-known theorem, with a Lean4 formalisation that is the genuinely new artifact. The proof for n ≥ 2(d−1) is correct: Lemmas 4–6 check out, and the dimension argument in Lemma 6 is sound. The citations are appropriate — the cleaning lemma is credited to Preskill's notes, and the KL97/NC10 attributions are right. The writing is clear.\n\nThe soft spot is real and it is exactly what the stress-test note says. Remark 3's handling of n < 2(d−1) is logically inverted. A non-positive right-hand side in k ≤ n−2(d−1) does not make the inequality 'automatically satisfied' for k≥0; it makes it false for every k≥0. The theorem may still be true in that regime (vacuously, if no such code exists), but the paper does not prove it. The formalisation cannot fill the gap: Appendix A lists an existence lemma for disjoint sets only under the n≥2(d−1) hypothesis, so the machine-checked proof likely carries the same restriction.\n\nSecond issue: the formalisation is not shipped. No repository link beyond a bare 'TCSlib/CodingTheory/QuantumSingleton.lean', no commit hash, no code listing. For a claim of 'first machine-checked proof', that is a reproducibility failure. A referee should be able to run or at least inspect the Lean files.\n\nAlso set expectations: this is not a new result. The bound is Knill–Laflamme/Bennett et al.; the entropic proofs are standard. The symplectic proof is a nice reformulation, but it is essentially the cleaning-lemma argument dressed in symplectic language. The value is in the formalisation, if it can be verified.\n\nGiven the gap in the proof text and the missing code, I would not cite this myself yet. But I would send it to peer review: the main argument is correct and the formalisation, if real, is a modest but genuine contribution to formal verification of quantum information. The right referee could quickly confirm the edge-case fix and demand the code.\n\nRecommendation: conditional acceptance — require the edge case to be resolved and the Lean files released.","headline":"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.","tokens_in":8801,"tokens_out":3797,"would_cite":false,"duration_ms":34161,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["81P70","15A63","94B65"],"pacs":["03.67.Pp"],"model":"deepseek-v4-flash","headline":"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.","keywords":["Quantum Singleton Bound","stabiliser codes","symplectic vector space","cleaning lemma","erasure correction","dimension counting","formal verification","quantum error correction"],"falsifier":"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.","tokens_in":8005,"feed_emoji":"🧮","tokens_out":7862,"duration_ms":61420,"temperature":0.7,"pith_summary":"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.","feed_headline":"Symplectic dimension count proves quantum Singleton bound","feed_subtitle":"A purely algebraic argument replaces entropy-based proofs for stabiliser codes, and a machine verifies every step.","key_machinery":"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.","core_discovery":"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).","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["Symplectic count proves quantum Singleton bound","Machine-checked symplectic proof of Singleton bound","Quantum Singleton bound via symplectic algebra alone","Stabiliser codes: symplectic dimension count seals bound","Lean4 formalises symplectic Singleton bound proof"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Symplectic count proves quantum Singleton bound","Machine-checked symplectic proof of Singleton bound","Quantum Singleton bound via symplectic algebra alone","Stabiliser codes: symplectic dimension count seals bound","Lean4 formalises symplectic Singleton bound proof"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000608,"raw_usage":{"total_tokens":2629,"prompt_tokens":665,"completion_tokens":1964,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":409,"completion_tokens_details":{"reasoning_tokens":1899}},"tokens_in":409,"tokens_out":1964,"duration_ms":14325,"temperature":1.0,"reasoning_tokens":1899,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T21:53:02.887633+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}