Elements of FluxesFive and FluxesTen with no chiral exotics

There are only a finite number of elements of FluxesFive and FluxesTen which do not lead to chiral exotics in the spectrum.

These elements are given in the definitions elemsNoExotics in the respective namespaces.

For FluxesFive there are 31 such elements, and for FluxesTen there are 6 such elements.

def FTheory.SU5U1.FluxesFive.elemsNoExotics : Multiset FluxesFive

The elements of FluxesFive for which the NoExotics condition holds.

Equations

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

theorem FTheory.SU5U1.FluxesFive.elemsNoExotics_card : elemsNoExotics.card = 31

theorem FTheory.SU5U1.FluxesFive.elemsNoExotics_nodup : elemsNoExotics.Nodup

theorem FTheory.SU5U1.FluxesFive.noExotics_of_mem_elemsNoExotics (F : FluxesFive) (h : F ∈ elemsNoExotics) : F.NoExotics

theorem FTheory.SU5U1.FluxesFive.toFinset_card_le_four_mem_elemsNoExotics (F : FluxesFive) (h : F ∈ elemsNoExotics) : (Multiset.toFinset F).card ≤ 4

theorem FTheory.SU5U1.FluxesFive.sum_of_mem_elemsNoExotics (F : FluxesFive) (h : F ∈ elemsNoExotics) : Multiset.sum F = (3, 0)

theorem FTheory.SU5U1.FluxesFive.hasNoZero_of_mem_elemsNoExotics (F : FluxesFive) (h : F ∈ elemsNoExotics) : F.HasNoZero

def FTheory.SU5U1.FluxesTen.elemsNoExotics : Multiset FluxesTen

The elements of FluxesTen for which the NoExotics condition holds.

Equations

• FTheory.SU5U1.FluxesTen.elemsNoExotics = {{(1, 0), (1, 0), (1, 0)}, {(1, 1), (1, -1), (1, 0)}, {(1, 0), (2, 0)}, {(1, -1), (2, 1)}, {(1, 1), (2, -1)}, {(3, 0)}}

theorem FTheory.SU5U1.FluxesTen.elemsNoExotics_card : elemsNoExotics.card = 6

theorem FTheory.SU5U1.FluxesTen.elemsNoExotics_nodup : elemsNoExotics.Nodup

theorem FTheory.SU5U1.FluxesTen.noExotics_of_mem_elemsNoExotics (F : FluxesTen) (h : F ∈ elemsNoExotics) : F.NoExotics

theorem FTheory.SU5U1.FluxesTen.toFinset_card_le_three_mem_elemsNoExotics (F : FluxesTen) (h : F ∈ elemsNoExotics) : (Multiset.toFinset F).card ≤ 3

theorem FTheory.SU5U1.FluxesTen.sum_of_mem_elemsNoExotics (F : FluxesTen) (h : F ∈ elemsNoExotics) : Multiset.sum F = (3, 0)

theorem FTheory.SU5U1.FluxesTen.hasNoZero_of_mem_elemsNoExotics (F : FluxesTen) (h : F ∈ elemsNoExotics) : F.HasNoZero