Physlib

Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoConstrained

15 declarations

definition

Phenomenologically constrained charge spectrum

#IsPhenoConstrained

Let xx be a charge spectrum over a group Z\mathcal{Z}. The predicate `IsPhenoConstrained` is true for xx if xx allows any of the following terms: μ,β,Λ,W1,W2,W4,K1\mu, \beta, \Lambda, W_1, W_2, W_4, K_1, or K2K_2. 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.

instance

Decidability of whether a charge spectrum is phenomenologically constrained

#decidableIsPhenoConstrained

Let Z\mathcal{Z} be a group with decidable equality and xx be a charge spectrum over Z\mathcal{Z}. The property that xx is phenomenologically constrained, denoted as IsPhenoConstrained(x)\text{IsPhenoConstrained}(x), 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.

theorem

The empty charge spectrum \emptyset is not phenomenologically constrained

#not_isPhenoConstrained_empty

The empty charge spectrum \emptyset over a group Z\mathcal{Z} is not phenomenologically constrained. That is, the predicate `IsPhenoConstrained` is false for the spectrum containing no charges.

theorem

Monotonicity of the phenomenologically constrained property of charge spectra

#isPhenoConstrained_mono

Let xx and yy be charge spectra over a group Z\mathcal{Z}. If xx is a subset of yy (xyx \subseteq y) and xx is phenomenologically constrained, then yy is also phenomenologically constrained. A charge spectrum is phenomenologically constrained if it allows any of the terms μ,β,Λ,W1,W2,W4,K1\mu, \beta, \Lambda, W_1, W_2, W_4, K_1, or K2K_2, which correspond to superpotential or Kähler potential operators leading to proton decay or R-parity violation.

definition

Multiset of pheno-constraining superpotential charges of xx

#phenoConstrainingChargesSP

For a given charge spectrum xx with charges in a group Z\mathcal{Z}, 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 μ,β,Λ,W2,W4,\mu, \beta, \Lambda, W_2, W_4, and W1W_1 as determined by the spectrum xx.

theorem

The multiset of pheno-constraining superpotential charges for the empty spectrum is empty

#phenoConstrainingChargesSP_empty

For a given group of charges Z\mathcal{Z}, the multiset of charges associated with pheno-constraining superpotential terms (such as μ,β,Λ,W1,W2\mu, \beta, \Lambda, W_1, W_2, and W4W_4) for the empty charge spectrum \emptyset is the empty multiset \emptyset.

theorem

Monotonicity of pheno-constraining superpotential charges: xy    x.phenoConstrainingChargesSPy.phenoConstrainingChargesSPx \subseteq y \implies x.\text{phenoConstrainingChargesSP} \subseteq y.\text{phenoConstrainingChargesSP}

#phenoConstrainingChargesSP_mono

Let Z\mathcal{Z} be a group of charges. Given two charge spectra xx and yy such that xyx \subseteq y, the multiset of charges of the pheno-constraining superpotential terms (the charges of terms μ,β,Λ,W1,W2,W4\mu, \beta, \Lambda, W_1, W_2, W_4 as determined by the spectrum) for xx is a sub-multiset of those for yy: xy    x.phenoConstrainingChargesSPy.phenoConstrainingChargesSP.x \subseteq y \implies x.\text{phenoConstrainingChargesSP} \subseteq y.\text{phenoConstrainingChargesSP}.

definition

Phenomenological constraint of a charge spectrum xx with additional charge q5q_5

#IsPhenoConstrainedQ5

For a given charge spectrum xx and a charge q5q_5, the predicate `IsPhenoConstrainedQ5` is defined as the condition that the addition of q5q_5 to the spectrum xx allows at least one of the following phenomenologically constrained terms: μ,β,Λ,W1,W2,W4,K1,\mu, \beta, \Lambda, W_1, W_2, W_4, K_1, or K2K_2. These terms typically correspond to superpotential or Kähler potential operators that lead to physical effects such as proton decay or R-parity violation.

theorem

x.IsPhenoConstrainedQ5(q5)x.\text{IsPhenoConstrainedQ5}(q_5) iff β,Λ,W4,K1,\beta, \Lambda, W_4, K_1, or W1W_1 is allowed

#isPhenoConstrainedQ5_iff

For a charge spectrum xx and a charge q5Zq_5 \in \mathcal{Z}, the condition that the addition of q5q_5 to the Q5Q_5 set of xx makes the spectrum phenomenologically constrained (denoted by `IsPhenoConstrainedQ5`) is equivalent to the spectrum allowing at least one of the following physical terms: β,Λ,W4,K1,\beta, \Lambda, W_4, K_1, or W1W_1. That is, x.IsPhenoConstrainedQ5(q5)    AllowsTermQ5(x,q5,β)AllowsTermQ5(x,q5,W1).x.\text{IsPhenoConstrainedQ5}(q_5) \iff \text{AllowsTermQ5}(x, q_5, \beta) \lor \dots \lor \text{AllowsTermQ5}(x, q_5, W_1).

instance

Decidability of `IsPhenoConstrainedQ5` for a charge spectrum xx and charge q5q_5

#decidableIsPhenoConstrainedQ5

For a given charge spectrum xx and a charge q5Zq_5 \in \mathcal{Z}, the predicate `IsPhenoConstrainedQ5` is decidable. This means there is an algorithmic procedure to determine whether the addition of the charge q5q_5 to the spectrum xx allows terms in the superpotential or Kähler potential—specifically β,Λ,W4,K1\beta, \Lambda, W_4, K_1, or W1W_1—that lead to phenomenological issues such as proton decay or R-parity violation.

theorem

`IsPhenoConstrained` with q5Q5q_5 \in Q_5 iff `IsPhenoConstrainedQ5` holds or the spectrum is already constrained

#isPhenoConstrained_insertQ5_iff_isPhenoConstrainedQ5

Let x=qHd,qHu,Q5,Q10x = \langle q_{H_d}, q_{H_u}, Q_5, Q_{10} \rangle be a charge spectrum over a group Z\mathcal{Z}. For any charge q5Zq_5 \in \mathcal{Z}, the charge spectrum qHd,qHu,Q5{q5},Q10\langle q_{H_d}, q_{H_u}, Q_5 \cup \{q_5\}, Q_{10} \rangle is phenomenologically constrained if and only if either the addition of q5q_5 to xx satisfies the predicate `IsPhenoConstrainedQ5` or the original spectrum xx is already phenomenologically constrained.

definition

xx is phenomenologically constrained by q10q_{10}

#IsPhenoConstrainedQ10

Given a charge spectrum xx and a specific charge q10Zq_{10} \in \mathcal{Z} (representing a charge in the 10\mathbf{10} representation of SU(5)SU(5)), the proposition `IsPhenoConstrainedQ10` is true if the inclusion of q10q_{10} allows at least one of the following terms in the superpotential or Kähler potential: μ,β,Λ,W1,W2,W4,K1\mu, \beta, \Lambda, W_1, W_2, W_4, K_1, or K2K_2. These terms typically correspond to operators that lead to proton decay or R-parity violation in the phenomenological analysis of the model.

theorem

x.IsPhenoConstrainedQ10 q10    x.\text{IsPhenoConstrainedQ10 } q_{10} \iff allowing Λ,W1,W2,K1\Lambda, W_1, W_2, K_1, or K2K_2

#isPhenoConstrainedQ10_iff

For a charge spectrum xx and a charge q10Zq_{10} \in \mathcal{Z}, the spectrum is phenomenologically constrained by the addition of q10q_{10} (denoted by `IsPhenoConstrainedQ10`) if and only if the inclusion of q10q_{10} allows at least one of the following terms: Λ,W1,W2,K1\Lambda, W_1, W_2, K_1, or K2K_2. These terms typically correspond to operators in the superpotential or Kähler potential that lead to proton decay or R-parity violation.

instance

Decidability of whether xx is phenomenologically constrained by q10q_{10}

#decidableIsPhenoConstrainedQ10

For a given charge spectrum xx and a specific charge q10Zq_{10} \in \mathcal{Z} (representing a charge in the 10\mathbf{10} representation of SU(5)SU(5)), the property that the spectrum is phenomenologically constrained by q10q_{10} (denoted as x.IsPhenoConstrainedQ10(q10)x.\text{IsPhenoConstrainedQ10}(q_{10})) is decidable. This means there is a computational procedure to determine if the inclusion of q10q_{10} allows terms in the superpotential or Kähler potential—specifically Λ,W1,W2,K1\Lambda, W_1, W_2, K_1, or K2K_2—which correspond to operators leading to proton decay or R-parity violation.

theorem

IsPhenoConstrained\text{IsPhenoConstrained} with added q10q_{10} iff IsPhenoConstrainedQ10 q10IsPhenoConstrained\text{IsPhenoConstrainedQ10 } q_{10} \lor \text{IsPhenoConstrained}

#isPhenoConstrained_insertQ10_iff_isPhenoConstrainedQ10

For a charge spectrum x=qHd,qHu,Q5,Q10x = \langle q_{H_d}, q_{H_u}, Q_5, Q_{10} \rangle over a group Z\mathcal{Z} and a charge q10Zq_{10} \in \mathcal{Z}, the spectrum qHd,qHu,Q5,Q10{q10}\langle q_{H_d}, q_{H_u}, Q_5, Q_{10} \cup \{q_{10}\} \rangle is phenomenologically constrained if and only if xx is phenomenologically constrained by the addition of q10q_{10} (denoted as x.IsPhenoConstrainedQ10(q10)x.\text{IsPhenoConstrainedQ10}(q_{10})) or the original spectrum xx is already phenomenologically constrained. A charge spectrum is phenomenologically constrained if it allows terms in the superpotential or Kähler potential (such as μ,β,Λ,Wi,Ki\mu, \beta, \Lambda, W_i, K_i) that lead to proton decay or RR-parity violation.