G_at_zero

formal source

  61theorem G_is_Jcost_log (t : ℝ) : G t = Real.cosh t - 1 := rfl
  62
  63/-- G(0) = 0: the vacuum (x = 1, t = 0) has zero cost. -/
  64theorem G_at_zero : G 0 = 0 := by
  65  unfold G; simp [Real.cosh_zero]
  66
  67/-- G is non-negative: J-cost is always ≥ 0. -/
  68theorem G_nonneg (t : ℝ) : 0 ≤ G t := by
  69  unfold G
  70  linarith [Real.one_le_cosh t]
  71
  72/-- G(t) > 0 for t ≠ 0: the vacuum is the unique zero. -/
  73theorem G_pos_of_ne_zero {t : ℝ} (ht : t ≠ 0) : 0 < G t := by
  74  unfold G
  75  have : 1 < Real.cosh t := Real.one_lt_cosh.mpr ht
  76  linarith
  77
  78/-! ## Part 2: Slow-Roll Parameters from G -/
  79
  80/-- The first slow-roll parameter ε.
  81    Standard form for V = G: ε = (V')² / (2(V+1)²)
  82    For G = cosh(t) − 1: V+1 = cosh(t), V' = sinh(t).
  83    So ε = sinh²(t) / (2 cosh²(t)) = (tanh(t))² / 2. -/
  84def slow_roll_epsilon (t : ℝ) : ℝ :=
  85  Real.sinh t ^ 2 / (2 * Real.cosh t ^ 2)
  86
  87/-- ε is the sinh²/(2·cosh²) ratio — directly from definition. -/
  88theorem epsilon_formula (t : ℝ) :
  89    slow_roll_epsilon t = Real.sinh t ^ 2 / (2 * Real.cosh t ^ 2) := rfl
  90
  91/-- The second slow-roll parameter η.
  92    η = V'' / (V+1) for the normalized potential.
  93    For G: V'' = cosh(t), V+1 = cosh(t), so η = 1 always.
  94    This means the J-cost is exactly at the critical self-similar point. -/