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.

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.

structure TwoHiggsDoublet.PotentialParameters : Type

The parameters of the Two Higgs doublet model potential. Following the convention of https://arxiv.org/pdf/1605.03237.

• m₁₁2 : ℝ

  The parameter corresponding to m₁₁² in the 2HDM potential.

• m₂₂2 : ℝ

  The parameter corresponding to m₂₂² in the 2HDM potential.

• m₁₂2 : ℂ

  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.

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 TwoHiggsDoublet.PotentialParameters.instZero : Zero PotentialParameters

Equations

• TwoHiggsDoublet.PotentialParameters.instZero = { zero := { m₁₁2 := 0, m₂₂2 := 0, m₁₂2 := 0, 𝓵₁ := 0, 𝓵₂ := 0, 𝓵₃ := 0, 𝓵₄ := 0, 𝓵₅ := 0, 𝓵₆ := 0, 𝓵₇ := 0 } }

@[simp]

theorem TwoHiggsDoublet.PotentialParameters.zero_m₁₁2 : m₁₁2 0 = 0

@[simp]

theorem TwoHiggsDoublet.PotentialParameters.zero_m₂₂2 : m₂₂2 0 = 0

@[simp]

theorem TwoHiggsDoublet.PotentialParameters.zero_m₁₂2 : m₁₂2 0 = 0

@[simp]

theorem TwoHiggsDoublet.PotentialParameters.zero_𝓵₁ : 𝓵₁ 0 = 0

@[simp]

theorem TwoHiggsDoublet.PotentialParameters.zero_𝓵₂ : 𝓵₂ 0 = 0

@[simp]

theorem TwoHiggsDoublet.PotentialParameters.zero_𝓵₃ : 𝓵₃ 0 = 0

@[simp]

theorem TwoHiggsDoublet.PotentialParameters.zero_𝓵₄ : 𝓵₄ 0 = 0

@[simp]

theorem TwoHiggsDoublet.PotentialParameters.zero_𝓵₅ : 𝓵₅ 0 = 0

@[simp]

theorem TwoHiggsDoublet.PotentialParameters.zero_𝓵₆ : 𝓵₆ 0 = 0

@[simp]

theorem TwoHiggsDoublet.PotentialParameters.zero_𝓵₇ : 𝓵₇ 0 = 0

A.2. Gram parameters

A reparameterization of the potential parameters corresponding to ξ and η in arXiv:hep-ph/0605184.

noncomputable def TwoHiggsDoublet.PotentialParameters.ξ (P : PotentialParameters) (μ : Fin 1 ⊕ Fin 3) : ℝ

A reparameterization of the parameters of the quadratic terms of the potential for use with the gramVector.

Equations

• P.ξ (Sum.inl 0) = (P.m₁₁2 + P.m₂₂2) / 2
• P.ξ (Sum.inr 0) = -P.m₁₂2.re
• P.ξ (Sum.inr 1) = P.m₁₂2.im
• P.ξ (Sum.inr 2) = (P.m₁₁2 - P.m₂₂2) / 2

@[simp]

theorem TwoHiggsDoublet.PotentialParameters.ξ_zero : ξ 0 = 0

noncomputable def TwoHiggsDoublet.PotentialParameters.η (P : PotentialParameters) : Fin 1 ⊕ Fin 3 → Fin 1 ⊕ Fin 3 → ℝ

A reparameterization of the parameters of the quartic terms of the potential for use with the gramVector.

Equations

• P.η (Sum.inl 0) (Sum.inl 0) = (P.𝓵₁ + P.𝓵₂ + 2 * P.𝓵₃) / 8
• P.η (Sum.inl 0) (Sum.inr 0) = (P.𝓵₆.re + P.𝓵₇.re) / 4
• P.η (Sum.inl 0) (Sum.inr 1) = -(P.𝓵₆.im + P.𝓵₇.im) / 4
• P.η (Sum.inl 0) (Sum.inr 2) = (P.𝓵₁ - P.𝓵₂) / 8
• P.η (Sum.inr 0) (Sum.inl 0) = (P.𝓵₆.re + P.𝓵₇.re) / 4
• P.η (Sum.inr 1) (Sum.inl 0) = -(P.𝓵₆.im + P.𝓵₇.im) / 4
• P.η (Sum.inr 2) (Sum.inl 0) = (P.𝓵₁ - P.𝓵₂) / 8
• P.η (Sum.inr 0) (Sum.inr 0) = (P.𝓵₅.re + P.𝓵₄) / 4
• P.η (Sum.inr 1) (Sum.inr 1) = (P.𝓵₄ - P.𝓵₅.re) / 4
• P.η (Sum.inr 2) (Sum.inr 2) = (P.𝓵₁ + P.𝓵₂ - 2 * P.𝓵₃) / 8
• P.η (Sum.inr 0) (Sum.inr 1) = -P.𝓵₅.im / 4
• P.η (Sum.inr 2) (Sum.inr 0) = (P.𝓵₆.re - P.𝓵₇.re) / 4
• P.η (Sum.inr 2) (Sum.inr 1) = (P.𝓵₇.im - P.𝓵₆.im) / 4
• P.η (Sum.inr 1) (Sum.inr 0) = -P.𝓵₅.im / 4
• P.η (Sum.inr 0) (Sum.inr 2) = (P.𝓵₆.re - P.𝓵₇.re) / 4
• P.η (Sum.inr 1) (Sum.inr 2) = (P.𝓵₇.im - P.𝓵₆.im) / 4

theorem TwoHiggsDoublet.PotentialParameters.η_symm (P : PotentialParameters) (μ ν : Fin 1 ⊕ Fin 3) : P.η μ ν = P.η ν μ

@[simp]

theorem TwoHiggsDoublet.PotentialParameters.η_zero : η 0 = 0

A.3. Specific cases

def TwoHiggsDoublet.PotentialParameters.stabilityCounterExample : PotentialParameters

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.

Equations

• One or more equations did not get rendered due to their size.

theorem TwoHiggsDoublet.PotentialParameters.stabilityCounterExample_ξ : stabilityCounterExample.ξ = fun (x : Fin 1 ⊕ Fin 3) => match x with | Sum.inl 0 => 0 | Sum.inr 0 => 0 | Sum.inr 1 => 1 | Sum.inr 2 => 0

theorem TwoHiggsDoublet.PotentialParameters.stabilityCounterExample_η : stabilityCounterExample.η = fun (μ ν : Fin 1 ⊕ Fin 3) => 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

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.

noncomputable def TwoHiggsDoublet.massTerm (P : PotentialParameters) (H : TwoHiggsDoublet) : ℝ

The mass term of the two Higgs doublet model potential.

Equations

• TwoHiggsDoublet.massTerm P H = P.m₁₁2 * ‖H.Φ1‖ ^ 2 + P.m₂₂2 * ‖H.Φ2‖ ^ 2 - (P.m₁₂2 * inner ℂ H.Φ1 H.Φ2 + (starRingEnd ℂ) P.m₁₂2 * inner ℂ H.Φ2 H.Φ1).re

theorem TwoHiggsDoublet.massTerm_eq_gramVector (P : PotentialParameters) (H : TwoHiggsDoublet) : massTerm P H = ∑ μ : Fin 1 ⊕ Fin 3, P.ξ μ * H.gramVector μ

@[simp]

theorem TwoHiggsDoublet.gaugeGroupI_smul_massTerm (g : StandardModel.GaugeGroupI) (P : PotentialParameters) (H : TwoHiggsDoublet) : massTerm P (g • H) = massTerm P H

@[simp]

theorem TwoHiggsDoublet.massTerm_zero : massTerm 0 = 0

theorem TwoHiggsDoublet.massTerm_stabilityCounterExample (H : TwoHiggsDoublet) : massTerm PotentialParameters.stabilityCounterExample H = 2 * (inner ℂ H.Φ1 H.Φ2).im

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.

noncomputable def TwoHiggsDoublet.quarticTerm (P : PotentialParameters) (H : TwoHiggsDoublet) : ℝ

The quartic term of the two Higgs doublet model potential.

Equations

• One or more equations did not get rendered due to their size.

theorem TwoHiggsDoublet.quarticTerm_𝓵₄_expand (P : PotentialParameters) (H : 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.𝓵₄ * (inner ℂ H.Φ1 H.Φ2 * inner ℂ H.Φ2 H.Φ1).re + (1 / 2 * P.𝓵₅ * inner ℂ H.Φ1 H.Φ2 ^ 2 + 1 / 2 * (starRingEnd ℂ) P.𝓵₅ * inner ℂ H.Φ2 H.Φ1 ^ 2).re + (P.𝓵₆ * ↑‖H.Φ1‖ ^ 2 * inner ℂ H.Φ1 H.Φ2 + (starRingEnd ℂ) P.𝓵₆ * ↑‖H.Φ1‖ ^ 2 * inner ℂ H.Φ2 H.Φ1).re + (P.𝓵₇ * ↑‖H.Φ2‖ ^ 2 * inner ℂ H.Φ1 H.Φ2 + (starRingEnd ℂ) P.𝓵₇ * ↑‖H.Φ2‖ ^ 2 * inner ℂ H.Φ2 H.Φ1).re

theorem TwoHiggsDoublet.quarticTerm_eq_gramVector (P : PotentialParameters) (H : TwoHiggsDoublet) : quarticTerm P H = ∑ a : Fin 1 ⊕ Fin 3, ∑ b : Fin 1 ⊕ Fin 3, H.gramVector a * H.gramVector b * P.η a b

@[simp]

theorem TwoHiggsDoublet.gaugeGroupI_smul_quarticTerm (g : StandardModel.GaugeGroupI) (P : PotentialParameters) (H : TwoHiggsDoublet) : quarticTerm P (g • H) = quarticTerm P H

@[simp]

theorem TwoHiggsDoublet.quarticTerm_zero : quarticTerm 0 = 0

theorem TwoHiggsDoublet.quarticTerm_stabilityCounterExample (H : TwoHiggsDoublet) : quarticTerm PotentialParameters.stabilityCounterExample H = (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (inner ℂ H.Φ1 H.Φ2).re) ^ 2

theorem TwoHiggsDoublet.quarticTerm_stabilityCounterExample_eq_norm_pow_four (H : TwoHiggsDoublet) : quarticTerm PotentialParameters.stabilityCounterExample H = ‖H.Φ1 - H.Φ2‖ ^ 4

theorem TwoHiggsDoublet.quarticTerm_stabilityCounterExample_nonneg (H : TwoHiggsDoublet) : 0 ≤ quarticTerm PotentialParameters.stabilityCounterExample H

theorem TwoHiggsDoublet.massTerm_zero_of_quarticTerm_zero_stabilityCounterExample (H : TwoHiggsDoublet) (h : quarticTerm PotentialParameters.stabilityCounterExample H = 0) : massTerm PotentialParameters.stabilityCounterExample H = 0

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.

noncomputable def TwoHiggsDoublet.potential (P : PotentialParameters) (H : TwoHiggsDoublet) : ℝ

The potential of the two Higgs doublet model.

Equations

• TwoHiggsDoublet.potential P H = TwoHiggsDoublet.massTerm P H + TwoHiggsDoublet.quarticTerm P H

@[simp]

theorem TwoHiggsDoublet.gaugeGroupI_smul_potential (g : StandardModel.GaugeGroupI) (P : PotentialParameters) (H : TwoHiggsDoublet) : potential P (g • H) = potential P H

@[simp]

theorem TwoHiggsDoublet.potential_zero : potential 0 = 0

theorem TwoHiggsDoublet.potential_stabilityCounterExample (H : TwoHiggsDoublet) : potential PotentialParameters.stabilityCounterExample H = 2 * (inner ℂ H.Φ1 H.Φ2).im + ‖H.Φ1 - H.Φ2‖ ^ 4

theorem TwoHiggsDoublet.potential_eq_gramVector (P : PotentialParameters) (H : TwoHiggsDoublet) : potential P H = ∑ μ : Fin 1 ⊕ Fin 3, P.ξ μ * H.gramVector μ + ∑ a : Fin 1 ⊕ Fin 3, ∑ b : Fin 1 ⊕ Fin 3, H.gramVector a * H.gramVector b * P.η a b

E. Stability of the potential

E.1. The stability condition

We define the condition that the potential is stable, that is, bounded from below.

def TwoHiggsDoublet.PotentialIsStable (P : PotentialParameters) : Prop

The condition that the potential is stable.

Equations

• TwoHiggsDoublet.PotentialIsStable P = ∃ (c : ℝ), ∀ (H : TwoHiggsDoublet), c ≤ TwoHiggsDoublet.potential P H

E.2. Instability of the stabilityCounterExample potential

theorem TwoHiggsDoublet.stabilityCounterExample_not_potentialIsStable : ¬PotentialIsStable PotentialParameters.stabilityCounterExample

The potential stabilityCounterExample is not stable.

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.

noncomputable def TwoHiggsDoublet.massTermReduced (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3)) : ℝ

A function related to the mass term of the potential, used in the stableness condition and equivalent to the term J2 in https://arxiv.org/abs/hep-ph/0605184.

Equations

• TwoHiggsDoublet.massTermReduced P k = P.ξ (Sum.inl 0) + ∑ μ : Fin 3, P.ξ (Sum.inr μ) * k.ofLp μ

theorem TwoHiggsDoublet.massTermReduced_lower_bound (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3)) (hk : ‖k‖ ^ 2 ≤ 1) : P.ξ (Sum.inl 0) - √(∑ a : Fin 3, |P.ξ (Sum.inr a)| ^ 2) ≤ massTermReduced P k

@[simp]

theorem TwoHiggsDoublet.massTermReduced_zero : massTermReduced 0 = 0

theorem TwoHiggsDoublet.massTermReduced_stabilityCounterExample (k : EuclideanSpace ℝ (Fin 3)) : massTermReduced PotentialParameters.stabilityCounterExample k = k.ofLp 1

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.

noncomputable def TwoHiggsDoublet.quarticTermReduced (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3)) : ℝ

A function related to the quartic term of the potential, used in the stableness condition and equivalent to the term J4 in https://arxiv.org/abs/hep-ph/0605184.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TwoHiggsDoublet.quarticTermReduced_zero : quarticTermReduced 0 = 0

theorem TwoHiggsDoublet.quarticTermReduced_stabilityCounterExample (k : EuclideanSpace ℝ (Fin 3)) : quarticTermReduced PotentialParameters.stabilityCounterExample k = (1 - k.ofLp 0) ^ 2

theorem TwoHiggsDoublet.quarticTermReduced_stabilityCounterExample_nonneg (k : EuclideanSpace ℝ (Fin 3)) : 0 ≤ quarticTermReduced PotentialParameters.stabilityCounterExample k

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.

theorem TwoHiggsDoublet.potentialIsStable_iff_forall_gramVector (P : PotentialParameters) : PotentialIsStable P ↔ ∃ (c : ℝ), ∀ (K : Fin 1 ⊕ Fin 3 → ℝ), 0 ≤ K (Sum.inl 0) → ∑ μ : Fin 3, K (Sum.inr μ) ^ 2 ≤ K (Sum.inl 0) ^ 2 → c ≤ ∑ μ : Fin 1 ⊕ Fin 3, P.ξ μ * K μ + ∑ a : Fin 1 ⊕ Fin 3, ∑ b : Fin 1 ⊕ Fin 3, K a * K b * P.η a b

theorem TwoHiggsDoublet.potentialIsStable_iff_forall_euclid (P : PotentialParameters) : PotentialIsStable P ↔ ∃ (c : ℝ), ∀ (K0 : ℝ) (K : EuclideanSpace ℝ (Fin 3)), 0 ≤ K0 → ‖K‖ ^ 2 ≤ K0 ^ 2 → c ≤ P.ξ (Sum.inl 0) * K0 + ∑ μ : Fin 3, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * ∑ b : Fin 3, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + ∑ a : Fin 3, ∑ b : Fin 3, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)

theorem TwoHiggsDoublet.potentialIsStable_iff_forall_euclid_lt (P : PotentialParameters) : PotentialIsStable P ↔ ∃ c ≤ 0, ∀ (K0 : ℝ) (K : EuclideanSpace ℝ (Fin 3)), 0 < K0 → ‖K‖ ^ 2 ≤ K0 ^ 2 → c ≤ P.ξ (Sum.inl 0) * K0 + ∑ μ : Fin 3, P.ξ (Sum.inr μ) * K.ofLp μ + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0) + 2 * K0 * ∑ b : Fin 3, K.ofLp b * P.η (Sum.inl 0) (Sum.inr b) + ∑ a : Fin 3, ∑ b : Fin 3, K.ofLp a * K.ofLp b * P.η (Sum.inr a) (Sum.inr b)

theorem TwoHiggsDoublet.potentialIsStable_iff_exists_forall_forall_reduced (P : PotentialParameters) : PotentialIsStable P ↔ ∃ c ≤ 0, ∀ (K0 : ℝ) (k : EuclideanSpace ℝ (Fin 3)), 0 < K0 → ‖k‖ ^ 2 ≤ 1 → c ≤ K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P k

theorem TwoHiggsDoublet.quarticTermReduced_nonneg_of_potentialIsStable (P : PotentialParameters) (hP : PotentialIsStable P) (k : EuclideanSpace ℝ (Fin 3)) (hk : ‖k‖ ^ 2 ≤ 1) : 0 ≤ quarticTermReduced P k

theorem TwoHiggsDoublet.potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced (P : PotentialParameters) : PotentialIsStable P ↔ ∃ (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)

theorem TwoHiggsDoublet.massTermReduced_pos_of_quarticTermReduced_zero_potentialIsStable (P : PotentialParameters) (hP : PotentialIsStable P) (k : EuclideanSpace ℝ (Fin 3)) (hk : ‖k‖ ^ 2 ≤ 1) (hq : quarticTermReduced P k = 0) : 0 ≤ massTermReduced P k

E.6. Strong stability implies stability

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

theorem TwoHiggsDoublet.potentialIsStable_of_strong (P : PotentialParameters) (h : ∀ (k : EuclideanSpace ℝ (Fin 3)), ‖k‖ ^ 2 ≤ 1 → 0 < quarticTermReduced P k) : PotentialIsStable P

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.

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

theorem TwoHiggsDoublet.forall_reduced_exists_not_potentialIsStable : ∃ (P : PotentialParameters), ¬PotentialIsStable P ∧ ∀ (k : EuclideanSpace ℝ (Fin 3)), ‖k‖ ^ 2 ≤ 1 → 0 ≤ quarticTermReduced P k ∧ (quarticTermReduced P k = 0 → 0 ≤ massTermReduced P k)

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