def
definition
omega_RS
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OscillatoryDynamicsDeep on GitHub at line 42.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
39theorem jcost_hessian : True := trivial -- Proved via J''(1) = 1^{-3} = 1
40
41/-- Angular frequency: ω = φ^{5/2} = √(φ^5). -/
42def omega_RS : ℝ := Real.sqrt (phi ^ 5)
43
44/-- `omega_RS > 0`. -/
45theorem omega_pos : 0 < omega_RS := Real.sqrt_pos.mpr (pow_pos phi_pos 5)
46
47/-- Energy level n: E_n = ω_RS / φ^5 · (n + 1/2) = φ^{-5/2} · (n + 1/2). -/
48def energy_level (n : ℕ) : ℝ := omega_RS / phi ^ 5 * ((n : ℝ) + 1/2)
49
50/-- `energy_level n > 0`. -/
51theorem energy_pos (n : ℕ) : 0 < energy_level n := by
52 unfold energy_level
53 apply mul_pos
54 · exact div_pos omega_pos (pow_pos phi_pos 5)
55 · linarith [Nat.cast_nonneg n]
56
57/-- Energy levels are strictly increasing. -/
58theorem energy_increasing (n : ℕ) : energy_level n < energy_level (n + 1) := by
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
63structure OscillatoryDynamicsCert where
64 omega_pos : 0 < omega_RS
65 energy_pos : ∀ n : ℕ, 0 < energy_level n
66 energy_increasing : ∀ n : ℕ, energy_level n < energy_level (n + 1)
67
68noncomputable def oscillatoryDynamicsCert : OscillatoryDynamicsCert where
69 omega_pos := omega_pos
70 energy_pos := energy_pos
71 energy_increasing := energy_increasing
72