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

The 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 section

A. 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 := rfl

A.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 3P.η μ ν = P.η ν μ P:PotentialParametersν:Fin 1 Fin 3P.η (Sum.inl ((fun i => i) 0, )) ν = P.η ν (Sum.inl ((fun i => i) 0, ))P:PotentialParametersν:Fin 1 Fin 3P.η (Sum.inr ((fun i => i) 0, )) ν = P.η ν (Sum.inr ((fun i => i) 0, ))P:PotentialParametersν:Fin 1 Fin 3P.η (Sum.inr ((fun i => i) 1, )) ν = P.η ν (Sum.inr ((fun i => i) 1, ))P:PotentialParametersν:Fin 1 Fin 3P.η (Sum.inr ((fun i => i) 2, )) ν = P.η ν (Sum.inr ((fun i => i) 2, )) P:PotentialParametersν:Fin 1 Fin 3P.η (Sum.inl ((fun i => i) 0, )) ν = P.η ν (Sum.inl ((fun i => i) 0, ))P:PotentialParametersν:Fin 1 Fin 3P.η (Sum.inr ((fun i => i) 0, )) ν = P.η ν (Sum.inr ((fun i => i) 0, ))P:PotentialParametersν:Fin 1 Fin 3P.η (Sum.inr ((fun i => i) 1, )) ν = P.η ν (Sum.inr ((fun i => i) 1, ))P:PotentialParametersν:Fin 1 Fin 3P.η (Sum.inr ((fun i => i) 2, )) ν = P.η ν (Sum.inr ((fun i => i) 2, )) P:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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:PotentialParametersP.η (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 3stabilityCounterExample.ξ μ = 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 3stabilityCounterExample.η μ ν = 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:TwoHiggsDoubletmassTerm P H = μ, P.ξ μ * H.gramVector μ P:PotentialParametersH:TwoHiggsDoubletP.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:TwoHiggsDoubletmassTerm P (g H) = massTerm P H All goals completed! 🐙@[simp] lemma massTerm_zero : massTerm 0 = 0 := massTerm 0 = 0 H:TwoHiggsDoubletmassTerm 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 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.

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 := P:PotentialParametersH:TwoHiggsDoubletquarticTerm P H = a, b, H.gramVector a * H.gramVector b * P.η a b P:PotentialParametersH:TwoHiggsDoublet2⁻¹ * 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)))) P:PotentialParametersH:TwoHiggsDoubletP.𝓵₁ * 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) P:PotentialParametersH:TwoHiggsDoubletP.𝓵₁ * 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) All goals completed! 🐙@[simp] lemma gaugeGroupI_smul_quarticTerm (g : StandardModel.GaugeGroupI) (P : PotentialParameters) (H : TwoHiggsDoublet) : quarticTerm P (g H) = quarticTerm P H := g:GaugeGroupIP:PotentialParametersH:TwoHiggsDoubletquarticTerm P (g H) = quarticTerm P H All goals completed! 🐙@[simp] lemma quarticTerm_zero : quarticTerm 0 = 0 := quarticTerm 0 = 0 H:TwoHiggsDoubletquarticTerm 0 H = 0 H All goals completed! 🐙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 * 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) 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 All goals completed! 🐙H:TwoHiggsDoublet0 H.Φ1 - H.Φ2 ^ 4 All goals completed! 🐙H:TwoHiggsDoubleth:H.Φ1 - H.Φ2 ^ 4 = 0h1:H.Φ1 = H.Φ22 * (H.Φ1, H.Φ2⟫_).im = 0 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 := g:GaugeGroupIP:PotentialParametersH:TwoHiggsDoubletpotential P (g H) = potential P H All goals completed! 🐙@[simp] lemma potential_zero : potential 0 = 0 := potential 0 = 0 H:TwoHiggsDoubletpotential 0 H = 0 H All goals completed! 🐙lemma potential_stabilityCounterExample (H : TwoHiggsDoublet) : potential .stabilityCounterExample H = 2 * (H.Φ1, H.Φ2⟫_).im + H.Φ1 - H.Φ2 ^ 4 := H:TwoHiggsDoubletpotential PotentialParameters.stabilityCounterExample H = 2 * (H.Φ1, H.Φ2⟫_).im + H.Φ1 - H.Φ2 ^ 4 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 H

E.2. Instability of the stabilityCounterExample potential

The potential stabilityCounterExample is not stable.

c:t: := arctan (2 * (|c| + 1))⁻¹t_pos:0 < tt_le_pi_div_2:t π / 2t_ne_zero:t 0sin_t_pos:0 < sin tcos_t_pos:0 < cos tt_mul_sin_t_nonneg:0 2 * t * sin t - t ^ 2H:TwoHiggsDoublet := { Φ1 := ![(cos t / (4 * t * sin t ^ 2)), 0], Φ2 := (cos t / (4 * t * sin t ^ 2)) ![1 - t * (sin t) - Complex.I * t * (cos t), (2 * t * sin t - t ^ 2)] }Φ1_norm_sq:H.Φ1 ^ 2 = cos t / (4 * t * sin t ^ 2)Φ2_norm_sq:H.Φ2 ^ 2 = cos t / (4 * t * sin t ^ 2)Φ1_inner_Φ2:H.Φ1, H.Φ2⟫_ = (cos t / (4 * t * sin t ^ 2) * (1 - t * sin t)) + Complex.I * (cos t / (4 * t * sin t ^ 2) * (-t * cos t))Φ1_inner_Φ2_re:(H.Φ1, H.Φ2⟫_).re = cos t / (4 * t * sin t ^ 2) * (1 - t * sin t)Φ1_inner_Φ2_im:(H.Φ1, H.Φ2⟫_).im = cos t / (4 * t * sin t ^ 2) * (-t * cos t)potential_H_cos_sin:potential PotentialParameters.stabilityCounterExample H = -cos t ^ 2 / (4 * sin t ^ 2)potential_eq_c:potential PotentialParameters.stabilityCounterExample H = -(|c| + 1)-(|c| + 1) < c All goals completed! 🐙

E.3. The reduced mass term

The reduced mass term is a function that helps express the stability condition. It is the function J2 in https://arxiv.org/abs/hep-ph/0605184.

P:PotentialParametersk:EuclideanSpace (Fin 3)h1: (a b c : ), -b c a - b a + cξEuclid:EuclideanSpace (Fin 3) := WithLp.toLp 2 fun a => P.ξ (Sum.inr a)hk:k 1ha: (a b : ), a 1 0 a 0 b a * b bk * ξEuclid ξEuclid All goals completed! 🐙 P:PotentialParametersk:EuclideanSpace (Fin 3)hk:k ^ 2 1h1: (a b c : ), -b c a - b a + cξEuclid:EuclideanSpace (Fin 3) := WithLp.toLp 2 fun a => P.ξ (Sum.inr a)-(k * ξEuclid) -k, ξEuclid⟫_P:PotentialParametersk:EuclideanSpace (Fin 3)hk:k ^ 2 1h1: (a b c : ), -b c a - b a + cξEuclid:EuclideanSpace (Fin 3) := WithLp.toLp 2 fun a => P.ξ (Sum.inr a)-k, ξEuclid⟫_ x, P.ξ (Sum.inr x) * k.ofLp x P:PotentialParametersk:EuclideanSpace (Fin 3)hk:k ^ 2 1h1: (a b c : ), -b c a - b a + cξEuclid:EuclideanSpace (Fin 3) := WithLp.toLp 2 fun a => P.ξ (Sum.inr a)-(k * ξEuclid) -k, ξEuclid⟫_ P:PotentialParametersk:EuclideanSpace (Fin 3)hk:k ^ 2 1h1: (a b c : ), -b c a - b a + cξEuclid:EuclideanSpace (Fin 3) := WithLp.toLp 2 fun a => P.ξ (Sum.inr a)|k, ξEuclid⟫_| k * ξEuclid All goals completed! 🐙 P:PotentialParametersk:EuclideanSpace (Fin 3)hk:k ^ 2 1h1: (a b c : ), -b c a - b a + cξEuclid:EuclideanSpace (Fin 3) := WithLp.toLp 2 fun a => P.ξ (Sum.inr a)-k, ξEuclid⟫_ k, ξEuclid⟫_P:PotentialParametersk:EuclideanSpace (Fin 3)hk:k ^ 2 1h1: (a b c : ), -b c a - b a + cξEuclid:EuclideanSpace (Fin 3) := WithLp.toLp 2 fun a => P.ξ (Sum.inr a)k, ξEuclid⟫_ x, P.ξ (Sum.inr x) * k.ofLp x P:PotentialParametersk:EuclideanSpace (Fin 3)hk:k ^ 2 1h1: (a b c : ), -b c a - b a + cξEuclid:EuclideanSpace (Fin 3) := WithLp.toLp 2 fun a => P.ξ (Sum.inr a)-k, ξEuclid⟫_ k, ξEuclid⟫_ P:PotentialParametersk:EuclideanSpace (Fin 3)hk:k ^ 2 1h1: (a b c : ), -b c a - b a + cξEuclid:EuclideanSpace (Fin 3) := WithLp.toLp 2 fun a => P.ξ (Sum.inr a)-|k, ξEuclid⟫_| k, ξEuclid⟫_ All goals completed! 🐙 All goals completed! 🐙@[simp] lemma massTermReduced_zero : massTermReduced 0 = 0 := massTermReduced 0 = 0 k:EuclideanSpace (Fin 3)massTermReduced 0 k = 0 k All goals completed! 🐙lemma massTermReduced_stabilityCounterExample (k : EuclideanSpace (Fin 3)) : massTermReduced .stabilityCounterExample k = k 1 := k:EuclideanSpace (Fin 3)massTermReduced PotentialParameters.stabilityCounterExample k = k.ofLp 1 All goals completed! 🐙

E.4. The reduced quartic term

The reduced quartic term is a function that helps express the stability condition. It is the function J4 in https://arxiv.org/abs/hep-ph/0605184.

@[simp] lemma quarticTermReduced_zero : quarticTermReduced 0 = 0 := quarticTermReduced 0 = 0 k:EuclideanSpace (Fin 3)quarticTermReduced 0 k = 0 k All goals completed! 🐙lemma quarticTermReduced_stabilityCounterExample (k : EuclideanSpace (Fin 3)) : quarticTermReduced .stabilityCounterExample k = (1 - k 0) ^ 2 := k:EuclideanSpace (Fin 3)quarticTermReduced PotentialParameters.stabilityCounterExample k = (1 - k.ofLp 0) ^ 2 k:EuclideanSpace (Fin 3)(2 + 2 + 2 * 2) / 8 + 2 * (k.ofLp 0 * ((-2 + -2) / 4)) + (k.ofLp 0 * k.ofLp 0 * ((2 + 2) / 4) + k.ofLp 2 * k.ofLp 2 * ((2 + 2 - 2 * 2) / 8)) = (1 - k.ofLp 0) ^ 2 All goals completed! 🐙k:EuclideanSpace (Fin 3)0 (1 - k.ofLp 0) ^ 2 All goals completed! 🐙

E.5. Stability in terms of the gram vectors

We give some necessary and sufficient conditions for the potential to be stable in terms of the gram vectors.

This follows the analysis in https://arxiv.org/abs/hep-ph/0605184.

We also give some necessary conditions.

All goals completed! 🐙P:PotentialParametersc:K0:(∀ (b : WithLp 2 ((i : Fin 3) (fun x => ) i)), 0 (Equiv.funUnique (Fin 1) ).symm K0 0 x, (WithLp.equiv 2 ((i : Fin 3) (fun x => ) i)).symm.symm b x ^ 2 (Equiv.funUnique (Fin 1) ).symm K0 0 ^ 2 c P.ξ (Sum.inl 0) * (Equiv.funUnique (Fin 1) ).symm K0 0 + x, P.ξ (Sum.inr x) * (WithLp.equiv 2 ((i : Fin 3) (fun x => ) i)).symm.symm b x + ((Equiv.funUnique (Fin 1) ).symm K0 0 * (Equiv.funUnique (Fin 1) ).symm K0 0 * P.η (Sum.inl 0) (Sum.inl 0) + x, (Equiv.funUnique (Fin 1) ).symm K0 0 * (WithLp.equiv 2 ((i : Fin 3) (fun x => ) i)).symm.symm b x * P.η (Sum.inl 0) (Sum.inr x) + x, ((WithLp.equiv 2 ((i : Fin 3) (fun x => ) i)).symm.symm b x * (Equiv.funUnique (Fin 1) ).symm K0 0 * P.η (Sum.inr x) (Sum.inl 0) + x_1, (WithLp.equiv 2 ((i : Fin 3) (fun x => ) i)).symm.symm b x * (WithLp.equiv 2 ((i : Fin 3) (fun x => ) i)).symm.symm b x_1 * P.η (Sum.inr x) (Sum.inr x_1)))) (K : EuclideanSpace (Fin 3)), 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) P:PotentialParametersc:K0:K:WithLp 2 ((i : Fin 3) (fun x => ) i)0 (Equiv.funUnique (Fin 1) ).symm K0 0 x, (WithLp.equiv 2 ((i : Fin 3) (fun x => ) i)).symm.symm K x ^ 2 (Equiv.funUnique (Fin 1) ).symm K0 0 ^ 2 c P.ξ (Sum.inl 0) * (Equiv.funUnique (Fin 1) ).symm K0 0 + x, P.ξ (Sum.inr x) * (WithLp.equiv 2 ((i : Fin 3) (fun x => ) i)).symm.symm K x + ((Equiv.funUnique (Fin 1) ).symm K0 0 * (Equiv.funUnique (Fin 1) ).symm K0 0 * P.η (Sum.inl 0) (Sum.inl 0) + x, (Equiv.funUnique (Fin 1) ).symm K0 0 * (WithLp.equiv 2 ((i : Fin 3) (fun x => ) i)).symm.symm K x * P.η (Sum.inl 0) (Sum.inr x) + x, ((WithLp.equiv 2 ((i : Fin 3) (fun x => ) i)).symm.symm K x * (Equiv.funUnique (Fin 1) ).symm K0 0 * P.η (Sum.inr x) (Sum.inl 0) + x_1, (WithLp.equiv 2 ((i : Fin 3) (fun x => ) i)).symm.symm K x * (WithLp.equiv 2 ((i : Fin 3) (fun x => ) i)).symm.symm K x_1 * P.η (Sum.inr x) (Sum.inr x_1))) 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) P:PotentialParametersc:K0:K:WithLp 2 ((i : Fin 3) (fun x => ) i)0 K0 x, K.ofLp x ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + (K0 * K0 * P.η (Sum.inl 0) (Sum.inl 0) + x, K0 * K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, (K.ofLp x * K0 * P.η (Sum.inr x) (Sum.inl 0) + x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1))) 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) P:PotentialParametersc:K0:K:WithLp 2 ((i : Fin 3) (fun x => ) i)x✝:0 K0 x, K.ofLp x ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + (K0 * K0 * P.η (Sum.inl 0) (Sum.inl 0) + x, K0 * K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, (K.ofLp x * K0 * P.η (Sum.inr x) (Sum.inl 0) + x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1))) K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) P:PotentialParametersc:K0:K:WithLp 2 ((i : Fin 3) (fun x => ) i)x✝:0 K0 x, K.ofLp x ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + (K0 * K0 * P.η (Sum.inl 0) (Sum.inl 0) + x, K0 * K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, (K.ofLp x * K0 * P.η (Sum.inr x) (Sum.inl 0) + x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1))) x, K.ofLp x ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) P:PotentialParametersc:K0:K:WithLp 2 ((i : Fin 3) (fun x => ) i)x✝¹:0 K0x✝: x, K.ofLp x ^ 2 K0 ^ 2c P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + (K0 * K0 * P.η (Sum.inl 0) (Sum.inl 0) + x, K0 * K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, (K.ofLp x * K0 * P.η (Sum.inr x) (Sum.inl 0) + x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1))) c P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) P:PotentialParametersc:K0:K:WithLp 2 ((i : Fin 3) (fun x => ) i)x✝¹:0 K0x✝: x, K.ofLp x ^ 2 K0 ^ 2cmp c (P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + (K0 * K0 * P.η (Sum.inl 0) (Sum.inl 0) + x, K0 * K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, (K.ofLp x * K0 * P.η (Sum.inr x) (Sum.inl 0) + x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1)))) = cmp c (P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1)) P:PotentialParametersc:K0:K:WithLp 2 ((i : Fin 3) (fun x => ) i)x✝¹:0 K0x✝: x, K.ofLp x ^ 2 K0 ^ 2P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + (K0 * K0 * P.η (Sum.inl 0) (Sum.inl 0) + x, K0 * K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, (K.ofLp x * K0 * P.η (Sum.inr x) (Sum.inl 0) + x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1))) = P.ξ (Sum.inl 0) * K0 + x, P.ξ (Sum.inr x) * K.ofLp x + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) P:PotentialParametersc:K0:K:WithLp 2 ((i : Fin 3) (fun x => ) i)x✝¹:0 K0x✝: x, K.ofLp x ^ 2 K0 ^ 2 x, K0 * K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + ( x, K.ofLp x * K0 * P.η (Sum.inr x) (Sum.inl 0) + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1)) = 2 * K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) P:PotentialParametersc:K0:K:WithLp 2 ((i : Fin 3) (fun x => ) i)x✝¹:0 K0x✝: x, K.ofLp x ^ 2 K0 ^ 2 x, K0 * K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, K0 * K.ofLp x * P.η (Sum.inr x) (Sum.inl 0) + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) = (K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2 + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) P:PotentialParametersc:K0:K:WithLp 2 ((i : Fin 3) (fun x => ) i)x✝¹:0 K0x✝: x, K.ofLp x ^ 2 K0 ^ 2K0 * i, K.ofLp i * P.η (Sum.inl 0) (Sum.inr i) + K0 * i, K.ofLp i * P.η (Sum.inr i) (Sum.inl 0) = K0 * ((∑ x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2) conv_lhs => P:PotentialParametersc:K0:K:WithLp 2 ((i : Fin 3) (fun x => ) i)x✝¹:0 K0x✝: x, K.ofLp x ^ 2 K0 ^ 2i:Fin 3| K.ofLp i * P.η (Sum.inr i) (Sum.inl 0) P:PotentialParametersc:K0:K:WithLp 2 ((i : Fin 3) (fun x => ) i)x✝¹:0 K0x✝: x, K.ofLp x ^ 2 K0 ^ 2i:Fin 3| K.ofLp i * P.η (Sum.inl 0) (Sum.inr i) All goals completed! 🐙P:PotentialParameters(∃ c, (K0 : ) (K : EuclideanSpace (Fin 3)), 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)) c 0, (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) P:PotentialParameters(∃ c, (K0 : ) (K : EuclideanSpace (Fin 3)), 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)) c 0, (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)P:PotentialParameters(∃ c 0, (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)) c, (K0 : ) (K : EuclideanSpace (Fin 3)), 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) P:PotentialParameters(∃ c, (K0 : ) (K : EuclideanSpace (Fin 3)), 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)) c 0, (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) P:PotentialParametersc:hc: (K0 : ) (K : EuclideanSpace (Fin 3)), 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) c 0, (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) P:PotentialParametersc:hc: (K0 : ) (K : EuclideanSpace (Fin 3)), 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)c 0 simpa using hc 0 0 (P:PotentialParametersc:hc: (K0 : ) (K : EuclideanSpace (Fin 3)), 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)0 0 All goals completed! 🐙) (P:PotentialParametersc:hc: (K0 : ) (K : EuclideanSpace (Fin 3)), 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)0 ^ 2 0 ^ 2 All goals completed! 🐙) P:PotentialParameters(∃ c 0, (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)) c, (K0 : ) (K : EuclideanSpace (Fin 3)), 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) P:PotentialParametersc:hc₀:c 0hc: (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) c, (K0 : ) (K : EuclideanSpace (Fin 3)), 0 K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) P:PotentialParametersc:hc₀:c 0hc: (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)K0:K:EuclideanSpace (Fin 3)hK0:0 K0hle:K ^ 2 K0 ^ 2c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) P:PotentialParametersc:hc₀:c 0hc: (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)K0:K:EuclideanSpace (Fin 3)hK0:0 K0hle:K ^ 2 K0 ^ 2hK0':K0 = 0c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)P:PotentialParametersc:hc₀:c 0hc: (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)K0:K:EuclideanSpace (Fin 3)hK0:0 K0hle:K ^ 2 K0 ^ 2hK0':¬K0 = 0c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) P:PotentialParametersc:hc₀:c 0hc: (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)K0:K:EuclideanSpace (Fin 3)hK0:0 K0hle:K ^ 2 K0 ^ 2hK0':K0 = 0c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) P:PotentialParametersc:hc₀:c 0hc: (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)K:EuclideanSpace (Fin 3)hK0:0 0hle:K ^ 2 0 ^ 2c P.ξ (Sum.inl 0) * 0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + 0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * 0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) All goals completed! 🐙 P:PotentialParametersc:hc₀:c 0hc: (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)K0:K:EuclideanSpace (Fin 3)hK0:0 K0hle:K ^ 2 K0 ^ 2hK0':¬K0 = 0c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) P:PotentialParametersc:hc₀:c 0hc: (K0 : ) (K : EuclideanSpace (Fin 3)), 0 < K0 K ^ 2 K0 ^ 2 c P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)K0:K:EuclideanSpace (Fin 3)hK0:0 K0hle:K ^ 2 K0 ^ 2hK0':¬K0 = 00 < K0 All goals completed! 🐙P:PotentialParametersc:hc:c 0K0:h: (k : EuclideanSpace (Fin 3)), 0 < K0 k ^ 2 1 c K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P kK:EuclideanSpace (Fin 3)hK0:0 < K0hle:|K| |K0|K |K0| All goals completed! 🐙 P:PotentialParametersc:hc:c 0K0:h: (k : EuclideanSpace (Fin 3)), 0 < K0 k ^ 2 1 c K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P kK:EuclideanSpace (Fin 3)hK0:0 < K0hle:K ^ 2 K0 ^ 2K0 * massTermReduced P ((1 / K0) K) + K0 ^ 2 * quarticTermReduced P ((1 / K0) K) = P.ξ (Sum.inl 0) * K0 + μ, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * b, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + a, b, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b) P:PotentialParametersc:hc:c 0K0:h: (k : EuclideanSpace (Fin 3)), 0 < K0 k ^ 2 1 c K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P kK:EuclideanSpace (Fin 3)hK0:0 < K0hle:K ^ 2 K0 ^ 2K0 * (P.ξ (Sum.inl 0) + x, P.ξ (Sum.inr x) * (K0⁻¹ * K.ofLp x)) + K0 ^ 2 * (P.η (Sum.inl 0) (Sum.inl 0) + (2 * x, K0⁻¹ * K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, x_1, K0⁻¹ * K.ofLp x * (K0⁻¹ * K.ofLp x_1) * P.η (Sum.inr x) (Sum.inr x_1))) = P.ξ (Sum.inl 0) * K0 + ( x, P.ξ (Sum.inr x) * K.ofLp x + (K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + (2 * K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x) + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1)))) P:PotentialParametersc:hc:c 0K0:h: (k : EuclideanSpace (Fin 3)), 0 < K0 k ^ 2 1 c K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P kK:EuclideanSpace (Fin 3)hK0:0 < K0hle:K ^ 2 K0 ^ 2K0 * P.ξ (Sum.inl 0) + K0 * x, P.ξ (Sum.inr x) * K0⁻¹ * K.ofLp x + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + (K0 ^ 2 * x, K0⁻¹ * K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2 + K0 ^ 2 * x, x_1, K0⁻¹ ^ 2 * K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) = K0 * P.ξ (Sum.inl 0) + (K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2 + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + x, P.ξ (Sum.inr x) * K.ofLp x + x, x_1, K.ofLp x * K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) P:PotentialParametersc:hc:c 0K0:h: (k : EuclideanSpace (Fin 3)), 0 < K0 k ^ 2 1 c K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P kK:EuclideanSpace (Fin 3)hK0:0 < K0hle:K ^ 2 K0 ^ 2K0 * x, P.ξ (Sum.inr x) * (K0⁻¹ * K.ofLp x) + (K0 * (K0 * P.η (Sum.inl 0) (Sum.inl 0)) + (K0 * (K0 * (K0⁻¹ * ((∑ i, K.ofLp i * P.η (Sum.inl 0) (Sum.inr i)) * 2))) + K0 * (K0 * (K0⁻¹ * (K0⁻¹ * i, K.ofLp i * i_1, K.ofLp i_1 * P.η (Sum.inr i) (Sum.inr i_1)))))) = K0 * ((∑ x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2) + (K0 * (K0 * P.η (Sum.inl 0) (Sum.inl 0)) + ( x, P.ξ (Sum.inr x) * K.ofLp x + i, K.ofLp i * i_1, K.ofLp i_1 * P.η (Sum.inr i) (Sum.inr i_1))) P:PotentialParametersc:hc:c 0K0:h: (k : EuclideanSpace (Fin 3)), 0 < K0 k ^ 2 1 c K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P kK:EuclideanSpace (Fin 3)hK0:0 < K0hle:K ^ 2 K0 ^ 2K0 * x, P.ξ (Sum.inr x) * K.ofLp x / K0 + (K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + ((K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2 + x, K.ofLp x * x_1, K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1))) = (K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2 + (K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + ( x, P.ξ (Sum.inr x) * K.ofLp x + x, K.ofLp x * x_1, K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1))) P:PotentialParametersc:hc:c 0K0:h: (k : EuclideanSpace (Fin 3)), 0 < K0 k ^ 2 1 c K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P kK:EuclideanSpace (Fin 3)hK0:0 < K0hle:K ^ 2 K0 ^ 2K0 * x, P.ξ (Sum.inr x) * K.ofLp x * K0⁻¹ + (K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2 + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + x, K.ofLp x * x_1, K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) = (K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2 + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + x, K.ofLp x * x_1, K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) + x, P.ξ (Sum.inr x) * K.ofLp x P:PotentialParametersc:hc:c 0K0:h: (k : EuclideanSpace (Fin 3)), 0 < K0 k ^ 2 1 c K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P kK:EuclideanSpace (Fin 3)hK0:0 < K0hle:K ^ 2 K0 ^ 2K0 * ((∑ i, P.ξ (Sum.inr i) * K.ofLp i) * K0⁻¹) + (K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2 + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + x, K.ofLp x * x_1, K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) = (K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2 + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + x, K.ofLp x * x_1, K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) + i, P.ξ (Sum.inr i) * K.ofLp i P:PotentialParametersc:hc:c 0K0:h: (k : EuclideanSpace (Fin 3)), 0 < K0 k ^ 2 1 c K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P kK:EuclideanSpace (Fin 3)hK0:0 < K0hle:K ^ 2 K0 ^ 2 x, P.ξ (Sum.inr x) * K.ofLp x + (K0 * x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2 + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + x, K.ofLp x * x_1, K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) = K0 * ((∑ x, K.ofLp x * P.η (Sum.inl 0) (Sum.inr x)) * 2 + K0 * P.η (Sum.inl 0) (Sum.inl 0)) + x, K.ofLp x * x_1, K.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1) + x, P.ξ (Sum.inr x) * K.ofLp x All goals completed! 🐙P:PotentialParametershP: c 0, (K0 : ) (k : EuclideanSpace (Fin 3)), 0 < K0 k ^ 2 1 c K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P kk:EuclideanSpace (Fin 3)hk:k ^ 2 1a:b:hb:¬b = 0c1:d:h1: (x : ), a * x + b * x ^ 2 = b * (x + d) ^ 2 - c1hlt: (c x : ), c a * x + b * x ^ 2 c + c1 b * (x + d) ^ 2c:hc: (x : ), 0 < x c b * (x + d) ^ 2hn:¬0 b (x : ), 0 < x (x + d) ^ 2 c / b exact fun x hx => (le_div_iff_of_neg (P:PotentialParametershP: c 0, (K0 : ) (k : EuclideanSpace (Fin 3)), 0 < K0 k ^ 2 1 c K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P kk:EuclideanSpace (Fin 3)hk:k ^ 2 1a:b:hb:¬b = 0c1:d:h1: (x : ), a * x + b * x ^ 2 = b * (x + d) ^ 2 - c1hlt: (c x : ), c a * x + b * x ^ 2 c + c1 b * (x + d) ^ 2c:hc: (x : ), 0 < x c b * (x + d) ^ 2hn:¬0 bx:hx:0 < xb < 0 All goals completed! 🐙)).mpr (P:PotentialParametershP: c 0, (K0 : ) (k : EuclideanSpace (Fin 3)), 0 < K0 k ^ 2 1 c K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P kk:EuclideanSpace (Fin 3)hk:k ^ 2 1a:b:hb:¬b = 0c1:d:h1: (x : ), a * x + b * x ^ 2 = b * (x + d) ^ 2 - c1hlt: (c x : ), c a * x + b * x ^ 2 c + c1 b * (x + d) ^ 2c:hc: (x : ), 0 < x c b * (x + d) ^ 2hn:¬0 bx:hx:0 < xc (x + d) ^ 2 * b All goals completed! 🐙)P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)-c j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4) P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:j2 < 0-c j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:¬j2 < 0-c j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4) P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:j2 < 0-c j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4) P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:j2 < 0-c j4 * (K0 + j2 / (2 * j4)) ^ 2 - cP:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:j2 < 0j4 * (K0 + j2 / (2 * j4)) ^ 2 - c j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4) P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:j2 < 0-c j4 * (K0 + j2 / (2 * j4)) ^ 2 - c All goals completed! 🐙 P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:j2 < 0j4 * (K0 + j2 / (2 * j4)) ^ 2 - c j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4) P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:j2 < 0((j4 * K0 * 2 + j2) ^ 2 - j4 * 2 ^ 2 * c) * 4 (j4 * K0 * 2 + j2) ^ 2 * 4 - j2 ^ 2 * 2 ^ 2 All goals completed! 🐙 P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:¬j2 < 0-c j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4) P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:¬j2 < 0j2 ^ 2 / (4 * j4) j4 * (K0 + j2 / (2 * j4)) ^ 2 + c P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:¬j2 < 0j2 ^ 2 / (4 * j4) j4 * (K0 + j2 / (2 * j4)) ^ 2P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:¬j2 < 0j4 * (K0 + j2 / (2 * j4)) ^ 2 j4 * (K0 + j2 / (2 * j4)) ^ 2 + c P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:¬j2 < 0j2 ^ 2 / (4 * j4) j4 * (K0 + j2 / (2 * j4)) ^ 2 All goals completed! 🐙 P:PotentialParametersx✝: c, 0 c (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 quarticTermReduced P k (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * quarticTermReduced P k * c)c:hc:0 cK0:k:EuclideanSpace (Fin 3)hk0:0 < K0hk:k ^ 2 1j2:j4:h:0 j4 (j2 < 0 j2 ^ 2 4 * j4 * c)hJ4:¬j4 = 0hJ4_pos:0 < j4h0:K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4)hJ2_neg:¬j2 < 0j4 * (K0 + j2 / (2 * j4)) ^ 2 j4 * (K0 + j2 / (2 * j4)) ^ 2 + c All goals completed! 🐙P:PotentialParametersk:EuclideanSpace (Fin 3)hk:k ^ 2 1hq:quarticTermReduced P k = 0c:hc₀:0 chc:0 0 (massTermReduced P k < 0 massTermReduced P k ^ 2 4 * 0 * c)0 massTermReduced P k P:PotentialParametersk:EuclideanSpace (Fin 3)hk:k ^ 2 1hq:quarticTermReduced P k = 0c:hc₀:0 chc:massTermReduced P k < 0 massTermReduced P k = 00 massTermReduced P k All goals completed! 🐙

E.6. Strong stability implies stability

Stability in terms of the positivity of the quartic term, implies that the whole potential is stable.

The potential is stable if it is strongly stable, i.e. its quartic term is always positive. The proof of this result relies on the compactness of the closed unit ball in EuclideanSpace ℝ (Fin 3), and the extreme value theorem.

P:PotentialParametersh: (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 < quarticTermReduced P kS:Set (EuclideanSpace (Fin 3)) := Metric.closedBall 0 1S_nonEmpty:S.Nonemptykmax:EuclideanSpace (Fin 3)kmax_S:kmax Metric.closedBall 0 1kmax_isMax: x Metric.closedBall 0 1, massTermReduced P x ^ 2 / (4 * quarticTermReduced P x) massTermReduced P kmax ^ 2 / (4 * quarticTermReduced P kmax)k:EuclideanSpace (Fin 3)hk:k ^ 2 1hq:massTermReduced P k < 0massTermReduced P k ^ 2 4 * quarticTermReduced P k * (massTermReduced P kmax ^ 2 / (4 * quarticTermReduced P kmax)) refine (div_le_iff₀' ?_).mp (kmax_isMax k (P:PotentialParametersh: (k : EuclideanSpace (Fin 3)), k ^ 2 1 0 < quarticTermReduced P kS:Set (EuclideanSpace (Fin 3)) := Metric.closedBall 0 1S_nonEmpty:S.Nonemptykmax:EuclideanSpace (Fin 3)kmax_S:kmax Metric.closedBall 0 1kmax_isMax: x Metric.closedBall 0 1, massTermReduced P x ^ 2 / (4 * quarticTermReduced P x) massTermReduced P kmax ^ 2 / (4 * quarticTermReduced P kmax)k:EuclideanSpace (Fin 3)hk:k ^ 2 1hq:massTermReduced P k < 0k Metric.closedBall 0 1 All goals completed! 🐙)) All goals completed! 🐙

E.7. Showing step in hep-ph/0605184 is invalid

A lemma invalidating the step in https://arxiv.org/pdf/hep-ph/0605184 leading to equation (4.4).

All goals completed! 🐙