Fluxes into list

The types FluxesFive and FluxesTen are defined as multisets, but when combining them with charges, they are needed as lists. Usually turning a multiset into a list is done using choice, and therefore is not computable. However, in the cases when NoExotics and HasNoZero hold, the elements of FluxesFive and FluxesTen are known. Thus we can use those elements to construct a list of the fluxes from multisets, in a way which is computable. This file provides the definitions and lemmas needed to do this.

FluxesFive to lists

def FTheory.SU5U1.FluxesFive.allowedPairs : List (ℤ × ℤ)

The allowed pairs of fluxes in FluxesFive which have no exotics.

This can be found using: (elemsNoExotics.bind (fun x => x.1)).toFinset

Equations

• FTheory.SU5U1.FluxesFive.allowedPairs = [(1, -1), (2, 1), (1, 0), (2, 0), (1, 1), (2, -1), (1, 2), (2, -2), (3, -3), (0, 3), (3, -2), (0, 2), (3, -1), (0, 1), (3, 0)]

theorem FTheory.SU5U1.FluxesFive.mem_allowedPairs_count_one (x : ℤ × ℤ) (hx : x ∈ allowedPairs) : List.count x allowedPairs = 1

theorem FTheory.SU5U1.FluxesFive.mem_allowedPairs_of_mem_noExotics (F : FluxesFive) (hf : F.NoExotics ∧ F.HasNoZero) (x : ℤ × ℤ) (h : x ∈ F) : x ∈ allowedPairs

def FTheory.SU5U1.FluxesFive.toList (F : FluxesFive) : List (ℤ × ℤ)

Constructs a list of ℤ × ℤ from a F : FluxesFive, if F is obeys NoExotics and HasNoZero, then this returns a list equivalent to the underlying multiset of F, else it returns junk.

Equations

• F.toList = List.flatMap (fun (x : ℤ × ℤ) => List.replicate (Multiset.count x F) x) FTheory.SU5U1.FluxesFive.allowedPairs

theorem FTheory.SU5U1.FluxesFive.mem_allowedPairs_of_mem_toList (F : FluxesFive) (x : ℤ × ℤ) (h : x ∈ F.toList) : x ∈ allowedPairs

theorem FTheory.SU5U1.FluxesFive.zero_not_mem_toList (F : FluxesFive) : (0, 0) ∉ F.toList

theorem FTheory.SU5U1.FluxesFive.mem_toList_iff {F : FluxesFive} (hf : F.NoExotics ∧ F.HasNoZero) {a : ℤ × ℤ} : a ∈ F.toList ↔ a ∈ F

theorem FTheory.SU5U1.FluxesFive.toList_count {F : FluxesFive} {a : ℤ × ℤ} (hf : F.NoExotics ∧ F.HasNoZero) (hmema : a ∈ allowedPairs) : List.count a F.toList = Multiset.count a F

theorem FTheory.SU5U1.FluxesFive.coe_toList (F : FluxesFive) (h : F.NoExotics ∧ F.HasNoZero) : ↑F.toList = F

theorem FTheory.SU5U1.FluxesFive.toList_length (F : FluxesFive) (h : F.NoExotics ∧ F.HasNoZero) : F.toList.length = Multiset.card F

FluxesTen to lists

def FTheory.SU5U1.FluxesTen.allowedPairs : List (ℤ × ℤ)

The allowed pairs of fluxes in FluxesTen which have no exotics.

This can be found using: (elemsNoExotics.bind (fun x => x.1)).toFinset

Equations

• FTheory.SU5U1.FluxesTen.allowedPairs = [(1, 0), (2, 0), (1, -1), (2, 1), (1, 1), (2, -1), (3, 0)]

theorem FTheory.SU5U1.FluxesTen.mem_allowedPairs_count_one (x : ℤ × ℤ) (hx : x ∈ allowedPairs) : List.count x allowedPairs = 1

theorem FTheory.SU5U1.FluxesTen.mem_allowedPairs_of_mem_noExotics (F : FluxesTen) (hf : F.NoExotics ∧ F.HasNoZero) (x : ℤ × ℤ) (h : x ∈ F) : x ∈ allowedPairs

def FTheory.SU5U1.FluxesTen.toList (F : FluxesTen) : List (ℤ × ℤ)

Constructs a list of ℤ × ℤ from a F : FluxesTen, if F is obeys NoExotics and HasNoZero, then this returns a list equivalent to the underlying multiset of F, else it returns junk.

Equations

• F.toList = List.flatMap (fun (x : ℤ × ℤ) => List.replicate (Multiset.count x F) x) FTheory.SU5U1.FluxesTen.allowedPairs

theorem FTheory.SU5U1.FluxesTen.mem_allowedPairs_of_mem_toList (F : FluxesTen) (x : ℤ × ℤ) (h : x ∈ F.toList) : x ∈ allowedPairs

theorem FTheory.SU5U1.FluxesTen.zero_not_mem_toList (F : FluxesTen) : (0, 0) ∉ F.toList

theorem FTheory.SU5U1.FluxesTen.mem_toList_iff {F : FluxesTen} (hf : F.NoExotics ∧ F.HasNoZero) {a : ℤ × ℤ} : a ∈ F.toList ↔ a ∈ F

theorem FTheory.SU5U1.FluxesTen.toList_count {F : FluxesTen} {a : ℤ × ℤ} (hf : F.NoExotics ∧ F.HasNoZero) (hmema : a ∈ allowedPairs) : List.count a F.toList = Multiset.count a F

theorem FTheory.SU5U1.FluxesTen.coe_toList (F : FluxesTen) (h : F.NoExotics ∧ F.HasNoZero) : ↑F.toList = F

theorem FTheory.SU5U1.FluxesTen.toList_length (F : FluxesTen) (h : F.NoExotics ∧ F.HasNoZero) : F.toList.length = Multiset.card F