QuantumGateType
plain-language theorem explainer
The QuantumGateType inductive enumerates the five gate families (Pauli, Clifford, T, CNOT, Toffoli) that fix the second factor in the 25-element molecular state space. Cross-domain researchers on quantum circuit depth for molecular substrates cite this enumeration to obtain the exact cardinality five. The definition is a direct inductive construction with automatic derivation of finiteness and decidability instances.
Claim. The type of quantum gates is the inductive type generated by the five constructors Pauli, Clifford, T-gate, CNOT, and Toffoli.
background
The module establishes the C4 cross-domain bound: the reachable state space on a molecular substrate is the product of five energy levels and five gate types, yielding cardinality 25. This satisfies 25 ≤ 2^5 = 32, so every state is reachable in at most five gate layers. The definition of QuantumGateType is imported from the quantum computing depth module, where it populates the five_gates field of QuantumComputingDepthCert together with the assertions pauliGroupSize = 2^3 and universalGates = 3.
proof idea
The declaration is an inductive definition that directly lists the five constructors and derives DecidableEq, Repr, BEq, and Fintype via the deriving clause. No separate proof steps are required.
why it matters
This enumeration supplies the gate factor for the 5 × 5 = 25 state space in the quantum molecular bound. It is used by gateCount to prove Fintype.card = 5, by the abbrev QuantumMolecularState as the product type, and by energy_surj to witness surjectivity onto energy levels. Downstream it fills the five_gates component of QuantumComputingDepthCert. The construction supports the Recognition Science claim that molecular targets remain reachable within five layers per phi-rung, closing the cross-domain cardinality argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.