Prove2Me

Box 2 scalar terms =−λ(Φ†Φ)2+(12mh2−βh) Φ†Φ=-\lambda(\Phi^\dagger\Phi)^2+(\tfrac12m_h^2-\beta_h)\,\Phi^\dagger\Phi

Proved
SMHiggsPotential.scalarLagrangian_eq_doublet_potential

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

higgsparticle-physicsstandard-model

Let g≠0g\neq0 and M≠0M\neq0, and let mh,βhm_h,\beta_h be real. For all real H,ϕ0H,\phi^0 and complex ϕ+\phi^+, the non-derivative scalar terms LV\mathcal L_V of box 2 (see the definition file) depend on the fields only through the doublet norm Φ†Φ\Phi^\dagger\Phi, with Φ=(ϕ+,(v+H+iϕ0)/2)\Phi=(\phi^+,(v+H+i\phi^0)/\sqrt2) and v=2M/gv=2M/g:

LV=−λ (Φ†Φ)2+(mh22−βh)Φ†Φ,λ=g2mh28M2.\mathcal L_V=-\lambda\,(\Phi^\dagger\Phi)^2+\Big(\frac{m_h^2}{2}-\beta_h\Big)\Phi^\dagger\Phi,\qquad \lambda=\frac{g^2m_h^2}{8M^2}.

So the scalar sector of the chart is minus the standard Higgs potential V(Φ)=λ(Φ†Φ)2−μ2Φ†ΦV(\Phi)=\lambda(\Phi^\dagger\Phi)^2-\mu^2\Phi^\dagger\Phi with μ2=mh22−βh\mu^2=\frac{m_h^2}{2}-\beta_h. Equivalently, LV=−λ(Φ†Φ−v22)2−βhΦ†Φ+2M4g2αh\mathcal L_V=-\lambda(\Phi^\dagger\Phi-\frac{v^2}{2})^2-\beta_h\Phi^\dagger\Phi+\frac{2M^4}{g^2}\alpha_h.

Preamble
import Mathlib
import Definitions.Def_SMHiggsPotential_Defs
open Complex
Formal statement
namespace SMHiggsPotential

theorem scalarLagrangian_eq_doublet_potential (g M mh βh H φ0 : ℝ) (φp : ℂ)
    (hM : M ≠ 0) (hg : g ≠ 0) :
    scalarLagrangian g M mh βh H φ0 φp =
      - quarticCoupling g M mh * doubletNormSq (higgsDoublet g M H φ0 φp) ^ 2
        + (mh ^ 2 / 2 - βh) * doubletNormSq (higgsDoublet g M H φ0 φp) := by sorry

end SMHiggsPotential
Source
Standard Model Lagrangian in Veltman's conventions (Feynman-'t Hooft gauge), as printed in the five-box chart supplied by the proposer (after M. Veltman, *Diagrammatica: The Path to Feynman Diagrams*, Cambridge University Press, 1994). Box 2, the non-derivative scalar terms: −12mh2H2-\frac12 m_h^2H^2, the βh[… ]\beta_h[\dots] term, +2M4g2αh+\frac{2M^4}{g^2}\alpha_h, −gα[H3+Hϕ0ϕ0+2Hϕ+ϕ−]-g\alpha[H^3+H\phi^0\phi^0+2H\phi^+\phi^-] and −18g2αh[H4+… ]-\frac18g^2\alpha_h[H^4+\dots].
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - drafting agent, NON-BLIND (not an independent auditor)

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the intended meaning and of the source image. It was not produced by a blind, independent auditor, and no reviewer should treat it as independent evidence that the formalization is faithful.

Binders. Real numbers g,M,mh,βh,H,ϕ0g,M,m_h,\beta_h,H,\phi^0 and a complex number ϕ+\phi^+. Hypotheses: M≠0M\neq0 and g≠0g\neq0.

Claim. Write X=∥Φ(g,M,H,ϕ0,ϕ+)∥2=∣ϕ+∣2+12((2M/g+H)2+(ϕ0)2)X=\|\Phi(g,M,H,\phi^0,\phi^+)\|^2=|\phi^+|^2+\tfrac12\big((2M/g+H)^2+(\phi^0)^2\big), with the doublet and norm from the definition file. Then

LV(g,M,mh,βh;H,ϕ0,ϕ+)=−g22⋅mh24M2 X2+(mh22−βh)X,\mathcal L_V(g,M,m_h,\beta_h;H,\phi^0,\phi^+)=-\frac{g^2}{2}\cdot\frac{m_h^2}{4M^2}\,X^2+\Big(\frac{m_h^2}{2}-\beta_h\Big)X,

where LV\mathcal L_V is the scalar-terms function from the definition file, with cubic coefficient gMαhgM\alpha_h. No sign conditions are placed on mhm_h or βh\beta_h.

View graph