Minimally allows a set of terms

i. Overview

In this module we consider those charge spectra which minimally allow a finite set of potential terms. That is, they those charge spectra which allow each term in the set, but no proper subset of the charge spectra allows each term in that set.

We have special focus on those charge spectra which minimally allow a top and bottom Yukawa term.

ii. Key results

• MinimallyAllowsFinsetTerms: the proposition that a charge spectrum minimally allows a given finite set of potential terms.
• minTopBottom: a finite set of charge spectra which contains every charge spectrum which minimally allows a top and bottom Yukawa term, given finite sets of possible 5-bar and 10 charges.

iii. Table of contents

• A. Charge spectra which minimally allow a finite set of potential terms
  • A.1. MinimallyAllowsFinsetTerms: Prop of minimally allowing a finset of potential terms
  • A.2. The prop MinimallyAllowsFinsetTerms is decidable
  • A.3. Every element of MinimallyAllowsFinsetTerms allows each term in the finset
  • A.4. MinimallyAllowsFinsetTerms for the singleton set is equivalent to MinimallyAllowsTerm
• B. Minimally allowing the top and bottom Yukawa
  • B.1. Finset of charge spectra containing those which minimally allow top and bottom Yukawa
  • B.2. Every element of minTopBottom allows a top Yukawa
  • B.3. Every element of minTopBottom allows a bottom Yukawa
  • B.4. Every charge spectrum minimally allowing a top and bottom Yukawa in minTopBottom

iv. References

There are no references for this module.

A. Charge spectra which minimally allow a finite set of potential terms

We start by defining the proposition that a charge spectrum minimally allows a finite set of potential terms, and prove some basic properties there of.

A.1. MinimallyAllowsFinsetTerms: Prop of minimally allowing a finset of potential terms

def SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsFinsetTerms {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (Ts : Finset PotentialTerm) : Prop

A collection of charge spectra is said to minimally allow a finite set of potential terms Ts if it allows all terms in Ts and no strict subset of it allows all terms in Ts.

Equations

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

A.2. The prop MinimallyAllowsFinsetTerms is decidable

instance SuperSymmetry.SU5.ChargeSpectrum.instDecidableMinimallyAllowsFinsetTerms {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (Ts : Finset PotentialTerm) : Decidable (x.MinimallyAllowsFinsetTerms Ts)

Equations

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

A.3. Every element of MinimallyAllowsFinsetTerms allows each term in the finset

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_of_minimallyAllowsFinsetTerms {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {Ts : Finset PotentialTerm} {x : ChargeSpectrum 𝓩} {T : PotentialTerm} (h : x.MinimallyAllowsFinsetTerms Ts) (hT : T ∈ Ts) : x.AllowsTerm T

A.4. MinimallyAllowsFinsetTerms for the singleton set is equivalent to MinimallyAllowsTerm

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.minimallyAllowsFinsetTerms_singleton {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x : ChargeSpectrum 𝓩} {T : PotentialTerm} : x.MinimallyAllowsFinsetTerms {T} ↔ x.MinimallyAllowsTerm T

B. Minimally allowing the top and bottom Yukawa

We now consider the special case of those charge spectra which minimally allow a top and bottom Yukawa term.

We construct a finite set of such charge spectra given finite sets of possible 5-bar and 10 charges which contains every charge spectrum which minimally allows a top and bottom Yukawa term.

B.1. Finset of charge spectra containing those which minimally allow top and bottom Yukawa

Here we define minTopBottom in a way which is computationally efficient.

def SuperSymmetry.SU5.ChargeSpectrum.minTopBottom {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) : Multiset (ChargeSpectrum 𝓩)

The set of charges of the form (qHd, qHu, {q5}, {-qHd-q5, q10, qHu - q10}) This includes every charge which minimally allows for the top and bottom Yukawas.

Equations

• One or more equations did not get rendered due to their size.

B.2. Every element of minTopBottom allows a top Yukawa

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_topYukawa_of_mem_minTopBottom {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x : ChargeSpectrum 𝓩} (h : x ∈ minTopBottom S5 S10) : x.AllowsTerm PotentialTerm.topYukawa

B.3. Every element of minTopBottom allows a bottom Yukawa

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_bottomYukawa_of_mem_minTopBottom {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x : ChargeSpectrum 𝓩} (h : x ∈ minTopBottom S5 S10) : x.AllowsTerm PotentialTerm.bottomYukawa

B.4. Every charge spectrum minimally allowing a top and bottom Yukawa in minTopBottom

theorem SuperSymmetry.SU5.ChargeSpectrum.mem_minTopBottom_of_minimallyAllowsFinsetTerms {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x : ChargeSpectrum 𝓩} {S5 S10 : Finset 𝓩} (h : x.MinimallyAllowsFinsetTerms {PotentialTerm.topYukawa, PotentialTerm.bottomYukawa}) (hx : x ∈ ofFinset S5 S10) : x ∈ minTopBottom S5 S10