quantumGateTypeCount
The theorem establishes that the finite type of canonical quantum gate types has cardinality exactly five. A quantum information theorist bounding circuit depth from RS recognition sequences would cite this count when assembling the quantumComputingDepthCert. The proof is a one-line decide tactic that enumerates the inductive constructors of QuantumGateType.
claimThe finite type of quantum gate types has cardinality 5, 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 enumerates five constructors (pauli, clifford, tGate, cnot, toffoli) and derives Fintype, Repr, and DecidableEq. This matches the module's assignment of five gate types to configuration dimension D = 5, while the single-qubit Pauli group has eight elements equal to 2^D.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute Fintype.card QuantumGateType directly from the inductive definition.
why it matters in Recognition Science
This supplies the five_gates field inside quantumComputingDepthCert, which is then used by molecularQuantumStateClasses_25 via rw [molecularEnergyCount, quantumGateTypeCount]. It fills the RS_PAT_043 / B15 proposition on quantum computing depth and connects to the forcing chain landmarks T7 (eight-tick octave) and T8 (D = 3).
scope and limits
- Does not derive the five gate types from the J-function or recognition composition law.
- Does not address multi-qubit extensions or continuous-parameter gate families.
- Does not claim these types are universal outside the RS model.
Lean usage
rw [molecularEnergyCount, quantumGateTypeCount]formal statement (Lean)
25theorem quantumGateTypeCount : Fintype.card QuantumGateType = 5 := by decide
proof body
Term-mode proof.
26
27/-- Pauli group (single qubit) has 8 elements. -/