Prove2Me

The box 2 scalar terms are U(2)U(2)-invariant

Proved
SMHiggsPotential.scalarLagrangian_unitary_invariant

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

higgsparticle-physicsstandard-model

Let g≠0g\neq0, M≠0M\neq0 and mh,βh∈Rm_h,\beta_h\in\mathbb R. Let (H,ϕ0,ϕ+)(H,\phi^0,\phi^+) and (H′,ϕ0′,ϕ+′)(H',\phi^{0\prime},\phi^{+\prime}) be two field configurations, and let UU be a 2×22\times2 unitary matrix with Φ(H′,ϕ0′,ϕ+′)=U Φ(H,ϕ0,ϕ+)\Phi(H',\phi^{0\prime},\phi^{+\prime})=U\,\Phi(H,\phi^0,\phi^+). Then the scalar terms of box 2 agree:

LV(H′,ϕ0′,ϕ+′)=LV(H,ϕ0,ϕ+).\mathcal L_V(H',\phi^{0\prime},\phi^{+\prime})=\mathcal L_V(H,\phi^0,\phi^+).
Preamble
import Mathlib
import Definitions.Def_SMHiggsPotential_Defs
open Complex
Formal statement
namespace SMHiggsPotential

theorem scalarLagrangian_unitary_invariant (g M mh βh H φ0 H' φ0' : ℝ) (φp φp' : ℂ)
    (hM : M ≠ 0) (hg : g ≠ 0) (U : Matrix.unitaryGroup (Fin 2) ℂ)
    (hU : higgsDoublet g M H' φ0' φp' =
      Matrix.mulVec (U : Matrix (Fin 2) (Fin 2) ℂ) (higgsDoublet g M H φ0 φp)) :
    scalarLagrangian g M mh βh H' φ0' φp' = scalarLagrangian g M mh βh 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 g,M,mh,βh,H,ϕ0,H′,ϕ0′g,M,m_h,\beta_h,H,\phi^0,H',\phi^{0\prime}; complex ϕ+,ϕ+′\phi^+,\phi^{+\prime}; a 2×22\times2 complex matrix UU with U∗U=UU∗=IU^*U=UU^*=I. Hypotheses: M≠0M\neq0, g≠0g\neq0, and Φ(g,M,H′,ϕ0′,ϕ+′)=U Φ(g,M,H,ϕ0,ϕ+)\Phi(g,M,H',\phi^{0\prime},\phi^{+\prime})=U\,\Phi(g,M,H,\phi^0,\phi^+) (matrix-vector product), with Φ\Phi the doublet of the definition file.

Claim. LV(g,M,mh,βh;H′,ϕ0′,ϕ+′)=LV(g,M,mh,βh;H,ϕ0,ϕ+)\mathcal L_V(g,M,m_h,\beta_h;H',\phi^{0\prime},\phi^{+\prime})=\mathcal L_V(g,M,m_h,\beta_h;H,\phi^0,\phi^+). The same g,M,mh,βhg,M,m_h,\beta_h are used on both sides.

View graph