energy_increasing
plain-language theorem explainer
Energy levels E_n = φ^{-5/2}(n + 1/2) in the Recognition Science oscillator are strictly monotonic in the quantum number n. Researchers assembling the master certificate for oscillatory dynamics or ordering the phi-ladder spectrum cite this result. The proof reduces the inequality to positivity of the angular frequency by unfolding the energy definition and invoking linear arithmetic.
Claim. For every natural number $n$, the energy level $E_n = φ^{-5/2}(n + 1/2)$ satisfies $E_n < E_{n+1}$.
background
The module derives the simple harmonic oscillator from the second-order expansion of the J-cost function near equilibrium, where J(1 + ε) ≈ ε²/2. In RS units the angular frequency is ω_RS = φ^{5/2}, yielding discrete energy levels E_n = ω_RS / φ^5 · (n + 1/2) = φ^{-5/2}(n + 1/2). The upstream definition energy_level supplies the explicit formula while the theorem omega_pos establishes that the frequency is positive.
proof idea
The proof is a one-line wrapper that unfolds the definition of energy_level, applies mul_lt_mul_of_pos_left using the positivity of omega_RS together with phi_pos, then finishes with push_cast and linarith.
why it matters
This theorem supplies the monotonicity field required by the structure OscillatoryDynamicsCert, which certifies the full set of oscillator properties including positive frequency and positive energies. It closes the structural theorem block for the J-cost to SHO reduction, ensuring the spectrum is ordered as required for the eight-tick octave and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.