Generators and relations for real stabilizer operators, in Lean

A formalization of the main result of J. Makary, N. J. Ross, P. Selinger, "Generators and relations for real stabilizer operators" (QPL 2021): the relations R1–R16 (Figure 1) are sound and complete for real stabilizer circuits, and so are the alternative relations S1–S19 (Appendix A).

The files are listed in order of dependency: each file only imports earlier ones (RealStab.lean imports all of them).

(a) Background

File Contents
PRO/Basic.lean PROs (strict monoidal categories whose objects are the natural numbers) and their laws, including the spatial law for scalars.
PRO/Free.lean The free PRO on a signature, presentations by relations (Γ ⊢ t = u), interpretations of terms (⟦t⟧ρ), and soundness of interpretations.
PRO/Matrix.lean The PRO of matrices indexed by bit vectors, with the Kronecker product as tensor.
PRO/Subst.lean Substituting terms for generators; it preserves provable equations.

(b) Statements of the results

File Contents
Statement.lean Generators -1, H, Z, CZ, the relations R1–R16, the interpretation as real matrices, and MainTheorem (soundness and completeness).
AltStatement.lean Generators -1, H, Z, CZ, X, CX, XC, the relations S1–S19, their interpretation, and Alt.MainTheorem.

These two files depend only on the background in (a).

(c) Proofs

File Contents Paper
Soundness.lean Soundness: R1–R16 hold as matrix equations, decided over the integers.
Word.lean Circuits as words of gates on adjacent wires; every circuit is equal to the circuit of its word; gates on disjoint wires commute.
Rule.lean Rules (provable equations between words), applied at an offset and up to commuting gates; time reversal.
Reduce.lean Sorting commuting gates and cancelling equal neighbours.
AxiomRules.lean R1–R16 as rules; every gate is an involution.
Derivations/Part1.lean … Part7.lean The lemmas L1–L19 and the typed relations of Appendix B, with the proofs of the supplement, step by step. Part 1: L1–L17. Part 2: L18, L19, 3.1–3.18. Part 3: 3.19–3.25, 4.1–4.4, 4.9–4.17. Part 4: 4.18–4.20, 4.33–4.38, 5.1–5.8, 6.1. Part 5: 6.2–6.16, 8.1–8.5. Part 6: 8.6–8.18, 9.1–9.7. Part 7: 9.8–9.16, 10.1, 10.2, 4.5–4.8, 4.21–4.32, 7.1–7.16. Supplement, Appendix B
NormalForm/Basic.lean Clean gates (derived generators), dirty gates, labelled wires (Bundle), normal forms as circuits of clean gates between labelled wires. Sec. 4.1, Defs. 4.8–4.10, 5.2, 5.3
NormalForm/Lemmas.lean, NormalForm/Step.lean Absorbing one dirty gate: by a typed relation, or by moving it past a clean gate on other wires. Lemma 5.4
NormalForm/Cases.lean Every admissible dirty gate is absorbed: the case distinction over the typed relations. Lemma 5.4
NormalForm/Exists.lean The normal form of the identity; every circuit is equal to a normal form. Prop. 5.5
Uniqueness/Pauli.lean Real Pauli operators and the action of gates on them by conjugation. Sec. 2
Uniqueness/Local.lean, Uniqueness/Facts.lean The action of the derived generators on the Pauli operators on their wires. Prop. 4.7
Uniqueness/ZX.lean Uniqueness of Z-circuits and X-circuits; X-circuits take Z ⊗ I ⊗ ⋯ to I ⊗ ⋯ ⊗ Z. Props. 4.11–4.13
Uniqueness/Unique.lean Normal forms with the same action on Pauli operators are equal. Props. 4.14, 4.15
Uniqueness/Conj.lean, Uniqueness/Matrix.lean Circuits with equal matrices act equally on Pauli operators. Sec. 2
Completeness.lean Completeness of R1–R16. Prop. 5.5, 4.15
Alt/Translate.lean Translating S-circuits into R-circuits (writing out X, CX, XC) preserves matrices. App. A
Alt/Derive.lean Deriving R1–R16 from S1–S19 (R15 and R16 from S18 and S19, via the two-wire identity CX XC CX XC = XC CX). App. A
Alt/Complete.lean Soundness and completeness of S1–S19. App. A

(d) The final witnesses

File Contents
Main.lean theorem mainTheorem : MainTheorem and theorem Alt.mainTheorem : Alt.MainTheorem.

Both depend only on the standard axioms propext, Classical.choice, and Quot.sound; Main.lean prints them (#print axioms) when it is checked.

Generated files

Derivations/Part1.lean … Part7.lean (by scripts/emit.py) and NormalForm/Cases.lean (by scripts/nfcases.py) are generated by Python scripts. They read the relations and the derivations of the supplement from the data file data/realstab.json, which contains all circuits of the paper and its supplement in machine-readable form (its conventions are described in the file).

Checking the proofs

You need an internet connection, about 8 GB of disk space (mostly for Mathlib), and the programs git and curl. The versions of Lean and Mathlib are fixed by the files lean-toolchain and lake-manifest.json; the commands below install exactly these versions.

  1. Install elan, the installer of Lean (Linux and macOS; for Windows, see https://lean-lang.org/install/):

    curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

    Answer the question with 1 (proceed with the default installation), then open a new terminal window, so that the commands lean and lake are found.

  2. Go to the directory containing this file, and download Mathlib, already compiled (this takes a few minutes):

    lake exe cache get

  3. Check all proofs (this takes about 5 to 15 minutes, depending on the computer):

    lake build

    The output ends with

    info: RealStab/Main.lean:20:0: 'RealStab.mainTheorem' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RealStab/Main.lean:21:0: 'RealStab.Alt.mainTheorem' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [1876/1877] Built RealStab (2.7s)
Build completed successfully (1877 jobs).

    This certifies that both theorems are proved, using only the standard axioms.

The Python scripts

The Python scripts in scripts/ are included for reference only. They are not needed for checking the proofs, and they need not be trusted: Lean checks every proof, whichever program wrote it. What a reader has to check is only that the statements in (b) say what the paper says. To regenerate the generated files, run python3 scripts/emit.py and python3 scripts/nfcases.py (Python 3, no other packages); they read data/realstab.json and write only the generated files listed above.

License

Copyright (c) 2026 Peter Selinger.

Copyright (c) 2021 Justin Makary, Neil J. Ross, and Peter Selinger.

The files in this directory (the Lean files, the Python scripts, and the data file) are released under the MIT license; see the file LICENSE. They are provided "as is", without warranty of any kind.