Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.NoGrav.Basic

Imports

/-
Copyright (c) 2024 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.RHN.AnomalyCancellation.Permutations
public import Physlib.QFT.AnomalyCancellation.GroupActions

ACC system for SM with RHN and no gravitational anomaly.

We define the ACC system for the Standard Model with right-handed neutrinos and no gravitational anomaly.

@[expose] public section

The ACC system for the SM plus RHN with no gravitational anomaly.

@[simps!]
def SMNoGrav (n : ℕ) : ACCSystem where
  toACCSystemCharges := SMνCharges n
  numberLinear := 2
  linearACCs := fun i =>
    match i with
    | 0 => @accSU2 n
    | 1 => accSU3
  numberQuadratic := 0
  quadraticACCs := fun i ↦ Fin.elim0 i
  cubicACC := accCube

              lemma SU2Sol (S : (SMNoGrav n).LinSols) : accSU2 S.val = 0 := S.linearSol ⟨0, byn:ℕS:(SMNoGrav n).LinSols⊢ 0 < (SMNoGrav n).numberLinear simpAll goals completed! 🐙⟩lemma SU3Sol (S : (SMNoGrav n).LinSols) : accSU3 S.val = 0 := S.linearSol ⟨1, byn:ℕS:(SMNoGrav n).LinSols⊢ 1 < (SMNoGrav n).numberLinear simpAll goals completed! 🐙⟩lemma cubeSol (S : (SMNoGrav n).Sols) : accCube S.val = 0 := S.cubicSol

An element of charges which satisfies the linear ACCs gives us a element of LinSols.

def chargeToLinear (S : (SMNoGrav n).Charges) (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0) :
    (SMNoGrav n).LinSols :=
  ⟨S, byn:ℕS:(SMNoGrav n).ChargeshSU2:accSU2 S = 0hSU3:accSU3 S = 0⊢ ∀ (i : Fin (SMNoGrav n).numberLinear), ((SMNoGrav n).linearACCs i) S = 0
    intro in:ℕS:(SMNoGrav n).ChargeshSU2:accSU2 S = 0hSU3:accSU3 S = 0i:Fin (SMNoGrav n).numberLinear⊢ ((SMNoGrav n).linearACCs i) S = 0
    match i with
    | ⟨0, _⟩ =>n:ℕS:(SMNoGrav n).ChargeshSU2:accSU2 S = 0hSU3:accSU3 S = 0i:Fin (SMNoGrav n).numberLinearisLt✝:0 < (SMNoGrav n).numberLinear⊢ ((SMNoGrav n).linearACCs ⟨0, isLt✝⟩) S = 0 exact hSU2All goals completed! 🐙
    | ⟨1, _⟩ =>n:ℕS:(SMNoGrav n).ChargeshSU2:accSU2 S = 0hSU3:accSU3 S = 0i:Fin (SMNoGrav n).numberLinearisLt✝:1 < (SMNoGrav n).numberLinear⊢ ((SMNoGrav n).linearACCs ⟨1, isLt✝⟩) S = 0 exact hSU3All goals completed! 🐙⟩

An element of LinSols which satisfies the quadratic ACCs gives us a element of QuadSols.

def linearToQuad (S : (SMNoGrav n).LinSols) : (SMNoGrav n).QuadSols := ⟨S, fun i ↦ Fin.elim0 i⟩

An element of QuadSols which satisfies the quadratic ACCs gives us a element of LinSols.

def quadToAF (S : (SMNoGrav n).QuadSols) (hc : accCube S.val = 0) :
    (SMNoGrav n).Sols := ⟨S, hc⟩

An element of charges which satisfies the linear and quadratic ACCs gives us a element of QuadSols.

def chargeToQuad (S : (SMNoGrav n).Charges) (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0) :
    (SMNoGrav n).QuadSols :=
  linearToQuad $ chargeToLinear S hSU2 hSU3

An element of charges which satisfies the linear, quadratic and cubic ACCs gives us a element of Sols.

def chargeToAF (S : (SMNoGrav n).Charges) (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0)
    (hc : accCube S = 0) : (SMNoGrav n).Sols :=
  quadToAF (chargeToQuad S hSU2 hSU3) hc

An element of LinSols which satisfies the quadratic and cubic ACCs gives us a element of Sols.

def linearToAF (S : (SMNoGrav n).LinSols)
    (hc : accCube S.val = 0) : (SMNoGrav n).Sols :=
  quadToAF (linearToQuad S) hc

The permutations acting on the ACC system corresponding to the SM with RHN, and no gravitational anomaly.

def perm (n : ℕ) : ACCSystemGroupAction (SMNoGrav n) where
  group := PermGroup n
  groupInst := inferInstance
  rep := repCharges
  linearInvariant := byn✝:ℕn:ℕ⊢ ∀ (i : Fin (SMNoGrav n).numberLinear) (g : PermGroup n) (S : (SMNoGrav n).Charges),
  ((SMNoGrav n).linearACCs i) ((repCharges g) S) = ((SMNoGrav n).linearACCs i) S
    intro in✝:ℕn:ℕi:Fin (SMNoGrav n).numberLinear⊢ ∀ (g : PermGroup n) (S : (SMNoGrav n).Charges),
  ((SMNoGrav n).linearACCs i) ((repCharges g) S) = ((SMNoGrav n).linearACCs i) S
    match i with
    | ⟨0, _⟩ =>n✝:ℕn:ℕi:Fin (SMNoGrav n).numberLinearisLt✝:0 < (SMNoGrav n).numberLinear⊢ ∀ (g : PermGroup n) (S : (SMNoGrav n).Charges),
  ((SMNoGrav n).linearACCs ⟨0, isLt✝⟩) ((repCharges g) S) = ((SMNoGrav n).linearACCs ⟨0, isLt✝⟩) S exact accSU2_invariantAll goals completed! 🐙
    | ⟨1, _⟩ =>n✝:ℕn:ℕi:Fin (SMNoGrav n).numberLinearisLt✝:1 < (SMNoGrav n).numberLinear⊢ ∀ (g : PermGroup n) (S : (SMNoGrav n).Charges),
  ((SMNoGrav n).linearACCs ⟨1, isLt✝⟩) ((repCharges g) S) = ((SMNoGrav n).linearACCs ⟨1, isLt✝⟩) S exact accSU3_invariantAll goals completed! 🐙
  quadInvariant := byn✝:ℕn:ℕ⊢ ∀ (i : Fin (SMNoGrav n).numberQuadratic) (g : PermGroup n) (S : (SMNoGrav n).Charges),
  ((SMNoGrav n).quadraticACCs i) ((repCharges g) S) = ((SMNoGrav n).quadraticACCs i) S
    intro in✝:ℕn:ℕi:Fin (SMNoGrav n).numberQuadratic⊢ ∀ (g : PermGroup n) (S : (SMNoGrav n).Charges),
  ((SMNoGrav n).quadraticACCs i) ((repCharges g) S) = ((SMNoGrav n).quadraticACCs i) S
    simp only [SMNoGrav_numberQuadratic] at in✝:ℕn:ℕi✝:Fin (SMNoGrav n).numberQuadratici:Fin 0⊢ ∀ (g : PermGroup n) (S : (SMNoGrav n).Charges),
  ((SMNoGrav n).quadraticACCs i) ((repCharges g) S) = ((SMNoGrav n).quadraticACCs i) S
    exact Fin.elim0 iAll goals completed! 🐙
  cubicInvariant := accCube_invariant