Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Particles.BeyondTheStandardModel.TwoHDM.GramMatrixThe potential of the Two Higgs doublet model
i. Overview
In this module we give the define the parameters of the 2HDM potential, and give stability properties of the potential.
ii. Key results
PotentialParameters : The parameters of the 2HDM potential.
massTerm : The mass term of the 2HDM potential.
quarticTerm : The quartic term of the 2HDM potential.
potential : The full potential of the 2HDM.
PotentialIsStable : The condition that the potential is stable.
iii. Table of contents
A. The parameters of the potential
A.1. The potential parameters corresponding to zero
A.2. Gram parameters
A.3. Specific cases
B. The mass term
C. The quartic term
D. The full potential
E. Stability of the potential
E.1. The stability condition
E.2. Instability of the stabilityCounterExample potential
E.3. The reduced mass term
E.4. The reduced quartic term
E.5. Stability in terms of the gram vectors
E.6. Strong stability implies stability
E.7. Showing step in hep-ph/0605184 is invalid
iv. References
For the parameterization of the potential we follow the convention of
https://arxiv.org/pdf/1605.03237
Stability arguments of the potential follow, in part, those from
https://arxiv.org/abs/hep-ph/0605184 Although we note that we explicitly prove that one of the steps in this paper is not valid.
@[expose] public sectionA. The parameters of the potential
We define a type for the parameters of the Higgs potential in the 2HDM.
We follow the convention of 1605.03237, which is highlighted in the explicit construction
of the potential itself.
We relate these parameters to the ξ and η parameters used in the gram vector formalism
given in arXiv:hep-ph/0605184.
The parameters of the Two Higgs doublet model potential. Following the convention of https://arxiv.org/pdf/1605.03237.
The parameter corresponding to m₁₁² in the 2HDM potential.
The parameter corresponding to m₂₂² in the 2HDM potential.
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.
structure PotentialParameters where m₁₁2 : ℝ m₂₂2 : ℝ m₁₂2 : ℂ 𝓵₁ : ℝ 𝓵₂ : ℝ 𝓵₃ : ℝ 𝓵₄ : ℝ 𝓵₅ : ℂ 𝓵₆ : ℂ 𝓵₇ : ℂA.1. The potential parameters corresponding to zero
We define an instance of Zero for the potential parameters, corresponding to all
parameters being zero, and therefore the potential itself being zero.
instance : Zero PotentialParameters where
zero :=
{ m₁₁2 := 0
m₂₂2 := 0
m₁₂2 := 0
𝓵₁ := 0
𝓵₂ := 0
𝓵₃ := 0
𝓵₄ := 0
𝓵₅ := 0
𝓵₆ := 0
𝓵₇ := 0 }@[simp] lemma zero_m₁₁2 : (0 : PotentialParameters).m₁₁2 = 0 := rfl@[simp] lemma zero_m₂₂2 : (0 : PotentialParameters).m₂₂2 = 0 := rfl@[simp] lemma zero_m₁₂2 : (0 : PotentialParameters).m₁₂2 = 0 := rfl@[simp] lemma zero_𝓵₁ : (0 : PotentialParameters).𝓵₁ = 0 := rfl@[simp] lemma zero_𝓵₂ : (0 : PotentialParameters).𝓵₂ = 0 := rfl@[simp] lemma zero_𝓵₃ : (0 : PotentialParameters).𝓵₃ = 0 := rfl@[simp] lemma zero_𝓵₄ : (0 : PotentialParameters).𝓵₄ = 0 := rfl@[simp] lemma zero_𝓵₅ : (0 : PotentialParameters).𝓵₅ = 0 := rfl@[simp] lemma zero_𝓵₆ : (0 : PotentialParameters).𝓵₆ = 0 := rfl@[simp] lemma zero_𝓵₇ : (0 : PotentialParameters).𝓵₇ = 0 := rflA.2. Gram parameters
A reparameterization of the potential parameters corresponding to ξ and η in
arXiv:hep-ph/0605184.
@[simp]
lemma ξ_zero : (0 : PotentialParameters).ξ = 0 := ⊢ ξ 0 = 0
μ:Fin 1 ⊕ Fin 3⊢ ξ 0 μ = 0 μ
⊢ ξ 0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) = 0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩))⊢ ξ 0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) = 0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩))⊢ ξ 0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) = 0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩))⊢ ξ 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) = 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ⊢ ξ 0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) = 0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩))⊢ ξ 0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) = 0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩))⊢ ξ 0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) = 0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩))⊢ ξ 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) = 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) All goals completed! 🐙lemma η_symm (P : PotentialParameters) (μ ν : Fin 1 ⊕ Fin 3) :
P.η μ ν = P.η ν μ := P:PotentialParametersμ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ P.η μ ν = P.η ν μ
P:PotentialParametersν:Fin 1 ⊕ Fin 3⊢ P.η (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν = P.η ν (Sum.inl ((fun i => i) ⟨0, ⋯⟩))P:PotentialParametersν:Fin 1 ⊕ Fin 3⊢ P.η (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν = P.η ν (Sum.inr ((fun i => i) ⟨0, ⋯⟩))P:PotentialParametersν:Fin 1 ⊕ Fin 3⊢ P.η (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν = P.η ν (Sum.inr ((fun i => i) ⟨1, ⋯⟩))P:PotentialParametersν:Fin 1 ⊕ Fin 3⊢ P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν = P.η ν (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) P:PotentialParametersν:Fin 1 ⊕ Fin 3⊢ P.η (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν = P.η ν (Sum.inl ((fun i => i) ⟨0, ⋯⟩))P:PotentialParametersν:Fin 1 ⊕ Fin 3⊢ P.η (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν = P.η ν (Sum.inr ((fun i => i) ⟨0, ⋯⟩))P:PotentialParametersν:Fin 1 ⊕ Fin 3⊢ P.η (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν = P.η ν (Sum.inr ((fun i => i) ⟨1, ⋯⟩))P:PotentialParametersν:Fin 1 ⊕ Fin 3⊢ P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν = P.η ν (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
P.η (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) P:PotentialParameters⊢ P.η (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
P.η (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
P.η (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
P.η (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
P.η (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))P:PotentialParameters⊢ P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
P.η (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) All goals completed! 🐙@[simp]
lemma η_zero : (0 : PotentialParameters).η = 0 := ⊢ η 0 = 0
μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ η 0 μ ν = 0 μ ν
ν:Fin 1 ⊕ Fin 3⊢ η 0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν = 0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) νν:Fin 1 ⊕ Fin 3⊢ η 0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν = 0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) νν:Fin 1 ⊕ Fin 3⊢ η 0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν = 0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) νν:Fin 1 ⊕ Fin 3⊢ η 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν = 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν ν:Fin 1 ⊕ Fin 3⊢ η 0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν = 0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) νν:Fin 1 ⊕ Fin 3⊢ η 0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν = 0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) νν:Fin 1 ⊕ Fin 3⊢ η 0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν = 0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) νν:Fin 1 ⊕ Fin 3⊢ η 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν = 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν ⊢ η 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ⊢ η 0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))⊢ η 0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))⊢ η 0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))⊢ η 0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
0 (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))⊢ η 0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
0 (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) All goals completed! 🐙A.3. Specific cases
An example of potential parameters that serve as a counterexample to the stability
condition given in arXiv:hep-ph/0605184.
This corresponds to the potential:
2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im + ‖H.Φ1 - H.Φ2‖ ^ 4
which has the property that the quartic term is non-negative and only zero if
the mass term is also zero, but the potential is not stable.
In the proof that stabilityCounterExample_not_potentialIsStable, we give
explicit vectors H.Φ1 and H.Φ2 that show this potential is not stable.
This is the first occurrence of such a counterexample in the literature to the best of the author's knowledge.
def stabilityCounterExample : PotentialParameters := {(0 : PotentialParameters) with
m₁₂2 := Complex.I
𝓵₁ := 2
𝓵₂ := 2
𝓵₃ := 2
𝓵₄ := 2
𝓵₅ := 2
𝓵₆ := -2
𝓵₇ := -2}lemma stabilityCounterExample_ξ :
stabilityCounterExample.ξ = fun
| .inl 0 => 0
| .inr 0 => 0
| .inr 1 => 1
| .inr 2 => 0 := ⊢ stabilityCounterExample.ξ = fun x =>
match x with
| Sum.inl 0 => 0
| Sum.inr 0 => 0
| Sum.inr 1 => 1
| Sum.inr 2 => 0
μ:Fin 1 ⊕ Fin 3⊢ stabilityCounterExample.ξ μ =
match μ with
| Sum.inl 0 => 0
| Sum.inr 0 => 0
| Sum.inr 1 => 1
| Sum.inr 2 => 0
All goals completed! 🐙lemma stabilityCounterExample_η :
stabilityCounterExample.η = fun μ => fun ν =>
match μ, ν with
| .inl 0, .inl 0 => 1
| .inl 0, .inr 0 => -1
| .inl 0, .inr 1 => 0
| .inl 0, .inr 2 => 0
| .inr 0, .inl 0 => -1
| .inr 1, .inl 0 => 0
| .inr 2, .inl 0 => 0
| .inr 0, .inr 0 => 1
| .inr 1, .inr 1 => 0
| .inr 2, .inr 2 => 0
| .inr 0, .inr 1 => 0
| .inr 2, .inr 0 => 0
| .inr 2, .inr 1 => 0
| .inr 1, .inr 0 => 0
| .inr 0, .inr 2 => 0
| .inr 1, .inr 2 => 0 := ⊢ stabilityCounterExample.η = fun μ ν =>
match μ, ν with
| Sum.inl 0, Sum.inl 0 => 1
| Sum.inl 0, Sum.inr 0 => -1
| Sum.inl 0, Sum.inr 1 => 0
| Sum.inl 0, Sum.inr 2 => 0
| Sum.inr 0, Sum.inl 0 => -1
| Sum.inr 1, Sum.inl 0 => 0
| Sum.inr 2, Sum.inl 0 => 0
| Sum.inr 0, Sum.inr 0 => 1
| Sum.inr 1, Sum.inr 1 => 0
| Sum.inr 2, Sum.inr 2 => 0
| Sum.inr 0, Sum.inr 1 => 0
| Sum.inr 2, Sum.inr 0 => 0
| Sum.inr 2, Sum.inr 1 => 0
| Sum.inr 1, Sum.inr 0 => 0
| Sum.inr 0, Sum.inr 2 => 0
| Sum.inr 1, Sum.inr 2 => 0
μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ stabilityCounterExample.η μ ν =
match μ, ν with
| Sum.inl 0, Sum.inl 0 => 1
| Sum.inl 0, Sum.inr 0 => -1
| Sum.inl 0, Sum.inr 1 => 0
| Sum.inl 0, Sum.inr 2 => 0
| Sum.inr 0, Sum.inl 0 => -1
| Sum.inr 1, Sum.inl 0 => 0
| Sum.inr 2, Sum.inl 0 => 0
| Sum.inr 0, Sum.inr 0 => 1
| Sum.inr 1, Sum.inr 1 => 0
| Sum.inr 2, Sum.inr 2 => 0
| Sum.inr 0, Sum.inr 1 => 0
| Sum.inr 2, Sum.inr 0 => 0
| Sum.inr 2, Sum.inr 1 => 0
| Sum.inr 1, Sum.inr 0 => 0
| Sum.inr 0, Sum.inr 2 => 0
| Sum.inr 1, Sum.inr 2 => 0
μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ (match μ, ν with
| Sum.inl 0, Sum.inl 0 => (2 + 2 + 2 * 2) / 8
| Sum.inl 0, Sum.inr 0 => (-2 + -2) / 4
| Sum.inl 0, Sum.inr 1 => 0
| Sum.inl 0, Sum.inr 2 => 0
| Sum.inr 0, Sum.inl 0 => (-2 + -2) / 4
| Sum.inr 1, Sum.inl 0 => 0
| Sum.inr 2, Sum.inl 0 => 0
| Sum.inr 0, Sum.inr 0 => (2 + 2) / 4
| Sum.inr 1, Sum.inr 1 => 0
| Sum.inr 2, Sum.inr 2 => (2 + 2 - 2 * 2) / 8
| Sum.inr 0, Sum.inr 1 => 0
| Sum.inr 2, Sum.inr 0 => 0
| Sum.inr 2, Sum.inr 1 => 0
| Sum.inr 1, Sum.inr 0 => 0
| Sum.inr 0, Sum.inr 2 => 0
| Sum.inr 1, Sum.inr 2 => 0) =
match μ, ν with
| Sum.inl 0, Sum.inl 0 => 1
| Sum.inl 0, Sum.inr 0 => -1
| Sum.inl 0, Sum.inr 1 => 0
| Sum.inl 0, Sum.inr 2 => 0
| Sum.inr 0, Sum.inl 0 => -1
| Sum.inr 1, Sum.inl 0 => 0
| Sum.inr 2, Sum.inl 0 => 0
| Sum.inr 0, Sum.inr 0 => 1
| Sum.inr 1, Sum.inr 1 => 0
| Sum.inr 2, Sum.inr 2 => 0
| Sum.inr 0, Sum.inr 1 => 0
| Sum.inr 2, Sum.inr 0 => 0
| Sum.inr 2, Sum.inr 1 => 0
| Sum.inr 1, Sum.inr 0 => 0
| Sum.inr 0, Sum.inr 2 => 0
| Sum.inr 1, Sum.inr 2 => 0
All goals completed! 🐙B. The mass term
We define the mass term of the potential, write it in terms of the gram vector, and prove that it is gauge invariant.
lemma massTerm_eq_gramVector (P : PotentialParameters) (H : TwoHiggsDoublet) :
massTerm P H = ∑ μ, P.ξ μ * H.gramVector μ := P:PotentialParametersH:TwoHiggsDoublet⊢ massTerm P H = ∑ μ, P.ξ μ * H.gramVector μ
P:PotentialParametersH:TwoHiggsDoublet⊢ P.m₁₁2 * (2⁻¹ * (H.gramVector (Sum.inl 0) + H.gramVector (Sum.inr 2))) +
P.m₂₂2 * (2⁻¹ * (H.gramVector (Sum.inl 0) - H.gramVector (Sum.inr 2))) -
(P.m₁₂2.re * (2⁻¹ * H.gramVector (Sum.inr 0)) - P.m₁₂2.im * (2⁻¹ * H.gramVector (Sum.inr 1)) +
(P.m₁₂2.re * (2⁻¹ * H.gramVector (Sum.inr 0)) - P.m₁₂2.im * (2⁻¹ * H.gramVector (Sum.inr 1)))) =
(P.m₁₁2 + P.m₂₂2) / 2 * H.gramVector (Sum.inl 0) +
(-(P.m₁₂2.re * H.gramVector (Sum.inr 0)) + P.m₁₂2.im * H.gramVector (Sum.inr 1) +
(P.m₁₁2 - P.m₂₂2) / 2 * H.gramVector (Sum.inr 2))
All goals completed! 🐙@[simp]
lemma gaugeGroupI_smul_massTerm (g : StandardModel.GaugeGroupI) (P : PotentialParameters)
(H : TwoHiggsDoublet) :
massTerm P (g • H) = massTerm P H := g:GaugeGroupIP:PotentialParametersH:TwoHiggsDoublet⊢ massTerm P (g • H) = massTerm P H
All goals completed! 🐙@[simp]
lemma massTerm_zero : massTerm 0 = 0 := ⊢ massTerm 0 = 0
H:TwoHiggsDoublet⊢ massTerm 0 H = 0 H
All goals completed! 🐙H:TwoHiggsDoublet⊢ - -(⟪H.Φ1, H.Φ2⟫_ℂ).im + (⟪H.Φ1, H.Φ2⟫_ℂ).im = 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im
ring_nf All goals completed! 🐙C. The quartic term
We define the quartic term of the potential, write it in terms of the gram vector, and prove that it is gauge invariant.
lemma quarticTerm_𝓵₄_expand (P : PotentialParameters) (H : TwoHiggsDoublet) :
H.quarticTerm P =
1/2 * P.𝓵₁ * ‖H.Φ1‖ ^ 2 * ‖H.Φ1‖ ^ 2 + 1/2 * P.𝓵₂ * ‖H.Φ2‖ ^ 2 * ‖H.Φ2‖ ^ 2
+ P.𝓵₃ * ‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2
+ P.𝓵₄ * (⟪H.Φ1, H.Φ2⟫_ℂ * ⟪H.Φ2, H.Φ1⟫_ℂ).re
+ (1/2 * P.𝓵₅ * ⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + 1/2 * conj P.𝓵₅ * ⟪H.Φ2, H.Φ1⟫_ℂ ^ 2).re
+ (P.𝓵₆ * ‖H.Φ1‖ ^ 2 * ⟪H.Φ1, H.Φ2⟫_ℂ + conj P.𝓵₆ * ‖H.Φ1‖ ^ 2 * ⟪H.Φ2, H.Φ1⟫_ℂ).re
+ (P.𝓵₇ * ‖H.Φ2‖ ^ 2 * ⟪H.Φ1, H.Φ2⟫_ℂ + conj P.𝓵₇ * ‖H.Φ2‖ ^ 2 * ⟪H.Φ2, H.Φ1⟫_ℂ).re := by P:PotentialParametersH:TwoHiggsDoublet⊢ quarticTerm P H =
1 / 2 * P.𝓵₁ * ‖H.Φ1‖ ^ 2 * ‖H.Φ1‖ ^ 2 + 1 / 2 * P.𝓵₂ * ‖H.Φ2‖ ^ 2 * ‖H.Φ2‖ ^ 2 + P.𝓵₃ * ‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 +
P.𝓵₄ * (⟪H.Φ1, H.Φ2⟫_ℂ * ⟪H.Φ2, H.Φ1⟫_ℂ).re +
(1 / 2 * P.𝓵₅ * ⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + 1 / 2 * (starRingEnd ℂ) P.𝓵₅ * ⟪H.Φ2, H.Φ1⟫_ℂ ^ 2).re +
(P.𝓵₆ * ↑‖H.Φ1‖ ^ 2 * ⟪H.Φ1, H.Φ2⟫_ℂ + (starRingEnd ℂ) P.𝓵₆ * ↑‖H.Φ1‖ ^ 2 * ⟪H.Φ2, H.Φ1⟫_ℂ).re +
(P.𝓵₇ * ↑‖H.Φ2‖ ^ 2 * ⟪H.Φ1, H.Φ2⟫_ℂ + (starRingEnd ℂ) P.𝓵₇ * ↑‖H.Φ2‖ ^ 2 * ⟪H.Φ2, H.Φ1⟫_ℂ).re
simp [quarticTerm] P:PotentialParametersH:TwoHiggsDoublet⊢ ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2 = (⟪H.Φ1, H.Φ2⟫_ℂ).re * (⟪H.Φ2, H.Φ1⟫_ℂ).re - (⟪H.Φ1, H.Φ2⟫_ℂ).im * (⟪H.Φ2, H.Φ1⟫_ℂ).im ∨ P.𝓵₄ = 0
left P:PotentialParametersH:TwoHiggsDoublet⊢ ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2 = (⟪H.Φ1, H.Φ2⟫_ℂ).re * (⟪H.Φ2, H.Φ1⟫_ℂ).re - (⟪H.Φ1, H.Φ2⟫_ℂ).im * (⟪H.Φ2, H.Φ1⟫_ℂ).im
rw [Complex.sq_norm, P:PotentialParametersH:TwoHiggsDoublet⊢ Complex.normSq ⟪H.Φ1, H.Φ2⟫_ℂ = (⟪H.Φ1, H.Φ2⟫_ℂ).re * (⟪H.Φ2, H.Φ1⟫_ℂ).re - (⟪H.Φ1, H.Φ2⟫_ℂ).im * (⟪H.Φ2, H.Φ1⟫_ℂ).im All goals completed! 🐙 ← inner_conj_symm H.Φ2 H.Φ1, P:PotentialParametersH:TwoHiggsDoublet⊢ Complex.normSq ⟪H.Φ1, H.Φ2⟫_ℂ =
(⟪H.Φ1, H.Φ2⟫_ℂ).re * ((starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ).re - (⟪H.Φ1, H.Φ2⟫_ℂ).im * ((starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ).im All goals completed! 🐙 ← Complex.mul_re, P:PotentialParametersH:TwoHiggsDoublet⊢ Complex.normSq ⟪H.Φ1, H.Φ2⟫_ℂ = (⟪H.Φ1, H.Φ2⟫_ℂ * (starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ).re All goals completed! 🐙 Complex.mul_conj, P:PotentialParametersH:TwoHiggsDoublet⊢ Complex.normSq ⟪H.Φ1, H.Φ2⟫_ℂ = (↑(Complex.normSq ⟪H.Φ1, H.Φ2⟫_ℂ)).re All goals completed! 🐙
Complex.ofReal_re P:PotentialParametersH:TwoHiggsDoublet⊢ Complex.normSq ⟪H.Φ1, H.Φ2⟫_ℂ = Complex.normSq ⟪H.Φ1, H.Φ2⟫_ℂ All goals completed! 🐙] All goals completed! 🐙lemma quarticTerm_eq_gramVector (P : PotentialParameters) (H : TwoHiggsDoublet) :
quarticTerm P H = ∑ a, ∑ b, H.gramVector a * H.gramVector b * P.η a b := by P:PotentialParametersH:TwoHiggsDoublet⊢ quarticTerm P H = ∑ a, ∑ b, H.gramVector a * H.gramVector b * P.η a b
simp [quarticTerm_𝓵₄_expand, Fin.sum_univ_three, PotentialParameters.η, normSq_Φ1_eq_gramVector,
normSq_Φ2_eq_gramVector, Φ1_inner_Φ2_eq_gramVector, Φ2_inner_Φ1_eq_gramVector] P:PotentialParametersH:TwoHiggsDoublet⊢ 2⁻¹ * P.𝓵₁ * (2⁻¹ * (H.gramVector (Sum.inl 0) + H.gramVector (Sum.inr 2))) *
(2⁻¹ * (H.gramVector (Sum.inl 0) + H.gramVector (Sum.inr 2))) +
2⁻¹ * P.𝓵₂ * (2⁻¹ * (H.gramVector (Sum.inl 0) - H.gramVector (Sum.inr 2))) *
(2⁻¹ * (H.gramVector (Sum.inl 0) - H.gramVector (Sum.inr 2))) +
P.𝓵₃ * (2⁻¹ * (H.gramVector (Sum.inl 0) + H.gramVector (Sum.inr 2))) *
(2⁻¹ * (H.gramVector (Sum.inl 0) - H.gramVector (Sum.inr 2))) +
P.𝓵₄ *
(2⁻¹ * H.gramVector (Sum.inr 0) * (2⁻¹ * H.gramVector (Sum.inr 0)) +
2⁻¹ * H.gramVector (Sum.inr 1) * (2⁻¹ * H.gramVector (Sum.inr 1))) +
(2⁻¹ * P.𝓵₅.re * ((2⁻¹ * (↑(H.gramVector (Sum.inr 0)) + Complex.I * ↑(H.gramVector (Sum.inr 1)))) ^ 2).re -
2⁻¹ * P.𝓵₅.im * ((2⁻¹ * (↑(H.gramVector (Sum.inr 0)) + Complex.I * ↑(H.gramVector (Sum.inr 1)))) ^ 2).im +
(2⁻¹ * P.𝓵₅.re * ((2⁻¹ * (↑(H.gramVector (Sum.inr 0)) - Complex.I * ↑(H.gramVector (Sum.inr 1)))) ^ 2).re +
2⁻¹ * P.𝓵₅.im * ((2⁻¹ * (↑(H.gramVector (Sum.inr 0)) - Complex.I * ↑(H.gramVector (Sum.inr 1)))) ^ 2).im)) +
((P.𝓵₆.re * (↑‖H.Φ1‖ ^ 2).re - P.𝓵₆.im * (↑‖H.Φ1‖ ^ 2).im) * (2⁻¹ * H.gramVector (Sum.inr 0)) -
(P.𝓵₆.re * (↑‖H.Φ1‖ ^ 2).im + P.𝓵₆.im * (↑‖H.Φ1‖ ^ 2).re) * (2⁻¹ * H.gramVector (Sum.inr 1)) +
((P.𝓵₆.re * (↑‖H.Φ1‖ ^ 2).re + P.𝓵₆.im * (↑‖H.Φ1‖ ^ 2).im) * (2⁻¹ * H.gramVector (Sum.inr 0)) +
(P.𝓵₆.re * (↑‖H.Φ1‖ ^ 2).im + -(P.𝓵₆.im * (↑‖H.Φ1‖ ^ 2).re)) * (2⁻¹ * H.gramVector (Sum.inr 1)))) +
((P.𝓵₇.re * (↑‖H.Φ2‖ ^ 2).re - P.𝓵₇.im * (↑‖H.Φ2‖ ^ 2).im) * (2⁻¹ * H.gramVector (Sum.inr 0)) -
(P.𝓵₇.re * (↑‖H.Φ2‖ ^ 2).im + P.𝓵₇.im * (↑‖H.Φ2‖ ^ 2).re) * (2⁻¹ * H.gramVector (Sum.inr 1)) +
((P.𝓵₇.re * (↑‖H.Φ2‖ ^ 2).re + P.𝓵₇.im * (↑‖H.Φ2‖ ^ 2).im) * (2⁻¹ * H.gramVector (Sum.inr 0)) +
(P.𝓵₇.re * (↑‖H.Φ2‖ ^ 2).im + -(P.𝓵₇.im * (↑‖H.Φ2‖ ^ 2).re)) * (2⁻¹ * H.gramVector (Sum.inr 1)))) =
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inl 0) * ((P.𝓵₁ + P.𝓵₂ + 2 * P.𝓵₃) / 8) +
(H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 0) * ((P.𝓵₆.re + P.𝓵₇.re) / 4) +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 1) * ((-P.𝓵₇.im + -P.𝓵₆.im) / 4) +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 2) * ((P.𝓵₁ - P.𝓵₂) / 8)) +
(H.gramVector (Sum.inr 0) * H.gramVector (Sum.inl 0) * ((P.𝓵₆.re + P.𝓵₇.re) / 4) +
(H.gramVector (Sum.inr 0) * H.gramVector (Sum.inr 0) * ((P.𝓵₅.re + P.𝓵₄) / 4) +
H.gramVector (Sum.inr 0) * H.gramVector (Sum.inr 1) * (-P.𝓵₅.im / 4) +
H.gramVector (Sum.inr 0) * H.gramVector (Sum.inr 2) * ((P.𝓵₆.re - P.𝓵₇.re) / 4)) +
(H.gramVector (Sum.inr 1) * H.gramVector (Sum.inl 0) * ((-P.𝓵₇.im + -P.𝓵₆.im) / 4) +
(H.gramVector (Sum.inr 1) * H.gramVector (Sum.inr 0) * (-P.𝓵₅.im / 4) +
H.gramVector (Sum.inr 1) * H.gramVector (Sum.inr 1) * ((P.𝓵₄ - P.𝓵₅.re) / 4) +
H.gramVector (Sum.inr 1) * H.gramVector (Sum.inr 2) * ((P.𝓵₇.im - P.𝓵₆.im) / 4))) +
(H.gramVector (Sum.inr 2) * H.gramVector (Sum.inl 0) * ((P.𝓵₁ - P.𝓵₂) / 8) +
(H.gramVector (Sum.inr 2) * H.gramVector (Sum.inr 0) * ((P.𝓵₆.re - P.𝓵₇.re) / 4) +
H.gramVector (Sum.inr 2) * H.gramVector (Sum.inr 1) * ((P.𝓵₇.im - P.𝓵₆.im) / 4) +
H.gramVector (Sum.inr 2) * H.gramVector (Sum.inr 2) * ((P.𝓵₁ + P.𝓵₂ - 2 * P.𝓵₃) / 8))))
ring_nf P:PotentialParametersH:TwoHiggsDoublet⊢ P.𝓵₁ * H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 2) * (1 / 4) + P.𝓵₁ * H.gramVector (Sum.inl 0) ^ 2 * (1 / 8) +
P.𝓵₁ * H.gramVector (Sum.inr 2) ^ 2 * (1 / 8) +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 2) * P.𝓵₂ * (-1 / 4) +
H.gramVector (Sum.inl 0) ^ 2 * P.𝓵₂ * (1 / 8) +
H.gramVector (Sum.inl 0) ^ 2 * P.𝓵₃ * (1 / 4) +
H.gramVector (Sum.inr 2) ^ 2 * P.𝓵₂ * (1 / 8) +
H.gramVector (Sum.inr 2) ^ 2 * P.𝓵₃ * (-1 / 4) +
P.𝓵₄ * H.gramVector (Sum.inr 0) ^ 2 * (1 / 4) +
P.𝓵₄ * H.gramVector (Sum.inr 1) ^ 2 * (1 / 4) +
H.gramVector (Sum.inr 0) * P.𝓵₆.re * (↑‖H.Φ1‖ ^ 2).re +
H.gramVector (Sum.inr 0) * P.𝓵₇.re * (↑‖H.Φ2‖ ^ 2).re -
H.gramVector (Sum.inr 1) * (↑‖H.Φ1‖ ^ 2).re * P.𝓵₆.im -
H.gramVector (Sum.inr 1) * (↑‖H.Φ2‖ ^ 2).re * P.𝓵₇.im +
P.𝓵₅.re *
(↑(H.gramVector (Sum.inr 0)) * Complex.I * ↑(H.gramVector (Sum.inr 1)) * (1 / 2) +
↑(H.gramVector (Sum.inr 0)) ^ 2 * (1 / 4) +
Complex.I ^ 2 * ↑(H.gramVector (Sum.inr 1)) ^ 2 * (1 / 4)).re *
(1 / 2) +
P.𝓵₅.re *
(↑(H.gramVector (Sum.inr 0)) * Complex.I * ↑(H.gramVector (Sum.inr 1)) * (-1 / 2) +
↑(H.gramVector (Sum.inr 0)) ^ 2 * (1 / 4) +
Complex.I ^ 2 * ↑(H.gramVector (Sum.inr 1)) ^ 2 * (1 / 4)).re *
(1 / 2) +
P.𝓵₅.im *
(↑(H.gramVector (Sum.inr 0)) * Complex.I * ↑(H.gramVector (Sum.inr 1)) * (1 / 2) +
↑(H.gramVector (Sum.inr 0)) ^ 2 * (1 / 4) +
Complex.I ^ 2 * ↑(H.gramVector (Sum.inr 1)) ^ 2 * (1 / 4)).im *
(-1 / 2) +
P.𝓵₅.im *
(↑(H.gramVector (Sum.inr 0)) * Complex.I * ↑(H.gramVector (Sum.inr 1)) * (-1 / 2) +
↑(H.gramVector (Sum.inr 0)) ^ 2 * (1 / 4) +
Complex.I ^ 2 * ↑(H.gramVector (Sum.inr 1)) ^ 2 * (1 / 4)).im *
(1 / 2) =
P.𝓵₁ * H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 2) * (1 / 4) + P.𝓵₁ * H.gramVector (Sum.inl 0) ^ 2 * (1 / 8) +
P.𝓵₁ * H.gramVector (Sum.inr 2) ^ 2 * (1 / 8) +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 2) * P.𝓵₂ * (-1 / 4) +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 0) * P.𝓵₆.re * (1 / 2) +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 0) * P.𝓵₇.re * (1 / 2) +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 1) * P.𝓵₆.im * (-1 / 2) +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 1) * P.𝓵₇.im * (-1 / 2) +
H.gramVector (Sum.inl 0) ^ 2 * P.𝓵₂ * (1 / 8) +
H.gramVector (Sum.inl 0) ^ 2 * P.𝓵₃ * (1 / 4) +
H.gramVector (Sum.inr 2) * H.gramVector (Sum.inr 0) * P.𝓵₆.re * (1 / 2) +
H.gramVector (Sum.inr 2) * H.gramVector (Sum.inr 0) * P.𝓵₇.re * (-1 / 2) +
H.gramVector (Sum.inr 2) * H.gramVector (Sum.inr 1) * P.𝓵₆.im * (-1 / 2) +
H.gramVector (Sum.inr 2) * H.gramVector (Sum.inr 1) * P.𝓵₇.im * (1 / 2) +
H.gramVector (Sum.inr 2) ^ 2 * P.𝓵₂ * (1 / 8) +
H.gramVector (Sum.inr 2) ^ 2 * P.𝓵₃ * (-1 / 4) +
P.𝓵₄ * H.gramVector (Sum.inr 0) ^ 2 * (1 / 4) +
P.𝓵₄ * H.gramVector (Sum.inr 1) ^ 2 * (1 / 4) +
H.gramVector (Sum.inr 0) * H.gramVector (Sum.inr 1) * P.𝓵₅.im * (-1 / 2) +
H.gramVector (Sum.inr 0) ^ 2 * P.𝓵₅.re * (1 / 4) +
H.gramVector (Sum.inr 1) ^ 2 * P.𝓵₅.re * (-1 / 4)
simp [← Complex.ofReal_pow, Complex.ofReal_re, normSq_Φ1_eq_gramVector,
normSq_Φ2_eq_gramVector] P:PotentialParametersH:TwoHiggsDoublet⊢ P.𝓵₁ * H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 2) * 4⁻¹ + P.𝓵₁ * H.gramVector (Sum.inl 0) ^ 2 * 8⁻¹ +
P.𝓵₁ * H.gramVector (Sum.inr 2) ^ 2 * 8⁻¹ +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 2) * P.𝓵₂ * (-1 / 4) +
H.gramVector (Sum.inl 0) ^ 2 * P.𝓵₂ * 8⁻¹ +
H.gramVector (Sum.inl 0) ^ 2 * P.𝓵₃ * 4⁻¹ +
H.gramVector (Sum.inr 2) ^ 2 * P.𝓵₂ * 8⁻¹ +
H.gramVector (Sum.inr 2) ^ 2 * P.𝓵₃ * (-1 / 4) +
P.𝓵₄ * H.gramVector (Sum.inr 0) ^ 2 * 4⁻¹ +
P.𝓵₄ * H.gramVector (Sum.inr 1) ^ 2 * 4⁻¹ +
H.gramVector (Sum.inr 0) * P.𝓵₆.re * (2⁻¹ * (H.gramVector (Sum.inl 0) + H.gramVector (Sum.inr 2))) +
H.gramVector (Sum.inr 0) * P.𝓵₇.re * (2⁻¹ * (H.gramVector (Sum.inl 0) - H.gramVector (Sum.inr 2))) -
H.gramVector (Sum.inr 1) * (2⁻¹ * (H.gramVector (Sum.inl 0) + H.gramVector (Sum.inr 2))) * P.𝓵₆.im -
H.gramVector (Sum.inr 1) * (2⁻¹ * (H.gramVector (Sum.inl 0) - H.gramVector (Sum.inr 2))) * P.𝓵₇.im +
P.𝓵₅.re * (H.gramVector (Sum.inr 0) ^ 2 * 4⁻¹ + -(H.gramVector (Sum.inr 1) ^ 2 * 4⁻¹)) * 2⁻¹ +
P.𝓵₅.re * (H.gramVector (Sum.inr 0) ^ 2 * 4⁻¹ + -(H.gramVector (Sum.inr 1) ^ 2 * 4⁻¹)) * 2⁻¹ +
P.𝓵₅.im * (H.gramVector (Sum.inr 0) * H.gramVector (Sum.inr 1) * 2⁻¹) * (-1 / 2) +
P.𝓵₅.im * (H.gramVector (Sum.inr 0) * H.gramVector (Sum.inr 1) * (-1 / 2)) * 2⁻¹ =
P.𝓵₁ * H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 2) * 4⁻¹ + P.𝓵₁ * H.gramVector (Sum.inl 0) ^ 2 * 8⁻¹ +
P.𝓵₁ * H.gramVector (Sum.inr 2) ^ 2 * 8⁻¹ +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 2) * P.𝓵₂ * (-1 / 4) +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 0) * P.𝓵₆.re * 2⁻¹ +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 0) * P.𝓵₇.re * 2⁻¹ +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 1) * P.𝓵₆.im * (-1 / 2) +
H.gramVector (Sum.inl 0) * H.gramVector (Sum.inr 1) * P.𝓵₇.im * (-1 / 2) +
H.gramVector (Sum.inl 0) ^ 2 * P.𝓵₂ * 8⁻¹ +
H.gramVector (Sum.inl 0) ^ 2 * P.𝓵₃ * 4⁻¹ +
H.gramVector (Sum.inr 2) * H.gramVector (Sum.inr 0) * P.𝓵₆.re * 2⁻¹ +
H.gramVector (Sum.inr 2) * H.gramVector (Sum.inr 0) * P.𝓵₇.re * (-1 / 2) +
H.gramVector (Sum.inr 2) * H.gramVector (Sum.inr 1) * P.𝓵₆.im * (-1 / 2) +
H.gramVector (Sum.inr 2) * H.gramVector (Sum.inr 1) * P.𝓵₇.im * 2⁻¹ +
H.gramVector (Sum.inr 2) ^ 2 * P.𝓵₂ * 8⁻¹ +
H.gramVector (Sum.inr 2) ^ 2 * P.𝓵₃ * (-1 / 4) +
P.𝓵₄ * H.gramVector (Sum.inr 0) ^ 2 * 4⁻¹ +
P.𝓵₄ * H.gramVector (Sum.inr 1) ^ 2 * 4⁻¹ +
H.gramVector (Sum.inr 0) * H.gramVector (Sum.inr 1) * P.𝓵₅.im * (-1 / 2) +
H.gramVector (Sum.inr 0) ^ 2 * P.𝓵₅.re * 4⁻¹ +
H.gramVector (Sum.inr 1) ^ 2 * P.𝓵₅.re * (-1 / 4)
ring All goals completed! 🐙@[simp]
lemma gaugeGroupI_smul_quarticTerm (g : StandardModel.GaugeGroupI) (P : PotentialParameters)
(H : TwoHiggsDoublet) :
quarticTerm P (g • H) = quarticTerm P H := by g:GaugeGroupIP:PotentialParametersH:TwoHiggsDoublet⊢ quarticTerm P (g • H) = quarticTerm P H
simp [quarticTerm_eq_gramVector] All goals completed! 🐙@[simp]
lemma quarticTerm_zero : quarticTerm 0 = 0 := by ⊢ quarticTerm 0 = 0
ext H H:TwoHiggsDoublet⊢ quarticTerm 0 H = 0 H
simp [quarticTerm] All goals completed! 🐙
lemma quarticTerm_stabilityCounterExample (H : TwoHiggsDoublet) :
quarticTerm .stabilityCounterExample H =
(‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2:= by H:TwoHiggsDoublet⊢ quarticTerm PotentialParameters.stabilityCounterExample H = (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2
calc _ = (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2
+ 2 * ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2
+ (⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + ⟪H.Φ2, H.Φ1⟫_ℂ ^ 2).re
- 2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ2, H.Φ1⟫_ℂ).re) := by H:TwoHiggsDoublet⊢ quarticTerm PotentialParameters.stabilityCounterExample H =
(‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2 + 2 * ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2 + (⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + ⟪H.Φ2, H.Φ1⟫_ℂ ^ 2).re -
2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ2, H.Φ1⟫_ℂ).re)
simp [quarticTerm, PotentialParameters.stabilityCounterExample, Complex.add_re,
← Complex.ofReal_pow] H:TwoHiggsDoublet⊢ ‖H.Φ1‖ ^ 2 * ‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 * ‖H.Φ2‖ ^ 2 + 2 * ‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 + 2 * ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2 +
((⟪H.Φ1, H.Φ2⟫_ℂ ^ 2).re + (⟪H.Φ2, H.Φ1⟫_ℂ ^ 2).re) +
(-(2 * ‖H.Φ1‖ ^ 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) + -(2 * ‖H.Φ1‖ ^ 2 * (⟪H.Φ2, H.Φ1⟫_ℂ).re)) +
(-(2 * ‖H.Φ2‖ ^ 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) + -(2 * ‖H.Φ2‖ ^ 2 * (⟪H.Φ2, H.Φ1⟫_ℂ).re)) =
(‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2 + 2 * ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2 + ((⟪H.Φ1, H.Φ2⟫_ℂ ^ 2).re + (⟪H.Φ2, H.Φ1⟫_ℂ ^ 2).re) -
2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ2, H.Φ1⟫_ℂ).re)
ring All goals completed! 🐙
_ = (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 := by H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2 + 2 * ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2 + (⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + ⟪H.Φ2, H.Φ1⟫_ℂ ^ 2).re -
2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ2, H.Φ1⟫_ℂ).re) =
(‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2
rw [← inner_conj_symm H.Φ2 H.Φ1, H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2 + 2 * ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2 +
(⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + (starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ ^ 2).re -
2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + ((starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ).re) =
(‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2 +
2 * ((⟪H.Φ1, H.Φ2⟫_ℂ).re * (⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ1, H.Φ2⟫_ℂ).im * (⟪H.Φ1, H.Φ2⟫_ℂ).im) +
(⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + (starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ ^ 2).re -
2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + ((starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ).re) =
(‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 ← Complex.normSq_eq_norm_sq, H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2 + 2 * Complex.normSq ⟪H.Φ1, H.Φ2⟫_ℂ +
(⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + (starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ ^ 2).re -
2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + ((starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ).re) =
(‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2 +
2 * ((⟪H.Φ1, H.Φ2⟫_ℂ).re * (⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ1, H.Φ2⟫_ℂ).im * (⟪H.Φ1, H.Φ2⟫_ℂ).im) +
(⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + (starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ ^ 2).re -
2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + ((starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ).re) =
(‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 Complex.normSq_apply H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2 +
2 * ((⟪H.Φ1, H.Φ2⟫_ℂ).re * (⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ1, H.Φ2⟫_ℂ).im * (⟪H.Φ1, H.Φ2⟫_ℂ).im) +
(⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + (starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ ^ 2).re -
2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + ((starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ).re) =
(‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2 +
2 * ((⟪H.Φ1, H.Φ2⟫_ℂ).re * (⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ1, H.Φ2⟫_ℂ).im * (⟪H.Φ1, H.Φ2⟫_ℂ).im) +
(⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + (starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ ^ 2).re -
2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + ((starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ).re) =
(‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2] H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2 +
2 * ((⟪H.Φ1, H.Φ2⟫_ℂ).re * (⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ1, H.Φ2⟫_ℂ).im * (⟪H.Φ1, H.Φ2⟫_ℂ).im) +
(⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + (starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ ^ 2).re -
2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + ((starRingEnd ℂ) ⟪H.Φ1, H.Φ2⟫_ℂ).re) =
(‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2
simp only [Complex.add_re, Complex.mul_re, Complex.conj_re, Complex.conj_im, pow_two] H:TwoHiggsDoublet⊢ (‖H.Φ1‖ * ‖H.Φ1‖ + ‖H.Φ2‖ * ‖H.Φ2‖) * (‖H.Φ1‖ * ‖H.Φ1‖ + ‖H.Φ2‖ * ‖H.Φ2‖) +
2 * ((⟪H.Φ1, H.Φ2⟫_ℂ).re * (⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ1, H.Φ2⟫_ℂ).im * (⟪H.Φ1, H.Φ2⟫_ℂ).im) +
((⟪H.Φ1, H.Φ2⟫_ℂ).re * (⟪H.Φ1, H.Φ2⟫_ℂ).re - (⟪H.Φ1, H.Φ2⟫_ℂ).im * (⟪H.Φ1, H.Φ2⟫_ℂ).im +
((⟪H.Φ1, H.Φ2⟫_ℂ).re * (⟪H.Φ1, H.Φ2⟫_ℂ).re - -(⟪H.Φ1, H.Φ2⟫_ℂ).im * -(⟪H.Φ1, H.Φ2⟫_ℂ).im)) -
2 * (‖H.Φ1‖ * ‖H.Φ1‖ + ‖H.Φ2‖ * ‖H.Φ2‖) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ1, H.Φ2⟫_ℂ).re) =
(‖H.Φ1‖ * ‖H.Φ1‖ + ‖H.Φ2‖ * ‖H.Φ2‖ - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) *
(‖H.Φ1‖ * ‖H.Φ1‖ + ‖H.Φ2‖ * ‖H.Φ2‖ - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re)
ring All goals completed! 🐙
lemma quarticTerm_stabilityCounterExample_eq_norm_pow_four (H : TwoHiggsDoublet) :
quarticTerm .stabilityCounterExample H = ‖H.Φ1 - H.Φ2‖ ^ 4 := by H:TwoHiggsDoublet⊢ quarticTerm PotentialParameters.stabilityCounterExample H = ‖H.Φ1 - H.Φ2‖ ^ 4
rw [quarticTerm_stabilityCounterExample H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 = ‖H.Φ1 - H.Φ2‖ ^ 4 H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 = ‖H.Φ1 - H.Φ2‖ ^ 4] H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 = ‖H.Φ1 - H.Φ2‖ ^ 4
rw [show ‖H.Φ1 - H.Φ2‖ ^ 4 = (‖H.Φ1 - H.Φ2‖ ^ 2) ^ 2 from by H:TwoHiggsDoublet⊢ ‖H.Φ1 - H.Φ2‖ ^ 4 = (‖H.Φ1 - H.Φ2‖ ^ 2) ^ 2 H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 = (‖H.Φ1‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re + ‖H.Φ2‖ ^ 2) ^ 2 ring All goals completed! 🐙 H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 = (‖H.Φ1‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re + ‖H.Φ2‖ ^ 2) ^ 2, norm_sub_sq (𝕜 := ℂ), H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 = (‖H.Φ1‖ ^ 2 - 2 * RCLike.re ⟪H.Φ1, H.Φ2⟫_ℂ + ‖H.Φ2‖ ^ 2) ^ 2 H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 = (‖H.Φ1‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re + ‖H.Φ2‖ ^ 2) ^ 2
RCLike.re_to_complex H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 = (‖H.Φ1‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re + ‖H.Φ2‖ ^ 2) ^ 2 H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 = (‖H.Φ1‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re + ‖H.Φ2‖ ^ 2) ^ 2] H:TwoHiggsDoublet⊢ (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 = (‖H.Φ1‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re + ‖H.Φ2‖ ^ 2) ^ 2
ring All goals completed! 🐙
lemma quarticTerm_stabilityCounterExample_nonneg (H : TwoHiggsDoublet) :
0 ≤ quarticTerm .stabilityCounterExample H := by H:TwoHiggsDoublet⊢ 0 ≤ quarticTerm PotentialParameters.stabilityCounterExample H
rw [quarticTerm_stabilityCounterExample_eq_norm_pow_four H:TwoHiggsDoublet⊢ 0 ≤ ‖H.Φ1 - H.Φ2‖ ^ 4 H:TwoHiggsDoublet⊢ 0 ≤ ‖H.Φ1 - H.Φ2‖ ^ 4] H:TwoHiggsDoublet⊢ 0 ≤ ‖H.Φ1 - H.Φ2‖ ^ 4
positivity All goals completed! 🐙
lemma massTerm_zero_of_quarticTerm_zero_stabilityCounterExample (H : TwoHiggsDoublet)
(h : quarticTerm .stabilityCounterExample H = 0) :
massTerm .stabilityCounterExample H = 0 := by H:TwoHiggsDoubleth:quarticTerm PotentialParameters.stabilityCounterExample H = 0⊢ massTerm PotentialParameters.stabilityCounterExample H = 0
rw [quarticTerm_stabilityCounterExample_eq_norm_pow_four H:TwoHiggsDoubleth:‖H.Φ1 - H.Φ2‖ ^ 4 = 0⊢ massTerm PotentialParameters.stabilityCounterExample H = 0 H:TwoHiggsDoubleth:‖H.Φ1 - H.Φ2‖ ^ 4 = 0⊢ massTerm PotentialParameters.stabilityCounterExample H = 0] at h H:TwoHiggsDoubleth:‖H.Φ1 - H.Φ2‖ ^ 4 = 0⊢ massTerm PotentialParameters.stabilityCounterExample H = 0
rw [massTerm_stabilityCounterExample H:TwoHiggsDoubleth:‖H.Φ1 - H.Φ2‖ ^ 4 = 0⊢ 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im = 0 H:TwoHiggsDoubleth:‖H.Φ1 - H.Φ2‖ ^ 4 = 0⊢ 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im = 0] H:TwoHiggsDoubleth:‖H.Φ1 - H.Φ2‖ ^ 4 = 0⊢ 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im = 0
have h1 : H.Φ1 = H.Φ2 := by H:TwoHiggsDoubleth:quarticTerm PotentialParameters.stabilityCounterExample H = 0⊢ massTerm PotentialParameters.stabilityCounterExample H = 0 H:TwoHiggsDoubleth:‖H.Φ1 - H.Φ2‖ ^ 4 = 0h1:H.Φ1 = H.Φ2⊢ 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im = 0 simpa [sub_eq_zero] using h H:TwoHiggsDoubleth:‖H.Φ1 - H.Φ2‖ ^ 4 = 0h1:H.Φ1 = H.Φ2⊢ 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im = 0 H:TwoHiggsDoubleth:‖H.Φ1 - H.Φ2‖ ^ 4 = 0h1:H.Φ1 = H.Φ2⊢ 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im = 0
simp [← Complex.ofReal_pow, h1] All goals completed! 🐙D. The full potential
We define the full potential as the sum of the mass and quartic terms, and prove that it is gauge invariant.
@[simp]
lemma gaugeGroupI_smul_potential (g : StandardModel.GaugeGroupI)
(P : PotentialParameters) (H : TwoHiggsDoublet) :
potential P (g • H) = potential P H := by g:GaugeGroupIP:PotentialParametersH:TwoHiggsDoublet⊢ potential P (g • H) = potential P H
simp [potential] All goals completed! 🐙@[simp]
lemma potential_zero : potential 0 = 0 := by ⊢ potential 0 = 0
ext H H:TwoHiggsDoublet⊢ potential 0 H = 0 H
simp [potential] All goals completed! 🐙lemma potential_stabilityCounterExample (H : TwoHiggsDoublet) :
potential .stabilityCounterExample H = 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im + ‖H.Φ1 - H.Φ2‖ ^ 4 := by H:TwoHiggsDoublet⊢ potential PotentialParameters.stabilityCounterExample H = 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im + ‖H.Φ1 - H.Φ2‖ ^ 4
simp [potential, massTerm_stabilityCounterExample,
quarticTerm_stabilityCounterExample_eq_norm_pow_four] All goals completed! 🐙
lemma potential_eq_gramVector (P : PotentialParameters) (H : TwoHiggsDoublet) :
potential P H = ∑ μ, P.ξ μ * H.gramVector μ +
∑ a, ∑ b, H.gramVector a * H.gramVector b * P.η a b := by P:PotentialParametersH:TwoHiggsDoublet⊢ potential P H = ∑ μ, P.ξ μ * H.gramVector μ + ∑ a, ∑ b, H.gramVector a * H.gramVector b * P.η a b
rw [potential, P:PotentialParametersH:TwoHiggsDoublet⊢ massTerm P H + quarticTerm P H = ∑ μ, P.ξ μ * H.gramVector μ + ∑ a, ∑ b, H.gramVector a * H.gramVector b * P.η a b All goals completed! 🐙 massTerm_eq_gramVector, P:PotentialParametersH:TwoHiggsDoublet⊢ ∑ μ, P.ξ μ * H.gramVector μ + quarticTerm P H =
∑ μ, P.ξ μ * H.gramVector μ + ∑ a, ∑ b, H.gramVector a * H.gramVector b * P.η a b All goals completed! 🐙 quarticTerm_eq_gramVector P:PotentialParametersH:TwoHiggsDoublet⊢ ∑ μ, P.ξ μ * H.gramVector μ + ∑ a, ∑ b, H.gramVector a * H.gramVector b * P.η a b =
∑ μ, P.ξ μ * H.gramVector μ + ∑ a, ∑ b, H.gramVector a * H.gramVector b * P.η a b All goals completed! 🐙] All goals completed! 🐙TODO "Define a general effective potential for the two Higgs doublet model, mirroring
`StandardModel.HiggsField.EffectivePotential`"E. Stability of the potential
E.1. The stability condition
We define the condition that the potential is stable, that is, bounded from below.
The condition that the potential is stable.
def PotentialIsStable (P : PotentialParameters) : Prop :=
∃ c : ℝ, ∀ H : TwoHiggsDoublet, c ≤ potential P HE.2. Instability of the stabilityCounterExample potential
The potential stabilityCounterExample is not stable.