QuantumGateType
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not claim these five families are the only possible quantum gates.
- Does not supply explicit matrix representations or unitaries for the gates.
- Does not prove that the set is universal; that property is stated upstream.
- Does not derive the depth bound; that follows from the sibling cardinality theorems.
formal statement (Lean)
26inductive QuantumGateType where
27 | pauli | clifford | tGate | cnot | toffoli
28 deriving DecidableEq, Repr, BEq, Fintype
29