Yukawa charges

i. Overview

In this module we look at the charges associated with the Yukawa terms in the super potential, and when they can regenerate phenomenologically constrained super-potential terms at different levels.

We do not not consider the regeneration of terms in the Kähler potential within this module.

ii. Key results

• ofYukawaTerms: the multiset of charges associated with the Yukawa terms
• ofYukawaTermsNSum: the multiset of charges associated with up-to n copies of the Yukawa terms or equivalently the charges of singlet insertions needed to regenerate Yukawa terms.
• YukawaGeneratesDangerousAtLevel: the proposition that a charge spectrum regenerates a phenomenologically constrained term in the super-potential with up-to n insertions of singlets needed to regenerate the Yukawa terms.

iii. Table of contents

• A. Charges of the Yukawa terms
  • A.1. Monoticity of charges of the Yukawa terms
  • A.2. upto n-copies of charges of the Yukawa terms (aka charges of singlet insertions)
  • A.3. Monoticity of set of charges of upto n-copies of the Yukawa terms
• B. Regeneration of phenomenologically constrained terms via upto n Yukawa singlet insertions
  • B.1. Decidability of YukawaGeneratesDangerousAtLevel
  • B.2. Simplififications of condition for regenerating dangerous terms
  • B.3. Empty charge spectrum does not regenerate dangerous terms
  • B.4. Monotonicity of regeneration of dangerous terms in charge spectra
  • B.5. Monotonicity of regeneration of dangerous terms in level

iv. References

There are no known references for this module.

A. Charges of the Yukawa terms

def SuperSymmetry.SU5.ChargeSpectrum.ofYukawaTerms {𝓩 : Type} [AddCommGroup 𝓩] (x : ChargeSpectrum 𝓩) : 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

A.1. Monoticity of charges of the Yukawa terms

theorem SuperSymmetry.SU5.ChargeSpectrum.ofYukawaTerms_subset_of_subset {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) : x.ofYukawaTerms ⊆ y.ofYukawaTerms

A.2. upto n-copies of charges of the Yukawa terms (aka charges of singlet insertions)

def SuperSymmetry.SU5.ChargeSpectrum.ofYukawaTermsNSum {𝓩 : Type} [AddCommGroup 𝓩] (x : ChargeSpectrum 𝓩) : ℕ → 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

A.3. Monoticity of set of charges of upto n-copies of the Yukawa terms

theorem SuperSymmetry.SU5.ChargeSpectrum.ofYukawaTermsNSum_subset_of_subset {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) (n : ℕ) : x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum n

B. Regeneration of phenomenologically constrained terms via upto n Yukawa singlet insertions

def SuperSymmetry.SU5.ChargeSpectrum.YukawaGeneratesDangerousAtLevel {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (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.

Note: If defined as (x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset ≠ ∅ the exicution time is greatley increased.

Equations

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

B.1. Decidability of YukawaGeneratesDangerousAtLevel

instance SuperSymmetry.SU5.ChargeSpectrum.instDecidableYukawaGeneratesDangerousAtLevel {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (n : ℕ) : Decidable (x.YukawaGeneratesDangerousAtLevel n)

Equations

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

B.2. Simplififications of condition for regenerating dangerous terms

theorem SuperSymmetry.SU5.ChargeSpectrum.YukawaGeneratesDangerousAtLevel_iff_inter {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x : ChargeSpectrum 𝓩} {n : ℕ} : x.YukawaGeneratesDangerousAtLevel n ↔ x.ofYukawaTermsNSum n ∩ x.phenoConstrainingChargesSP ≠ ∅

theorem SuperSymmetry.SU5.ChargeSpectrum.yukawaGeneratesDangerousAtLevel_iff_toFinset {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (n : ℕ) : x.YukawaGeneratesDangerousAtLevel n ↔ (x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset ≠ ∅

B.3. Empty charge spectrum does not regenerate dangerous terms

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.not_yukawaGeneratesDangerousAtLevel_of_empty {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (n : ℕ) : ¬∅.YukawaGeneratesDangerousAtLevel n

B.4. Monotonicity of regeneration of dangerous terms in charge spectra

If x regenerates a dangerous term with up-to n insertions of Yukawa singlets, and x ⊆ y, then y also regenerates a dangerous term with up-to n insertions.

theorem SuperSymmetry.SU5.ChargeSpectrum.yukawaGeneratesDangerousAtLevel_of_subset {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x y : ChargeSpectrum 𝓩} {n : ℕ} (h : x ⊆ y) (hx : x.YukawaGeneratesDangerousAtLevel n) : y.YukawaGeneratesDangerousAtLevel n

B.5. Monotonicity of regeneration of dangerous terms in level

If x regenerates a dangerous term with up-to n insertions of Yukawa singlets, then x also regenerates a dangerous term with up-to n + 1 insertions.

theorem SuperSymmetry.SU5.ChargeSpectrum.yukawaGeneratesDangerousAtLevel_succ {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x : ChargeSpectrum 𝓩} {n : ℕ} (hx : x.YukawaGeneratesDangerousAtLevel n) : x.YukawaGeneratesDangerousAtLevel (n + 1)

theorem SuperSymmetry.SU5.ChargeSpectrum.yukawaGeneratesDangerousAtLevel_add_of_left {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x : ChargeSpectrum 𝓩} {n k : ℕ} (hx : x.YukawaGeneratesDangerousAtLevel n) : x.YukawaGeneratesDangerousAtLevel (n + k)

theorem SuperSymmetry.SU5.ChargeSpectrum.yukawaGeneratesDangerousAtLevel_of_le {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x : ChargeSpectrum 𝓩} {n m : ℕ} (h : n ≤ m) (hx : x.YukawaGeneratesDangerousAtLevel n) : x.YukawaGeneratesDangerousAtLevel m