Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.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 (without hypercharge).

We define the ACC system for the Standard Model (without hypercharge) with right-handed neutrinos.

@[expose] public section

The ACC system for the SM plus RHN.

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

              lemma gravSol (S : (SM n).LinSols) : accGrav S.val = 0 := S.linearSol ⟨0, byn:ℕS:(SM n).LinSols⊢ 0 < (SM n).numberLinear simpAll goals completed! 🐙⟩lemma SU2Sol (S : (SM n).LinSols) : accSU2 S.val = 0 := S.linearSol ⟨1, byn:ℕS:(SM n).LinSols⊢ 1 < (SM n).numberLinear simpAll goals completed! 🐙⟩lemma SU3Sol (S : (SM n).LinSols) : accSU3 S.val = 0 := S.linearSol ⟨2, byn:ℕS:(SM n).LinSols⊢ 2 < (SM n).numberLinear simpAll goals completed! 🐙⟩lemma cubeSol (S : (SM 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 : (SM n).Charges) (hGrav : accGrav S = 0)
    (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0) : (SM n).LinSols :=
  ⟨S, byn:ℕS:(SM n).ChargeshGrav:accGrav S = 0hSU2:accSU2 S = 0hSU3:accSU3 S = 0⊢ ∀ (i : Fin (SM n).numberLinear), ((SM n).linearACCs i) S = 0
    intro in:ℕS:(SM n).ChargeshGrav:accGrav S = 0hSU2:accSU2 S = 0hSU3:accSU3 S = 0i:Fin (SM n).numberLinear⊢ ((SM n).linearACCs i) S = 0
    match i with
    | ⟨0, _⟩ =>n:ℕS:(SM n).ChargeshGrav:accGrav S = 0hSU2:accSU2 S = 0hSU3:accSU3 S = 0i:Fin (SM n).numberLinearisLt✝:0 < (SM n).numberLinear⊢ ((SM n).linearACCs ⟨0, isLt✝⟩) S = 0 exact hGravAll goals completed! 🐙
    | ⟨1, _⟩ =>n:ℕS:(SM n).ChargeshGrav:accGrav S = 0hSU2:accSU2 S = 0hSU3:accSU3 S = 0i:Fin (SM n).numberLinearisLt✝:1 < (SM n).numberLinear⊢ ((SM n).linearACCs ⟨1, isLt✝⟩) S = 0 exact hSU2All goals completed! 🐙
    | ⟨2, _⟩ =>n:ℕS:(SM n).ChargeshGrav:accGrav S = 0hSU2:accSU2 S = 0hSU3:accSU3 S = 0i:Fin (SM n).numberLinearisLt✝:2 < (SM n).numberLinear⊢ ((SM n).linearACCs ⟨2, 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 : (SM n).LinSols) : (SM n).QuadSols :=
  ⟨S, fun i ↦ Fin.elim0 i⟩

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

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

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

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

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

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

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

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

The permutations acting on the ACC system corresponding to the SM with RHN.

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