The gram matrix for the two Higgs doublet model

The main reference for material in this section is https://arxiv.org/pdf/hep-ph/0605184.

We will show that the gram matrix of the two Higgs doublet model describes the gauge orbits of the configuration space.

A. The Gram matrix

noncomputable def TwoHiggsDoublet.gramMatrix (H : TwoHiggsDoublet) : Matrix (Fin 2) (Fin 2) ℂ

The Gram matrix of the two Higgs doublet. This matrix is used in https://arxiv.org/abs/hep-ph/0605184.

Equations

• H.gramMatrix = !![inner ℂ H.Φ1 H.Φ1, inner ℂ H.Φ2 H.Φ1; inner ℂ H.Φ1 H.Φ2, inner ℂ H.Φ2 H.Φ2]

theorem TwoHiggsDoublet.gramMatrix_selfAdjoint (H : TwoHiggsDoublet) : IsSelfAdjoint H.gramMatrix

theorem TwoHiggsDoublet.eq_fst_norm_of_eq_gramMatrix {H1 H2 : TwoHiggsDoublet} (h : H1.gramMatrix = H2.gramMatrix) : ‖H1.Φ1‖ = ‖H2.Φ1‖

theorem TwoHiggsDoublet.eq_snd_norm_of_eq_gramMatrix {H1 H2 : TwoHiggsDoublet} (h : H1.gramMatrix = H2.gramMatrix) : ‖H1.Φ2‖ = ‖H2.Φ2‖

@[simp]

theorem TwoHiggsDoublet.gaugeGroupI_smul_gramMatrix (g : StandardModel.GaugeGroupI) (H : TwoHiggsDoublet) : (g • H).gramMatrix = H.gramMatrix

theorem TwoHiggsDoublet.gramMatrix_det_eq (H : TwoHiggsDoublet) : H.gramMatrix.det = ↑‖H.Φ1‖ ^ 2 * ↑‖H.Φ2‖ ^ 2 - ↑‖inner ℂ H.Φ1 H.Φ2‖ ^ 2

theorem TwoHiggsDoublet.gramMatrix_det_eq_real (H : TwoHiggsDoublet) : H.gramMatrix.det.re = ‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖inner ℂ H.Φ1 H.Φ2‖ ^ 2

theorem TwoHiggsDoublet.gramMatrix_det_nonneg (H : TwoHiggsDoublet) : 0 ≤ H.gramMatrix.det.re

theorem TwoHiggsDoublet.gramMatrix_tr_nonneg (H : TwoHiggsDoublet) : 0 ≤ H.gramMatrix.trace.re

theorem TwoHiggsDoublet.gaugeGroupI_exists_fst_eq {H : TwoHiggsDoublet} (h1 : H.Φ1 ≠ 0) : ∃ (g : StandardModel.GaugeGroupI), g • H.Φ1 = !₂[↑‖H.Φ1‖, 0] ∧ (g • H.Φ2).ofLp 0 = inner ℂ H.Φ1 H.Φ2 / ↑‖H.Φ1‖ ∧ ‖(g • H.Φ2).ofLp 1‖ = √H.gramMatrix.det.re / ‖H.Φ1‖

theorem TwoHiggsDoublet.gaugeGroupI_exists_fst_eq_snd_eq {H : TwoHiggsDoublet} (h1 : H.Φ1 ≠ 0) : ∃ (g : StandardModel.GaugeGroupI), g • H.Φ1 = !₂[↑‖H.Φ1‖, 0] ∧ g • H.Φ2 = !₂[inner ℂ H.Φ1 H.Φ2 / ↑‖H.Φ1‖, ↑√H.gramMatrix.det.re / ↑‖H.Φ1‖]

theorem TwoHiggsDoublet.mem_orbit_gaugeGroupI_iff_gramMatrix (H1 H2 : TwoHiggsDoublet) : H1 ∈ MulAction.orbit StandardModel.GaugeGroupI H2 ↔ H1.gramMatrix = H2.gramMatrix

A.1. Gram matrix is surjective

theorem TwoHiggsDoublet.gramMatrix_surjective_det_tr (K : Matrix (Fin 2) (Fin 2) ℂ) (hKs : IsSelfAdjoint K) (hKdet : 0 ≤ K.det.re) (hKtr : 0 ≤ K.trace.re) : ∃ (H : TwoHiggsDoublet), H.gramMatrix = K

B. The Gram vector

noncomputable def TwoHiggsDoublet.gramVector (H : TwoHiggsDoublet) : Fin 1 ⊕ Fin 3 → ℝ

A real vector containing the components of the Gram matrix in the Pauli basis.

Equations

• H.gramVector μ = 2 * (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) μ

@[simp]

theorem TwoHiggsDoublet.gaugeGroupI_smul_fst_gramVector (g : StandardModel.GaugeGroupI) (H : TwoHiggsDoublet) (μ : Fin 1 ⊕ Fin 3) : (g • H).gramVector μ = H.gramVector μ

theorem TwoHiggsDoublet.gramMatrix_eq_gramVector_sum_pauliMatrix (H : TwoHiggsDoublet) : H.gramMatrix = (1 / 2) • ∑ μ : Fin 1 ⊕ Fin 3, H.gramVector μ • PauliMatrix.pauliMatrix μ

theorem TwoHiggsDoublet.gramMatrix_eq_component_gramVector (H : TwoHiggsDoublet) : H.gramMatrix = !![1 / 2 * (↑(H.gramVector (Sum.inl 0)) + ↑(H.gramVector (Sum.inr 2))), 1 / 2 * (↑(H.gramVector (Sum.inr 0)) - Complex.I * ↑(H.gramVector (Sum.inr 1))); 1 / 2 * (↑(H.gramVector (Sum.inr 0)) + Complex.I * ↑(H.gramVector (Sum.inr 1))), 1 / 2 * (↑(H.gramVector (Sum.inl 0)) - ↑(H.gramVector (Sum.inr 2)))]

theorem TwoHiggsDoublet.gramVector_inl_eq_trace_gramMatrix (H : TwoHiggsDoublet) : H.gramVector (Sum.inl 0) = H.gramMatrix.trace.re

theorem TwoHiggsDoublet.gramVector_inl_nonneg (H : TwoHiggsDoublet) : 0 ≤ H.gramVector (Sum.inl 0)

theorem TwoHiggsDoublet.normSq_Φ1_eq_gramVector (H : TwoHiggsDoublet) : ‖H.Φ1‖ ^ 2 = 1 / 2 * (H.gramVector (Sum.inl 0) + H.gramVector (Sum.inr 2))

theorem TwoHiggsDoublet.normSq_Φ2_eq_gramVector (H : TwoHiggsDoublet) : ‖H.Φ2‖ ^ 2 = 1 / 2 * (H.gramVector (Sum.inl 0) - H.gramVector (Sum.inr 2))

theorem TwoHiggsDoublet.Φ1_inner_Φ2_eq_gramVector (H : TwoHiggsDoublet) : inner ℂ H.Φ1 H.Φ2 = ↑(1 / 2) * (↑(H.gramVector (Sum.inr 0)) + Complex.I * ↑(H.gramVector (Sum.inr 1)))

theorem TwoHiggsDoublet.Φ2_inner_Φ1_eq_gramVector (H : TwoHiggsDoublet) : inner ℂ H.Φ2 H.Φ1 = ↑(1 / 2) * (↑(H.gramVector (Sum.inr 0)) - Complex.I * ↑(H.gramVector (Sum.inr 1)))

theorem TwoHiggsDoublet.Φ1_inner_Φ2_normSq_eq_gramVector (H : TwoHiggsDoublet) : ‖inner ℂ H.Φ1 H.Φ2‖ ^ 2 = 1 / 4 * (H.gramVector (Sum.inr 0) ^ 2 + H.gramVector (Sum.inr 1) ^ 2)

theorem TwoHiggsDoublet.gramVector_inl_zero_eq (H : TwoHiggsDoublet) : H.gramVector (Sum.inl 0) = ‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2

theorem TwoHiggsDoublet.gramVector_inl_zero_eq_gramMatrix (H : TwoHiggsDoublet) : H.gramVector (Sum.inl 0) = (H.gramMatrix 0 0).re + (H.gramMatrix 1 1).re

theorem TwoHiggsDoublet.gramVector_inr_zero_eq (H : TwoHiggsDoublet) : H.gramVector (Sum.inr 0) = 2 * (inner ℂ H.Φ1 H.Φ2).re

theorem TwoHiggsDoublet.gramVector_inr_zero_eq_gramMatrix (H : TwoHiggsDoublet) : H.gramVector (Sum.inr 0) = 2 * (H.gramMatrix 1 0).re

theorem TwoHiggsDoublet.gramVector_inr_one_eq (H : TwoHiggsDoublet) : H.gramVector (Sum.inr 1) = 2 * (inner ℂ H.Φ1 H.Φ2).im

theorem TwoHiggsDoublet.gramVector_inr_one_eq_gramMatrix (H : TwoHiggsDoublet) : H.gramVector (Sum.inr 1) = 2 * (H.gramMatrix 1 0).im

theorem TwoHiggsDoublet.gramVector_inr_two_eq (H : TwoHiggsDoublet) : H.gramVector (Sum.inr 2) = ‖H.Φ1‖ ^ 2 - ‖H.Φ2‖ ^ 2

theorem TwoHiggsDoublet.gramVector_inr_two_eq_gramMatrix (H : TwoHiggsDoublet) : H.gramVector (Sum.inr 2) = (H.gramMatrix 0 0).re - (H.gramMatrix 1 1).re

theorem TwoHiggsDoublet.gramMatrix_det_eq_gramVector (H : TwoHiggsDoublet) : H.gramMatrix.det.re = 1 / 4 * (H.gramVector (Sum.inl 0) ^ 2 - ∑ μ : Fin 3, H.gramVector (Sum.inr μ) ^ 2)

theorem TwoHiggsDoublet.gramVector_inr_sum_sq_le_inl (H : TwoHiggsDoublet) : ∑ μ : Fin 3, H.gramVector (Sum.inr μ) ^ 2 ≤ H.gramVector (Sum.inl 0) ^ 2

theorem TwoHiggsDoublet.gramVector_surjective (v : Fin 1 ⊕ Fin 3 → ℝ) (h_inl : 0 ≤ v (Sum.inl 0)) (h_det : ∑ μ : Fin 3, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2) : ∃ (H : TwoHiggsDoublet), H.gramVector = v