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.

def SMRHN.SMNoGrav (n : ℕ) : ACCSystem

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

Equations

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

@[simp]

theorem SMRHN.SMNoGrav_quadraticACCs (n : ℕ) (i : Fin 0) : (SMNoGrav n).quadraticACCs i = i.elim0

@[simp]

theorem SMRHN.SMNoGrav_numberCharges (n : ℕ) : (SMNoGrav n).numberCharges = 6 * n

@[simp]

theorem SMRHN.SMNoGrav_cubicACC_apply (n : ℕ) (S : (SMνCharges n).Charges) : (SMNoGrav 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.SMNoGrav_numberQuadratic (n : ℕ) : (SMNoGrav n).numberQuadratic = 0

@[simp]

theorem SMRHN.SMNoGrav_linearACCs (n : ℕ) (i : Fin 2) : (SMNoGrav n).linearACCs i = match i with | 0 => { toFun := fun (S : (SMνCharges n).Charges) => ∑ i : Fin n, (3 * S (finProdFinEquiv (0, i)) + S (finProdFinEquiv (3, i))), map_add' := ⋯, map_smul' := ⋯ } | 1 => { 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' := ⋯ }

@[simp]

theorem SMRHN.SMNoGrav_numberLinear (n : ℕ) : (SMNoGrav n).numberLinear = 2

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

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

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

def SMRHN.SMNoGrav.chargeToLinear {n : ℕ} (S : (SMNoGrav n).Charges) (hSU2 : SMνACCs.accSU2 S = 0) (hSU3 : SMνACCs.accSU3 S = 0) : (SMNoGrav n).LinSols

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

Equations

• SMRHN.SMNoGrav.chargeToLinear S hSU2 hSU3 = { val := S, linearSol := ⋯ }

def SMRHN.SMNoGrav.linearToQuad {n : ℕ} (S : (SMNoGrav n).LinSols) : (SMNoGrav n).QuadSols

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

Equations

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

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

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

Equations

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

def SMRHN.SMNoGrav.chargeToQuad {n : ℕ} (S : (SMNoGrav n).Charges) (hSU2 : SMνACCs.accSU2 S = 0) (hSU3 : SMνACCs.accSU3 S = 0) : (SMNoGrav n).QuadSols

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

Equations

• SMRHN.SMNoGrav.chargeToQuad S hSU2 hSU3 = SMRHN.SMNoGrav.linearToQuad (SMRHN.SMNoGrav.chargeToLinear S hSU2 hSU3)

def SMRHN.SMNoGrav.chargeToAF {n : ℕ} (S : (SMNoGrav n).Charges) (hSU2 : SMνACCs.accSU2 S = 0) (hSU3 : SMνACCs.accSU3 S = 0) (hc : SMνACCs.accCube S = 0) : (SMNoGrav n).Sols

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

Equations

• SMRHN.SMNoGrav.chargeToAF S hSU2 hSU3 hc = SMRHN.SMNoGrav.quadToAF (SMRHN.SMNoGrav.chargeToQuad S hSU2 hSU3) hc

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

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

Equations

• SMRHN.SMNoGrav.linearToAF S hc = SMRHN.SMNoGrav.quadToAF (SMRHN.SMNoGrav.linearToQuad S) hc

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

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

Equations

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