V_nonneg

formal source

  50  exact Cost.Jcost_unit0
  51
  52/-- `V` is nonnegative throughout the physical domain `φ_inf > -1`. -/
  53theorem V_nonneg {phi_inf : ℝ} (h : -1 < phi_inf) : 0 ≤ V phi_inf := by
  54  unfold V
  55  apply Cost.Jcost_nonneg
  56  linarith
  57
  58/-- `V` is strictly positive away from the vacuum. -/
  59theorem V_pos_off_vacuum {phi_inf : ℝ} (h_ne : phi_inf ≠ 0) (h_gt : -1 < phi_inf) :
  60    0 < V phi_inf := by
  61  unfold V
  62  apply Cost.Jcost_pos_of_ne_one (1 + phi_inf) (by linarith)
  63  intro h; apply h_ne; linarith
  64
  65/-- Reciprocal symmetry of `V`: the potential is symmetric under
  66`(1 + φ_inf) ↔ 1/(1 + φ_inf)`. The same reciprocal symmetry that
  67governs every other RS J-cost identity also constrains the inflaton
  68potential, making the slow-roll trajectory canonical and universal. -/
  69theorem V_reciprocal_symm {phi_inf : ℝ} (h : -1 < phi_inf) :
  70    V phi_inf = V ((1 + phi_inf)⁻¹ - 1) := by
  71  unfold V
  72  have h_arg_pos : (0 : ℝ) < 1 + phi_inf := by linarith
  73  have h_eq : 1 + ((1 + phi_inf)⁻¹ - 1) = (1 + phi_inf)⁻¹ := by ring
  74  rw [h_eq]
  75  exact Cost.Jcost_symm h_arg_pos
  76
  77/-- The squared-form expression for `V`:
  78`V(φ_inf) = φ_inf² / (2 (1 + φ_inf))`. Standard quadratic potential
  79near the vacuum, deviates at large displacement. -/
  80theorem V_eq_quadratic {phi_inf : ℝ} (h : -1 < phi_inf) :
  81    V phi_inf = phi_inf ^ 2 / (2 * (1 + phi_inf)) := by
  82  unfold V
  83  have h_arg_pos : (0 : ℝ) < 1 + phi_inf := by linarith