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 Physlib.Particles.BeyondTheStandardModel.TwoHDM.GramMatrixA polynomial family of orbit representatives for the two Higgs doublet model
Every gauge orbit of the two Higgs doublet model meets the four–real–parameter family
repHiggs X = ⟨(X₀, 0), (X₁ + i X₂, X₃)⟩.
The crucial feature of this family (compared with the normalised representatives of
gaugeGroupI_exists_fst_eq_snd_eq) is that it is a polynomial family: the Gram vector of
repHiggs X is a polynomial in X, with no square roots. Consequently the value of a gauge
invariant potential on any field configuration is V (repHiggs X) for a suitable X, and the
question of whether V is a polynomial in the Gram vector reduces to the purely algebraic question
of whether V ∘ repHiggs lies in the subring generated by the (polynomial) Gram components of the
representative family.
@[expose] public section
A four–real–parameter polynomial family of representatives for the gauge orbits: the first
doublet is (X₀, 0) and the second is (X₁ + i X₂, X₃).
def repHiggs (X : Fin 4 → ℝ) : TwoHiggsDoublet where
Φ1 := !2[(X 0 : ℂ), 0]
Φ2 := !2[(X 1 : ℂ) + Complex.I * (X 2 : ℂ), (X 3 : ℂ)]@[simp]
lemma repHiggs_Φ1 (X : Fin 4 → ℝ) : (repHiggs X).Φ1 = !2[(X 0 : ℂ), 0] := rfl@[simp]
lemma repHiggs_Φ2 (X : Fin 4 → ℝ) :
(repHiggs X).Φ2 = !2[(X 1 : ℂ) + Complex.I * (X 2 : ℂ), (X 3 : ℂ)] := rflX:Fin 4 → ℝ⊢ ‖!₂[↑(X 0), 0].ofLp 0‖ ^ 2 + ‖!₂[↑(X 0), 0].ofLp 1‖ ^ 2 = X 0 ^ 2
All goals completed! 🐙X:Fin 4 → ℝ⊢ Complex.normSq (!₂[↑(X 1) + Complex.I * ↑(X 2), ↑(X 3)].ofLp 0) +
Complex.normSq (!₂[↑(X 1) + Complex.I * ↑(X 2), ↑(X 3)].ofLp 1) =
X 1 ^ 2 + X 2 ^ 2 + X 3 ^ 2
X:Fin 4 → ℝ⊢ (X 1 + (0 * X 2 - 1 * 0)) * (X 1 + (0 * X 2 - 1 * 0)) + (0 + (0 * 0 + 1 * X 2)) * (0 + (0 * 0 + 1 * X 2)) +
(X 3 * X 3 + 0 * 0) =
X 1 ^ 2 + X 2 ^ 2 + X 3 ^ 2
All goals completed! 🐙X:Fin 4 → ℝ⊢ ⟪!₂[↑(X 0), 0].ofLp 0, !₂[↑(X 1) + Complex.I * ↑(X 2), ↑(X 3)].ofLp 0⟫_ℂ +
⟪!₂[↑(X 0), 0].ofLp 1, !₂[↑(X 1) + Complex.I * ↑(X 2), ↑(X 3)].ofLp 1⟫_ℂ =
↑(X 0) * (↑(X 1) + Complex.I * ↑(X 2))
X:Fin 4 → ℝ⊢ (↑(X 1) + Complex.I * ↑(X 2)) * ↑(X 0) + ↑(X 3) * 0 = ↑(X 0) * (↑(X 1) + Complex.I * ↑(X 2))
All goals completed! 🐙The Gram vector of a representative
The Gram vector of repHiggs X is an explicit polynomial in the four real parameters X.
All goals completed! 🐙X:Fin 4 → ℝ⊢ 2 * (↑(X 0) * (↑(X 1) + Complex.I * ↑(X 2))).re = 2 * X 0 * X 1
X:Fin 4 → ℝ⊢ 2 * (X 0 * (X 1 + (0 * X 2 - 1 * 0)) - 0 * (0 + (0 * 0 + 1 * X 2))) = 2 * X 0 * X 1
All goals completed! 🐙X:Fin 4 → ℝ⊢ 2 * (↑(X 0) * (↑(X 1) + Complex.I * ↑(X 2))).im = 2 * X 0 * X 2
X:Fin 4 → ℝ⊢ 2 * (X 0 * (0 + (0 * 0 + 1 * X 2)) + 0 * (X 1 + (0 * X 2 - 1 * 0))) = 2 * X 0 * X 2
All goals completed! 🐙All goals completed! 🐙Every configuration is gauge equivalent to a representative
Every field configuration is in the gauge orbit of a representative repHiggs X. This is the
key fact that lets a gauge invariant potential be evaluated on the polynomial family.
All goals completed! 🐙
φ:TwoHiggsDoubleth:¬φ.Φ1 = 0g:GaugeGroupIh1:g • φ.Φ1 = !₂[↑‖φ.Φ1‖, 0]h2:g • φ.Φ2 = !₂[⟪φ.Φ1, φ.Φ2⟫_ℂ / ↑‖φ.Φ1‖, ↑√φ.gramMatrix.det.re / ↑‖φ.Φ1‖]⊢ !₂[⟪φ.Φ1, φ.Φ2⟫_ℂ / ↑‖φ.Φ1‖, ↑√φ.gramMatrix.det.re / ↑‖φ.Φ1‖].ofLp ((fun i => i) ⟨1, ⋯⟩) =
!₂[↑(![‖φ.Φ1‖, (⟪φ.Φ1, φ.Φ2⟫_ℂ / ↑‖φ.Φ1‖).re, (⟪φ.Φ1, φ.Φ2⟫_ℂ / ↑‖φ.Φ1‖).im, √φ.gramMatrix.det.re / ‖φ.Φ1‖] 1) +
Complex.I *
↑(![‖φ.Φ1‖, (⟪φ.Φ1, φ.Φ2⟫_ℂ / ↑‖φ.Φ1‖).re, (⟪φ.Φ1, φ.Φ2⟫_ℂ / ↑‖φ.Φ1‖).im, √φ.gramMatrix.det.re / ‖φ.Φ1‖] 2),
↑(![‖φ.Φ1‖, (⟪φ.Φ1, φ.Φ2⟫_ℂ / ↑‖φ.Φ1‖).re, (⟪φ.Φ1, φ.Φ2⟫_ℂ / ↑‖φ.Φ1‖).im, √φ.gramMatrix.det.re / ‖φ.Φ1‖]
3)].ofLp
((fun i => i) ⟨1, ⋯⟩) All goals completed! 🐙