`DetuningStopsRunaway`

proved

show as: view math explainer →

module: IndisputableMonolith.Safety.DampeningField
domain: Safety
line: 41 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Safety.DampeningField on GitHub at line 41.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  38  Real.exp (-phase_error ^ 2)
  39
  40/-- Safety Theorem: De-tuning prevents runaway. -/
  41theorem DetuningStopsRunaway (rpm rpm_limit : ℝ) :
  42  let slip := Governor rpm rpm_limit
  43  let eff := Efficiency slip
  44  rpm > rpm_limit → eff < 1 := by
  45  intro slip eff h_over
  46  simp [slip, Governor, h_over]
  47  -- exp(-0.1^2) = exp(-0.01) < 1
  48  exact Real.exp_lt_one_iff.mpr (by norm_num)
  49
  50end DampeningField
  51end Safety
  52end IndisputableMonolith

papers checked against this theorem

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