QuantumComputingDepthCert
plain-language theorem explainer
QuantumComputingDepthCert is a structure that packages three equalities tying quantum gate counts to Recognition Science dimensions: five gate types, Pauli group size eight, and three universal gates. Researchers deriving quantum computation depth bounds from the RS framework would cite this certificate when instantiating depth calculations. The declaration is a pure structure definition with no proof obligations or computational content.
Claim. A structure asserting that the cardinality of the set of quantum gate types equals 5, the size of the single-qubit Pauli group equals $2^3$, and the number of gates in a universal set equals 3.
background
The module Quantum Computing Depth from RS (RS_PAT_043 / B15) treats quantum computation as sequences of J-cost-minimizing recognition operations. QuantumGateType is the inductive type with five constructors (pauli, clifford, tGate, cnot, toffoli). pauliGroupSize is defined as 8 and universalGates as 3, matching the eight-tick octave and spatial dimension D=3 from the forcing chain.
proof idea
Structure definition that directly declares the three fields; no tactics or lemmas are applied. The equalities are supplied by the sibling definitions quantumGateTypeCount, pauliGroupSize_2cubed, and universalGates_eq_D at the point of instantiation.
why it matters
Supplies the bundled certificate instantiated by quantumComputingDepthCert, which closes the RS_PAT_043 claim. It directly encodes the T7 eight-tick octave (period 2^3) and T8 D=3 landmarks, together with the five gate types required for universal computation in the Recognition Science setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.