theorem proved term proof

`canonicalGateCount`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  25theorem canonicalGateCount : Fintype.card CanonicalGate = 5 := by decide

Term-mode proof.

  26
  27/-- Clifford group size: 8 = 2^D for single qubit. -/

From the project-wide theorem graph. These declarations reference this one in their body.

qcGateCert in IndisputableMonolith.Physics.QuantumComputingGatesFromRS decl_use

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
CanonicalGate in IndisputableMonolith.Physics.QuantumComputingGatesFromRS decl_use