Higgs: the Mexican-hat potential is a completed square with floor -μ⁴/(4λ)
ProvedEveryday.higgs_squareThe image's Higgs label is -|D_μ Φ|² - V(Φ), the potential V written abstractly; the Standard Model potential it denotes is the Mexican hat -μ²|φ|² + λ|φ|⁴. The item is the potential's algebraic shape: the Mexican hat is a completed square. For nonzero quartic coupling, -μ²|φ|² + λ|φ|⁴ equals λ(|φ|² - μ²/(2λ))² minus the constant μ⁴/(4λ): a quartic bowl in |φ|² with its floor and its location read off the square.
Formalization Note The potential is the Standard Model Mexican hat with real parameters μ and λ, the standard instantiation of the source's abstract V(Φ); the single hypothesis is that the quartic coupling is nonzero, which the completion needs for its denominators. The quartic coupling λ is bound as lam in the formal statement, λ being a reserved keyword in Lean 4. The proof: after clearing the nonzero denominators, both sides expand to the same polynomial in the real number |φ|².
import Mathlib import Definitions.Def_Everyday_spacetime import Definitions.Def_Everyday_sectors
namespace Everyday
/-- Higgs: the Mexican-hat potential is a completed square —
-μ²|φ|² + λ|φ|⁴ equals λ(|φ|² - μ²/(2λ))² minus the floor μ⁴/(4λ).
The potential's shape is a hat: a quadratic bowl in |φ|² lifted by the
quartic, with its minimum value and its location read off the square.
The quartic coupling λ is bound as lam, λ being a reserved keyword in
Lean 4. -/
theorem higgs_square (μ lam : ℝ) (φ : ℂ) (hlam : lam ≠ 0) :
higgsV μ lam φ
= -(μ ^ 4 / (4 * lam)) + lam * (Complex.normSq φ - μ ^ 2 / (2 * lam)) ^ 2 := 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 lam is nonzero, then the value of higgsV on μ, lam, and φ — which unfolds to minus μ squared times the squared complex modulus of φ, plus lam times the square of that squared modulus — equals the negation of (μ to the fourth power, divided by four times lam), plus lam times the square of (the squared modulus of φ minus μ squared over twice lam). The conclusion is an equation between real numbers.