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.
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.
A quantum error-correcting code's logical operators, taken modulo its stabilizers, form a finite abelian group; that group, not any single number, is the code's logical identity. We identify the group as one mathematical object across a divide usually treated as fundamental: the cokernel of an integer matrix, read off its Smith normal form. For a Gottesman–Kitaev– Preskill bosonic code the matrix is an integral symplectic Gram matrix and the cokernel is Q 2 (Z/d i Z) ; for a quantum low-density-parity-check digital code the matrix is a boundary i map and the cokernel is its first homology; the reading is the same computation, and code concatenation is the cokernel of a direct sum, so the two Smith normal forms simply concatenate. Because the cokernel is the complete invariant of the two-sided unimodular action, a code's logical group is certified by verifying a witness rather than by trusting a table: a prover supplies (U, D, V ) and a checker re-derives U AV = D in pure integer arithmetic. Every result is checked in Lean 4, and its load-bearing arithmetic is reproved in a second, toolchain-disjoint Cubical Agda kernel from the Peano axioms up. We prove that the group order alone is an incomplete invariant—(Z/2Z)4 and (Z/4Z)2 share order sixteen but differ in two-torsion—give an analog-weighted decoder whose correctable region provably exceeds the hard-decision region because the soft metric widens the distance, and expose the entire certified construction inside a live PennyLane and Strawberry Fields workflow, the software and hardware setting of a photonic fault-tolerant program built on exactly this concatenation. 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.
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.
Fault-tolerant quantum computation requires error-correcting codes that not only protect quantum information but also support useful logical operations with practical physical realizations. Here we develop a general framework in which the stabilizer syndromes of commuting Pauli rotations directly organize logical-gate design. We derive an exact codespace-preservation condition valid at arbitrary rotation angles, providing a common stabilizer-level description for CSS and non-CSS codes and for both Clifford and non-Clifford operations. A particularly useful equal-syndrome specialization reduces Clifford gate design to stabilizer factorization, yields a general generator weight bound of ⌈d/2⌉ for distance-d codes, and systematically extends to logical rotations higher in the Clifford hierarchy. Applied to bivariate-bicycle (BB) and non-CSS Mirror qLDPC codes, the framework gives explicit low-weight Clifford and controlled-phase gates. Our implementations yield new low-weight gates, including an addressed T gate on the [[16,4,4]] BB code, T-type rotations on the [[64,8,8]] BB code, and CCZ-, CS-, and T-type operations on the [[36,6,6]] Mirror code. We also develop analytic constructions using Clifford algebra bases, which turn the syndrome constraints into explicit algebraic relations and provide a systematic route to logical addressability. We use this approach to analytically construct addressed CNOT, SWAP, controlled, and CCZ-type gates on recursive hypercube codes. An independent construction on middle quantum Reed--Muller codes yields CrZ gates that saturate the equal-syndrome weight bound. These results establish stabilizer syndromes as a constructive link between the stabilizer structure of a quantum code, the logical computations it can directly support, and the fault-tolerance properties of their physical realizations.
A classical bit fails one way: it flips. A qubit fails three ways—X, Z, or both at once—and that single change of arithmetic, from one error per site to three, is the whole difference between the classical theory of error-correcting codes and the quantum one. It has a precise home. The MacWilliams identity of 1963 is the exact law relating a linear code's weight distribution to its dual's; its quantum analogue, due to Shor and Laflamme, carries the same law across the stabilizer formalism with one coefficient changed—a +1 becomes a +3. We prove that quantum identity in the kernel of a proof assistant, and we prove it the honest way: by reusing, unchanged, the finite character-orthogonality argument that certifies the classical identity, isolating the +3 to a single new lemma about the four Pauli operators at one qubit. The classical coefficient is not merely inapplicable to quantum codes; we exhibit a code on which the +1 law is false and its failure is itself a theorem. From the certified identity the entire Shor–Laflamme weight spectrum of a code follows—the count of stabilizers and of logical operators at every weight—and from the spectrum two numbers the field cares about: the code distance (the minimum weight of a logical operator, recovered as the first place the spectra part) and the sub-threshold error-rate prefactor (the count of minimum-weight logical representatives, which the distance alone cannot see). We certify both for the five-qubit perfect code and the Steane code, exhibit the exact spectra, and place the result beside a companion certificate that reaches the distance by a single witness: the witness is a local probe, the enumerator a global census, and a code is fully accounted for only when both have spoken. A public instrument reproduces every number by independent enumeration, trusting neither our kernel nor our word. Published by The Institute for Applied Ontological Mathematics.
The quantum logic gates used in the design of a quantum computer should be both universal, meaning arbitrary quantum computations can be performed, and fault-tolerant, meaning the gates keep errors from cascading out of control. A number of no-go theorems constrain the ways in which a set of fault-tolerant logic gates can be universal. These theorems are very restrictive, and conventional wisdom holds that a universal fault-tolerant logic gate set cannot be implemented natively, requiring us to use costly distillation procedures for quantum computation. Here, we present a general framework for universal fault-tolerant logic with stabilizer codes, together with a no-go theorem that reveals the very broad conditions constraining such gate sets. Our theorem applies to a wide range of stabilizer code families, including concatenated codes and conventional topological stabilizer codes such as the surface code. The broad applicability of our no-go theorem provides a new perspective on how the constraints on universal fault-tolerant gate sets can be overcome. In particular, we show how nonunitary implementations of logic gates provide a general approach to circumvent the no-go theorem, and we present a rich landscape of constructions for logic gate sets that are both universal and fault-tolerant. That is, rather than restricting what is possible, our no-go theorem provides a signpost to guide us to new, efficient architectures for fault-tolerant quantum computing.