QuantumGateType
plain-language theorem explainer
Five quantum gate types are defined inductively as Pauli, Clifford, T-gate, CNOT and Toffoli to serve as the basis for depth certification in RS quantum models. Depth bound researchers reference the enumeration when proving that gate cardinality equals five and that Pauli elements number eight. The construction is a bare inductive type with derived finite-type and equality instances.
Claim. Let $G$ be the inductive collection of quantum gate types consisting of the Pauli family, the Clifford family, the T-gate family, the controlled-NOT family, and the Toffoli family, equipped with decidable equality and finite cardinality.
background
Recognition Science models quantum computation as sequences of J-cost-minimizing recognition operations on states. The module equates the number of canonical gate types to the configuration dimension D = 5. The single-qubit Pauli group then has size 2^D = 8, matching the eight-tick octave structure from the forcing chain.
proof idea
This is a direct inductive definition of the five constructors, followed by a deriving clause that automatically generates instances for decidable equality, representation, boolean equality, and finite type structure.
why it matters
The definition supplies the gate set for the QuantumComputingDepthCert certificate, which records that five gates, Pauli size 2^3, and three universal gates align with RS dimension D. It supports the gateCount theorem establishing cardinality five and enables downstream results on molecular quantum states. The construction realizes the framework claim that universal gate sets of cardinality D generate all unitaries, consistent with D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.