omega_RS
plain-language theorem explainer
Angular frequency omega_RS is defined as the square root of phi to the fifth power. Derivations of quantized energy levels in the oscillatory dynamics module cite it when converting the J-cost Hessian into SHO parameters. The assignment is a direct one-line computation using the real square root on phi^5.
Claim. $ω_{RS} := √(φ^5) = φ^{5/2}$
background
The Oscillatory Dynamics module shows that the simple harmonic oscillator potential arises as the leading-order expansion of J-cost near equilibrium: J(1 + ε) = ε²/2 + O(ε³). With spring constant k = J''(1) = 1 and coherent mass m = φ^{-5} in RS units, the frequency is ω = 1/√m = φ^{5/2}. This definition supplies the concrete value used for all subsequent energy calculations in the module.
proof idea
Direct definition that assigns omega_RS to Real.sqrt applied to phi raised to the fifth power. No lemmas or tactics are invoked beyond the built-in square-root operation on positive reals.
why it matters
This definition supplies the angular frequency required by energy_level and the OscillatoryDynamicsCert structure. It implements the ω_RS step that converts the J-cost Hessian into the SHO energy levels E_n = φ^{-5/2}(n + 1/2). It anchors the module's derivation of harmonic motion from the Recognition Composition Law and the phi-ladder constants ħ = φ^{-5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.