universalGates_eq_D
plain-language theorem explainer
The theorem equates the size of the universal gate set to three, matching the spatial dimension D in the Recognition Science model of quantum computation. Researchers certifying circuit depths in RS-native quantum algorithms would cite this equality when constructing the QuantumComputingDepthCert record. The proof is a direct reflexivity step on the constant definition of universalGates.
Claim. The cardinality of the minimal universal gate set satisfies $|{H, T, CNOT}| = 3$, where this set generates all unitaries in the RS model of quantum computation.
background
The module models quantum computation as sequences of J-cost-minimizing recognition operations. It identifies five canonical gate types with configuration dimension five and states that the single-qubit Pauli group has eight elements equal to $2^3$. The upstream definition sets universalGates to the constant three, corresponding to the universal set {H, T, CNOT}.
proof idea
This is a one-line wrapper that applies the reflexivity tactic directly to the definition universalGates := 3.
why it matters
The result supplies the universal_D field inside the QuantumComputingDepthCert definition, completing a certification step for quantum computing depth under the RS framework. It connects the three-element gate set to the T8 forcing step that yields D = 3 spatial dimensions and the eight-tick octave that produces the Pauli group size of eight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.