Clifford project

 Clifford project🔗

Compiled2026-06-26T14:46:08ZProjectfbccfd1More lemmasLeanleanprover/lean4:v4.30.0VersoBlueprintv4.30.0@eae235f696d9Mathlibv4.30.0@c5ea00351c28

This is a blueprint for the Clifford project whose goal is to formalize the structure theorem of the single-qudit Clifford group based on Appleby (2005). This formalization is work in progress and is done by participants of the Lean seminar at the University of Amsterdam.

Contents

  1. 1. Overview
  2. 2. Roots of unity
  3. 3. Symplectic form
  4. 4. Pauli matrices
  5. 5. Displacement operators
  6. 6. Clifford group
  7. 7. Symplectic action
  8. 8. Weyl representation
  9. 9. Clifford group structure
  10. Dependency Graph
  11. Blueprint Summary
  12. Blueprint Bibliography