Physlib.StringTheory.FTheory.SU5.Quanta.Basic

This definition provides an instance of the `Repr` typeclass for the `Quanta 𝓩` structure, which defines how to format an element as a string for display. For a given `Quanta` object $x$, its string representation is given by the tuple $\langle q_{H_d}, q_{H_u}, F, T \rangle$, where $q_{H_d}$ and $q_{H_u}$ are the $U(1)$ charges of the $H_d$ and $H_u$ particles, $F$ denotes the data for the 5-bar representations, and $T$ denotes the data for the 10-dimensional representations.

Let $\mathcal{Z}$ be a type. For any two `Quanta` objects $x, y$ over $\mathcal{Z}$, if their Higgs charges $q_{H_d}$ and $q_{H_u}$ are equal ($x.q_{H_d} = y.q_{H_d}$ and $x.q_{H_u} = y.q_{H_u}$), and their flux data $F$ and $T$ for the $\bar{\mathbf{5}}$ and $\mathbf{10}$ representations respectively are equal ($x.F = y.F$ and $x.T = y.T$), then the two objects are equal ($x = y$).

For any type $\mathcal{Z}$ with decidable equality, the equality between two objects $x, y \in \text{Quanta } \mathcal{Z}$ is decidable. This is established by checking the equality of their four constituent fields: the $U(1)$ charges $x.q_{H_d} = y.q_{H_d}$ and $x.q_{H_u} = y.q_{H_u}$, and the flux data $x.F = y.F$ and $x.T = y.T$.

This function maps a `Quanta` object $x$ (which contains quantum numbers for $SU(5) \times U(1)$ representations) to its corresponding `ChargeSpectrum`. It extracts the $U(1)$ charges $q_{H_d}$ and $q_{H_u}$ of the Higgs particles $H_d$ and $H_u$, and determines the finite sets of charges $Q_{\bar{\mathbf{5}}}$ and $Q_{\mathbf{10}}$ by extracting all unique charges present in the flux data $F$ and $T$ associated with the $\bar{\mathbf{5}}$ and $\mathbf{10}$ representations, respectively.

For any `Quanta` object $x$ representing the quantum numbers of $SU(5) \times U(1)$ representations, the $U(1)$ charge of the $H_d$ Higgs particle in the corresponding charge spectrum, denoted $(\text{toCharges } x).q_{H_d}$, is equal to the charge $x.q_{H_d}$ defined in the original object.

For any `Quanta` object $x$ representing the quantum numbers of $SU(5) \times U(1)$ representations, the $U(1)$ charge of the $H_u$ Higgs particle in the corresponding charge spectrum, denoted $(\text{toCharges } x).q_{H_u}$, is equal to the charge $x.q_{H_u}$ defined in the original object.

The reduction of a `Quanta` object $x$, denoted as $\text{reduce}(x)$, is a new `Quanta` object that preserves the $U(1)$ charges of the Higgs fields $q_{H_d}$ and $q_{H_u}$ from $x$. For the $\mathbf{\bar{5}}$ and $\mathbf{10}$ representations, the respective flux collections $F$ and $T$ are replaced by their reduced versions, in which all fluxes corresponding to the same $U(1)$ charge (or representation) are summed together.

Given a charge spectrum $c$ of an $SU(5) \times U(1)$ model, this function constructs a multiset of all possible `Quanta` objects that correspond to that spectrum. Each `Quanta` object in the resulting multiset preserves the $U(1)$ charges of the Higgs fields $q_{H_d}$ and $q_{H_u}$ from the spectrum $c$. The $\mathbf{\bar{5}}$ and $\mathbf{10}$ representation-specific quanta are obtained by lifting the respective charge components $c.Q_5$ and $c.Q_{10}$ using `FiveQuanta.liftCharge` and `TenQuanta.liftCharge`. The resulting multiset contains only those configurations that do not have chiral exotics and have no zero fluxes.

For a charge spectrum $c$ and a quanta object $x$ in an $SU(5) \times U(1)$ F-theory model, $x$ is an element of the multiset of lifted quanta $\text{liftCharge}(c)$ if and only if the following conditions are met: 1. The $U(1)$ charges of the Higgs fields $H_d$ and $H_u$ in $x$ match those in $c$ ($x.q_{H_d} = c.q_{H_d}$ and $x.q_{H_u} = c.q_{H_u}$). 2. The $\mathbf{\bar{5}}$ representation quanta $F$ of $x$ are in the lifted multiset of the charge component $c.Q_5$. 3. The $\mathbf{10}$ representation quanta $T$ of $x$ are in the lifted multiset of the charge component $c.Q_{10}$.

In an $SU(5) \times U(1)$ F-theory model, let $c$ be a charge spectrum and $x$ be a quanta object. If $x$ is an element of the multiset $\text{liftCharge}(c)$, which consists of all valid quantum configurations (fluxes and charges) compatible with the spectrum $c$ that have no chiral exotics or zero fluxes, then the charge spectrum derived from $x$ is equal to $c$ (i.e., $x.\text{toCharges} = c$).

For a commutative ring $\mathcal{Z}$, given an optional $U(1)$ charge $q_{H_d} \in \mathcal{Z}$ associated with the $H_d$ particle, the anomaly cancellation coefficients are defined as the pair $(q_{H_d}, q_{H_d}^2) \in \mathcal{Z} \times \mathcal{Z}$. If the charge is not provided (represented as `none`), the coefficients are $(0, 0)$.

Let $\mathcal{Z}$ and $\mathcal{Z}_1$ be commutative rings, and let $f: \mathcal{Z} \to \mathcal{Z}_1$ be a ring homomorphism. For any optional $U(1)$ charge $q_{H_d}$ associated with the $H_d$ particle, applying the anomaly coefficient function to the mapped charge $f(q_{H_d})$ (where $f$ maps `none` to `none`) is equivalent to applying $f$ component-wise to the resulting pair of anomaly coefficients. That is, $$\text{HdAnomalyCoefficient}(f(q_{H_d})) = (f(c_1), f(c_2))$$ where $(c_1, c_2) = \text{HdAnomalyCoefficient}(q_{H_d})$ is the pair of coefficients in $\mathcal{Z} \times \mathcal{Z}$.

For a commutative ring $\mathcal{Z}$, given an optional $U(1)$ charge $q_{H_u}$ associated with the $H_u$ particle, the function returns a pair of anomaly cancellation coefficients in $\mathcal{Z} \times \mathcal{Z}$ defined by: $$\begin{cases} (0, 0) & \text{if } q_{H_u} = \text{none} \\ (-q, -q^2) & \text{if } q_{H_u} = q \end{cases}$$ These values represent the contribution of the $H_u$ particle to the linear and quadratic $U(1)$ anomaly cancellation conditions in the $SU(5) \times U(1)$ model.

Let $\mathcal{Z}$ and $\mathcal{Z}_1$ be commutative rings and $f: \mathcal{Z} \to \mathcal{Z}_1$ be a ring homomorphism. For an optional $U(1)$ charge $q_{H_u}$ associated with the $H_u$ particle, the anomaly coefficient function commutes with the ring homomorphism $f$ in the following sense: $$\text{HuAnomalyCoefficient}(\text{map } f \, q_{H_u}) = (f(x), f(y))$$ where $(x, y) = \text{HuAnomalyCoefficient}(q_{H_u})$. Here, $\text{map } f$ denotes the application of $f$ to the charge if it exists (returning `none` otherwise), and the right-hand side represents the application of $f$ to each component of the anomaly coefficient pair in $\mathcal{Z} \times \mathcal{Z}$.

In the $SU(5) \times U(1)$ F-theory model, for a given set of quanta $Q$ over a commutative ring $\mathcal{Z}$, the linear anomaly cancellation condition is the proposition that the sum of the $U(1)$ charge contributions from the Higgs particles and the matter representations vanishes. Specifically, the condition is given by: $$q_{H_d} - q_{H_u} + \sum_{i} q_i N_i + \sum_{a} q_a N_a = 0$$ where $q_{H_d}$ and $q_{H_u}$ are the $U(1)$ charges of the $H_d$ and $H_u$ particles respectively, the first sum corresponds to the $\overline{\mathbf{5}}$ representations with charges $q_i$ and multiplicities (fluxes) $N_i$, and the second sum corresponds to the $\mathbf{10}$ representations with charges $q_a$ and multiplicities $N_a$.

In the $SU(5) \times U(1)$ F-theory model, for a given set of quanta $Q$ over a commutative ring $\mathcal{Z}$, the quartic anomaly cancellation condition is the proposition that the sum of the quadratic $U(1)$ charge contributions from the Higgs particles and the matter representations vanishes. Specifically, the condition is given by: $$q_{H_d}^2 - q_{H_u}^2 + \sum_{i} q_i^2 N_i + 3 \sum_{a} q_a^2 N_a = 0$$ where $q_{H_d}$ and $q_{H_u}$ are the $U(1)$ charges of the $H_d$ and $H_u$ particles, the first sum corresponds to the $\overline{\mathbf{5}}$ representations with charges $q_i$ and multiplicities (fluxes) $N_i$, and the second sum corresponds to the $\mathbf{10}$ representations with charges $q_a$ and multiplicities $N_a$.

In the $SU(5) \times U(1)$ F-theory model, for a given set of quanta $Q$ defined over a commutative ring $\mathcal{Z}$ with decidable equality, the linear anomaly cancellation condition is a decidable proposition. Specifically, it is decidable whether the sum of $U(1)$ charge contributions from the Higgs particles ($H_d, H_u$) and the matter representations ($\mathbf{\overline{5}}, \mathbf{10}$) vanishes: $$q_{H_d} - q_{H_u} + \sum_{i} q_i N_i + \sum_{a} q_a N_a = 0$$ where $q_{H_d}$ and $q_{H_u}$ are the $U(1)$ charges of the $H_d$ and $H_u$ particles, and the sums represent the contributions from the $\mathbf{\overline{5}}$ and $\mathbf{10}$ representations respectively.

For a set of quanta $Q$ defined over a commutative ring $\mathcal{Z}$ that has decidable equality, it is decidable whether $Q$ satisfies the quartic anomaly cancellation condition. This condition is expressed as: $$q_{H_d}^2 - q_{H_u}^2 + \sum_{i} q_i^2 N_i + 3 \sum_{a} q_a^2 N_a = 0$$ where $q_{H_d}$ and $q_{H_u}$ are the $U(1)$ charges of the Higgs particles $H_d$ and $H_u$, and the sums are taken over the $\overline{\mathbf{5}}$ and $\mathbf{10}$ representations with $U(1)$ charges $q$ and multiplicities (fluxes) $N$.