Physlib.StringTheory.FTheory.SU5.Fluxes.Basic

Equality between two fluxes $f_1$ and $f_2$ is decidable. Given that each flux is uniquely determined by a chirality flux $M \in \mathbb{Z}$ and a hypercharge flux $N \in \mathbb{Z}$, the condition $f_1 = f_2$ is equivalent to the conjunction $M_1 = M_2 \land N_1 = N_2$, which can be algorithmically evaluated.

This definition provides an instance of the `Repr` typeclass for the `Fluxes` structure, which defines how to display a flux as a string. For a flux $x$ characterized by a chirality flux $M$ and a hypercharge flux $N$, the string representation is formatted as $\langle M, N \rangle$.

Two fluxes $f_1$ and $f_2$, which are characterized by a chirality flux $M \in \mathbb{Z}$ and a hypercharge flux $N \in \mathbb{Z}$, are equal if and only if their respective chirality flux components are equal ($f_1.M = f_2.M$) and their respective hypercharge flux components are equal ($f_1.N = f_2.N$). This is expressed as $f_1 = f_2 \iff f_1.M = f_2.M \land f_1.N = f_2.N$.

The zero element for the `Fluxes` structure is defined as the pair $(0, 0)$, representing a state with zero chirality flux ($M = 0$) and zero hypercharge flux ($N = 0$).

For the zero flux $0$, the chirality flux component $M$ is equal to $0$.

For the zero flux $0$, the hypercharge flux component $N$ is equal to $0$.

For any two fluxes $f_1$ and $f_2$, each represented as a pair $(M, N)$ consisting of a chirality flux $M$ and a hypercharge flux $N$, their sum $f_1 + f_2$ is defined by the component-wise addition of these fluxes: $f_1 + f_2 = (M_1 + M_2, N_1 + N_2)$.

For any two fluxes $f_1$ and $f_2$, the chirality flux $M$ of their sum $f_1 + f_2$ is equal to the sum of the chirality fluxes of $f_1$ and $f_2$ individually. That is, $(f_1 + f_2).M = f_1.M + f_2.M$.

For any two fluxes $f_1$ and $f_2$, where each flux is characterized by a chirality flux $M$ and a hypercharge flux $N$, the hypercharge flux of their sum $f_1 + f_2$ is equal to the sum of the individual hypercharge fluxes of $f_1$ and $f_2$. That is, $(f_1 + f_2).N = f_1.N + f_2.N$.

The type `Fluxes`, consisting of pairs $(M, N) \in \mathbb{Z}^2$ where $M$ is the chirality flux and $N$ is the hypercharge flux, forms an additive commutative monoid. This algebraic structure is equipped with component-wise addition, the identity element $(0, 0)$, and scalar multiplication by natural numbers $n \in \mathbb{N}$ defined by $n \cdot (M, N) = (nM, nN)$.

The type `FluxesFive` represents a multiset of flux pairs $(M, N) \in \mathbb{Z} \times \mathbb{Z}$ associated with the $\mathbf{\bar{5}}$ (5-bar) representation matter curves in an $SU(5)$ F-theory model. Each element in the multiset corresponds to the fluxes of a specific matter curve, where $M$ is the chirality flux and $N$ is the hypercharge flux.

Equality between two multisets of flux pairs $F_1, F_2 \in \text{FluxesFive}$ is decidable. Given that each flux pair $(M, N) \in \mathbb{Z}^2$ has a decidable equality, there exists an algorithm to determine whether two such multisets contain the same elements with the same multiplicities.

Given a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z} \times \mathbb{Z}$ associated with the $\bar{\mathbf{5}}$ (5-bar) representation matter curves, this proposition states that the zero flux $(0, 0)$ is not an element of $F$. This condition implies that every matter curve in the multiset contributes non-trivially to the chiral matter spectrum.

Given a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z} \times \mathbb{Z}$ associated with $\bar{\mathbf{5}}$ matter curves, this definition returns the multiset of chiral indices for the representation $D = (\bar{3}, 1)_{1/3}$. Each index in the resulting multiset corresponds to the chirality flux $M$ of a matter curve in $F$.

Given a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z} \times \mathbb{Z}$ associated with $\bar{\mathbf{5}}$ matter curves, the total number of chiral representations of $D = (\bar{3}, 1)_{1/3}$ is defined as the sum of all non-negative values in the multiset of chiral indices $M$ corresponding to each matter curve in $F$.

For a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z} \times \mathbb{Z}$ associated with $\bar{\mathbf{5}}$ matter curves, the total number of anti-chiral $D = (\bar{3}, 1)_{1/3}$ representations is defined as the sum of all negative chiral indices $M$ in the multiset.

For a multiset of fluxes $F$ associated with $\mathbf{\bar{5}}$ matter curves, let $\chi(D) = M$ be the chiral index of the $D = (\bar{3}, 1)_{1/3}$ representation for each curve. If $N_{\text{chiral}}(D)$ is the sum of all non-negative chiral indices and $N_{\text{anti-chiral}}(D)$ is the sum of all negative chiral indices in $F$, then the total number of chiral $D$ representations is given by $$N_{\text{chiral}}(D) = \sum \chi(D) - N_{\text{anti-chiral}}(D)$$ where $\sum \chi(D)$ is the sum of the chiral indices across all curves in $F$.

Given a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z} \times \mathbb{Z}$ associated with the $\mathbf{\bar{5}}$ representation matter curves, this function computes the multiset of chiral indices for the Standard Model representation $L = (1,2)_{-1/2}$. For each matter curve in the collection, the chiral index is given by the sum $M + N$ of its chirality flux $M$ and hypercharge flux $N$.

Given a collection $F$ of flux pairs $(M, N) \in \mathbb{Z} \times \mathbb{Z}$ associated with the $\mathbf{\bar{5}}$ representation matter curves, the total number of chiral $L = (1,2)_{-1/2}$ representations is defined as the sum of all non-negative chiral indices $\chi(L) = M + N$ across the curves in the collection.

Given a collection $F$ of flux pairs $(M, N) \in \mathbb{Z} \times \mathbb{Z}$ associated with the $\mathbf{\bar{5}}$ (5-bar) representation matter curves, the total number of anti-chiral $L = (1,2)_{-1/2}$ representations is defined as the sum of all negative chiral indices $\chi(L) = M + N$ across the curves in the collection.

For a given collection $F$ of flux pairs $(M, N)$ associated with the $\mathbf{\bar{5}}$ matter curves, the total number of chiral $L = (1,2)_{-1/2}$ representations $n_{\text{chiral}}(L)$ is equal to the sum of the chiral indices $\chi(L) = M + N$ over all curves in $F$ minus the total number of anti-chiral $L$ representations $n_{\text{anti-chiral}}(L)$.

For a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z}^2$ associated with $\mathbf{\bar{5}}$ (5-bar) representation matter curves, the condition `NoExotics` is satisfied if the following conditions hold: 1. The total number of chiral $L = (1, 2)_{-1/2}$ representations is 3. 2. The total number of anti-chiral $L$ representations is 0. 3. The total number of chiral $D = (\bar{3}, 1)_{1/3}$ representations is 3. 4. The total number of anti-chiral $D$ representations is 0. These conditions ensure that the resulting spectrum contains exactly three generations of lepton doublets $L$ and down-type quarks $D$ with no corresponding anti-chiral states.

For a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z}^2$ associated with the $\bar{\mathbf{5}}$ (5-bar) representation matter curves, it is decidable whether $F$ satisfies the `NoExotics` condition. This condition holds if there are exactly 3 chiral generations of $L = (1, 2)_{-1/2}$ and $D = (\bar{3}, 1)_{1/3}$ representations, and no anti-chiral representations of either.

The type `FluxesTen` represents a multiset of flux pairs $(M, N) \in \mathbb{Z}^2$ associated with the 10-dimensional representation matter curves in an $SU(5)$ F-theory model. Each pair in the multiset corresponds to a specific matter curve, where $M$ is the chirality flux and $N$ is the hypercharge flux.

Equality between two multisets of $10$-dimensional representation fluxes is decidable. For any two elements $F_1, F_2 \in \text{FluxesTen}$, where each element is a multiset of flux pairs $(M, N) \in \mathbb{Z}^2$ associated with matter curves in $SU(5)$ F-theory, there exists an algorithmic procedure to determine whether $F_1 = F_2$.

Given a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z}^2$ associated with $10$-dimensional matter curves in $SU(5)$ F-theory, this proposition states that the zero flux $(0, 0)$ is not an element of $F$. This condition implies that every matter curve in the collection possesses non-zero flux and thus contributes to chiral matter.

For a multiset $F$ of flux pairs $(M, N)$ associated with $10$-dimensional matter curves in $SU(5)$ F-theory, the chiral index of the representation $Q = (3, 2)_{1/6}$ for each curve is given by the chirality flux $M$. This function returns the multiset of these chiral indices by mapping each flux pair $(M, N) \in F$ to its first component $M$.

Given a multiset $F$ of flux pairs $(M, N)$ associated with $10$-dimensional matter curves in $SU(5)$ F-theory, the chiral index of the representation $Q = (3, 2)_{1/6}$ for each curve is given by the chirality flux $M$. This function calculates the total number of chiral $Q$ representations by summing all non-negative chiral indices in the multiset: $$\sum_{M \in \text{chiralIndicesOfQ}(F), M \ge 0} M$$ where $\text{chiralIndicesOfQ}(F)$ is the multiset of $M$ values for each flux pair in $F$.

Given a multiset $F$ of flux pairs $(M, N)$ associated with 10-dimensional matter curves in $SU(5)$ F-theory, the chiral index of the representation $Q = (3, 2)_{1/6}$ for each curve is given by the chirality flux $M$. This function calculates the total contribution of anti-chiral $Q$ representations by summing all negative chiral indices in the multiset: $$\sum_{M \in \text{chiralIndicesOfQ}(F), M < 0} M$$ where $\text{chiralIndicesOfQ}(F)$ is the multiset of $M$ values for each flux pair in $F$.

For a multiset $F$ of flux pairs $(M, N)$ associated with 10-dimensional matter curves in $SU(5)$ F-theory, the total number of chiral $Q = (3, 2)_{1/6}$ representations is equal to the sum of all its chiral indices $\chi(Q) = M$ minus the total sum of its negative chiral indices: $$\text{numChiralQ}(F) = \sum_{M \in F} M - \text{numAntiChiralQ}(F)$$ where $\text{numChiralQ}(F) = \sum_{M \in F, M \ge 0} M$ is the sum of non-negative chiral indices and $\text{numAntiChiralQ}(F) = \sum_{M \in F, M < 0} M$ is the sum of negative chiral indices.

Given a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z}^2$ associated with 10-dimensional representation matter curves in an $SU(5)$ F-theory model, this function returns the multiset of chiral indices $\chi(U)$ for the Standard Model representation $U = (\bar{\mathbf{3}}, \mathbf{1})_{-2/3}$. For each matter curve with chirality flux $M$ and hypercharge flux $N$, the chiral index is calculated as $M - N$.

For a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z}^2$ associated with 10-dimensional representation matter curves, this function calculates the total number of chiral fermions in the $U = (\bar{\mathbf{3}}, \mathbf{1})_{-2/3}$ representation. It is defined as the sum of all non-negative chiral indices $\chi(U) = M - N$ across the curves in $F$.

For a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z}^2$ associated with 10-dimensional representation matter curves in an $SU(5)$ F-theory model, this function calculates the total number of anti-chiral fermions in the $U = (\bar{\mathbf{3}}, \mathbf{1})_{-2/3}$ representation. It is defined as the sum of all negative chiral indices $\chi(U) = M - N$ across the curves in the multiset $F$.

For a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z}^2$ associated with 10-dimensional representation matter curves in an $SU(5)$ F-theory model, let $\chi(U) = M - N$ be the chiral index for the Standard Model representation $U = (\bar{\mathbf{3}}, \mathbf{1})_{-2/3}$. The total number of chiral $U$ fermions $n_{\text{chiral}}(U)$ (defined as the sum of all non-negative chiral indices) and the total number of anti-chiral $U$ fermions $n_{\text{anti-chiral}}(U)$ (defined as the sum of all negative chiral indices) are related by: $$n_{\text{chiral}}(U) = \sum_{f \in F} \chi(U)_f - n_{\text{anti-chiral}}(U)$$

Given a multiset $F$ of fluxes $(M, N)$ associated with 10-dimensional matter curves in an $SU(5)$ F-theory model, this function returns a multiset of the chiral indices for the Standard Model representation $E = (1, 1)_1$. For each flux pair $(M, N)$ in the multiset $F$, the corresponding chiral index is calculated as $M + N$.

Given a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z}^2$ associated with 10-dimensional matter curves, let $\chi_E = M + N$ be the chiral index of the Standard Model representation $E = (1, 1)_1$ for each curve. This function calculates the total number of chiral $E$ representations by summing all non-negative chiral indices in the multiset: $$\sum_{\chi_E \ge 0} \chi_E$$

Given a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z}^2$ associated with 10-dimensional matter curves, let $\chi_E = M + N$ be the chiral index of the Standard Model representation $E = (1, 1)_1$ for each curve. This function calculates the sum of all negative chiral indices in the multiset: $$\sum_{\chi_E < 0} \chi_E$$ This value represents the total contribution of anti-chiral $E$ representations arising from these matter curves.

Let $F$ be a multiset of flux pairs $(M, N)$ associated with 10-dimensional matter curves in an $SU(5)$ F-theory model. For each curve, the chiral index of the Standard Model representation $E = (1, 1)_1$ is defined as $\chi_E = M + N$. The total number of chiral $E$ representations (the sum of all non-negative indices, $\sum_{\chi_E \ge 0} \chi_E$) is equal to the sum of all chiral indices in $F$ minus the total number of anti-chiral $E$ representations (the sum of all negative indices, $\sum_{\chi_E < 0} \chi_E$): $$\text{numChiralE}(F) = \sum \chi_E - \text{numAntiChiralE}(F)$$

For a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z}^2$ associated with 10-dimensional matter curves in an $SU(5)$ F-theory model, the condition that these representations do not lead to exotic chiral matter in the Minimal Supersymmetric Standard Model (MSSM) spectrum is satisfied if: - The total number of chiral $Q = (3, 2)_{1/6}$ representations is 3, and the total number of anti-chiral $Q$ representations is 0. - The total number of chiral $U = (\bar{\mathbf{3}}, \mathbf{1})_{-2/3}$ representations is 3, and the total number of anti-chiral $U$ representations is 0. - The total number of chiral $E = (1, 1)_1$ representations is 3, and the total number of anti-chiral $E$ representations is 0.

For a multiset $F$ of flux pairs $(M, N) \in \mathbb{Z}^2$ representing 10-dimensional matter curves in an $SU(5)$ F-theory model, the property `NoExotics` is decidable. This property signifies that the fluxes satisfy the conditions for the Minimal Supersymmetric Standard Model (MSSM) spectrum, specifically that the total number of chiral representations for $Q, U,$ and $E$ is exactly 3, while the total number of anti-chiral representations for these same fields is 0.