V_reciprocal_symm

formal source

  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
  84  have h_arg_ne : (1 : ℝ) + phi_inf ≠ 0 := ne_of_gt h_arg_pos
  85  rw [Cost.Jcost_eq_sq h_arg_ne]
  86  congr 1
  87  ring
  88
  89/-- Quadratic small-`φ_inf` regime: at the reference point the leading
  90behaviour is `V(φ_inf) ≈ φ_inf² / 2`, the canonical slow-roll
  91quadratic-potential form with calibration coefficient `1/2`. -/
  92theorem V_quadratic_at_origin (phi_inf : ℝ) (h : -1 < phi_inf) :
  93    V phi_inf * (2 * (1 + phi_inf)) = phi_inf ^ 2 := by
  94  rw [V_eq_quadratic h]
  95  have h_pos : (0 : ℝ) < 1 + phi_inf := by linarith
  96  have h_ne : (1 : ℝ) + phi_inf ≠ 0 := ne_of_gt h_pos
  97  have h2_ne : (2 : ℝ) * (1 + phi_inf) ≠ 0 := by positivity
  98  field_simp [h_ne, h2_ne]
  99