Terms of FluxesFive and FluxesTen with no chiral exotics

i. Overview

In this module we give the terms of type FluxesFive and FluxesTen which obey the NoExotics and HasNoZero propositions.

In each case, there is only a finite set of such elements, which we give explicitly. We show that these sets are complete in the module StringTheory.FTheory.SU5.Fluxes.NoExotics.Completeness.

This module is reserved for the explicit sets of elements, and simple lemmas about the elements of those elements.

ii. Key results

• FluxesFive.elemsNoExotics : The multiset of elements of FluxesFive which obey NoExotics and HasNoZero.
• FluxesTen.elemsNoExotics : The multiset of elements of FluxesTen which obey NoExotics and HasNoZero.

iii. Table of contents

• A. The multiset sets of FluxesFive with no chiral exotics and no zero fluxes
  • A.1. The definition of the multiset
  • A.2. The cardinality of the multiset is 31
  • A.3. The multiset has no duplicates
  • A.4. Every element of the multiset obeys NoExotics
  • A.5. Every element of the multiset has at most 4 distinct flux pairs
  • A.6. Every element of the multiset has at most 6 flux pairs
  • A.7. The sum of all flux-pairs in any element of the multiset is (3, 0)
  • A.8. Every element of the multiset obeys HasNoZero
  • A.9. A sum relation for subsets of elements of the multiset
• B. The multiset sets of FluxesFive with no chiral exotics and no zero fluxes
  • B.1. The definition of the multiset
  • B.2. The cardinality of the multiset is 6
  • B.3. The multiset has no duplicates
  • B.4. Every element of the multiset obeys NoExotics
  • B.5. Every element of the multiset has at most 3 distinct flux pairs
  • B.6. The sum of all flux-pairs in any element of the multiset is (3, 0)
  • B.7. Every element of the multiset obeys HasNoZero

iv. References

There are no known references for the material in this module.

A. The multiset sets of FluxesFive with no chiral exotics and no zero fluxes

A.1. The definition of the multiset

def FTheory.SU5.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.

A.2. The cardinality of the multiset is 31

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

A.3. The multiset has no duplicates

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

A.4. Every element of the multiset obeys NoExotics

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

A.5. Every element of the multiset has at most 4 distinct flux pairs

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

A.6. Every element of the multiset has at most 6 flux pairs

theorem FTheory.SU5.FluxesFive.card_le_six_mem_elemsNoExotics (F : FluxesFive) (h : F ∈ elemsNoExotics) : Multiset.card F ≤ 6

A.7. The sum of all flux-pairs in any element of the multiset is (3, 0)

theorem FTheory.SU5.FluxesFive.sum_of_mem_elemsNoExotics (F : FluxesFive) (h : F ∈ elemsNoExotics) : Multiset.sum F = { M := 3, N := 0 }

A.8. Every element of the multiset obeys HasNoZero

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

A.9. A sum relation for subsets of elements of the multiset

theorem FTheory.SU5.FluxesFive.map_sum_add_of_mem_powerset_elemsNoExotics (F S : FluxesFive) (hf : F ∈ elemsNoExotics) (hS : S ∈ Multiset.powerset F) : (Multiset.map (fun (x : Fluxes) => { M := |x.M|, N := -|x.M| }) S).sum + (Multiset.map (fun (x : Fluxes) => { M := 0, N := |x.M + x.N| }) S).sum = Multiset.sum S

B. The multiset sets of FluxesFive with no chiral exotics and no zero fluxes

B.1. The definition of the multiset

def FTheory.SU5.FluxesTen.elemsNoExotics : Multiset FluxesTen

The elements of FluxesTen for which the NoExotics condition holds.

Equations

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

B.2. The cardinality of the multiset is 6

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

B.3. The multiset has no duplicates

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

B.4. Every element of the multiset obeys NoExotics

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

B.5. Every element of the multiset has at most 3 distinct flux pairs

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

B.6. The sum of all flux-pairs in any element of the multiset is (3, 0)

theorem FTheory.SU5.FluxesTen.sum_of_mem_elemsNoExotics (F : FluxesTen) (h : F ∈ elemsNoExotics) : Multiset.sum F = { M := 3, N := 0 }

B.7. Every element of the multiset obeys HasNoZero

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