OscillatoryDynamicsCert
plain-language theorem explainer
OscillatoryDynamicsCert bundles the positivity of the RS angular frequency together with the positivity and strict monotonicity of the derived energy levels. Researchers working on the harmonic-oscillator limit of J-cost patterns cite the certificate to invoke the complete SHO spectrum at once. The structure is populated by direct reference to the three supporting theorems that establish each field separately.
Claim. Let $E_n = φ^{-5/2}(n + 1/2)$ with $ω_{RS} = φ^{5/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 starts from the local expansion of J-cost near equilibrium, J(1 + ε) ≈ ε²/2, which supplies the SHO potential with spring constant 1. In RS units the mass scale is φ^{-5}, so the angular frequency is defined as ω_RS = √(φ^5) = φ^{5/2}. Energy levels are then given by the standard formula E_n = ω_RS / φ^5 · (n + 1/2), which reduces to φ^{-5/2}(n + 1/2). Upstream results supply the three facts packaged by the certificate: omega_pos proves ω_RS > 0, energy_pos proves E_n > 0, and energy_increasing proves the sequence is strictly increasing.
proof idea
The structure is a direct bundling of the three upstream theorems omega_pos, energy_pos, and energy_increasing. No additional tactics or reductions are performed; each field is filled by naming the corresponding lemma.
why it matters
The certificate is the master container for the SHO properties derived from J-cost and feeds the construction oscillatoryDynamicsCert together with the inhabited theorem. It completes the structural block that confirms the energy ladder is positive and ordered, consistent with the phi-ladder scaling and the eight-tick octave in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.