QuantumComputingDepthCert
plain-language theorem explainer
QuantumComputingDepthCert packages three numerical identities that tie the count of canonical quantum gate types, the size of the single-qubit Pauli group, and the size of a universal gate set to the spatial dimension in Recognition Science. A researcher deriving circuit-depth bounds from the J-cost model would cite the structure to certify consistency with D equals three. The definition is realized as a direct record constructor that references the precomputed constants for gate cardinality, Pauli size, and universal-set size.
Claim. A record asserting that the number of canonical quantum gate types equals 5, the single-qubit Pauli group has cardinality $2^3$, and a universal gate set has cardinality 3, where the gate types are the five elements Pauli, Clifford, T-gate, CNOT, and Toffoli.
background
The module models quantum computation as sequences of J-cost-minimizing recognition operations. The inductive type enumerating canonical gates contains exactly the five constructors Pauli, Clifford, T-gate, CNOT, and Toffoli. The sibling constant for Pauli-group size is fixed at 8 and the constant for universal-gate count is fixed at 3, matching the spatial dimension D.
proof idea
The declaration is a direct structure definition whose three fields are set equal to the Fintype cardinality of the gate-type inductive, the pre-defined Pauli-group size, and the pre-defined universal-gate count. No lemmas or tactics are invoked beyond these sibling references.
why it matters
The structure supplies the type for the downstream instance that certifies gate counts under RS_PAT_043 / B15. It anchors the numerical matches to the eight-tick octave (period $2^3$) and the forcing-chain result that spatial dimension equals 3, thereby supporting later bounds on quantum-computation depth expressed in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.