Completeness of Elems with regard to the NoExotics condition

In the module:

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

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

In this module we prove that these sets are complete, in the sense that every element of FluxesFive or FluxesTen which satisfies the NoExotics condition is contained in them. This statement corresponds to the following lemmas:

• FluxesFive.noExotics_iff_mem_elemsNoExotics
• FluxesTen.noExotics_iff_mem_elemsNoExotics

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.

Completeness for FluxesFive

theorem FTheory.SU5U1.FluxesFive.mem_mem_finset_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (hnZ : F.HasNoZero) (x : ℤ × ℤ) (hx : x ∈ F) : x ∈ {(0, 1), (0, 2), (0, 3), (1, -1), (1, 0), (1, 1), (1, 2), (2, -2), (2, -1), (2, 0), (2, 1), (3, -3), (3, -2), (3, -1), (3, 0)}

Allowed subsets of FluxesFive obeying NoExotics

theorem FTheory.SU5U1.FluxesFive.subset_le_mem_of_card_eq_one {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : S.card = 1) (hS : S ≤ F) : S ∈ {{(0, 1)}, {(0, 2)}, {(0, 3)}, {(1, -1)}, {(1, 0)}, {(1, 1)}, {(1, 2)}, {(2, -2)}, {(2, -1)}, {(2, 0)}, {(2, 1)}, {(3, -3)}, {(3, -2)}, {(3, -1)}, {(3, 0)}}

theorem FTheory.SU5U1.FluxesFive.subset_le_mem_of_card_eq_two {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : S.card = 2) (hS : S ≤ F) : S ∈ {{(0, 1), (0, 1)}, {(0, 1), (1, -1)}, {(0, 1), (1, 0)}, {(0, 1), (0, 2)}, {(0, 1), (1, 1)}, {(0, 1), (2, -2)}, {(0, 1), (2, -1)}, {(0, 1), (2, 0)}, {(0, 1), (3, -3)}, {(0, 1), (3, -2)}, {(0, 1), (3, -1)}, {(0, 2), (1, -1)}, {(0, 2), (1, 0)}, {(0, 2), (2, -2)}, {(0, 2), (2, -1)}, {(0, 2), (3, -3)}, {(0, 2), (3, -2)}, {(0, 3), (1, -1)}, {(0, 3), (2, -2)}, {(0, 3), (3, -3)}, {(1, -1), (1, -1)}, {(1, -1), (1, 0)}, {(1, -1), (1, 1)}, {(1, -1), (1, 2)}, {(1, -1), (2, -2)}, {(1, -1), (2, -1)}, {(1, -1), (2, 0)}, {(1, 0), (1, 0)}, {(1, -1), (2, 1)}, {(1, 0), (1, 1)}, {(1, 0), (2, -2)}, {(1, 0), (2, -1)}, {(1, 0), (2, 0)}, {(1, 1), (2, -2)}, {(1, 1), (2, -1)}, {(1, 2), (2, -2)}}

theorem FTheory.SU5U1.FluxesFive.subset_le_mem_of_card_eq_three {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : S.card = 3) (hS : S ≤ F) : S ∈ {{(0, 1), (0, 1), (0, 1)}, {(0, 1), (0, 1), (1, -1)}, {(0, 1), (0, 1), (1, 0)}, {(0, 1), (0, 1), (2, -2)}, {(0, 1), (0, 1), (2, -1)}, {(0, 1), (0, 1), (3, -3)}, {(0, 1), (0, 1), (3, -2)}, {(0, 1), (0, 2), (1, -1)}, {(0, 1), (0, 2), (2, -2)}, {(0, 1), (0, 2), (3, -3)}, {(0, 1), (1, -1), (1, -1)}, {(0, 1), (1, -1), (1, 0)}, {(0, 1), (1, -1), (1, 1)}, {(0, 1), (1, -1), (2, -2)}, {(0, 1), (1, -1), (2, -1)}, {(0, 1), (1, -1), (2, 0)}, {(0, 1), (1, 0), (1, 0)}, {(0, 1), (1, 0), (2, -2)}, {(0, 1), (1, 0), (2, -1)}, {(0, 1), (1, 1), (2, -2)}, {(0, 2), (1, -1), (1, -1)}, {(0, 2), (1, -1), (1, 0)}, {(0, 2), (1, -1), (2, -2)}, {(0, 2), (1, -1), (2, -1)}, {(0, 2), (1, 0), (2, -2)}, {(0, 3), (1, -1), (1, -1)}, {(0, 3), (1, -1), (2, -2)}, {(1, -1), (1, -1), (1, -1)}, {(1, -1), (1, -1), (1, 0)}, {(1, -1), (1, -1), (1, 1)}, {(1, -1), (1, -1), (1, 2)}, {(1, -1), (1, 0), (1, 0)}, {(1, -1), (1, 0), (1, 1)}, {(1, 0), (1, 0), (1, 0)}}

theorem FTheory.SU5U1.FluxesFive.subset_le_mem_of_card_eq_four {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : S.card = 4) (hS : S ≤ F) : S ∈ {{(0, 1), (0, 1), (0, 1), (1, -1)}, {(0, 1), (0, 1), (0, 1), (2, -2)}, {(0, 1), (0, 1), (0, 1), (3, -3)}, {(0, 1), (0, 1), (1, -1), (1, -1)}, {(0, 1), (0, 1), (1, -1), (1, 0)}, {(0, 1), (0, 1), (1, -1), (2, -2)}, {(0, 1), (0, 1), (1, -1), (2, -1)}, {(0, 1), (0, 1), (1, 0), (2, -2)}, {(0, 1), (0, 2), (1, -1), (1, -1)}, {(0, 1), (0, 2), (1, -1), (2, -2)}, {(0, 1), (1, -1), (1, -1), (1, -1)}, {(0, 1), (1, -1), (1, -1), (1, 0)}, {(0, 1), (1, -1), (1, -1), (1, 1)}, {(0, 1), (1, -1), (1, 0), (1, 0)}, {(0, 2), (1, -1), (1, -1), (1, -1)}, {(0, 2), (1, -1), (1, -1), (1, 0)}, {(0, 3), (1, -1), (1, -1), (1, -1)}}

theorem FTheory.SU5U1.FluxesFive.subset_le_mem_of_card_eq_five {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : S.card = 5) (hS : S ≤ F) : S ∈ {{(0, 1), (0, 1), (0, 1), (1, -1), (1, -1)}, {(0, 1), (0, 1), (0, 1), (1, -1), (2, -2)}, {(0, 1), (0, 1), (1, -1), (1, -1), (1, -1)}, {(0, 1), (0, 1), (1, -1), (1, -1), (1, 0)}, {(0, 1), (0, 2), (1, -1), (1, -1), (1, -1)}}

theorem FTheory.SU5U1.FluxesFive.subset_le_mem_of_card_eq_six {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : S.card = 6) (hS : S ≤ F) : S ∈ {{(0, 1), (0, 1), (0, 1), (1, -1), (1, -1), (1, -1)}}

theorem FTheory.SU5U1.FluxesFive.subset_le_mem_of_card_eq_seven {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : S.card = 7) (hS : S ≤ F) : S ∈ ∅

theorem FTheory.SU5U1.FluxesFive.subset_le_mem_of_card_eq_seven_add {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) {n : ℕ} (hcard : S.card = 7 + n) (hS : S ≤ F) : S ∈ ∅

theorem FTheory.SU5U1.FluxesFive.subset_le_mem_of_card_ge_seven {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : 7 ≤ S.card) (hS : S ≤ F) : S ∈ ∅

Resulting properties on FluxesFive with NoExotics

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

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

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

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

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

Completeness for FluxesTen

theorem FTheory.SU5U1.FluxesTen.mem_mem_finset_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (hnZ : F.HasNoZero) (x : ℤ × ℤ) (hx : x ∈ F) : x ∈ {(1, -1), (1, 0), (1, 1), (2, -1), (2, 0), (2, 1), (3, 0)}

Allowed subsets of FluxesTen obeying NoExotics

theorem FTheory.SU5U1.FluxesTen.subset_le_mem_of_card_eq_one {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : S.card = 1) (hS : S ≤ F) : S ∈ {{(1, -1)}, {(1, 0)}, {(1, 1)}, {(2, -1)}, {(2, 0)}, {(2, 1)}, {(3, 0)}}

theorem FTheory.SU5U1.FluxesTen.subset_le_mem_of_card_eq_two {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : S.card = 2) (hS : S ≤ F) : S ∈ {{(1, -1), (1, 0)}, {(1, -1), (1, 1)}, {(1, -1), (2, 1)}, {(1, 0), (1, 0)}, {(1, 0), (1, 1)}, {(1, 0), (2, 0)}, {(1, 1), (2, -1)}}

theorem FTheory.SU5U1.FluxesTen.subset_le_mem_of_card_eq_three {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : S.card = 3) (hS : S ≤ F) : S ∈ {{(1, -1), (1, 0), (1, 1)}, {(1, 0), (1, 0), (1, 0)}}

theorem FTheory.SU5U1.FluxesTen.subset_le_mem_of_card_eq_four {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : S.card = 4) (hS : S ≤ F) : S ∈ ∅

theorem FTheory.SU5U1.FluxesTen.subset_le_mem_of_card_eq_four_add {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) {n : ℕ} (hcard : S.card = 4 + n) (hS : S ≤ F) : S ∈ ∅

theorem FTheory.SU5U1.FluxesTen.subset_le_mem_of_card_ge_four {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero) (S : Multiset (ℤ × ℤ)) (hcard : 4 ≤ S.card) (hS : S ≤ F) : S ∈ ∅

Resulting properties on FluxesTen with NoExotics

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

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

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

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

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