ACC system for SM with RHN

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

def SMRHN.PlusU1 (n : ℕ) : ACCSystem

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SMRHN.PlusU1_linearACCs (n : ℕ) (i : Fin 4) : (PlusU1 n).linearACCs i = match i with | 0 => { toFun := fun (S : (SMνCharges n).Charges) => ∑ i : Fin n, (6 * S (finProdFinEquiv (0, i)) + 3 * S (finProdFinEquiv (1, i)) + 3 * S (finProdFinEquiv (2, i)) + 2 * S (finProdFinEquiv (3, i)) + S (finProdFinEquiv (4, i)) + S (finProdFinEquiv (5, i))), map_add' := ⋯, map_smul' := ⋯ } | 1 => { toFun := fun (S : (SMνCharges n).Charges) => ∑ i : Fin n, (3 * S (finProdFinEquiv (0, i)) + S (finProdFinEquiv (3, i))), map_add' := ⋯, map_smul' := ⋯ } | 2 => { toFun := fun (S : (SMνCharges n).Charges) => ∑ i : Fin n, (2 * S (finProdFinEquiv (0, i)) + S (finProdFinEquiv (1, i)) + S (finProdFinEquiv (2, i))), map_add' := ⋯, map_smul' := ⋯ } | 3 => { toFun := fun (S : (SMνCharges n).Charges) => ∑ i : Fin n, (S (finProdFinEquiv (0, i)) + 8 * S (finProdFinEquiv (1, i)) + 2 * S (finProdFinEquiv (2, i)) + 3 * S (finProdFinEquiv (3, i)) + 6 * S (finProdFinEquiv (4, i))), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SMRHN.PlusU1_numberCharges (n : ℕ) : (PlusU1 n).numberCharges = 6 * n

@[simp]

theorem SMRHN.PlusU1_numberLinear (n : ℕ) : (PlusU1 n).numberLinear = 4

@[simp]

theorem SMRHN.PlusU1_cubicACC_apply (n : ℕ) (S : (SMνCharges n).Charges) : (PlusU1 n).cubicACC S = ∑ i : Fin n, (6 * (S (finProdFinEquiv (0, i)) * S (finProdFinEquiv (0, i)) * S (finProdFinEquiv (0, i))) + 3 * (S (finProdFinEquiv (1, i)) * S (finProdFinEquiv (1, i)) * S (finProdFinEquiv (1, i))) + 3 * (S (finProdFinEquiv (2, i)) * S (finProdFinEquiv (2, i)) * S (finProdFinEquiv (2, i))) + 2 * (S (finProdFinEquiv (3, i)) * S (finProdFinEquiv (3, i)) * S (finProdFinEquiv (3, i))) + S (finProdFinEquiv (4, i)) * S (finProdFinEquiv (4, i)) * S (finProdFinEquiv (4, i)) + S (finProdFinEquiv (5, i)) * S (finProdFinEquiv (5, i)) * S (finProdFinEquiv (5, i)))

@[simp]

theorem SMRHN.PlusU1_quadraticACCs (n : ℕ) (i : Fin 1) : (PlusU1 n).quadraticACCs i = match i with | 0 => SMνACCs.quadBiLin.toHomogeneousQuad

@[simp]

theorem SMRHN.PlusU1_numberQuadratic (n : ℕ) : (PlusU1 n).numberQuadratic = 1

theorem SMRHN.PlusU1.gravSol {n : ℕ} (S : (PlusU1 n).LinSols) : SMνACCs.accGrav S.val = 0

theorem SMRHN.PlusU1.SU2Sol {n : ℕ} (S : (PlusU1 n).LinSols) : SMνACCs.accSU2 S.val = 0

theorem SMRHN.PlusU1.SU3Sol {n : ℕ} (S : (PlusU1 n).LinSols) : SMνACCs.accSU3 S.val = 0

theorem SMRHN.PlusU1.YYsol {n : ℕ} (S : (PlusU1 n).LinSols) : SMνACCs.accYY S.val = 0

theorem SMRHN.PlusU1.quadSol {n : ℕ} (S : (PlusU1 n).QuadSols) : SMνACCs.accQuad S.val = 0

theorem SMRHN.PlusU1.cubeSol {n : ℕ} (S : (PlusU1 n).Sols) : SMνACCs.accCube S.val = 0

def SMRHN.PlusU1.chargeToLinear {n : ℕ} (S : (PlusU1 n).Charges) (hGrav : SMνACCs.accGrav S = 0) (hSU2 : SMνACCs.accSU2 S = 0) (hSU3 : SMνACCs.accSU3 S = 0) (hYY : SMνACCs.accYY S = 0) : (PlusU1 n).LinSols

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

Equations

• SMRHN.PlusU1.chargeToLinear S hGrav hSU2 hSU3 hYY = { val := S, linearSol := ⋯ }

def SMRHN.PlusU1.linearToQuad {n : ℕ} (S : (PlusU1 n).LinSols) (hQ : SMνACCs.accQuad S.val = 0) : (PlusU1 n).QuadSols

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

Equations

• SMRHN.PlusU1.linearToQuad S hQ = { toLinSols := S, quadSol := ⋯ }

def SMRHN.PlusU1.quadToAF {n : ℕ} (S : (PlusU1 n).QuadSols) (hc : SMνACCs.accCube S.val = 0) : (PlusU1 n).Sols

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

Equations

• SMRHN.PlusU1.quadToAF S hc = { toQuadSols := S, cubicSol := hc }

def SMRHN.PlusU1.chargeToQuad {n : ℕ} (S : (PlusU1 n).Charges) (hGrav : SMνACCs.accGrav S = 0) (hSU2 : SMνACCs.accSU2 S = 0) (hSU3 : SMνACCs.accSU3 S = 0) (hYY : SMνACCs.accYY S = 0) (hQ : SMνACCs.accQuad S = 0) : (PlusU1 n).QuadSols

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

Equations

• SMRHN.PlusU1.chargeToQuad S hGrav hSU2 hSU3 hYY hQ = SMRHN.PlusU1.linearToQuad (SMRHN.PlusU1.chargeToLinear S hGrav hSU2 hSU3 hYY) hQ

def SMRHN.PlusU1.chargeToAF {n : ℕ} (S : (PlusU1 n).Charges) (hGrav : SMνACCs.accGrav S = 0) (hSU2 : SMνACCs.accSU2 S = 0) (hSU3 : SMνACCs.accSU3 S = 0) (hYY : SMνACCs.accYY S = 0) (hQ : SMνACCs.accQuad S = 0) (hc : SMνACCs.accCube S = 0) : (PlusU1 n).Sols

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

Equations

• SMRHN.PlusU1.chargeToAF S hGrav hSU2 hSU3 hYY hQ hc = SMRHN.PlusU1.quadToAF (SMRHN.PlusU1.chargeToQuad S hGrav hSU2 hSU3 hYY hQ) hc

def SMRHN.PlusU1.linearToAF {n : ℕ} (S : (PlusU1 n).LinSols) (hQ : SMνACCs.accQuad S.val = 0) (hc : SMνACCs.accCube S.val = 0) : (PlusU1 n).Sols

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

Equations

• SMRHN.PlusU1.linearToAF S hQ hc = SMRHN.PlusU1.quadToAF (SMRHN.PlusU1.linearToQuad S hQ) hc

def SMRHN.PlusU1.perm (n : ℕ) : ACCSystemGroupAction (PlusU1 n)

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

Equations

• SMRHN.PlusU1.perm n = { group := SMRHN.PermGroup n, groupInst := inferInstance, rep := SMRHN.repCharges, linearInvariant := ⋯, quadInvariant := ⋯, cubicInvariant := ⋯ }