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 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.
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.
This paper develops a MacWilliams-type enumerator theory and semidefinite programming bounds for intrinsic quantum codes. An intrinsic code is a subspace C⊂V of a finite-dimensional unitary representation V of a group G, with errors organized into the isotypic components of L(V) under conjugation. The Knill-Laflamme conditions persist under every G-equivariant realization of V, aallowing intrinsic bounds to apply across diverse physical encodings. Without a group action, we first construct projector and twirl quadratic enumerators for an arbitrary orthogonal decomposition of L(V), analogous respectively to the A and B enumerators of Shor-Laflamme theory. These enumerators satisfy positivity, normalization, and Knill-Laflamme inequalities, but the two superoperator families need not span the same space and therefore admit no canonical duality. A group action places their generalized versions in the same equivariant intertwiner algebra, and the change of basis between them defines the intrinsic MacWilliams transform. When the conjugation representation has multiplicities, this algebra is noncommutative and the enumerators are matrix-valued; positivity and detection are encoded by Loewner-order constraints, making the natural programming bound a semidefinite program. The multiplicity-free specialization recovers the known scalar MacWilliams transform and linear-programming framework. For symmetric powers, intrinsic depth equals ordinary qudit distance, yielding extremality certificates for permutation-invariant qudit codes. Finally, for the 27-dimensional SU(3) representation V=(2,2), an exact dual certificate proves the sharp bound K≤5 for codes detecting the full adjoint isotypic component. An explicit 5-dimensional code attains the bound and, under the canonical embedding, gives a four-qutrit distance-2 code.
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.
In 1997, Shor and Laflamme defined the weight enumerators for quantum error-correcting codes and derived a MacWilliams identity. We extend their work by introducing our double weight enumerators and complete weight enumerators for qubit codes and then investigate the MacWilliams identities for these enumerators. Based on the generalized MacWilliams identities, we solve an open problem, namely, the Singleton-type bound for asymmetric quantum codes (AQCs). Besides, the Hamming-type and the first linear-programming-type bounds for the AQCs are deduced similarly.
As emerging quantum architectures evolve into heterogeneous networks combining different physical substrates, such as qubits for logic and higher-dimensional qudits for robust communication, the traditional scalar metrics of quantum error correction become insufficient. To address this, we introduce a mathematical framework based on dimension multisets to characterize quantum error-correcting codes (QECC) and absolutely maximally entangled (AME) states in mixed-dimensional Hilbert spaces. By replacing scalar weights with multisets, we accurately capture the exact physical composition of error supports across these diverse systems. Our central result is the mixed-dimensional quantum MacWilliams identity, which establishes the formal algebraic relationship between Shor-Laflamme enumerators and unitary weight enumerators. From this foundation, we deduce the mixed-dimensional shadow identity and derive rigorous, generalized constraints on code parameters, explicitly formulating the mixed-dimensional quantum Hamming, Singleton and Scott bounds, and developing a linear program to systematically evaluate code viability. For the Singleton bound, a tighter bound that has no homogeneous analogue is derived for pure mixed-dimensional codes. Finally, we deploy this enumerator machinery to thoroughly analyze AME states, utilizing shadow inequalities to constrain their existence and introducing a combinatorial grid method for the explicit construction of mixed-dimensional tripartite AME states.
For a stabilizer code carrying one tracked logical qubit, perturbed by a centered Gaussian ensemble of Pauli Hamiltonian modes, the fourth-order coefficient of the mean relative-entropy disturbance of the reduced logical state was conjectured by the present author to be the pure counting expression (1/2) N_ac (N_ac + 2) <Zbar>_0^2 sum_u 1/p_u, with N_ac the number of modes anticommuting with the bare logical Zbar; it was certified rational-exactly at three configurations and reported as an exactly verified conjecture. This note proves it. Both second-order kernels are evaluated in closed form by Pauli algebra alone. The diagonal kernel is K_aa = (1 - eps_a) <Zbar>_0 sigma_z, with eps_a the commutation sign of the mode with Zbar, which yields the induced drift, its quartic coefficient, and the diagonal part of the connected channel unconditionally - using neither the Knill-Laflamme conditions nor the code distance. The off-diagonal kernel carries a sign factor f_m = 1 + eps_am eps_bm - eps_bm eta_ab - eps_am multiplying an expectation that vanishes unless the product of the two modes lies in the normalizer of the stabilizer group. This gives a necessary and sufficient vanishing criterion and, from it, the explicit hypothesis the counting law needs: 2w < d_N(S), where w is the mode weight and d_N(S) the weight of the lightest non-identity normalizer element. The hypothesis covers the two distance-three certifications, explains why the law fails on the distance-two [[4,2,2]] code, and is sufficient but not necessary - the degenerate Shor code violates it yet satisfies the law, because the sign factor annihilates the offending pairs. Every kernel identity is certified mode by mode and pair by pair: 732 modes and 1,602 pairs across four codes, with no exception. This note is posted here for the first time. It proves a conjecture stated in A Complete Fourth-Order Expansion of Reconstruction and Logical Errors for Arbitrary Gaussian Coherent Noise (Zenodo DOI 10.5281/zenodo.23644208) and resting on the stabilizer-code framework of Knill-Laflamme Violations, Induced Logical Dephasing, and Deterministic Danger Maps for Coherent Noise on Stabilizer Codes (Zenodo DOI 10.5281/zenodo.23622023). The scripts reproducing every number in the note are deposited in this record as counting_law_scripts.zip. They require Python 3.10+ and NumPy; no other dependencies, CPU only. Version 2 adds counting_law_scripts.zip, which an upload error left out of version 1. The note itself is unchanged: the PDF is byte-for-byte the file published in version 1.