pith. machine review for the scientific record. sign in
theorem proved tactic proof

DetuningStopsRunaway

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  41theorem DetuningStopsRunaway (rpm rpm_limit : ℝ) :
  42  let slip := Governor rpm rpm_limit

proof body

Tactic-mode proof.

  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

depends on (2)

Lean names referenced from this declaration's body.