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 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.
We construct three new weight-6 bivariate-bicycle (BB) codes—two [[336,20,12]] codes, inequivalent under the BB presentation symmetries, over Z₂ × Z₈₄ and a [[360,24,12]] code over Z₆ × Z₃₀—and certify exact distance 12 in both the X and Z sectors. They encode 25% and 50% more logical qubits than the best distance-12, weight-6 code reported by IBM's evolutionary search (k = 16) [Cruz-Benito et al., arXiv:2606.02418]. They are also the only ones: a symmetry-reduced enumeration of every connected weight-6 BB code with three-term polynomials, n ≤ 360 and k ≥ 20 eliminates 1,448 of the 1,584 candidates with checked logical operators of weight at most 11, and the remaining 136 presentations fall into three classes under group automorphisms, renormalisation and A ↔ B, represented by the new codes; within the polynomial ansatz of [Bravyi et al., Nature 627, 778 (2024)], every one of the 432 such candidates has distance at most 10. The same certificates settle the distances of the IBM ladder [Bravyi et al., Nature 627, 778 (2024)]—[[72,12,6]], [[90,8,10]], [[108,8,10]], the gross code [[144,12,12]] and the two-gross code [[288,12,18]], both sectors—and certify 19 ≤ d ≤ 24 for [[360,12]], whose distance we establish to be exactly 24 by exhaustive enumeration, resolving the upper bound reported in [Bravyi et al., Nature 627, 778 (2024)]. For the depth-8 syndrome-extraction circuit they certify circuit-level distance exactly 6 for [[72,12,6]] in both memory bases and at least 6 for every other code tested. Certified lower bounds are DRAT refutations for n ≤ 144 and replayable search trees above, whose single pruning lemma is proved in Lean 4; a reader replays any certificate with a standard-library Python verifier plus drat-trim or a 200-line C replayer, without the software that produced it. In a 1.1-million-shot circuit-level benchmark under one frozen BP-OSD decoder, the new codes' block failure probabilities at p = 0.004 are 3.6–6.2 times lower than the gross code's and 3.4–5.6 times higher than the two-gross code's, in both memory bases. Every computation—search, certification, replay and benchmark—ran on one laptop (Apple M3 Pro, 18 GB) with no GPU and no cluster. Contents of the release paper/ — the manuscript (LaTeX source, bibliography and PDF). certificates/ — one manifest per code and sector (<code_id>_<sector>.json), its standard-library Python verifier (verify_qec_<code_id>_<sector>.py), the proofs in proofs/ (DRAT proofs and gzipped proof trees), the problem files and C source of the tree replayer, the Lean 4 minimality lemma (qec_minimality.lean), the weight-6 envelope witnesses with their checkers, the distance table, FORMAT.md (the certificate format) and REPLAY.md (a clean replay of every certificate: 44 of 44 pass). simulation/ — the projected detector error models, the BP-OSD and BP-LSD evaluation scripts, every 2,000-shot chunk record with its seed, the decoder-tuning grid and the joint-model controls. SHA256SUMS — the SHA-256 of every file. Verification In certificates/: python3 verify_qec_<code_id>_<sector>.py rebuilds the code from its polynomials, checks the logical basis by rank, regenerates every CNF or problem file byte for byte and replays the proof; its last line is the verdict. DRAT rows need drat-trim (set DRAT_TRIM); tree rows need a C compiler. The Lean lemma checks with lake env lean qec_minimality.lean in a project with the pinned Lean 4 v4.33.1 and Mathlib 0df444a3 (exit status 0). Integrity: shasum -a 256 -c SHA256SUMS. Hardware Every computation — search, certificate production, replay and the benchmark — ran on one MacBook Pro (Apple M3 Pro, 11 CPU cores, 18 GB memory, macOS 15.5), with no GPU and no cluster. License: Licensed by SmartLedger Solutions under CC BY-NC 4.0 (LICENSE.md). Commercial use requires a written license from SmartLedger Solutions (labs@smartledger.solutions). The certificate producer is proprietary and not distributed; verification does not need it.
Bivariate bicycle (BB) codes of Bravyi \emph{et al.}~\cite{Bravyi2024} are quantum low-density parity-check codes with weight-6 checks, exemplified by [[144,12,12]] with kd2/n=12. We develop the algebraic structure theory of BB-type codes with weight-8 checks (weight-4 generator polynomials) and use it, together with an exactly validated search pipeline, to construct and certify new codes. We prove an exact dimension formula k=2dimR/(A,B) (forcing even k), a 4ℓm-element symmetry group on generator pairs, an X/Z distance equality dX=dZ, and a family of subgroup-coset kernel vectors giving rigorous distance upper bounds and a design rule for high-distance constructions; all distances are computed exhaustively by a cross-validated bit-mask verifier. At n=144 the pipeline returns a census of 53 codes whose strongest members surpass the BB benchmark: [[144,6,d≥15]] exceeds the benchmark distance 12 (certified d≥15), [[144,10,12]] reaches it with weight-8 checks, and [[144,16,10]] encodes a third more logical qubits at kd2/n=11.11 (7.4% below benchmark) while decoding no worse. At n=72, [[72,14,8]] attains kd2/n=12.44---more than twice the same-length BB code---and decodes better; a circuit-level memory experiment places our weight-8 codes at ≈0.1% pseudo-threshold versus ≈0.4% for the BB reference under an identical model, quantifying the threshold cost of the heavier checks. All structural statements are verified numerically on the whole census.
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.
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.
Quantum error correction protects quantum information by encoding it in a code described by three numbers: how many physical qubits it uses, how many logical qubits it protects, and the smallest error it cannot detect. The last is an optimum over exponentially many candidates, so it is read off a solver rather than checked. Here we show that code parameters can be certified by a short certificate, a list or a pairing or a symbolic instance, whose correctness the kernel of a proof assistant decides by computation, and whose size is itself a theorem rather than an estimate. Two published code families have distances settled here: the bivariate bicycle code's [[144,12,12]], certified, and the affine-permutation codes printed at [[1152,580,≤12]] and [[2304,1156,≤14]], settled at twelve and fourteen. Eleven code families and thirty-nine parameter sets follow, with nothing beyond three standard axioms trusted and the pipeline's specification step preset to twenty columns.
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).