The potential of the two Higgs doublet model

i. Overview

In this file we give the potential of the two Higgs doublet model (2HDM) in Lean, and derive properties thereof.

Note: This file is currently independent of TwoHiggsDoublet, it is a TODO to integrate them.

structure TwoHDM.Potential : Type

The parameters of the Two Higgs doublet model potential.

• m₁₁2 : ℝ

  The parameter corresponding to m₁₁² in the 2HDM potential.

• m₂₂2 : ℝ

  The parameter corresponding to m₂₂² in the 2HDM potential.

• m₁₂2 : ℂ

  The parameter corresponding to m₁₂² in the 2HDM potential.

• 𝓵₁ : ℝ

  The parameter corresponding to λ₁ in the 2HDM potential.

• 𝓵₂ : ℝ

  The parameter corresponding to λ₂ in the 2HDM potential.

• 𝓵₃ : ℝ

  The parameter corresponding to λ₃ in the 2HDM potential.

• 𝓵₄ : ℝ

  The parameter corresponding to λ₄ in the 2HDM potential.

• 𝓵₅ : ℂ

  The parameter corresponding to λ₅ in the 2HDM potential.

• 𝓵₆ : ℂ

  The parameter corresponding to λ₆ in the 2HDM potential.

• 𝓵₇ : ℂ

  The parameter corresponding to λ₇ in the 2HDM potential.

def TwoHDM.Potential.toFun (P : Potential) (Φ1 Φ2 : StandardModel.HiggsField) (x : SpaceTime) : ℝ

The potential of the two Higgs doublet model.

Equations

• One or more equations did not get rendered due to their size.

def TwoHDM.Potential.zero : Potential

The potential where all parameters are zero.

Equations

• TwoHDM.Potential.zero = { m₁₁2 := 0, m₂₂2 := 0, m₁₂2 := 0, 𝓵₁ := 0, 𝓵₂ := 0, 𝓵₃ := 0, 𝓵₄ := 0, 𝓵₅ := 0, 𝓵₆ := 0, 𝓵₇ := 0 }

theorem TwoHDM.Potential.swap_fields (P : Potential) (Φ1 Φ2 : StandardModel.HiggsField) : P.toFun Φ1 Φ2 = { m₁₁2 := P.m₂₂2, m₂₂2 := P.m₁₁2, m₁₂2 := (starRingEnd ℂ) P.m₁₂2, 𝓵₁ := P.𝓵₂, 𝓵₂ := P.𝓵₁, 𝓵₃ := P.𝓵₃, 𝓵₄ := P.𝓵₄, 𝓵₅ := (starRingEnd ℂ) P.𝓵₅, 𝓵₆ := (starRingEnd ℂ) P.𝓵₇, 𝓵₇ := (starRingEnd ℂ) P.𝓵₆ }.toFun Φ2 Φ1

theorem TwoHDM.Potential.right_zero (P : Potential) (Φ1 : StandardModel.HiggsField) : P.toFun Φ1 0 = { μ2 := -P.m₁₁2, 𝓵 := P.𝓵₁ / 2 }.toFun Φ1

If Φ₂ is zero the potential reduces to the Higgs potential on Φ₁.

theorem TwoHDM.Potential.left_zero (P : Potential) (Φ2 : StandardModel.HiggsField) : P.toFun 0 Φ2 = { μ2 := -P.m₂₂2, 𝓵 := P.𝓵₂ / 2 }.toFun Φ2

If Φ₁ is zero the potential reduces to the Higgs potential on Φ₂.

theorem TwoHDM.Potential.neg_left (P : Potential) (Φ1 Φ2 : StandardModel.HiggsField) : P.toFun (-Φ1) Φ2 = { m₁₁2 := P.m₁₁2, m₂₂2 := P.m₂₂2, m₁₂2 := -P.m₁₂2, 𝓵₁ := P.𝓵₁, 𝓵₂ := P.𝓵₂, 𝓵₃ := P.𝓵₃, 𝓵₄ := P.𝓵₄, 𝓵₅ := P.𝓵₅, 𝓵₆ := -P.𝓵₆, 𝓵₇ := -P.𝓵₇ }.toFun Φ1 Φ2

Negating Φ₁ is equivalent to negating m₁₂2, 𝓵₆ and 𝓵₇.

theorem TwoHDM.Potential.neg_right (P : Potential) (Φ1 Φ2 : StandardModel.HiggsField) : P.toFun Φ1 (-Φ2) = { m₁₁2 := P.m₁₁2, m₂₂2 := P.m₂₂2, m₁₂2 := -P.m₁₂2, 𝓵₁ := P.𝓵₁, 𝓵₂ := P.𝓵₂, 𝓵₃ := P.𝓵₃, 𝓵₄ := P.𝓵₄, 𝓵₅ := P.𝓵₅, 𝓵₆ := -P.𝓵₆, 𝓵₇ := -P.𝓵₇ }.toFun Φ1 Φ2

Negating Φ₁ is equivalent to negating m₁₂2, 𝓵₆ and 𝓵₇.

theorem TwoHDM.Potential.left_eq_right (P : Potential) (Φ1 : StandardModel.HiggsField) : P.toFun Φ1 Φ1 = { μ2 := -P.m₁₁2 - P.m₂₂2 + 2 * P.m₁₂2.re, 𝓵 := P.𝓵₁ / 2 + P.𝓵₂ / 2 + P.𝓵₃ + P.𝓵₄ + P.𝓵₅.re + 2 * P.𝓵₆.re + 2 * P.𝓵₇.re }.toFun Φ1

theorem TwoHDM.Potential.left_eq_neg_right (P : Potential) (Φ1 : StandardModel.HiggsField) : P.toFun Φ1 (-Φ1) = { μ2 := -P.m₁₁2 - P.m₂₂2 - 2 * P.m₁₂2.re, 𝓵 := P.𝓵₁ / 2 + P.𝓵₂ / 2 + P.𝓵₃ + P.𝓵₄ + P.𝓵₅.re - 2 * P.𝓵₆.re - 2 * P.𝓵₇.re }.toFun Φ1

Potential bounded from below

def TwoHDM.Potential.IsBounded (P : Potential) : Prop

The proposition on the coefficients for a potential to be bounded.

Equations

• P.IsBounded = ∃ (c : ℝ), ∀ (Φ1 Φ2 : StandardModel.HiggsField) (x : SpaceTime), c ≤ P.toFun Φ1 Φ2 x

theorem TwoHDM.Potential.isBounded_right_zero {P : Potential} (h : P.IsBounded) : { μ2 := -P.m₁₁2, 𝓵 := P.𝓵₁ / 2 }.IsBounded

theorem TwoHDM.Potential.isBounded_left_zero {P : Potential} (h : P.IsBounded) : { μ2 := -P.m₂₂2, 𝓵 := P.𝓵₂ / 2 }.IsBounded

theorem TwoHDM.Potential.isBounded_𝓵₁_nonneg {P : Potential} (h : P.IsBounded) : 0 ≤ P.𝓵₁

theorem TwoHDM.Potential.isBounded_𝓵₂_nonneg {P : Potential} (h : P.IsBounded) : 0 ≤ P.𝓵₂

theorem TwoHDM.Potential.isBounded_of_left_eq_right {P : Potential} (h : P.IsBounded) : 0 ≤ P.𝓵₁ / 2 + P.𝓵₂ / 2 + P.𝓵₃ + P.𝓵₄ + P.𝓵₅.re + 2 * P.𝓵₆.re + 2 * P.𝓵₇.re

theorem TwoHDM.Potential.isBounded_of_left_eq_neg_right {P : Potential} (h : P.IsBounded) : 0 ≤ P.𝓵₁ / 2 + P.𝓵₂ / 2 + P.𝓵₃ + P.𝓵₄ + P.𝓵₅.re - 2 * P.𝓵₆.re - 2 * P.𝓵₇.re

theorem TwoHDM.Potential.nonneg_sum_𝓵₁_to_𝓵₅_of_isBounded {P : Potential} (h : P.IsBounded) : 0 ≤ P.𝓵₁ / 2 + P.𝓵₂ / 2 + P.𝓵₃ + P.𝓵₄ + P.𝓵₅.re