quantumComputingDepthCert
plain-language theorem explainer
quantumComputingDepthCert instantiates the QuantumComputingDepthCert structure by supplying three explicit equalities on gate counts. Researchers modeling quantum circuits inside Recognition Science would reference it to certify that five gate types, an eight-element Pauli group, and a three-gate universal set align with the framework's dimension and octave counts. The definition is a direct record constructor that invokes decide and rfl lemmas on the sibling theorems.
Claim. The certificate structure is populated by the assertions that the cardinality of the set of quantum gate types equals 5, the single-qubit Pauli group has cardinality exactly $2^3$, and a universal gate set contains exactly 3 gates.
background
The module Quantum Computing Depth from RS (RS_PAT_043 / B15) treats quantum computation as sequences of J-cost-minimizing recognition operations. It records that five canonical gate types (Pauli, Clifford, T, CNOT, Toffoli) equal configDim D = 5, that the single-qubit Pauli group has eight elements equal to $2^D$ with D = 3, and that the universal set {H, T, CNOT} has three members equal to D. The upstream theorems supply the concrete values: quantumGateTypeCount proves the gate-type cardinality is 5 by decide, pauliGroupSize_2cubed proves the Pauli count is $2^3$ by decide, and universalGates_eq_D proves the universal count is 3 by rfl.
proof idea
The definition is a one-line record constructor. It assigns the field five_gates the value of quantumGateTypeCount, the field pauli_8 the value of pauliGroupSize_2cubed, and the field universal_D the value of universalGates_eq_D.
why it matters
The definition supplies the concrete certificate required by the RS_PAT_043 / B15 statement that gate counts must match the Recognition Science dimension and octave structure. It directly encodes the eight-tick octave (T7) via the $2^3$ Pauli count and the spatial dimension D = 3 via the universal-gate count of 3. No downstream theorems yet consume the certificate, leaving open whether it will be invoked inside larger derivations of quantum depth or circuit complexity from the J-cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.