3.1. Higgs potential🔗

3.1.1. Introduction

The Higgs potential is a key part of the Standard Model of particle physics. It is a scalar potential which is used to give mass to the elementary particles. The Higgs potential is a polynomial of degree four in the Higgs field.

3.1.2. The Higgs field

Definition (StandardModel.HiggsVec):

The vector space HiggsVec is defined to be the complex Euclidean space of dimension 2. For a given spacetime point a Higgs field gives a value in HiggsVec.

Show Lean signature:
StandardModel.HiggsVec : Type
Definition (StandardModel.HiggsBundle):

The HiggsBundle is defined as the trivial vector bundle with base SpaceTime and fiber HiggsVec. Thus as a manifold it corresponds to ℝ⁴ × ℂ².

Show Lean signature:
StandardModel.HiggsBundle : SpaceTime → Type
Definition (StandardModel.HiggsField):

The type HiggsField is defined such that elements are smooth sections of the trivial vector bundle HiggsBundle. Such elements are Higgs fields. Since HiggsField is trivial as a vector bundle, a Higgs field is equivalent to a smooth map from SpaceTime to HiggsVec.

Show Lean signature:
StandardModel.HiggsField : Type

3.1.3. The Higgs potential

Definition (StandardModel.HiggsField.Potential):

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 λ.

Show Lean signature:
StandardModel.HiggsField.Potential : Type
Definition (StandardModel.HiggsField.normSq):

Given an element φ of HiggsField, normSq φ is defined as the the function SpaceTime → ℝ obtained by taking the square norm of the pointwise Higgs vector. In other words, normSq φ x = ‖φ x‖ ^ 2.

The notation ‖φ‖_H^2 is used for the normSq φ.

Show Lean signature:
StandardModel.HiggsField.normSq (φ : HiggsField)
    : SpaceTime → ℝ
Definition (StandardModel.HiggsField.Potential.toFun):

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.

Show Lean signature:
StandardModel.HiggsField.Potential.toFun
    (P : Potential) (φ : HiggsField)
    (x : SpaceTime) : ℝ

3.1.3.1. Properties of the Higgs potential

Lemma (StandardModel.HiggsField.Potential.neg_𝓵_quadDiscrim_zero_bound):

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

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

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

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

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

Show Lean signature:
StandardModel.HiggsField.Potential.pos_𝓵_quadDiscrim_zero_bound
    (P : Potential) (h : 0 < P.𝓵)
    (φ : HiggsField) (x : SpaceTime)
    : -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x
Lemma (StandardModel.HiggsField.Potential.neg_𝓵_sol_exists_iff):

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.

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

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.

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

3.1.3.2. Boundedness of the Higgs potential

Definition (StandardModel.HiggsField.Potential.IsBounded):

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.

Show Lean signature:
StandardModel.HiggsField.Potential.IsBounded
    (P : Potential) : Prop
Lemma (StandardModel.HiggsField.Potential.isBounded_𝓵_nonneg):

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

Show Lean signature:
StandardModel.HiggsField.Potential.isBounded_𝓵_nonneg
    (P : Potential) (h : P.IsBounded) : 0 ≤ P.𝓵
Lemma (StandardModel.HiggsField.Potential.isBounded_of_𝓵_pos):

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

Show Lean signature:
StandardModel.HiggsField.Potential.isBounded_of_𝓵_pos
    (P : Potential) (h : 0 < P.𝓵) : P.IsBounded

3.1.3.3. Maximum and minimum of the Higgs potential

Lemma (StandardModel.HiggsField.Potential.isMaxOn_iff_field_of_𝓵_neg):

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.

Show Lean signature:
StandardModel.HiggsField.Potential.isMaxOn_iff_field_of_𝓵_neg
    (P : Potential) (h𝓵 : P.𝓵 < 0)
    (φ : HiggsField) (x : SpaceTime)
    : IsMaxOn
        (fun x =>
          match x with
          | (φ, x) => P.toFun φ x)
        Set.univ (φ, x) ↔
      P.μ2 ≤ 0 ∧ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) ∨
        0 < P.μ2 ∧ φ x = 0
Theorem (StandardModel.HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos):

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.

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