QCGateCert
plain-language theorem explainer
QCGateCert packages two numerical assertions from the recognition lattice into a certificate structure: the canonical gate set has cardinality five and the single-qubit Clifford group has order eight. Physicists building RS-derived quantum gate sets would cite it to confirm the lattice matches the expected five-gate basis and eight-tick Clifford period. The declaration is a bare structure definition that directly records the Fintype cardinality of CanonicalGate and the explicit value of cliffordSingleQubit.
Claim. The structure $QCGateCert$ asserts that the set of canonical gates has cardinality five and that the number of single-qubit Clifford gates equals eight.
background
The module Quantum Computing Gates from RS maps the recognition lattice to standard quantum gates for B16/S6 QC depth. CanonicalGate is the inductive type with constructors H, X, Y, Z, CNOT. The constant cliffordSingleQubit is defined as $2^3$, matching the eight-tick octave period for $D=3$ spatial dimensions. Module documentation states: 'The recognition lattice provides a natural gate set. Five canonical quantum gates (H, X, Y, Z, CNOT) = configDim D = 5. Also: 8 Clifford gates (Pauli × phase) = 8 = 2^D = 8-tick period.'
proof idea
This is a structure definition with an empty proof body. It declares two fields that record the Fintype cardinality of the CanonicalGate inductive type equaling five and the value of cliffordSingleQubit equaling eight, both established by prior sibling definitions.
why it matters
QCGateCert supplies the numerical invariants required by the downstream qcGateCert construction. It closes the B16/S6 QC Depth section by confirming the lattice yields the expected five-gate set and the $8=2^3$ Clifford count, directly instantiating the eight-tick octave (T7) and $D=3$ (T8) from the forcing chain. No open questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.