PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.SwapDoublet

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 Mathlib.Algebra.MvPolynomial.Rename
public import Mathlib.Algebra.MvPolynomial.Degrees

Swapping the two Higgs doublets

i. Overview

Exchanging the two doublets Φ1 ↔ Φ2 is an ℝ-linear map swapDoublet that commutes with the gauge action. It therefore preserves gauge invariance and the maximum mass dimension, while turning the alignment of Φ1 into the alignment of Φ2. This is precisely the symmetry used to clear the ‖Φ2‖² factor when writing the potential through the gauge invariants, mirroring the ‖Φ1‖² clearing.

ii. Key results

swapDoublet — the doublet exchange, as an ℝ-linear map.

swapDoublet_smul — it commutes with the gauge action.

gramVector_swapDoublet_* — its effect on the Gram vector (a sign flip on the imaginary and difference components).

IsInvariant.comp_swapDoublet, HasMaxMassDimLE.comp_swapDoublet — it preserves gauge invariance and bounded mass dimension.

iii. Table of contents

A. The doublet-swap map and its components

B. Commutation with the gauge action

C. The action on the Gram vector

D. Effect on gauge invariance and mass dimension

@[expose] public section

A. The doublet-swap map and its components

Swapping the two doublets, as an ℝ-linear map. It commutes with the gauge action, so it sends gauge-invariant polynomial potentials to gauge-invariant polynomial potentials, but turns the alignment of Φ1 into the alignment of Φ2.

def swapDoublet : TwoHiggsDoublet →ₗ[ℝ] TwoHiggsDoublet where
  toFun φ := { Φ1 := φ.Φ2, Φ2 := φ.Φ1 }
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

              @[simp] lemma swapDoublet_Φ1 (φ : TwoHiggsDoublet) : (swapDoublet φ).Φ1 = φ.Φ2 := rfl@[simp] lemma swapDoublet_Φ2 (φ : TwoHiggsDoublet) : (swapDoublet φ).Φ2 = φ.Φ1 := rfl@[simp] lemma swapDoublet_swapDoublet (φ : TwoHiggsDoublet) : swapDoublet (swapDoublet φ) = φ := byφ:TwoHiggsDoublet⊢ swapDoublet (swapDoublet φ) = φ
  apply ext_of_fst_sndh1φ:TwoHiggsDoublet⊢ (swapDoublet (swapDoublet φ)).Φ1 = φ.Φ1h2φ:TwoHiggsDoublet⊢ (swapDoublet (swapDoublet φ)).Φ2 = φ.Φ2 <;>h1φ:TwoHiggsDoublet⊢ (swapDoublet (swapDoublet φ)).Φ1 = φ.Φ1h2φ:TwoHiggsDoublet⊢ (swapDoublet (swapDoublet φ)).Φ2 = φ.Φ2 rflAll goals completed! 🐙

B. Commutation with the gauge action

lemma swapDoublet_smul (g : StandardModel.GaugeGroupI) (φ : TwoHiggsDoublet) :
    swapDoublet (g • φ) = g • swapDoublet φ := byg:GaugeGroupIφ:TwoHiggsDoublet⊢ swapDoublet (g • φ) = g • swapDoublet φ
  apply ext_of_fst_sndh1g:GaugeGroupIφ:TwoHiggsDoublet⊢ (swapDoublet (g • φ)).Φ1 = (g • swapDoublet φ).Φ1h2g:GaugeGroupIφ:TwoHiggsDoublet⊢ (swapDoublet (g • φ)).Φ2 = (g • swapDoublet φ).Φ2 <;>h1g:GaugeGroupIφ:TwoHiggsDoublet⊢ (swapDoublet (g • φ)).Φ1 = (g • swapDoublet φ).Φ1h2g:GaugeGroupIφ:TwoHiggsDoublet⊢ (swapDoublet (g • φ)).Φ2 = (g • swapDoublet φ).Φ2 simpAll goals completed! 🐙

C. The action on the Gram vector

Swapping the doublets sends the gram vector through the sign flip of the imaginary and difference components.


lemma gramVector_swapDoublet_inl (φ : TwoHiggsDoublet) :
    (swapDoublet φ).gramVector (Sum.inl 0) = φ.gramVector (Sum.inl 0) := byφ:TwoHiggsDoublet⊢ (swapDoublet φ).gramVector (Sum.inl 0) = φ.gramVector (Sum.inl 0)
  rw [gramVector_inl_zero_eq,φ:TwoHiggsDoublet⊢ ‖(swapDoublet φ).Φ1‖ ^ 2 + ‖(swapDoublet φ).Φ2‖ ^ 2 = φ.gramVector (Sum.inl 0)φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 + ‖φ.Φ1‖ ^ 2 = ‖φ.Φ1‖ ^ 2 + ‖φ.Φ2‖ ^ 2 gramVector_inl_zero_eq,φ:TwoHiggsDoublet⊢ ‖(swapDoublet φ).Φ1‖ ^ 2 + ‖(swapDoublet φ).Φ2‖ ^ 2 = ‖φ.Φ1‖ ^ 2 + ‖φ.Φ2‖ ^ 2φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 + ‖φ.Φ1‖ ^ 2 = ‖φ.Φ1‖ ^ 2 + ‖φ.Φ2‖ ^ 2 swapDoublet_Φ1,φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 + ‖(swapDoublet φ).Φ2‖ ^ 2 = ‖φ.Φ1‖ ^ 2 + ‖φ.Φ2‖ ^ 2φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 + ‖φ.Φ1‖ ^ 2 = ‖φ.Φ1‖ ^ 2 + ‖φ.Φ2‖ ^ 2 swapDoublet_Φ2φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 + ‖φ.Φ1‖ ^ 2 = ‖φ.Φ1‖ ^ 2 + ‖φ.Φ2‖ ^ 2φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 + ‖φ.Φ1‖ ^ 2 = ‖φ.Φ1‖ ^ 2 + ‖φ.Φ2‖ ^ 2]φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 + ‖φ.Φ1‖ ^ 2 = ‖φ.Φ1‖ ^ 2 + ‖φ.Φ2‖ ^ 2; ringAll goals completed! 🐙

              

lemma gramVector_swapDoublet_inr0 (φ : TwoHiggsDoublet) :
    (swapDoublet φ).gramVector (Sum.inr 0) = φ.gramVector (Sum.inr 0) := byφ:TwoHiggsDoublet⊢ (swapDoublet φ).gramVector (Sum.inr 0) = φ.gramVector (Sum.inr 0)
  rw [gramVector_inr_zero_eq,φ:TwoHiggsDoublet⊢ 2 * (⟪(swapDoublet φ).Φ1, (swapDoublet φ).Φ2⟫_ℂ).re = φ.gramVector (Sum.inr 0)All goals completed! 🐙 gramVector_inr_zero_eq,φ:TwoHiggsDoublet⊢ 2 * (⟪(swapDoublet φ).Φ1, (swapDoublet φ).Φ2⟫_ℂ).re = 2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).reAll goals completed! 🐙 swapDoublet_Φ1,φ:TwoHiggsDoublet⊢ 2 * (⟪φ.Φ2, (swapDoublet φ).Φ2⟫_ℂ).re = 2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).reAll goals completed! 🐙 swapDoublet_Φ2,φ:TwoHiggsDoublet⊢ 2 * (⟪φ.Φ2, φ.Φ1⟫_ℂ).re = 2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).reAll goals completed! 🐙
    ← inner_conj_symm,φ:TwoHiggsDoublet⊢ 2 * ((starRingEnd ℂ) ⟪φ.Φ1, φ.Φ2⟫_ℂ).re = 2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).reAll goals completed! 🐙 Complex.conj_reφ:TwoHiggsDoublet⊢ 2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).re = 2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).reAll goals completed! 🐙]All goals completed! 🐙

lemma gramVector_swapDoublet_inr1 (φ : TwoHiggsDoublet) :
    (swapDoublet φ).gramVector (Sum.inr 1) = -φ.gramVector (Sum.inr 1) := byφ:TwoHiggsDoublet⊢ (swapDoublet φ).gramVector (Sum.inr 1) = -φ.gramVector (Sum.inr 1)
  rw [gramVector_inr_one_eq,φ:TwoHiggsDoublet⊢ 2 * (⟪(swapDoublet φ).Φ1, (swapDoublet φ).Φ2⟫_ℂ).im = -φ.gramVector (Sum.inr 1)φ:TwoHiggsDoublet⊢ 2 * -(⟪φ.Φ1, φ.Φ2⟫_ℂ).im = -(2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).im) gramVector_inr_one_eq,φ:TwoHiggsDoublet⊢ 2 * (⟪(swapDoublet φ).Φ1, (swapDoublet φ).Φ2⟫_ℂ).im = -(2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).im)φ:TwoHiggsDoublet⊢ 2 * -(⟪φ.Φ1, φ.Φ2⟫_ℂ).im = -(2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).im) swapDoublet_Φ1,φ:TwoHiggsDoublet⊢ 2 * (⟪φ.Φ2, (swapDoublet φ).Φ2⟫_ℂ).im = -(2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).im)φ:TwoHiggsDoublet⊢ 2 * -(⟪φ.Φ1, φ.Φ2⟫_ℂ).im = -(2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).im) swapDoublet_Φ2,φ:TwoHiggsDoublet⊢ 2 * (⟪φ.Φ2, φ.Φ1⟫_ℂ).im = -(2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).im)φ:TwoHiggsDoublet⊢ 2 * -(⟪φ.Φ1, φ.Φ2⟫_ℂ).im = -(2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).im)
    ← inner_conj_symm,φ:TwoHiggsDoublet⊢ 2 * ((starRingEnd ℂ) ⟪φ.Φ1, φ.Φ2⟫_ℂ).im = -(2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).im)φ:TwoHiggsDoublet⊢ 2 * -(⟪φ.Φ1, φ.Φ2⟫_ℂ).im = -(2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).im) Complex.conj_imφ:TwoHiggsDoublet⊢ 2 * -(⟪φ.Φ1, φ.Φ2⟫_ℂ).im = -(2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).im)φ:TwoHiggsDoublet⊢ 2 * -(⟪φ.Φ1, φ.Φ2⟫_ℂ).im = -(2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).im)]φ:TwoHiggsDoublet⊢ 2 * -(⟪φ.Φ1, φ.Φ2⟫_ℂ).im = -(2 * (⟪φ.Φ1, φ.Φ2⟫_ℂ).im); ringAll goals completed! 🐙

lemma gramVector_swapDoublet_inr2 (φ : TwoHiggsDoublet) :
    (swapDoublet φ).gramVector (Sum.inr 2) = -φ.gramVector (Sum.inr 2) := byφ:TwoHiggsDoublet⊢ (swapDoublet φ).gramVector (Sum.inr 2) = -φ.gramVector (Sum.inr 2)
  rw [gramVector_inr_two_eq,φ:TwoHiggsDoublet⊢ ‖(swapDoublet φ).Φ1‖ ^ 2 - ‖(swapDoublet φ).Φ2‖ ^ 2 = -φ.gramVector (Sum.inr 2)φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 - ‖φ.Φ1‖ ^ 2 = -(‖φ.Φ1‖ ^ 2 - ‖φ.Φ2‖ ^ 2) gramVector_inr_two_eq,φ:TwoHiggsDoublet⊢ ‖(swapDoublet φ).Φ1‖ ^ 2 - ‖(swapDoublet φ).Φ2‖ ^ 2 = -(‖φ.Φ1‖ ^ 2 - ‖φ.Φ2‖ ^ 2)φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 - ‖φ.Φ1‖ ^ 2 = -(‖φ.Φ1‖ ^ 2 - ‖φ.Φ2‖ ^ 2) swapDoublet_Φ1,φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 - ‖(swapDoublet φ).Φ2‖ ^ 2 = -(‖φ.Φ1‖ ^ 2 - ‖φ.Φ2‖ ^ 2)φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 - ‖φ.Φ1‖ ^ 2 = -(‖φ.Φ1‖ ^ 2 - ‖φ.Φ2‖ ^ 2) swapDoublet_Φ2φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 - ‖φ.Φ1‖ ^ 2 = -(‖φ.Φ1‖ ^ 2 - ‖φ.Φ2‖ ^ 2)φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 - ‖φ.Φ1‖ ^ 2 = -(‖φ.Φ1‖ ^ 2 - ‖φ.Φ2‖ ^ 2)]φ:TwoHiggsDoublet⊢ ‖φ.Φ2‖ ^ 2 - ‖φ.Φ1‖ ^ 2 = -(‖φ.Φ1‖ ^ 2 - ‖φ.Φ2‖ ^ 2); ringAll goals completed! 🐙

D. Effect on gauge invariance and mass dimension



lemma HasMaxMassDimLE.comp_swapDoublet {V : EffectivePotential} {n : ℕ}
    (h : HasMaxMassDimLE V n) : HasMaxMassDimLE (fun φ => V (swapDoublet φ)) n := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE n⊢ HasMaxMassDimLE (fun φ => V (swapDoublet φ)) n
  obtain ⟨p, hp, hdeg⟩ := hV:EffectivePotentialn:ℕp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) phdeg:p.totalDegree ≤ n⊢ HasMaxMassDimLE (fun φ => V (swapDoublet φ)) n
  refine ⟨MvPolynomial.rename
    (fun i : Module.Dual ℝ TwoHiggsDoublet => i.comp swapDoublet) p, fun φ => ?_, ?_⟩refine_1V:EffectivePotentialn:ℕp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) phdeg:p.totalDegree ≤ nφ:TwoHiggsDoublet⊢ (fun φ => V (swapDoublet φ)) φ = (MvPolynomial.eval fun i => i φ) ((MvPolynomial.rename fun i => i ∘ₗ swapDoublet) p)refine_2V:EffectivePotentialn:ℕp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) phdeg:p.totalDegree ≤ n⊢ ((MvPolynomial.rename fun i => i ∘ₗ swapDoublet) p).totalDegree ≤ n
  ·refine_1V:EffectivePotentialn:ℕp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) phdeg:p.totalDegree ≤ nφ:TwoHiggsDoublet⊢ (fun φ => V (swapDoublet φ)) φ = (MvPolynomial.eval fun i => i φ) ((MvPolynomial.rename fun i => i ∘ₗ swapDoublet) p) change V (swapDoublet φ) = _refine_1V:EffectivePotentialn:ℕp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) phdeg:p.totalDegree ≤ nφ:TwoHiggsDoublet⊢ V (swapDoublet φ) = (MvPolynomial.eval fun i => i φ) ((MvPolynomial.rename fun i => i ∘ₗ swapDoublet) p)
    rw [MvPolynomial.eval_rename,refine_1V:EffectivePotentialn:ℕp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) phdeg:p.totalDegree ≤ nφ:TwoHiggsDoublet⊢ V (swapDoublet φ) = (MvPolynomial.eval ((fun i => i φ) ∘ fun i => i ∘ₗ swapDoublet)) prefine_1V:EffectivePotentialn:ℕp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) phdeg:p.totalDegree ≤ nφ:TwoHiggsDoublet⊢ (MvPolynomial.eval fun i => i (swapDoublet φ)) p = (MvPolynomial.eval ((fun i => i φ) ∘ fun i => i ∘ₗ swapDoublet)) p hp (swapDoublet φ)refine_1V:EffectivePotentialn:ℕp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) phdeg:p.totalDegree ≤ nφ:TwoHiggsDoublet⊢ (MvPolynomial.eval fun i => i (swapDoublet φ)) p = (MvPolynomial.eval ((fun i => i φ) ∘ fun i => i ∘ₗ swapDoublet)) prefine_1V:EffectivePotentialn:ℕp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) phdeg:p.totalDegree ≤ nφ:TwoHiggsDoublet⊢ (MvPolynomial.eval fun i => i (swapDoublet φ)) p = (MvPolynomial.eval ((fun i => i φ) ∘ fun i => i ∘ₗ swapDoublet)) p]refine_1V:EffectivePotentialn:ℕp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) phdeg:p.totalDegree ≤ nφ:TwoHiggsDoublet⊢ (MvPolynomial.eval fun i => i (swapDoublet φ)) p = (MvPolynomial.eval ((fun i => i φ) ∘ fun i => i ∘ₗ swapDoublet)) p; rflAll goals completed! 🐙
  ·refine_2V:EffectivePotentialn:ℕp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) phdeg:p.totalDegree ≤ n⊢ ((MvPolynomial.rename fun i => i ∘ₗ swapDoublet) p).totalDegree ≤ n exact le_trans (MvPolynomial.totalDegree_rename_le _ _) hdegAll goals completed! 🐙



lemma IsInvariant.comp_swapDoublet {V : EffectivePotential} (hI : IsInvariant V) :
    IsInvariant (fun φ => V (swapDoublet φ)) := byV:EffectivePotentialhI:V.IsInvariant⊢ IsInvariant fun φ => V (swapDoublet φ)
  intro g φV:EffectivePotentialhI:V.IsInvariantg:GaugeGroupIφ:TwoHiggsDoublet⊢ (fun φ => V (swapDoublet φ)) (g • φ) = (fun φ => V (swapDoublet φ)) φ
  show V (swapDoublet (g • φ)) = V (swapDoublet φ)V:EffectivePotentialhI:V.IsInvariantg:GaugeGroupIφ:TwoHiggsDoublet⊢ V (swapDoublet (g • φ)) = V (swapDoublet φ)
  rw [swapDoublet_smul,V:EffectivePotentialhI:V.IsInvariantg:GaugeGroupIφ:TwoHiggsDoublet⊢ V (g • swapDoublet φ) = V (swapDoublet φ)All goals completed! 🐙 hI gV:EffectivePotentialhI:V.IsInvariantg:GaugeGroupIφ:TwoHiggsDoublet⊢ V (swapDoublet φ) = V (swapDoublet φ)All goals completed! 🐙]All goals completed! 🐙