slowRollEpsilon

formal source

  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 -/
  90
  91/-- Number of e-foldings of inflation.
  92    N = ∫ (V/V') dφ ≈ ∫ φ dφ for large φ.
  93    We need N ≈ 60 to solve the horizon problem. -/
  94noncomputable def eFoldings (φ_start φ_end : ℝ) : ℝ :=
  95  -- For J-cost potential: N ≈ (φ_start² - φ_end²) / 4
  96  (φ_start^2 - φ_end^2) / 4
  97
  98/-- **THEOREM (60 e-Foldings)**: Starting from φ ≈ 16, we get N ≈ 60.