omega_pos
plain-language theorem explainer
Recognition Science angular frequency omega_RS is shown to be positive. Workers on the J-cost reduction to the harmonic oscillator cite it to guarantee that all energy levels E_n remain positive and strictly increasing. The proof is a term-mode one-liner that invokes square-root positivity on phi raised to the fifth power.
Claim. $0 < ω_{RS}$ where $ω_{RS} := √(φ^5)$.
background
The module shows that the simple harmonic oscillator arises as the leading-order expansion of J-cost near the equilibrium point 1. For small ε, J(1 + ε) ≈ ε²/2, fixing the spring constant at 1. With coherent mass m = φ^{-5} the angular frequency is then ω_RS = φ^{5/2} = √(φ^5).
proof idea
The proof is a term-mode one-liner. It applies Real.sqrt_pos.mpr directly to the result of pow_pos phi_pos 5, using the upstream definition of omega_RS as the square root of phi to the fifth.
why it matters
It supplies the positivity field required by the OscillatoryDynamicsCert structure and is invoked by energy_pos and energy_increasing. The result completes the positivity step for the RS energy spectrum E_n = φ^{-5/2}(n + 1/2) listed in the module documentation, ensuring the harmonic-oscillator reduction of J-cost yields a well-ordered spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.