feat(PhyslibAlpha/Particles): The effective potential of the 2HDM

PhyslibAlpha.lean

@@ -30,3 +30,11 @@ public import PhyslibAlpha.QuantumMechanics.QuantumHarmonicOscillator
 public import PhyslibAlpha.QuantumMechanics.StinespringDilation
 public import PhyslibAlpha.Mathematics.PartialDerivativeTest
 public import PhyslibAlpha.ClassicalMechanics.CoupledSpringPotential
+public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.ChargeBalance
+public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.EffectivePotential
+public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.GaugeSlice
+public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.GaugeTorus
+public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.Invariants
+public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.Module
+public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.OrbitRepresentative
+public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.SwapDoublet

PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/ChargeBalance.lean

@@ -0,0 +1,89 @@
+/-
+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 Mathlib.Algebra.MvPolynomial.Basic
+public import Mathlib.Algebra.MvPolynomial.CommRing
+public import Mathlib.Tactic.Ring
+/-!
+# Charge balancing for polynomials
+
+If the variables of a polynomial carry charges under a phase (here a single element `c` of infinite
+order), then invariance under the simultaneous phase rotation `Xᵢ ↦ c^{wᵢ} Xᵢ` forces every
+monomial to be *charge balanced* (net charge zero). This is the algebraic content of the statement
+that a gauge invariant potential, restricted to a slice on which the gauge torus acts diagonally,
+can only contain charge-balanced monomials.
+-/
+
+@[expose] public section
+
+namespace MvPolynomial
+
+open scoped Classical in
+/-- Rescaling each variable `Xᵢ` by a constant `d i` multiplies the coefficient of the monomial `m`
+  by `∏ᵢ (d i) ^ (m i)`. -/
+lemma coeff_aeval_diag {σ R : Type*} [CommRing R] (d : σ → R) (f : MvPolynomial σ R)
+    (m : σ →₀ ℕ) :
+    coeff m (aeval (fun i => C (d i) * X i) f) = (m.prod fun i k => d i ^ k) * coeff m f := by
+  induction f using MvPolynomial.induction_on generalizing m with
+  | C a =>
+    rw [aeval_C, MvPolynomial.algebraMap_eq, coeff_C]
+    by_cases hm : (0 : σ →₀ ℕ) = m
+    · subst hm; simp
+    · rw [if_neg hm, mul_zero]
+  | add p q hp hq =>
+    rw [map_add, coeff_add, coeff_add, hp m, hq m, mul_add]
+  | mul_X p i hp =>
+    rw [map_mul, aeval_X]
+    have hrw : (aeval (fun i => C (d i) * X i) p) * (C (d i) * X i)
+        = C (d i) * ((aeval (fun i => C (d i) * X i) p) * X i) := by
+      rw [mul_left_comm]
+    rw [hrw, coeff_C_mul, coeff_mul_X', coeff_mul_X']
+    by_cases hi : i ∈ m.support
+    · rw [if_pos hi, if_pos hi, hp (m - Finsupp.single i 1)]
+      have hmi : 1 ≤ m i := Nat.one_le_iff_ne_zero.mpr (Finsupp.mem_support_iff.mp hi)
+      have hle : Finsupp.single i 1 ≤ m := Finsupp.single_le_iff.mpr hmi
+      have hsplit : m = (m - Finsupp.single i 1) + Finsupp.single i 1 :=
+        (tsub_add_cancel_of_le hle).symm
+      have hprod : (m.prod fun i k => d i ^ k)
+          = ((m - Finsupp.single i 1).prod fun i k => d i ^ k) * d i := by
+        conv_lhs => rw [hsplit]
+        rw [Finsupp.prod_add_index' (by intro a; simp) (by intro a b c; rw [pow_add]),
+          Finsupp.prod_single_index (by simp)]
+        simp
+      rw [hprod]
+      ring
+    · rw [if_neg hi, if_neg hi, mul_zero, mul_zero]
+
+/-- **Charge balancing.** If each variable `Xᵢ` carries an integer charge `w i`, `c` is a phase of
+  infinite order, and the polynomial `f` is invariant under the charge rotation
+  `Xᵢ ↦ c^{wᵢ} Xᵢ`, then every monomial with nonzero net charge has vanishing coefficient. -/
+lemma coeff_eq_zero_of_charge_ne_zero {σ K : Type*} [Field K] (w : σ → ℤ) (c : K) (hc : c ≠ 0)
+    (hroot : ∀ n : ℤ, c ^ n = 1 → n = 0) {f : MvPolynomial σ K}
+    (hf : aeval (fun i => C (c ^ (w i)) * X i) f = f) {m : σ →₀ ℕ}
+    (hm : ∑ i ∈ m.support, (m i : ℤ) * w i ≠ 0) :
+    coeff m f = 0 := by
+  classical
+  have key := coeff_aeval_diag (fun i => c ^ (w i)) f m
+  rw [hf] at key
+  have hgen : ∀ s : Finset σ, ∏ i ∈ s, (c ^ (w i)) ^ (m i)
+      = c ^ (∑ i ∈ s, (m i : ℤ) * w i) := by
+    intro s
+    induction s using Finset.induction with
+    | empty => simp
+    | @insert x t hx ih =>
+      rw [Finset.prod_insert hx, Finset.sum_insert hx, ih, zpow_add₀ hc]
+      congr 1
+      rw [← zpow_natCast (c ^ w x) (m x), ← zpow_mul, mul_comm]
+  rw [Finsupp.prod, hgen] at key
+  have hne : c ^ (∑ i ∈ m.support, (m i : ℤ) * w i) ≠ 1 := fun h => hm (hroot _ h)
+  have h2 : (1 - c ^ (∑ i ∈ m.support, (m i : ℤ) * w i)) * coeff m f = 0 := by
+    rw [sub_mul, one_mul, ← key, sub_self]
+  rcases mul_eq_zero.mp h2 with h | h
+  · exact absurd (sub_eq_zero.mp h).symm hne
+  · exact h
+
+end MvPolynomial

PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/EffectivePotential.lean

@@ -0,0 +1,98 @@
+/-
+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.GramMatrix
+public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.Module
+public import Mathlib.RingTheory.MvPolynomial.Tower
+/-!
+# The effective potential of the two Higgs doublet model
+
+## i. Overview
+
+An *effective potential* of the two Higgs doublet model is a real-valued function
+`V : TwoHiggsDoublet → ℝ` of the field configuration. This file introduces the two physical
+properties of such a potential used when expressing it through the gauge-invariant bilinears:
+
+* `IsInvariant V` — invariance under the global gauge group, and
+* `HasMaxMassDimLE V n` — being a polynomial in the field components of mass dimension `≤ n`.
+
+## ii. Key results
+
+* `EffectivePotential` — the type of effective potentials.
+* `IsInvariant` — gauge invariance of a potential.
+* `HasMaxMassDimLE` — being a bounded-degree polynomial in the field components.
+* `HasMaxMassDimLE.exists_comp_linear_poly` — a polynomial potential, restricted along any
+  real-linear parametrisation of configurations, is a polynomial in the parameters.
+
+## iii. Table of contents
+
+* A. The effective potential and its gauge invariance
+* B. Maximum mass dimension
+
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace TwoHiggsDoublet
+open InnerProductSpace
+open StandardModel
+
+/-- A general potential of the Higgs field. -/
+abbrev EffectivePotential : Type := TwoHiggsDoublet → ℝ
+
+namespace EffectivePotential
+
+/-!
+## A. The effective potential and its gauge invariance
+-/
+
+/-- The proposition that the general potential is invariant under
+  the global action of the gauge group. -/
+def IsInvariant (V : EffectivePotential) : Prop :=
+  ∀ (g : GaugeGroupI), ∀ (φ : TwoHiggsDoublet), V (g • φ) = V φ
+
+/-!
+## B. Maximum mass dimension
+-/
+
+/-- The proposition that the potential `V` has a maximum mass dimension
+  less then or equal to `n` - also implying it is a polynomial. -/
+def HasMaxMassDimLE (V : EffectivePotential) (n : ℕ) : Prop :=
+  ∃ p : MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝ, (∀ φ : TwoHiggsDoublet, V φ = p.eval
+   (fun i => i φ) ) ∧ p.totalDegree ≤ n
+
+/-- A polynomial potential, restricted along any real-linear parametrisation `L` of field
+  configurations, is a genuine polynomial in the parameters. This is the bookkeeping that lets the
+  potential be evaluated on the field components of a gauge slice. -/
+lemma HasMaxMassDimLE.exists_comp_linear_poly {V : EffectivePotential} {n : ℕ}
+    (h : HasMaxMassDimLE V n) {ι : Type*} [Fintype ι] [DecidableEq ι]
+    (L : (ι → ℝ) →ₗ[ℝ] TwoHiggsDoublet) :
+    ∃ P : MvPolynomial ι ℝ, ∀ a : ι → ℝ, V (L a) = P.eval a := by
+  obtain ⟨p, hp, -⟩ := h
+  refine ⟨MvPolynomial.aeval
+    (fun i => ∑ k : ι, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p, fun a => ?_⟩
+  have key : (fun i : Module.Dual ℝ TwoHiggsDoublet => i (L a))
+      = fun i => MvPolynomial.eval a
+        (∑ k : ι, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) := by
+    funext i
+    have ha : a = ∑ k : ι, a k • (Pi.single k 1 : ι → ℝ) := by
+      funext j
+      simp [Finset.sum_apply, Pi.single_apply, Finset.sum_ite_eq]
+    rw [map_sum]
+    conv_lhs => rw [ha, map_sum, map_sum]
+    apply Finset.sum_congr rfl
+    intro k _
+    rw [map_smul, map_smul, MvPolynomial.eval_mul, MvPolynomial.eval_C, MvPolynomial.eval_X,
+      smul_eq_mul, mul_comm]
+  rw [hp, key, MvPolynomial.aeval_def, MvPolynomial.algebraMap_eq, ← MvPolynomial.eval_assoc]
+  rfl
+
+end EffectivePotential
+
+end TwoHiggsDoublet

PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/GaugeSlice.lean

@@ -0,0 +1,131 @@
+/-
+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.Module
+public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.GaugeTorus
+public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.OrbitRepresentative
+/-!
+# The gauge slice and the hypercharges of the doublet components
+
+After using `SU(2)` to align the first doublet with the first axis, a configuration lies on the
+*upper-triangular slice* `sliceHiggs z w₀ w₁ = ⟨(z, 0), (w₀, w₁)⟩`. The gauge torus acts on the
+three surviving components `z = Φ1₀`, `w₀ = Φ2₀`, `w₁ = Φ2₁` by their hypercharges:
+
+* the Cartan phase `a` multiplies the *first* components `z, w₀` (and conjugates the would-be second
+  component of `Φ1`, which vanishes here), giving `(z, w₀, w₁) ↦ (a z, a w₀, ā w₁)`;
+* the residual `U(1)` (`ofU1Subgroup c`) multiplies the *second* component `w₁` by `c⁶`, giving
+  `(z, w₀, w₁) ↦ (z, w₀, c⁶ w₁)`.
+
+These two phase rotations are the source of the charge balancing of the effective potential.
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace TwoHiggsDoublet
+
+open InnerProductSpace
+open StandardModel
+open ComplexConjugate
+
+/-- The upper-triangular slice configuration `⟨(z, 0), (w₀, w₁)⟩`. It specialises to `repHiggs`
+  when the components take their real "canonical frame" values. -/
+def sliceHiggs (z w0 w1 : ℂ) : TwoHiggsDoublet where
+  Φ1 := !₂[z, 0]
+  Φ2 := !₂[w0, w1]
+
+@[simp] lemma sliceHiggs_Φ1 (z w0 w1 : ℂ) : (sliceHiggs z w0 w1).Φ1 = !₂[z, 0] := rfl
+@[simp] lemma sliceHiggs_Φ2 (z w0 w1 : ℂ) : (sliceHiggs z w0 w1).Φ2 = !₂[w0, w1] := rfl
+
+@[simp] lemma real_smul_fst (c : ℝ) (H : TwoHiggsDoublet) : (c • H).Φ1 = c • H.Φ1 := rfl
+@[simp] lemma real_smul_snd (c : ℝ) (H : TwoHiggsDoublet) : (c • H).Φ2 = c • H.Φ2 := rfl
+
+/-- The slice as a real-linear map from the six real field parameters
+  `(Re Φ1₀, Im Φ1₀, Re Φ2₀, Im Φ2₀, Re Φ2₁, Im Φ2₁)`. -/
+def sliceR : (Fin 6 → ℝ) →ₗ[ℝ] TwoHiggsDoublet where
+  toFun a := sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3))
+    (↑(a 4) + Complex.I * ↑(a 5))
+  map_add' a b := by
+    apply ext_of_fst_snd
+    · ext i; fin_cases i <;> simp [sliceHiggs]
+      ring
+    · ext i; fin_cases i <;> simp [sliceHiggs] <;> ring
+  map_smul' c a := by
+    apply ext_of_fst_snd
+    · ext i; fin_cases i <;> simp [sliceHiggs, Complex.real_smul]
+      ring
+    · ext i; fin_cases i <;> simp [sliceHiggs, Complex.real_smul] <;> ring
+
+@[simp] lemma sliceR_apply (a : Fin 6 → ℝ) :
+    sliceR a = sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3))
+      (↑(a 4) + Complex.I * ↑(a 5)) := rfl
+
+/-- The representative family is the real slice. -/
+lemma repHiggs_eq_sliceHiggs (X : Fin 4 → ℝ) :
+    repHiggs X = sliceHiggs (X 0) ((X 1 : ℂ) + Complex.I * (X 2 : ℂ)) (X 3) := rfl
+
+/-- Hypercharge action of the Cartan phase on the slice: it multiplies the first components by `a`
+  and the perpendicular second component by `ā`. -/
+lemma gaugeCartan_smul_sliceHiggs (a : unitary ℂ) (z w0 w1 : ℂ) :
+    GaugeGroupI.gaugeCartan a • sliceHiggs z w0 w1
+      = sliceHiggs ((a : ℂ) * z) ((a : ℂ) * w0) ((star a : ℂ) * w1) := by
+  apply ext_of_fst_snd
+  · rw [gaugeGroupI_smul_fst, GaugeGroupI.gaugeCartan_smul_eq]
+    ext i
+    fin_cases i <;> simp [Matrix.mulVec, dotProduct, Fin.sum_univ_two]
+  · rw [gaugeGroupI_smul_snd, GaugeGroupI.gaugeCartan_smul_eq]
+    ext i
+    fin_cases i <;> simp [Matrix.mulVec, dotProduct, Fin.sum_univ_two]
+
+/-- Hypercharge action of the residual `U(1)` on the slice: it multiplies the perpendicular second
+  component by `c⁶` and leaves the first components fixed. -/
+lemma ofU1Subgroup_smul_sliceHiggs (c : unitary ℂ) (z w0 w1 : ℂ) :
+    GaugeGroupI.ofU1Subgroup c • sliceHiggs z w0 w1
+      = sliceHiggs z w0 ((c : ℂ) ^ 6 * w1) := by
+  apply ext_of_fst_snd
+  · rw [gaugeGroupI_smul_fst, HiggsVec.ofU1Subgroup_smul_eq_smul]
+    ext i
+    fin_cases i <;> simp [Matrix.mulVec, dotProduct, Fin.sum_univ_two]
+  · rw [gaugeGroupI_smul_snd, HiggsVec.ofU1Subgroup_smul_eq_smul]
+    ext i
+    fin_cases i <;> simp [Matrix.mulVec, dotProduct, Fin.sum_univ_two]
+
+open Complex in
+/-- The Cartan hypercharge phase `u`, transported to a rotation of the six real field parameters:
+  it phases the first-component pairs by `u` and the perpendicular pair by `ū`. -/
+def cartanRotParam (u : unitary ℂ) (a : Fin 6 → ℝ) : Fin 6 → ℝ :=
+  ![((u : ℂ) * (↑(a 0) + I * ↑(a 1))).re, ((u : ℂ) * (↑(a 0) + I * ↑(a 1))).im,
+    ((u : ℂ) * (↑(a 2) + I * ↑(a 3))).re, ((u : ℂ) * (↑(a 2) + I * ↑(a 3))).im,
+    ((star u : ℂ) * (↑(a 4) + I * ↑(a 5))).re, ((star u : ℂ) * (↑(a 4) + I * ↑(a 5))).im]
+
+/-- Acting by the Cartan phase on a slice configuration is the same as rotating its parameters. -/
+lemma gaugeCartan_smul_sliceR (u : unitary ℂ) (a : Fin 6 → ℝ) :
+    GaugeGroupI.gaugeCartan u • sliceR a = sliceR (cartanRotParam u a) := by
+  have h : ∀ z : ℂ, (↑z.re + Complex.I * ↑z.im) = z := fun z => by
+    rw [mul_comm]; exact Complex.re_add_im z
+  rw [sliceR_apply, gaugeCartan_smul_sliceHiggs, sliceR_apply]
+  congr 1 <;> simp only [cartanRotParam, Matrix.cons_val_zero, Matrix.cons_val_one,
+    Matrix.cons_val, Fin.isValue] <;> rw [h]
+
+open Complex in
+/-- The residual `U(1)` phase `c`, transported to a rotation of the perpendicular parameter pair. -/
+def resRotParam (c : unitary ℂ) (a : Fin 6 → ℝ) : Fin 6 → ℝ :=
+  ![a 0, a 1, a 2, a 3, (((c : ℂ) ^ 6) * ((a 4 : ℂ) + I * (a 5 : ℂ))).re,
+    (((c : ℂ) ^ 6) * ((a 4 : ℂ) + I * (a 5 : ℂ))).im]
+
+/-- Acting by the residual `U(1)` on a slice configuration rotates only the perpendicular pair. -/
+lemma ofU1Subgroup_smul_sliceR (c : unitary ℂ) (a : Fin 6 → ℝ) :
+    GaugeGroupI.ofU1Subgroup c • sliceR a = sliceR (resRotParam c a) := by
+  have h : ∀ z : ℂ, (↑z.re + Complex.I * ↑z.im) = z := fun z => by
+    rw [mul_comm]; exact Complex.re_add_im z
+  rw [sliceR_apply, ofU1Subgroup_smul_sliceHiggs, sliceR_apply]
+  congr 1
+  simp only [resRotParam, Matrix.cons_val, Fin.isValue]
+  first | rfl | rw [h]
+
+end TwoHiggsDoublet

PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/GaugeTorus.lean

@@ -0,0 +1,60 @@
+/-
+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.GramMatrix
+/-!
+# The gauge torus acting on Higgs vectors
+
+The maximal torus of the gauge group acting on a Higgs doublet is the group of diagonal phase
+rotations `diag(a, b)` of the two components. We realise it using
+
+* the `SU(2)` Cartan element `diag(a, ā)` (constructed here as `gaugeCartan`), and
+* the existing `ofU1Subgroup`, whose action is `diag(1, μ)`.
+
+Together these realise an arbitrary diagonal phase `diag(a, b)`, which is the symmetry underlying
+the charge-balancing ("Condition A") of the effective potential on the orbit representatives.
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace StandardModel
+namespace GaugeGroupI
+
+open Matrix Complex
+
+/-- The Cartan `SU(2)` gauge element `diag(a, ā)`, for `a` a phase. -/
+noncomputable def gaugeCartan (a : unitary ℂ) : GaugeGroupI :=
+  (1,
+  ⟨!![(a : ℂ), 0; 0, (star a : ℂ)], by
+    have h1 : (starRingEnd ℂ) (a : ℂ) * (a : ℂ) = 1 := a.2.1
+    have h2 : (a : ℂ) * (starRingEnd ℂ) (a : ℂ) = 1 := a.2.2
+    simp only [SetLike.mem_coe]
+    rw [mem_unitaryGroup_iff']
+    funext i j
+    rw [Matrix.mul_apply]
+    fin_cases i <;> fin_cases j <;>
+      simp [Fin.sum_univ_two, h1, h2], by
+    simp only [RCLike.star_def, SetLike.mem_coe, MonoidHom.mem_mker, coe_detMonoidHom,
+      det_fin_two_of, mul_zero, sub_zero]
+    simpa using a.2.2⟩, 1)
+
+@[simp]
+lemma gaugeCartan_toU1 (a : unitary ℂ) : (gaugeCartan a).toU1 = 1 := rfl
+
+@[simp]
+lemma gaugeCartan_toSU2_coe (a : unitary ℂ) :
+    ((gaugeCartan a).toSU2 : Matrix (Fin 2) (Fin 2) ℂ) = !![(a : ℂ), 0; 0, (star a : ℂ)] := rfl
+
+/-- The Cartan element acts as the diagonal matrix `diag(a, ā)`. -/
+lemma gaugeCartan_smul_eq (a : unitary ℂ) (φ : HiggsVec) :
+    gaugeCartan a • φ = WithLp.toLp 2 (!![(a : ℂ), 0; 0, (star a : ℂ)] *ᵥ φ.ofLp) := by
+  rw [HiggsVec.gaugeGroupI_smul_eq, gaugeCartan_toU1, one_pow, one_smul, gaugeCartan_toSU2_coe]
+
+end GaugeGroupI
+end StandardModel