oscillatoryDynamicsCert
plain-language theorem explainer
This definition assembles the positivity of the RS angular frequency together with the positivity and strict increase of the derived energy levels into a single certificate record. Researchers verifying the harmonic-oscillator limit of J-cost near equilibrium would cite it to confirm that the spectrum satisfies the required sign and ordering properties. The construction is a direct record builder that supplies three sibling theorems as field values.
Claim. Let $ω_{RS}=φ^{5/2}$ and define the energy levels by $E_n=ω_{RS}φ^{-5}(n+1/2)$. The certificate asserts $ω_{RS}>0$, $E_n>0$ for every natural number $n$, and $E_n<E_{n+1}$ for every $n$.
background
The module derives the simple-harmonic-oscillator limit from the quadratic expansion of J-cost: J(1+ε)≈ε²/2 near the fixed point, yielding spring constant k=1. In RS units the angular frequency is ω_RS=φ^{5/2} and the energy levels are E_n=φ^{-5/2}(n+1/2). The structure OscillatoryDynamicsCert packages the three required properties: positivity of ω_RS, positivity of every E_n, and strict monotonicity of the sequence E_n.
proof idea
The definition is a one-line record constructor that populates the three fields of OscillatoryDynamicsCert by direct reference to the theorems omega_pos, energy_pos and energy_increasing.
why it matters
The certificate is the single object used to prove that OscillatoryDynamicsCert is inhabited. It thereby closes the structural verification that the energy spectrum derived from J-cost satisfies the positivity and ordering axioms required by the Recognition Science treatment of the harmonic oscillator. The construction relies on the explicit RS formulas for ω_RS and the energy ladder that follow from the phi-ladder calibration of constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.