QuantumMolecularState
QuantumMolecularState is the Cartesian product of the five molecular energy modes and five quantum gate families, yielding a discrete state space of size 25. Cross-domain arguments in Recognition Science cite it to bound circuit depth for molecular targets. The declaration is a direct one-line abbreviation of the product type that immediately inherits finite cardinality from its factors.
claimLet $E$ be the finite set of molecular energy levels with elements electronic, vibrational, rotational, translational, spin. Let $G$ be the finite set of quantum gate types with elements Pauli, Clifford, T-gate, CNOT, Toffoli. The quantum molecular state space is the Cartesian product $E × G$.
background
The module CrossDomain.QuantumMolecularBound frames a structural claim that any state reachable by a quantum circuit on a molecular substrate has cardinality 5 × 5 = 25. MolecularEnergyLevel is the inductive type whose five constructors label the distinct energy modes (electronic, vibrational, rotational, translational, spin) and derives DecidableEq together with Fintype. QuantumGateType is the parallel inductive type whose five constructors label the gate families (pauli, clifford, tGate, cnot, toffoli) and likewise derives the same instances.
proof idea
The declaration is a one-line abbreviation that directly forms the Cartesian product of MolecularEnergyLevel and QuantumGateType. No lemmas or tactics are invoked; the resulting type inherits its Fintype instance from the product of two finite types.
why it matters in Recognition Science
QuantumMolecularState supplies the state space whose cardinality is computed by the downstream theorem stateCount, which establishes Fintype.card QuantumMolecularState = 25. It is also used to build the QuantumMolecularBoundCert structure that packages the count, the inequality 2^5 ≥ 25, and the surjectivity of the two projections. Within the Recognition Science framework this realizes the cross-domain bound between molecular physics and quantum computing depth, confirming that the 25-state space fits inside a five-layer gate circuit as required by the phi-ladder decomposition.
scope and limits
- Does not assert that the five listed energy modes exhaust all molecular excitations.
- Does not prove circuit reachability or depth bounds; those are separate theorems.
- Does not incorporate continuous parameters or infinite-dimensional Hilbert spaces.
- Does not reference J-cost, defectDist, or the core T0-T8 forcing chain.
formal statement (Lean)
33abbrev QuantumMolecularState : Type := MolecularEnergyLevel × QuantumGateType
proof body
Definition body.
34