CanonicalGate
plain-language theorem explainer
CanonicalGate enumerates the five gates H, X, Y, Z, CNOT that arise as the natural gate set from the recognition lattice. Workers on RS-derived quantum computing models cite this enumeration when establishing gate counts or Clifford subgroup sizes. The inductive definition lists the constructors explicitly and derives DecidableEq, Repr, BEq, Fintype by automation.
Claim. The set of canonical quantum gates is the inductive type whose constructors are the Hadamard gate $H$, the Pauli gates $X$, $Y$, $Z$, and the controlled-NOT gate CNOT, equipped with decidable equality, representation, boolean equality, and finite type structure.
background
The module states that the recognition lattice supplies a natural gate set for quantum computation. Five canonical gates are identified with configuration dimension D = 5. The identity gate maps to J = 0 (equilibrium recognition) while single-qubit gates correspond to Bloch-sphere rotations; eight Clifford gates equal 2^D, matching the eight-tick period. Upstream, the shifted cost H(x) = J(x) + 1 converts the Recognition Composition Law into the d'Alembert equation, and the anchor map Z assigns integers to lepton and quark sectors for mass calculations.
proof idea
The declaration is an inductive definition that enumerates the five gate constructors H, X, Y, Z, CNOT. The deriving clause invokes Lean automation to generate the DecidableEq, Repr, BEq, and Fintype instances without further proof steps.
why it matters
This inductive type supplies the gate set for the downstream theorems canonicalGateCount (cardinality equals 5) and QCGateCert (five gates together with Clifford size 8). It realizes the module claim that five gates equal configDim D = 5 and aligns with the eight-tick octave (T7) and D = 3 spatial dimensions (T8) from the unified forcing chain. No open scaffolding is present.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.