Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Basic

For a type of charges $\mathcal{Z}$ with decidable equality, the equality between any two charge spectra $s_1, s_2 \in \text{ChargeSpectrum } \mathcal{Z}$ is also decidable.

For a given type of charges $\mathcal{Z}$, there exists an equivalence (bijection) between the charge spectrum $\text{ChargeSpectrum } \mathcal{Z}$ and the product type $\text{Option } \mathcal{Z} \times \text{Option } \mathcal{Z} \times \text{Finset } \mathcal{Z} \times \text{Finset } \mathcal{Z}$. This mapping sends a charge spectrum $s$ to a quadruple $(q_{H_d}, q_{H_u}, Q_{\bar{5}}, Q_{10})$, where $q_{H_d}$ and $q_{H_u}$ represent the optional charges of the $H_d$ and $H_u$ Higgs fields, and $Q_{\bar{5}}$ and $Q_{10}$ are finite sets of charges corresponding to the $\mathbf{\bar{5}}$ and $\mathbf{10}$ matter representations, respectively.

Given a type of charges $\mathcal{Z}$ that possesses a string representation, this definition provides a string representation for a charge spectrum $s \in \text{ChargeSpectrum } \mathcal{Z}$. If the charge spectrum is given by the quadruple $s = \langle q_{H_d}, q_{H_u}, Q_{\bar{5}}, Q_{10} \rangle$—where $q_{H_d}$ and $q_{H_u}$ are the optional charges of the $H_d$ and $H_u$ Higgs fields, and $Q_{\bar{5}}$ and $Q_{10}$ are finite sets of charges for the $\mathbf{\bar{5}}$ and $\mathbf{10}$ matter representations respectively—it is represented as a string in the format $\langle q_{H_d}, q_{H_u}, Q_{\bar{5}}, Q_{10} \rangle$.

For two $SU(5)$ charge spectra $x, y \in \text{ChargeSpectrum } \mathcal{Z}$, the subset relation $x \subseteq y$ is defined by the component-wise subset inclusion of their constituent charges. Specifically, $x \subseteq y$ if and only if: 1. $\text{toFinset}(x.q_{H_d}) \subseteq \text{toFinset}(y.q_{H_d})$ 2. $\text{toFinset}(x.q_{H_u}) \subseteq \text{toFinset}(y.q_{H_u})$ 3. $x.Q_{\bar{5}} \subseteq y.Q_{\bar{5}}$ 4. $x.Q_{10} \subseteq y.Q_{10}$ where $q_{H_d}$ and $q_{H_u}$ are the optional charges of the $H_d$ and $H_u$ Higgs fields, $Q_{\bar{5}}$ and $Q_{10}$ are the finite sets of charges for the $\mathbf{\bar{5}}$ and $\mathbf{10}$ matter representations, and $\text{toFinset}$ is the mapping that sends an optional value to a singleton set if it exists or to the empty set otherwise.

For two $SU(5)$ charge spectra $x, y \in \text{ChargeSpectrum } \mathcal{Z}$, the strict subset relation $x \subset y$ is defined to hold if and only if $x$ is a subset of $y$ ($x \subseteq y$) and $x$ is not equal to $y$ ($x \neq y$).

Given a type $\mathcal{Z}$ with decidable equality, the subset relation $x \subseteq y$ between two $SU(5)$ charge spectra $x, y \in \text{ChargeSpectrum } \mathcal{Z}$ is decidable. This means there is an algorithm to determine whether $x \subseteq y$, which is defined by the conjunction of the following conditions: 1. $\text{toFinset}(x.q_{H_d}) \subseteq \text{toFinset}(y.q_{H_d})$ 2. $\text{toFinset}(x.q_{H_u}) \subseteq \text{toFinset}(y.q_{H_u})$ 3. $x.Q_{\bar{5}} \subseteq y.Q_{\bar{5}}$ 4. $x.Q_{10} \subseteq y.Q_{10}$ where $q_{H_d}$ and $q_{H_u}$ are optional charges for the Higgs fields, $Q_{\bar{5}}$ and $Q_{10}$ are finite sets of charges for the matter representations, and $\text{toFinset}$ converts optional values into singleton or empty sets.

For any two $SU(5)$ charge spectra $x, y \in \text{ChargeSpectrum } \mathcal{Z}$, the subset relation $x \subseteq y$ holds if and only if: 1. $\text{toFinset}(x.q_{H_d}) \subseteq \text{toFinset}(y.q_{H_d})$ 2. $\text{toFinset}(x.q_{H_u}) \subseteq \text{toFinset}(y.q_{H_u})$ 3. $x.Q_{\bar{5}} \subseteq y.Q_{\bar{5}}$ 4. $x.Q_{10} \subseteq y.Q_{10}$ where $q_{H_d}$ and $q_{H_u}$ are the optional charges of the $H_d$ and $H_u$ Higgs fields, $Q_{\bar{5}}$ and $Q_{10}$ are the finite sets of charges for the $\mathbf{\bar{5}}$ and $\mathbf{10}$ matter representations, and $\text{toFinset}$ is a function that maps an optional value to a singleton set containing the value if it exists, or to the empty set otherwise.

For any $SU(5)$ charge spectrum $x \in \text{ChargeSpectrum } \mathcal{Z}$, the subset relation $x \subseteq x$ holds. This relation is defined as the component-wise subset inclusion of the charges associated with the Higgs fields and matter representations within the spectrum.

For any two optional values $x$ and $y$ of type $\mathcal{Z}$, the values are equal ($x = y$) if and only if their corresponding finite sets are equal ($x.\text{toFinset} = y.\text{toFinset}$). Here, the finite set representation of an optional value is the singleton set $\{z\}$ if the value exists (i.e., $x = \text{some } z$), and the empty set $\emptyset$ if the value is absent (i.e., $x = \text{none}$).

Let $x, y, z \in \text{ChargeSpectrum } \mathcal{Z}$ be charge spectra in an $SU(5)$ SUSY GUT. If $x \subseteq y$ and $y \subseteq z$, then $x \subseteq z$.

For any two $SU(5)$ SUSY GUT charge spectra $x, y \in \text{ChargeSpectrum } \mathcal{Z}$, if $x \subseteq y$ and $y \subseteq x$, then $x = y$. The subset relation $x \subseteq y$ is defined by the component-wise inclusion of the charges associated with the theory's particles. Specifically, $x \subseteq y$ if and only if: 1. $\text{toFinset}(x.q_{H_d}) \subseteq \text{toFinset}(y.q_{H_d})$ 2. $\text{toFinset}(x.q_{H_u}) \subseteq \text{toFinset}(y.q_{H_u})$ 3. $x.Q_{\bar{5}} \subseteq y.Q_{\bar{5}}$ 4. $x.Q_{10} \subseteq y.Q_{10}$ where $q_{H_d}$ and $q_{H_u}$ are the optional charges of the $H_d$ and $H_u$ Higgs fields, $Q_{\bar{5}}$ and $Q_{10}$ are the finite sets of charges for the $\mathbf{\bar{5}}$ and $\mathbf{10}$ matter representations, and $\text{toFinset}$ maps an optional value to a singleton set if it exists or to an empty set if it is absent.

The empty charge spectrum $\emptyset \in \text{ChargeSpectrum } \mathcal{Z}$ is defined as the specific configuration where no particles are present. Formally, it is represented by the quadruple $(\text{none}, \text{none}, \emptyset, \emptyset)$, indicating that: - The optional Higgs down ($H_d$) charge is absent. - The optional Higgs up ($H_u$) charge is absent. - The finite set of charges for matter in the $\bar{\mathbf{5}}$ representation is empty. - The finite set of charges for matter in the $\mathbf{10}$ representation is empty.

In the context of $SU(5)$ SUSY GUT theories, the empty charge spectrum $\emptyset \in \text{ChargeSpectrum } \mathcal{Z}$ is equal to the quadruple $(\text{none}, \text{none}, \emptyset, \emptyset)$. This represents a configuration where: - The optional Higgs down ($H_d$) charge is absent ($\text{none}$). - The optional Higgs up ($H_u$) charge is absent ($\text{none}$). - The set of charges for matter in the $\bar{\mathbf{5}}$ representation is empty ($\emptyset$). - The set of charges for matter in the $\mathbf{10}$ representation is empty ($\emptyset$).

For any $SU(5)$ charge spectrum $x \in \text{ChargeSpectrum } \mathcal{Z}$, the empty charge spectrum $\emptyset$ is a subset of $x$, denoted as $\emptyset \subseteq x$.

For any $SU(5)$ charge spectrum $x \in \text{ChargeSpectrum } \mathcal{Z}$, it holds that $x \subseteq \emptyset$ if and only if $x = \emptyset$. Here, $\emptyset$ denotes the empty charge spectrum where no particles are present.

In an $SU(5)$ SUSY GUT theory, the charge of the Higgs down particle ($H_d$) in the empty charge spectrum $\emptyset \in \text{ChargeSpectrum } \mathcal{Z}$, denoted by $q_{H_d}$, is $\text{none}$, indicating that the particle is absent from the spectrum.

In an $SU(5)$ SUSY GUT theory, the optional charge of the Higgs up ($H_u$) particle in the empty charge spectrum $\emptyset$, denoted by $q_{H_u}$, is absent (represented by `none`).

In an $SU(5)$ SUSY GUT theory, the finite set of charges for matter in the $\bar{\mathbf{5}}$ representation of the empty charge spectrum $\emptyset$, denoted by $Q_{\bar{5}}$, is the empty set $\emptyset$.

In an $SU(5)$ SUSY GUT theory, the finite set of charges for matter in the $\mathbf{10}$ representation of the empty charge spectrum $\emptyset$, denoted by $Q_{10}$, is the empty set $\emptyset$.

The cardinality of a charge spectrum $x$ is the sum of the sizes of its constituent charge sets. Specifically, it is defined as: \[ \text{card}(x) = |q_{H_u}| + |q_{H_d}| + |Q_5| + |Q_{10}| \] where $|q_{H_u}|$ and $|q_{H_d}|$ are the cardinalities of the optional charges for the $H_u$ and $H_d$ particles (equal to $1$ if the charge is present and $0$ if it is absent), and $|Q_5|$ and $|Q_{10}|$ are the cardinalities of the finite sets of charges for the $\bar{5}$ and $10$ representations, respectively.

For an $SU(5)$ SUSY GUT theory, the cardinality of the empty charge spectrum $\emptyset \in \text{ChargeSpectrum } \mathcal{Z}$ is equal to $0$.

For any two $SU(5)$ charge spectra $x$ and $y$ with charges in $\mathcal{Z}$, if $x \subseteq y$ (meaning each constituent set of charges in $x$ is a subset of the corresponding set in $y$), then the cardinality of $x$ is less than or equal to the cardinality of $y$, denoted as $\text{card}(x) \le \text{card}(y)$.

Given a set of charges $\mathcal{Z}$, let $\text{Option } \mathcal{Z}$ denote the type representing an optional value, which is either a value from $\mathcal{Z}$ (denoted $\text{some } y$ for $y \in \mathcal{Z}$) or an empty value (denoted $\text{none}$). For an element $x \in \text{Option } \mathcal{Z}$, the powerset function returns a finite set of optional values defined by: \[ \text{powerset}(x) = \begin{cases} \{ \text{none} \} & \text{if } x = \text{none} \\ \{ \text{none}, \text{some } y \} & \text{if } x = \text{some } y \end{cases} \] This construction treats $x$ as a set of at most one element and returns the set containing all its possible "subsets" in the $\text{Option}$ type representation.

For any optional values $x, y$ of type $\text{Option } \mathcal{Z}$, $y$ is an element of the powerset of $x$ if and only if the finite set representation of $y$ is a subset of the finite set representation of $x$. Here, the finite set representation $\text{toFinset}(a)$ is defined as the empty set $\emptyset$ if $a = \text{none}$ and the singleton set $\{z\}$ if $a = \text{some } z$.

For a given charge spectrum $x \in \text{ChargeSpectrum } \mathcal{Z}$, its powerset is the finite set consisting of all charge spectra $y$ that are subsets of $x$ (denoted $y \subseteq x$). If the spectrum $x$ is represented by the components $(q_{H_d}, q_{H_u}, Q_{\bar{5}}, Q_{10})$, where $q_{H_d}$ and $q_{H_u}$ are optional charges for the Higgs fields and $Q_{\bar{5}}, Q_{10}$ are finite sets of matter charges, then a spectrum $y = (q'_{H_d}, q'_{H_u}, Q'_{\bar{5}}, Q'_{10})$ belongs to the powerset if and only if: - $q'_{H_d}$ is a subset of $q_{H_d}$ in the sense of the optional type (i.e., $q'_{H_d} = q_{H_d}$ or $q'_{H_d} = \text{none}$), - $q'_{H_u}$ is a subset of $q_{H_u}$, - $Q'_{\bar{5}} \subseteq Q_{\bar{5}}$, and - $Q'_{10} \subseteq Q_{10}$.

For any two $SU(5)$ charge spectra $x, y \in \text{ChargeSpectrum } \mathcal{Z}$, the spectrum $x$ is an element of the powerset of $y$ if and only if each of its components is an element of the powerset of the corresponding component in $y$. That is, \[ x \in \text{powerset}(y) \iff x.q_{H_d} \in \text{powerset}(y.q_{H_d}) \land x.q_{H_u} \in \text{powerset}(y.q_{H_u}) \land x.Q_{\bar{5}} \in \text{powerset}(y.Q_{\bar{5}}) \land x.Q_{10} \in \text{powerset}(y.Q_{10}) \] where $q_{H_d}$ and $q_{H_u}$ are the optional Higgs charges, $Q_{\bar{5}}$ and $Q_{10}$ are the finite sets of matter charges, and $\text{powerset}$ denotes the power set operation defined for the respective types.

For any two $SU(5)$ charge spectra $x, y \in \text{ChargeSpectrum } \mathcal{Z}$, $x$ is an element of the powerset of $y$ if and only if $x$ is a subset of $y$ ($x \subseteq y$). Here, the subset relation for charge spectra is defined by the component-wise inclusion of the charges for the Higgs fields $H_d, H_u$ and the matter representations $\mathbf{\bar{5}}, \mathbf{10}$.

For any $SU(5)$ SUSY GUT charge spectrum $x \in \text{ChargeSpectrum } \mathcal{Z}$, it holds that $x$ is an element of its own powerset, denoted as $x \in \text{powerset } x$.

For any $SU(5)$ charge spectrum $x \in \text{ChargeSpectrum } \mathcal{Z}$, the empty charge spectrum $\emptyset$ is an element of the powerset of $x$.

The powerset of the empty $SU(5)$ charge spectrum $\emptyset \in \text{ChargeSpectrum } \mathcal{Z}$ is equal to the singleton set containing only the empty charge spectrum itself, denoted as $\{\emptyset\}$.

For any two $SU(5)$ charge spectra $x, y \in \text{ChargeSpectrum } \mathcal{Z}$, the powerset of $x$ is a subset of the powerset of $y$ if and only if $x$ is a subset of $y$. In mathematical notation, this is expressed as: $$\text{powerset } x \subseteq \text{powerset } y \iff x \subseteq y$$ where the powerset of a spectrum consists of all spectra that are its subsets.

Let $S$ be a non-empty finite set of $SU(5)$ charge spectra over a type of charges $\mathcal{Z}$. For any natural number $n$ such that the cardinality of the set is $|S| = n$, there exists a charge spectrum $y \in S$ such that the intersection of its powerset and $S$ contains only $y$ itself, i.e., $\text{powerset}(y) \cap S = \{y\}$. Here, $\text{powerset}(y)$ is the set of all charge spectra $z$ such that $z \subseteq y$. This property implies that $y$ is a minimal element of $S$ with respect to the subset relation.

Let $S$ be a non-empty finite set of $SU(5)$ charge spectra over a type of charges $\mathcal{Z}$. There exists a charge spectrum $y \in S$ such that the intersection of its powerset and $S$ is the singleton set $\{y\}$. Here, $\text{powerset}(y)$ is defined as the set of all charge spectra $z$ such that $z \subseteq y$. This condition implies that $y$ is a minimal element of $S$ with respect to the subset relation.

Given two finite sets of charges $S_{\bar{5}}, S_{10} \subset \mathcal{Z}$, this function defines the finite set of all charge spectra $x \in \text{ChargeSpectrum } \mathcal{Z}$ such that the charges associated with the $\mathbf{\bar{5}}$ representations (the optional $H_d$ and $H_u$ Higgs charges and the set of matter charges $Q_{\bar{5}}$) are contained in $S_{\bar{5}}$, and the charges associated with the $\mathbf{10}$ representation ($Q_{10}$) are contained in $S_{10}$. Specifically, $x$ is an element of the resulting set if $x.q_{H_d} \in S_{\bar{5}} \cup \{\text{none}\}$, $x.q_{H_u} \in S_{\bar{5}} \cup \{\text{none}\}$, $x.Q_{\bar{5}} \subseteq S_{\bar{5}}$, and $x.Q_{10} \subseteq S_{10}$.

For any finite sets of charges $S_{\bar{5}}, S_{10} \subseteq \mathcal{Z}$, a charge spectrum $x \in \text{ChargeSpectrum } \mathcal{Z}$ belongs to the finite set `ofFinset` $S_{\bar{5}} S_{10}$ if and only if the following conditions hold: - The finite set representation of the optional $H_d$ Higgs charge, $q_{H_d}$, is a subset of $S_{\bar{5}}$. - The finite set representation of the optional $H_u$ Higgs charge, $q_{H_u}$, is a subset of $S_{\bar{5}}$. - The set of $\bar{5}$ matter charges $Q_{\bar{5}}$ is a subset of $S_{\bar{5}}$. - The set of $10$ matter charges $Q_{10}$ is a subset of $S_{10}$. (Note: For an optional charge $q$, its finite set representation is $\{q\}$ if the particle exists and $\emptyset$ otherwise.)

Let $\mathcal{Z}$ be a type of charges and $S_{\bar{5}}, S_{10} \subseteq \mathcal{Z}$ be finite sets. For any two charge spectra $x, y \in \text{ChargeSpectrum } \mathcal{Z}$, if $x \subseteq y$ and $y \in \text{ofFinset } S_{\bar{5}} S_{10}$, then $x \in \text{ofFinset } S_{\bar{5}} S_{10}$. Here, the subset relation $x \subseteq y$ indicates that each component of the charge spectrum $x$ (the optional Higgs charges $q_{H_d}, q_{H_u}$ and the matter charge sets $Q_{\bar{5}}, Q_{10}$) is contained within the corresponding component of $y$. The set $\text{ofFinset } S_{\bar{5}} S_{10}$ consists of all charge spectra whose $\mathbf{\bar{5}}$-representation charges are contained in $S_{\bar{5}}$ and whose $\mathbf{10}$-representation charges are contained in $S_{10}$.

Let $\mathcal{Z}$ be the type of charges. For any finite sets of charges $S_{\bar{5}}, S_{\bar{5}}', S_{10}, S_{10}' \subseteq \mathcal{Z}$, if $S_{\bar{5}} \subseteq S_{\bar{5}}'$ and $S_{10} \subseteq S_{10}'$, then the set of charge spectra $\text{ofFinset}(S_{\bar{5}}, S_{10})$ is a subset of $\text{ofFinset}(S_{\bar{5}}', S_{10}')$. Here, $\text{ofFinset}(S_{\bar{5}}, S_{10})$ is defined as the finite set of all $SU(5)$ SUSY GUT charge spectra $x$ such that: - The charges of the optional Higgs particles $H_d$ and $H_u$ (if they exist) are contained in $S_{\bar{5}}$. - The set of matter charges in the $\mathbf{\bar{5}}$ representation, $Q_{\bar{5}}$, is a subset of $S_{\bar{5}}$. - The set of matter charges in the $\mathbf{10}$ representation, $Q_{10}$, is a subset of $S_{10}$.

If the type of charges $\mathcal{Z}$ is finite, then for any charge spectrum $x \in \text{ChargeSpectrum } \mathcal{Z}$, $x$ is an element of the set of charge spectra whose charges are restricted to the universal set of all possible charges in $\mathcal{Z}$. That is, $x \in \text{ofFinset } (\text{univ } \mathcal{Z}) (\text{univ } \mathcal{Z})$.

Given two finite sets of charges $S_5$ and $S_{10}$ in the charge space $\mathcal{Z}$, this definition calculates the cardinality of the set of all possible $SU(5)$ SUSY GUT charge spectra restricted to these sets. The value is given by: \[ (|S_5| + 1)^2 \cdot 2^{|S_5|} \cdot 2^{|S_{10}|} \] where $|S_5|$ and $|S_{10}|$ denote the number of elements in $S_5$ and $S_{10}$ respectively. This formula accounts for the optional existence of $H_d$ and $H_u$ (each having $|S_5| + 1$ possibilities including the absence of the particle), and the power sets of $S_5$ and $S_{10}$ for the matter charges in the $\bar{5}$ and $10$ representations.

For any two finite sets of charges $S_{\bar{5}}$ and $S_{10}$ in the charge space $\mathcal{Z}$, the cardinality of the finite set of $SU(5)$ charge spectra whose components are restricted to these sets is given by: \[ |\{ x \in \text{ChargeSpectrum } \mathcal{Z} \mid x.q_{H_d} \in S_{\bar{5}} \cup \{\text{none}\}, x.q_{H_u} \in S_{\bar{5}} \cup \{\text{none}\}, x.Q_{\bar{5}} \subseteq S_{\bar{5}}, x.Q_{10} \subseteq S_{10} \}| = (|S_{\bar{5}}| + 1)^2 \cdot 2^{|S_{\bar{5}}|} \cdot 2^{|S_{10}|} \]