The Certified Quantum-Code Calculator

Exact distance, weight enumerators, and error-rate constants for real quantum codes — as theorems you can check

The distance of a quantum error-correcting code is its single most-quoted property, it is NP-hard to find in general, and establishing it for a specific code is a research result (the "12" in the IBM [[144,12,12]] code was a computational feat). The sub-threshold logical error rate is P_L ≈ (prefactor)·pᵈ⁄², and the whole field estimates that prefactor by Monte Carlo.

This artifact makes both exact kernel theorems. The accompanying paper — The Enumerator Is a Theorem (IAOM 2026, paper/) — proves a general quantum (symplectic Shor–Laflamme) MacWilliams identity in Lean 4 by finite character orthogonality, the same engine that certifies the classical MacWilliams identity:

|S| · W_normalizer(x, y)  =  W_stabilizer(x + 3y, x − y)

The +3 (versus the classical +1) is the quantum content — a qubit carries three nontrivial single-qubit errors (X, Y, Z), not one bit flip — and it is load-bearing: with +1 the identity provably fails on every quantum code. From this the calculator reads off, for any stabilizer code, its exact A/B enumerators, its exact distance, and its exact error-rate prefactor.

Certified in the Lean development (declarations named in the paper): the five-qubit [[5,1,3]], Steane [[7,1,3]], and Shor [[9,1,3]] codes — distances 3, 3, 3 and prefactors 30, 21, 39.

Validate it yourself in 30 seconds — trusting nothing

git clone <this-repo> && cd certified-quantum-enumerator
python verify_code.py                              # the [[5,1,3]], Steane, Shor ladder
python verify_code.py XZZXI IXZZX XIXZZ ZXIXZ     # ... or any code you type
python tests/test_enumerator.py                    # the anti-vacuity suite (incl. the +3 mutant)

verify_code.py uses nothing from our engine: it enumerates the full stabilizer group and its symplectic normalizer by brute force, computes the enumerators and distance, and independently checks the quantum MacWilliams identity. If it prints VERIFIED, the identity holds — independent of us, of Lean, and of the paper.

Trust model

this repository (Python)          ← brute-force enumeration + independent MacWilliams check
        ▼ names
Lean 4 theorems (proven tier)     ← sympWeightEnum_dual (the quantum MacWilliams identity),
                                    A513/B513, distance513/713/913, prefactor513/713,
                                    enumerator_macwilliams_513, coord_sum_not_binary (the +3 mutant)

The Lean sources are not distributed here; the declarations are named so every claim is auditable against the paper, and the sources are available from the authors for audit. The brute-force verifier exists precisely so third parties need not take our word — or our kernel — for the arithmetic.

License

Public for validation and review; see LICENSE. © 2026 IAOM / AgentPMT.