QuantumGateType
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not specify the unitary matrices realized by each gate type.
- Does not prove that the set is universal for quantum computation.
- Does not quantify the J-cost of individual gates.
- Does not address multi-qubit extensions beyond the listed types.
formal statement (Lean)
21inductive QuantumGateType where
22 | pauli | clifford | tGate | cnot | toffoli
23 deriving DecidableEq, Repr, BEq, Fintype
24