theorem proved term proof

`potential_positive`

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

formal statement (Lean)

  59theorem potential_positive (φ : ℝ) (hφ : φ > 0) (hne : φ ≠ 1) :
  60    inflatonPotential φ hφ > 0 := by

proof body

Term-mode proof.

  61  unfold inflatonPotential
  62  exact Cost.Jcost_pos_of_ne_one φ hφ hne
  63
  64/-! ## Slow Roll Parameters -/
  65
  66/-- First slow-roll parameter ε = (V'/V)² / 2.
  67    Inflation requires ε < 1. -/

depends on (8)

Lean names referenced from this declaration's body.

inflatonPotential in IndisputableMonolith.Cosmology.Inflation decl_use
V in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost decl_use
Jcost_pos_of_ne_one in IndisputableMonolith.Cost decl_use
Jcost_pos_of_ne_one in IndisputableMonolith.Cost.JcostCore decl_use
V in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Jcost_pos_of_ne_one in IndisputableMonolith.Information.LocalCache decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
V in IndisputableMonolith.RRF.Core.Glossary decl_use