cliffordSingleQubit
plain-language theorem explainer
The definition sets the single-qubit Clifford gate count to 8, matching 2 raised to the spatial dimension. Researchers deriving quantum gates from the recognition lattice cite this constant to link the Clifford group order with the eight-tick period. It is introduced as the direct power 2^3 with no lemmas or reductions required.
Claim. Let $N_C$ denote the number of single-qubit Clifford gates. Then $N_C = 2^D$ where $D=3$ is the spatial dimension, so $N_C=8$.
background
The module derives a quantum gate set from the recognition lattice. Five canonical gates arise from configuration dimension 5, while the Clifford group supplies eight elements that match the 8-tick octave period. The identity gate is identified with zero J-cost at recognition equilibrium. This definition supplies the numerical constant 8 that appears in the gate certification structure.
proof idea
Direct definition as the power 2 raised to 3. It functions as a one-line wrapper that establishes the numerical value without invoking external lemmas or tactics.
why it matters
This definition supplies the value that feeds the equality theorem clifford_eq_8 and the QCGateCert structure. It realizes the eight-tick octave landmark from the forcing chain where the period equals 2^3 for D=3. The parent results are the equality theorem and the gate certification structure in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.