Imports
/-
Copyright (c) 2025 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.BasicThe 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.
@[expose] public sectionA. The Gram matrix
H:TwoHiggsDoublet⊢ IsSelfAdjoint !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ]
H:TwoHiggsDoubleti:Fin 2j:Fin 2⊢ star !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] i j =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] i j
H:TwoHiggsDoubletj:Fin 2⊢ star !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩) j =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩) jH:TwoHiggsDoubletj:Fin 2⊢ star !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) j =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) j H:TwoHiggsDoubletj:Fin 2⊢ star !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩) j =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩) jH:TwoHiggsDoubletj:Fin 2⊢ star !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) j =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) j H:TwoHiggsDoublet⊢ star !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)H:TwoHiggsDoublet⊢ star !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) H:TwoHiggsDoublet⊢ star !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)H:TwoHiggsDoublet⊢ star !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)H:TwoHiggsDoublet⊢ star !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)H:TwoHiggsDoublet⊢ star !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙g:GaugeGroupIH:TwoHiggsDoublet⊢ !![⟪g • H.Φ1, g • H.Φ1⟫_ℂ, ⟪g • H.Φ2, g • H.Φ1⟫_ℂ; ⟪g • H.Φ1, g • H.Φ2⟫_ℂ, ⟪g • H.Φ2, g • H.Φ2⟫_ℂ] =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ]
g:GaugeGroupIH:TwoHiggsDoubleti:Fin 2j:Fin 2⊢ !![⟪g • H.Φ1, g • H.Φ1⟫_ℂ, ⟪g • H.Φ2, g • H.Φ1⟫_ℂ; ⟪g • H.Φ1, g • H.Φ2⟫_ℂ, ⟪g • H.Φ2, g • H.Φ2⟫_ℂ] i j =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] i j
g:GaugeGroupIH:TwoHiggsDoubletj:Fin 2⊢ !![⟪g • H.Φ1, g • H.Φ1⟫_ℂ, ⟪g • H.Φ2, g • H.Φ1⟫_ℂ; ⟪g • H.Φ1, g • H.Φ2⟫_ℂ, ⟪g • H.Φ2, g • H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩)
j =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩) jg:GaugeGroupIH:TwoHiggsDoubletj:Fin 2⊢ !![⟪g • H.Φ1, g • H.Φ1⟫_ℂ, ⟪g • H.Φ2, g • H.Φ1⟫_ℂ; ⟪g • H.Φ1, g • H.Φ2⟫_ℂ, ⟪g • H.Φ2, g • H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩)
j =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) j g:GaugeGroupIH:TwoHiggsDoubletj:Fin 2⊢ !![⟪g • H.Φ1, g • H.Φ1⟫_ℂ, ⟪g • H.Φ2, g • H.Φ1⟫_ℂ; ⟪g • H.Φ1, g • H.Φ2⟫_ℂ, ⟪g • H.Φ2, g • H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩)
j =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩) jg:GaugeGroupIH:TwoHiggsDoubletj:Fin 2⊢ !![⟪g • H.Φ1, g • H.Φ1⟫_ℂ, ⟪g • H.Φ2, g • H.Φ1⟫_ℂ; ⟪g • H.Φ1, g • H.Φ2⟫_ℂ, ⟪g • H.Φ2, g • H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩)
j =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) j g:GaugeGroupIH:TwoHiggsDoublet⊢ !![⟪g • H.Φ1, g • H.Φ1⟫_ℂ, ⟪g • H.Φ2, g • H.Φ1⟫_ℂ; ⟪g • H.Φ1, g • H.Φ2⟫_ℂ, ⟪g • H.Φ2, g • H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩)
((fun i => i) ⟨0, ⋯⟩) =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)g:GaugeGroupIH:TwoHiggsDoublet⊢ !![⟪g • H.Φ1, g • H.Φ1⟫_ℂ, ⟪g • H.Φ2, g • H.Φ1⟫_ℂ; ⟪g • H.Φ1, g • H.Φ2⟫_ℂ, ⟪g • H.Φ2, g • H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩)
((fun i => i) ⟨1, ⋯⟩) =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) g:GaugeGroupIH:TwoHiggsDoublet⊢ !![⟪g • H.Φ1, g • H.Φ1⟫_ℂ, ⟪g • H.Φ2, g • H.Φ1⟫_ℂ; ⟪g • H.Φ1, g • H.Φ2⟫_ℂ, ⟪g • H.Φ2, g • H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩)
((fun i => i) ⟨0, ⋯⟩) =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)g:GaugeGroupIH:TwoHiggsDoublet⊢ !![⟪g • H.Φ1, g • H.Φ1⟫_ℂ, ⟪g • H.Φ2, g • H.Φ1⟫_ℂ; ⟪g • H.Φ1, g • H.Φ2⟫_ℂ, ⟪g • H.Φ2, g • H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩)
((fun i => i) ⟨1, ⋯⟩) =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)g:GaugeGroupIH:TwoHiggsDoublet⊢ !![⟪g • H.Φ1, g • H.Φ1⟫_ℂ, ⟪g • H.Φ2, g • H.Φ1⟫_ℂ; ⟪g • H.Φ1, g • H.Φ2⟫_ℂ, ⟪g • H.Φ2, g • H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩)
((fun i => i) ⟨0, ⋯⟩) =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)g:GaugeGroupIH:TwoHiggsDoublet⊢ !![⟪g • H.Φ1, g • H.Φ1⟫_ℂ, ⟪g • H.Φ2, g • H.Φ1⟫_ℂ; ⟪g • H.Φ1, g • H.Φ2⟫_ℂ, ⟪g • H.Φ2, g • H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩)
((fun i => i) ⟨1, ⋯⟩) =
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) All goals completed! 🐙All goals completed! 🐙H:TwoHiggsDoublet⊢ (↑‖H.Φ1‖ ^ 2 * ↑‖H.Φ2‖ ^ 2 - ↑‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2).re = ‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2
All goals completed! 🐙H:TwoHiggsDoublet⊢ 0 ≤ ‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2
H:TwoHiggsDoublet⊢ ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2 ≤ ‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2
H:TwoHiggsDoublet⊢ ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2 = ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ * ‖⟪H.Φ2, H.Φ1⟫_ℂ‖H:TwoHiggsDoublet⊢ ‖H.Φ1‖ ^ 2 = RCLike.re ⟪H.Φ1, H.Φ1⟫_ℂH:TwoHiggsDoublet⊢ ‖H.Φ2‖ ^ 2 = RCLike.re ⟪H.Φ2, H.Φ2⟫_ℂ
H:TwoHiggsDoublet⊢ ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2 = ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ * ‖⟪H.Φ2, H.Φ1⟫_ℂ‖ All goals completed! 🐙
H:TwoHiggsDoublet⊢ ‖H.Φ1‖ ^ 2 = RCLike.re ⟪H.Φ1, H.Φ1⟫_ℂ All goals completed! 🐙
H:TwoHiggsDoublet⊢ ‖H.Φ2‖ ^ 2 = RCLike.re ⟪H.Φ2, H.Φ2⟫_ℂ All goals completed! 🐙H:TwoHiggsDoublet⊢ 0 ≤
(!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] 0 0 +
!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] 1 1).re
H:TwoHiggsDoublet⊢ 0 ≤ ‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2
All goals completed! 🐙H:TwoHiggsDoubleth1:H.Φ1 ≠ 0g:GaugeGroupIh:g • H.Φ1 = !₂[↑‖H.Φ1‖, 0]h_fst:(g • H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ↑‖H.Φ1‖hx:‖(g • H.Φ2).ofLp 0‖ ^ 2 + ‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2hx0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2 - ‖(g • H.Φ2).ofLp 0‖ ^ 2h0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2habc:∀ (a b c : ℝ), 0 ≤ a → a ^ 2 = b / c ^ 2 → c ≠ 0 → 0 < c → a = √b / c⊢ ‖H.Φ1‖ ≠ 0H:TwoHiggsDoubleth1:H.Φ1 ≠ 0g:GaugeGroupIh:g • H.Φ1 = !₂[↑‖H.Φ1‖, 0]h_fst:(g • H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ↑‖H.Φ1‖hx:‖(g • H.Φ2).ofLp 0‖ ^ 2 + ‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2hx0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2 - ‖(g • H.Φ2).ofLp 0‖ ^ 2h0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2habc:∀ (a b c : ℝ), 0 ≤ a → a ^ 2 = b / c ^ 2 → c ≠ 0 → 0 < c → a = √b / c⊢ 0 < ‖H.Φ1‖H:TwoHiggsDoubleth1:H.Φ1 ≠ 0g:GaugeGroupIh:g • H.Φ1 = !₂[↑‖H.Φ1‖, 0]h_fst:(g • H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ↑‖H.Φ1‖hx:‖(g • H.Φ2).ofLp 0‖ ^ 2 + ‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2hx0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2 - ‖(g • H.Φ2).ofLp 0‖ ^ 2h0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2habc:∀ (a b c : ℝ), 0 ≤ a → a ^ 2 = b / c ^ 2 → c ≠ 0 → 0 < c → a = √b / c⊢ 0 ≤ ‖(g • H.Φ2).ofLp 1‖
H:TwoHiggsDoubleth1:H.Φ1 ≠ 0g:GaugeGroupIh:g • H.Φ1 = !₂[↑‖H.Φ1‖, 0]h_fst:(g • H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ↑‖H.Φ1‖hx:‖(g • H.Φ2).ofLp 0‖ ^ 2 + ‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2hx0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2 - ‖(g • H.Φ2).ofLp 0‖ ^ 2h0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2habc:∀ (a b c : ℝ), 0 ≤ a → a ^ 2 = b / c ^ 2 → c ≠ 0 → 0 < c → a = √b / c⊢ ‖H.Φ1‖ ≠ 0H:TwoHiggsDoubleth1:H.Φ1 ≠ 0g:GaugeGroupIh:g • H.Φ1 = !₂[↑‖H.Φ1‖, 0]h_fst:(g • H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ↑‖H.Φ1‖hx:‖(g • H.Φ2).ofLp 0‖ ^ 2 + ‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2hx0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2 - ‖(g • H.Φ2).ofLp 0‖ ^ 2h0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2habc:∀ (a b c : ℝ), 0 ≤ a → a ^ 2 = b / c ^ 2 → c ≠ 0 → 0 < c → a = √b / c⊢ 0 < ‖H.Φ1‖H:TwoHiggsDoubleth1:H.Φ1 ≠ 0g:GaugeGroupIh:g • H.Φ1 = !₂[↑‖H.Φ1‖, 0]h_fst:(g • H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ↑‖H.Φ1‖hx:‖(g • H.Φ2).ofLp 0‖ ^ 2 + ‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2hx0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2 - ‖(g • H.Φ2).ofLp 0‖ ^ 2h0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2habc:∀ (a b c : ℝ), 0 ≤ a → a ^ 2 = b / c ^ 2 → c ≠ 0 → 0 < c → a = √b / c⊢ 0 ≤ ‖(g • H.Φ2).ofLp 1‖
H:TwoHiggsDoubleth1:H.Φ1 ≠ 0g:GaugeGroupIh:g • H.Φ1 = !₂[↑‖H.Φ1‖, 0]h_fst:(g • H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ↑‖H.Φ1‖hx:‖(g • H.Φ2).ofLp 0‖ ^ 2 + ‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2hx0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2 - ‖(g • H.Φ2).ofLp 0‖ ^ 2h0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2habc:∀ (a b c : ℝ), 0 ≤ a → a ^ 2 = b / c ^ 2 → c ≠ 0 → 0 < c → a = √b / c⊢ ‖H.Φ1‖ ≠ 0 All goals completed! 🐙
H:TwoHiggsDoubleth1:H.Φ1 ≠ 0g:GaugeGroupIh:g • H.Φ1 = !₂[↑‖H.Φ1‖, 0]h_fst:(g • H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ↑‖H.Φ1‖hx:‖(g • H.Φ2).ofLp 0‖ ^ 2 + ‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2hx0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2 - ‖(g • H.Φ2).ofLp 0‖ ^ 2h0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2habc:∀ (a b c : ℝ), 0 ≤ a → a ^ 2 = b / c ^ 2 → c ≠ 0 → 0 < c → a = √b / c⊢ 0 < ‖H.Φ1‖ All goals completed! 🐙
H:TwoHiggsDoubleth1:H.Φ1 ≠ 0g:GaugeGroupIh:g • H.Φ1 = !₂[↑‖H.Φ1‖, 0]h_fst:(g • H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ↑‖H.Φ1‖hx:‖(g • H.Φ2).ofLp 0‖ ^ 2 + ‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2hx0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2 - ‖(g • H.Φ2).ofLp 0‖ ^ 2h0:‖(g • H.Φ2).ofLp 1‖ ^ 2 = (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2habc:∀ (a b c : ℝ), 0 ≤ a → a ^ 2 = b / c ^ 2 → c ≠ 0 → 0 < c → a = √b / c⊢ 0 ≤ ‖(g • H.Φ2).ofLp 1‖ All goals completed! 🐙H:TwoHiggsDoubleth1✝:H.Φ1 ≠ 0g:GaugeGroupIh_fst:g • H.Φ1 = !₂[↑‖H.Φ1‖, 0]h_snd_0:(g • H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ↑‖H.Φ1‖h_snd_1:‖(g • H.Φ2).ofLp 1‖ = √H.gramMatrix.det.re / ‖H.Φ1‖k:GaugeGroupIh1:(k • g • H.Φ2).ofLp 1 = ↑‖(g • H.Φ2).ofLp 1‖h2:∀ (φ1 : HiggsVec), (k • φ1).ofLp 0 = φ1.ofLp 0h3:∀ (a : ℝ), k • !₂[↑a, 0] = !₂[↑a, 0]⊢ ↑(√H.gramMatrix.det.re / ‖H.Φ1‖) = ↑√H.gramMatrix.det.re / ↑‖H.Φ1‖
All goals completed! 🐙H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0⊢ H1 ∈ MulAction.orbit GaugeGroupI H2
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ H1 ∈ MulAction.orbit GaugeGroupI H2
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ (fun m => m • H2) (g1⁻¹ * g2) = H1
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ (g1⁻¹ * g2) • H2 = H1
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ((g1⁻¹ * g2) • H2).Φ1 = H1.Φ1H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ((g1⁻¹ * g2) • H2).Φ2 = H1.Φ2
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ((g1⁻¹ * g2) • H2).Φ1 = H1.Φ1 H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ g1⁻¹ • g2 • H2.Φ1 = H1.Φ1
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ g2 • H2.Φ1 = g1 • H1.Φ1
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ‖H2.Φ1‖ = ‖H1.Φ1‖
All goals completed! 🐙
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ((g1⁻¹ * g2) • H2).Φ2 = H1.Φ2 H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ g1⁻¹ • g2 • H2.Φ2 = H1.Φ2
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ g2 • H2.Φ2 = g1 • H1.Φ2
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖ = ⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖ ∧
↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖ = ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖ = ⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖ = ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖ = ⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖ H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ⟪H2.Φ1, H2.Φ2⟫_ℂ = ⟪H1.Φ1, H1.Φ2⟫_ℂH1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ↑‖H2.Φ1‖ = ↑‖H1.Φ1‖
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ⟪H2.Φ1, H2.Φ2⟫_ℂ = ⟪H1.Φ1, H1.Φ2⟫_ℂ H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ⟪H1.Φ1, H1.Φ2⟫_ℂ = ⟪H2.Φ1, H2.Φ2⟫_ℂ
All goals completed! 🐙
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ↑‖H2.Φ1‖ = ↑‖H1.Φ1‖ H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ‖H2.Φ1‖ = ‖H1.Φ1‖
All goals completed! 🐙
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖ = ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖ H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ √H2.gramMatrix.det.re = √H1.gramMatrix.det.reH1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ‖H2.Φ1‖ = ‖H1.Φ1‖
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ √H2.gramMatrix.det.re = √H1.gramMatrix.det.re All goals completed! 🐙
H1:TwoHiggsDoubletH2:TwoHiggsDoubletΦ1_zero:¬H1.Φ1 = 0h:H1.gramMatrix = H2.gramMatrixg1:GaugeGroupIH1_Φ1:g1 • H1.Φ1 = !₂[↑‖H1.Φ1‖, 0]H1_Φ2:g1 • H1.Φ2 = !₂[⟪H1.Φ1, H1.Φ2⟫_ℂ / ↑‖H1.Φ1‖, ↑√H1.gramMatrix.det.re / ↑‖H1.Φ1‖]Φ2_nezero:H2.Φ1 ≠ 0g2:GaugeGroupIH2_Φ1:g2 • H2.Φ1 = !₂[↑‖H2.Φ1‖, 0]H2_Φ2:g2 • H2.Φ2 = !₂[⟪H2.Φ1, H2.Φ2⟫_ℂ / ↑‖H2.Φ1‖, ↑√H2.gramMatrix.det.re / ↑‖H2.Φ1‖]⊢ ‖H2.Φ1‖ = ‖H1.Φ1‖ All goals completed! 🐙A.1. Gram matrix is surjective
K:Matrix (Fin 2) (Fin 2) ℂa:ℝb:ℝhKtr:0 ≤ a + bc:ℂhKdet:‖c‖ ^ 2 ≤ a * bha_nonneg:0 ≤ ahb_nonneg:0 ≤ bha:¬a = 0h1:↑√a ≠ 0hD:0 ≤ a * b - ‖c‖ ^ 2⊢ ‖c‖ ^ 2 / a + (a * b - ‖c‖ ^ 2) / a = b
K:Matrix (Fin 2) (Fin 2) ℂa:ℝb:ℝhKtr:0 ≤ a + bc:ℂhKdet:‖c‖ ^ 2 ≤ a * bha_nonneg:0 ≤ ahb_nonneg:0 ≤ bha:¬a = 0h1:↑√a ≠ 0hD:0 ≤ a * b - ‖c‖ ^ 2⊢ ‖c‖ ^ 2 + (a * b - ‖c‖ ^ 2) = a * b
All goals completed! 🐙B. The Gram vector
The lemma manifesting the definitional equality for the gramVector.
lemma gramVector_eq (H : TwoHiggsDoublet) : H.gramVector = fun μ =>
2 * PauliMatrix.pauliBasis.repr ⟨gramMatrix H, gramMatrix_selfAdjoint H⟩ μ := rflg:GaugeGroupIH:TwoHiggsDoubletμ:Fin 1 ⊕ Fin 3⊢ 2 * (PauliMatrix.pauliBasis.repr ⟨(g • H).gramMatrix, ⋯⟩) μ = 2 * (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) μ
g:GaugeGroupIH:TwoHiggsDoubletμ:Fin 1 ⊕ Fin 3⊢ (PauliMatrix.pauliBasis.repr ⟨(g • H).gramMatrix, ⋯⟩) μ = (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) μ
All goals completed! 🐙H:TwoHiggsDoubleth1:(PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • ↑(PauliMatrix.pauliBasis (Sum.inl 0)) +
∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • ↑(PauliMatrix.pauliBasis (Sum.inr x)) =
H.gramMatrix⊢ (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • ↑(PauliMatrix.pauliBasis (Sum.inl 0)) +
∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • ↑(PauliMatrix.pauliBasis (Sum.inr x)) =
(1 / 2) • ∑ μ, H.gramVector μ • PauliMatrix.pauliMatrix μ
H:TwoHiggsDoubleth1:(PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • ↑(PauliMatrix.pauliBasis (Sum.inl 0)) +
∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • ↑(PauliMatrix.pauliBasis (Sum.inr x)) =
H.gramMatrix⊢ (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • ↑(PauliMatrix.pauliBasis (Sum.inl 0)) +
∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • ↑(PauliMatrix.pauliBasis (Sum.inr x)) =
(PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • PauliMatrix.pauliMatrix (Sum.inl 0) +
∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • PauliMatrix.pauliMatrix (Sum.inr x)
H:TwoHiggsDoubleth1:(PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • ↑(PauliMatrix.pauliBasis (Sum.inl 0)) +
∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • ↑(PauliMatrix.pauliBasis (Sum.inr x)) =
H.gramMatrix⊢ (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • ↑(PauliMatrix.pauliBasis (Sum.inl 0)) =
(PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • PauliMatrix.pauliMatrix (Sum.inl 0)H:TwoHiggsDoubleth1:(PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • ↑(PauliMatrix.pauliBasis (Sum.inl 0)) +
∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • ↑(PauliMatrix.pauliBasis (Sum.inr x)) =
H.gramMatrix⊢ ∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • ↑(PauliMatrix.pauliBasis (Sum.inr x)) =
∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • PauliMatrix.pauliMatrix (Sum.inr x) H:TwoHiggsDoubleth1:(PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • ↑(PauliMatrix.pauliBasis (Sum.inl 0)) +
∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • ↑(PauliMatrix.pauliBasis (Sum.inr x)) =
H.gramMatrix⊢ (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • ↑(PauliMatrix.pauliBasis (Sum.inl 0)) =
(PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • PauliMatrix.pauliMatrix (Sum.inl 0)H:TwoHiggsDoubleth1:(PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inl 0) • ↑(PauliMatrix.pauliBasis (Sum.inl 0)) +
∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • ↑(PauliMatrix.pauliBasis (Sum.inr x)) =
H.gramMatrix⊢ ∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • ↑(PauliMatrix.pauliBasis (Sum.inr x)) =
∑ x, (PauliMatrix.pauliBasis.repr ⟨H.gramMatrix, ⋯⟩) (Sum.inr x) • PauliMatrix.pauliMatrix (Sum.inr x) All goals completed! 🐙H:TwoHiggsDoublet⊢ (1 / 2) • ∑ μ, H.gramVector μ • PauliMatrix.pauliMatrix μ =
!![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)))]
H:TwoHiggsDoublet⊢ (2⁻¹ * ↑(H.gramVector (Sum.inl 0)) + 2⁻¹ * ↑(H.gramVector (Sum.inr 2)) =
2⁻¹ * (↑(H.gramVector (Sum.inl 0)) + ↑(H.gramVector (Sum.inr 2))) ∧
2⁻¹ * ↑(H.gramVector (Sum.inr 0)) + -(2⁻¹ * (↑(H.gramVector (Sum.inr 1)) * Complex.I)) =
2⁻¹ * (↑(H.gramVector (Sum.inr 0)) - Complex.I * ↑(H.gramVector (Sum.inr 1)))) ∧
2⁻¹ * ↑(H.gramVector (Sum.inr 0)) + 2⁻¹ * (↑(H.gramVector (Sum.inr 1)) * Complex.I) =
2⁻¹ * (↑(H.gramVector (Sum.inr 0)) + Complex.I * ↑(H.gramVector (Sum.inr 1))) ∧
2⁻¹ * ↑(H.gramVector (Sum.inl 0)) + -(2⁻¹ * ↑(H.gramVector (Sum.inr 2))) =
2⁻¹ * (↑(H.gramVector (Sum.inl 0)) - ↑(H.gramVector (Sum.inr 2)))
H:TwoHiggsDoublet⊢ (True ∧ True) ∧ True ∧ True
All goals completed! 🐙H:TwoHiggsDoublet⊢ H.gramVector (Sum.inl 0) =
(!![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)))]
0 0 +
!![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)))]
1 1).re
H:TwoHiggsDoublet⊢ H.gramVector (Sum.inl 0) =
2⁻¹ * (H.gramVector (Sum.inl 0) + H.gramVector (Sum.inr 2)) +
2⁻¹ * (H.gramVector (Sum.inl 0) - H.gramVector (Sum.inr 2))
All goals completed! 🐙H:TwoHiggsDoublet⊢ 0 ≤ H.gramMatrix.trace.re
All goals completed! 🐙H:TwoHiggsDoublet⊢ (!![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)))]
0 0).re =
1 / 2 * (H.gramVector (Sum.inl 0) + H.gramVector (Sum.inr 2))
All goals completed! 🐙H:TwoHiggsDoublet⊢ (!![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)))]
1 1).re =
1 / 2 * (H.gramVector (Sum.inl 0) - H.gramVector (Sum.inr 2))
All goals completed! 🐙lemma Φ1_inner_Φ2_eq_gramVector (H : TwoHiggsDoublet) :
(⟪H.Φ1, H.Φ2⟫_ℂ) = (1/2 : ℝ) * (H.gramVector (Sum.inr 0) +
Complex.I * H.gramVector (Sum.inr 1)) := H:TwoHiggsDoublet⊢ ⟪H.Φ1, H.Φ2⟫_ℂ = ↑(1 / 2) * (↑(H.gramVector (Sum.inr 0)) + Complex.I * ↑(H.gramVector (Sum.inr 1)))
H:TwoHiggsDoublet⊢ ⟪H.Φ1, H.Φ2⟫_ℂ = H.gramMatrix 1 0H:TwoHiggsDoublet⊢ H.gramMatrix 1 0 = ↑(1 / 2) * (↑(H.gramVector (Sum.inr 0)) + Complex.I * ↑(H.gramVector (Sum.inr 1)))
H:TwoHiggsDoublet⊢ ⟪H.Φ1, H.Φ2⟫_ℂ = H.gramMatrix 1 0 All goals completed! 🐙
H:TwoHiggsDoublet⊢ H.gramMatrix 1 0 = ↑(1 / 2) * (↑(H.gramVector (Sum.inr 0)) + Complex.I * ↑(H.gramVector (Sum.inr 1))) All goals completed! 🐙lemma Φ2_inner_Φ1_eq_gramVector (H : TwoHiggsDoublet) :
(⟪H.Φ2, H.Φ1⟫_ℂ) = (1/2 : ℝ) * (H.gramVector (Sum.inr 0) -
Complex.I * H.gramVector (Sum.inr 1)) := H:TwoHiggsDoublet⊢ ⟪H.Φ2, H.Φ1⟫_ℂ = ↑(1 / 2) * (↑(H.gramVector (Sum.inr 0)) - Complex.I * ↑(H.gramVector (Sum.inr 1)))
H:TwoHiggsDoublet⊢ ⟪H.Φ2, H.Φ1⟫_ℂ = H.gramMatrix 0 1H:TwoHiggsDoublet⊢ H.gramMatrix 0 1 = ↑(1 / 2) * (↑(H.gramVector (Sum.inr 0)) - Complex.I * ↑(H.gramVector (Sum.inr 1)))
H:TwoHiggsDoublet⊢ ⟪H.Φ2, H.Φ1⟫_ℂ = H.gramMatrix 0 1 All goals completed! 🐙
H:TwoHiggsDoublet⊢ H.gramMatrix 0 1 = ↑(1 / 2) * (↑(H.gramVector (Sum.inr 0)) - Complex.I * ↑(H.gramVector (Sum.inr 1))) All goals completed! 🐙H:TwoHiggsDoublet⊢ (↑(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))))).re =
1 / 4 * (H.gramVector (Sum.inr 0) ^ 2 + H.gramVector (Sum.inr 1) ^ 2)
H:TwoHiggsDoublet⊢ 2⁻¹ * H.gramVector (Sum.inr 0) * (2⁻¹ * H.gramVector (Sum.inr 0)) +
2⁻¹ * H.gramVector (Sum.inr 1) * (2⁻¹ * H.gramVector (Sum.inr 1)) =
4⁻¹ * (H.gramVector (Sum.inr 0) ^ 2 + H.gramVector (Sum.inr 1) ^ 2)
All goals completed! 🐙H:TwoHiggsDoublet⊢ H.gramVector (Sum.inl 0) =
1 / 2 * (H.gramVector (Sum.inl 0) + H.gramVector (Sum.inr 2)) +
1 / 2 * (H.gramVector (Sum.inl 0) - H.gramVector (Sum.inr 2))
All goals completed! 🐙lemma gramVector_inl_zero_eq_gramMatrix (H : TwoHiggsDoublet) :
H.gramVector (Sum.inl 0) = (H.gramMatrix 0 0).re + (H.gramMatrix 1 1).re := H:TwoHiggsDoublet⊢ H.gramVector (Sum.inl 0) = (H.gramMatrix 0 0).re + (H.gramMatrix 1 1).re
All goals completed! 🐙H:TwoHiggsDoublet⊢ H.gramVector (Sum.inr 0) = 2 * (↑(1 / 2) * (↑(H.gramVector (Sum.inr 0)) + Complex.I * ↑(H.gramVector (Sum.inr 1)))).re
All goals completed! 🐙H:TwoHiggsDoublet⊢ 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re = 2 * (!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] 1 0).re
All goals completed! 🐙H:TwoHiggsDoublet⊢ H.gramVector (Sum.inr 1) = 2 * (↑(1 / 2) * (↑(H.gramVector (Sum.inr 0)) + Complex.I * ↑(H.gramVector (Sum.inr 1)))).im
All goals completed! 🐙H:TwoHiggsDoublet⊢ 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im = 2 * (!![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ] 1 0).im
All goals completed! 🐙H:TwoHiggsDoublet⊢ H.gramVector (Sum.inr 2) =
1 / 2 * (H.gramVector (Sum.inl 0) + H.gramVector (Sum.inr 2)) -
1 / 2 * (H.gramVector (Sum.inl 0) - H.gramVector (Sum.inr 2))
All goals completed! 🐙lemma gramVector_inr_two_eq_gramMatrix (H : TwoHiggsDoublet) :
H.gramVector (Sum.inr 2) = (H.gramMatrix 0 0).re - (H.gramMatrix 1 1).re := H:TwoHiggsDoublet⊢ H.gramVector (Sum.inr 2) = (H.gramMatrix 0 0).re - (H.gramMatrix 1 1).re
All goals completed! 🐙H:TwoHiggsDoublet⊢ ‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2 =
1 / 4 * (H.gramVector (Sum.inl 0) ^ 2 - ∑ μ, H.gramVector (Sum.inr μ) ^ 2)
H:TwoHiggsDoublet⊢ 2⁻¹ * (H.gramVector (Sum.inl 0) + H.gramVector (Sum.inr 2)) *
(2⁻¹ * (H.gramVector (Sum.inl 0) - H.gramVector (Sum.inr 2))) -
4⁻¹ * (H.gramVector (Sum.inr 0) ^ 2 + H.gramVector (Sum.inr 1) ^ 2) =
4⁻¹ *
(H.gramVector (Sum.inl 0) ^ 2 -
(H.gramVector (Sum.inr 0) ^ 2 + H.gramVector (Sum.inr 1) ^ 2 + H.gramVector (Sum.inr 2) ^ 2))
All goals completed! 🐙H:TwoHiggsDoubleth:0 ≤ 1 / 4 * (H.gramVector (Sum.inl 0) ^ 2 - ∑ μ, H.gramVector (Sum.inr μ) ^ 2)⊢ ∑ μ, H.gramVector (Sum.inr μ) ^ 2 ≤ H.gramVector (Sum.inl 0) ^ 2
All goals completed! 🐙v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.re⊢ ∃ H, H.gramVector = v
v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = K⊢ ∃ H, H.gramVector = v
v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = K⊢ H.gramVector = v
v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = Kμ:Fin 1 ⊕ Fin 3⊢ H.gramVector μ = v μ
v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = K⊢ H.gramVector (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) = v (Sum.inl ((fun i => i) ⟨0, ⋯⟩))v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = K⊢ H.gramVector (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) = v (Sum.inr ((fun i => i) ⟨0, ⋯⟩))v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = K⊢ H.gramVector (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) = v (Sum.inr ((fun i => i) ⟨1, ⋯⟩))v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = K⊢ H.gramVector (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) = v (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = K⊢ H.gramVector (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) = v (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = K⊢ 2⁻¹ * (v (Sum.inl 0) + v (Sum.inr 2)) + 2⁻¹ * (v (Sum.inl 0) - v (Sum.inr 2)) = v (Sum.inl 0)
All goals completed! 🐙
v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = K⊢ H.gramVector (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) = v (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) All goals completed! 🐙
v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = K⊢ H.gramVector (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) = v (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) All goals completed! 🐙
v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = K⊢ H.gramVector (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) = v (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) v:Fin 1 ⊕ Fin 3 → ℝh_inl:0 ≤ v (Sum.inl 0)h_det:∑ μ, v (Sum.inr μ) ^ 2 ≤ v (Sum.inl 0) ^ 2K:Matrix (Fin 2) (Fin 2) ℂ :=
!![1 / 2 * (↑(v (Sum.inl 0)) + ↑(v (Sum.inr 2))), 1 / 2 * (↑(v (Sum.inr 0)) - Complex.I * ↑(v (Sum.inr 1)));
1 / 2 * (↑(v (Sum.inr 0)) + Complex.I * ↑(v (Sum.inr 1))), 1 / 2 * (↑(v (Sum.inl 0)) - ↑(v (Sum.inr 2)))]hK_selfAdjoint:IsSelfAdjoint KhK_det_nonneg:0 ≤ K.det.rehK_tr:0 ≤ K.trace.reH:TwoHiggsDoublethH:H.gramMatrix = K⊢ 2⁻¹ * (v (Sum.inl 0) + v (Sum.inr 2)) - 2⁻¹ * (v (Sum.inl 0) - v (Sum.inr 2)) = v (Sum.inr 2)
All goals completed! 🐙All goals completed! 🐙