Physlib

Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.FinsetTerms

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

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

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.

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`

8 declarations

definition

xx minimally allows potential terms TsTs

A charge spectrum xx minimally allows a finite set of potential terms TsTs if xx allows every term T∈TsT \in Ts and no proper sub-spectrum y⊊xy \subsetneq x allows all terms in TsTs. Formally, this is defined such that for every yy in the powerset of xx, y=xy = x if and only if yy allows every potential term T∈TsT \in Ts.

instance

Decidability of xx minimally allowing potential terms TsTs

For a given charge spectrum xx and a finite set of potential terms TsTs, the property that xx minimally allows TsTs is decidable. This implies there is a computational procedure to determine if xx allows every term T∈TsT \in Ts while ensuring that no proper subset y⊊xy \subsetneq x allows all terms in TsTs.

theorem

xx minimally allows Ts  ⟹  ∀T∈Ts,x allows TTs \implies \forall T \in Ts, x \text{ allows } T

Let xx be a charge spectrum and TsTs be a finite set of potential terms. If xx minimally allows the set of potential terms TsTs, then for any potential term T∈TsT \in Ts, the spectrum xx allows the term TT.

theorem

Minimal allowance of {T}\{T\} is equivalent to minimal allowance of TT

For any potential term TT and charge spectrum xx, xx minimally allows the finite set of terms {T}\{T\} if and only if xx minimally allows the individual term TT.

definition

Multiset of charge spectra minimally allowing top and bottom Yukawa terms

Given finite sets S5S_5 and S10S_{10} of possible charges in a type Z\mathcal{Z}, `minTopBottom S5 S10` is the multiset of all unique charge spectra of the form (qHd,qHu,{q5ˉ},{−qHd−q5ˉ,q10,qHu−q10})(q_{H_d}, q_{H_u}, \{q_{\bar{5}}\}, \{-q_{H_d} - q_{\bar{5}}, q_{10}, q_{H_u} - q_{10}\}) such that qHd,qHu,q5ˉ∈S5q_{H_d}, q_{H_u}, q_{\bar{5}} \in S_5 and q10∈S10q_{10} \in S_{10}. This multiset includes every charge spectrum which minimally allows for both top and bottom Yukawa terms.

theorem

Elements of minTopBottom\text{minTopBottom} allow top Yukawa terms

For any finite sets of charges S5S_5 and S10S_{10} and any charge spectrum xx, if xx is an element of the multiset minTopBottom(S5,S10)\text{minTopBottom}(S_5, S_{10}), then xx allows a top Yukawa term. Here, minTopBottom(S5,S10)\text{minTopBottom}(S_5, S_{10}) denotes the multiset of all charge spectra that minimally allow for both top and bottom Yukawa terms, given the sets of possible charges S5S_5 and S10S_{10}.

theorem

Every element of `minTopBottom` allows a bottom Yukawa term

For any finite sets of charges S5S_5 and S10S_{10} in a type Z\mathcal{Z}, if a charge spectrum xx is an element of the multiset minTopBottom(S5,S10)\text{minTopBottom}(S_5, S_{10}), then xx allows the bottom Yukawa term.

theorem

Minimally allowing top and bottom Yukawa terms implies x∈minTopBottom(S5ˉ,S10)x \in \text{minTopBottom}(S_{\bar{5}}, S_{10})

For any SU(5)SU(5) charge spectrum xx and any finite sets of charges S5ˉ,S10⊂ZS_{\bar{5}}, S_{10} \subset \mathcal{Z}, if xx minimally allows the set of potential terms {topYukawa,bottomYukawa}\{ \text{topYukawa}, \text{bottomYukawa} \} and xx is contained in the set of spectra ofFinset(S5ˉ,S10)\text{ofFinset}(S_{\bar{5}}, S_{10}), then xx is an element of the multiset minTopBottom(S5ˉ,S10)\text{minTopBottom}(S_{\bar{5}}, S_{10}).