Yukawa charges

This module includes the charges associated with the Yukawa terms in the superpotential. It also asks the following question: Do the singlets needed to regenerate the Yukawa terms regenerate a dangerous coupling in the superpotential with up to n insertions of the Yukawa singlets? This questions is manifested in the YukawaGeneratesDangerousAtLevel predicate.

def SuperSymmetry.SU5.Charges.ofYukawaTerms (x : Charges) : Multiset ℤ

The collection of charges associated with Yukawa terms. Correspondingly, the (negative) of the charges of the singlets needed to regenerate all Yukawa terms in the potential.

Equations

• x.ofYukawaTerms = x.ofPotentialTerm SuperSymmetry.SU5.PotentialTerm.topYukawa + x.ofPotentialTerm SuperSymmetry.SU5.PotentialTerm.bottomYukawa

theorem SuperSymmetry.SU5.Charges.ofYukawaTerms_subset_of_subset {x y : Charges} (h : x ⊆ y) : x.ofYukawaTerms ⊆ y.ofYukawaTerms

def SuperSymmetry.SU5.Charges.ofYukawaTermsNSum (x : Charges) : ℕ → Multiset ℤ

The charges of those terms which can be regenerated with up-to n insertions of singlets needed to regenerate the Yukawa terms. Equivalently, the sum of up-to n integers each corresponding to a charge of the Yukawa terms.

Equations

• x.ofYukawaTermsNSum 0 = {0}
• x.ofYukawaTermsNSum n.succ = x.ofYukawaTermsNSum n + (x.ofYukawaTermsNSum n).bind fun (sSum : ℤ) => Multiset.map (fun (s : ℤ) => sSum + s) x.ofYukawaTerms

theorem SuperSymmetry.SU5.Charges.ofYukawaTermsNSum_subset_of_subset {x y : Charges} (h : x ⊆ y) (n : ℕ) : x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum n

def SuperSymmetry.SU5.Charges.YukawaGeneratesDangerousAtLevel (x : Charges) (n : ℕ) : Prop

For charges x : Charges, the proposition which states that the singlets needed to regenerate the Yukawa couplings regnerate a dangerous coupling (in the superpotential) with up-to n insertions of the scalars.

Equations

• x.YukawaGeneratesDangerousAtLevel n = ((x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset ≠ ∅)

@[simp]

theorem SuperSymmetry.SU5.Charges.not_yukawaGeneratesDangerousAtLevel_of_empty (n : ℕ) : ¬∅.YukawaGeneratesDangerousAtLevel n

instance SuperSymmetry.SU5.Charges.instDecidableYukawaGeneratesDangerousAtLevel (x : Charges) (n : ℕ) : Decidable (x.YukawaGeneratesDangerousAtLevel n)

Equations

• x.instDecidableYukawaGeneratesDangerousAtLevel n = inferInstanceAs (Decidable ((x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset ≠ ∅))

theorem SuperSymmetry.SU5.Charges.yukawaGeneratesDangerousAtLevel_of_subset {x y : Charges} {n : ℕ} (h : x ⊆ y) (hx : x.YukawaGeneratesDangerousAtLevel n) : y.YukawaGeneratesDangerousAtLevel n

theorem SuperSymmetry.SU5.Charges.yukawaGeneratesDangerousAtLevel_succ {x : Charges} {n : ℕ} (hx : x.YukawaGeneratesDangerousAtLevel n) : x.YukawaGeneratesDangerousAtLevel (n + 1)

theorem SuperSymmetry.SU5.Charges.yukawaGeneratesDangerousAtLevel_add_of_left {x : Charges} {n k : ℕ} (hx : x.YukawaGeneratesDangerousAtLevel n) : x.YukawaGeneratesDangerousAtLevel (n + k)

theorem SuperSymmetry.SU5.Charges.yukawaGeneratesDangerousAtLevel_of_le {x : Charges} {n m : ℕ} (h : n ≤ m) (hx : x.YukawaGeneratesDangerousAtLevel n) : x.YukawaGeneratesDangerousAtLevel m