energy_increasing
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit energy formula from first principles.
- Does not address degeneracy or higher-dimensional oscillators.
- Does not connect to the mass formula or Berry threshold.
Lean usage
example : energy_level 0 < energy_level 1 := energy_increasing 0formal statement (Lean)
58theorem energy_increasing (n : ℕ) : energy_level n < energy_level (n + 1) := by
proof body
Term-mode proof.
59 unfold energy_level
60 apply mul_lt_mul_of_pos_left _ (div_pos omega_pos (pow_pos phi_pos 5))
61 push_cast; linarith
62