omega_pos
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 in Recognition Science
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.
scope and limits
- Does not compute the numerical value of omega_RS.
- Does not prove the J-cost expansion to the harmonic oscillator.
- Does not address anharmonic or higher-order corrections.
- Assumes the RS-native units with phi the self-similar fixed point.
Lean usage
theorem energy_pos (n : ℕ) : 0 < energy_level n := by unfold energy_level; apply mul_pos; exact omega_pos; linarithformal statement (Lean)
45theorem omega_pos : 0 < omega_RS := Real.sqrt_pos.mpr (pow_pos phi_pos 5)
proof body
Term-mode proof.
46
47/-- Energy level n: E_n = ω_RS / φ^5 · (n + 1/2) = φ^{-5/2} · (n + 1/2). -/