1. PhyslibAlpha
  2. Particles
  3. BeyondTheStandardModel
  4. TwoHDM
  5. Invariants
Imports
/- Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.EffectivePotential public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.SwapDoublet public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.GaugeSlice public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.OrbitRepresentative public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.ChargeBalance public import Mathlib.Algebra.MvPolynomial.Funext public import Mathlib.Algebra.MvPolynomial.Monad public import Mathlib.Algebra.MvPolynomial.Division public import Mathlib.RingTheory.MvPolynomial.Tower public import Mathlib.Analysis.Real.Pi.Irrational

The two Higgs doublet potential as a polynomial in the gauge invariants

i. Overview

In the bilinear formalism of the two Higgs doublet model (hep-ph/0605184) the four gauge-invariant bilinears — the Gram vector gramVector — describe the gauge orbits of the configuration space. This file proves the corresponding statement for the potential: every gauge-invariant polynomial effective potential is a polynomial in these four gauge-invariant bilinears.

The proof gauge-fixes the potential to the polynomial family of orbit representatives repHiggs X and runs the following physical pipeline:

    Charge balancing. Invariance under the gauge torus forces the potential, written in hypercharge eigen-coordinates, to be supported only on hypercharge-neutral monomials.

    Generation. Every neutral monomial is a product of the five neutral gauge-invariant quadratic bilinears, so the potential is a polynomial in them.

    Clearing the norms. A power of ‖Φ1‖² (resp. ‖Φ2‖², via the doublet swap) times the potential is a genuine polynomial in the Gram vector.

    Coprimality. ‖Φ1‖² and ‖Φ2‖² are coprime in the (algebraically independent) Gram ring, which removes these factors and yields the Gram polynomial.

ii. Key results

    exists_polynomial_repHiggs_sliceBilinear — on gauge representatives, the potential is a polynomial in the five real gauge-invariant bilinears.

    exists_normSq_Φ1_clearing, exists_normSq_Φ2_clearing — a power of ‖Φ1‖² (resp. ‖Φ2‖²) times the potential is a polynomial in the Gram vector.

    exists_polynomial_on_repHiggs — the potential on representatives is a polynomial in the Gram vector.

    effectivePotential_is_polynomial_gramVector — a gauge-invariant polynomial potential is a polynomial in the four gauge-invariant bilinears.

iii. Table of contents

    A. Gauge-torus invariance of the potential on the slice

    B. Hypercharge eigen-coordinates and charge balancing

    C. Generation by the neutral gauge-invariant bilinears

    D. The potential on representatives as a polynomial in the bilinears

    E. Clearing the ‖Φ1‖² and ‖Φ2‖² factors

    F. Independence and coprimality of the Gram invariants

    G. The gauge-invariant potential as a polynomial in the Gram vector

iv. References

    The bilinear formalism: https://arxiv.org/abs/hep-ph/0605184.

Mathematically the result is the first fundamental theorem of invariant theory for SU(2) acting on two doublets in ℂ².

@[expose] public section

A. Gauge-torus invariance of the potential on the slice

Invariance of the potential under the gauge torus forces the slice polynomial P to be invariant under the hypercharge rotations of its variables: the Cartan rotation cartanSubst and the residual U(1) rotation residualSubst.

B. Hypercharge eigen-coordinates and charge balancing

Changing to hypercharge eigen-coordinates z, z̄, w₀, w̄₀, w₁, w̄₁ diagonalises the gauge-torus rotation into a scaling by the hypercharges cartanCharge (Cartan) and hyperCharge (residual). Feeding an infinite-order phase into the invariance from part A shows that every monomial of the potential carrying nonzero hypercharge has vanishing coefficient.

The Cartan hypercharges of z, z̄, w₀, w̄₀, w₁, w̄₁.

def cartanCharge : Fin 6 → ℤ := ![1, -1, 1, -1, -1, 1]

The residual-U(1) hypercharges (only the perpendicular pair is charged).

def hyperCharge : Fin 6 → ℤ := ![0, 0, 0, 0, 1, -1]

There is a gauge phase of infinite order (exp i), needed to run charge balancing.

key:star (Complex.exp Complex.I) * Complex.exp Complex.I = 1key2:Complex.exp Complex.I * star (Complex.exp Complex.I) = 1n:ℤk:ℤhk:↑n * Complex.I = ↑k * (2 * ↑Real.pi * Complex.I)hc:↑n = ↑k * (2 * ↑Real.pi)hr:↑n = ↑k * (2 * Real.pi)hk0:k ≠ 0h2k:2 * ↑k ≠ 0hpi:Real.pi = ↑n / (2 * ↑k)⊢ ↑n / (2 * ↑k) = ↑(↑n / (2 * ↑k)); key:star (Complex.exp Complex.I) * Complex.exp Complex.I = 1key2:Complex.exp Complex.I * star (Complex.exp Complex.I) = 1n:ℤk:ℤhk:↑n * Complex.I = ↑k * (2 * ↑Real.pi * Complex.I)hc:↑n = ↑k * (2 * ↑Real.pi)hr:↑n = ↑k * (2 * Real.pi)hk0:k ≠ 0h2k:2 * ↑k ≠ 0hpi:Real.pi = ↑n / (2 * ↑k)⊢ ↑n / (2 * ↑k) = ↑n / (2 * ↑k); All goals completed! 🐙)

C. Generation by the neutral gauge-invariant bilinears

The hypercharge-neutral monomials of Qslice P are exactly the products of the five neutral quadratic bilinears z z̄, w₀ w̄₀, z w̄₀, z̄ w₀, w₁ w̄₁ — the gauge invariants. This is the (abelian)generation step: combined Cartan- and residual-neutrality of a monomial forces it to be a product of these five, because every charged variable carries a unit Cartan charge and the residual charges come in an exact ±1 pair.

The charge of a monomial, summed over the whole index set, equals the sum over its support.

w:Fin 6 → ℤm:Fin 6 →₀ ℕi:Fin 6a✝:i ∈ Finset.univhi:i ∉ m.support⊢ ↑0 * w i = 0; All goals completed! 🐙

A charge sum is additive in the monomial.

w:Fin 6 → ℤa:Fin 6 →₀ ℕb:Fin 6 →₀ ℕk:Fin 6a✝:k ∈ Finset.univ⊢ ↑(a k + b k) * w k = ↑(a k) * w k + ↑(b k) * w k; w:Fin 6 → ℤa:Fin 6 →₀ ℕb:Fin 6 →₀ ℕk:Fin 6a✝:k ∈ Finset.univ⊢ (↑(a k) + ↑(b k)) * w k = ↑(a k) * w k + ↑(b k) * w k; All goals completed! 🐙

The charge sum of a single generator is the charge of that variable.

lemma chargeSum_single (w : Fin 6 → ℤ) (i : Fin 6) : ∑ k, ((Finsupp.single i (1 : ℕ)) k : ℤ) * w k = w i := w:Fin 6 → ℤi:Fin 6⊢ ∑ k, ↑((Finsupp.single i 1) k) * w k = w i All goals completed! 🐙

D. The potential on representatives as a polynomial in the bilinears

Evaluating at the hypercharge eigen-point of a representative repHiggs X, and descending from the complex value back to its real part, turns the generation result of part C into the statement that the value V (repHiggs X) is a polynomial in the five real gauge-invariant bilinears ‖Φ1‖², Re⟪⟫, Im⟪⟫, |Φ2₀|², |Φ2₁|².

The slice parameters realising repHiggs X as a point of the slice family.

def aRep (X : Fin 4 → ℝ) : Fin 6 → ℝ := ![X 0, 0, X 1, X 2, X 3, 0]
X:Fin 4 → ℝ⊢ sliceHiggs (↑(X 0)) (↑(X 1) + Complex.I * ↑(X 2)) ↑(X 3) = sliceHiggs (↑(aRep X 0) + Complex.I * ↑(aRep X 1)) (↑(aRep X 2) + Complex.I * ↑(aRep X 3)) (↑(aRep X 4) + Complex.I * ↑(aRep X 5)) All goals completed! 🐙

The five real gauge-invariant bilinears, evaluated at repHiggs X: ‖Φ1‖², Re⟪⟫, Im⟪⟫, |Φ2₀|², |Φ2₁|².

def sliceBilinear (X : Fin 4 → ℝ) : Fin 5 → ℝ := ![X 0 ^ 2, X 0 * X 1, X 0 * X 2, X 1 ^ 2 + X 2 ^ 2, X 3 ^ 2]

E. Clearing the ‖Φ1‖² and ‖Φ2‖² factors

Part D expresses the value as a polynomial in the bilinears, but two of them — |Φ2₀|² and |Φ2₁|² — are not directly Gram polynomials. Multiplying by a power of ‖Φ1‖² clears these; the doublet swap of SwapDoublet then gives the mirror statement with ‖Φ2‖².

F. Independence and coprimality of the Gram invariants

The four Gram invariants are algebraically independent (gramPoly_injective), and the two linear combinations ‖Φ1‖² = (g₀+g₃)/2 and ‖Φ2‖² = (g₀-g₃)/2 are coprime in the Gram ring (uPow_dvd). Together these let the ‖Φ1‖² and ‖Φ2‖² factors be cancelled.

G. The gauge-invariant potential as a polynomial in the Gram vector

Every configuration is gauge equivalent to a representative repHiggs X (exists_smul_eq_repHiggs) whose Gram vector is polynomial in the parameters (gramVector_repHiggs_*). Combining the two norm clearings of part E with the coprimality of part F removes the ‖Φ1‖²/‖Φ2‖² factors and produces the Gram polynomial on representatives (exists_polynomial_on_repHiggs); gauge invariance then transports it to all configurations.

The two Higgs doublet potential in the bilinear formalism. A gauge-invariant polynomial effective potential of maximum mass dimension n is a polynomial in the four gauge-invariant bilinears — the entries of the Gram vector.

All goals completed! 🐙