We prove an exact distance law for 3-fold cyclic covers of lifted-product quantum LDPCcodes over Z3m: a CRT splitting of the cover kernel yields a weight-tracking bijection underwhich the cover distance is d3m = minw,z [ 3 wt(w) − 2(|supp z ∩ supp w| − |supp z \ supp w|) ],the minimum running over nontrivial base logicals w and elements z of an explicitly computabletwisted (F4) kernel. To our knowledge this is the first exact (rather than two-sided) distancelaw for a lift tower of quantum codes. The law reduces cover-distance computation to base-levelcost, identifies sections (zero-cost lifts of base logicals) as the binding mechanism, and recaststower distance growth as section scarcity, an exactly computable per-seed invariant. Combinedwith a chain-map floor-propagation theorem, one exact certification at n = 288 floors an entiretower. We report a weight-6 [[288, 12, 12]] code certified exactly by two independent solverstacks; complete weight-12 and weight-14 logical censuses of its [[864, 12]] lift proving d ≥ 16modulo three named, separately retirable trust assumptions (with d ≤ 36 by exact witnesses);a [[2592, 12]] level with certified floor 12; fully certified constant-distance control towers; and alift-portfolio result: distance verdicts are per-lift, with section structure provably varying acrossthe admissible lift space while k is preserved. A further contribution is methodological: anevidence-graded certification discipline (per-class SAT censuses run to UNSAT with retainedartifacts, known-answer gates, pre-registered readings, and theorems encoded as constraints) inwhich every reported number carries its grade.
We prove an exact distance law for 3-fold cyclic covers of lifted-product quantum LDPCcodes over Z3m: a CRT splitting of the cover kernel yields a weight-tracking bijection underwhich the cover distance is d3m = minw,z [ 3 wt(w) − 2(|supp z ∩ supp w| − |supp z \ supp w|) ],the minimum running over nontrivial base logicals w and elements z of an explicitly computabletwisted (F4) kernel. To our knowledge this is the first exact (rather than two-sided) distancelaw for a lift tower of quantum codes. The law reduces cover-distance computation to base-levelcost, identifies sections (zero-cost lifts of base logicals) as the binding mechanism, and recaststower distance growth as section scarcity, an exactly computable per-seed invariant. Combinedwith a chain-map floor-propagation theorem, one exact certification at n = 288 floors an entiretower. We report a weight-6 [[288, 12, 12]] code certified exactly by two independent solverstacks; complete weight-12 and weight-14 logical censuses of its [[864, 12]] lift proving d ≥ 16modulo three named, separately retirable trust assumptions (with d ≤ 36 by exact witnesses);a [[2592, 12]] level with certified floor 12; fully certified constant-distance control towers; and alift-portfolio result: distance verdicts are per-lift, with section structure provably varying acrossthe admissible lift space while k is preserved. A further contribution is methodological: anevidence-graded certification discipline (per-class SAT censuses run to UNSAT with retainedartifacts, known-answer gates, pre-registered readings, and theorems encoded as constraints) inwhich every reported number carries its grade.
Short cycles in the Tanner graph of a low-density parity-check (LDPC) code degrade belief-propagation (BP) decoding, and counting them is a standard step in code design and evaluation. This paper does not count them faster. It contributes a short-cycle diagnostic whose defining identity is a machine-checked theorem -- the trace-formula gap law tr(A^k) - p_k = tr(B^k), with A the adjacency matrix, B the Hashimoto non-backtracking operator and p_k the power sums of the matching-polynomial roots -- and whose per-code outputs are validated by three mutually independent computations that agree exactly. We report a certified census of the four deployed LDPC codes of the IEEE 802.11n (WiFi) standard at block length n=648, and, to our knowledge the first such diagnostic on a quantum LDPC code, of the IBM "gross code" [[144,12,12]] bivariate-bicycle (BB) code, finding girth 6 and c_6=144 shortest cycles. We then give a covering-tower factorization: a BB code whose Tanner graph is a double cover of a smaller code's Tanner graph inherits its short-cycle profile through the classical Artin-Ihara / 2-lift identity tr B^k(cover) = tr B^k(base) + tr B_s^k(base), verified exactly on the gross/[[72,12,6]] pair (c_6 doubles, 144 = 2*72). The contribution is the theorem-backed, cross-validated, reproducible methodology and its transfer from classical to quantum codes; the underlying mathematics is classical and is not claimed as new. We are explicit about what the certificate does and does not guarantee.
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.
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.
Additive codes over $\Ffour$ that are self-orthogonal under the trace inner product correspond to binary quantum stabilizer codes. We study 1-generator (1,2)-quasi-cyclic (QC) additive codes and their exact quantum distances. For composite lengths n=ℓm, an ancestor-lifting theorem transports dual words of the folded ancestor to the length-n code. A two-layer decomposition for ℓ=2 and a CRT splitting for odd ℓ yield dimension laws and explain equality, escape, and mixed-branch behavior in the certified examples. A palindromic criterion ensures symplectic self-orthogonality, while reversal pairing and a symplectic Gram rank formula describe broader construction families. Exact distances are established by information-set decoding screening, Brouwer--Zimmermann computation on the additive dual, and independent witness verification. We certify twenty-one record-breaking binary quantum codes across twenty entries of Grassl's code table, with twenty-eight certified members in total. Propagation improves thirty-four further entries, and explicit constructions are supplied for three table-tying GV entries marked Code Missing Construction. Six additional candidates are reported only with rigorous upper bounds and heuristic screening evidence. The results connect divisor-lattice structure in additive quasi-cyclic codes with reproducible certification of exact quantum distances.
This paper investigates certified upper bounds on the minimum distance of an explicit family of Calderbank-Shor-Steane quantum LDPC codes constructed from affine permutation matrices. All codes considered here have active Tanner graphs of girth eight. Rather than attempting to prove a general lower bound for the full code distance, we focus on constructing low-weight non-stabilizer logical representatives, which yield valid upper bounds once they are verified to lie in the opposite parity-check kernel and outside the stabilizer row space. We develop a unified framework for such witnesses arising from latent row relations, restricted-lift subspaces including block-compressed, selected-fiber, and CRT-stripe constructions, cycle- 8 elementary trapping-set structures, and decoder-failure residuals. In every case, search is used only to generate candidates; the reported bounds begin only after explicit kernel and row-space exclusion tests have been passed. For the latent part, we also identify a block-compression criterion under which the certification becomes exact. Applying these methods to representative APM-LDPC codes sharpens previously reported upper bounds and provides concrete certified values across the explored parameter range.