oscillatoryDynamicsCert
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.
claimLet $ω_{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 in Recognition Science
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.
scope and limits
- Does not derive the quadratic J-cost expansion; that step precedes this module.
- Does not compute explicit numerical spectra; only sign and ordering are asserted.
- Does not address anharmonic corrections or higher-order terms in the J-cost expansion.
- Does not establish the value of φ itself; that is supplied by upstream uniqueness results.
Lean usage
theorem cert_nonempty : Nonempty OscillatoryDynamicsCert := ⟨oscillatoryDynamicsCert⟩formal statement (Lean)
68noncomputable def oscillatoryDynamicsCert : OscillatoryDynamicsCert where
69 omega_pos := omega_pos
proof body
Definition body.
70 energy_pos := energy_pos
71 energy_increasing := energy_increasing
72