Higgs: the potential is bounded below, with its minimum on the symmetry-breaking circle
ProvedEveryday.higgs_groundThe everyday world rests on a nonzero value of the Higgs field: the Mexican-hat potential's minimum is not at φ = 0 but on the circle |φ|² = μ²/(2λ) — the spontaneous symmetry breaking locus. The item is the vacuum structure: for positive μ and λ, the potential is bounded below by its floor -μ⁴/(4λ), and the floor is attained exactly on the circle — the potential equals its minimum if and only if |φ|² = μ²/(2λ).
Formalization Note The hypotheses are the physical signs μ > 0 and λ > 0 under which the hat has its shape; the quartic coupling λ is bound as lam in the formal statement, λ being a reserved keyword in Lean 4. The proof uses the completed square of the higgs_square milestone: the potential minus its floor is λ(|φ|² - μ²/(2λ))², nonnegative since λ > 0, and zero exactly when |φ|² = μ²/(2λ) — the positivity of λ makes the equivalence exact rather than one-way.
import Mathlib import Definitions.Def_Everyday_spacetime import Definitions.Def_Everyday_sectors
namespace Everyday
/-- Higgs: the vacuum. The Mexican-hat potential is bounded below, with
its minimum value -μ⁴/(4λ) attained exactly on the circle of fields with
|φ|² = μ²/(2λ) — the spontaneous symmetry breaking locus of the Higgs
field, the nonzero field value the everyday world rests on. The quartic
coupling λ is bound as lam, λ being a reserved keyword in Lean 4. -/
theorem higgs_ground (μ lam : ℝ) (φ : ℂ) (hμ : 0 < μ) (hlam : 0 < lam) :
-(μ ^ 4 / (4 * lam)) ≤ higgsV μ lam φ ∧
(higgsV μ lam φ = -(μ ^ 4 / (4 * lam)) ↔
Complex.normSq φ = μ ^ 2 / (2 * lam)) := by sorry
end Everyday
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for all real numbers μ and lam and every complex number φ, if μ and lam are strictly positive, then two conclusions hold. First, the real number -μ⁴/(4 lam) is less than or equal to the value of higgsV on μ, lam, and φ. Second, the value of higgsV on μ, lam, and φ equals -μ⁴/(4 lam) if and only if the squared complex modulus of φ equals μ²/(2 lam). The conclusions are an inequality and a biconditional between real numbers.