We determine the exact minimum distance of a two-block quasi-cyclic CSS quantum LDPC code with n = 832 physical qubits and k = 10 logical qubits (genus5 GB CLEAN, QECTOR artifact lineage). Earlier releases had established 10 β€ d β€ 15. We prove d = 15: in each CSS sector the classical kernel contains no nonzero word of weight 1 to 14 and exactly 416 words of weight 15, forming a single orbit under simultaneous cyclic shifts, all of them nontrivial logical operators. The proof uses the repeated-root structure of the kernel over F2[x]/(x^416 + 1): since 416 = 13Β·2^5 and x^(2m) + 1 = (x^m + 1)^2 over F2, the kernel folds exactly to a 26-bit code and lifts back without loss, giving an exact, symmetry-reduced enumeration of low-weight words. An 18-check validation suite passes, a separately written re-implementation reproduces every intermediate count, and both implementations show that no kernel word has weight 16 to 20. Computer-assisted proof, not formally verified. Version 2.1 supersedes version 1.0 (version 2.0 was an internal revision, not released). Changes: summary box, notation table, algorithm listing and pipeline figure; narrower novelty statement, related-work section and 20 additional references, independent re-implementation, extended enumeration to weight 20, full re-run for bundle release 1.2.2, corrected availability statement. Results unchanged. The code specification is published in Appendix C, and the verification bundle, with machine-checked proofs of the upper bound, is public (doi:10.5281/zenodo.23463892).
We determine the exact minimum distance of a two-block quasi-cyclic CSS quantum LDPC code with n = 832 physical qubits and k = 10 logical qubits (genus5 GB CLEAN, QECTOR artifact lineage). Earlier releases had established 10 β€ d β€ 15. We prove d = 15: in each CSS sector the classical kernel contains no nonzero word of weight 1 to 14 and exactly 416 words of weight 15, forming a single orbit under simultaneous cyclic shifts, all of them nontrivial logical operators. The proof uses the repeated-root structure of the kernel over F2[x]/(x^416 + 1): since 416 = 13Β·2^5 and x^(2m) + 1 = (x^m + 1)^2 over F2, the kernel folds exactly to a 26-bit code and lifts back without loss, giving an exact, symmetry-reduced enumeration of low-weight words. An 18-check validation suite passes, a separately written re-implementation reproduces every intermediate count, and both implementations show that no kernel word has weight 16 to 20. Computer-assisted proof, not formally verified. Version 2.1 supersedes version 1.0 (version 2.0 was an internal revision, not released). Changes: summary box, notation table, algorithm listing and pipeline figure; narrower novelty statement, related-work section and 20 additional references, independent re-implementation, extended enumeration to weight 20, full re-run for bundle release 1.2.2, corrected availability statement. Results unchanged. The code specification is published in Appendix C, and the verification bundle, with machine-checked proofs of the upper bound, is public (doi:10.5281/zenodo.23463892).
We determine the exact minimum distance of a two block quasi cyclic CSS code with 832 physical and 10 logical qubits. Earlier work had shown 10 β€ d β€ 15. We close the interval and prove d = 15. In each CSS sector the classical kernel has no nonzero word of weight 1 to 14 and exactly 416 words of weight 15, one orbit under cyclic shifts, all of them nontrivial logical operators. The proof uses the identity x^(2m) + 1 = (x^m + 1)^2 over GF(2). Since 416 = 13 Β· 2^5, the kernel folds down to a 26 bit code and lifts back exactly, so all low weight words can be enumerated level by level in about one second per sector. The paper gives the full proofs, the results, an 18 check validation suite, and the limits: this is a computer assisted proof, not a formally verified one. The code matrices and source files are not part of this record. They are held in a separate restricted record [restricted record link], and SHA256 digests in the paper pin every file.
We give an exact method for enumerating every codeword of weight at most W in the kernel of a block matrix over S[x]/(xM+1), where S is a commutative GF(2)-algebra with a fixed basis and M = m0Β·2L. The class contains quasi-cyclic codes of any index, block-circulant matrices with several block rows, generalized and bivariate bicycle codes, and two-block group-algebra codes over abelian groups with a cyclic factor of order m0Β·2L. The method rests on x2m+1 = (xm+1)2 in characteristic two: the kernel folds onto half the length without increasing weight, and every low-weight word is recovered exactly from its fold. The paper proves the recursion in this generality, reduces it to one representative per symmetry orbit, specifies the lift step in full, proves every implementation step and the whole algorithm correct, gives a dimension formula (k = 2 deg gcd(ru, rv, xm+1) for two-block CSS codes) and a certified-distance procedure for CSS codes, degenerate ones included, with certificates checkable by a proof assistant, and a random-code heuristic that predicts where the cost concentrates. A worked [[24,4,4]] example and a case study at length 832 are included: the method certifies d = 15 for a [[832,10]] code in about one second per sector, three separately written implementations agree, and the dimension formula explains the whole tower and proves k = 10. Code. The reference implementation, the tests and the example scripts are in the companion record doi:10.5281/zenodo.23466024. Related records. Case study paper v2.1: doi:10.5281/zenodo.23466181 (version 1.0: doi:10.5281/zenodo.23327681). Verification bundle 1.2.2: doi:10.5281/zenodo.23463892. License. CC BY 4.0. Copyright (c) 2026 Guillaume Lessard.
Bivariate bicycle (BB) quantum codes are a prominent finite-length family of quantum low-density parity-check codes, but their minimum distance is usually established numerically rather than read from the defining polynomials. We study the Z-logical quotient K/S over F2β[x,y]/(xββ1,ymβ1) and show that it fits into a short exact sequence with an annihilator quotient as kernel and a colon quotient as cokernel. The sequence gives an explicit logical basis, a dimension formula, and a componentwise distance identity dZβ=min(dAβ,dCβ). Using the Frobenius structure of the finite group algebra, we prove rAβ=rCβ=k/2 for every BB code, including repeated-root cases. The algebraic component of a logical class is distinct from the support shape of its lightest representatives: an annihilator class can have a lighter two-block representative, and a colon class can have a one-sided minimum. For lower bounds we show that every proper subset of a minimum-weight logical operator has nonzero syndrome, and that this property persists inside the colon component but not inside the annihilator component. A translation-anchored cluster search built on it proves the distances 4,6,10,10,12,18 of the six standard BB codes of lengths 18 to 288 and enumerates every minimum-weight logical operator. The resulting census shows that [[108,8,10]] is the only one of the six whose distance is attained in a single component, with dCβ=10 and dAβ=12.
Computing the minimum distance of a quantum LDPC code is easy in one direction and expensive in the other: exhibiting a light logical operator is a search, while proving that no lighter one exists is what actually decides the parameter. This note proves an orbit reduction for the second half. If a group of code automorphisms acts on the qubits with r orbits, the minimum distance is the smallest of r restricted problems, one per orbit representative, so the number of solver calls is the number of orbits and not one. We give the a priori condition under which restricting to a single qubit is legitimate, namely transitivity on all qubits, and a counterexample showing what happens without it: on a hypergraph product code with n = 27 and d = 3, the widely used tool dist-m4ri prints a pair of equal bounds, which its own documentation calls a confirmed exact distance, and that value is 6. The reduction is coupled to a proof producing pipeline in which every nonexistence claim is re-verified by an independent checker, drat-trim or, for the largest closure, cake_lpr, whose soundness is proved inside CakeML. This closes with replayable certificates the distances of the five smaller bivariate bicycle codes of Bravyi et al., up to and including the code with n = 288 and d = 18, whose exactness was published with no replayable artifact and is established here at both ends. For the two larger codes it yields the first lower bounds a third party can re-check from the deposited files: d at least 18 for the code with n = 360, against a published upper bound of 24 and against d at least 11 for the best previously re-executable method, and a first lower bound of any kind for the code with n = 756. A separate and much cheaper ingredient, a sweep over logical operators supported on unions of cosets of a subgroup, tightens two upper bounds printed in a recent table of two block group algebra codes. The code printed there as [[140, 8, at most 16]] carries a logical operator of weight 14; the code printed as [[144, 10, at most 16]] has distance exactly 12, established at both ends and so closed four below the published bound. Both witnesses are re-checked outside any solver by two rank computations over the field with two elements, so neither of these two upper bounds rests on a solver at all. Both entries are printed with the inequality sign in that reference, which states no method for the tables they sit in; nothing it proves is contradicted here, and no error of its authors is corrected. What is improved are two bounds they offered as bounds. Finally we show that the two instance form of the reduction is a consequence of commutativity and not of the two block structure. On two block group algebra codes over non-abelian groups, taken from the published catalogue, the translation subgroup has two orbits for one code and twelve for another, so the number of solver calls has to be computed from the group before any search rather than assumed. On three such codes we certify the minimum distance. The argument that makes one orientation enough in the abelian case does not apply there, and we check that it does not, so both orientations are certified separately rather than assumed equal; on these three codes the two turn out to coincide, which is a measured fact about each code and not a consequence of that argument. The published values for these codes come from randomised search, and a certificate of nonexistence a reader can replay is, to our knowledge, new for non-abelian codes of this family. What this work does not claim is stated explicitly in the note: the restriction itself is not our idea, it is an option of dist-m4ri present since 2020; a machine checkable chain covering a symmetry breaking step is not a first; our proofs are checked by an independent checker and not by the kernel of a proof assistant; and the encoding step is not formally verified. A public question asking whether the orbit reduction is already in the literature was posted on MathOverflow on 28 August 2026 and carried no answer at the time of deposit. Every table of numbers in the note is generated from the deposited artifacts by a script that refuses to emit a row it cannot source. 27 pages. Verification scripts and certificate digests included as separate archives. MSC 2020: 81P73, 94B05, 68Q25, 20C05.
Computing the distance of a stabilizer code is NP-hard, yet certifying the distance of a given code needs no search at all β only two one-sided certificates that meet. An upper bound is a single explicit logical operator: one vector, checked in milliseconds against the actual check matrix β it commutes with every stabilizer, it is provably outside their span, and it acts on exactly w qubits. A lower bound is a universal statement β no logical operator lives below weight w β discharged by a finite scan whose completeness is itself a theorem, not a convention: a reconstruction lemma proves that every light Pauli vector appears in the scanned list, so the scan quantifies over the whole space rather than over a table someone chose. When the two certificates touch, the distance is exact, and the receipt can be replayed by a referee who trusts neither the authors nor their software. We build this bracket calculus over the binary symplectic carrier, close it exactly on the classical menagerie β the five-qubit perfect code, Steane, Shor, the distance-three rotated surface code, and the 3 Γ 3 toric code β and report an instructive refutation: our own frozen reference data claimed distance at least 2 for a punctured code fragment, and the certificate layer produced an explicit weight-one logical operator. Puncturing buys a logical qubit and leaves it bare; the count and the distance are independent shadows of the same subgroup lattice. The same prover-proposes/kernel-disposes architecture certifies logical counts at bivariate-bicycle scale (k = 12 at n = 144) from change-of-basis rank certificates checked in linear time, and every number in the system wears a two-valued trust badge whose semantics is an event, not a citation: no kernel run on your instance, no badge. The results are proved in a machine-checked formal kernel. Published by The Institute for Applied Ontological Mathematics.