`energy_increasing`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.OscillatoryDynamicsDeep
domain: Foundation
line: 58 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.OscillatoryDynamicsDeep on GitHub at line 58.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
  79end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.