Bravyi et al. conjectured that their depth-8 syndrome cycle for the [[144,12,12]] gross code has circuit distance 10. We prove it. In their noise model and for every number of noisy cycles, no set of nine or fewer faults causes an undetected logical error of either Pauli type, and we give explicit ten-fault logical errors of both types. When we released our data on 15 October 2026, the best reported bounds for X-type faults were 9 ≤ d_circ ≤ 12, at 12 rounds; since then, Crocker and Pan have reported the value 10 in both bases, for 12 noisy cycles and for every number of cycles up to 12, respectively. For the same family of circuits we show that the [[90,8,10]] and [[108,8,10]] cycles have circuit distance 8 for every number of cycles, extending values reported for fixed numbers of rounds; for [[72,12,6]] we confirm the known value 6. We also find that, for three of these codes, Google's Tesseract test circuits have the same detector-error-model columns as the depth-8 cycle once restricted to the detectors of the memory basis, for every number of rounds we checked, so circuit-distance results carry over between the two at those round counts. The lower bounds combine 607 SAT refutations, each with a DRAT proof, with exhaustive enumerations of extended-code logicals that carry no certificate. Finally, we independently confirm two results that others reported first: the [[360,12]] bivariate bicycle code has distance 24, and the left-right gross-code circuit of Strikis, Browne and Beverland, as reconstructed from their figures, has circuit distance 11. All code, formulas, proofs and fault sets are available at doi:10.5281/zenodo.23394575.
Bravyi et al. conjectured that their depth-8 syndrome cycle for the [[144,12,12]] gross code has circuit distance 10. We prove it. In their noise model and for every number of noisy cycles, no set of nine or fewer faults causes an undetected logical error of either Pauli type, and we give explicit ten-fault logical errors of both types. When we released our data on 15 October 2026, the best reported bounds for X-type faults were 9 ≤ d_circ ≤ 12, at 12 rounds; since then, Crocker and Pan have reported the value 10 in both bases, for 12 noisy cycles and for every number of cycles up to 12, respectively. For the same family of circuits we show that the [[90,8,10]] and [[108,8,10]] cycles have circuit distance 8 for every number of cycles, extending values reported for fixed numbers of rounds; for [[72,12,6]] we confirm the known value 6. We also find that, for three of these codes, Google's Tesseract test circuits have the same detector-error-model columns as the depth-8 cycle once restricted to the detectors of the memory basis, for every number of rounds we checked, so circuit-distance results carry over between the two at those round counts. The lower bounds combine 607 SAT refutations, each with a DRAT proof, with exhaustive enumerations of extended-code logicals that carry no certificate. Finally, we independently confirm two results that others reported first: the [[360,12]] bivariate bicycle code has distance 24, and the left-right gross-code circuit of Strikis, Browne and Beverland, as reconstructed from their figures, has circuit distance 11. All code, formulas, proofs and fault sets are available at doi:10.5281/zenodo.23394575.
For the bivariate bicycle code [[288,12,18]] ("two-gross"), with the depth-8 syndrome-extraction cycle of Bravyi et al. (arXiv:2308.07915), this deposit gives explicit sets of 16 circuit faults that trigger no detector and apply a nontrivial logical operator. They exist for Z-type and X-type faults and under both readings of the CNOT term labels. One of them lies entirely inside the noise model and memory layout of Beverland et al., "Fail fast" (arXiv:2511.15177: Z-type noise, 18 noisy cycles and one fault-free cycle), whose search reported a lowest weight of 18. So the circuit distance of this cycle is at most 16. No lower bound is claimed, and no claim is made about logical error rates. Contents. A two-page note; the four fault sets listed gate by gate (cycle, timestep, gate, qubit coordinates, Pauli) so they can be checked by hand; a standalone checker (Python 3 + numpy) that builds the code and cycle from the polynomials and replays each set; tamper controls; logs. Checks. Two separately written circuit builds (one written from the papers only) reproduce the matrix sizes in Fail fast, Table 1, and agree on all four sets at cycles 1, 9 and 18; the gate order and indexing were checked against the text of the public BivariateBicycleCodes repository (inspected, not executed). A third propagator, written from the fault table and the papers only, is included. Removing any single fault makes detectors fire in every case tested. Use of AI. The author is not a professional researcher. The search, checks and drafting were carried out by AI models (Anthropic's Claude via Claude Code; OpenAI's ChatGPT as a reviewer) under the author's direction. The author is responsible for the content. No human expert has reviewed the work to date. Corrections are welcome.
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.
We present an analytical theory of greedy peeling decoding for bivariate bicycle (BB) codes under circuit-level noise. The deferred greedy decoder achieves 330x latency reduction over belief propagation (BP) at p = 10^{-3} while maintaining identical logical error rate. Our main theoretical contribution is a closed-form collision resolution factor A_0 = |true collisions| / |birthday collisions|, derived from XOR syndrome analysis with no free parameters, that quantifies the fraction of detector-sharing fault pairs genuinely blocking iterative peeling. For the [[144,12,12]] Gross code, A_0 = 0.8685 (within 0.5% of the empirical value), with shared-2 pairs (4-cycles) always resolving under peeling. We show A_0 depends on the mean fault-graph degree d-bar rather than code size: A_0 = 0.87 for d-bar = 52 (Gross family) versus A_0 = 0.76 for d-bar = 17 ([[32,8,6]]). We establish a syndrome code stopping distance d_S = n/4.5 for the Gross family and demonstrate that [[32,8,6]] (d_S = 4) enables two-shot streaming decoding: T = 2 rounds achieve 89% peeling success with 1.29 +/- 0.03 LER ratio versus T = 12, at estimated latency ~50 ns. The full formula P_peel = exp(-A_0 * gamma_analytic * exp(-BTp) * n * p^2) is validated across five BB codes, four noise levels, and four values of T with R^2 = 0.86. Cross-platform reproduction of the Kunlun [[18,4,4]] experiment matches their hardware LER within 0.73 percentage points.
The distance of a classical or quantum code is a key figure of merit which reflects its capacity to detect errors. Quantum LDPC code families have considerable promise in reducing the overhead required for fault-tolerant quantum computation, but calculating their distance is challenging with existing methods. We generally assess the performance of a quantum code under circuit level error models, and for such scenarios the circuit distance is an important consideration. Calculating circuit distance is in general more difficult than finding the distance of the corresponding code as the detector error matrix of the circuit is usually much larger than the code's check matrix. In this work, we benchmark a wide range of distance-finding methods for various classical and quantum code families, as well as syndrome-extraction circuits. We consider both exact methods (such as Brouwer-Zimmermann, connected cluster, SAT and mixed integer programming) and heuristic methods which have lower run-time but can only give a bound on distance (examples include random information set, syndrome decoder algorithms, and Stim undetectable error methods). We further develop the QDistEvol algorithm and show that it performs well for the quantum LDPC codes in our benchmark. The algorithms and test data have been made available to the community in the codeDistance Python package.
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.
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.