slowRollEta

formal source

  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.
  99    (256 - 4) / 4 = 252 / 4 = 63 ≈ 60 -/
 100theorem sixty_efolds :
 101    eFoldings 16 2 = 63 := by
 102  unfold eFoldings
 103  norm_num
 104
 105/-! ## Solving Cosmological Problems -/
 106
 107/-- **THEOREM (Horizon Problem Solved)**: Inflation stretches causal regions,