pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Physics.QuantumComputingDepthFromRS

show as:
view Lean formalization →

The module derives quantum computing depth bounds from Recognition Science by proving the single-qubit Pauli group has eight elements and defining five gate types. It supports calculations showing 25 state classes fit within 2^5 depth. Researchers modeling RS-constrained molecular simulations cite it for the gate cardinality and octave match. The structure consists of direct definitions and equalities such as pauliGroupSize_2cubed without extended tactic sequences.

claimThe single-qubit Pauli group has cardinality $8$. There exist five quantum gate types, and the universal gate set satisfies $|U| = D = 3$.

background

This module operates in the Physics domain and introduces quantum gate types to link the Recognition Science forcing chain to computation. Key objects include QuantumGateType (enumerating five classes) and pauliGroupSize (the order of the single-qubit Pauli group). It draws on the eight-tick octave (T7) and D = 3 (T8) from the upstream chain to constrain gate counts.

proof idea

This is a definition module, no proofs. It supplies supporting constants and lemmas such as quantumGateTypeCount, pauliGroupSize_2cubed, and universalGates_eq_D to prepare the depth certificate.

why it matters in Recognition Science

This module supplies the gate foundations for the C4 claim in QuantumMolecularDesignDepthC4, where five energy levels times five gate types produce 25 classes addressable by 5-bit depth. It closes the quantum side of the RS framework by matching the Pauli order to the eight-tick octave and D = 3.

scope and limits

used by (1)

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

declarations in this module (8)