Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoClosed

Let $S_5 \subset \mathcal{Z}$ be a finite set of charges and $\mathcal{C}$ be a multiset of charge spectra. The proposition `IsPhenoClosedQ5` asserts that $\mathcal{C}$ is phenomenologically closed under the addition of $\bar{5}$ charges from $S_5$. Specifically, for every $q_5 \in S_5$ and every charge spectrum $x \in \mathcal{C}$, the modified charge spectrum $y = \langle x.q_{H_d}, x.q_{H_u}, x.Q_{\bar{5}} \cup \{q_5\}, x.Q_{10} \rangle$ must satisfy at least one of the following conditions: 1. $y$ is already contained in the multiset $\mathcal{C}$ ($y \in \mathcal{C}$). 2. $y$ is phenomenologically constrained ($\text{IsPhenoConstrained}(y)$), meaning it allows terms that lead to proton decay or R-parity violation (such as $\mu, \beta, \Lambda, W_i, K_i$). 3. $y$ generates dangerous couplings with a single singlet insertion ($\text{YukawaGeneratesDangerousAtLevel}(y, 1)$).

Let $S_5 \subset \mathcal{Z}$ be a finite set of charges and $\mathcal{C}$ be a multiset of charge spectra. The multiset $\mathcal{C}$ is phenomenologically closed under the addition of $\bar{5}$ charges from $S_5$ (denoted $\text{IsPhenoClosedQ5}(S_5, \mathcal{C})$) if for every charge $q_5 \in S_5$ and every charge spectrum $x \in \mathcal{C}$, the modified charge spectrum $y = \langle x.q_{H_d}, x.q_{H_u}, x.Q_{\bar{5}} \cup \{q_5\}, x.Q_{10} \rangle$ satisfies at least one of the following conditions: 1. The addition of the charge $q_5$ to the spectrum $x$ is phenomenologically constrained, meaning it allows terms that lead to proton decay or R-parity violation, such as $\mu, \beta, \Lambda, W_i, K_i$ ($\text{IsPhenoConstrainedQ5}(x, q_5)$). 2. the spectrum $y$ is already contained in the multiset $\mathcal{C}$ ($y \in \mathcal{C}$). 3. the spectrum $y$ generates dangerous couplings through the insertion of a single singlet ($\text{YukawaGeneratesDangerousAtLevel}(y, 1)$).

Let $S_{10} \subset \mathcal{Z}$ be a finite set of charges and $\mathcal{C}$ be a multiset of charge spectra over $\mathcal{Z}$. The proposition `IsPhenoClosedQ10` asserts that for every charge $q_{10} \in S_{10}$ and every charge spectrum $x \in \mathcal{C}$, the new spectrum $y$—formed by taking the Higgs charges ($q_{H_d}, q_{H_u}$) and the $5$-bar charges ($Q_{\bar{5}}$) from $x$, and adding $q_{10}$ to the multiset of $10$-dimensional charges $Q_{10}$—must satisfy at least one of the following conditions: 1. $y$ is phenomenologically constrained (`IsPhenoConstrained`). 2. $y$ is already contained in the multiset $\mathcal{C}$. 3. $y$ generates dangerous couplings via the insertion of one singlet (`YukawaGeneratesDangerousAtLevel y 1`).

Let $\mathcal{Z}$ be a group of charges and $S_{10} \subset \mathcal{Z}$ be a finite set of $10$-dimensional representation charges. Let $\mathcal{C}$ be a multiset of charge spectra. Suppose that for every charge $q_{10} \in S_{10}$ and every charge spectrum $x = \langle q_{H_d}, q_{H_u}, Q_{\bar{5}}, Q_{10} \rangle \in \mathcal{C}$, the spectrum $y = \langle q_{H_d}, q_{H_u}, Q_{\bar{5}}, Q_{10} \cup \{q_{10}\} \rangle$ satisfies at least one of the following conditions: 1. $x$ is phenomenologically constrained by the addition of $q_{10}$ ($\text{IsPhenoConstrainedQ10}(x, q_{10})$), meaning the inclusion of $q_{10}$ allows at least one dangerous superpotential or Kähler potential term (such as $\mu, \beta, \Lambda, W_i, K_i$). 2. $y$ is an element of the multiset $\mathcal{C}$. 3. $y$ generates dangerous couplings via the insertion of one singlet ($\text{YukawaGeneratesDangerousAtLevel}(y, 1)$). Then the multiset $\mathcal{C}$ is phenomenologically closed under the addition of $10$-dimensional charges from $S_{10}$.

Let $S_5$ and $S_{10}$ be finite sets of allowed $\overline{\mathbf{5}}$ and $\mathbf{10}$ charges in a group $\mathcal{Z}$, and let $\text{charges}$ be a multiset of charge spectra. The proposition `ContainsPhenoCompletionsOfMinimallyAllows` asserts that for every charge spectrum $x$ in the set of spectra that minimally allow the top Yukawa interaction (given $S_5$ and $S_{10}$), if $x$ is not phenomenologically constrained, then any completion $y$ of $x$ that is neither phenomenologically constrained nor generates dangerous couplings with one singlet insertion must be an element of the multiset $\text{charges}$. Here, a spectrum $y$ is "phenomenologically constrained" if it allows dangerous operators (such as those leading to proton decay), and "generates dangerous couplings" if the insertion of one singlet can regenerate such operators.

Let $S_5$ and $S_{10}$ be finite sets of charges in a group $\mathcal{Z}$, and let $\text{charges}$ be a multiset of charge spectra. The proposition `ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges` holds if and only if for every charge spectrum $x$ in the set of spectra that minimally allow the top Yukawa interaction (given $S_5$ and $S_{10}$), and for every completion $y$ of $x$ (relative to $S_5$), if $y$ is not phenomenologically constrained and does not generate dangerous couplings with one singlet insertion (level 1), then $y$ is an element of $\text{charges}$. Here, a spectrum $y$ is "phenomenologically constrained" if it allows dangerous operators (such as those leading to proton decay or R-parity violation), and it "generates dangerous couplings at level 1" if the insertion of one singlet can regenerate such operators.

Let $\mathcal{Z}$ be a group with decidable equality. Given finite sets of charges $S_5, S_{10} \subseteq \mathcal{Z}$ and a multiset of charge spectra $\text{charges}$, the proposition `ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges` is decidable. This proposition asserts that for every charge spectrum $x$ that minimally allows the top Yukawa interaction, any completion $y$ of $x$ (relative to $S_5$) that is not phenomenologically constrained and does not generate dangerous couplings with one singlet insertion must be an element of the multiset $\text{charges}$.

Let $S_5$ and $S_{10}$ be finite sets of allowed charges in $\mathcal{Z}$. Suppose that a multiset of charge spectra, $\text{charges}$, contains all phenomenologically viable completions of minimal top-Yukawa spectra. If $\text{charges}$ is a sub-multiset of another multiset $\text{charges}'$ (i.e., every element of $\text{charges}$ is also an element of $\text{charges}'$), then $\text{charges}'$ also contains all phenomenologically viable completions of minimal top-Yukawa spectra.

Given finite sets of charges $S_5, S_{10} \subseteq \mathcal{Z}$, the multiset `completeMinSubset` consists of the charge spectra obtained by taking all completions (relative to $S_5$) of those spectra that minimally allow the top Yukawa term. The resulting collection is deduplicated and then filtered to include only those spectra $x$ that are not phenomenologically constrained ($\neg \text{IsPhenoConstrained}(x)$) and do not generate dangerous couplings with one singlet insertion ($\neg \text{YukawaGeneratesDangerousAtLevel}(x, 1)$). This multiset is the unique minimal multiset that satisfies the condition of containing all phenomenologically viable completions of charge spectra permitting the top Yukawa coupling.

For any finite sets of charges $S_5, S_{10} \subseteq \mathcal{Z}$, the multiset of phenomenologically viable completions of charge spectra permitting the top Yukawa coupling, denoted `completeMinSubset S_5 S_{10}`, contains no duplicate elements.

Let $S_5$ and $S_{10}$ be finite sets of charges in a group $\mathcal{Z}$, and let $\text{charges}$ be a multiset of charge spectra. The multiset of charge spectra `completeMinSubset S5 S10` is a subset of $\text{charges}$ if and only if $\text{charges}$ satisfies the property `ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges`. Here, `completeMinSubset S5 S10` is defined as the minimal multiset containing all charge spectra $x$ that: 1. Are obtained as completions (relative to $S_5$) of spectra that minimally allow the top Yukawa term (given $S_5, S_{10}$). 2. Are not phenomenologically constrained ($\neg \text{IsPhenoConstrained}(x)$). 3. Do not generate dangerous couplings with one singlet insertion ($\neg \text{YukawaGeneratesDangerousAtLevel}(x, 1)$). The property `ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges` holds if every such phenomenologically viable completion $y$ of a minimal top-Yukawa spectrum $x$ is contained in the multiset $\text{charges}$.

For any finite sets of allowed $\bar{\mathbf{5}}$ and $\mathbf{10}$ charges $S_5, S_{10} \subseteq \mathcal{Z}$, the multiset `completeMinSubset S_5 S_{10}` satisfies the property `ContainsPhenoCompletionsOfMinimallyAllows`. Specifically, for every charge spectrum $x$ that minimally allows the top Yukawa interaction (given $S_5$ and $S_{10}$), if $x$ is not phenomenologically constrained, then any completion $y$ of $x$ (relative to $S_5$) that is neither phenomenologically constrained nor generates dangerous couplings with one singlet insertion is an element of the multiset `completeMinSubset S_5 S_{10}`.

Let $\mathcal{Z}$ be a group of charges and $S_5, S_{10} \subset \mathcal{Z}$ be finite sets of allowed $\bar{\mathbf{5}}$ and $\mathbf{10}$ charges, respectively. Let $\mathcal{C}$ be a multiset of charge spectra. Suppose that every spectrum $x \in \mathcal{C}$ satisfies the following conditions: 1. $x$ allows the top Yukawa interaction. 2. $x$ is not phenomenologically constrained (i.e., it does not allow terms such as $\mu, \beta, \Lambda, W_i, K_i$). 3. $x$ does not generate dangerous couplings with the insertion of one singlet (i.e., $\text{YukawaGeneratesDangerousAtLevel}(x, 1)$ is false). 4. $x$ is complete. Suppose further that: - $\mathcal{C}$ is phenomenologically closed under the addition of $\bar{\mathbf{5}}$ charges from $S_5$ (as defined by `IsPhenoClosedQ5`). - $\mathcal{C}$ is phenomenologically closed under the addition of $\mathbf{10}$ charges from $S_{10}$ (as defined by `IsPhenoClosedQ10`). - $\mathcal{C}$ contains all phenomenologically viable completions of spectra that minimally allow the top Yukawa interaction (as defined by `ContainsPhenoCompletionsOfMinimallyAllows`). Then, for any charge spectrum $x$ whose charges are restricted to the sets $S_5$ and $S_{10}$, $x$ is an element of the multiset $\mathcal{C}$ if and only if $x$ allows the top Yukawa interaction, is not phenomenologically constrained, does not generate dangerous couplings with one singlet insertion, and is complete.

Given finite sets $S_5, S_{10} \subseteq \mathcal{Z}$ of allowed $\bar{\mathbf{5}}$ and $\mathbf{10}$ charges, the multiset `viableChargesMultiset` consists of all charge spectra $x$ constructed from these sets that satisfy the following phenomenological criteria: 1. $x$ allows the top Yukawa interaction. 2. $x$ is not phenomenologically constrained ($\neg \text{IsPhenoConstrained}(x)$). 3. $x$ does not generate dangerous couplings with one singlet insertion ($\neg \text{YukawaGeneratesDangerousAtLevel}(x, 1)$). 4. $x$ is complete ($\text{IsComplete}(x)$). The multiset is constructed via a recursive process starting from `completeMinSubset S5 S10`. In each step, it identifies new charge spectra by taking minimal supersets (through the addition of charges from $S_5$ or $S_{10}$) of the current spectra, filtering for those that remain unconstrained and do not generate dangerous couplings, and adding them to the collection until no more such spectra can be found. The final result is deduplicated to ensure each valid charge spectrum appears exactly once.