molecularEnergyCount
plain-language theorem explainer
The theorem establishes that the finite type of molecular energy levels contains exactly five elements corresponding to the canonical states in Recognition Science. Researchers modeling quantum molecular systems from the phi-ladder would cite this cardinality when counting discrete levels before deriving ratios or total states. The proof is a direct one-line computation via the decide tactic on the Fintype instance induced by the five-constructor inductive definition.
Claim. The finite type of molecular energy levels, consisting of the electronic, vibrational, rotational, translational, and spin states, has cardinality 5.
background
The module defines five canonical molecular energy levels as electronic, vibrational, rotational, translational, and spin, setting configDim D equal to 5. In Recognition Science each level corresponds to a rung on the phi-ladder of recognition energy, with adjacent levels related by the golden ratio phi. The inductive type MolecularEnergyLevel enumerates these five cases and derives DecidableEq, Repr, BEq, and Fintype instances directly from the constructors.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic computes Fintype.card by enumerating the five constructors of the inductive type MolecularEnergyLevel and confirming the cardinality equals 5.
why it matters
This result supplies the five_levels field inside the molecularPhysicsCert bundle and is rewritten into the proof that molecularQuantumStateClasses equals 25. It anchors the molecular physics layer of the Recognition framework by fixing the number of energy levels at five, consistent with the five-level structure and the 5 times 2 polarisations yielding ten total states. The declaration closes a direct counting step before phi-ratio and total-state derivations are applied downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.