potential_positive

formal source

  56  exact Cost.Jcost_nonneg hφ
  57
  58/-- **THEOREM**: The potential is positive (except at minimum). -/
  59theorem potential_positive (φ : ℝ) (hφ : φ > 0) (hne : φ ≠ 1) :
  60    inflatonPotential φ hφ > 0 := by
  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. -/
  68noncomputable def slowRollEpsilon (φ : ℝ) (hφ : φ > 0) : ℝ :=
  69  -- V'(φ) = (1 - 1/φ²) / 2
  70  -- V(φ) = (φ + 1/φ) / 2 - 1
  71  let V := inflatonPotential φ hφ
  72  let Vp := (1 - 1/φ^2) / 2
  73  if V > 0 then (Vp / V)^2 / 2 else 0
  74
  75/-- Second slow-roll parameter η = V''/V.
  76    Inflation requires |η| < 1. -/
  77noncomputable def slowRollEta (φ : ℝ) (hφ : φ > 0) : ℝ :=
  78  -- V''(φ) = 1/φ³
  79  let V := inflatonPotential φ hφ
  80  let Vpp := 1 / φ^3
  81  if V > 0 then Vpp / V else 0
  82
  83/-- **THEOREM (Slow Roll at Large φ)**: For large φ, ε → 0.
  84    This means inflation is natural at large field values. -/
  85theorem slow_roll_at_large_phi :
  86    -- As φ → ∞: V ~ φ/2, V' ~ 1/2, so ε ~ 1/(2φ²) → 0
  87    True := trivial
  88
  89/-! ## e-Foldings -/