qcGateCert
plain-language theorem explainer
The qcGateCert definition assembles a certificate confirming that recognition science yields five canonical quantum gates and eight single-qubit Clifford gates. Physicists deriving gate sets from the recognition lattice would cite it to tie gate counts to the eight-tick period. The construction is a direct record that invokes two decide-based theorems establishing the respective cardinalities.
Claim. The quantum gate certificate asserts that the set of canonical gates has cardinality 5 and that the number of single-qubit Clifford gates equals 8.
background
In the Recognition Science treatment of quantum computing the recognition lattice supplies a natural gate set. Five canonical gates (H, X, Y, Z, CNOT) match configDim D = 5, while the Clifford group for one qubit has size 8 = 2^D, aligning with the eight-tick octave. The identity gate is identified with J = 0, the equilibrium of the J-cost function. The structure QCGateCert packages these two numerical claims. Upstream, canonicalGateCount proves the five-gate count by direct computation and clifford_eq_8 proves the Clifford count of 8, both via the decide tactic.
proof idea
This definition constructs the QCGateCert instance by supplying the five_gates field directly from the canonicalGateCount theorem and the clifford_8 field from the clifford_eq_8 theorem. It is a one-line wrapper that assembles the two decide-proved equalities into the required structure.
why it matters
This certificate anchors the quantum gate set to the Recognition Science framework, linking the five gates to configDim D = 5 and the eight Clifford gates to the 2^D period from the eight-tick octave. It supports derivations of quantum computing operations from the recognition lattice without new axioms. No downstream uses appear yet, leaving open its integration with full circuit proofs in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.