The $\beta_h$ bracket is $\Phi^\dagger\Phi$

Proved

SMHiggsPotential.doubletNormSq_higgsDoublet

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

higgsparticle-physicsstandard-model

For all real $g,M,H,\phi^0$ and complex $\phi^+$ , the Higgs doublet $\Phi=(\phi^+,(v+H+i\phi^0)/\sqrt2)$ , $v=2M/g$ , satisfies

\Phi^\dagger\Phi=\frac{2M^2}{g^2}+\frac{2M}{g}H+\frac12\big(H^2+(\phi^0)^2+2\phi^+\phi^-\big),

which is the bracket multiplying $-\beta_h$ in box 2. (No hypothesis on $g$ is needed: for $g=0$ both sides use the Lean convention $x/0=0$ .)

Preamble

import Mathlib
import Definitions.Def_SMHiggsPotential_Defs
open Complex

Formal statement

namespace SMHiggsPotential

theorem doubletNormSq_higgsDoublet (g M H φ0 : ℝ) (φp : ℂ) :
    doubletNormSq (higgsDoublet g M H φ0 φp) =
      2 * M ^ 2 / g ^ 2 + 2 * M / g * H + (1 / 2) * (H ^ 2 + φ0 ^ 2 + 2 * normSq φ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:

-\frac12 m_h^2H^2

, the

\beta_h[\dots]

term,

+\frac{2M^4}{g^2}\alpha_h

-g\alpha[H^3+H\phi^0\phi^0+2H\phi^+\phi^-]

and

-\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 $g,M,H,\phi^0$ and complex $\phi^+$ ; no hypotheses. In particular $g=0$ is allowed, and then $2M/g=0$ and $2M^2/g^2=0$ .

Claim.

|\phi^+|^2+\Big|\frac{(2M/g+H)+i\phi^0}{\sqrt2}\Big|^2=\frac{2M^2}{g^2}+\frac{2M}{g}H+\frac12\big(H^2+(\phi^0)^2+2|\phi^+|^2\big).

View graph

The βh\beta_hβh​ bracket is Φ†Φ\Phi^\dagger\PhiΦ†Φ

The $\beta_h$ bracket is $\Phi^\dagger\Phi$