`G`

definition

show as: view math explainer →

module: IndisputableMonolith.Gravity.JCostInflaton
domain: Gravity
line: 58 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gravity.JCostInflaton on GitHub at line 58.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  55    G(t) = J(eᵗ) = cosh(t) − 1.
  56    This is exact (not an approximation): J(x) = ½(x + x⁻¹) − 1 and
  57    ½(eᵗ + e⁻ᵗ) = cosh(t). -/
  58def G (t : ℝ) : ℝ := Real.cosh t - 1
  59
  60/-- G is the J-cost in log coordinates. -/
  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 : ℝ) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.