The Higgs potential

Note Authors: Joseph Tooby-Smith

These notes are created using an interactive theorem prover called Lean. Lean formally checks definitions, theorems and proofs for correctness. These notes are part of a much larger project called PhysLean, which aims to digitalize physics into Lean. Please consider contributing to this project.

Please provide feedback or suggestions for improvements by creating a GitHub issue here.

Table of content

1. Introduction
2. The Higgs field
3. The Higgs potential
    3.1. Properties of the Higgs potential
    3.2. Boundedness of the Higgs potential
    3.3. Maximum and minimum of the Higgs potential

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.

2. The Higgs field

Definition 2.1 (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 code:

abbrev HiggsVec := EuclideanSpace ℂ (Fin 2)

Definition 2.2 (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 code:

abbrev HiggsBundle := Bundle.Trivial SpaceTime HiggsVec

Definition 2.3 (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 code:

abbrev HiggsField : Type := ContMDiffSection SpaceTime.asSmoothManifold HiggsVec ⊤ HiggsBundle

3. The Higgs potential

Definition 3.1 (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 code:

structure Potential where
  /-- The mass-squared of the Higgs boson. -/
  μ2 : ℝ
  /-- The quartic coupling of the Higgs boson. Usually denoted λ. -/
  𝓵 : ℝ

Definition 3.2 (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 code:

def normSq (φ : HiggsField) : SpaceTime → ℝ := fun x => ‖φ x‖ ^ 2

Definition 3.3 (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 code:

def toFun (φ : HiggsField) (x : SpaceTime) : ℝ :=
  - P.μ2 * ‖φ‖_H^2 x + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x

3.1. Properties of the Higgs potential

Lemma 3.4 (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 code:

lemma neg_𝓵_quadDiscrim_zero_bound (h : P.𝓵 < 0) (φ : HiggsField) (x : SpaceTime) :
    P.toFun φ x ≤ - P.μ2 ^ 2 / (4 * P.𝓵) := by
  have h1 := P.quadDiscrim_nonneg (ne_of_lt h) φ x
  simp only [quadDiscrim, discrim, even_two, Even.neg_pow] at h1
  ring_nf at h1
  rw [← neg_le_iff_add_nonneg',
    show P.𝓵 * P.toFun φ x * 4 = (- 4 * P.𝓵) * (- P.toFun φ x) by ring] at h1
  have h2 := le_neg_of_le_neg <| (div_le_iff₀' (by linarith : 0 < - 4 * P.𝓵)).mpr h1
  ring_nf at h2 ⊢
  exact h2

Lemma 3.5 (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 code:

lemma pos_𝓵_quadDiscrim_zero_bound (h : 0 < P.𝓵) (φ : HiggsField) (x : SpaceTime) :
    - P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x := by
  have h1 := P.neg.neg_𝓵_quadDiscrim_zero_bound (by simpa [neg] using h) φ x
  simp only [toFun_neg, μ2_neg, even_two, Even.neg_pow, 𝓵_neg, mul_neg, neg_div_neg_eq] at h1
  rw [neg_le, neg_div'] at h1
  exact h1

Lemma 3.6 (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 code:

lemma neg_𝓵_sol_exists_iff (h𝓵 : P.𝓵 < 0) (c : ℝ) : (∃ φ x, P.toFun φ x = c) ↔ (0 < P.μ2 ∧ c ≤ 0) ∨
    (P.μ2 ≤ 0 ∧ c ≤ - P.μ2 ^ 2 / (4 * P.𝓵)) := by
  refine Iff.intro (fun ⟨φ, x, hV⟩ => ?_) (fun h => ?_)
  · rcases P.neg_𝓵_toFun_neg h𝓵 φ x with hr | hr
    · rw [← hV]
      exact Or.inl hr
    · rw [← hV]
      exact Or.inr (And.intro hr (P.neg_𝓵_quadDiscrim_zero_bound h𝓵 φ x))
  · simp only [toFun, neg_mul]
    simp only [← sub_eq_zero, sub_zero]
    ring_nf
    let a := (P.μ2 - Real.sqrt (discrim P.𝓵 (- P.μ2) (- c))) / (2 * P.𝓵)
    have ha : 0 ≤ a := by
      simp only [discrim, even_two, Even.neg_pow, mul_neg, sub_neg_eq_add, a]
      rw [div_nonneg_iff]
      refine Or.inr (And.intro ?_ ?_)
      · rw [sub_nonpos]
        by_cases hμ : P.μ2 < 0
        · have h1 : 0 ≤ √(P.μ2 ^ 2 + 4 * P.𝓵 * c) := Real.sqrt_nonneg (P.μ2 ^ 2 + 4 * P.𝓵 * c)
          linarith
        · refine Real.le_sqrt_of_sq_le ?_
          rw [le_add_iff_nonneg_right]
          refine mul_nonneg_of_nonpos_of_nonpos ?_ ?_
          · refine mul_nonpos_of_nonneg_of_nonpos ?_ ?_
            · linarith
            · linarith
          · rcases h with h | h
            · linarith
            · have h1 : P.μ2 = 0 := by linarith
              rw [h1] at h
              simpa using h.2
      · linarith
    use (ofReal a)
    use 0
    rw [ofReal_normSq ha]
    trans P.𝓵 * a * a + (- P.μ2) * a + (- c)
    · ring
    have hd : 0 ≤ (discrim P.𝓵 (- P.μ2) (-c)) := by
      simp only [discrim, even_two, Even.neg_pow, mul_neg, sub_neg_eq_add]
      rcases h with h | h
      · refine Left.add_nonneg (sq_nonneg P.μ2) ?_
        refine mul_nonneg_of_nonpos_of_nonpos ?_ h.2
        linarith
      · rw [← @neg_le_iff_add_nonneg']
        rw [← le_div_iff_of_neg']
        · exact h.2
        · linarith
    have hdd : discrim P.𝓵 (- P.μ2) (-c) = Real.sqrt (discrim P.𝓵 (- P.μ2) (-c))
        * Real.sqrt (discrim P.𝓵 (- P.μ2) (-c)) := by
      exact (Real.mul_self_sqrt hd).symm
    rw [mul_assoc]
    refine (quadratic_eq_zero_iff (ne_of_gt h𝓵).symm hdd _).mpr ?_
    simp only [neg_neg, or_true, a]

Lemma 3.7 (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 code:

lemma pos_𝓵_sol_exists_iff (h𝓵 : 0 < P.𝓵) (c : ℝ) : (∃ φ x, P.toFun φ x = c) ↔ (P.μ2 < 0 ∧ 0 ≤ c) ∨
    (0 ≤ P.μ2 ∧ - P.μ2 ^ 2 / (4 * P.𝓵) ≤ c) := by
  have h1 := P.neg.neg_𝓵_sol_exists_iff (by simpa using h𝓵) (- c)
  simp only [toFun_neg, neg_inj, μ2_neg, Left.neg_pos_iff, Left.neg_nonpos_iff, even_two,
    Even.neg_pow, 𝓵_neg, mul_neg, neg_div_neg_eq] at h1
  rw [neg_le, neg_div'] at h1
  exact h1

3.2. Boundedness of the Higgs potential

Definition 3.8 (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 code:

def IsBounded : Prop :=
  ∃ c, ∀ Φ x, c ≤ P.toFun Φ x

Lemma 3.9 (StandardModel.HiggsField.Potential.isBounded_𝓵_nonneg):

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

Show Lean code:

lemma isBounded_𝓵_nonneg (h : P.IsBounded) : 0 ≤ P.𝓵 := by
  by_contra hl
  rw [not_le] at hl
  obtain ⟨c, hc⟩ := h
  by_cases hμ : P.μ2 ≤ 0
  · by_cases hcz : c ≤ - P.μ2 ^ 2 / (4 * P.𝓵)
    · have hcm1 : ∃ φ x, P.toFun φ x = c - 1 := by
        rw [P.neg_𝓵_sol_exists_iff hl (c - 1)]
        apply Or.inr
        simp_all
        linarith
      obtain ⟨φ, x, hφ⟩ := hcm1
      have hc2 := hc φ x
      rw [hφ] at hc2
      linarith
    · rw [not_le] at hcz
      have hcm1 : ∃ φ x, P.toFun φ x = - P.μ2 ^ 2 / (4 * P.𝓵) - 1 := by
        rw [P.neg_𝓵_sol_exists_iff hl _]
        apply Or.inr
        simp_all
      obtain ⟨φ, x, hφ⟩ := hcm1
      have hc2 := hc φ x
      rw [hφ] at hc2
      linarith
  · rw [not_le] at hμ
    by_cases hcz : c ≤ 0
    · have hcm1 : ∃ φ x, P.toFun φ x = c - 1 := by
        rw [P.neg_𝓵_sol_exists_iff hl (c - 1)]
        apply Or.inl
        simp_all
        linarith
      obtain ⟨φ, x, hφ⟩ := hcm1
      have hc2 := hc φ x
      rw [hφ] at hc2
      linarith
    · have hcm1 : ∃ φ x, P.toFun φ x = 0 := by
        rw [P.neg_𝓵_sol_exists_iff hl 0]
        apply Or.inl
        simp_all
      obtain ⟨φ, x, hφ⟩ := hcm1
      have hc2 := hc φ x
      rw [hφ] at hc2
      linarith

Lemma 3.10 (StandardModel.HiggsField.Potential.isBounded_of_𝓵_pos):

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

Show Lean code:

lemma isBounded_of_𝓵_pos (h : 0 < P.𝓵) : P.IsBounded := by
  simp only [IsBounded]
  have h2 := P.pos_𝓵_quadDiscrim_zero_bound h
  by_contra hn
  simp only [not_exists, not_forall, not_le] at hn
  obtain ⟨φ, x, hx⟩ := hn (-P.μ2 ^ 2 / (4 * P.𝓵))
  have h2' := h2 φ x
  linarith

3.3. Maximum and minimum of the Higgs potential

Lemma 3.11 (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 code:

lemma isMaxOn_iff_field_of_𝓵_neg (h𝓵 : P.𝓵 < 0) (φ : HiggsField) (x : SpaceTime) :
    IsMaxOn (fun (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔
    (P.μ2 ≤ 0 ∧ ‖φ‖_H^2 x = P.μ2 /(2 * P.𝓵)) ∨ (0 < P.μ2 ∧ φ x = 0) := by
  rw [P.isMaxOn_iff_isMinOn_neg,
    P.neg.isMinOn_iff_field_of_𝓵_pos (by simpa using h𝓵)]
  simp

Theorem 3.12 (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 code:

theorem isMinOn_iff_field_of_𝓵_pos (h𝓵 : 0 < P.𝓵) (φ : HiggsField) (x : SpaceTime) :
    IsMinOn (fun (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔
    (0 ≤ P.μ2 ∧ ‖φ‖_H^2 x = P.μ2 /(2 * P.𝓵)) ∨ (P.μ2 < 0 ∧ φ x = 0) := by
  by_cases hμ2 : 0 ≤ P.μ2
  · simpa [not_lt.mpr hμ2, hμ2] using P.isMinOn_iff_field_of_μSq_nonneg_𝓵_pos h𝓵 hμ2 φ x
  · simpa [hμ2, lt_of_not_ge hμ2] using P.isMinOn_iff_field_of_μSq_nonpos_𝓵_pos h𝓵 (by linarith) φ x

PhysLean: Digitalizing Physics in Lean 4

A project to digitalize results from physics into Lean 4.

The Higgs potential

Note Authors: Joseph Tooby-Smith

Table of content

1. Introduction

2. The Higgs field

3. The Higgs potential

3.1. Properties of the Higgs potential

3.2. Boundedness of the Higgs potential

3.3. Maximum and minimum of the Higgs potential