PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.GaugeSlice

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.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

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 := !2[z, 0]
  Φ2 := !2[w0, w1]

              @[simp] lemma sliceHiggs_Φ1 (z w0 w1 : ℂ) : (sliceHiggs z w0 w1).Φ1 = !2[z, 0] := rfl@[simp] lemma sliceHiggs_Φ2 (z w0 w1 : ℂ) : (sliceHiggs z w0 w1).Φ2 = !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 := bya:Fin 6 → ℝb:Fin 6 → ℝ⊢ sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
    (↑((a + b) 4) + Complex.I * ↑((a + b) 5)) =
  sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
    sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))
    apply ext_of_fst_sndh1a:Fin 6 → ℝb:Fin 6 → ℝ⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
      (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ1 =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
      sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ1h2a:Fin 6 → ℝb:Fin 6 → ℝ⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
      (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ2 =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
      sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ2
    ·h1a:Fin 6 → ℝb:Fin 6 → ℝ⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
      (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ1 =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
      sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ1 ext ih1a:Fin 6 → ℝb:Fin 6 → ℝi:Fin 2⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
          (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ1.ofLp
    i =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
          sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ1.ofLp
    i; fin_cases ih1.«0»a:Fin 6 → ℝb:Fin 6 → ℝ⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
          (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ1.ofLp
    ((fun i => i) ⟨0, ⋯⟩) =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
          sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ1.ofLp
    ((fun i => i) ⟨0, ⋯⟩)h1.«1»a:Fin 6 → ℝb:Fin 6 → ℝ⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
          (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ1.ofLp
    ((fun i => i) ⟨1, ⋯⟩) =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
          sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ1.ofLp
    ((fun i => i) ⟨1, ⋯⟩) <;>h1.«0»a:Fin 6 → ℝb:Fin 6 → ℝ⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
          (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ1.ofLp
    ((fun i => i) ⟨0, ⋯⟩) =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
          sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ1.ofLp
    ((fun i => i) ⟨0, ⋯⟩)h1.«1»a:Fin 6 → ℝb:Fin 6 → ℝ⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
          (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ1.ofLp
    ((fun i => i) ⟨1, ⋯⟩) =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
          sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ1.ofLp
    ((fun i => i) ⟨1, ⋯⟩) simp [sliceHiggs]All goals completed! 🐙
      ringAll goals completed! 🐙
    ·h2a:Fin 6 → ℝb:Fin 6 → ℝ⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
      (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ2 =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
      sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ2 ext ih2a:Fin 6 → ℝb:Fin 6 → ℝi:Fin 2⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
          (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ2.ofLp
    i =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
          sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ2.ofLp
    i; fin_cases ih2.«0»a:Fin 6 → ℝb:Fin 6 → ℝ⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
          (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ2.ofLp
    ((fun i => i) ⟨0, ⋯⟩) =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
          sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ2.ofLp
    ((fun i => i) ⟨0, ⋯⟩)h2.«1»a:Fin 6 → ℝb:Fin 6 → ℝ⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
          (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ2.ofLp
    ((fun i => i) ⟨1, ⋯⟩) =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
          sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ2.ofLp
    ((fun i => i) ⟨1, ⋯⟩) <;>h2.«0»a:Fin 6 → ℝb:Fin 6 → ℝ⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
          (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ2.ofLp
    ((fun i => i) ⟨0, ⋯⟩) =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
          sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ2.ofLp
    ((fun i => i) ⟨0, ⋯⟩)h2.«1»a:Fin 6 → ℝb:Fin 6 → ℝ⊢ (sliceHiggs (↑((a + b) 0) + Complex.I * ↑((a + b) 1)) (↑((a + b) 2) + Complex.I * ↑((a + b) 3))
          (↑((a + b) 4) + Complex.I * ↑((a + b) 5))).Φ2.ofLp
    ((fun i => i) ⟨1, ⋯⟩) =
  (sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) +
          sliceHiggs (↑(b 0) + Complex.I * ↑(b 1)) (↑(b 2) + Complex.I * ↑(b 3)) (↑(b 4) + Complex.I * ↑(b 5))).Φ2.ofLp
    ((fun i => i) ⟨1, ⋯⟩) simp [sliceHiggs]h2.«1»a:Fin 6 → ℝb:Fin 6 → ℝ⊢ ↑(a 4) + ↑(b 4) + Complex.I * (↑(a 5) + ↑(b 5)) = ↑(a 4) + Complex.I * ↑(a 5) + (↑(b 4) + Complex.I * ↑(b 5)) <;>h2.«0»a:Fin 6 → ℝb:Fin 6 → ℝ⊢ ↑(a 2) + ↑(b 2) + Complex.I * (↑(a 3) + ↑(b 3)) = ↑(a 2) + Complex.I * ↑(a 3) + (↑(b 2) + Complex.I * ↑(b 3))h2.«1»a:Fin 6 → ℝb:Fin 6 → ℝ⊢ ↑(a 4) + ↑(b 4) + Complex.I * (↑(a 5) + ↑(b 5)) = ↑(a 4) + Complex.I * ↑(a 5) + (↑(b 4) + Complex.I * ↑(b 5)) ringAll goals completed! 🐙
  map_smul' c a := byc:ℝa:Fin 6 → ℝ⊢ sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
    (↑((c • a) 4) + Complex.I * ↑((c • a) 5)) =
  (RingHom.id ℝ) c •
    sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))
    apply ext_of_fst_sndh1c:ℝa:Fin 6 → ℝ⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
      (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ1 =
  ((RingHom.id ℝ) c •
      sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ1h2c:ℝa:Fin 6 → ℝ⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
      (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ2 =
  ((RingHom.id ℝ) c •
      sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ2
    ·h1c:ℝa:Fin 6 → ℝ⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
      (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ1 =
  ((RingHom.id ℝ) c •
      sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ1 ext ih1c:ℝa:Fin 6 → ℝi:Fin 2⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
          (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ1.ofLp
    i =
  ((RingHom.id ℝ) c •
          sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ1.ofLp
    i; fin_cases ih1.«0»c:ℝa:Fin 6 → ℝ⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
          (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ1.ofLp
    ((fun i => i) ⟨0, ⋯⟩) =
  ((RingHom.id ℝ) c •
          sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ1.ofLp
    ((fun i => i) ⟨0, ⋯⟩)h1.«1»c:ℝa:Fin 6 → ℝ⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
          (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ1.ofLp
    ((fun i => i) ⟨1, ⋯⟩) =
  ((RingHom.id ℝ) c •
          sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ1.ofLp
    ((fun i => i) ⟨1, ⋯⟩) <;>h1.«0»c:ℝa:Fin 6 → ℝ⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
          (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ1.ofLp
    ((fun i => i) ⟨0, ⋯⟩) =
  ((RingHom.id ℝ) c •
          sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ1.ofLp
    ((fun i => i) ⟨0, ⋯⟩)h1.«1»c:ℝa:Fin 6 → ℝ⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
          (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ1.ofLp
    ((fun i => i) ⟨1, ⋯⟩) =
  ((RingHom.id ℝ) c •
          sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ1.ofLp
    ((fun i => i) ⟨1, ⋯⟩) simp [sliceHiggs, Complex.real_smul]All goals completed! 🐙
      ringAll goals completed! 🐙
    ·h2c:ℝa:Fin 6 → ℝ⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
      (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ2 =
  ((RingHom.id ℝ) c •
      sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ2 ext ih2c:ℝa:Fin 6 → ℝi:Fin 2⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
          (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ2.ofLp
    i =
  ((RingHom.id ℝ) c •
          sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ2.ofLp
    i; fin_cases ih2.«0»c:ℝa:Fin 6 → ℝ⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
          (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ2.ofLp
    ((fun i => i) ⟨0, ⋯⟩) =
  ((RingHom.id ℝ) c •
          sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ2.ofLp
    ((fun i => i) ⟨0, ⋯⟩)h2.«1»c:ℝa:Fin 6 → ℝ⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
          (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ2.ofLp
    ((fun i => i) ⟨1, ⋯⟩) =
  ((RingHom.id ℝ) c •
          sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ2.ofLp
    ((fun i => i) ⟨1, ⋯⟩) <;>h2.«0»c:ℝa:Fin 6 → ℝ⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
          (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ2.ofLp
    ((fun i => i) ⟨0, ⋯⟩) =
  ((RingHom.id ℝ) c •
          sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ2.ofLp
    ((fun i => i) ⟨0, ⋯⟩)h2.«1»c:ℝa:Fin 6 → ℝ⊢ (sliceHiggs (↑((c • a) 0) + Complex.I * ↑((c • a) 1)) (↑((c • a) 2) + Complex.I * ↑((c • a) 3))
          (↑((c • a) 4) + Complex.I * ↑((c • a) 5))).Φ2.ofLp
    ((fun i => i) ⟨1, ⋯⟩) =
  ((RingHom.id ℝ) c •
          sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5))).Φ2.ofLp
    ((fun i => i) ⟨1, ⋯⟩) simp [sliceHiggs, Complex.real_smul]h2.«1»c:ℝa:Fin 6 → ℝ⊢ Complex.I * (↑c * ↑(a 5)) = ↑c * (Complex.I * ↑(a 5)) <;>h2.«0»c:ℝa:Fin 6 → ℝ⊢ Complex.I * (↑c * ↑(a 3)) = ↑c * (Complex.I * ↑(a 3))h2.«1»c:ℝa:Fin 6 → ℝ⊢ Complex.I * (↑c * ↑(a 5)) = ↑c * (Complex.I * ↑(a 5)) ringAll goals completed! 🐙

@[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) := bya:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ GaugeGroupI.gaugeCartan a • sliceHiggs z w0 w1 = sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)
  apply ext_of_fst_sndh1a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (GaugeGroupI.gaugeCartan a • sliceHiggs z w0 w1).Φ1 = (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ1h2a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (GaugeGroupI.gaugeCartan a • sliceHiggs z w0 w1).Φ2 = (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ2
  ·h1a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (GaugeGroupI.gaugeCartan a • sliceHiggs z w0 w1).Φ1 = (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ1 rw [gaugeGroupI_smul_fst,h1a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ GaugeGroupI.gaugeCartan a • (sliceHiggs z w0 w1).Φ1 = (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ1h1a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ1.ofLp) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ1 GaugeGroupI.gaugeCartan_smul_eqh1a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ1.ofLp) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ1h1a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ1.ofLp) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ1]h1a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ1.ofLp) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ1
    ext ih1a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂi:Fin 2⊢ (WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ1.ofLp)).ofLp i =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ1.ofLp i
    fin_cases ih1.«0»a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ1.ofLp)).ofLp ((fun i => i) ⟨0, ⋯⟩) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ1.ofLp ((fun i => i) ⟨0, ⋯⟩)h1.«1»a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ1.ofLp)).ofLp ((fun i => i) ⟨1, ⋯⟩) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ1.ofLp ((fun i => i) ⟨1, ⋯⟩) <;>h1.«0»a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ1.ofLp)).ofLp ((fun i => i) ⟨0, ⋯⟩) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ1.ofLp ((fun i => i) ⟨0, ⋯⟩)h1.«1»a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ1.ofLp)).ofLp ((fun i => i) ⟨1, ⋯⟩) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ1.ofLp ((fun i => i) ⟨1, ⋯⟩) simp [Matrix.mulVec, dotProduct, Fin.sum_univ_two]All goals completed! 🐙
  ·h2a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (GaugeGroupI.gaugeCartan a • sliceHiggs z w0 w1).Φ2 = (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ2 rw [gaugeGroupI_smul_snd,h2a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ GaugeGroupI.gaugeCartan a • (sliceHiggs z w0 w1).Φ2 = (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ2h2a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ2.ofLp) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ2 GaugeGroupI.gaugeCartan_smul_eqh2a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ2.ofLp) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ2h2a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ2.ofLp) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ2]h2a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ2.ofLp) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ2
    ext ih2a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂi:Fin 2⊢ (WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ2.ofLp)).ofLp i =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ2.ofLp i
    fin_cases ih2.«0»a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ2.ofLp)).ofLp ((fun i => i) ⟨0, ⋯⟩) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ2.ofLp ((fun i => i) ⟨0, ⋯⟩)h2.«1»a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ2.ofLp)).ofLp ((fun i => i) ⟨1, ⋯⟩) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ2.ofLp ((fun i => i) ⟨1, ⋯⟩) <;>h2.«0»a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ2.ofLp)).ofLp ((fun i => i) ⟨0, ⋯⟩) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ2.ofLp ((fun i => i) ⟨0, ⋯⟩)h2.«1»a:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![↑a, 0; 0, star ↑a].mulVec (sliceHiggs z w0 w1).Φ2.ofLp)).ofLp ((fun i => i) ⟨1, ⋯⟩) =
  (sliceHiggs (↑a * z) (↑a * w0) (star ↑a * w1)).Φ2.ofLp ((fun i => i) ⟨1, ⋯⟩) simp [Matrix.mulVec, dotProduct, Fin.sum_univ_two]All goals completed! 🐙

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) := byc:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ GaugeGroupI.ofU1Subgroup c • sliceHiggs z w0 w1 = sliceHiggs z w0 (↑c ^ 6 * w1)
  apply ext_of_fst_sndh1c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (GaugeGroupI.ofU1Subgroup c • sliceHiggs z w0 w1).Φ1 = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ1h2c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (GaugeGroupI.ofU1Subgroup c • sliceHiggs z w0 w1).Φ2 = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ2
  ·h1c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (GaugeGroupI.ofU1Subgroup c • sliceHiggs z w0 w1).Φ1 = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ1 rw [gaugeGroupI_smul_fst,h1c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ GaugeGroupI.ofU1Subgroup c • (sliceHiggs z w0 w1).Φ1 = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ1h1c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ1.ofLp) = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ1 HiggsVec.ofU1Subgroup_smul_eq_smulh1c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ1.ofLp) = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ1h1c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ1.ofLp) = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ1]h1c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ1.ofLp) = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ1
    ext ih1c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂi:Fin 2⊢ (WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ1.ofLp)).ofLp i =
  (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ1.ofLp i
    fin_cases ih1.«0»c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ1.ofLp)).ofLp ((fun i => i) ⟨0, ⋯⟩) =
  (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ1.ofLp ((fun i => i) ⟨0, ⋯⟩)h1.«1»c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ1.ofLp)).ofLp ((fun i => i) ⟨1, ⋯⟩) =
  (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ1.ofLp ((fun i => i) ⟨1, ⋯⟩) <;>h1.«0»c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ1.ofLp)).ofLp ((fun i => i) ⟨0, ⋯⟩) =
  (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ1.ofLp ((fun i => i) ⟨0, ⋯⟩)h1.«1»c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ1.ofLp)).ofLp ((fun i => i) ⟨1, ⋯⟩) =
  (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ1.ofLp ((fun i => i) ⟨1, ⋯⟩) simp [Matrix.mulVec, dotProduct, Fin.sum_univ_two]All goals completed! 🐙
  ·h2c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (GaugeGroupI.ofU1Subgroup c • sliceHiggs z w0 w1).Φ2 = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ2 rw [gaugeGroupI_smul_snd,h2c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ GaugeGroupI.ofU1Subgroup c • (sliceHiggs z w0 w1).Φ2 = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ2h2c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ2.ofLp) = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ2 HiggsVec.ofU1Subgroup_smul_eq_smulh2c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ2.ofLp) = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ2h2c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ2.ofLp) = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ2]h2c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ2.ofLp) = (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ2
    ext ih2c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂi:Fin 2⊢ (WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ2.ofLp)).ofLp i =
  (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ2.ofLp i
    fin_cases ih2.«0»c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ2.ofLp)).ofLp ((fun i => i) ⟨0, ⋯⟩) =
  (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ2.ofLp ((fun i => i) ⟨0, ⋯⟩)h2.«1»c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ2.ofLp)).ofLp ((fun i => i) ⟨1, ⋯⟩) =
  (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ2.ofLp ((fun i => i) ⟨1, ⋯⟩) <;>h2.«0»c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ2.ofLp)).ofLp ((fun i => i) ⟨0, ⋯⟩) =
  (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ2.ofLp ((fun i => i) ⟨0, ⋯⟩)h2.«1»c:↥(unitary ℂ)z:ℂw0:ℂw1:ℂ⊢ (WithLp.toLp 2 (!![1, 0; 0, ↑c ^ 6].mulVec (sliceHiggs z w0 w1).Φ2.ofLp)).ofLp ((fun i => i) ⟨1, ⋯⟩) =
  (sliceHiggs z w0 (↑c ^ 6 * w1)).Φ2.ofLp ((fun i => i) ⟨1, ⋯⟩) simp [Matrix.mulVec, dotProduct, Fin.sum_univ_two]All goals completed! 🐙

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) := byu:↥(unitary ℂ)a:Fin 6 → ℝ⊢ GaugeGroupI.gaugeCartan u • sliceR a = sliceR (cartanRotParam u a)
  have h : ∀ z : ℂ, (↑z.re + Complex.I * ↑z.im) = z := fun z => byu:↥(unitary ℂ)a:Fin 6 → ℝz:ℂ⊢ ↑z.re + Complex.I * ↑z.im = zu:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ GaugeGroupI.gaugeCartan u • sliceR a = sliceR (cartanRotParam u a)
    rw [mul_commu:↥(unitary ℂ)a:Fin 6 → ℝz:ℂ⊢ ↑z.re + ↑z.im * Complex.I = zu:↥(unitary ℂ)a:Fin 6 → ℝz:ℂ⊢ ↑z.re + ↑z.im * Complex.I = zu:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ GaugeGroupI.gaugeCartan u • sliceR a = sliceR (cartanRotParam u a)]u:↥(unitary ℂ)a:Fin 6 → ℝz:ℂ⊢ ↑z.re + ↑z.im * Complex.I = zu:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ GaugeGroupI.gaugeCartan u • sliceR a = sliceR (cartanRotParam u a); exact Complex.re_add_im zu:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ GaugeGroupI.gaugeCartan u • sliceR a = sliceR (cartanRotParam u a)u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ GaugeGroupI.gaugeCartan u • sliceR a = sliceR (cartanRotParam u a)
  rw [sliceR_apply,u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ GaugeGroupI.gaugeCartan u •
    sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) =
  sliceR (cartanRotParam u a)u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ sliceHiggs (↑u * (↑(a 0) + Complex.I * ↑(a 1))) (↑u * (↑(a 2) + Complex.I * ↑(a 3)))
    (star ↑u * (↑(a 4) + Complex.I * ↑(a 5))) =
  sliceHiggs (↑(cartanRotParam u a 0) + Complex.I * ↑(cartanRotParam u a 1))
    (↑(cartanRotParam u a 2) + Complex.I * ↑(cartanRotParam u a 3))
    (↑(cartanRotParam u a 4) + Complex.I * ↑(cartanRotParam u a 5)) gaugeCartan_smul_sliceHiggs,u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ sliceHiggs (↑u * (↑(a 0) + Complex.I * ↑(a 1))) (↑u * (↑(a 2) + Complex.I * ↑(a 3)))
    (star ↑u * (↑(a 4) + Complex.I * ↑(a 5))) =
  sliceR (cartanRotParam u a)u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ sliceHiggs (↑u * (↑(a 0) + Complex.I * ↑(a 1))) (↑u * (↑(a 2) + Complex.I * ↑(a 3)))
    (star ↑u * (↑(a 4) + Complex.I * ↑(a 5))) =
  sliceHiggs (↑(cartanRotParam u a 0) + Complex.I * ↑(cartanRotParam u a 1))
    (↑(cartanRotParam u a 2) + Complex.I * ↑(cartanRotParam u a 3))
    (↑(cartanRotParam u a 4) + Complex.I * ↑(cartanRotParam u a 5)) sliceR_applyu:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ sliceHiggs (↑u * (↑(a 0) + Complex.I * ↑(a 1))) (↑u * (↑(a 2) + Complex.I * ↑(a 3)))
    (star ↑u * (↑(a 4) + Complex.I * ↑(a 5))) =
  sliceHiggs (↑(cartanRotParam u a 0) + Complex.I * ↑(cartanRotParam u a 1))
    (↑(cartanRotParam u a 2) + Complex.I * ↑(cartanRotParam u a 3))
    (↑(cartanRotParam u a 4) + Complex.I * ↑(cartanRotParam u a 5))u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ sliceHiggs (↑u * (↑(a 0) + Complex.I * ↑(a 1))) (↑u * (↑(a 2) + Complex.I * ↑(a 3)))
    (star ↑u * (↑(a 4) + Complex.I * ↑(a 5))) =
  sliceHiggs (↑(cartanRotParam u a 0) + Complex.I * ↑(cartanRotParam u a 1))
    (↑(cartanRotParam u a 2) + Complex.I * ↑(cartanRotParam u a 3))
    (↑(cartanRotParam u a 4) + Complex.I * ↑(cartanRotParam u a 5))]u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ sliceHiggs (↑u * (↑(a 0) + Complex.I * ↑(a 1))) (↑u * (↑(a 2) + Complex.I * ↑(a 3)))
    (star ↑u * (↑(a 4) + Complex.I * ↑(a 5))) =
  sliceHiggs (↑(cartanRotParam u a 0) + Complex.I * ↑(cartanRotParam u a 1))
    (↑(cartanRotParam u a 2) + Complex.I * ↑(cartanRotParam u a 3))
    (↑(cartanRotParam u a 4) + Complex.I * ↑(cartanRotParam u a 5))
  congr 1e_zu:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ ↑u * (↑(a 0) + Complex.I * ↑(a 1)) = ↑(cartanRotParam u a 0) + Complex.I * ↑(cartanRotParam u a 1)e_w0u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ ↑u * (↑(a 2) + Complex.I * ↑(a 3)) = ↑(cartanRotParam u a 2) + Complex.I * ↑(cartanRotParam u a 3)e_w1u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ star ↑u * (↑(a 4) + Complex.I * ↑(a 5)) = ↑(cartanRotParam u a 4) + Complex.I * ↑(cartanRotParam u a 5) <;>e_zu:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ ↑u * (↑(a 0) + Complex.I * ↑(a 1)) = ↑(cartanRotParam u a 0) + Complex.I * ↑(cartanRotParam u a 1)e_w0u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ ↑u * (↑(a 2) + Complex.I * ↑(a 3)) = ↑(cartanRotParam u a 2) + Complex.I * ↑(cartanRotParam u a 3)e_w1u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ star ↑u * (↑(a 4) + Complex.I * ↑(a 5)) = ↑(cartanRotParam u a 4) + Complex.I * ↑(cartanRotParam u a 5) simp only [cartanRotParam, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.cons_val, Fin.isValue]e_w1u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ star ↑u * (↑(a 4) + Complex.I * ↑(a 5)) =
  ↑(star ↑u * (↑(a 4) + Complex.I * ↑(a 5))).re + Complex.I * ↑(star ↑u * (↑(a 4) + Complex.I * ↑(a 5))).im <;>e_zu:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ ↑u * (↑(a 0) + Complex.I * ↑(a 1)) =
  ↑(↑u * (↑(a 0) + Complex.I * ↑(a 1))).re + Complex.I * ↑(↑u * (↑(a 0) + Complex.I * ↑(a 1))).ime_w0u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ ↑u * (↑(a 2) + Complex.I * ↑(a 3)) =
  ↑(↑u * (↑(a 2) + Complex.I * ↑(a 3))).re + Complex.I * ↑(↑u * (↑(a 2) + Complex.I * ↑(a 3))).ime_w1u:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ star ↑u * (↑(a 4) + Complex.I * ↑(a 5)) =
  ↑(star ↑u * (↑(a 4) + Complex.I * ↑(a 5))).re + Complex.I * ↑(star ↑u * (↑(a 4) + Complex.I * ↑(a 5))).im rw [he_zu:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ ↑u * (↑(a 0) + Complex.I * ↑(a 1)) = ↑u * (↑(a 0) + Complex.I * ↑(a 1))All goals completed! 🐙]All goals completed! 🐙

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) := byc:↥(unitary ℂ)a:Fin 6 → ℝ⊢ GaugeGroupI.ofU1Subgroup c • sliceR a = sliceR (resRotParam c a)
  have h : ∀ z : ℂ, (↑z.re + Complex.I * ↑z.im) = z := fun z => byc:↥(unitary ℂ)a:Fin 6 → ℝz:ℂ⊢ ↑z.re + Complex.I * ↑z.im = zc:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ GaugeGroupI.ofU1Subgroup c • sliceR a = sliceR (resRotParam c a)
    rw [mul_commc:↥(unitary ℂ)a:Fin 6 → ℝz:ℂ⊢ ↑z.re + ↑z.im * Complex.I = zc:↥(unitary ℂ)a:Fin 6 → ℝz:ℂ⊢ ↑z.re + ↑z.im * Complex.I = zc:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ GaugeGroupI.ofU1Subgroup c • sliceR a = sliceR (resRotParam c a)]c:↥(unitary ℂ)a:Fin 6 → ℝz:ℂ⊢ ↑z.re + ↑z.im * Complex.I = zc:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ GaugeGroupI.ofU1Subgroup c • sliceR a = sliceR (resRotParam c a); exact Complex.re_add_im zc:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ GaugeGroupI.ofU1Subgroup c • sliceR a = sliceR (resRotParam c a)c:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ GaugeGroupI.ofU1Subgroup c • sliceR a = sliceR (resRotParam c a)
  rw [sliceR_apply,c:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ GaugeGroupI.ofU1Subgroup c •
    sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑(a 4) + Complex.I * ↑(a 5)) =
  sliceR (resRotParam c a)c:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5))) =
  sliceHiggs (↑(resRotParam c a 0) + Complex.I * ↑(resRotParam c a 1))
    (↑(resRotParam c a 2) + Complex.I * ↑(resRotParam c a 3)) (↑(resRotParam c a 4) + Complex.I * ↑(resRotParam c a 5)) ofU1Subgroup_smul_sliceHiggs,c:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5))) =
  sliceR (resRotParam c a)c:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5))) =
  sliceHiggs (↑(resRotParam c a 0) + Complex.I * ↑(resRotParam c a 1))
    (↑(resRotParam c a 2) + Complex.I * ↑(resRotParam c a 3)) (↑(resRotParam c a 4) + Complex.I * ↑(resRotParam c a 5)) sliceR_applyc:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5))) =
  sliceHiggs (↑(resRotParam c a 0) + Complex.I * ↑(resRotParam c a 1))
    (↑(resRotParam c a 2) + Complex.I * ↑(resRotParam c a 3)) (↑(resRotParam c a 4) + Complex.I * ↑(resRotParam c a 5))c:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5))) =
  sliceHiggs (↑(resRotParam c a 0) + Complex.I * ↑(resRotParam c a 1))
    (↑(resRotParam c a 2) + Complex.I * ↑(resRotParam c a 3)) (↑(resRotParam c a 4) + Complex.I * ↑(resRotParam c a 5))]c:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ sliceHiggs (↑(a 0) + Complex.I * ↑(a 1)) (↑(a 2) + Complex.I * ↑(a 3)) (↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5))) =
  sliceHiggs (↑(resRotParam c a 0) + Complex.I * ↑(resRotParam c a 1))
    (↑(resRotParam c a 2) + Complex.I * ↑(resRotParam c a 3)) (↑(resRotParam c a 4) + Complex.I * ↑(resRotParam c a 5))
  congr 1e_w1c:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ ↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5)) = ↑(resRotParam c a 4) + Complex.I * ↑(resRotParam c a 5)
  simp only [resRotParam, Matrix.cons_val, Fin.isValue]e_w1c:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ ↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5)) =
  ↑(↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5))).re + Complex.I * ↑(↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5))).im
  first | rfle_w1c:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ ↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5)) =
  ↑(↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5))).re + Complex.I * ↑(↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5))).im | rw [he_w1c:↥(unitary ℂ)a:Fin 6 → ℝh:∀ (z : ℂ), ↑z.re + Complex.I * ↑z.im = z⊢ ↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5)) = ↑c ^ 6 * (↑(a 4) + Complex.I * ↑(a 5))All goals completed! 🐙]All goals completed! 🐙