Physlib

Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimalSuperSet

Minimal super set

i. Overview

The minimally super set of a spectrum of charges `x` is the finite set of spectrums of charges `y` such that `x ⊆ y` and there is no `z` such that `x ⊆ z ⊂ y`. The minimal super set is defined using a finite set of possible charges in the `5`-bar and `10` representations of `su(5)`. This is to ensure that the minimal super set is itself finite.

In this file we define the minimal super set and prove some basic properties of it.

ii. Key results

- `minimalSuperSet`: the minimal super set of a charge spectrum. - `exists_minimalSuperSet`: the existence of a member of the minimal super set between two charge spectra. - `subset_insert_filter_card_zero`: a statement related to closure properties of multisets of charge spectra under a proposition `p` satisfying certain properties. The proof of this result relies on induction on minimal super sets.

iii. Table of contents

- A. The minimal super set - A.1. Members of the minimal super set are super sets - A.2. Self is not a member of the minimal super set - A.3. Cardinality of member of the minimal super set - A.4. Inserting charges and minimal super sets - A.5. Existence of a minimal super set member between two charges - B. Induction properties on the minimal super set - B.1. Lifting propositions from minimal super sets to super sets - B.2. Closure of multisets based on proposition for minimal super sets - B.3. Closure of multisets based on propositions

iv. References

There are no known references for the material in this file.

A. The minimal super set

We define the minimal super set.

A.1. Members of the minimal super set are super sets

We show the basic property of a member `y ∈ minimalSuperSet S5 S10 x`, that is that they are indeed super sets, namely `x ⊆ y`.

A.2. Self is not a member of the minimal super set

A charge spectrum is not a member of its own minimal super set. We give two different forms of this result.

A.3. Cardinality of member of the minimal super set

We show that any member `y` of the minimal super set of `x` has cardinality one more than that of `x`. I.e. it contains exactly one more unique charge.

A.4. Inserting charges and minimal super sets

We show that inserting a charge from `S5` or `S10` into `x`'s `Q5` or `Q10` respectively which is not already present in `x` gives a member of the minimal super set.

Likewise we show that if `x` has no `qHd` or `qHu` charge, then inserting a charge from `S5` into `qHd` or `qHu` respectively gives a member of the minimal super set.

A.5. Existence of a minimal super set member between two charges

We show that if `y` has charges from `S5` and `S10` and is a super set of `x` but not equal to `x` then there is a `z` in the minimal super set of `x` which is a subset of `y`.

This shows, in a sense, that `minimalSuperSet` is "minimal", although it does not go all the way to doing that. In particular, it does show that every minimal super set is a member of `minimalSuperSet`.

B. Induction properties on the minimal super set

We now prove a number of induction properties related to minimal super sets.

B.1. Lifting propositions from minimal super sets to super sets

We show that for a proposition `p` on charge spectra with the property that it is true on all minimal super sets of `x` if it true on `x` itself, then it is true on all super sets of `x` if it is true for `x` itself.

B.2. Closure of multisets based on proposition for minimal super sets

We show that for a predicate `p` on charge spectrum, if a multiset `T` of complete charge spectra has the property that - all insertions of a `q10` charge either ends in `T` or fails `p`. - all insertions of a `q5` charge either ends in `T` or fails `p`. Then if `x` is in `T` then all members of the minimal super set of `x` either are in `T` or fail `p`.

B.3. Closure of multisets based on propositions

We show that for a predicate `p` on charge spectrum which if false on a charge spectrum is also false on all its super sets, if a multiset `T` of complete charge spectra has the property that - all insertions of a `q10` charge either ends in `T` or fails `p`. - all insertions of a `q5` charge either ends in `T` or fails `p`. Then if `y` is not in `T` then it does not satisfy `p`.

We first prove this with an explicit induction argument, `n`, and then we prove it in a more user friendly way.

14 declarations

definition

Minimal super set of an SU(5)SU(5) charge spectrum xx relative to S5S_5 and S10S_{10}

Given finite sets of possible charges S5,S10ZS_5, S_{10} \subset \mathcal{Z} and a charge spectrum x=(qHd,qHu,Q5,Q10)x = (q_{H_d}, q_{H_u}, Q_5, Q_{10}), the **minimal super set** of xx is the collection of all charge spectra yy obtained by adding exactly one charge from the allowed sets to a component of xx that does not already contain it. Specifically, it is the union of the following sets, excluding xx itself: 1. If x.qHdx.q_{H_d} is empty, the set of spectra where qHdq_{H_d} is set to some cS5c \in S_5 and all other components remain as in xx. 2. If x.qHux.q_{H_u} is empty, the set of spectra where qHuq_{H_u} is set to some cS5c \in S_5 and all other components remain as in xx. 3. The set of spectra where Q5Q_5 is replaced by Q5{c}Q_5 \cup \{c\} for some cS5x.Q5c \in S_5 \setminus x.Q_5. 4. The set of spectra where Q10Q_{10} is replaced by Q10{c}Q_{10} \cup \{c\} for some cS10x.Q10c \in S_{10} \setminus x.Q_{10}.

theorem

Members of the Minimal Super Set are Super Sets

For any finite sets of charges S5,S10ZS_5, S_{10} \subset \mathcal{Z} and any SU(5)SU(5) charge spectra x,yChargeSpectrum Zx, y \in \text{ChargeSpectrum } \mathcal{Z}, if yy is an element of the minimal super set of xx relative to S5S_5 and S10S_{10}, then xx is a subset of yy (xyx \subseteq y).

theorem

xminimalSuperSet(S5,S10,x)x \notin \text{minimalSuperSet}(S_5, S_{10}, x)

Let S5S_5 and S10S_{10} be finite sets of charges in Z\mathcal{Z}. For any SU(5)SU(5) charge spectrum xx, the spectrum xx is not a member of its own minimal super set relative to S5S_5 and S10S_{10}, denoted as xminimalSuperSet(S5,S10,x)x \notin \text{minimalSuperSet}(S_5, S_{10}, x).

theorem

yminimalSuperSet(x)    xyy \in \text{minimalSuperSet}(x) \implies x \neq y

Let S5S_5 and S10S_{10} be finite sets of charges in Z\mathcal{Z}. For any charge spectra xx and yy, if yy is a member of the minimal super set of xx relative to S5S_5 and S10S_{10}, then xyx \neq y.

theorem

card(y)=card(x)+1\text{card}(y) = \text{card}(x) + 1 for yminimalSuperSet(x)y \in \text{minimalSuperSet}(x)

Let Z\mathcal{Z} be a type of charges, and let S5,S10ZS_5, S_{10} \subset \mathcal{Z} be finite sets of allowed charges. For any SU(5)SU(5) charge spectrum xx, if a spectrum yy is a member of the minimal super set of xx relative to S5S_5 and S10S_{10}, then the cardinality of yy is exactly one greater than the cardinality of xx: card(y)=card(x)+1 \text{card}(y) = \text{card}(x) + 1 where the cardinality card(x)\text{card}(x) is defined as the total number of charges present across all components (qHu,qHd,Q5,Q10q_{H_u}, q_{H_d}, Q_5, Q_{10}) of the spectrum.

theorem

Inserting a charge from S5S_5 into Q5Q_5 yields a member of the minimal super set

Let S5S_5 and S10S_{10} be finite sets of charges in Z\mathcal{Z} and let x=(qHd,qHu,Q5,Q10)x = (q_{H_d}, q_{H_u}, Q_5, Q_{10}) be an SU(5)SU(5) charge spectrum. For any charge zS5z \in S_5, if zQ5z \notin Q_5, then the charge spectrum (qHd,qHu,Q5{z},Q10)(q_{H_d}, q_{H_u}, Q_5 \cup \{z\}, Q_{10}) is a member of the minimal super set of xx relative to S5S_5 and S10S_{10}.

theorem

Inserting zS10Q10z \in S_{10} \setminus Q_{10} into xx yields a member of its minimal super set

Let S5S_5 and S10S_{10} be finite sets of allowed charges in a type Z\mathcal{Z}. For any SU(5)SU(5) charge spectrum x=(qHd,qHu,Q5,Q10)x = (q_{H_d}, q_{H_u}, Q_5, Q_{10}), if zz is a charge such that zS10z \in S_{10} and zQ10z \notin Q_{10}, then the charge spectrum obtained by adding zz to the set Q10Q_{10}—specifically the spectrum (qHd,qHu,Q5,Q10{z})(q_{H_d}, q_{H_u}, Q_5, Q_{10} \cup \{z\})—is a member of the minimal super set of xx relative to S5S_5 and S10S_{10}.

theorem

Assigning an empty qHdq_{H_d} charge from S5S_5 results in a member of the minimal super set

Let S5,S10ZS_5, S_{10} \subset \mathcal{Z} be finite sets of allowed charges. Suppose xx is an SU(5)SU(5) charge spectrum where the down-type Higgs charge component qHdq_{H_d} is empty (represented as `none`), such that x=(none,qHu,Q5,Q10)x = (\text{none}, q_{H_u}, Q_5, Q_{10}). For any charge zS5z \in S_5, the charge spectrum y=(z,qHu,Q5,Q10)y = (z, q_{H_u}, Q_5, Q_{10}), which is identical to xx except that its qHdq_{H_d} component is set to zz, is a member of the minimal super set of xx relative to S5S_5 and S10S_{10}.

theorem

Assigning an empty qHuq_{H_u} charge from S5S_5 results in a member of the minimal super set

Let S5,S10ZS_5, S_{10} \subset \mathcal{Z} be finite sets of allowed charges. Suppose xx is an SU(5)SU(5) charge spectrum where the up-type Higgs charge component qHuq_{H_u} is empty (represented as `none`), such that x=(qHd,none,Q5,Q10)x = (q_{H_d}, \text{none}, Q_5, Q_{10}). For any charge zS5z \in S_5, the charge spectrum y=(qHd,z,Q5,Q10)y = (q_{H_d}, z, Q_5, Q_{10}), which is identical to xx except that its qHuq_{H_u} component is set to zz, is a member of the minimal super set of xx relative to S5S_5 and S10S_{10}.

theorem

Existence of a minimal super set member zz such that zyz \subseteq y

Let S5,S10ZS_5, S_{10} \subset \mathcal{Z} be finite sets of allowed charges. Let xx and yy be SU(5)SU(5) charge spectra such that yy belongs to the set of spectra whose charges are contained in S5S_5 and S10S_{10} (i.e., yofFinset(S5,S10)y \in \text{ofFinset}(S_5, S_{10})). If xx is a proper subset of yy (xyx \subseteq y and xyx \neq y), then there exists a charge spectrum zz in the minimal super set of xx relative to S5S_5 and S10S_{10} such that zyz \subseteq y.

theorem

Minimal Super Set Property Preservation via Induction on card(y)card(x)\text{card}(y) - \text{card}(x)

Let S5S_5 and S10S_{10} be finite sets of charges in Z\mathcal{Z}, and let pp be a property defined on SU(5)SU(5) charge spectra. Suppose that for any spectrum xx, if p(x)p(x) holds, then p(z)p(z) holds for every zz in the minimal super set of xx relative to S5S_5 and S10S_{10} (i.e., zminimalSuperSet(S5,S10,x)z \in \text{minimalSuperSet}(S_5, S_{10}, x)). If xx and yy are charge spectra such that xyx \subseteq y, p(x)p(x) is true, and yy is a spectrum whose charges are all contained in S5S_5 and S10S_{10}, then p(y)p(y) is true. This result is proved by induction on the cardinality difference n=card(y)card(x)n = \text{card}(y) - \text{card}(x), where the cardinality card(x)\text{card}(x) is the total number of charges across all components of the spectrum.

theorem

Minimal Super Sets of Spectra in TT satisfy pp only if they are in TT

Let TT be a multiset of SU(5)SU(5) charge spectra, S5S_5 and S10S_{10} be finite sets of charges, and pp be a predicate on charge spectra. Suppose the following conditions hold: 1. Every charge spectrum xTx \in T is complete (i.e., it possesses qHdq_{H_d}, qHuq_{H_u}, and non-empty sets of charges Q5ˉQ_{\bar{5}} and Q10Q_{10}). 2. For every q10S10q_{10} \in S_{10}, any spectrum yy formed by adding q10q_{10} to the Q10Q_{10} component of some xTx \in T satisfies the property that if yTy \notin T, then p(y)p(y) is false. 3. For every q5S5q_5 \in S_5, any spectrum yy formed by adding q5q_5 to the Q5ˉQ_{\bar{5}} component of some xTx \in T satisfies the property that if yTy \notin T, then p(y)p(y) is false. Then, for any xTx \in T and any yy in the minimal super set of xx relative to S5S_5 and S10S_{10}, if yTy \notin T, then p(y)p(y) is false.

theorem

Inductive Step: yxTy \supseteq x \in T and yT    ¬p(y)y \notin T \implies \neg p(y) for SU(5)SU(5) Spectra Difference nn

Let TT be a multiset of SU(5)SU(5) charge spectra and let S5,S10S_5, S_{10} be finite sets of charges. Let pp be a predicate on charge spectra such that for any two spectra xx and yy, xyx \subseteq y and ¬p(x)\neg p(x) implies ¬p(y)\neg p(y) (equivalently, the property pp is downward-closed under the subset relation). Suppose the following conditions hold: 1. Every charge spectrum xTx \in T is complete. 2. For every q10S10q_{10} \in S_{10}, any spectrum yy' formed by adding q10q_{10} to the Q10Q_{10} component of some xTx \in T satisfies yT    ¬p(y)y' \notin T \implies \neg p(y'). 3. For every q5S5q_5 \in S_5, any spectrum yy' formed by adding q5q_5 to the Q5ˉQ_{\bar{5}} component of some xTx \in T satisfies yT    ¬p(y)y' \notin T \implies \neg p(y'). Then, for any xTx \in T and any yy with charges in S5S_5 and S10S_{10} such that xyx \subseteq y, if n=card(y)card(x)n = \text{card}(y) - \text{card}(x), then yTy \notin T implies ¬p(y)\neg p(y).

theorem

For yxTy \supseteq x \in T, p(y)    yTp(y) \implies y \in T

Let TT be a multiset of SU(5)SU(5) charge spectra and let S5,S10S_5, S_{10} be finite sets of charges. Let pp be a predicate on charge spectra that is downward-closed under the subset relation, such that for any two spectra xx and yy, xyx \subseteq y and ¬p(x)\neg p(x) implies ¬p(y)\neg p(y). Suppose the following conditions hold: 1. Every spectrum xTx \in T is complete (i.e., it contains qHdq_{H_d}, qHuq_{H_u}, and non-empty sets Q5ˉQ_{\bar{5}} and Q10Q_{10}). 2. For every charge q10S10q_{10} \in S_{10} and every xTx \in T, the spectrum yy' formed by inserting q10q_{10} into the Q10Q_{10} component of xx satisfies yT    ¬p(y)y' \notin T \implies \neg p(y'). 3. For every charge q5S5q_5 \in S_5 and every xTx \in T, the spectrum yy' formed by inserting q5q_5 into the Q5ˉQ_{\bar{5}} component of xx satisfies yT    ¬p(y)y' \notin T \implies \neg p(y'). Then, for any xTx \in T and any spectrum yy whose charges are contained in S5S_5 and S10S_{10}, if xyx \subseteq y and yTy \notin T, then ¬p(y)\neg p(y).