A proof assistant's kernel evaluates by reducing terms symbolically—and that is slow. Asking the kernel to sum a stabilizer code's weight enumerator over its 224 elements is hours of reduction; the same sum, compiled, is milliseconds. This gap is not a footnote. It means a machine-checked certificate is not one thing: for an object too large for the kernel to reduce, certification splits into a ladder. On the first rung the kernel proves the method exact—that bucket elimination equals the flat sum, a small general theorem with no compiler trust. On the second the compiler executes the instance—the actual census over a real code's generators, carrying only the compiler-correctness axiom. On the third the consequences are axiom-free: the quantum MacWilliams identity forces the normalizer spectrum, the code distance, and the sub-threshold error-rate prefactor from the executed spectrum, with an empty footprint. We make this ladder the object of study, draw its trust boundary exactly, and certify the rotated surface code [[25, 1, 5]]—distance 5, prefactor 160—past a census the kernel cannot touch. The ladder has an outer wall that is a theorem, not a limitation: computing an arbitrary code's exact spectrum is #P-hard, so the bounded-treewidth codes—the surface and toric family that hardware actually deploys—are the tractable island by complexity theory, and the determinant shortcut is provably blocked on the coupled CSS enumerator by a local free-fermion obstruction. We also state the discipline the ladder demands: a certificate that reads back a constant it was handed certifies nothing; certification must be tied to the actual object, and we show the difference is a theorem that fails when the tie is cut. Published by The Institute for Applied Ontological Mathematics.
A proof assistant's kernel evaluates by reducing terms symbolically—and that is slow. Asking the kernel to sum a stabilizer code's weight enumerator over its 224 elements is hours of reduction; the same sum, compiled, is milliseconds. This gap is not a footnote. It means a machine-checked certificate is not one thing: for an object too large for the kernel to reduce, certification splits into a ladder. On the first rung the kernel proves the method exact—that bucket elimination equals the flat sum, a small general theorem with no compiler trust. On the second the compiler executes the instance—the actual census over a real code's generators, carrying only the compiler-correctness axiom. On the third the consequences are axiom-free: the quantum MacWilliams identity forces the normalizer spectrum, the code distance, and the sub-threshold error-rate prefactor from the executed spectrum, with an empty footprint. We make this ladder the object of study, draw its trust boundary exactly, and certify the rotated surface code [[25, 1, 5]]—distance 5, prefactor 160—past a census the kernel cannot touch. The ladder has an outer wall that is a theorem, not a limitation: computing an arbitrary code's exact spectrum is #P-hard, so the bounded-treewidth codes—the surface and toric family that hardware actually deploys—are the tractable island by complexity theory, and the determinant shortcut is provably blocked on the coupled CSS enumerator by a local free-fermion obstruction. We also state the discipline the ladder demands: a certificate that reads back a constant it was handed certifies nothing; certification must be tied to the actual object, and we show the difference is a theorem that fails when the tie is cut. 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.
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 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.
A computational claim you cannot recompute is hearsay. We ask what a certified answer must be so that anyone can recompute it and refuse anything that does not match, and we answer that it must be a canonical form: a representative stable under the ways the answer can be re-expressed. We build three and show each survives a different transport. An optimum survives change of algorithm: one integer reached by exhaustive search below a size wall, by exact tropical variable elimination past that wall (bounded by a graph's width, not by its number of variables), and by the published literature. A quantum code's number of logical qubits survives change of proof: it is the block length minus two matrix ranks certified by a proof kernel, and its distance is either enumerated exactly or witnessed by an exhibited logical operator proven genuine by a rank increase. A certified answer survives change of language: its content hash agrees byte-for-byte across two independent implementations and refuses any value, such as a floating-point number, with no language-independent form. The consequence is operational: a reader re-derives the answer and serves it only if it matches. We place a live 2024 quantum-error-correction result on the classical side of this discipline, certifying the code parameters its own published matrices imply without disputing the demonstration. The through-line is old and exact: truth is invariant under change of notation, and a certificate is that invariant made computable. 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.
A quantum memory that accumulates k successive records of a single system can audit itself: its memory-side statistics obey polynomial identities, and its physical realizability is a positivity question. The companion paper (Gleason from Inside, doi:10.5281/zenodo.22014602) proved the two-record certificate (identity ideal + one back-action-corrected moment inequality M*) and left the k >= 3 ladder open. This note closes it for the single-collision comb architecture at every k. The entire identity structure is generated by the transverse Bloch block of the per-record collision channel, read in its two operator orders: a route-damping chain law (every skip-pair correlation as a sum over sine-pair routes, each damped by the visibility of every record strictly between its sine vertices) and a response transfer law carrying odd higher-sine routes; both are census-exact at machine precision through five records at every span and start. The identity variety's free chart has dimension exactly 2k+1, one transport identity per added record. The completeness theorem: a chart point is realizable if and only if its outcome probabilities are valid and the FIRST pair's M* is positive semidefinite; every later adjacent certificate is a consequence (the transported effective state inherits the Bloch ball). The proof is a constructive, optimization-free rung inversion; machine confirmations include 200/200 exact round trips, a 1703-point redundancy test with zero violations, and exact inversion of all 1094 points of a persisted certification sample. The comb moment hierarchy collapses at level one: identities do all equality work (linear in k) and a single two-record inequality does all positivity work forever. The frontier is named: multi-collision cells, reused cells, and non-commuting rotation axes are outside the theorem. The ledger of failed predictions, including two wrong transfer compositions killed by census gates, is an appendix.