Charges allowing terms

The charges of representations x : Charges allow a potential term T : PotentialTerm if the zero charge is in the set of charges associated with that potential term.

We define this proposition AllowsTerm and prove results about it.

We also define allowsTermForm, which is a function that takes three integers a, b, and c and a potential term T, and returns a Charges that allows the term T. We prove that any charges that allows a term T has a subset which can be expressed as allowsTermForm a b c T for some integers a, b, and c.

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

The charges of representations x : Charges allow a potential term T : PotentialTerm if the zero charge is in the set of charges associated with that potential term.

Equations

• x.AllowsTerm T = (0 ∈ x.ofPotentialTerm T)

theorem FTheory.SU5U1.Charges.allowsTerm_iff_zero_mem_ofPotentialTerm' {x : Charges} {T : SuperSymmetry.SU5.PotentialTerm} : x.AllowsTerm T ↔ 0 ∈ x.ofPotentialTerm' T

instance FTheory.SU5U1.Charges.instDecidableAllowsTerm (x : Charges) (T : SuperSymmetry.SU5.PotentialTerm) : Decidable (x.AllowsTerm T)

Equations

• x.instDecidableAllowsTerm T = decidable_of_iff (0 ∈ x.ofPotentialTerm' T) ⋯

theorem FTheory.SU5U1.Charges.allowsTerm_of_subset {T : SuperSymmetry.SU5.PotentialTerm} {y x : Charges} (h : y ⊆ x) (hy : y.AllowsTerm T) : x.AllowsTerm T

allowsTermForm

def FTheory.SU5U1.Charges.allowsTermForm (a b c : ℤ) (T : SuperSymmetry.SU5.PotentialTerm) : Charges

A element of Charges from three intergers a b c : ℤ for a given potential term T. Defined such that allowsTermForm a b c T always allows the potential term T, and if any over charge x allows T then it is due to a subset of the form allowsTermForm a b c T.

Equations

• FTheory.SU5U1.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.μ = (some a, some a, ∅, ∅)
• FTheory.SU5U1.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.β = (none, some a, {a}, ∅)
• FTheory.SU5U1.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.Λ = (none, none, {a, b}, {-a - b})
• FTheory.SU5U1.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.W1 = (none, none, {-a - b - c}, {a, b, c})
• FTheory.SU5U1.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.W2 = (some (-a - b - c), none, ∅, {a, b, c})
• FTheory.SU5U1.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.W3 = (none, some (-a), {b, -b - 2 * a}, ∅)
• FTheory.SU5U1.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.W4 = (some (-c - 2 * b), some (-b), {c}, ∅)
• FTheory.SU5U1.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.K1 = (none, none, {-a}, {b, -a - b})
• FTheory.SU5U1.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.K2 = (some a, some b, ∅, {-a - b})
• FTheory.SU5U1.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.topYukawa = (none, some (-a), ∅, {b, -a - b})
• FTheory.SU5U1.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.bottomYukawa = (some a, none, {b}, {-a - b})

theorem FTheory.SU5U1.Charges.allowsTermForm_allowsTerm {a b c : ℤ} {T : SuperSymmetry.SU5.PotentialTerm} : (allowsTermForm a b c T).AllowsTerm T

theorem FTheory.SU5U1.Charges.allowsTerm_of_eq_allowsTermForm {T : SuperSymmetry.SU5.PotentialTerm} (x : Charges) (h : ∃ (a : ℤ) (b : ℤ) (c : ℤ), x = allowsTermForm a b c T) : x.AllowsTerm T

theorem FTheory.SU5U1.Charges.allowsTermForm_eq_of_subset {a b c a' b' c' : ℤ} {T : SuperSymmetry.SU5.PotentialTerm} (h : allowsTermForm a b c T ⊆ allowsTermForm a' b' c' T) (hT : T ≠ SuperSymmetry.SU5.PotentialTerm.W1 ∧ T ≠ SuperSymmetry.SU5.PotentialTerm.W2) : allowsTermForm a b c T = allowsTermForm a' b' c' T

theorem FTheory.SU5U1.Charges.allowsTermForm_card_le_degree {a b c : ℤ} {T : SuperSymmetry.SU5.PotentialTerm} : (allowsTermForm a b c T).card ≤ T.degree

theorem FTheory.SU5U1.Charges.allowsTermForm_subset_allowsTerm_of_allowsTerm {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} (h : x.AllowsTerm T) : ∃ (a : ℤ) (b : ℤ) (c : ℤ), allowsTermForm a b c T ⊆ x ∧ (allowsTermForm a b c T).AllowsTerm T

theorem FTheory.SU5U1.Charges.subset_card_le_degree_allowsTerm_of_allowsTerm {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} (h : x.AllowsTerm T) : ∃ y ∈ x.powerset, y.card ≤ T.degree ∧ y.AllowsTerm T