No exotics for 10d representations

In this module we give lemmas on the 10d matter content arising from the conditions of a valid spectrum.

Important results

• quantaTen_card_le_three : The number of 10d representations is less than or equal to three.
• quantaTen_chiralityFlux_mem : The multiset of chirality fluxes of matter content in the 10d representation satisfying ThreeChiralFamiles and ThreeLeptonDoublets must either be {1, 1, 1}, {1, 2}, or {3}.

theorem FTheory.SU5U1.MatterContent.quantaTen_chiralityFlux_nonneg' {I : CodimensionOneConfig} {𝓜 : MatterContent I} {a : QuantaTen I} (h3 : 𝓜.ThreeChiralFamiles) (h : a ∈ 𝓜.quantaTen) : 0 ≤ a.M

The chirality flux associated with a 10d representation must be non-negative.

theorem FTheory.SU5U1.MatterContent.quantaTen_chiralityFlux_nonneg {I : CodimensionOneConfig} {𝓜 : MatterContent I} {a : ChiralityFlux} (h3 : 𝓜.ThreeChiralFamiles) (h : a ∈ Multiset.map QuantaTen.M 𝓜.quantaTen) : 0 ≤ a

The chirality flux associated with a 5-bar representation must be non-negative.

theorem FTheory.SU5U1.MatterContent.quantaTen_chiralityFlux_ne_zero {I : CodimensionOneConfig} {𝓜 : MatterContent I} {a : ChiralityFlux} (he : 𝓜.NoExotics) (h : a ∈ Multiset.map QuantaTen.M 𝓜.quantaTen) : ¬a = 0

Due to the condition of having no exotics in the spectrum, the chirality flux of a 10d representation must be non-zero. This also uses the condition that the hypercharge flux and the chirality flux cannot both be zero.

theorem FTheory.SU5U1.MatterContent.quantaTen_chiralityFlux_pos {I : CodimensionOneConfig} {𝓜 : MatterContent I} {a : ChiralityFlux} (he : 𝓜.NoExotics) (h3 : 𝓜.ThreeChiralFamiles) (h : a ∈ Multiset.map QuantaTen.M 𝓜.quantaTen) : 0 < a

The chirality flux associated with a 5-bar representation must be non-negative.

theorem FTheory.SU5U1.MatterContent.quantaTen_chiralityFlux_filter_ne_zero_eq_self {I : CodimensionOneConfig} {𝓜 : MatterContent I} (he : 𝓜.NoExotics) : Multiset.filter (fun (x : ChiralityFlux) => ¬x = 0) (Multiset.map QuantaTen.M 𝓜.quantaTen) = Multiset.map QuantaTen.M 𝓜.quantaTen

theorem FTheory.SU5U1.MatterContent.quantaTen_chiralityFlux_le_three {I : CodimensionOneConfig} {𝓜 : MatterContent I} {a : QuantaTen I} (h3 : 𝓜.ThreeChiralFamiles) (h : a ∈ 𝓜.quantaTen) : a.M ≤ 3

The chirality flux associated with a 10d representation must be less then or equal to three.

theorem FTheory.SU5U1.MatterContent.quantaTen_chiralityFlux_card_le_three {I : CodimensionOneConfig} {𝓜 : MatterContent I} (he : 𝓜.NoExotics) (h3 : 𝓜.ThreeChiralFamiles) : (Multiset.map QuantaTen.M 𝓜.quantaTen).card ≤ 3

theorem FTheory.SU5U1.MatterContent.quantaTen_chiralityFlux_card_mem {I : CodimensionOneConfig} {𝓜 : MatterContent I} (he : 𝓜.NoExotics) (h3 : 𝓜.ThreeChiralFamiles) : (Multiset.map QuantaTen.M 𝓜.quantaTen).card ∈ {1, 2, 3}

theorem FTheory.SU5U1.MatterContent.quantaTen_card_le_three {I : CodimensionOneConfig} {𝓜 : MatterContent I} (he : 𝓜.NoExotics) (h3 : 𝓜.ThreeChiralFamiles) : 𝓜.quantaTen.card ≤ 3

The number of 10d representations is less than or equal to three.

theorem FTheory.SU5U1.MatterContent.quantaTen_chiralityFlux_mem {I : CodimensionOneConfig} {𝓜 : MatterContent I} (he : 𝓜.NoExotics) (h3 : 𝓜.ThreeChiralFamiles) : Multiset.map QuantaTen.M 𝓜.quantaTen ∈ {{1, 1, 1}, {1, 2}, {3}}

The multiset of chirality fluxes of matter content in the 10d representation satisfying NoExotics and ThreeChiralFamiles must either be

• {1, 1, 1}
• {1, 2}
• {3}