The potential of the Higgs field

We define the potential of the Higgs field.

We show that the potential is a smooth function on spacetime.

The Higgs potential

structure StandardModel.HiggsField.Potential : Type

The structure Potential is defined with two fields, μ2 corresponding to the mass-squared of the Higgs boson, and l corresponding to the coefficent of the quartic term in the Higgs potential. Note that l is usually denoted λ.

• μ2 : ℝ

  The mass-squared of the Higgs boson.

• 𝓵 : ℝ

  The quartic coupling of the Higgs boson. Usually denoted λ.

def StandardModel.HiggsField.Potential.toFun (P : Potential) (φ : HiggsField) (x : SpaceTime) : ℝ

Given a element P of Potential, P.toFun is Higgs potential. It is defined for a Higgs field φ and a spacetime point x as

-μ² ‖φ‖_H^2 x + l * ‖φ‖_H^2 x * ‖φ‖_H^2 x.

Equations

• P.toFun φ x = -P.μ2 * φ.normSq x + P.𝓵 * φ.normSq x * φ.normSq x

theorem StandardModel.HiggsField.Potential.toFun_smooth (P : Potential) (φ : HiggsField) : ContMDiff (modelWithCornersSelf ℝ SpaceTime) (modelWithCornersSelf ℝ ℝ) ⊤ fun (x : SpaceTime) => P.toFun φ x

The potential is smooth.

def StandardModel.HiggsField.Potential.neg (P : Potential) : Potential

The Higgs potential formed by negating the mass squared and the quartic coupling.

Equations

• P.neg = { μ2 := -P.μ2, 𝓵 := -P.𝓵 }

@[simp]

theorem StandardModel.HiggsField.Potential.toFun_neg (P : Potential) (φ : HiggsField) (x : SpaceTime) : P.neg.toFun φ x = -P.toFun φ x

@[simp]

theorem StandardModel.HiggsField.Potential.μ2_neg (P : Potential) : P.neg.μ2 = -P.μ2

@[simp]

theorem StandardModel.HiggsField.Potential.𝓵_neg (P : Potential) : P.neg.𝓵 = -P.𝓵

Basic properties

@[simp]

theorem StandardModel.HiggsField.Potential.toFun_zero (P : Potential) (x : SpaceTime) : P.toFun zero x = 0

theorem StandardModel.HiggsField.Potential.complete_square (P : Potential) (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) : P.toFun φ x = P.𝓵 * (φ.normSq x - P.μ2 / (2 * P.𝓵)) ^ 2 - P.μ2 ^ 2 / (4 * P.𝓵)

theorem StandardModel.HiggsField.Potential.as_quad (P : Potential) (φ : HiggsField) (x : SpaceTime) : P.𝓵 * φ.normSq x * φ.normSq x + -P.μ2 * φ.normSq x + -P.toFun φ x = 0

The quadratic equation satisfied by the Higgs potential at a spacetime point x.

theorem StandardModel.HiggsField.Potential.toFun_eq_zero_iff (P : Potential) (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) : P.toFun φ x = 0 ↔ φ x = 0 ∨ φ.normSq x = P.μ2 / P.𝓵

The Higgs potential is zero iff and only if the higgs field is zero, or the higgs field has norm-squared P.μ2 / P.𝓵, assuming P.𝓁 = 0.

The descriminant

def StandardModel.HiggsField.Potential.quadDiscrim (P : Potential) (φ : HiggsField) (x : SpaceTime) : ℝ

The discriminant of the quadratic equation formed by the Higgs potential.

Equations

• P.quadDiscrim φ x = discrim P.𝓵 (-P.μ2) (-P.toFun φ x)

theorem StandardModel.HiggsField.Potential.quadDiscrim_nonneg (P : Potential) (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) : 0 ≤ P.quadDiscrim φ x

The discriminant of the quadratic formed by the potential is non-negative.

theorem StandardModel.HiggsField.Potential.quadDiscrim_eq_sqrt_mul_sqrt (P : Potential) (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) : P.quadDiscrim φ x = √(P.quadDiscrim φ x) * √(P.quadDiscrim φ x)

theorem StandardModel.HiggsField.Potential.quadDiscrim_eq_zero_iff (P : Potential) (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) : P.quadDiscrim φ x = 0 ↔ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)

theorem StandardModel.HiggsField.Potential.quadDiscrim_eq_zero_iff_normSq (P : Potential) (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) : P.quadDiscrim φ x = 0 ↔ φ.normSq x = P.μ2 / (2 * P.𝓵)

theorem StandardModel.HiggsField.Potential.neg_𝓵_quadDiscrim_zero_bound (P : Potential) (h : P.𝓵 < 0) (φ : HiggsField) (x : SpaceTime) : P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)

For an element P of Potential, if l < 0 then the following upper bound for the potential exists

P.toFun φ x ≤ - μ2 ^ 2 / (4 * 𝓵).

theorem StandardModel.HiggsField.Potential.pos_𝓵_quadDiscrim_zero_bound (P : Potential) (h : 0 < P.𝓵) (φ : HiggsField) (x : SpaceTime) : -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x

For an element P of Potential, if 0 < l then the following lower bound for the potential exists

- μ2 ^ 2 / (4 * 𝓵) ≤ P.toFun φ x.

theorem StandardModel.HiggsField.Potential.neg_𝓵_toFun_neg (P : Potential) (h : P.𝓵 < 0) (φ : HiggsField) (x : SpaceTime) : 0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0

If P.𝓵 is negative, then if P.μ2 is greater than zero, for all space-time points, the potential is negative P.toFun φ x ≤ 0.

theorem StandardModel.HiggsField.Potential.pos_𝓵_toFun_pos (P : Potential) (h : 0 < P.𝓵) (φ : HiggsField) (x : SpaceTime) : P.μ2 < 0 ∧ 0 ≤ P.toFun φ x ∨ 0 ≤ P.μ2

If P.𝓵 is bigger then zero, then if P.μ2 is less than zero, for all space-time points, the potential is positive 0 ≤ P.toFun φ x.

theorem StandardModel.HiggsField.Potential.neg_𝓵_sol_exists_iff (P : Potential) (h𝓵 : P.𝓵 < 0) (c : ℝ) : (∃ (φ : HiggsField) (x : SpaceTime), P.toFun φ x = c) ↔ 0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)

For an element P of Potential with l < 0 and a real c : ℝ, there exists a Higgs field φ and a spacetime point x such that P.toFun φ x = c iff one of the following two conditions hold:

• 0 < μ2 and c ≤ 0. That is, if l is negative and μ2 positive, then the potential takes every non-positive value.
• or μ2 ≤ 0 and c ≤ - μ2 ^ 2 / (4 * 𝓵). That is, if l is negative and μ2 non-positive, then the potential takes every value less then or equal to its bound.

theorem StandardModel.HiggsField.Potential.pos_𝓵_sol_exists_iff (P : Potential) (h𝓵 : 0 < P.𝓵) (c : ℝ) : (∃ (φ : HiggsField) (x : SpaceTime), P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ c

For an element P of Potential with 0 < l and a real c : ℝ, there exists a Higgs field φ and a spacetime point x such that P.toFun φ x = c iff one of the following two conditions hold:

• μ2 < 0 and 0 ≤ c. That is, if l is positive and μ2 negative, then the potential takes every non-negative value.
• or 0 ≤ μ2 and - μ2 ^ 2 / (4 * 𝓵) ≤ c. That is, if l is positive and μ2 non-negative, then the potential takes every value greater then or equal to its bound.

Boundness of the potential

def StandardModel.HiggsField.Potential.IsBounded (P : Potential) : Prop

Given a element P of Potential, the proposition IsBounded P is true if and only if there exists a real c such that for all Higgs fields φ and spacetime points x, the Higgs potential corresponding to φ at x is greater then or equal toc. I.e.

∀ Φ x, c ≤ P.toFun Φ x.

Equations

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

theorem StandardModel.HiggsField.Potential.isBounded_𝓵_nonneg (P : Potential) (h : P.IsBounded) : 0 ≤ P.𝓵

Given a element P of Potential which is bounded, the quartic coefficent 𝓵 of P is non-negative.

theorem StandardModel.HiggsField.Potential.isBounded_of_𝓵_pos (P : Potential) (h : 0 < P.𝓵) : P.IsBounded

Given a element P of Potential with 0 < 𝓵, then the potential is bounded.

def StandardModel.HiggsField.Potential.isBounded_iff_of_𝓵_zero : InformalLemma

When there is no quartic coupling, the potential is bounded iff the mass squared is non-positive, i.e., for P : Potential then P.IsBounded iff P.μ2 ≤ 0. That is to say - P.μ2 * ‖φ‖_H^2 x is bounded below iff P.μ2 ≤ 0.

Equations

• StandardModel.HiggsField.Potential.isBounded_iff_of_𝓵_zero = { deps := [`StandardModel.HiggsField.Potential.IsBounded, `StandardModel.HiggsField.Potential] }

Minimum and maximum

theorem StandardModel.HiggsField.Potential.eq_zero_iff_of_μSq_nonpos_𝓵_pos (P : Potential) (h𝓵 : 0 < P.𝓵) (hμ2 : P.μ2 ≤ 0) (φ : HiggsField) (x : SpaceTime) : P.toFun φ x = 0 ↔ φ x = 0

theorem StandardModel.HiggsField.Potential.isMinOn_iff_of_μSq_nonpos_𝓵_pos (P : Potential) (h𝓵 : 0 < P.𝓵) (hμ2 : P.μ2 ≤ 0) (φ : HiggsField) (x : SpaceTime) : IsMinOn (fun (x : HiggsField × SpaceTime) => match x with | (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔ P.toFun φ x = 0

theorem StandardModel.HiggsField.Potential.isMinOn_iff_field_of_μSq_nonpos_𝓵_pos (P : Potential) (h𝓵 : 0 < P.𝓵) (hμ2 : P.μ2 ≤ 0) (φ : HiggsField) (x : SpaceTime) : IsMinOn (fun (x : HiggsField × SpaceTime) => match x with | (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔ φ x = 0

theorem StandardModel.HiggsField.Potential.isMinOn_iff_of_μSq_nonneg_𝓵_pos (P : Potential) (h𝓵 : 0 < P.𝓵) (hμ2 : 0 ≤ P.μ2) (φ : HiggsField) (x : SpaceTime) : IsMinOn (fun (x : HiggsField × SpaceTime) => match x with | (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)

theorem StandardModel.HiggsField.Potential.isMinOn_iff_field_of_μSq_nonneg_𝓵_pos (P : Potential) (h𝓵 : 0 < P.𝓵) (hμ2 : 0 ≤ P.μ2) (φ : HiggsField) (x : SpaceTime) : IsMinOn (fun (x : HiggsField × SpaceTime) => match x with | (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔ φ.normSq x = P.μ2 / (2 * P.𝓵)

theorem StandardModel.HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos (P : Potential) (h𝓵 : 0 < P.𝓵) (φ : HiggsField) (x : SpaceTime) : IsMinOn (fun (x : HiggsField × SpaceTime) => match x with | (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔ 0 ≤ P.μ2 ∧ φ.normSq x = P.μ2 / (2 * P.𝓵) ∨ P.μ2 < 0 ∧ φ x = 0

Given an element P of Potential with 0 < l, then the Higgs field φ and spacetime point x minimize the potential if and only if one of the following conditions holds

• 0 ≤ μ2 and ‖φ‖_H^2 x = μ2 / (2 * 𝓵).
• or μ2 < 0 and φ x = 0.

theorem StandardModel.HiggsField.Potential.isMaxOn_iff_isMinOn_neg (P : Potential) (φ : HiggsField) (x : SpaceTime) : IsMaxOn (fun (x : HiggsField × SpaceTime) => match x with | (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔ IsMinOn (fun (x : HiggsField × SpaceTime) => match x with | (φ, x) => P.neg.toFun φ x) Set.univ (φ, x)

theorem StandardModel.HiggsField.Potential.isMaxOn_iff_field_of_𝓵_neg (P : Potential) (h𝓵 : P.𝓵 < 0) (φ : HiggsField) (x : SpaceTime) : IsMaxOn (fun (x : HiggsField × SpaceTime) => match x with | (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔ P.μ2 ≤ 0 ∧ φ.normSq x = P.μ2 / (2 * P.𝓵) ∨ 0 < P.μ2 ∧ φ x = 0

Given an element P of Potential with l < 0, then the Higgs field φ and spacetime point x maximizes the potential if and only if one of the following conditions holds

• μ2 ≤ 0 and ‖φ‖_H^2 x = μ2 / (2 * 𝓵).
• or 0 < μ2 and φ x = 0.