MolecularPhysicsCert
plain-language theorem explainer
MolecularPhysicsCert records three invariants for molecular spectra under Recognition Science: exactly five energy levels via the inductive enumeration, constant scaling by the golden ratio phi between consecutive phi-ladder rungs, and ten total states from five levels times two polarizations. Molecular spectroscopists or quantum chemists building RS-derived models would cite this certificate to verify phi-ladder consistency. The declaration is a direct structure definition that assembles the three fields from the module's sibling computations.
Claim. A structure certifying molecular physics from recognition science asserts that the set of molecular energy levels has cardinality five, that the ratio of energy at rung $k+1$ to energy at rung $k$ equals the golden ratio $phi$ for every natural number $k$, and that the total number of molecular states equals ten.
background
The module sets the local theoretical setting as deriving molecular physics from RS with five canonical levels (electronic, vibrational, rotational, translational, spin) equal to configDim D and adjacent levels scaling by phi on the recognition ladder. MolecularEnergyLevel is the inductive type with exactly those five constructors. energyAtRung is defined by $phi^k$ for rung index $k$. totalMolecularStates is the arithmetic product $5 times 2$.
proof idea
The structure is introduced directly by its three fields. The cardinality field applies the Fintype instance on the inductive MolecularEnergyLevel. The ratio field invokes the energyAtRung definition to state the constant phi scaling. The total field applies the totalMolecularStates definition. No further tactics or lemmas are used.
why it matters
This structure is the type of the molecularPhysicsCert definition in the same module, which populates the fields from molecularEnergyCount, energyRatio, and totalStates_10. It encodes the module's A1 Chemistry/Physics Depth claim that five levels times two polarizations yield ten states under the phi-ladder forced by T6. The declaration supplies the zero-sorry certificate linking RS constants to molecular spectra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.