Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.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

We define the ACC system for the Standard Model with right-handed neutrinos.

@[expose] public section

The ACC system for the SM plus RHN with an additional U1.

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

              lemma gravSol (S : (PlusU1 n).LinSols) : accGrav S.val = 0 := byn:ℕS:(PlusU1 n).LinSols⊢ accGrav S.val = 0
  have hS := S.linearSoln:ℕS:(PlusU1 n).LinSolshS:∀ (i : Fin (PlusU1 n).numberLinear), ((PlusU1 n).linearACCs i) S.val = 0⊢ accGrav S.val = 0
  simp only [PlusU1_linearACCs] at hSn:ℕS:(PlusU1 n).LinSolshS:∀ (i : Fin (PlusU1 n).numberLinear),
  (match i with
      | 0 => accGrav
      | 1 => accSU2
      | 2 => accSU3
      | 3 => accYY)
      S.val =
    0⊢ accGrav S.val = 0
  exact hS ⟨0, byn:ℕS:(PlusU1 n).LinSolshS:∀ (i : Fin (PlusU1 n).numberLinear),
  (match i with
      | 0 => accGrav
      | 1 => accSU2
      | 2 => accSU3
      | 3 => accYY)
      S.val =
    0⊢ 0 < (PlusU1 n).numberLinear simpAll goals completed! 🐙⟩lemma SU2Sol (S : (PlusU1 n).LinSols) : accSU2 S.val = 0 := byn:ℕS:(PlusU1 n).LinSols⊢ accSU2 S.val = 0
  have hS := S.linearSoln:ℕS:(PlusU1 n).LinSolshS:∀ (i : Fin (PlusU1 n).numberLinear), ((PlusU1 n).linearACCs i) S.val = 0⊢ accSU2 S.val = 0
  simp only [PlusU1_linearACCs] at hSn:ℕS:(PlusU1 n).LinSolshS:∀ (i : Fin (PlusU1 n).numberLinear),
  (match i with
      | 0 => accGrav
      | 1 => accSU2
      | 2 => accSU3
      | 3 => accYY)
      S.val =
    0⊢ accSU2 S.val = 0
  exact hS ⟨1, byn:ℕS:(PlusU1 n).LinSolshS:∀ (i : Fin (PlusU1 n).numberLinear),
  (match i with
      | 0 => accGrav
      | 1 => accSU2
      | 2 => accSU3
      | 3 => accYY)
      S.val =
    0⊢ 1 < (PlusU1 n).numberLinear simpAll goals completed! 🐙⟩lemma SU3Sol (S : (PlusU1 n).LinSols) : accSU3 S.val = 0 := byn:ℕS:(PlusU1 n).LinSols⊢ accSU3 S.val = 0
  have hS := S.linearSoln:ℕS:(PlusU1 n).LinSolshS:∀ (i : Fin (PlusU1 n).numberLinear), ((PlusU1 n).linearACCs i) S.val = 0⊢ accSU3 S.val = 0
  simp only [PlusU1_linearACCs] at hSn:ℕS:(PlusU1 n).LinSolshS:∀ (i : Fin (PlusU1 n).numberLinear),
  (match i with
      | 0 => accGrav
      | 1 => accSU2
      | 2 => accSU3
      | 3 => accYY)
      S.val =
    0⊢ accSU3 S.val = 0
  exact hS ⟨2, byn:ℕS:(PlusU1 n).LinSolshS:∀ (i : Fin (PlusU1 n).numberLinear),
  (match i with
      | 0 => accGrav
      | 1 => accSU2
      | 2 => accSU3
      | 3 => accYY)
      S.val =
    0⊢ 2 < (PlusU1 n).numberLinear simpAll goals completed! 🐙⟩lemma YYsol (S : (PlusU1 n).LinSols) : accYY S.val = 0 := byn:ℕS:(PlusU1 n).LinSols⊢ accYY S.val = 0
  have hS := S.linearSoln:ℕS:(PlusU1 n).LinSolshS:∀ (i : Fin (PlusU1 n).numberLinear), ((PlusU1 n).linearACCs i) S.val = 0⊢ accYY S.val = 0
  simp only [PlusU1_linearACCs] at hSn:ℕS:(PlusU1 n).LinSolshS:∀ (i : Fin (PlusU1 n).numberLinear),
  (match i with
      | 0 => accGrav
      | 1 => accSU2
      | 2 => accSU3
      | 3 => accYY)
      S.val =
    0⊢ accYY S.val = 0
  exact hS ⟨3, byn:ℕS:(PlusU1 n).LinSolshS:∀ (i : Fin (PlusU1 n).numberLinear),
  (match i with
      | 0 => accGrav
      | 1 => accSU2
      | 2 => accSU3
      | 3 => accYY)
      S.val =
    0⊢ 3 < (PlusU1 n).numberLinear simpAll goals completed! 🐙⟩lemma quadSol (S : (PlusU1 n).QuadSols) : accQuad S.val = 0 := byn:ℕS:(PlusU1 n).QuadSols⊢ accQuad S.val = 0
  have hS := S.quadSoln:ℕS:(PlusU1 n).QuadSolshS:∀ (i : Fin (PlusU1 n).numberQuadratic), ((PlusU1 n).quadraticACCs i) S.val = 0⊢ accQuad S.val = 0
  simp only [PlusU1_quadraticACCs] at hSn:ℕS:(PlusU1 n).QuadSolshS:∀ (i : Fin (PlusU1 n).numberQuadratic),
  (match i with
      | 0 => quadBiLin.toHomogeneousQuad)
      S.val =
    0⊢ accQuad S.val = 0
  exact hS ⟨0, byn:ℕS:(PlusU1 n).QuadSolshS:∀ (i : Fin (PlusU1 n).numberQuadratic),
  (match i with
      | 0 => quadBiLin.toHomogeneousQuad)
      S.val =
    0⊢ 0 < (PlusU1 n).numberQuadratic simpAll goals completed! 🐙⟩lemma cubeSol (S : (PlusU1 n).Sols) : accCube S.val = 0 := byn:ℕS:(PlusU1 n).Sols⊢ accCube S.val = 0
  exact S.cubicSolAll goals completed! 🐙

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

def chargeToLinear (S : (PlusU1 n).Charges) (hGrav : accGrav S = 0)
    (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0) (hYY : accYY S = 0) :
    (PlusU1 n).LinSols :=
  ⟨S, byn:ℕS:(PlusU1 n).ChargeshGrav:accGrav S = 0hSU2:accSU2 S = 0hSU3:accSU3 S = 0hYY:accYY S = 0⊢ ∀ (i : Fin (PlusU1 n).numberLinear), ((PlusU1 n).linearACCs i) S = 0
    intro in:ℕS:(PlusU1 n).ChargeshGrav:accGrav S = 0hSU2:accSU2 S = 0hSU3:accSU3 S = 0hYY:accYY S = 0i:Fin (PlusU1 n).numberLinear⊢ ((PlusU1 n).linearACCs i) S = 0
    match i with
    | ⟨0, _⟩ =>n:ℕS:(PlusU1 n).ChargeshGrav:accGrav S = 0hSU2:accSU2 S = 0hSU3:accSU3 S = 0hYY:accYY S = 0i:Fin (PlusU1 n).numberLinearisLt✝:0 < (PlusU1 n).numberLinear⊢ ((PlusU1 n).linearACCs ⟨0, isLt✝⟩) S = 0 exact hGravAll goals completed! 🐙
    | ⟨1, _⟩ =>n:ℕS:(PlusU1 n).ChargeshGrav:accGrav S = 0hSU2:accSU2 S = 0hSU3:accSU3 S = 0hYY:accYY S = 0i:Fin (PlusU1 n).numberLinearisLt✝:1 < (PlusU1 n).numberLinear⊢ ((PlusU1 n).linearACCs ⟨1, isLt✝⟩) S = 0 exact hSU2All goals completed! 🐙
    | ⟨2, _⟩ =>n:ℕS:(PlusU1 n).ChargeshGrav:accGrav S = 0hSU2:accSU2 S = 0hSU3:accSU3 S = 0hYY:accYY S = 0i:Fin (PlusU1 n).numberLinearisLt✝:2 < (PlusU1 n).numberLinear⊢ ((PlusU1 n).linearACCs ⟨2, isLt✝⟩) S = 0 exact hSU3All goals completed! 🐙
    | ⟨3, _⟩ =>n:ℕS:(PlusU1 n).ChargeshGrav:accGrav S = 0hSU2:accSU2 S = 0hSU3:accSU3 S = 0hYY:accYY S = 0i:Fin (PlusU1 n).numberLinearisLt✝:3 < (PlusU1 n).numberLinear⊢ ((PlusU1 n).linearACCs ⟨3, isLt✝⟩) S = 0 exact hYYAll goals completed! 🐙⟩

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

def linearToQuad (S : (PlusU1 n).LinSols) (hQ : accQuad S.val = 0) :
    (PlusU1 n).QuadSols :=
  ⟨S, byn:ℕS:(PlusU1 n).LinSolshQ:accQuad S.val = 0⊢ ∀ (i : Fin (PlusU1 n).numberQuadratic), ((PlusU1 n).quadraticACCs i) S.val = 0
    intro in:ℕS:(PlusU1 n).LinSolshQ:accQuad S.val = 0i:Fin (PlusU1 n).numberQuadratic⊢ ((PlusU1 n).quadraticACCs i) S.val = 0
    match i with
    | ⟨0, _⟩ =>n:ℕS:(PlusU1 n).LinSolshQ:accQuad S.val = 0i:Fin (PlusU1 n).numberQuadraticisLt✝:0 < (PlusU1 n).numberQuadratic⊢ ((PlusU1 n).quadraticACCs ⟨0, isLt✝⟩) S.val = 0 exact hQAll goals completed! 🐙⟩

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

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

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

def chargeToQuad (S : (PlusU1 n).Charges) (hGrav : accGrav S = 0)
    (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0) (hYY : accYY S = 0) (hQ : accQuad S = 0) :
    (PlusU1 n).QuadSols :=
  linearToQuad (chargeToLinear S hGrav hSU2 hSU3 hYY) hQ

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

def chargeToAF (S : (PlusU1 n).Charges) (hGrav : accGrav S = 0) (hSU2 : accSU2 S = 0)
    (hSU3 : accSU3 S = 0) (hYY : accYY S = 0) (hQ : accQuad S = 0) (hc : accCube S = 0) :
    (PlusU1 n).Sols :=
  quadToAF (chargeToQuad S hGrav hSU2 hSU3 hYY hQ) hc

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

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

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

def perm (n : ℕ) : ACCSystemGroupAction (PlusU1 n) where
  group := PermGroup n
  groupInst := inferInstance
  rep := repCharges
  linearInvariant := byn✝:ℕn:ℕ⊢ ∀ (i : Fin (PlusU1 n).numberLinear) (g : PermGroup n) (S : (PlusU1 n).Charges),
  ((PlusU1 n).linearACCs i) ((repCharges g) S) = ((PlusU1 n).linearACCs i) S
    intro in✝:ℕn:ℕi:Fin (PlusU1 n).numberLinear⊢ ∀ (g : PermGroup n) (S : (PlusU1 n).Charges), ((PlusU1 n).linearACCs i) ((repCharges g) S) = ((PlusU1 n).linearACCs i) S
    match i with
    | ⟨0, _⟩ =>n✝:ℕn:ℕi:Fin (PlusU1 n).numberLinearisLt✝:0 < (PlusU1 n).numberLinear⊢ ∀ (g : PermGroup n) (S : (PlusU1 n).Charges),
  ((PlusU1 n).linearACCs ⟨0, isLt✝⟩) ((repCharges g) S) = ((PlusU1 n).linearACCs ⟨0, isLt✝⟩) S exact accGrav_invariantAll goals completed! 🐙
    | ⟨1, _⟩ =>n✝:ℕn:ℕi:Fin (PlusU1 n).numberLinearisLt✝:1 < (PlusU1 n).numberLinear⊢ ∀ (g : PermGroup n) (S : (PlusU1 n).Charges),
  ((PlusU1 n).linearACCs ⟨1, isLt✝⟩) ((repCharges g) S) = ((PlusU1 n).linearACCs ⟨1, isLt✝⟩) S exact accSU2_invariantAll goals completed! 🐙
    | ⟨2, _⟩ =>n✝:ℕn:ℕi:Fin (PlusU1 n).numberLinearisLt✝:2 < (PlusU1 n).numberLinear⊢ ∀ (g : PermGroup n) (S : (PlusU1 n).Charges),
  ((PlusU1 n).linearACCs ⟨2, isLt✝⟩) ((repCharges g) S) = ((PlusU1 n).linearACCs ⟨2, isLt✝⟩) S exact accSU3_invariantAll goals completed! 🐙
    | ⟨3, _⟩ =>n✝:ℕn:ℕi:Fin (PlusU1 n).numberLinearisLt✝:3 < (PlusU1 n).numberLinear⊢ ∀ (g : PermGroup n) (S : (PlusU1 n).Charges),
  ((PlusU1 n).linearACCs ⟨3, isLt✝⟩) ((repCharges g) S) = ((PlusU1 n).linearACCs ⟨3, isLt✝⟩) S exact accYY_invariantAll goals completed! 🐙
  quadInvariant := byn✝:ℕn:ℕ⊢ ∀ (i : Fin (PlusU1 n).numberQuadratic) (g : PermGroup n) (S : (PlusU1 n).Charges),
  ((PlusU1 n).quadraticACCs i) ((repCharges g) S) = ((PlusU1 n).quadraticACCs i) S
    intro in✝:ℕn:ℕi:Fin (PlusU1 n).numberQuadratic⊢ ∀ (g : PermGroup n) (S : (PlusU1 n).Charges),
  ((PlusU1 n).quadraticACCs i) ((repCharges g) S) = ((PlusU1 n).quadraticACCs i) S
    match i with
    | ⟨0, _⟩ =>n✝:ℕn:ℕi:Fin (PlusU1 n).numberQuadraticisLt✝:0 < (PlusU1 n).numberQuadratic⊢ ∀ (g : PermGroup n) (S : (PlusU1 n).Charges),
  ((PlusU1 n).quadraticACCs ⟨0, isLt✝⟩) ((repCharges g) S) = ((PlusU1 n).quadraticACCs ⟨0, isLt✝⟩) S exact accQuad_invariantAll goals completed! 🐙
  cubicInvariant := accCube_invariant