energy_level
plain-language theorem explainer
Energy levels in the Recognition Science harmonic oscillator are defined by E_n = ω_RS / φ^5 ⋅ (n + 1/2), which equals φ^{-5/2} (n + 1/2). Researchers deriving quantized spectra from J-cost expansions in oscillatory patterns would cite this expression. The definition is a direct algebraic substitution of the precomputed angular frequency omega_RS into the standard SHO formula.
Claim. The energy level for nonnegative integer n is E_n = (ω_RS / φ^5) ⋅ (n + 1/2), where ω_RS = √(φ^5) and the expression simplifies to φ^{-5/2} (n + 1/2).
background
The Oscillatory Dynamics module derives the simple harmonic oscillator from the quadratic leading term of J-cost near equilibrium: J(1 + ε) ≈ ε²/2, with Hessian calibration k = 1. In RS units the effective mass is φ^{-5}, so the angular frequency is ω_RS = φ^{5/2}. The upstream definition omega_RS supplies exactly this value as Real.sqrt (phi ^ 5) and records its positivity.
proof idea
The definition is a direct one-line algebraic expression that multiplies omega_RS by the factor 1/φ^5 and the shifted index (n + 1/2). No lemmas or tactics are invoked beyond the built-in real arithmetic.
why it matters
This supplies the explicit spectrum required by the downstream structure OscillatoryDynamicsCert, whose three fields certify positivity and strict increase of the levels. It completes the energy_levels_phi item in the module's structural theorem list and connects the J-cost Hessian directly to the quantized energies used in the Recognition framework's phi-ladder scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.