Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoConstrained
15 declarations
Phenomenologically constrained charge spectrum
#IsPhenoConstrainedLet be a charge spectrum over a group . The predicate `IsPhenoConstrained` is true for if allows any of the following terms: , or . Mathematically, this is defined as the disjunction: \[ \text{AllowsTerm}(x, \mu) \lor \text{AllowsTerm}(x, \beta) \lor \text{AllowsTerm}(x, \Lambda) \lor \text{AllowsTerm}(x, W_2) \lor \text{AllowsTerm}(x, W_4) \lor \text{AllowsTerm}(x, K_1) \lor \text{AllowsTerm}(x, K_2) \lor \text{AllowsTerm}(x, W_1) \] In the context of SU(5) supersymmetry, these terms correspond to operators in the superpotential or Kähler potential that lead to proton decay or R-parity violation.
Decidability of whether a charge spectrum is phenomenologically constrained
#decidableIsPhenoConstrainedLet be a group with decidable equality and be a charge spectrum over . The property that is phenomenologically constrained, denoted as , is decidable. This predicate is defined as the disjunction of whether the spectrum allows any of the following terms: \[ \text{AllowsTerm}(x, \mu) \lor \text{AllowsTerm}(x, \beta) \lor \text{AllowsTerm}(x, \Lambda) \lor \text{AllowsTerm}(x, W_2) \lor \text{AllowsTerm}(x, W_4) \lor \text{AllowsTerm}(x, K_1) \lor \text{AllowsTerm}(x, K_2) \lor \text{AllowsTerm}(x, W_1) \] In the context of SU(5) supersymmetry, these terms correspond to operators in the superpotential or Kähler potential that lead to proton decay or R-parity violation.
The empty charge spectrum is not phenomenologically constrained
#not_isPhenoConstrained_emptyThe empty charge spectrum over a group is not phenomenologically constrained. That is, the predicate `IsPhenoConstrained` is false for the spectrum containing no charges.
Monotonicity of the phenomenologically constrained property of charge spectra
#isPhenoConstrained_monoLet and be charge spectra over a group . If is a subset of () and is phenomenologically constrained, then is also phenomenologically constrained. A charge spectrum is phenomenologically constrained if it allows any of the terms , or , which correspond to superpotential or Kähler potential operators leading to proton decay or R-parity violation.
Multiset of pheno-constraining superpotential charges of
#phenoConstrainingChargesSPFor a given charge spectrum with charges in a group , this function computes the multiset of charges associated with specific superpotential terms that lead to a phenomenologically constrained model (one allowing proton decay or R-parity violation). The resulting multiset is the sum of the charges of the potential terms and as determined by the spectrum .
The multiset of pheno-constraining superpotential charges for the empty spectrum is empty
#phenoConstrainingChargesSP_emptyFor a given group of charges , the multiset of charges associated with pheno-constraining superpotential terms (such as , and ) for the empty charge spectrum is the empty multiset .
Monotonicity of pheno-constraining superpotential charges:
#phenoConstrainingChargesSP_monoLet be a group of charges. Given two charge spectra and such that , the multiset of charges of the pheno-constraining superpotential terms (the charges of terms as determined by the spectrum) for is a sub-multiset of those for :
Phenomenological constraint of a charge spectrum with additional charge
#IsPhenoConstrainedQ5For a given charge spectrum and a charge , the predicate `IsPhenoConstrainedQ5` is defined as the condition that the addition of to the spectrum allows at least one of the following phenomenologically constrained terms: or . These terms typically correspond to superpotential or Kähler potential operators that lead to physical effects such as proton decay or R-parity violation.
iff or is allowed
#isPhenoConstrainedQ5_iffFor a charge spectrum and a charge , the condition that the addition of to the set of makes the spectrum phenomenologically constrained (denoted by `IsPhenoConstrainedQ5`) is equivalent to the spectrum allowing at least one of the following physical terms: or . That is,
Decidability of `IsPhenoConstrainedQ5` for a charge spectrum and charge
#decidableIsPhenoConstrainedQ5For a given charge spectrum and a charge , the predicate `IsPhenoConstrainedQ5` is decidable. This means there is an algorithmic procedure to determine whether the addition of the charge to the spectrum allows terms in the superpotential or Kähler potential—specifically , or —that lead to phenomenological issues such as proton decay or R-parity violation.
`IsPhenoConstrained` with iff `IsPhenoConstrainedQ5` holds or the spectrum is already constrained
#isPhenoConstrained_insertQ5_iff_isPhenoConstrainedQ5Let be a charge spectrum over a group . For any charge , the charge spectrum is phenomenologically constrained if and only if either the addition of to satisfies the predicate `IsPhenoConstrainedQ5` or the original spectrum is already phenomenologically constrained.
is phenomenologically constrained by
#IsPhenoConstrainedQ10Given a charge spectrum and a specific charge (representing a charge in the representation of ), the proposition `IsPhenoConstrainedQ10` is true if the inclusion of allows at least one of the following terms in the superpotential or Kähler potential: , or . These terms typically correspond to operators that lead to proton decay or R-parity violation in the phenomenological analysis of the model.
allowing , or
#isPhenoConstrainedQ10_iffFor a charge spectrum and a charge , the spectrum is phenomenologically constrained by the addition of (denoted by `IsPhenoConstrainedQ10`) if and only if the inclusion of allows at least one of the following terms: , or . These terms typically correspond to operators in the superpotential or Kähler potential that lead to proton decay or R-parity violation.
Decidability of whether is phenomenologically constrained by
#decidableIsPhenoConstrainedQ10For a given charge spectrum and a specific charge (representing a charge in the representation of ), the property that the spectrum is phenomenologically constrained by (denoted as ) is decidable. This means there is a computational procedure to determine if the inclusion of allows terms in the superpotential or Kähler potential—specifically , or —which correspond to operators leading to proton decay or R-parity violation.
with added iff
#isPhenoConstrained_insertQ10_iff_isPhenoConstrainedQ10For a charge spectrum over a group and a charge , the spectrum is phenomenologically constrained if and only if is phenomenologically constrained by the addition of (denoted as ) or the original spectrum is already phenomenologically constrained. A charge spectrum is phenomenologically constrained if it allows terms in the superpotential or Kähler potential (such as ) that lead to proton decay or -parity violation.
