ZMod charges #

In this module we investigate the possible ℤ₂ charges that one can assign to charges associated with ℤ₂ we can assign to particles in the SU(5) model, whilst keeping charges anomaly free.

source

def SuperSymmetry.SU5.Charges.ZModCharges (n : ℕ) [NeZero n] :

Finset (Charges (ZMod n))

The finite set of ZMod n valued charges which are complete, not pheno-constrained and don't regenerate dangerous couplings with the Yukawa term up-to 4-inserstions of singlets.

Equations

SuperSymmetry.SU5.Charges.ZModCharges n = {x ∈ SuperSymmetry.SU5.Charges.ofFinset Finset.univ Finset.univ | x.IsComplete ∧ ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 4}

Instances For

source

theorem SuperSymmetry.SU5.Charges.ZModCharges_one_eq :

ZModCharges 1 = ∅

This lemma corresponds to the statement that there are no choices of ℤ₁ representations which give a phenomenologically viable theory.

source

theorem SuperSymmetry.SU5.Charges.ZModCharges_two_eq :

ZModCharges 2 = ∅

This lemma corresponds to the statement that there are no choices of ℤ₂ representations which give a phenomenologically viable theory.

source

theorem SuperSymmetry.SU5.Charges.ZModCharges_three_eq :

ZModCharges 3 = ∅

This lemma corresponds to the statement that there are no choices of ℤ₃ representations which give a phenomenologically viable theory.

source

theorem SuperSymmetry.SU5.Charges.ZModCharges_four_eq :

ZModCharges 4 = {(some 0, some 2, {1}, {3}), (some 0, some 2, {3}, {1}), (some 1, some 2, {0}, {3}), (some 3, some 2, {0}, {1})}

source

theorem SuperSymmetry.SU5.Charges.ZModCharges_five_eq :

ZModCharges 5 = ∅

This lemma corresponds to the statement that there are no choices of ℤ₅ representations which give a phenomenologically viable theory.

source

theorem SuperSymmetry.SU5.Charges.ZModCharges_six_eq :

ZModCharges 6 = {(some 0, some 2, {5}, {1}), (some 0, some 4, {1}, {5}), (some 1, some 0, {2}, {3}), (some 1, some 2, {4}, {1}), (some 1, some 4, {0}, {5}), (some 1, some 4, {3}, {2}), (some 2, some 0, {1}, {3}), (some 2, some 4, {5}, {5}), (some 3, some 2, {5}, {4}), (some 3, some 4, {1}, {2}), (some 4, some 0, {5}, {3}), (some 4, some 2, {1}, {1}), (some 5, some 0, {4}, {3}), (some 5, some 2, {0}, {1}), (some 5, some 2, {3}, {4}), (some 5, some 4, {2}, {5})}

source

def SuperSymmetry.SU5.Charges.ZModZModCharges (n m : ℕ) [NeZero n] [NeZero m] :

Finset (Charges (ZMod n × ZMod m))

The finite set of ZMod n × ZMod m valued charges which are complete, not pheno-constrained and don't regenerate dangerous couplings with the Yukawa term up-to 4-inserstions of singlets.

Equations