Research proof index

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

For an element P of Potential with l < 0 and a real c : ℝ, there exists a Higgs field φ and a spacetime point x such that P.toFun φ x = c iff one of the following two conditions hold: - 0 < μ2 and c ≤ 0. That is, if l is negative and μ2 positive, then the potential takes every non-positive value. - or μ2 ≤ 0 and `c ≤ - μ2 ^ 2 / (4...

The Higgs potential is zero iff and only if the higgs field is zero, or the higgs field has norm-squared P.μ2 / P.𝓵, assuming P.𝓁 = 0.

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

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. -/ noncomputable def quarticTermReduced (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3)) : ℝ := P.η (Sum.inl 0) (Sum.inl 0) + 2 * ∑ b, k b * P.η (Sum.inl 0) (Sum.inr b) + ∑ a, ∑ b, k a *...

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.