Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm
Charges allowing terms
i. Overview
To each charge spectrum `x : ChargeSpectrum 𝓩` we say it allows the potential term `T : PotentialTerm`, if one of the charges associated with that potential term is zero.
What this means, is that there is a choice of charges from the charge spectrum `x` that can be assigned to the fields in the potential term `T` such that the total charge is zero, and therefore that the term is present in the potential. The presence of absence of certain terms is of phenomenological importance.
This concept is captured by the proposition `AllowsTerm`.
In addition to this, for each potential term `T`, we define a function `allowsTermForm` which takes three elements of `𝓩`, `a`, `b`, and `c` and returns a charge spectrum which allows the term `T`. We will show in `allowsTerm_iff_subset_allowsTermForm` that any charge spectrum that allows a term `T` has a subset which can be expressed as `allowsTermForm a b c T` for some `a`, `b`, and `c`.
We also define the propositions `AllowsTermQ5 x q5 T` and `AllowsTermQ10 x q10 T` which correspond to the condition that adding a charge `q5` to the `Q5` charges of the charge spectrum `x`, or adding a charge `q10` to the `Q10` charges of the charge spectrum `x`, leads to a zero charge in the charges of potential term `T`.
ii. Key results
- `AllowsTerm` : The proposition that a charge spectrum allows a potential term. - `allowsTermForm` : A function which for each potential term `T` and three charges `a`, `b`, and `c` returns a charge spectrum which allows the term `T`, and such that any charge spectrum allowing `T` has a subset of this form. - `AllowsTermQ5` : The proposition that adding a charge `q5` to the `Q5` charges of a charge spectrum `x` allows the potential term `T` due to the addition of that charge. - `AllowsTermQ10` : The proposition that adding a charge `q10` to the `Q10` charges of a charge spectrum `x` allows the potential term `T` due to the addition of that charge.
iii. Table of contents
- A. Charge spectrums allowing potential terms - A.1. Decidability of `AllowsTerm` - A.2. Monotonicity of `AllowsTerm` - B. Forms of charges which allow potential terms - B.1. `allowsTermForm` allows the potential term - B.2. Subset relations for `allowsTermForm` - B.3. Card of `allowsTermForm` - B.4. If `AllowsTerm` then subset equal to `allowsTermForm a b c T` - B.5. `AllowsTerm` if and only if subset equal to `allowsTermForm a b c T` - B.6. Cardinality of subset allowing potential term - C. Allowing a potential term by insertion of a `Q5` charge - C.1. Decidability of `AllowsTermQ5` - C.2. AllowsTermQ5 or AllowsTerm from AllowsTerm with inserted of `Q5` charge - C.3. AllowsTerm with inserted of `Q5` charge from AllowsTermQ5 - C.4. AllowsTerm with inserted of `Q5` charge iff AllowsTermQ5 or AllowsTerm - D. Allowing a potential term by insertion of a `Q10` charge - D.1. Decidability of `AllowsTermQ5` - D.2. AllowsTermQ10 or AllowsTerm from AllowsTerm with inserted of `Q10` charge - D.3. AllowsTerm with inserted of `Q10` charge from AllowsTermQ5 - D.4. AllowsTerm with inserted of `Q10` charge iff AllowsTermQ10 or AllowsTerm
iv. References
There are no known references for the results in this file.
A. Charge spectrums allowing potential terms
We first define the proposition `AllowsTerm`, which for a charge spectrum `x : ChargeSpectrum 𝓩` and a potential term `T : PotentialTerm`, is true if the zero charge is in the set of charges associated with that potential term.
That is, if there is some choice of representations present in the theory which will allow that potential term via symmetry.
A.1. Decidability of `AllowsTerm`
We define the decidability of `AllowsTerm` through `ofPotentialTerm'` rather than `ofPotentialTerm` due to the speed of the former compared to the latter.
A.2. Monotonicity of `AllowsTerm`
The proposition `AllowsTerm` is monotone in its charge spectrum argument. That is if a charge spectrum `y` is a subset of a charge spectrum `x`, and `y` allows a potential term `T`, then `x` also allows that potential term `T`.
B. Forms of charges which allow potential terms
We now define the function `allowsTermForm` which for each potential term `T` and three charges `a`, `b`, and `c` returns a charge spectrum which allows the term `T`.
These charges are in a minimal form, in the sense that any charge spectrum allowing `T` has a subset of this form.
B.1. `allowsTermForm` allows the potential term
Any charge spectrum of the form `allowsTermForm a b c T` allows the potential term `T`.
B.2. Subset relations for `allowsTermForm`
For any potential term `T` except for `W¹ᵢⱼₖₗ 10ⁱ 10ʲ 10ᵏ 5̄Mˡ` or `W²ᵢⱼₖ 10ⁱ 10ʲ 10ᵏ 5̄Hd`, a charge spectrum `allowsTermForm a b c T` is a subset of another charge spectrum `allowsTermForm a' b' c' T` if they are equal.
The reason this does not work for `W1` an `W2` is due to the presence of three charges in the 10d representation.
B.3. Card of `allowsTermForm`
The cardinality of the charge spectrum `allowsTermForm a b c T` is always less than or equal to the degree of the potential term `T`.
B.4. If `AllowsTerm` then subset equal to `allowsTermForm a b c T`
We now show one of the more important properties of `allowsTermForm`. Namely that if a charge spectrum `x` allows a potential term `T`, then there exists charges `a`, `b`, and `c` such that `allowsTermForm a b c T ⊆ x`.
The proof of this result is rather long, relying on case-by-case analysis of each of the potential terms of interest.
B.5. `AllowsTerm` if and only if subset equal to `allowsTermForm a b c T`
We now lift the previous result to show that a charge spectrum `x` allows a potential term `T` if and only if there exists charges `a`, `b`, and `c` such that `allowsTermForm a b c T ⊆ x`.
Given what has already been shown, this result is now trivial.
B.6. Cardinality of subset allowing potential term
We show that if a charge spectrum `x` allows a potential term `T`, then there exists a subset of `x` which allows `T` and whose cardinality is less than or equal to the degree of `T`.
This follows from the fact that `allowsTermForm a b c T` always has cardinality less than or equal to the degree of `T`.
C. Allowing a potential term by insertion of a `Q5` charge
We now study what happens when we add a charge `q5` to the `Q5` charges of a charge spectrum `x`. We define the proposition `AllowsTermQ5 x q5 T` which is true if adding the charge `q5` to the `Q5` charges of `x` allows the potential term `T` due to the addition of that charge.
We prove a number of properties of this proposition, including its relation to `AllowsTerm` and its decidability.
C.1. Decidability of `AllowsTermQ5`
We show that if the type `𝓩` has decidable equality, then the proposition `AllowsTermQ5 x q5 T` is decidable for any charge spectrum `x`, charge `q5`, and potential term `T`.
C.2. AllowsTermQ5 or AllowsTerm from AllowsTerm with inserted of `Q5` charge
We show that if a charge spectrum `x` with an inserted charge `q5` allows a potential term `T`, then either the charge spectrum `x` allows that potential term `T` *due to* the addition of that charge, or the charge spectrum `x` already allows that potential term `T`.
C.3. AllowsTerm with inserted of `Q5` charge from AllowsTermQ5
We show that if a charge spectrum `x` allows a potential term `T` *due to* the addition of a charge `q5`, then the charge spectrum `x` with that charge inserted allows that potential term `T`.
C.4. AllowsTerm with inserted of `Q5` charge iff AllowsTermQ5 or AllowsTerm
We show that the charge spectrum `x` with that charge inserted allows that potential term `T` if and only if either the charge spectrum `x` allows that potential term `T` *due to* the addition of that charge, or the charge spectrum `x` already allows that potential term `T`.
D. Allowing a potential term by insertion of a `Q10` charge
We now replicate the previous section, but for the insertion of a `Q10` charge, rather than a `Q5` charge.
We study what happens when we add a charge `q10` to the `Q10` charges of a charge spectrum `x`. We define the proposition `AllowsTermQ10 x q10 T` which is true if adding the charge `q10` to the `Q10` charges of `x` allows the potential term `T` due to the addition of that charge.
We prove a number of properties of this proposition, including its relation to `AllowsTerm` and its decidability.
D.1. Decidability of `AllowsTermQ5`
We show that if the type `𝓩` has decidable equality, then the proposition `AllowsTermQ10 x q10 T` is decidable for any charge spectrum `x`, charge `q10`, and potential term `T`.
D.2. AllowsTermQ10 or AllowsTerm from AllowsTerm with inserted of `Q10` charge
We show that if a charge spectrum `x` with an inserted charge `q10` allows a potential term `T`, then either the charge spectrum `x` allows that potential term `T` *due to* the addition of that charge, or the charge spectrum `x` already allows that potential term `T`.
D.3. AllowsTerm with inserted of `Q10` charge from AllowsTermQ5
We show that if a charge spectrum `x` allows a potential term `T` *due to* the addition of a charge `q10`, then the charge spectrum `x` with that charge inserted allows that potential term `T`.
D.4. AllowsTerm with inserted of `Q10` charge iff AllowsTermQ10 or AllowsTerm
We show that the charge spectrum `x` with that charge inserted allows that potential term `T` if and only if either the charge spectrum `x` allows that potential term `T` *due to* the addition of that charge, or the charge spectrum `x` already allows that potential term `T`.
22 declarations
Charge spectrum allows potential term
Let be an abelian group of charges and be a charge spectrum that assigns a multiset of charges to various field labels in an supersymmetric theory. A potential term is said to be **allowed** by the charge spectrum if the additive identity is an element of the multiset of all possible total charges associated with under the spectrum . More explicitly, if is an interaction term composed of fields , and assigns the multiset of charges to the field , then allows if there exists a selection of charges such that their sum vanishes: This condition signifies that there is a combination of field charges present in the spectrum that makes the potential term gauge-invariant (invariant under the symmetry group associated with ).
Let be a charge spectrum and be a potential term in an supersymmetric theory with charges in an abelian group . The spectrum allows the potential term if and only if the additive identity is an element of the multiset of possible total charges .
Decidability of
For a charge spectrum and a potential term within an theory, the property that allows (denoted ) is decidable, provided that equality is decidable in the underlying charge group . This means that it can be computationally determined whether there exists a selection of charges from assigned to the fields in such that their sum equals the additive identity .
Monotonicity of `AllowsTerm` under spectrum inclusion
Let be an abelian group of charges. For any potential term and any two charge spectra , if is a subset of (denoted ) and allows the potential term , then also allows the potential term .
Minimal charge spectrum form for potential term given
For a potential term and three charges in the charge group , the function `allowsTermForm` constructs a `ChargeSpectrum` representing the minimal set of charges assigned to the fields and required to allow that term. This spectrum is defined such that at least one combination of these charges satisfies the gauge invariance condition (the total charge sums to zero) for the specific interaction . The charge assignments for each potential term are as follows: - For (Higgs mass term ): has charge and has charge . - For (matter-Higgs mixing ): has charge and has charge . - For (trilinear matter interaction ): has charges and has charge . - For (): has charge and has charges . - For (): has charge and has charges . - For (): has charge and has charges . - For (): has charge , has charge , and has charge . - For (): has charge and has charges . - For (): has charge , has charge , and has charge . - For (): has charge and has charges . - For (): has charge , has charge , and has charge .
allows term
Let be an abelian group of charges and be a potential term in an supersymmetric theory. For any charges , the charge spectrum constructed by allows the potential term . This means there exists a selection of charges from the spectrum for the fields constituting such that their sum is the additive identity .
implies allows
Let be an abelian group of charges. For any potential term and charge spectrum , if there exist charges such that , then the charge spectrum allows the potential term . This means there exists a selection of charges from the spectrum for the fields constituting such that their sum is the additive identity .
for
Let be an abelian group of charges. For any charges and any potential term of the SUSY GUT, excluding the dimension-5 operators () and (), if the minimal charge spectrum is a subset of (denoted by the component-wise subset relation ), then the two charge spectra are equal: .
For any charges in the charge group and any potential term in an supersymmetric grand unified theory, the cardinality of the minimal charge spectrum constructed by is less than or equal to the degree of the potential term . Mathematically, this is expressed as: where denotes the total number of charges in the spectrum , and is the number of field labels that constitute the interaction term .
If allows , then for some
Let be an abelian group of charges. For any potential term and any charge spectrum over , if allows the potential term (meaning there exists a selection of charges for the fields in from the spectrum that sums to zero), then there exist charges such that the minimal charge spectrum is a subset of and itself allows the potential term .
Let be an abelian group of charges. For any potential term in an supersymmetric theory and any charge spectrum over , the spectrum allows the term if and only if there exist charges such that the minimal charge spectrum is a subset of .
If allows , there exists with that allows
Let be an abelian group of charges. Suppose an charge spectrum allows a potential term . Then there exists a subset charge spectrum such that also allows and the cardinality of is less than or equal to the degree of the term : where is the total number of charges in the spectrum , and is the number of fields constituting the interaction term .
Potential term is allowed by the addition of charge to
Given a charge spectrum with Higgs charges and sets of matter charges , the proposition `AllowsTermQ5 x q5 T` defines whether adding a charge to the representation allows the potential term due to the inclusion of . The conditions for each term are: - For : Always false. - For : and . - For : There exist and such that . - For : , , and . - For : There exist such that . - For : There exist such that . - For : Always false. - For the bottom Yukawa term: and there exists such that . - For the top Yukawa term: Always false. - For : Always false. - For : and there exists such that .
Decidability of whether adding charge allows potential term
Given a charge group with decidable equality, for any charge spectrum , charge , and potential term , it is decidable whether the term is allowed in the theory's potential due to the addition of to the representation matter charges. This decidability is established by evaluating the specific charge constraints associated with the term (such as the Higgs mass term , Yukawa couplings, or dimension-5 operators) against the charges present in and the additional charge .
Allowing with inserted implies `AllowsTerm` or `AllowsTermQ5`
Let be an abelian group of charges. Consider an SUSY GUT charge spectrum characterized by Higgs charges and finite sets of matter charges . For any potential term and any additional charge , if is allowed by the charge spectrum formed by inserting into the set (i.e., the spectrum ), then either the original spectrum already allows , or is allowed specifically due to the inclusion of as defined by the proposition `AllowsTermQ5`.
`AllowsTermQ5` implies `AllowsTerm` with inserted charge
Consider a charge spectrum with Higgs charges and sets of matter charges . For any potential term and charge , if is allowed due to the addition of to the representation (i.e., `AllowsTermQ5` holds for the spectrum and charge ), then the charge spectrum obtained by inserting into allows the potential term .
Allowance of with inserted `AllowsTerm` `AllowsTermQ5`
Let be an abelian group of charges. For any charge spectrum consisting of Higgs charges and finite sets of matter charges , and for any potential term and additional charge , the potential term is allowed by the augmented spectrum if and only if is allowed specifically due to the addition of to the representation (denoted by `AllowsTermQ5`) or is already allowed by the original spectrum .
Adding charge to the spectrum allows the potential term
Given a charge spectrum consisting of Higgs charges and , a set of charges for fields in the representation , and a set of charges for fields in the representation , the proposition `AllowsTermQ10 x q10 T` is true if the potential term is allowed by adding a specific charge to the -representation sector. The conditions for each potential term are as follows: - (trilinear matter interaction ): such that . - (Kähler term ): and such that . - (dimension-5 operator ): and such that . - (operator ): is present and such that . - : is present and such that . - : is present and such that . - (Kähler term ): and are both present and . - For , the proposition is always false.
Decidability of `AllowsTermQ10 x q10 T`
Given a charge spectrum (consisting of Higgs charges and finite sets of representation charges ), an potential term , and a specific charge , the proposition `AllowsTermQ10 x q10 T` is decidable, provided that equality in the charge group is decidable. This proposition determines whether the interaction term can be formed with total charge zero by selecting charges from the spectrum and the newly provided charge for the fields in the representation.
Allowedness of under implies `AllowsTerm` or `AllowsTermQ10`
Let be an abelian group of charges. Consider a potential term , a charge , and a charge spectrum consisting of Higgs charges , and sets of matter charges and . If the potential term is allowed by the charge spectrum obtained by adding to the -representation sector (i.e., using the set ), then either the original spectrum already allowed , or is allowed specifically due to the inclusion of the new charge (the condition `AllowsTermQ10 x q10 T` holds).
`AllowsTermQ10` implies `AllowsTerm` for spectrum with inserted
Let be an abelian group of charges. Consider a charge spectrum , where are optional Higgs charges and are finite sets of matter charges. For any potential term and any charge , if the proposition `AllowsTermQ10 x q10 T` holds (meaning is allowed specifically by using as a charge for a field in the representation), then the potential term is allowed by the augmented charge spectrum .
`AllowsTerm` with inserted iff `AllowsTermQ10` or `AllowsTerm`
Let be an abelian group of charges. Consider a potential term , a charge , and an charge spectrum . The augmented charge spectrum obtained by adding to the -representation sector, , allows the term if and only if either the original spectrum already allowed or the term is allowed specifically due to the inclusion of (i.e., the condition `AllowsTermQ10 x q10 T` holds).
