MolecularEnergyLevel
plain-language theorem explainer
MolecularEnergyLevel enumerates the five standard excitation modes of a molecule in the Recognition Science decomposition. Cross-domain proofs of quantum molecular bounds cite this enumeration to fix the molecular factor of the 5-by-5 state space. The declaration is an inductive definition that introduces the five constructors and derives the Fintype instance automatically.
Claim. Let $M$ be the set of molecular energy levels. Then $M$ consists of the five elements electronic, vibrational, rotational, translational and spin.
background
The CrossDomain.QuantumMolecularBound module pairs molecular energy levels with quantum gate types to obtain a 25-element state space. The module document states that 25 states are reachable in at most five two-qubit gate layers because $2^5 = 32$. The same inductive type first appears in MolecularPhysicsFromRS, where it is used to certify five levels and a phi-ratio between successive energy rungs.
proof idea
The declaration is an inductive definition that introduces the five constructors directly and derives DecidableEq, Repr, BEq and Fintype via the deriving clause.
why it matters
This enumeration supplies the molecular factor in the 5 × 5 = 25 state-space cardinality that bounds gate depth by five layers. It is used by energyCount to obtain Fintype.card = 5, by QuantumMolecularState to form the product type, and by gate_surj to establish surjectivity onto gate types. The construction closes the C4 cross-domain claim that no molecular target requires more than five gate layers per phi-rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.