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

potential_min_at_one

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)

  51theorem potential_min_at_one (φ : ℝ) (hφ : φ > 0) :
  52    inflatonPotential φ hφ ≥ inflatonPotential 1 (by norm_num : (1 : ℝ) > 0) := by

proof body

Term-mode proof.

  53  unfold inflatonPotential
  54  have h1 : Jcost 1 = 0 := Cost.Jcost_unit0
  55  rw [h1]
  56  exact Cost.Jcost_nonneg hφ
  57
  58/-- **THEOREM**: The potential is positive (except at minimum). -/

depends on (13)

Lean names referenced from this declaration's body.