Completeness of Elems with regard to the NoExotics condition

i. Overview

In the module:

• PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.Elems

we define finite sets of elements of FluxesFive and FluxesTen which satisfy the NoExotics and HasNoZero conditions.

In this module we prove that these sets are complete, in the sense that every element of FluxesFive or FluxesTen which satisfies the NoExotics and HasNoZero conditions is contained in them.

Our proof follows by building allowed subsets of fluxes by their cardinality, and heavily relies on the decide tactic.

Note that the 10d fluxes are much more constrained than the 5-bar fluxes. This is because they are constrained by 3 SM representations Q, U, and E, whereas the 5-bar fluxes are only constrained by 2 SM representations D and L.

ii. Key results

• FluxesFive.noExotics_iff_mem_elemsNoExotics : An element of FluxesFive satisfies NoExotics and HasNoZero if and only if it is an element of elemsNoExotics.
• FluxesTen.noExotics_iff_mem_elemsNoExotics : An element of FluxesTen satisfies NoExotics and HasNoZero if and only if it is an element of elemsNoExotics.

iii. Table of contents

• A. All terms of FluxesFive obeying NoExotics and HasNoZero
  • A.1. The allowed fluxes in a FluxesFive which obeys NoExotics and HasNoZero
  • A.2. Sufficient condition for a set to contain allowed subsets of card n.succ based on n
  • A.3. Statement of the allowed subsets of each cardinality
  • A.4. Lemma that stated allowed subsets are complete
  • A.5. Terms of FluxesFive obeying NoExotics and HasNoZero have card ≤ 6
  • A.6. Terms of FluxesFive obeying NoExotics and HasNoZero are in elemsNoExotics
  • A.7. Terms of FluxesFive obey NoExotics and HasNoZero if and only if in elemsNoExotics
• B. All terms of FluxesTen obeying NoExotics and HasNoZero
  • B.1. The allowed fluxes in a FluxesTen which obeys NoExotics and HasNoZero
  • B.2. Sufficient condition for a set to contain allowed subsets of card n.succ based on n
  • B.3. Statement of the allowed subsets of each cardinality
  • B.4. Lemma that stated allowed subsets are complete
  • B.5. Terms of FluxesTen obeying NoExotics and HasNoZero have card ≤ 3
  • B.6. Terms of FluxesTen obeying NoExotics and HasNoZero are in elemsNoExotics
  • B.7. Terms of FluxesTen obey NoExotics and HasNoZero if and only if in elemsNoExotics

iv. References

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

A. All terms of FluxesFive obeying NoExotics and HasNoZero

A.1. The allowed fluxes in a FluxesFive which obeys NoExotics and HasNoZero

theorem FTheory.SU5.FluxesFive.mem_mem_finset_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (hnZ : F.HasNoZero) (x : Fluxes) (hx : x ∈ F) : x ∈ {{ M := 0, N := 1 }, { M := 0, N := 2 }, { M := 0, N := 3 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }, { M := 1, N := 2 }, { M := 2, N := -2 }, { M := 2, N := -1 }, { M := 2, N := 0 }, { M := 2, N := 1 }, { M := 3, N := -3 }, { M := 3, N := -2 }, { M := 3, N := -1 }, { M := 3, N := 0 }}

A.2. Sufficient condition for a set to contain allowed subsets of card n.succ based on n

theorem FTheory.SU5.FluxesFive.subset_le_mem_of_card_eq_succ {n : ℕ} {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset Fluxes) (hcard : S.card = n.succ) (hS : S ≤ F) {Y X : Finset (Multiset Fluxes)} (hY : ∀ (S : Multiset Fluxes), S.card = n → S ≤ F → S ∈ Y) (hX : ∀ a ∈ {{ M := 0, N := 1 }, { M := 0, N := 2 }, { M := 0, N := 3 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }, { M := 1, N := 2 }, { M := 2, N := -2 }, { M := 2, N := -1 }, { M := 2, N := 0 }, { M := 2, N := 1 }, { M := 3, N := -3 }, { M := 3, N := -2 }, { M := 3, N := -1 }, { M := 3, N := 0 }}, ∀ y ∈ Y, (Multiset.map (fun (x : Fluxes) => x.M + x.N) (a ::ₘ y)).sum ≤ 3 → (Multiset.map (fun (x : Fluxes) => x.M) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ X) : S ∈ X

A.3. Statement of the allowed subsets of each cardinality

def FTheory.SU5.FluxesFive.noExoticsSubsets (n : ℕ) : Finset (Multiset Fluxes)

The allowed subsets of a FluxesFive which has no exotics or zeros.

Equations

• One or more equations did not get rendered due to their size.
• FTheory.SU5.FluxesFive.noExoticsSubsets 0 = {∅}
• FTheory.SU5.FluxesFive.noExoticsSubsets 6 = {{{ M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }}}
• FTheory.SU5.FluxesFive.noExoticsSubsets n.succ.succ.succ.succ.succ.succ.succ = ∅

A.4. Lemma that stated allowed subsets are complete

theorem FTheory.SU5.FluxesFive.subset_of_fluxesFive_mem_noExoticsSubsets_of_noExotics {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset Fluxes) (hS : S ≤ F) : S ∈ noExoticsSubsets S.card

theorem FTheory.SU5.FluxesFive.subset_of_fluxesFive_mem_noExoticsSubsets_of_noExotics.recS {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) (n : ℕ) (S : Multiset Fluxes) : S.card = n → S ≤ F → S ∈ noExoticsSubsets n

A.5. Terms of FluxesFive obeying NoExotics and HasNoZero have card ≤ 6

theorem FTheory.SU5.FluxesFive.card_le_six_of_noExotics {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) : Multiset.card F ≤ 6

theorem FTheory.SU5.FluxesFive.card_mem_range_seven_of_noExotics {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) : Multiset.card F ∈ Finset.range 7

A.6. Terms of FluxesFive obeying NoExotics and HasNoZero are in elemsNoExotics

theorem FTheory.SU5.FluxesFive.mem_elemsNoExotics_of_noExotics (F : FluxesFive) (hNE : F.NoExotics) (hnZ : F.HasNoZero) : F ∈ elemsNoExotics

A.7. Terms of FluxesFive obey NoExotics and HasNoZero if and only if in elemsNoExotics

theorem FTheory.SU5.FluxesFive.noExotics_iff_mem_elemsNoExotics (F : FluxesFive) : F.NoExotics ∧ F.HasNoZero ↔ F ∈ elemsNoExotics

Completeness of elemsNoExotics, that is, every element of FluxesFive which obeys NoExotics is an element of elemsNoExotics, and every element of elemsNoExotics obeys NoExotics.

B. All terms of FluxesTen obeying NoExotics and HasNoZero

B.1. The allowed fluxes in a FluxesTen which obeys NoExotics and HasNoZero

theorem FTheory.SU5.FluxesTen.mem_mem_finset_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (hnZ : F.HasNoZero) (x : Fluxes) (hx : x ∈ F) : x ∈ {{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }, { M := 2, N := -1 }, { M := 2, N := 0 }, { M := 2, N := 1 }, { M := 3, N := 0 }}

B.2. Sufficient condition for a set to contain allowed subsets of card n.succ based on n

theorem FTheory.SU5.FluxesTen.subset_le_mem_of_card_eq_succ {n : ℕ} {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset Fluxes) (hcard : S.card = n.succ) (hS : S ≤ F) {Y X : Finset (Multiset Fluxes)} (hY : ∀ (S : Multiset Fluxes), S.card = n → S ≤ F → S ∈ Y) (hX : ∀ a ∈ {{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }, { M := 2, N := -1 }, { M := 2, N := 0 }, { M := 2, N := 1 }, { M := 3, N := 0 }}, ∀ y ∈ Y, (Multiset.map (fun (x : Fluxes) => x.M) (a ::ₘ y)).sum ≤ 3 → (Multiset.map (fun (x : Fluxes) => x.M - x.N) (a ::ₘ y)).sum ≤ 3 → (Multiset.map (fun (x : Fluxes) => x.M + x.N) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ X) : S ∈ X

B.3. Statement of the allowed subsets of each cardinality

def FTheory.SU5.FluxesTen.noExoticsSubsets (n : ℕ) : Finset (Multiset Fluxes)

The allowed subsets of a FluxesTen which has no exotics or zeros.

Equations

• One or more equations did not get rendered due to their size.
• FTheory.SU5.FluxesTen.noExoticsSubsets 0 = {∅}
• FTheory.SU5.FluxesTen.noExoticsSubsets 3 = {{{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }}, {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }}}
• FTheory.SU5.FluxesTen.noExoticsSubsets n.succ.succ.succ.succ = ∅

B.4. Lemma that stated allowed subsets are complete

theorem FTheory.SU5.FluxesTen.subset_of_fluxesTen_mem_noExoticsSubsets_of_noExotics {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset Fluxes) (hS : S ≤ F) : S ∈ noExoticsSubsets S.card

theorem FTheory.SU5.FluxesTen.subset_of_fluxesTen_mem_noExoticsSubsets_of_noExotics.recS {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero) (n : ℕ) (S : Multiset Fluxes) : S.card = n → S ≤ F → S ∈ noExoticsSubsets n

B.5. Terms of FluxesTen obeying NoExotics and HasNoZero have card ≤ 3

theorem FTheory.SU5.FluxesTen.card_le_three_of_noExotics {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero) : Multiset.card F ≤ 3

theorem FTheory.SU5.FluxesTen.card_mem_range_four_of_noExotics {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero) : Multiset.card F ∈ Finset.range 4

B.6. Terms of FluxesTen obeying NoExotics and HasNoZero are in elemsNoExotics

theorem FTheory.SU5.FluxesTen.mem_elemsNoExotics_of_noExotics (F : FluxesTen) (hNE : F.NoExotics) (hnZ : F.HasNoZero) : F ∈ elemsNoExotics

B.7. Terms of FluxesTen obey NoExotics and HasNoZero if and only if in elemsNoExotics

theorem FTheory.SU5.FluxesTen.noExotics_iff_mem_elemsNoExotics (F : FluxesTen) : F.NoExotics ∧ F.HasNoZero ↔ F ∈ elemsNoExotics

Completeness of elemsNoExotics, that is, every element of FluxesTen which obeys NoExotics is an element of elemsNoExotics, and every element of elemsNoExotics obeys NoExotics.