Physlib.Particles.StandardModel.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.StandardModel.AnomalyCancellation.Basic

Anomaly Cancellation in the Standard Model without Gravity

This file defines the system of anomaly equations for the SM without RHN, and without the gravitational ACC.

@[expose] public section

The ACC system for the standard model without RHN and without the gravitational ACC.

@[simps!]
def SMNoGrav (n : ℕ) : ACCSystem where
  toACCSystemCharges := SMCharges n
  numberLinear := 2
  linearACCs := fun i =>
    match i with
    | 0 => @accSU2 n
    | 1 => accSU3
  numberQuadratic := 0
  quadraticACCs := byn:ℕ⊢ Fin 0 → HomogeneousQuadratic __ACCSystemCharges✝.Charges
    intro in:ℕi:Fin 0⊢ HomogeneousQuadratic __ACCSystemCharges✝.Charges
    exact Fin.elim0 iAll goals completed! 🐙
  cubicACC := accCube

The charges in (SMNoGrav n).LinSols satisfy the SU(2) anomaly-equation.

lemma SU2Sol (S : (SMNoGrav n).LinSols) : accSU2 S.val = 0 := byn:ℕS:(SMNoGrav n).LinSols⊢ accSU2 S.val = 0
  have hS := S.linearSoln:ℕS:(SMNoGrav n).LinSolshS:∀ (i : Fin (SMNoGrav n).numberLinear), ((SMNoGrav n).linearACCs i) S.val = 0⊢ accSU2 S.val = 0
  simp only [SMNoGrav_linearACCs] at hSn:ℕS:(SMNoGrav n).LinSolshS:∀ (i : Fin (SMNoGrav n).numberLinear),
  (match i with
      | 0 => accSU2
      | 1 => accSU3)
      S.val =
    0⊢ accSU2 S.val = 0
  exact hS ⟨0, byn:ℕS:(SMNoGrav n).LinSolshS:∀ (i : Fin (SMNoGrav n).numberLinear),
  (match i with
      | 0 => accSU2
      | 1 => accSU3)
      S.val =
    0⊢ 0 < (SMNoGrav n).numberLinear simpAll goals completed! 🐙⟩

The charges in (SMNoGrav n).LinSols satisfy the SU(3) anomaly-equation.

lemma SU3Sol (S : (SMNoGrav n).LinSols) : accSU3 S.val = 0 := byn:ℕS:(SMNoGrav n).LinSols⊢ accSU3 S.val = 0
  have hS := S.linearSoln:ℕS:(SMNoGrav n).LinSolshS:∀ (i : Fin (SMNoGrav n).numberLinear), ((SMNoGrav n).linearACCs i) S.val = 0⊢ accSU3 S.val = 0
  simp only [SMNoGrav_linearACCs] at hSn:ℕS:(SMNoGrav n).LinSolshS:∀ (i : Fin (SMNoGrav n).numberLinear),
  (match i with
      | 0 => accSU2
      | 1 => accSU3)
      S.val =
    0⊢ accSU3 S.val = 0
  exact hS ⟨1, byn:ℕS:(SMNoGrav n).LinSolshS:∀ (i : Fin (SMNoGrav n).numberLinear),
  (match i with
      | 0 => accSU2
      | 1 => accSU3)
      S.val =
    0⊢ 1 < (SMNoGrav n).numberLinear simpAll goals completed! 🐙⟩

The charges in (SMNoGrav n).Sols satisfy the cubic anomaly-equation.

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

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 AnomalyFreeLinear which satisfies the quadratic ACCs gives us a element of AnomalyFreeQuad.

def linearToQuad (S : (SMNoGrav n).LinSols) : (SMNoGrav n).QuadSols :=
  ⟨S, byn:ℕS:(SMNoGrav n).LinSols⊢ ∀ (i : Fin (SMNoGrav n).numberQuadratic), ((SMNoGrav n).quadraticACCs i) S.val = 0
    intro in:ℕS:(SMNoGrav n).LinSolsi:Fin (SMNoGrav n).numberQuadratic⊢ ((SMNoGrav n).quadraticACCs i) S.val = 0
    exact Fin.elim0 iAll goals completed! 🐙⟩

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

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

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

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 AnomalyFreeLinear which satisfies the quadratic and cubic ACCs gives us a element of AnomalyFree.

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