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.
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.
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.
Quantum error-correcting codes (QECCs) sit between noisy quantum hardware and reliable computation, so the code parameters used in practice must be trustworthy. The single number that summarizes a code's strength is its distance, yet certifying a distance lower bound is NP-hard in general, placing it beyond the reach of pen-and-paper proofs as well as direct proof-assistant scripting. As a result, distance values in the literature come either from non-scaling hand proofs, or from unverified solvers that leave a trust gap exactly where the code is supposed to provide a guarantee. We present Lean-QEC, the first Lean 4 formalization of stabilizer-code theory that delivers end-to-end, machine-checked distance certificates at industrial code sizes. Lean-QEC formalizes the linear algebra of qubit states, the Pauli group, stabilizer codes, the binary symplectic representation, classical coding theory, and the CSS and Bivariate Bicycle families. To break the combinatorial barrier, Lean-QEC translates the distance condition into a Boolean satisfiability formula through a verified reduction. The pipeline scales through a BitVec-flattened encoding that replaces Lean's Matrix representation, and an error-location encoding that reduces the variable count from n to k⌈log2n⌉. With these, we obtain automatically-generated Lean-checked distance proofs for a large range of industrially viable qLDPC codes within the Bivariate Bicycle and Generalized Bicycle families, including [[90, 8, 10]] and [[70, 6, 9]] BB codes, with the formulation scaling up to 144 qubits when performed outside the Lean kernel. The resulting library is reusable and is designed to plug into broader Lean-based efforts toward end-to-end verification of fault-tolerant quantum computation.
A CSS quantum error-correcting code is, on the nose, a length-three chain complex over F2 : the commutation law HZ H⊤ X = 0 that makes the code valid is exactly the condition ∂ 2 = 0 that makes a chain complex. We take this identification literally and show that the entire working theory of a quantum code is one homological object the same engine computes, at scale, and certifies. The number of logical qubits is the first Betti number, k = dim H1 = n − rank HX − rank HZ = b1 ; the code distance is the systole, the shortest non-contractible cycle. We reproduce the published parameters of state-of-the-art codes exactly—the toric and hypergraph-product families and the IBM bivariate-bicycle codes [[72, 12, 6]], [[144, 12, 12]], [[90, 8, 10]]—cross-validated four independent ways and kernelcertified for the small cases in Cubical Agda, on CPU and GPU. The two scale certificates—the Betti count b1 and the rank-derived logical count k—are themselves kernel-proved to be a single first-homology certificate (a DescentCertificate both readings factor through), closed terminally through a fixed-point engine. We then run the code, not just measure it. (i) The Union-Find decoder is the engine's connected-components reduction, and "a logical error occurred" is the engine's coboundary decision (the residual cycle has nonzero winding); decoding the toric code at growing distance recovers the accuracy threshold near 9.5%, and the optimal (maximum-likelihood) threshold near 11% is the engine's two homology sectors competing as the domain-wall free energy of a random-bond Ising model on the Nishimori line. (ii) A code's distance scaling is its Tanner-graph spectral expansion: the second eigenvalue λ2 versus the Ramanujan bound is a computable certificate (Sipser–Spielman), exact on the topological tier where the spectral gap obeys γ d2 → 4π 2 . (iii) The full chain complex carries metachecks—redundancies among the parity checks—and we compute them: the bivariate-bicycle codes have six, the engines of single-shot error correction; the 4-dimensional toric code's homology (1, 4, 6, 4, 1), with k = b2 = 6, is the tensor of four circle complexes. (iv) The logical error-rate prefactor is the multiplicity of the systole, A = 2L for the toric code, which we compute exactly. (v) Finally the engine measures a topological phase transition: as random noise thickens, torus-wrapping "giant" cycles appear in a sharp homological-percolation transition at pc ≈ 0.5 that sharpens with system size—the same homology machinery now detecting when noise spontaneously writes a logical operator. (vi) The engine runs over any coefficients: qudit (Fp ) codes are chain complexes over Fp , and the integral homology, computed by the Smith normal form, exposes torsion—so a code's logical-qudit count can depend on the qudit dimension, an extra logical appearing exactly when p divides a torsion coefficient (reproducing the known homology of the torus, the Moore spaces, the Klein bottle, and RP2 ). We are careful to fence what is not claimed: minimum distance is NP-hard in general and we compute it only on the systolic tier; the giant-cycle transition is the random-cluster one, distinct from the maximum-likelihood decoding threshold of the random-bond Ising model. The thesis is singular and operational: a quantum code's parameters, its decoder, its quality, its higher-dimensional structure, its performance prefactor, and its phase transition are not six theories but one—homology you can run. Published by The Institute for Applied Ontological Mathematics.
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.
Four questions sit at the base of fault-tolerant quantum computing: whether a code with given parameters can exist, whether two circuits denote the same operation, how much entropy a measurement irreversibly produces, and whether a compiled gate still means what it should. They are normally answered by four disjoint techniques. We show they are one technique. In each case the answer is an invariant—the object a governing transformation leaves fixed—and that invariant can be held as a certificate a proof kernel checks and an operator-native substrate computes. The instruments are the quantum weight enumerator, whose shadow variant yields what is, to our knowledge, the first machine-checked nonexistence certificate for a quantum error-correcting code (no pure [[4, 1, 3]] stabilizer code, reduced to an integer impossibility); the spider normal form, unique both as a linear map and as a content-addressed tree, at the minimal axiomatic footprint of a proof assistant; the measurement boundary defect, whose logical entropy equals a kernel-counted cohomology dimension; and the reduction receipt, round-tripping a certified gate word to bare metal on two independent substrates. Everything downstream of the explicitly labelled modeling step in each domain is exact integer or rational arithmetic. The common shape—find the invariant the transformation fixes, and read it off as a certificate—turns four hard quantum questions into arithmetic a machine can hold. Published by The Institute for Applied Ontological Mathematics.
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.