pith. sign in
module module high

IndisputableMonolith.Physics.QuantumComputingDepthFromRS

show as:
view Lean formalization →

Module supplies quantum gate primitives and counts for Recognition Science, proving the single-qubit Pauli group has eight elements and universal gate sets of size three. Researchers on quantum depth bounds cite these facts when indexing state classes. Arguments proceed by direct enumeration of the eight Pauli matrices and equality to the spatial dimension D.

claimThe single-qubit Pauli group satisfies $|P_1|=8$. Universal gate sets exist with cardinality $D=3$.

background

Module resides in the Physics domain and imports Mathlib. It defines QuantumGateType as an enumeration of gate operations, quantumGateTypeCount as its cardinality, pauliGroupSize as the order of the single-qubit Pauli group, and universalGates with the equality universalGates_eq_D. The module doc states that the Pauli group (single qubit) has 8 elements. These objects connect to the eight-tick octave (T7) and the forcing-chain result D=3 (T8).

proof idea

This is a definition module. It contains direct enumerations establishing pauliGroupSize by listing the eight elements and the equality universalGates_eq_D that identifies the gate count with spatial dimension D.

why it matters in Recognition Science

Feeds the C4 quantum molecular design depth theorem, which uses five gate types and five energy levels to obtain 25 state classes addressable in five bits. It supplies the gate-count infrastructure that links the eight-element Pauli group to the D=3 result from the unified forcing chain.

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)