The field labels

The field labels of the SU(5) SUSY GUT is an inductive type that labels the allowed representations present in the theory.

inductive SuperSymmetry.SU5.FieldLabel : Type

The types of field present in an SU(5) GUT.

• fiveBarHu : FieldLabel
• fiveHu : FieldLabel
• fiveBarHd : FieldLabel
• fiveHd : FieldLabel
• fiveBarMatter : FieldLabel
• fiveMatter : FieldLabel
• tenMatter : FieldLabel

instance SuperSymmetry.SU5.instDecidableEqFieldLabel : DecidableEq FieldLabel

Equations

• SuperSymmetry.SU5.instDecidableEqFieldLabel x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance SuperSymmetry.SU5.instFintypeFieldLabel : Fintype FieldLabel

Equations

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

def SuperSymmetry.SU5.FieldLabel.RParity : FieldLabel → Fin 2

The R-Parity of a field, landding on 1 if it is in the non-trivial representation and 0 otherwise.

Equations

• SuperSymmetry.SU5.FieldLabel.fiveBarHu.RParity = 0
• SuperSymmetry.SU5.FieldLabel.fiveHu.RParity = 0
• SuperSymmetry.SU5.FieldLabel.fiveBarHd.RParity = 0
• SuperSymmetry.SU5.FieldLabel.fiveHd.RParity = 0
• SuperSymmetry.SU5.FieldLabel.fiveBarMatter.RParity = 1
• SuperSymmetry.SU5.FieldLabel.fiveMatter.RParity = 1
• SuperSymmetry.SU5.FieldLabel.tenMatter.RParity = 1