energy_level

formal source

  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
  73theorem oscillatoryDynamicsCert_inhabited : Nonempty OscillatoryDynamicsCert :=
  74  ⟨oscillatoryDynamicsCert⟩
  75
  76end
  77end OscillatoryDynamicsDeep
  78end Foundation