Minimally allows terms

Given a set of charges x : Charges corresponding to charges of the representations present in the thoery, and a potential term T : PotentialTerm, we say that x minimally allows T if it allows the term T and no proper subset of x allows T.

def FTheory.SU5U1.Charges.MinimallyAllowsTerm (x : Charges) (T : SuperSymmetry.SU5.PotentialTerm) : Prop

A collection of charges x : Charges is said to minimally allow the potential term T if it allows T and no strict subset of it allows T.

Equations

• x.MinimallyAllowsTerm T = ∀ y ∈ x.powerset, y = x ↔ y.AllowsTerm T

instance FTheory.SU5U1.Charges.instDecidableMinimallyAllowsTerm (x : Charges) (T : SuperSymmetry.SU5.PotentialTerm) : Decidable (x.MinimallyAllowsTerm T)

Equations

• x.instDecidableMinimallyAllowsTerm T = inferInstanceAs (Decidable (∀ y ∈ x.powerset, y = x ↔ y.AllowsTerm T))

theorem FTheory.SU5U1.Charges.allowsTerm_of_minimallyAllowsTerm {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} (h : x.MinimallyAllowsTerm T) : x.AllowsTerm T

theorem FTheory.SU5U1.Charges.allowsTerm_of_has_minimallyAllowsTerm_subset {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} (hx : ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T) : x.AllowsTerm T

theorem FTheory.SU5U1.Charges.minimallyAllowsTerm_iff_powerset_filter_eq {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} : x.MinimallyAllowsTerm T ↔ {y ∈ x.powerset | y.AllowsTerm T} = {x}

theorem FTheory.SU5U1.Charges.minimallyAllowsTerm_iff_powerset_countP_eq_one {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} : x.MinimallyAllowsTerm T ↔ Multiset.countP (fun (y : Charges) => y.AllowsTerm T) x.powerset.val = 1

theorem FTheory.SU5U1.Charges.subset_minimallyAllowsTerm_of_allowsTerm {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} (hx : x.AllowsTerm T) : ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T

theorem FTheory.SU5U1.Charges.allowsTerm_iff_subset_minimallyAllowsTerm {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} : x.AllowsTerm T ↔ ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T

theorem FTheory.SU5U1.Charges.card_le_degree_of_minimallyAllowsTerm {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} (h : x.MinimallyAllowsTerm T) : x.card ≤ T.degree

theorem FTheory.SU5U1.Charges.eq_allowsTermForm_of_minimallyAllowsTerm {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} (h1 : x.MinimallyAllowsTerm T) : ∃ (a : ℤ) (b : ℤ) (c : ℤ), x = allowsTermForm a b c T

theorem FTheory.SU5U1.Charges.allowsTermForm_minimallyAllowsTerm {a b c : ℤ} {T : SuperSymmetry.SU5.PotentialTerm} (hT : T ≠ SuperSymmetry.SU5.PotentialTerm.W1 ∧ T ≠ SuperSymmetry.SU5.PotentialTerm.W2) : (allowsTermForm a b c T).MinimallyAllowsTerm T