canonicalGateCount
plain-language theorem explainer
The theorem establishes that the inductive type of canonical gates extracted from the recognition lattice has cardinality exactly five. Quantum information researchers constructing RS-based gate models cite this cardinality when certifying minimal gate sets. The proof reduces to a single decision procedure that enumerates the finite constructors and confirms the count.
Claim. The finite type whose constructors are the canonical gates $H$, $X$, $Y$, $Z$, and CNOT has cardinality five.
background
The module defines CanonicalGate as the inductive type with constructors H, X, Y, Z, CNOT, each deriving Fintype so that cardinality is computable. This set is presented as matching configDim D = 5 in the recognition lattice, with the identity gate corresponding to J-cost zero and single-qubit gates realized as Bloch-sphere rotations. The local setting is the B16/S6 quantum-computing depth in which the recognition lattice supplies a natural gate set; the upstream structure for supplies the meta-realization axioms that license such self-referential derivations of physical gate sets.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the Fintype.card equality on the inductive type CanonicalGate; decidability follows from the derived Fintype instance on the five constructors.
why it matters
The result populates the five_gates field of the downstream QCGateCert definition, which certifies the entire gate set for Recognition Science quantum computing. It instantiates the module claim that five gates equal configDim D and aligns with the eight-tick octave (T7) in which the Clifford group size is 2^D = 8. No open scaffolding remains; the declaration closes the finite enumeration step without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.