quantumGateTypeCount
plain-language theorem explainer
The theorem establishes that the finite type enumerating canonical quantum gates has exactly five elements. Researchers bounding quantum circuit depth or molecular state classes from Recognition Science would cite this cardinality to fix the gate basis. The proof is a one-line decision procedure that exhausts the five constructors of the inductive definition.
Claim. The cardinality of the set of quantum gate types is five, where the types are the Pauli, Clifford, T-gate, CNOT, and Toffoli operations.
background
In the Quantum Computing Depth from RS module, quantum computation is modeled as sequences of J-cost-minimizing recognition operations. The inductive type QuantumGateType lists five constructors: pauli, clifford, tGate, cnot, toffoli. This count is set equal to configDim D = 5, while the single-qubit Pauli group supplies eight elements matching 2^D for spatial D = 3. The upstream inductive definition of QuantumGateType in CrossDomain.QuantumMolecularBound supplies the identical enumeration used here.
proof idea
The proof is a term-mode application of the decide tactic. It automatically confirms the cardinality by enumerating the five constructors of the QuantumGateType inductive type and checking equality to the literal 5.
why it matters
This result populates the five_gates field of quantumComputingDepthCert and supplies the rewrite step in molecularQuantumStateClasses_25. It instantiates the five-gate universal set that, together with the eight-element Pauli group, generates all unitaries in the RS framework. The count aligns with the eight-tick octave (T7) and the forcing chain landmarks that fix D = 3 spatial dimensions while allowing configDim = 5 for gate types.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.