The Certified Magic Ledger

The constants at the bottom of every FTQC resource estimate — as theorems you can check

Every fault-tolerant resource estimate bottoms out in the 15-to-1 magic-state factory's constants: the output-error law "35p³" and the acceptance rate, derived on paper in 2005 and consumed as unexamined literals ever since. The accompanying paper, The Yield Is a Theorem (IAOM 2026, paper/), makes them exact kernel theorems via a MacWilliams identity proved in Lean 4: for input error p = a/d under the standard twirled noise model, with u = d−2a,

16·accept(a,d)   = d¹⁵ + 15·d⁷·u⁸
32·harmless(a,d) = d¹⁵ + 15·d⁸·u⁷ + 15·d⁷·u⁸ + u¹⁵

Consequences (each a kernel-checked theorem): the folklore coefficient is exactly 35 = 1120/32, with its full remainder polynomial — and the folklore is graded: the true output error exceeds 35p³ by +3.1% at p=1/100, +17.5% at p=1/20, +36.4% at p=1/10.

Validate it yourself in 30 seconds — trusting nothing

python verify_identities.py            # brute-forces all 2^15 patterns at three noise points
python verify_identities.py 3 25      # ... or any rational p = a/d you choose
python tests/test_ledger.py            # the anti-vacuity suite

verify_identities.py uses nothing from this repository's engine: it enumerates every error pattern of the protocol directly and checks the closed forms. If it prints MATCH, the identities hold — independent of us, of Lean, and of the paper.

The engine and the in-loop experiment

from fractions import Fraction as F
from magic_ledger import exact_round, magic_ledger

exact_round(F(1, 100))                 # exact acceptance + output error + folklore deviation
magic_ledger(F(1, 100), F(1, 10**12))  # the factory plan: rounds, overhead, states/output

With PennyLane installed, distillation_testbed.py runs the factory in the loop: a stim-backed 19-qubit Clifford circuit with genuine phase-kickback syndrome extraction (the syndrome is cross-checked against the data readout on every shot). Measured acceptance at 40,000 shots: 0.2201 vs the proven 0.219786 at p = 1/10.

pip install pennylane && python distillation_testbed.py

Trust model

this repository (Python)        ← exact arithmetic + independent brute-force validation
        ▼ names
Lean 4 theorems (proven tier)   ← weightEnum_dual (the kernel MacWilliams identity),
                                  accept_identity, harmless_identity, numerator_expansion,
                                  folklore_deviation_p100/p20/p10
        ▼ modeled by
twirled iid-Z noise (reported)  ← the standard Bravyi–Kitaev reduction, cited not proved

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 that third parties need not take our word — or our kernel — for the arithmetic.

License

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