PhysLean Notes

5.1.Ā Higgs potentialšŸ”—

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

5.1.2.Ā The Higgs field

šŸ”—def
StandardModel.HiggsVec : Type
StandardModel.HiggsVec : Type

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.

šŸ”—def
StandardModel.HiggsBundle : SpaceTime ā†’ Type
StandardModel.HiggsBundle :
  SpaceTime ā†’ Type

The HiggsBundle is defined as the trivial vector bundle with base SpaceTime and fiber HiggsVec. Thus as a manifold it corresponds to ā„ā“ Ɨ ā„‚Ā².

šŸ”—def
StandardModel.HiggsField : Type
StandardModel.HiggsField : Type

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.

5.1.3.Ā The Higgs potential

šŸ”—structure
StandardModel.HiggsField.Potential : Type
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 Ī».

Constructor

StandardModel.HiggsField.Potential.mk

Fields

Ī¼2 : ā„

The mass-squared of the Higgs boson.

š“µ : ā„

The quartic coupling of the Higgs boson. Usually denoted Ī».

šŸ”—def
StandardModel.HiggsField.normSq (Ļ† : HiggsField) : SpaceTime ā†’ ā„
StandardModel.HiggsField.normSq
  (Ļ† : HiggsField) : SpaceTime ā†’ ā„

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 Ļ†.

šŸ”—def
StandardModel.HiggsField.Potential.toFun (P : Potential)
  (Ļ† : HiggsField) (x : SpaceTime) : ā„
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.

5.1.3.1.Ā Properties of the Higgs potential

šŸ”—theorem
StandardModel.HiggsField.Potential.neg_š“µ_quadDiscrim_zero_bound
  (P : Potential) (h : P.š“µ < 0) (Ļ† : HiggsField) (x : SpaceTime) :
  P.toFun Ļ† x ā‰¤ -P.Ī¼2 ^ 2 / (4 * P.š“µ)
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
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_š“µ_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.š“µ)
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.š“µ)

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 : ā„) :
  (āˆƒ Ļ† x, P.toFun Ļ† x = c) ā†”
    P.Ī¼2 < 0 āˆ§ 0 ā‰¤ c āˆØ 0 ā‰¤ P.Ī¼2 āˆ§ -P.Ī¼2 ^ 2 / (4 * P.š“µ) ā‰¤ c
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

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.

5.1.3.2.Ā Boundedness of the Higgs potential

šŸ”—def
StandardModel.HiggsField.Potential.IsBounded (P : Potential) : Prop
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.

šŸ”—theorem
StandardModel.HiggsField.Potential.isBounded_š“µ_nonneg (P : Potential)
  (h : P.IsBounded) : 0 ā‰¤ P.š“µ
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
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.

5.1.3.3.Ā Maximum and minimum of the Higgs potential

šŸ”—theorem
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
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

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.

šŸ”—theorem
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
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

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.