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
Minimal super set of an charge spectrum relative to and
Given finite sets of possible charges and a charge spectrum , the **minimal super set** of is the collection of all charge spectra obtained by adding exactly one charge from the allowed sets to a component of that does not already contain it. Specifically, it is the union of the following sets, excluding itself: 1. If is empty, the set of spectra where is set to some and all other components remain as in . 2. If is empty, the set of spectra where is set to some and all other components remain as in . 3. The set of spectra where is replaced by for some . 4. The set of spectra where is replaced by for some .
Members of the Minimal Super Set are Super Sets
For any finite sets of charges and any charge spectra , if is an element of the minimal super set of relative to and , then is a subset of ().
Let and be finite sets of charges in . For any charge spectrum , the spectrum is not a member of its own minimal super set relative to and , denoted as .
Let and be finite sets of charges in . For any charge spectra and , if is a member of the minimal super set of relative to and , then .
for
Let be a type of charges, and let be finite sets of allowed charges. For any charge spectrum , if a spectrum is a member of the minimal super set of relative to and , then the cardinality of is exactly one greater than the cardinality of : where the cardinality is defined as the total number of charges present across all components () of the spectrum.
Inserting a charge from into yields a member of the minimal super set
Let and be finite sets of charges in and let be an charge spectrum. For any charge , if , then the charge spectrum is a member of the minimal super set of relative to and .
Inserting into yields a member of its minimal super set
Let and be finite sets of allowed charges in a type . For any charge spectrum , if is a charge such that and , then the charge spectrum obtained by adding to the set —specifically the spectrum —is a member of the minimal super set of relative to and .
Assigning an empty charge from results in a member of the minimal super set
Let be finite sets of allowed charges. Suppose is an charge spectrum where the down-type Higgs charge component is empty (represented as `none`), such that . For any charge , the charge spectrum , which is identical to except that its component is set to , is a member of the minimal super set of relative to and .
Assigning an empty charge from results in a member of the minimal super set
Let be finite sets of allowed charges. Suppose is an charge spectrum where the up-type Higgs charge component is empty (represented as `none`), such that . For any charge , the charge spectrum , which is identical to except that its component is set to , is a member of the minimal super set of relative to and .
Existence of a minimal super set member such that
Let be finite sets of allowed charges. Let and be charge spectra such that belongs to the set of spectra whose charges are contained in and (i.e., ). If is a proper subset of ( and ), then there exists a charge spectrum in the minimal super set of relative to and such that .
Minimal Super Set Property Preservation via Induction on
Let and be finite sets of charges in , and let be a property defined on charge spectra. Suppose that for any spectrum , if holds, then holds for every in the minimal super set of relative to and (i.e., ). If and are charge spectra such that , is true, and is a spectrum whose charges are all contained in and , then is true. This result is proved by induction on the cardinality difference , where the cardinality is the total number of charges across all components of the spectrum.
Minimal Super Sets of Spectra in satisfy only if they are in
Let be a multiset of charge spectra, and be finite sets of charges, and be a predicate on charge spectra. Suppose the following conditions hold: 1. Every charge spectrum is complete (i.e., it possesses , , and non-empty sets of charges and ). 2. For every , any spectrum formed by adding to the component of some satisfies the property that if , then is false. 3. For every , any spectrum formed by adding to the component of some satisfies the property that if , then is false. Then, for any and any in the minimal super set of relative to and , if , then is false.
Inductive Step: and for Spectra Difference
Let be a multiset of charge spectra and let be finite sets of charges. Let be a predicate on charge spectra such that for any two spectra and , and implies (equivalently, the property is downward-closed under the subset relation). Suppose the following conditions hold: 1. Every charge spectrum is complete. 2. For every , any spectrum formed by adding to the component of some satisfies . 3. For every , any spectrum formed by adding to the component of some satisfies . Then, for any and any with charges in and such that , if , then implies .
For ,
Let be a multiset of charge spectra and let be finite sets of charges. Let be a predicate on charge spectra that is downward-closed under the subset relation, such that for any two spectra and , and implies . Suppose the following conditions hold: 1. Every spectrum is complete (i.e., it contains , , and non-empty sets and ). 2. For every charge and every , the spectrum formed by inserting into the component of satisfies . 3. For every charge and every , the spectrum formed by inserting into the component of satisfies . Then, for any and any spectrum whose charges are contained in and , if and , then .
