energy_level
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the SHO approximation from J-cost; that occurs in sho_from_jcost.
- Does not establish positivity or monotonicity; those are proved separately in energy_pos and energy_increasing.
- Does not incorporate anharmonic corrections or higher-order J-cost terms.
- Does not assign numerical values or physical units beyond the symbolic RS form.
Lean usage
theorem demo (n : ℕ) : 0 < energy_level n := energy_pos nformal statement (Lean)
48def energy_level (n : ℕ) : ℝ := omega_RS / phi ^ 5 * ((n : ℝ) + 1/2)
proof body
Definition body.
49
50/-- `energy_level n > 0`. -/