Generators and relations for 2-qubit Clifford+T operators, in Lean

A formalization of the main result of X. Bian and P. Selinger, "Generators and relations for 2-qubit Clifford+T operators", QPL 2022, EPTCS 394, 2023 (doi:10.4204/EPTCS.394.2, arXiv:2204.02217): the relations of Figure 1 are sound and complete for the 2-qubit Clifford+T group, relative to Greylyn's presentation of U₄(ℤ[1/√2, i]) (Theorems 5.1 and 5.2). It is based on the Agda formalization by X. Bian and P. Selinger that accompanies the paper (the ancillary files of arXiv:2204.02217; Sec. 5.2 and Fig. 4 of the paper). One difference: here words are lists of generators (elements of the free monoid), so that associativity and the unit laws hold by definition, whereas the Agda code treats them as laws.

The files are listed in order of dependency: each file only imports earlier ones (CliffordT.lean imports all of them). In particular, the statement of the main result, in Statement.lean, is self-contained and does not depend on any of the files in (b) and (c), which are only used in the proof.

(a) Statement of the result

File	Contents	Paper
`Statement.lean`	Words (the free monoid `X*`) and derivability (`Γ ⊢ w = v`, the smallest congruence containing the relations `Γ`); the generators `ω, H₀, H₁, S₀, S₁, T₀, T₁, CZ` and the relations C1–C20; Greylyn's generators and relations G1–G20; the translation `f`; and `MainTheorem` (soundness and completeness).	Figs. 1, 3; Sec. 5.1

This file depends only on Mathlib's free monoids and congruences.

(b) Proofs

File	Contents	Paper
`ReidemeisterSchreier.lean`	The Reidemeister-Schreier theorem for monoids, in a simplified version (no cosets) and in the full version.	Def. 4.2, Thm. 4.3
`Rewriting.lean`	A rewriting engine: rewrite rules (equations with derivations), grouped in stages, canonical forms modulo commuting generators, and normalization with a bounded number of steps. The normalization functions are run by Lean's kernel (`decide`), so an equation is proved by rewriting both sides to the same normal form.
`GreylynLemmas.lean`	Rewrite systems for Greylyn's relations.
`Soundness.lean`	Soundness: `f` maps each of C1–C20 to a consequence of Greylyn's relations.	Thm. 5.1
`GreylynSimplified.lean`	A simplified presentation of U₄(ℤ[1/√2, i]) with 5 generators and 19 relations, equivalent to Greylyn's.
`CliffordLemmas.lean`	A decision procedure for the Clifford relations: rewrite systems built in stages, each justified by lemmas proved with the previous ones.
`CliffordTLemmas.lean`	Inverses, the swap gate, duality, commutations and orders in the Clifford+T monoid, which is a group.
`PauliRotations.lean`	Pauli operators, the action of Clifford words on them, and the Pauli rotations `R p`: their conjugation by Clifford words, commutation, combination and sign correction.	Sec. 4.3
`EquationTactics.lean`	Proof steps for long chains of equations: an equation applied to the subword at a given position, and Clifford rewriting of a subword.
`Equations/Equation1.lean` … `Equation46.lean`	The 46 equations needed for the hypotheses of the Reidemeister-Schreier theorem, each proved by a long chain of steps.
`Completeness.lean`	Completeness, by the Reidemeister-Schreier theorem: first for the simplified presentation, then for Greylyn's.	Thm. 5.2

(c) The final witness

File	Contents
`Main.lean`	`theorem mainTheorem : MainTheorem`.

It depends only on the standard axioms propext, Classical.choice, and Quot.sound; Main.lean prints them (#print axioms) when it is checked. In particular, the decision procedures are run by the kernel, not by compiled code (no native_decide).

The equations

Equations/Equation1.lean … Equation46.lean are witnesses meant to be checked rather than read: each proof is a long chain of equations, in which each line is either a word or the justification of the equation between it and the previous word.

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.

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 make the commands lean and lake available in the current shell:
```
source $HOME/.elan/env
```
Go to the directory containing this file, and download Mathlib, already compiled (this takes a few minutes):
```
lake exe cache get
```
Check all proofs (this takes about 10 to 60 minutes, depending on the computer):
```
lake build
```
The output ends with
```
info: CliffordT/Main.lean:20:0: 'CliffordT.mainTheorem' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (965 jobs).
```
This certifies that the theorem is proved, using only the standard axioms.

License

The Lean files are released under the MIT license; see the file LICENSE. They are provided "as is", without warranty of any kind. They are based on the Agda formalization by Xiaoning Bian and Peter Selinger, which accompanies the paper and is released under the Creative Commons Attribution license (CC BY 2.0).