V_RS

formal source

  64/-- The RS Higgs effective potential at canonical mass dimension four.
  65
  66    `V_RS Λ v h = Λ⁴ · J(exp (h / v))`. -/
  67def V_RS (Λ v h : ℝ) : ℝ := Λ ^ 4 * Jcost (Real.exp (h / v))
  68
  69/-- `V_RS` reduces to `Λ⁴ · (cosh(h/v) − 1)`. -/
  70theorem V_RS_eq_cosh (Λ v h : ℝ) :
  71    V_RS Λ v h = Λ ^ 4 * (Real.cosh (h / v) - 1) := by
  72  unfold V_RS
  73  rw [Cost.Jcost_exp_cosh]
  74
  75/-- The vacuum is at `h = 0` with zero potential. -/
  76theorem V_RS_at_vacuum (Λ v : ℝ) : V_RS Λ v 0 = 0 := by
  77  rw [V_RS_eq_cosh]
  78  simp [Real.cosh_zero]
  79
  80/-- The RS potential is non-negative. -/
  81theorem V_RS_nonneg (Λ v : ℝ) (h : ℝ) : 0 ≤ V_RS Λ v h := by
  82  rw [V_RS_eq_cosh]
  83  have hΛ4 : 0 ≤ Λ ^ 4 := by positivity
  84  have hcosh : 1 ≤ Real.cosh (h / v) := Real.one_le_cosh _
  85  have : 0 ≤ Real.cosh (h / v) - 1 := by linarith
  86  exact mul_nonneg hΛ4 this
  87
  88/-! ## §2. Quartic-Order Taylor Expansion -/
  89
  90/-- The quartic Taylor approximation to the RS potential about the vacuum. -/
  91def V_RS_quartic (Λ v h : ℝ) : ℝ :=
  92  Λ ^ 4 * ((h / v) ^ 2 / 2 + (h / v) ^ 4 / 24)
  93
  94/-- Mathlib truncation lemma, restated for real `t` to depth 6.
  95
  96    `|exp t − (1 + t + t²/2 + t³/6 + t⁴/24 + t⁵/120)| ≤ exp |t| · |t|⁶`.
  97