Physlib.Particles.StandardModel.HiggsBoson.Potential

Imports

/-
Copyright (c) 2024 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.StandardModel.HiggsBoson.Basic
public import Mathlib.RingTheory.MvPolynomial.Homogeneous

The potential of the Higgs field

We define the potential of the Higgs field.

We show that the potential is a smooth function on spacetime.

@[expose] public section

The Higgs potential

The structure Potential is defined with two fields, μ2 corresponding to the mass-squared of the Higgs boson, and l corresponding to the coefficient of the quartic term in the Higgs potential. Note that l is usually denoted λ.

The mass-squared of the Higgs boson.

The quartic coupling of the Higgs boson. Usually denoted λ.

              structure Potential where  μ2 : ℝ  𝓵 : ℝ

TODO "Define a CoeFun instance for the Higgs Potential (or similar), instead of relying on
  `P.toFun`."

Given a element P of Potential, P.toFun is Higgs potential. It is defined for a Higgs field φ and a spacetime point x as

-μ² ‖φ‖_H^2 x + l * ‖φ‖_H^2 x * ‖φ‖_H^2 x.

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

The potential is smooth.

lemma toFun_smooth (φ : HiggsField) :
    ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) ⊤ (fun x => P.toFun φ x) := byP:Potentialφ:HiggsField⊢ ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) ⊤ fun x => P.toFun φ x
  simp only [toFun, normSq, neg_mul]P:Potentialφ:HiggsField⊢ ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) ⊤ fun x => -(P.μ2 * ‖φ x‖ ^ 2) + P.𝓵 * ‖φ x‖ ^ 2 * ‖φ x‖ ^ 2
  exact ((contMDiff_const (I' := 𝓘(ℝ, ℝ)) (M' := ℝ)).smul φ.normSq_smooth).neg.add
    (((contMDiff_const (I' := 𝓘(ℝ, ℝ)) (M' := ℝ)).smul φ.normSq_smooth).smul φ.normSq_smooth)All goals completed! 🐙

The Higgs potential formed by negating the mass squared and the quartic coupling.

def neg : Potential where
  μ2 := - P.μ2
  𝓵 := - P.𝓵

              @[simp]
lemma toFun_neg (φ : HiggsField) (x : SpaceTime) : P.neg.toFun φ x = - P.toFun φ x := byP:Potentialφ:HiggsFieldx:SpaceTime⊢ P.neg.toFun φ x = -P.toFun φ x
  simp only [toFun, neg]P:Potentialφ:HiggsFieldx:SpaceTime⊢ - -P.μ2 * ‖φ‖_H^2 x + -P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x = -(-P.μ2 * ‖φ‖_H^2 x + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x)
  ringAll goals completed! 🐙@[simp]
lemma μ2_neg : P.neg.μ2 = - P.μ2 := byP:Potential⊢ P.neg.μ2 = -P.μ2 rflAll goals completed! 🐙@[simp]
lemma 𝓵_neg : P.neg.𝓵 = - P.𝓵 := byP:Potential⊢ P.neg.𝓵 = -P.𝓵 rflAll goals completed! 🐙

Basic properties

@[simp]
lemma toFun_zero (x : SpaceTime) : P.toFun 0 x = 0 := byP:Potentialx:SpaceTime⊢ P.toFun 0 x = 0
  simp [toFun]All goals completed! 🐙

lemma complete_square (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :
    P.toFun φ x = P.𝓵 * (‖φ‖_H^2 x - P.μ2 / (2 * P.𝓵)) ^ 2 - P.μ2 ^ 2 / (4 * P.𝓵) := byP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = P.𝓵 * (‖φ‖_H^2 x - P.μ2 / (2 * P.𝓵)) ^ 2 - P.μ2 ^ 2 / (4 * P.𝓵)
  simp only [toFun]P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ -P.μ2 * ‖φ‖_H^2 x + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x = P.𝓵 * (‖φ‖_H^2 x - P.μ2 / (2 * P.𝓵)) ^ 2 - P.μ2 ^ 2 / (4 * P.𝓵)
  field_simpP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ ‖φ‖_H^2 x * P.𝓵 * (-P.μ2 + ‖φ‖_H^2 x * P.𝓵) * 2 ^ 2 * 4 = (‖φ‖_H^2 x * P.𝓵 * 2 - P.μ2) ^ 2 * 4 - P.μ2 ^ 2 * 2 ^ 2
  ringAll goals completed! 🐙

The quadratic equation satisfied by the Higgs potential at a spacetime point x.

lemma as_quad (φ : HiggsField) (x : SpaceTime) :
    P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + (- P.μ2) * ‖φ‖_H^2 x + (- P.toFun φ x) = 0 := byP:Potentialφ:HiggsFieldx:SpaceTime⊢ P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -P.toFun φ x = 0
  simp only [toFun]P:Potentialφ:HiggsFieldx:SpaceTime⊢ P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -(-P.μ2 * ‖φ‖_H^2 x + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x) = 0
  ringAll goals completed! 🐙

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.


lemma toFun_eq_zero_iff (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :
    P.toFun φ x = 0 ↔ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵 := byP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = 0 ↔ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵
  refine Iff.intro (fun hV => ?_) (fun hD => ?_)refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵refine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehD:φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵⊢ P.toFun φ x = 0
  ·refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵 have h1 := P.as_quad φ xrefine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -P.toFun φ x = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵
    rw [hVrefine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵] at h1refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵
    have h2 : ‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + - P.μ2) = 0 := byP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = 0 ↔ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0h2:‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + -P.μ2) = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵 linear_combination h1refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0h2:‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + -P.μ2) = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0h2:‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + -P.μ2) = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵
    rcases mul_eq_zero.mp h2 with h2 | h2refine_1.inlP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0h2✝:‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + -P.μ2) = 0h2:‖φ‖_H^2 x = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵refine_1.inrP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0h2✝:‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + -P.μ2) = 0h2:P.𝓵 * ‖φ‖_H^2 x + -P.μ2 = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵
    ·refine_1.inlP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0h2✝:‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + -P.μ2) = 0h2:‖φ‖_H^2 x = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵 exact Or.inl (byP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0h2✝:‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + -P.μ2) = 0h2:‖φ‖_H^2 x = 0⊢ φ x = 0 simpa [normSq] using h2All goals completed! 🐙)
    ·refine_1.inrP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0h2✝:‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + -P.μ2) = 0h2:P.𝓵 * ‖φ‖_H^2 x + -P.μ2 = 0⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵 exact Or.inr (byP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0h2✝:‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + -P.μ2) = 0h2:P.𝓵 * ‖φ‖_H^2 x + -P.μ2 = 0⊢ ‖φ‖_H^2 x = P.μ2 / P.𝓵 rw [eq_div_iff hP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0h2✝:‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + -P.μ2) = 0h2:P.𝓵 * ‖φ‖_H^2 x + -P.μ2 = 0⊢ ‖φ‖_H^2 x * P.𝓵 = P.μ2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0h2✝:‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + -P.μ2) = 0h2:P.𝓵 * ‖φ‖_H^2 x + -P.μ2 = 0⊢ ‖φ‖_H^2 x * P.𝓵 = P.μ2]P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = 0h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -0 = 0h2✝:‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + -P.μ2) = 0h2:P.𝓵 * ‖φ‖_H^2 x + -P.μ2 = 0⊢ ‖φ‖_H^2 x * P.𝓵 = P.μ2; linear_combination h2All goals completed! 🐙)
  ·refine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehD:φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵⊢ P.toFun φ x = 0 cases' hD with hD hDrefine_2.inlP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehD:φ x = 0⊢ P.toFun φ x = 0refine_2.inrP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehD:‖φ‖_H^2 x = P.μ2 / P.𝓵⊢ P.toFun φ x = 0
    ·refine_2.inlP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehD:φ x = 0⊢ P.toFun φ x = 0 simp [toFun, hD]All goals completed! 🐙
    ·refine_2.inrP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehD:‖φ‖_H^2 x = P.μ2 / P.𝓵⊢ P.toFun φ x = 0 simp only [toFun, hD]refine_2.inrP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehD:‖φ‖_H^2 x = P.μ2 / P.𝓵⊢ -P.μ2 * (P.μ2 / P.𝓵) + P.𝓵 * (P.μ2 / P.𝓵) * (P.μ2 / P.𝓵) = 0
      field_simprefine_2.inrP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehD:‖φ‖_H^2 x = P.μ2 / P.𝓵⊢ P.μ2 ^ 2 * (-1 + 1) = P.𝓵 * 0
      ringAll goals completed! 🐙

The discriminant

The discriminant of the quadratic equation formed by the Higgs potential.

def quadDiscrim (φ : HiggsField) (x : SpaceTime) : ℝ := discrim P.𝓵 (- P.μ2) (- P.toFun φ x)

The discriminant of the quadratic formed by the potential is non-negative.


lemma quadDiscrim_nonneg (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :
    0 ≤ P.quadDiscrim φ x := byP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ 0 ≤ P.quadDiscrim φ x
  have h1 := P.as_quad φ xP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -P.toFun φ x = 0⊢ 0 ≤ P.quadDiscrim φ x
  rw [mul_assoc,P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:P.𝓵 * (‖φ‖_H^2 x * ‖φ‖_H^2 x) + -P.μ2 * ‖φ‖_H^2 x + -P.toFun φ x = 0⊢ 0 ≤ P.quadDiscrim φ xP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:discrim P.𝓵 (-P.μ2) (-P.toFun φ x) = (2 * P.𝓵 * ‖φ‖_H^2 x + -P.μ2) ^ 2⊢ 0 ≤ P.quadDiscrim φ xhaP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:P.𝓵 * (‖φ‖_H^2 x * ‖φ‖_H^2 x) + -P.μ2 * ‖φ‖_H^2 x + -P.toFun φ x = 0⊢ P.𝓵 ≠ 0 quadratic_eq_zero_iff_discrim_eq_sqP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:discrim P.𝓵 (-P.μ2) (-P.toFun φ x) = (2 * P.𝓵 * ‖φ‖_H^2 x + -P.μ2) ^ 2⊢ 0 ≤ P.quadDiscrim φ xhaP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:P.𝓵 * (‖φ‖_H^2 x * ‖φ‖_H^2 x) + -P.μ2 * ‖φ‖_H^2 x + -P.toFun φ x = 0⊢ P.𝓵 ≠ 0P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:discrim P.𝓵 (-P.μ2) (-P.toFun φ x) = (2 * P.𝓵 * ‖φ‖_H^2 x + -P.μ2) ^ 2⊢ 0 ≤ P.quadDiscrim φ xhaP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:P.𝓵 * (‖φ‖_H^2 x * ‖φ‖_H^2 x) + -P.μ2 * ‖φ‖_H^2 x + -P.toFun φ x = 0⊢ P.𝓵 ≠ 0] at h1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:discrim P.𝓵 (-P.μ2) (-P.toFun φ x) = (2 * P.𝓵 * ‖φ‖_H^2 x + -P.μ2) ^ 2⊢ 0 ≤ P.quadDiscrim φ xhaP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:P.𝓵 * (‖φ‖_H^2 x * ‖φ‖_H^2 x) + -P.μ2 * ‖φ‖_H^2 x + -P.toFun φ x = 0⊢ P.𝓵 ≠ 0
  ·P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:discrim P.𝓵 (-P.μ2) (-P.toFun φ x) = (2 * P.𝓵 * ‖φ‖_H^2 x + -P.μ2) ^ 2⊢ 0 ≤ P.quadDiscrim φ x simp only [quadDiscrim, h1]P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:discrim P.𝓵 (-P.μ2) (-P.toFun φ x) = (2 * P.𝓵 * ‖φ‖_H^2 x + -P.μ2) ^ 2⊢ 0 ≤ (2 * P.𝓵 * ‖φ‖_H^2 x + -P.μ2) ^ 2
    exact sq_nonneg (2 * P.𝓵 * ‖φ‖_H^2 x + - P.μ2)All goals completed! 🐙
  ·haP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimeh1:P.𝓵 * (‖φ‖_H^2 x * ‖φ‖_H^2 x) + -P.μ2 * ‖φ‖_H^2 x + -P.toFun φ x = 0⊢ P.𝓵 ≠ 0 exact hAll goals completed! 🐙

              lemma quadDiscrim_eq_sqrt_mul_sqrt (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :
    P.quadDiscrim φ x = Real.sqrt (P.quadDiscrim φ x) * Real.sqrt (P.quadDiscrim φ x) :=
  (Real.mul_self_sqrt (P.quadDiscrim_nonneg h φ x)).symm

lemma quadDiscrim_eq_zero_iff (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :
    P.quadDiscrim φ x = 0 ↔ P.toFun φ x = - P.μ2 ^ 2 / (4 * P.𝓵) := byP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ P.quadDiscrim φ x = 0 ↔ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)
  rw [quadDiscrim,P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ discrim P.𝓵 (-P.μ2) (-P.toFun φ x) = 0 ↔ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ (-P.μ2) ^ 2 - 4 * P.𝓵 * -P.toFun φ x = 0 ↔ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵) discrimP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ (-P.μ2) ^ 2 - 4 * P.𝓵 * -P.toFun φ x = 0 ↔ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ (-P.μ2) ^ 2 - 4 * P.𝓵 * -P.toFun φ x = 0 ↔ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)]P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ (-P.μ2) ^ 2 - 4 * P.𝓵 * -P.toFun φ x = 0 ↔ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)
  refine Iff.intro (fun hD => ?_) (fun hV => ?_)refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehD:(-P.μ2) ^ 2 - 4 * P.𝓵 * -P.toFun φ x = 0⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)refine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ (-P.μ2) ^ 2 - 4 * P.𝓵 * -P.toFun φ x = 0
  ·refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehD:(-P.μ2) ^ 2 - 4 * P.𝓵 * -P.toFun φ x = 0⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵) field_simprefine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehD:(-P.μ2) ^ 2 - 4 * P.𝓵 * -P.toFun φ x = 0⊢ P.toFun φ x * 4 * P.𝓵 = -P.μ2 ^ 2
    linear_combination hDAll goals completed! 🐙
  ·refine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ (-P.μ2) ^ 2 - 4 * P.𝓵 * -P.toFun φ x = 0 rw [hVrefine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ (-P.μ2) ^ 2 - 4 * P.𝓵 * -(-P.μ2 ^ 2 / (4 * P.𝓵)) = 0refine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ (-P.μ2) ^ 2 - 4 * P.𝓵 * -(-P.μ2 ^ 2 / (4 * P.𝓵)) = 0]refine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ (-P.μ2) ^ 2 - 4 * P.𝓵 * -(-P.μ2 ^ 2 / (4 * P.𝓵)) = 0
    field_simprefine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ P.μ2 ^ 2 * (1 - 1) = 0
    ringAll goals completed! 🐙

lemma quadDiscrim_eq_zero_iff_normSq (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :
    P.quadDiscrim φ x = 0 ↔ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) := byP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ P.quadDiscrim φ x = 0 ↔ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)
  rw [P.quadDiscrim_eq_zero_iff hP:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵) ↔ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵) ↔ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)]P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵) ↔ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)
  refine Iff.intro (fun hV => ?_) (fun hF => ?_)refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)refine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehF:‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)
  ·refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) have h1 := P.as_quad φ xrefine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)h1:P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x + -P.μ2 * ‖φ‖_H^2 x + -P.toFun φ x = 0⊢ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)
    rw [mul_assoc,refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)h1:P.𝓵 * (‖φ‖_H^2 x * ‖φ‖_H^2 x) + -P.μ2 * ‖φ‖_H^2 x + -P.toFun φ x = 0⊢ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)h1:‖φ‖_H^2 x = - -P.μ2 / (2 * P.𝓵)⊢ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) quadratic_eq_zero_iff_of_discrim_eq_zero h
      ((P.quadDiscrim_eq_zero_iff h φ x).mpr hV)refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)h1:‖φ‖_H^2 x = - -P.μ2 / (2 * P.𝓵)⊢ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)h1:‖φ‖_H^2 x = - -P.μ2 / (2 * P.𝓵)⊢ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)] at h1refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)h1:‖φ‖_H^2 x = - -P.μ2 / (2 * P.𝓵)⊢ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)
    simp_rw [refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)h1:‖φ‖_H^2 x = - -P.μ2 / (2 * P.𝓵)⊢ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)h1,refine_1P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehV:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)h1:‖φ‖_H^2 x = - -P.μ2 / (2 * P.𝓵)⊢ - -P.μ2 / (2 * P.𝓵) = P.μ2 / (2 * P.𝓵) neg_negAll goals completed! 🐙]
  ·refine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehF:‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵) rw [toFun,refine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehF:‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)⊢ -P.μ2 * ‖φ‖_H^2 x + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x = -P.μ2 ^ 2 / (4 * P.𝓵)refine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehF:‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)⊢ -P.μ2 * (P.μ2 / (2 * P.𝓵)) + P.𝓵 * (P.μ2 / (2 * P.𝓵)) * (P.μ2 / (2 * P.𝓵)) = -P.μ2 ^ 2 / (4 * P.𝓵) hFrefine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehF:‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)⊢ -P.μ2 * (P.μ2 / (2 * P.𝓵)) + P.𝓵 * (P.μ2 / (2 * P.𝓵)) * (P.μ2 / (2 * P.𝓵)) = -P.μ2 ^ 2 / (4 * P.𝓵)refine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehF:‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)⊢ -P.μ2 * (P.μ2 / (2 * P.𝓵)) + P.𝓵 * (P.μ2 / (2 * P.𝓵)) * (P.μ2 / (2 * P.𝓵)) = -P.μ2 ^ 2 / (4 * P.𝓵)]refine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehF:‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)⊢ -P.μ2 * (P.μ2 / (2 * P.𝓵)) + P.𝓵 * (P.μ2 / (2 * P.𝓵)) * (P.μ2 / (2 * P.𝓵)) = -P.μ2 ^ 2 / (4 * P.𝓵)
    field_simprefine_2P:Potentialh:P.𝓵 ≠ 0φ:HiggsFieldx:SpaceTimehF:‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)⊢ P.μ2 ^ 2 * (-2 + 1) * 4 = -(P.μ2 ^ 2 * 2 ^ 2)
    ringAll goals completed! 🐙

For an element P of Potential, if l < 0 then the following upper bound for the potential exists

P.toFun φ x ≤ - μ2 ^ 2 / (4 * 𝓵).


lemma neg_𝓵_quadDiscrim_zero_bound (h : P.𝓵 < 0) (φ : HiggsField) (x : SpaceTime) :
    P.toFun φ x ≤ - P.μ2 ^ 2 / (4 * P.𝓵) := byP:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)
  have h1 := P.quadDiscrim_nonneg (ne_of_lt h) φ xP:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTimeh1:0 ≤ P.quadDiscrim φ x⊢ P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)
  simp only [quadDiscrim, discrim, even_two, Even.neg_pow] at h1P:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTimeh1:0 ≤ P.μ2 ^ 2 - 4 * P.𝓵 * -P.toFun φ x⊢ P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)
  rw [le_div_iff_of_neg (show (4:ℝ) * P.𝓵 < 0 byP:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)P:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTimeh1:0 ≤ P.μ2 ^ 2 - 4 * P.𝓵 * -P.toFun φ x⊢ -P.μ2 ^ 2 ≤ P.toFun φ x * (4 * P.𝓵) linarithAll goals completed! 🐙P:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTimeh1:0 ≤ P.μ2 ^ 2 - 4 * P.𝓵 * -P.toFun φ x⊢ -P.μ2 ^ 2 ≤ P.toFun φ x * (4 * P.𝓵))]P:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTimeh1:0 ≤ P.μ2 ^ 2 - 4 * P.𝓵 * -P.toFun φ x⊢ -P.μ2 ^ 2 ≤ P.toFun φ x * (4 * P.𝓵)
  nlinarith [h1]All goals completed! 🐙

For an element P of Potential, if 0 < l then the following lower bound for the potential exists

- μ2 ^ 2 / (4 * 𝓵) ≤ P.toFun φ x.


lemma pos_𝓵_quadDiscrim_zero_bound (h : 0 < P.𝓵) (φ : HiggsField) (x : SpaceTime) :
    - P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x := byP:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTime⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x
  have h1 := P.neg.neg_𝓵_quadDiscrim_zero_bound (byP:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTime⊢ P.neg.𝓵 < 0P:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTimeh1:P.neg.toFun φ x ≤ -P.neg.μ2 ^ 2 / (4 * P.neg.𝓵)⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x simpa [neg] using hAll goals completed! 🐙P:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTimeh1:P.neg.toFun φ x ≤ -P.neg.μ2 ^ 2 / (4 * P.neg.𝓵)⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x) φ xP:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTimeh1:P.neg.toFun φ x ≤ -P.neg.μ2 ^ 2 / (4 * P.neg.𝓵)⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x
  simp only [toFun_neg, μ2_neg, even_two, Even.neg_pow, 𝓵_neg, mul_neg, neg_div_neg_eq] at h1P:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTimeh1:-P.toFun φ x ≤ P.μ2 ^ 2 / (4 * P.𝓵)⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x
  rw [neg_le,P:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTimeh1:-(P.μ2 ^ 2 / (4 * P.𝓵)) ≤ P.toFun φ x⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ xP:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTimeh1:-P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x neg_div'P:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTimeh1:-P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ xP:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTimeh1:-P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x] at h1P:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTimeh1:-P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x
  exact h1All goals completed! 🐙

If P.𝓵 is negative, then if P.μ2 is greater than zero, for all space-time points, the potential is negative P.toFun φ x ≤ 0.

lemma neg_𝓵_toFun_neg (h : P.𝓵 < 0) (φ : HiggsField) (x : SpaceTime) :
    (0 < P.μ2 ∧ P.toFun φ x ≤ 0) ∨ P.μ2 ≤ 0 := byP:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTime⊢ 0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0
  by_cases hμ2 : P.μ2 ≤ 0posP:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTimehμ2:P.μ2 ≤ 0⊢ 0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0negP:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTimehμ2:¬P.μ2 ≤ 0⊢ 0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0
  ·posP:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTimehμ2:P.μ2 ≤ 0⊢ 0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0 simp [hμ2]All goals completed! 🐙
  refine Or.inl ⟨lt_of_not_ge hμ2, ?_⟩negP:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTimehμ2:¬P.μ2 ≤ 0⊢ P.toFun φ x ≤ 0
  simp only [toFun, normSq, neg_mul]negP:Potentialh:P.𝓵 < 0φ:HiggsFieldx:SpaceTimehμ2:¬P.μ2 ≤ 0⊢ -(P.μ2 * ‖φ x‖ ^ 2) + P.𝓵 * ‖φ x‖ ^ 2 * ‖φ x‖ ^ 2 ≤ 0
  nlinarith [mul_nonneg (sq_nonneg ‖φ x‖) (sq_nonneg ‖φ x‖), sq_nonneg ‖φ x‖,
    h, lt_of_not_ge hμ2]All goals completed! 🐙

If P.𝓵 is bigger then zero, then if P.μ2 is less than zero, for all space-time points, the potential is positive 0 ≤ P.toFun φ x.

lemma pos_𝓵_toFun_pos (h : 0 < P.𝓵) (φ : HiggsField) (x : SpaceTime) :
    (P.μ2 < 0 ∧ 0 ≤ P.toFun φ x) ∨ 0 ≤ P.μ2 := byP:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTime⊢ P.μ2 < 0 ∧ 0 ≤ P.toFun φ x ∨ 0 ≤ P.μ2
  simpa using P.neg.neg_𝓵_toFun_neg (byP:Potentialh:0 < P.𝓵φ:HiggsFieldx:SpaceTime⊢ P.neg.𝓵 < 0 simpa using hAll goals completed! 🐙) φ x

For an element P of Potential with l < 0 and a real c : ℝ, there exists a Higgs field φ and a spacetime point x such that P.toFun φ x = c iff one of the following two conditions hold:

0 < μ2 and c ≤ 0. That is, if l is negative and μ2 positive, then the potential takes every non-positive value.

or μ2 ≤ 0 and c ≤ - μ2 ^ 2 / (4 * 𝓵). That is, if l is negative and μ2 non-positive, then the potential takes every value less then or equal to its bound.


lemma neg_𝓵_sol_exists_iff (h𝓵 : P.𝓵 < 0) (c : ℝ) : (∃ φ x, P.toFun φ x = c) ↔ (0 < P.μ2 ∧ c ≤ 0) ∨
    (P.μ2 ≤ 0 ∧ c ≤ - P.μ2 ^ 2 / (4 * P.𝓵)) := byP:Potentialh𝓵:P.𝓵 < 0c:ℝ⊢ (∃ φ x, P.toFun φ x = c) ↔ 0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)
  refine Iff.intro (fun ⟨φ, x, hV⟩ => ?_) (fun h => ?_)refine_1P:Potentialh𝓵:P.𝓵 < 0c:ℝx✝:∃ φ x, P.toFun φ x = cφ:HiggsFieldx:SpaceTimehV:P.toFun φ x = c⊢ 0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ ∃ φ x, P.toFun φ x = c
  ·refine_1P:Potentialh𝓵:P.𝓵 < 0c:ℝx✝:∃ φ x, P.toFun φ x = cφ:HiggsFieldx:SpaceTimehV:P.toFun φ x = c⊢ 0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵) rw [← hVrefine_1P:Potentialh𝓵:P.𝓵 < 0c:ℝx✝:∃ φ x, P.toFun φ x = cφ:HiggsFieldx:SpaceTimehV:P.toFun φ x = c⊢ 0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0 ∧ P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)refine_1P:Potentialh𝓵:P.𝓵 < 0c:ℝx✝:∃ φ x, P.toFun φ x = cφ:HiggsFieldx:SpaceTimehV:P.toFun φ x = c⊢ 0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0 ∧ P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)]refine_1P:Potentialh𝓵:P.𝓵 < 0c:ℝx✝:∃ φ x, P.toFun φ x = cφ:HiggsFieldx:SpaceTimehV:P.toFun φ x = c⊢ 0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0 ∧ P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)
    rcases P.neg_𝓵_toFun_neg h𝓵 φ x with hr | hrrefine_1.inlP:Potentialh𝓵:P.𝓵 < 0c:ℝx✝:∃ φ x, P.toFun φ x = cφ:HiggsFieldx:SpaceTimehV:P.toFun φ x = chr:0 < P.μ2 ∧ P.toFun φ x ≤ 0⊢ 0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0 ∧ P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)refine_1.inrP:Potentialh𝓵:P.𝓵 < 0c:ℝx✝:∃ φ x, P.toFun φ x = cφ:HiggsFieldx:SpaceTimehV:P.toFun φ x = chr:P.μ2 ≤ 0⊢ 0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0 ∧ P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)
    ·refine_1.inlP:Potentialh𝓵:P.𝓵 < 0c:ℝx✝:∃ φ x, P.toFun φ x = cφ:HiggsFieldx:SpaceTimehV:P.toFun φ x = chr:0 < P.μ2 ∧ P.toFun φ x ≤ 0⊢ 0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0 ∧ P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵) exact Or.inl hrAll goals completed! 🐙
    ·refine_1.inrP:Potentialh𝓵:P.𝓵 < 0c:ℝx✝:∃ φ x, P.toFun φ x = cφ:HiggsFieldx:SpaceTimehV:P.toFun φ x = chr:P.μ2 ≤ 0⊢ 0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0 ∧ P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵) exact Or.inr ⟨hr, P.neg_𝓵_quadDiscrim_zero_bound h𝓵 φ x⟩All goals completed! 🐙
  ·refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ ∃ φ x, P.toFun φ x = c simp only [toFun, neg_mul]refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x = c
    simp only [← sub_eq_zero, sub_zero]refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0
    let a := (P.μ2 - Real.sqrt (discrim P.𝓵 (- P.μ2) (- c))) / (2 * P.𝓵)refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0
    have ha : 0 ≤ a := byP:Potentialh𝓵:P.𝓵 < 0c:ℝ⊢ (∃ φ x, P.toFun φ x = c) ↔ 0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0
      simp only [discrim, even_two, Even.neg_pow, mul_neg, sub_neg_eq_add, a]P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)⊢ 0 ≤ (P.μ2 - √(P.μ2 ^ 2 + 4 * P.𝓵 * c)) / (2 * P.𝓵)refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0
      rw [div_nonneg_iffP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)⊢ 0 ≤ P.μ2 - √(P.μ2 ^ 2 + 4 * P.𝓵 * c) ∧ 0 ≤ 2 * P.𝓵 ∨ P.μ2 - √(P.μ2 ^ 2 + 4 * P.𝓵 * c) ≤ 0 ∧ 2 * P.𝓵 ≤ 0P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)⊢ 0 ≤ P.μ2 - √(P.μ2 ^ 2 + 4 * P.𝓵 * c) ∧ 0 ≤ 2 * P.𝓵 ∨ P.μ2 - √(P.μ2 ^ 2 + 4 * P.𝓵 * c) ≤ 0 ∧ 2 * P.𝓵 ≤ 0refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0]P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)⊢ 0 ≤ P.μ2 - √(P.μ2 ^ 2 + 4 * P.𝓵 * c) ∧ 0 ≤ 2 * P.𝓵 ∨ P.μ2 - √(P.μ2 ^ 2 + 4 * P.𝓵 * c) ≤ 0 ∧ 2 * P.𝓵 ≤ 0refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0
      refine Or.inr ⟨?_, byP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)⊢ 2 * P.𝓵 ≤ 0refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0 linarithAll goals completed! 🐙refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0⟩
      rw [sub_nonposP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)⊢ P.μ2 ≤ √(P.μ2 ^ 2 + 4 * P.𝓵 * c)P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)⊢ P.μ2 ≤ √(P.μ2 ^ 2 + 4 * P.𝓵 * c)refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0]P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)⊢ P.μ2 ≤ √(P.μ2 ^ 2 + 4 * P.𝓵 * c)refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0
      rcases h with h | hinlP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)h:0 < P.μ2 ∧ c ≤ 0⊢ P.μ2 ≤ √(P.μ2 ^ 2 + 4 * P.𝓵 * c)inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)h:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ P.μ2 ≤ √(P.μ2 ^ 2 + 4 * P.𝓵 * c)refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0
      ·inlP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)h:0 < P.μ2 ∧ c ≤ 0⊢ P.μ2 ≤ √(P.μ2 ^ 2 + 4 * P.𝓵 * c)refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0 exact Real.le_sqrt_of_sq_le (byP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)h:0 < P.μ2 ∧ c ≤ 0⊢ P.μ2 ^ 2 ≤ P.μ2 ^ 2 + 4 * P.𝓵 * crefine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0 nlinarith [h.2]All goals completed! 🐙refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0)
      ·inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)h:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ P.μ2 ≤ √(P.μ2 ^ 2 + 4 * P.𝓵 * c)refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0 exact h.1.trans (Real.sqrt_nonneg _)refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0refine_2P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ φ x, -(P.μ2 * ‖φ‖_H^2 x) + P.𝓵 * ‖φ‖_H^2 x * ‖φ‖_H^2 x - c - 0 = 0
    use (const (HiggsVec.ofReal a))hP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ ∃ x,
  -(P.μ2 * ‖const (HiggsVec.ofReal a)‖_H^2 x) +
          P.𝓵 * ‖const (HiggsVec.ofReal a)‖_H^2 x * ‖const (HiggsVec.ofReal a)‖_H^2 x -
        c -
      0 =
    0
    use 0hP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ -(P.μ2 * ‖const (HiggsVec.ofReal a)‖_H^2 0) +
        P.𝓵 * ‖const (HiggsVec.ofReal a)‖_H^2 0 * ‖const (HiggsVec.ofReal a)‖_H^2 0 -
      c -
    0 =
  0
    simp [HiggsVec.ofReal_normSq ha]hP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ -(P.μ2 * a) + P.𝓵 * a * a - c = 0
    trans P.𝓵 * a * a + (- P.μ2) * a + (- c)P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ -(P.μ2 * a) + P.𝓵 * a * a - c = P.𝓵 * a * a + -P.μ2 * a + -cP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0
    ·P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ -(P.μ2 * a) + P.𝓵 * a * a - c = P.𝓵 * a * a + -P.μ2 * a + -c ringAll goals completed! 🐙
    have hd : 0 ≤ (discrim P.𝓵 (- P.μ2) (-c)) := byP:Potentialh𝓵:P.𝓵 < 0c:ℝ⊢ (∃ φ x, P.toFun φ x = c) ↔ 0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0
      simp only [discrim, even_two, Even.neg_pow, mul_neg, sub_neg_eq_add]P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ a⊢ 0 ≤ P.μ2 ^ 2 + 4 * P.𝓵 * cP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0
      rcases h with h | hinlP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:0 < P.μ2 ∧ c ≤ 0⊢ 0 ≤ P.μ2 ^ 2 + 4 * P.𝓵 * cinrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ 0 ≤ P.μ2 ^ 2 + 4 * P.𝓵 * cP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0
      ·inlP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:0 < P.μ2 ∧ c ≤ 0⊢ 0 ≤ P.μ2 ^ 2 + 4 * P.𝓵 * cP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0 nlinarith [sq_nonneg P.μ2, h.2]All goals completed! 🐙P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0
      ·inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ 0 ≤ P.μ2 ^ 2 + 4 * P.𝓵 * cP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0 rw [← @neg_le_iff_add_nonneg',inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ -P.μ2 ^ 2 ≤ 4 * P.𝓵 * cinrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ 4 * P.𝓵 < 0P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0 ← le_div_iff_of_neg'inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ 4 * P.𝓵 < 0inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ 4 * P.𝓵 < 0P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0]inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ 4 * P.𝓵 < 0P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0
        ·inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0 exact h.2All goals completed! 🐙P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0
        ·inrP:Potentialh𝓵:P.𝓵 < 0c:ℝa:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ah:P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ 4 * P.𝓵 < 0P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0 linarithP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0
    have hdd := (Real.mul_self_sqrt hd).symmP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)hdd:discrim P.𝓵 (-P.μ2) (-c) = √(discrim P.𝓵 (-P.μ2) (-c)) * √(discrim P.𝓵 (-P.μ2) (-c))⊢ P.𝓵 * a * a + -P.μ2 * a + -c = 0
    rw [mul_assocP:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)hdd:discrim P.𝓵 (-P.μ2) (-c) = √(discrim P.𝓵 (-P.μ2) (-c)) * √(discrim P.𝓵 (-P.μ2) (-c))⊢ P.𝓵 * (a * a) + -P.μ2 * a + -c = 0P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)hdd:discrim P.𝓵 (-P.μ2) (-c) = √(discrim P.𝓵 (-P.μ2) (-c)) * √(discrim P.𝓵 (-P.μ2) (-c))⊢ P.𝓵 * (a * a) + -P.μ2 * a + -c = 0]P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)hdd:discrim P.𝓵 (-P.μ2) (-c) = √(discrim P.𝓵 (-P.μ2) (-c)) * √(discrim P.𝓵 (-P.μ2) (-c))⊢ P.𝓵 * (a * a) + -P.μ2 * a + -c = 0
    refine (quadratic_eq_zero_iff (ne_of_gt h𝓵).symm hdd _).mpr ?_P:Potentialh𝓵:P.𝓵 < 0c:ℝh:0 < P.μ2 ∧ c ≤ 0 ∨ P.μ2 ≤ 0 ∧ c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)a:ℝ := (P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)ha:0 ≤ ahd:0 ≤ discrim P.𝓵 (-P.μ2) (-c)hdd:discrim P.𝓵 (-P.μ2) (-c) = √(discrim P.𝓵 (-P.μ2) (-c)) * √(discrim P.𝓵 (-P.μ2) (-c))⊢ a = (- -P.μ2 + √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵) ∨ a = (- -P.μ2 - √(discrim P.𝓵 (-P.μ2) (-c))) / (2 * P.𝓵)
    simp only [neg_neg, or_true, a]All goals completed! 🐙

For an element P of Potential with 0 < l and a real c : ℝ, there exists a Higgs field φ and a spacetime point x such that P.toFun φ x = c iff one of the following two conditions hold:

μ2 < 0 and 0 ≤ c. That is, if l is positive and μ2 negative, then the potential takes every non-negative value.

or 0 ≤ μ2 and - μ2 ^ 2 / (4 * 𝓵) ≤ c. That is, if l is positive and μ2 non-negative, then the potential takes every value greater then or equal to its bound.


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

Boundedness of the potential

Given a element P of Potential, the proposition IsBounded P is true if and only if there exists a real c such that for all Higgs fields φ and spacetime points x, the Higgs potential corresponding to φ at x is greater then or equal toc. I.e.

∀ Φ x, c ≤ P.toFun Φ x.

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

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


lemma isBounded_𝓵_nonneg (h : P.IsBounded) : 0 ≤ P.𝓵 := byP:Potentialh:P.IsBounded⊢ 0 ≤ P.𝓵
  by_contra hlP:Potentialh:P.IsBoundedhl:¬0 ≤ P.𝓵⊢ False
  rw [not_leP:Potentialh:P.IsBoundedhl:P.𝓵 < 0⊢ FalseP:Potentialh:P.IsBoundedhl:P.𝓵 < 0⊢ False] at hlP:Potentialh:P.IsBoundedhl:P.𝓵 < 0⊢ False
  obtain ⟨c, hc⟩ := hP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ x⊢ False
  have c_le_of_attainable : ∀ v : ℝ, ((0 < P.μ2 ∧ v ≤ 0) ∨
      (P.μ2 ≤ 0 ∧ v ≤ - P.μ2 ^ 2 / (4 * P.𝓵))) → c ≤ v := byP:Potentialh:P.IsBounded⊢ 0 ≤ P.𝓵P:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ v⊢ False
    intro v hvP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xv:ℝhv:0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ c ≤ vP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ v⊢ False
    obtain ⟨φ, x, rfl⟩ := (P.neg_𝓵_sol_exists_iff hl v).mpr hvP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xφ:HiggsFieldx:SpaceTimehv:0 < P.μ2 ∧ P.toFun φ x ≤ 0 ∨ P.μ2 ≤ 0 ∧ P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ c ≤ P.toFun φ xP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ v⊢ False
    exact hc φ xP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ v⊢ FalseP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ v⊢ False
  by_cases hμ : P.μ2 ≤ 0posP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:P.μ2 ≤ 0⊢ FalsenegP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:¬P.μ2 ≤ 0⊢ False
  ·posP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:P.μ2 ≤ 0⊢ False by_cases hcz : c ≤ - P.μ2 ^ 2 / (4 * P.𝓵)posP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:P.μ2 ≤ 0hcz:c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ FalsenegP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:P.μ2 ≤ 0hcz:¬c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ False
    ·posP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:P.μ2 ≤ 0hcz:c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ False linarith [c_le_of_attainable (c - 1) (Or.inr ⟨hμ, byP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:P.μ2 ≤ 0hcz:c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ c - 1 ≤ -P.μ2 ^ 2 / (4 * P.𝓵) linarithAll goals completed! 🐙⟩)]
    ·negP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:P.μ2 ≤ 0hcz:¬c ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ False rw [not_lenegP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:P.μ2 ≤ 0hcz:-P.μ2 ^ 2 / (4 * P.𝓵) < c⊢ FalsenegP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:P.μ2 ≤ 0hcz:-P.μ2 ^ 2 / (4 * P.𝓵) < c⊢ False] at hcznegP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:P.μ2 ≤ 0hcz:-P.μ2 ^ 2 / (4 * P.𝓵) < c⊢ False
      linarith [c_le_of_attainable (- P.μ2 ^ 2 / (4 * P.𝓵) - 1) (Or.inr ⟨hμ, byP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:P.μ2 ≤ 0hcz:-P.μ2 ^ 2 / (4 * P.𝓵) < c⊢ -P.μ2 ^ 2 / (4 * P.𝓵) - 1 ≤ -P.μ2 ^ 2 / (4 * P.𝓵) linarithAll goals completed! 🐙⟩)]
  ·negP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:¬P.μ2 ≤ 0⊢ False rw [not_lenegP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:0 < P.μ2⊢ FalsenegP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:0 < P.μ2⊢ False] at hμnegP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:0 < P.μ2⊢ False
    by_cases hcz : c ≤ 0posP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:0 < P.μ2hcz:c ≤ 0⊢ FalsenegP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:0 < P.μ2hcz:¬c ≤ 0⊢ False
    ·posP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:0 < P.μ2hcz:c ≤ 0⊢ False linarith [c_le_of_attainable (c - 1) (Or.inl ⟨hμ, byP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:0 < P.μ2hcz:c ≤ 0⊢ c - 1 ≤ 0 linarithAll goals completed! 🐙⟩)]
    ·negP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:0 < P.μ2hcz:¬c ≤ 0⊢ False rw [not_lenegP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:0 < P.μ2hcz:0 < c⊢ FalsenegP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:0 < P.μ2hcz:0 < c⊢ False] at hcznegP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:0 < P.μ2hcz:0 < c⊢ False
      linarith [c_le_of_attainable 0 (Or.inl ⟨hμ, byP:Potentialhl:P.𝓵 < 0c:ℝhc:∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ xc_le_of_attainable:∀ (v : ℝ), 0 < P.μ2 ∧ v ≤ 0 ∨ P.μ2 ≤ 0 ∧ v ≤ -P.μ2 ^ 2 / (4 * P.𝓵) → c ≤ vhμ:0 < P.μ2hcz:0 < c⊢ 0 ≤ 0 linarithAll goals completed! 🐙⟩)]

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

lemma isBounded_of_𝓵_pos (h : 0 < P.𝓵) : P.IsBounded := byP:Potentialh:0 < P.𝓵⊢ P.IsBounded
  simp only [IsBounded]P:Potentialh:0 < P.𝓵⊢ ∃ c, ∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ x
  have h2 := P.pos_𝓵_quadDiscrim_zero_bound hP:Potentialh:0 < P.𝓵h2:∀ (φ : HiggsField) (x : SpaceTime), -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x⊢ ∃ c, ∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ x
  by_contra hnP:Potentialh:0 < P.𝓵h2:∀ (φ : HiggsField) (x : SpaceTime), -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ xhn:¬∃ c, ∀ (Φ : HiggsField) (x : SpaceTime), c ≤ P.toFun Φ x⊢ False
  simp only [not_exists, not_forall, not_le] at hnP:Potentialh:0 < P.𝓵h2:∀ (φ : HiggsField) (x : SpaceTime), -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ xhn:∀ (x : ℝ), ∃ x_1 x_2, P.toFun x_1 x_2 < x⊢ False
  obtain ⟨φ, x, hx⟩ := hn (-P.μ2 ^ 2 / (4 * P.𝓵))P:Potentialh:0 < P.𝓵h2:∀ (φ : HiggsField) (x : SpaceTime), -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ xhn:∀ (x : ℝ), ∃ x_1 x_2, P.toFun x_1 x_2 < xφ:HiggsFieldx:SpaceTimehx:P.toFun φ x < -P.μ2 ^ 2 / (4 * P.𝓵)⊢ False
  have h2' := h2 φ xP:Potentialh:0 < P.𝓵h2:∀ (φ : HiggsField) (x : SpaceTime), -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ xhn:∀ (x : ℝ), ∃ x_1 x_2, P.toFun x_1 x_2 < xφ:HiggsFieldx:SpaceTimehx:P.toFun φ x < -P.μ2 ^ 2 / (4 * P.𝓵)h2':-P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x⊢ False
  linarithAll goals completed! 🐙

When there is no quartic coupling, the potential is bounded iff the mass squared is non-positive, i.e., for P : Potential then P.IsBounded iff P.μ2 ≤ 0. That is to say - P.μ2 * ‖φ‖_H^2 x is bounded below iff P.μ2 ≤ 0.

informal_lemma isBounded_iff_of_𝓵_zero where
  deps := [`StandardModel.HiggsField.Potential.IsBounded, `StandardModel.HiggsField.Potential]
  tag := "6V2K5"

Minimum and maximum

              

lemma eq_zero_iff_of_μSq_nonpos_𝓵_pos (h𝓵 : 0 < P.𝓵) (hμ2 : P.μ2 ≤ 0) (φ : HiggsField)
    (x : SpaceTime) : P.toFun φ x = 0 ↔ φ x = 0 := byP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = 0 ↔ φ x = 0
  rw [P.toFun_eq_zero_iff (ne_of_lt h𝓵).symmP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTime⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵 ↔ φ x = 0P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTime⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵 ↔ φ x = 0]P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTime⊢ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵 ↔ φ x = 0
  simp only [or_iff_left_iff_imp]P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTime⊢ ‖φ‖_H^2 x = P.μ2 / P.𝓵 → φ x = 0
  intro hP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh:‖φ‖_H^2 x = P.μ2 / P.𝓵⊢ φ x = 0
  have hx' : ‖φ‖_H^2 x = 0 :=
    le_antisymm (h.trans_le (div_nonpos_of_nonpos_of_nonneg hμ2 h𝓵.le)) (normSq_nonneg φ x)P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh:‖φ‖_H^2 x = P.μ2 / P.𝓵hx':‖φ‖_H^2 x = 0⊢ φ x = 0
  simpa using hx'All goals completed! 🐙

lemma isMinOn_iff_of_μSq_nonpos_𝓵_pos (h𝓵 : 0 < P.𝓵) (hμ2 : P.μ2 ≤ 0) (φ : HiggsField)
    (x : SpaceTime) : IsMinOn (fun (φ, x) => P.toFun φ x) Set.univ (φ, x)
    ↔ P.toFun φ x = 0 := byP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTime⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.toFun φ x = 0
  have h1 := P.pos_𝓵_sol_exists_iff h𝓵P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ c⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.toFun φ x = 0
  have attainable_nonneg : ∀ v : ℝ, ((P.μ2 < 0 ∧ 0 ≤ v) ∨
      (0 ≤ P.μ2 ∧ - P.μ2 ^ 2 / (4 * P.𝓵) ≤ v)) → 0 ≤ v := by
    rintro v (⟨_, hv⟩ | ⟨h0, hv⟩)inlP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cv:ℝleft✝:P.μ2 < 0hv:0 ≤ v⊢ 0 ≤ vinrP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cv:ℝh0:0 ≤ P.μ2hv:-P.μ2 ^ 2 / (4 * P.𝓵) ≤ v⊢ 0 ≤ vP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ v⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.toFun φ x = 0
    ·inlP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cv:ℝleft✝:P.μ2 < 0hv:0 ≤ v⊢ 0 ≤ vP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ v⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.toFun φ x = 0 exact hvAll goals completed! 🐙P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ v⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.toFun φ x = 0
    ·inrP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cv:ℝh0:0 ≤ P.μ2hv:-P.μ2 ^ 2 / (4 * P.𝓵) ≤ v⊢ 0 ≤ vP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ v⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.toFun φ x = 0 simpa [le_antisymm hμ2 h0] using hvP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ v⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.toFun φ x = 0P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ v⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.toFun φ x = 0
  rw [isMinOn_univ_iffP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ v⊢ (∀ (x_1 : HiggsField × SpaceTime),
    (match (φ, x) with
      | (φ, x) => P.toFun φ x) ≤
      match x_1 with
      | (φ, x) => P.toFun φ x) ↔
  P.toFun φ x = 0P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ v⊢ (∀ (x_1 : HiggsField × SpaceTime),
    (match (φ, x) with
      | (φ, x) => P.toFun φ x) ≤
      match x_1 with
      | (φ, x) => P.toFun φ x) ↔
  P.toFun φ x = 0]P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ v⊢ (∀ (x_1 : HiggsField × SpaceTime),
    (match (φ, x) with
      | (φ, x) => P.toFun φ x) ≤
      match x_1 with
      | (φ, x) => P.toFun φ x) ↔
  P.toFun φ x = 0
  simp only [Prod.forall]P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ v⊢ (∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a b) ↔ P.toFun φ x = 0
  refine Iff.intro (fun h => ?_) (fun h => ?_)refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ vh:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a b⊢ P.toFun φ x = 0refine_2P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ vh:P.toFun φ x = 0⊢ ∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a b
  ·refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ vh:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a b⊢ P.toFun φ x = 0 have h1' : P.toFun φ x ≤ 0 := byP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTime⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.toFun φ x = 0refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ vh:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a bh1':P.toFun φ x ≤ 0⊢ P.toFun φ x = 0 simpa using h 0 0refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ vh:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a bh1':P.toFun φ x ≤ 0⊢ P.toFun φ x = 0refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ vh:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a bh1':P.toFun φ x ≤ 0⊢ P.toFun φ x = 0
    have h1'' := attainable_nonneg _ ((h1 (P.toFun φ x)).mp ⟨φ, x, rfl⟩)refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ vh:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a bh1':P.toFun φ x ≤ 0h1'':0 ≤ P.toFun φ x⊢ P.toFun φ x = 0
    linarithAll goals completed! 🐙
  ·refine_2P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ vh:P.toFun φ x = 0⊢ ∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a b rw [hrefine_2P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ vh:P.toFun φ x = 0⊢ ∀ (a : HiggsField) (b : SpaceTime), 0 ≤ P.toFun a brefine_2P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ vh:P.toFun φ x = 0⊢ ∀ (a : HiggsField) (b : SpaceTime), 0 ≤ P.toFun a b]refine_2P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ cattainable_nonneg:∀ (v : ℝ), P.μ2 < 0 ∧ 0 ≤ v ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ v → 0 ≤ vh:P.toFun φ x = 0⊢ ∀ (a : HiggsField) (b : SpaceTime), 0 ≤ P.toFun a b
    exact fun φ' x' => attainable_nonneg _ ((h1 (P.toFun φ' x')).mp ⟨φ', x', rfl⟩)All goals completed! 🐙

lemma isMinOn_iff_field_of_μSq_nonpos_𝓵_pos (h𝓵 : 0 < P.𝓵) (hμ2 : P.μ2 ≤ 0) (φ : HiggsField)
    (x : SpaceTime) : IsMinOn (fun (φ, x) => P.toFun φ x) Set.univ (φ, x)
    ↔ φ x = 0 := byP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTime⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  φ x = 0
  rw [P.isMinOn_iff_of_μSq_nonpos_𝓵_pos h𝓵 hμ2 φ xP:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = 0 ↔ φ x = 0P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = 0 ↔ φ x = 0]P:Potentialh𝓵:0 < P.𝓵hμ2:P.μ2 ≤ 0φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = 0 ↔ φ x = 0
  exact P.eq_zero_iff_of_μSq_nonpos_𝓵_pos h𝓵 hμ2 φ xAll goals completed! 🐙

lemma isMinOn_iff_of_μSq_nonneg_𝓵_pos (h𝓵 : 0 < P.𝓵) (hμ2 : 0 ≤ P.μ2) (φ : HiggsField)
    (x : SpaceTime) : IsMinOn (fun (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔
    P.toFun φ x = - P.μ2 ^ 2 / (4 * P.𝓵) := byP:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTime⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)
  have h1 := P.pos_𝓵_sol_exists_iff h𝓵P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ P.μ2 < 0 ∧ 0 ≤ c ∨ 0 ≤ P.μ2 ∧ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ c⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)
  simp only [not_lt.mpr hμ2, false_and, hμ2, true_and, false_or] at h1P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ c⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)
  rw [isMinOn_univ_iffP:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ c⊢ (∀ (x_1 : HiggsField × SpaceTime),
    (match (φ, x) with
      | (φ, x) => P.toFun φ x) ≤
      match x_1 with
      | (φ, x) => P.toFun φ x) ↔
  P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ c⊢ (∀ (x_1 : HiggsField × SpaceTime),
    (match (φ, x) with
      | (φ, x) => P.toFun φ x) ≤
      match x_1 with
      | (φ, x) => P.toFun φ x) ↔
  P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)]P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ c⊢ (∀ (x_1 : HiggsField × SpaceTime),
    (match (φ, x) with
      | (φ, x) => P.toFun φ x) ≤
      match x_1 with
      | (φ, x) => P.toFun φ x) ↔
  P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)
  simp only [Prod.forall]P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ c⊢ (∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a b) ↔ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)
  refine Iff.intro (fun h => ?_) (fun h => ?_)refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a b⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)refine_2P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ ∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a b
  ·refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a b⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵) obtain ⟨φ', x', hφ'⟩ := (h1 (- P.μ2 ^ 2 / (4 * P.𝓵))).mpr (byP:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a b⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ -P.μ2 ^ 2 / (4 * P.𝓵)refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a bφ':HiggsFieldx':SpaceTimehφ':P.toFun φ' x' = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵) rflAll goals completed! 🐙refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a bφ':HiggsFieldx':SpaceTimehφ':P.toFun φ' x' = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵))refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a bφ':HiggsFieldx':SpaceTimehφ':P.toFun φ' x' = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)
    have h' := h φ' x'refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a bφ':HiggsFieldx':SpaceTimehφ':P.toFun φ' x' = -P.μ2 ^ 2 / (4 * P.𝓵)h':P.toFun φ x ≤ P.toFun φ' x'⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)
    rw [hφ'refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a bφ':HiggsFieldx':SpaceTimehφ':P.toFun φ' x' = -P.μ2 ^ 2 / (4 * P.𝓵)h':P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a bφ':HiggsFieldx':SpaceTimehφ':P.toFun φ' x' = -P.μ2 ^ 2 / (4 * P.𝓵)h':P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)] at h'refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a bφ':HiggsFieldx':SpaceTimehφ':P.toFun φ' x' = -P.μ2 ^ 2 / (4 * P.𝓵)h':P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)
    have hφ := (h1 (P.toFun φ x)).mp ⟨φ, x, rfl⟩refine_1P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a bφ':HiggsFieldx':SpaceTimehφ':P.toFun φ' x' = -P.μ2 ^ 2 / (4 * P.𝓵)h':P.toFun φ x ≤ -P.μ2 ^ 2 / (4 * P.𝓵)hφ:-P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ x⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)
    linarithAll goals completed! 🐙
  ·refine_2P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)⊢ ∀ (a : HiggsField) (b : SpaceTime), P.toFun φ x ≤ P.toFun a b intro φ' x'refine_2P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)φ':HiggsFieldx':SpaceTime⊢ P.toFun φ x ≤ P.toFun φ' x'
    rw [hrefine_2P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)φ':HiggsFieldx':SpaceTime⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ' x'refine_2P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)φ':HiggsFieldx':SpaceTime⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ' x']refine_2P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTimeh1:∀ (c : ℝ), (∃ φ x, P.toFun φ x = c) ↔ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ ch:P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)φ':HiggsFieldx':SpaceTime⊢ -P.μ2 ^ 2 / (4 * P.𝓵) ≤ P.toFun φ' x'
    exact (h1 (P.toFun φ' x')).mp ⟨φ', x', rfl⟩All goals completed! 🐙

lemma isMinOn_iff_field_of_μSq_nonneg_𝓵_pos (h𝓵 : 0 < P.𝓵) (hμ2 : 0 ≤ P.μ2) (φ : HiggsField)
    (x : SpaceTime) : IsMinOn (fun (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔
    ‖φ‖_H^2 x = P.μ2 /(2 * P.𝓵) := byP:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTime⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)
  rw [P.isMinOn_iff_of_μSq_nonneg_𝓵_pos h𝓵 hμ2 φ x,P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵) ↔ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵)All goals completed! 🐙 ← P.quadDiscrim_eq_zero_iff_normSq
    (Ne.symm (ne_of_lt h𝓵)),P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵) ↔ P.quadDiscrim φ x = 0All goals completed! 🐙 P.quadDiscrim_eq_zero_iff (Ne.symm (ne_of_lt h𝓵))P:Potentialh𝓵:0 < P.𝓵hμ2:0 ≤ P.μ2φ:HiggsFieldx:SpaceTime⊢ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵) ↔ P.toFun φ x = -P.μ2 ^ 2 / (4 * P.𝓵)All goals completed! 🐙]All goals completed! 🐙

Given an element P of Potential with 0 < l, then the Higgs field φ and spacetime point x minimize the potential if and only if one of the following conditions holds

0 ≤ μ2 and ‖φ‖_H^2 x = μ2 / (2 * 𝓵).

or μ2 < 0 and φ x = 0.

theorem isMinOn_iff_field_of_𝓵_pos (h𝓵 : 0 < P.𝓵) (φ : HiggsField) (x : SpaceTime) :
    IsMinOn (fun (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔
    (0 ≤ P.μ2 ∧ ‖φ‖_H^2 x = P.μ2 /(2 * P.𝓵)) ∨ (P.μ2 < 0 ∧ φ x = 0) := byP:Potentialh𝓵:0 < P.𝓵φ:HiggsFieldx:SpaceTime⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  0 ≤ P.μ2 ∧ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) ∨ P.μ2 < 0 ∧ φ x = 0
  by_cases hμ2 : 0 ≤ P.μ2posP:Potentialh𝓵:0 < P.𝓵φ:HiggsFieldx:SpaceTimehμ2:0 ≤ P.μ2⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  0 ≤ P.μ2 ∧ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) ∨ P.μ2 < 0 ∧ φ x = 0negP:Potentialh𝓵:0 < P.𝓵φ:HiggsFieldx:SpaceTimehμ2:¬0 ≤ P.μ2⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  0 ≤ P.μ2 ∧ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) ∨ P.μ2 < 0 ∧ φ x = 0
  ·posP:Potentialh𝓵:0 < P.𝓵φ:HiggsFieldx:SpaceTimehμ2:0 ≤ P.μ2⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  0 ≤ P.μ2 ∧ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) ∨ P.μ2 < 0 ∧ φ x = 0 simpa [not_lt.mpr hμ2, hμ2] using P.isMinOn_iff_field_of_μSq_nonneg_𝓵_pos h𝓵 hμ2 φ xAll goals completed! 🐙
  ·negP:Potentialh𝓵:0 < P.𝓵φ:HiggsFieldx:SpaceTimehμ2:¬0 ≤ P.μ2⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  0 ≤ P.μ2 ∧ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) ∨ P.μ2 < 0 ∧ φ x = 0 simpa [hμ2, lt_of_not_ge hμ2] using P.isMinOn_iff_field_of_μSq_nonpos_𝓵_pos h𝓵 (byP:Potentialh𝓵:0 < P.𝓵φ:HiggsFieldx:SpaceTimehμ2:¬0 ≤ P.μ2⊢ P.μ2 ≤ 0 linarithAll goals completed! 🐙) φ x



lemma isMaxOn_iff_isMinOn_neg (φ : HiggsField) (x : SpaceTime) :
    IsMaxOn (fun (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔
    IsMinOn (fun (φ, x) => P.neg.toFun φ x) Set.univ (φ, x) := byP:Potentialφ:HiggsFieldx:SpaceTime⊢ IsMaxOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.neg.toFun φ x)
    Set.univ (φ, x)
  simp only [toFun_neg]P:Potentialφ:HiggsFieldx:SpaceTime⊢ IsMaxOn (fun x => P.toFun x.1 x.2) Set.univ (φ, x) ↔ IsMinOn (fun x => -P.toFun x.1 x.2) Set.univ (φ, x)
  rw [isMaxOn_univ_iff,P:Potentialφ:HiggsFieldx:SpaceTime⊢ (∀ (x_1 : HiggsField × SpaceTime), P.toFun x_1.1 x_1.2 ≤ P.toFun (φ, x).1 (φ, x).2) ↔
  IsMinOn (fun x => -P.toFun x.1 x.2) Set.univ (φ, x)P:Potentialφ:HiggsFieldx:SpaceTime⊢ (∀ (x_1 : HiggsField × SpaceTime), P.toFun x_1.1 x_1.2 ≤ P.toFun (φ, x).1 (φ, x).2) ↔
  ∀ (x_1 : HiggsField × SpaceTime), -P.toFun (φ, x).1 (φ, x).2 ≤ -P.toFun x_1.1 x_1.2 isMinOn_univ_iffP:Potentialφ:HiggsFieldx:SpaceTime⊢ (∀ (x_1 : HiggsField × SpaceTime), P.toFun x_1.1 x_1.2 ≤ P.toFun (φ, x).1 (φ, x).2) ↔
  ∀ (x_1 : HiggsField × SpaceTime), -P.toFun (φ, x).1 (φ, x).2 ≤ -P.toFun x_1.1 x_1.2P:Potentialφ:HiggsFieldx:SpaceTime⊢ (∀ (x_1 : HiggsField × SpaceTime), P.toFun x_1.1 x_1.2 ≤ P.toFun (φ, x).1 (φ, x).2) ↔
  ∀ (x_1 : HiggsField × SpaceTime), -P.toFun (φ, x).1 (φ, x).2 ≤ -P.toFun x_1.1 x_1.2]P:Potentialφ:HiggsFieldx:SpaceTime⊢ (∀ (x_1 : HiggsField × SpaceTime), P.toFun x_1.1 x_1.2 ≤ P.toFun (φ, x).1 (φ, x).2) ↔
  ∀ (x_1 : HiggsField × SpaceTime), -P.toFun (φ, x).1 (φ, x).2 ≤ -P.toFun x_1.1 x_1.2
  simp_all only [Prod.forall, neg_le_neg_iff]All goals completed! 🐙

Given an element P of Potential with l < 0, then the Higgs field φ and spacetime point x maximizes the potential if and only if one of the following conditions holds

μ2 ≤ 0 and ‖φ‖_H^2 x = μ2 / (2 * 𝓵).

or 0 < μ2 and φ x = 0.


lemma isMaxOn_iff_field_of_𝓵_neg (h𝓵 : P.𝓵 < 0) (φ : HiggsField) (x : SpaceTime) :
    IsMaxOn (fun (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔
    (P.μ2 ≤ 0 ∧ ‖φ‖_H^2 x = P.μ2 /(2 * P.𝓵)) ∨ (0 < P.μ2 ∧ φ x = 0) := byP:Potentialh𝓵:P.𝓵 < 0φ:HiggsFieldx:SpaceTime⊢ IsMaxOn
    (fun x =>
      match x with
      | (φ, x) => P.toFun φ x)
    Set.univ (φ, x) ↔
  P.μ2 ≤ 0 ∧ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) ∨ 0 < P.μ2 ∧ φ x = 0
  rw [P.isMaxOn_iff_isMinOn_neg,P:Potentialh𝓵:P.𝓵 < 0φ:HiggsFieldx:SpaceTime⊢ IsMinOn
    (fun x =>
      match x with
      | (φ, x) => P.neg.toFun φ x)
    Set.univ (φ, x) ↔
  P.μ2 ≤ 0 ∧ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) ∨ 0 < P.μ2 ∧ φ x = 0P:Potentialh𝓵:P.𝓵 < 0φ:HiggsFieldx:SpaceTime⊢ 0 ≤ P.neg.μ2 ∧ ‖φ‖_H^2 x = P.neg.μ2 / (2 * P.neg.𝓵) ∨ P.neg.μ2 < 0 ∧ φ x = 0 ↔
  P.μ2 ≤ 0 ∧ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) ∨ 0 < P.μ2 ∧ φ x = 0
    P.neg.isMinOn_iff_field_of_𝓵_pos (byP:Potentialh𝓵:P.𝓵 < 0φ:HiggsFieldx:SpaceTime⊢ 0 < P.neg.𝓵P:Potentialh𝓵:P.𝓵 < 0φ:HiggsFieldx:SpaceTime⊢ 0 ≤ P.neg.μ2 ∧ ‖φ‖_H^2 x = P.neg.μ2 / (2 * P.neg.𝓵) ∨ P.neg.μ2 < 0 ∧ φ x = 0 ↔
  P.μ2 ≤ 0 ∧ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) ∨ 0 < P.μ2 ∧ φ x = 0 simpa using h𝓵All goals completed! 🐙P:Potentialh𝓵:P.𝓵 < 0φ:HiggsFieldx:SpaceTime⊢ 0 ≤ P.neg.μ2 ∧ ‖φ‖_H^2 x = P.neg.μ2 / (2 * P.neg.𝓵) ∨ P.neg.μ2 < 0 ∧ φ x = 0 ↔
  P.μ2 ≤ 0 ∧ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) ∨ 0 < P.μ2 ∧ φ x = 0)]P:Potentialh𝓵:P.𝓵 < 0φ:HiggsFieldx:SpaceTime⊢ 0 ≤ P.neg.μ2 ∧ ‖φ‖_H^2 x = P.neg.μ2 / (2 * P.neg.𝓵) ∨ P.neg.μ2 < 0 ∧ φ x = 0 ↔
  P.μ2 ≤ 0 ∧ ‖φ‖_H^2 x = P.μ2 / (2 * P.𝓵) ∨ 0 < P.μ2 ∧ φ x = 0
  simpAll goals completed! 🐙