InflatonPotentialCert

formal source

  97  have h2_ne : (2 : ℝ) * (1 + phi_inf) ≠ 0 := by positivity
  98  field_simp [h_ne, h2_ne]
  99
 100structure InflatonPotentialCert where
 101  vacuum : V 0 = 0
 102  nonneg : ∀ {phi_inf : ℝ}, -1 < phi_inf → 0 ≤ V phi_inf
 103  pos_off_vacuum :
 104    ∀ {phi_inf : ℝ}, phi_inf ≠ 0 → -1 < phi_inf → 0 < V phi_inf
 105  reciprocal_symm :
 106    ∀ {phi_inf : ℝ}, -1 < phi_inf →
 107      V phi_inf = V ((1 + phi_inf)⁻¹ - 1)
 108  quadratic_form :
 109    ∀ {phi_inf : ℝ}, -1 < phi_inf →
 110      V phi_inf = phi_inf ^ 2 / (2 * (1 + phi_inf))
 111
 112/-- Inflaton-potential certificate. -/
 113def inflatonPotentialCert : InflatonPotentialCert where
 114  vacuum := V_vacuum
 115  nonneg := V_nonneg
 116  pos_off_vacuum := V_pos_off_vacuum
 117  reciprocal_symm := V_reciprocal_symm
 118  quadratic_form := V_eq_quadratic
 119
 120end
 121end InflatonPotentialFromJCost
 122end Cosmology
 123end IndisputableMonolith