The Higgs vacuum minimizes $\lambda(|h|^2 - v^2/2)^2$

Proved

ElectroweakWiki.higgs_vacuum_minimizes_potential

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

electroweakmathematical-physics

Let $\lambda>0$ and $v\in\mathbb R$ , and let $V(h) = \lambda\,(|h|^2 - v^2/2)^2$ be the Higgs potential on complex doublets $h\in\mathbb C^2$ , with $|h|^2 = |h_1|^2+|h_2|^2$ . Let $h_0 = (0, v/\sqrt2)$ . Then

$|h_0|^2 = v^2/2$ ;
$V(h_0) = 0$ ;
$V(h_0)\le V(h)$ for every $h$ ;
$V(h) = 0$ exactly when $|h|^2 = v^2/2$ .

This justifies calling $v$ the vacuum expectation value in $\mathcal L_h$ , and it identifies $h_0$ as a vacuum.

Preamble

import Definitions.Def_ElectroweakWiki_defs
open Matrix

Formal statement

namespace ElectroweakWiki

theorem higgs_vacuum_minimizes_potential (lam v : ℝ) (hlam : 0 < lam) :
    doubletNormSq (higgsVacuum v) = v ^ 2 / 2 ∧
      higgsPotential lam v (higgsVacuum v) = 0 ∧
      (∀ h : Fin 2 → ℂ, higgsPotential lam v (higgsVacuum v) ≤ higgsPotential lam v h) ∧
      (∀ h : Fin 2 → ℂ, higgsPotential lam v h = 0 ↔ doubletNormSq h = v ^ 2 / 2) := by sorry

end ElectroweakWiki

Source

Wikipedia, "Electroweak interaction", revision oldid=1360331872, https://en.wikipedia.org/w/index.php?title=Electroweak_interaction&oldid=1360331872; Section 'Before electroweak symmetry breaking', L_h = |D_μ h|² − λ(|h|² − v²/2)², 'where v is the vacuum expectation value' (p. 4 of the PDF)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted these Lean statements (at the explicit direction of the proposal's owner), not by an independent blind auditor. The author knew the intended meaning while writing it, so it must not be mistaken for independent testimony; reviewers should check it against the Lean code themselves.

For all real $\lambda, v$ with $\lambda>0$ , writing $|h|^2 = |h_1|^2+|h_2|^2$ for $h\in\mathbb C^2$ , $V(h) = \lambda(|h|^2 - v^2/2)^2$ and $h_0 = (0, v/\sqrt2)$ , the statement asserts: $|h_0|^2 = v^2/2$ ; $V(h_0) = 0$ ; for every $h\in\mathbb C^2$ , $V(h_0)\le V(h)$ ; and for every $h\in\mathbb C^2$ , $V(h)=0$ if and only if $|h|^2 = v^2/2$ . The case $v=0$ is allowed.

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The Higgs vacuum minimizes λ(∣h∣2−v2/2)2\lambda(|h|^2 - v^2/2)^2λ(∣h∣2−v2/2)2

The Higgs vacuum minimizes $\lambda(|h|^2 - v^2/2)^2$