theorem
proved
canonicalGateCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.QuantumComputingGatesFromRS on GitHub at line 25.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
22 | H | X | Y | Z | CNOT
23 deriving DecidableEq, Repr, BEq, Fintype
24
25theorem canonicalGateCount : Fintype.card CanonicalGate = 5 := by decide
26
27/-- Clifford group size: 8 = 2^D for single qubit. -/
28def cliffordSingleQubit : ℕ := 2 ^ 3
29theorem clifford_eq_8 : cliffordSingleQubit = 8 := by decide
30
31/-- Identity gate corresponds to J = 0. -/
32-- Structural claim: the identity gate = recognition equilibrium.
33
34structure QCGateCert where
35 five_gates : Fintype.card CanonicalGate = 5
36 clifford_8 : cliffordSingleQubit = 8
37
38def qcGateCert : QCGateCert where
39 five_gates := canonicalGateCount
40 clifford_8 := clifford_eq_8
41
42end IndisputableMonolith.Physics.QuantumComputingGatesFromRS