Conditions on matter content to no exotics

https://arxiv.org/pdf/1401.5084

• Condition (26) for the requirement of three chiral familes.
• Condition (27) and (28) for no exotics in the spectrum.
• Condition (29) for the three lepton doublets with exactly one pair of Higges.

References

see also: https://arxiv.org/pdf/1011.2212

def FTheory.SU5U1.MatterContent.ThreeChiralFamiles {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Prop

The condition on the matter content for there to exist three chiral familes.

This corresponds to the conditons that:

• ∑ₐ Mₐ = 3
• ∑ᵢ Mᵢ = 3
• 0 ≤ Mₐ
• 0 ≤ Mᵢ

Ref: Equation (26) of arXiv:1401.5084.

Equations

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

instance FTheory.SU5U1.MatterContent.instDecidableThreeChiralFamiles {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Decidable 𝓜.ThreeChiralFamiles

Equations

• 𝓜.instDecidableThreeChiralFamiles = instDecidableAnd

def FTheory.SU5U1.MatterContent.NoExotics {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Prop

The condition on the matter content for there to be no exotics in the spectrum.

This corresponds to the conditions that:

• ∑ₐ Nₐ = 0
• ∑ᵢ Nᵢ = 0
• - Mₐ ≤ Nₐ ≤ Mₐ
• - Mᵢ - 1 ≤ Nᵢ ≤ 3

Ref: Equation (27) and (28) of arXiv:1401.5084.

Equations

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

instance FTheory.SU5U1.MatterContent.instDecidableNoExotics {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Decidable 𝓜.NoExotics

Equations

• 𝓜.instDecidableNoExotics = instDecidableAnd

def FTheory.SU5U1.MatterContent.ThreeLeptonDoublets {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Prop

The condition on the matter content for there to be three lepton doublets with exactly one pair of Higgs.

This corresponds to the conditions that:

• ∑ᵢ |Mᵢ + Nᵢ| = 5

Ref: Equation (29) of arXiv:1401.5084.

Equations

• 𝓜.ThreeLeptonDoublets = ((Multiset.map (fun (a : FTheory.SU5U1.QuantaBarFive I) => |a.M + a.N|) 𝓜.quantaBarFive).sum = 5)

instance FTheory.SU5U1.MatterContent.instDecidableThreeLeptonDoublets {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Decidable 𝓜.ThreeLeptonDoublets

Equations

• 𝓜.instDecidableThreeLeptonDoublets = decEq (Multiset.map (fun (a : FTheory.SU5U1.QuantaBarFive I) => |a.M + a.N|) 𝓜.quantaBarFive).sum 5

Condition on Higges

def FTheory.SU5U1.MatterContent.IsUpHiggs {I : CodimensionOneConfig} (a : QuantaBarFive I) : Prop

The quanta of a bar-5 representation corresponds to an up-type higgs if it has zero chirality flux and negative one hypercharge.

Ref: This is used in arXiv:1507.05961 with no explanation. It is also referenced in arXiv:1011.2212.

Equations

• FTheory.SU5U1.MatterContent.IsUpHiggs a = (a.M = 0 ∧ a.N = -1)

instance FTheory.SU5U1.MatterContent.instDecidablePredQuantaBarFiveIsUpHiggs {I : CodimensionOneConfig} : DecidablePred IsUpHiggs

Equations

• FTheory.SU5U1.MatterContent.instDecidablePredQuantaBarFiveIsUpHiggs x✝ = instDecidableAnd

def FTheory.SU5U1.MatterContent.IsDownHiggs {I : CodimensionOneConfig} (a : QuantaBarFive I) : Prop

The quanta of a bar-5 representation corresponds to an down-type higgs if it has zero chirality flux and positive on hypercharge.

Ref: This is used in arXiv:1507.05961 with no explanation. It is also referenced in arXiv:1011.2212.

Equations

• FTheory.SU5U1.MatterContent.IsDownHiggs a = (a.M = 0 ∧ a.N = 1)

instance FTheory.SU5U1.MatterContent.instDecidablePredQuantaBarFiveIsDownHiggs {I : CodimensionOneConfig} : DecidablePred IsDownHiggs

Equations

• FTheory.SU5U1.MatterContent.instDecidablePredQuantaBarFiveIsDownHiggs x✝ = instDecidableAnd

def FTheory.SU5U1.MatterContent.HasExclusiveHigges {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Prop

The condition on the matter content for there to be exactly one 5-bar representation corresponding to IsUpHiggs and one corresponding to IsDownHiggs.

Equations

• 𝓜.HasExclusiveHigges = (Multiset.countP FTheory.SU5U1.MatterContent.IsUpHiggs 𝓜.quantaBarFive = 1 ∧ Multiset.countP FTheory.SU5U1.MatterContent.IsDownHiggs 𝓜.quantaBarFive = 1)

instance FTheory.SU5U1.MatterContent.instDecidableHasExclusiveHigges {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Decidable 𝓜.HasExclusiveHigges

Equations

• 𝓜.instDecidableHasExclusiveHigges = instDecidableAnd

Combined conditions

def FTheory.SU5U1.MatterContent.ValidMatterSpectrum {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Prop

The condition on the matter content for it to produce a valid spectrum.

Equations

• 𝓜.ValidMatterSpectrum = (𝓜.ThreeChiralFamiles ∧ 𝓜.NoExotics ∧ 𝓜.ThreeLeptonDoublets ∧ 𝓜.HasExclusiveHigges)

instance FTheory.SU5U1.MatterContent.instDecidableValidMatterSpectrum {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Decidable 𝓜.ValidMatterSpectrum

Equations

• 𝓜.instDecidableValidMatterSpectrum = instDecidableAnd