pith. machine review for the scientific record. sign in
structure definition def or abbrev high

QuantumComputingDepthCert

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  35structure QuantumComputingDepthCert where
  36  five_gates : Fintype.card QuantumGateType = 5
  37  pauli_8 : pauliGroupSize = 2 ^ 3
  38  universal_D : universalGates = 3
  39

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.