PhyslibSearch

Physlib.StringTheory.FTheory.SU5.Quanta.TenQuanta

47 declarations

definition

Multiset of fluxes of a `TenQuanta` xx

#toFluxesTen

For an object xx of type `TenQuanta` Z\mathcal{Z}, which represents a collection (multiset) of quanta where each quantum is a pair (c,f)(c, f) consisting of a U(1)U(1) charge cZc \in \mathcal{Z} and a flux ff, this function returns the multiset of all fluxes ff associated with these quanta. This is defined by mapping the projection onto the second component across the multiset xx, resulting in an object of type `FluxesTen`.

definition

Multiset of charges of a `TenQuanta` xx

#toCharges

For an object xx of type `TenQuanta` Z\mathcal{Z}, which represents a collection of 10-dimensional representations in an SU(5)×U(1)SU(5) \times U(1) model, the function returns the multiset of U(1)U(1) charges in Z\mathcal{Z} associated with those representations. This is defined by projecting each element in the collection xx (which consists of pairs of charges and fluxes) to its first component, the charge.

definition

Mapping charges to their total fluxes in a `TenQuanta` xx

#toChargeMap

For an object xx of type `TenQuanta` Z\mathcal{Z}, which represents a multiset of pairs (c,f)(c, f) consisting of a U(1)U(1) charge cZc \in \mathcal{Z} and a flux fFluxesf \in \text{Fluxes}, the function `toChargeMap` returns a map that associates each charge zZz \in \mathcal{Z} with the sum of all fluxes ff in xx whose corresponding charge cc is equal to zz. Mathematically, for a given zz, the value is (c,f)x,c=zf\sum_{(c, f) \in x, c = z} f.

theorem

The total flux of a charge zx.toChargesz \notin x.\text{toCharges} is zero

#toChargeMap_of_not_mem

For an object xx of type `TenQuanta` Z\mathcal{Z} and a U(1)U(1) charge zZz \in \mathcal{Z}, if zz is not contained in the multiset of charges of xx (denoted by x.toChargesx.\text{toCharges}), then the total flux associated with zz in xx (calculated by x.toChargeMap(z)x.\text{toChargeMap}(z)) is equal to the zero flux 00.

definition

Reduction of `TenQuanta` by summing fluxes per charge

#reduce

For a given `TenQuanta` xx consisting of a collection of pairs (q,ϕ)(q, \phi), where qZq \in \mathcal{Z} is a U(1)U(1) charge and ϕ\phi is a flux, the function `reduce` returns a new `TenQuanta` where each distinct charge qq present in xx is associated with the sum of all fluxes ϕ\phi that were paired with qq in the original collection. Formally, for each unique charge qq in xx, the reduced collection contains a single pair (q,Φq)(q, \Phi_q) with Φq=(qi,ϕi)x,qi=qϕi\Phi_q = \sum_{(q_i, \phi_i) \in x, q_i=q} \phi_i.

theorem

The Reduction of a `TenQuanta` Has No Duplicate Elements

#reduce_nodup

For any `TenQuanta` xx, the reduced collection x.reducex.\text{reduce} (obtained by summing the fluxes for each distinct charge) contains no duplicate elements.

theorem

x.reduce.dedup=x.reducex.\text{reduce}.\text{dedup} = x.\text{reduce}

#reduce_dedup

For any collection of 10-dimensional representation quanta xx (a `TenQuanta`), the reduction x.reducex.\text{reduce} is obtained by summing all fluxes associated with each unique charge. This theorem states that the deduplication of this reduced collection is equal to the reduced collection itself: x.reduce.dedup=x.reducex.\text{reduce}.\text{dedup} = x.\text{reduce}

theorem

x.reduce.toCharges=x.toCharges.dedupx.\text{reduce}.\text{toCharges} = x.\text{toCharges}.\text{dedup}

#reduce_toCharges

For a `TenQuanta` xx over a set of U(1)U(1) charges Z\mathcal{Z} (a collection of charge-flux pairs), let x.toChargesx.\text{toCharges} be the multiset of its charges and x.reducex.\text{reduce} be the reduced collection where fluxes for each unique charge are summed together. The multiset of charges of the reduced collection is equal to the multiset of charges of the original collection with all duplicates removed, i.e., x.reduce.toCharges=x.toCharges.dedupx.\text{reduce}.\text{toCharges} = x.\text{toCharges}.\text{dedup}.

theorem

Membership in x.reducex.\text{reduce} iff qx.toChargesq \in x.\text{toCharges} and Φ=ϕ\Phi = \sum \phi

#mem_reduce_iff

Let xx be a collection of 10-dimensional representation quanta (a `TenQuanta`), and let p=(q,Φ)p = (q, \Phi) be a pair consisting of a U(1)U(1) charge qZq \in \mathcal{Z} and a flux Φ\Phi. Then pp is an element of the reduced collection xreducex_{\text{reduce}} if and only if qq is a charge present in the original collection xx, and the flux Φ\Phi is equal to the sum of all fluxes ϕi\phi_i associated with the charge qq in xx. Mathematically, this is expressed as: (q,Φ)xreduce    qcharges(x)Φ=(qi,ϕi)x,qi=qϕi (q, \Phi) \in x_{\text{reduce}} \iff q \in \text{charges}(x) \land \Phi = \sum_{(q_i, \phi_i) \in x, q_i=q} \phi_i

theorem

Filtering x.reducex.\text{reduce} by charge qq yields the sum of all fluxes associated with qq in xx

#reduce_filter

For a `TenQuanta` xx (a collection of charge-flux pairs) and a U(1)U(1) charge qq present in the multiset of charges of xx, the result of filtering the reduced version of xx (where fluxes are summed for each distinct charge) for the charge qq is a singleton set containing the pair (q,Φq)(q, \Phi_q), where Φq\Phi_q is the sum of all fluxes associated with the charge qq in the original collection xx.

theorem

The `reduce` Operation on `TenQuanta` is Idempotent (x.reduce.reduce=x.reducex.\text{reduce}.\text{reduce} = x.\text{reduce})

#reduce_reduce

For a given collection of 10-dimensional representation quanta xx (a `TenQuanta`), the reduction operation—which sums all fluxes associated with the same U(1)U(1) charge—is idempotent. That is, reducing an already reduced collection results in the same collection: x.reduce.reduce=x.reducex.\text{reduce}.\text{reduce} = x.\text{reduce}.

theorem

Sum of charge-indexed flux homomorphisms is invariant under `TenQuanta.reduce`

#reduce_sum_eq_sum_toCharges

Let xx be a collection of 10-dimensional representation quanta of type `TenQuanta` Z\mathcal{Z}, which consists of pairs (q,ϕ)(q, \phi) where qZq \in \mathcal{Z} is a U(1)U(1) charge and ϕ\phi is a flux. Let MM be an additive commutative monoid, and let ff be a function that assigns to each charge qq an additive monoid homomorphism fq:FluxesMf_q: \text{Fluxes} \to M. Then, the sum of fq(ϕ)f_q(\phi) over all pairs in the original collection xx is equal to the sum of fq(Φ)f_q(\Phi) over all pairs (q,Φ)(q, \Phi) in the reduced collection reduce(x)\text{reduce}(x), where each Φ\Phi represents the accumulated flux for a unique charge qq. Mathematically, this is expressed as: (q,Φ)reduce(x)fq(Φ)=(q,ϕ)xfq(ϕ)\sum_{(q, \Phi) \in \text{reduce}(x)} f_q(\Phi) = \sum_{(q, \phi) \in x} f_q(\phi)

theorem

x.reduce=xx.\text{reduce} = x if the charges of xx have no duplicates

#reduce_eq_self_of_ofCharges_nodup

Let xx be a collection of 10-dimensional representations (quanta) in an SU(5)×U(1)SU(5) \times U(1) model, represented as a set of pairs (q,ϕ)(q, \phi) where qZq \in \mathcal{Z} is a U(1)U(1) charge and ϕ\phi is a flux. If the multiset of charges x.toChargesx.\text{toCharges} contains no duplicate elements (i.e., each charge qq appears at most once in the collection), then the reduction of xx, denoted x.reducex.\text{reduce}—which sums the fluxes for each distinct charge—is equal to the original collection xx.

theorem

x.reduce.toChargeMap=x.toChargeMapx.\text{reduce}.\text{toChargeMap} = x.\text{toChargeMap}

#reduce_toChargeMap_eq

Let xx be an object of type `TenQuanta` Z\mathcal{Z}, representing a collection of pairs (q,ϕ)(q, \phi) where qZq \in \mathcal{Z} is a U(1)U(1) charge and ϕ\phi is a flux. The function `toChargeMap` associates each charge zZz \in \mathcal{Z} with the sum of all fluxes associated with that charge in the collection. The theorem states that the charge map of the reduced collection x.reducex.\text{reduce} (where all fluxes belonging to the same charge are pre-summed) is equal to the charge map of the original collection xx. Mathematically, for any xx, it holds that: x.reduce.toChargeMap=x.toChargeMapx.\text{reduce}.\text{toChargeMap} = x.\text{toChargeMap}

theorem

Fluxes in F.reduceF.\text{reduce} are sums of sub-multisets of F.toFluxesTenF.\text{toFluxesTen}

#mem_powerset_sum_of_mem_reduce_toFluxesTen

Let FF be a collection of 10-dimensional representation quanta (a `TenQuanta`), and let FreduceF_{\text{reduce}} be its reduction obtained by summing the fluxes for each distinct U(1)U(1) charge. If a flux ff is an element of the multiset of fluxes associated with FreduceF_{\text{reduce}}, then ff is equal to the sum of some sub-multiset of the fluxes in the original collection FF.

theorem

Each flux in FreduceF_{\text{reduce}} is the sum of a non-empty sub-multiset of fluxes in FF

#mem_powerset_sum_of_mem_reduce_toFluxesTen_filter

Let FF be a collection of 10-dimensional representation quanta (a `TenQuanta`) and let Φ(F)\Phi(F) be the multiset of its associated fluxes. For any flux ff that is an element of the multiset of fluxes of the reduced collection FreduceF_{\text{reduce}}, it holds that ff is equal to the sum of the elements of some non-empty sub-multiset of Φ(F)\Phi(F).

theorem

The Number of Chiral UU Representations in Reduced `TenQuanta` from `elemsNoExotics` is 3

#reduce_numChiralU_of_mem_elemsNoExotics

Let FF be a collection of 10-dimensional representation quanta (`TenQuanta`) and let Φ(F)\Phi(F) be its multiset of flux pairs (M,N)Z2(M, N) \in \mathbb{Z}^2. If Φ(F)\Phi(F) is one of the six configurations in `elemsNoExotics` (which are the flux configurations satisfying the "no chiral exotics" and "no zero flux" conditions), then the total number of chiral U=(3ˉ,1)2/3U = (\bar{\mathbf{3}}, \mathbf{1})_{-2/3} representations in the reduced collection FreduceF_{\text{reduce}} is 3. The total number of chiral UU representations is calculated as the sum of all non-negative chiral indices χ(U)=MN\chi(U) = M - N associated with the fluxes in the multiset.

theorem

The number of anti-chiral UU representations in a reduced no-exotic `TenQuanta` is 0

#reduce_numAntiChiralU_of_mem_elemsNoExotics

Let FF be a collection of 10-dimensional representation quanta (a `TenQuanta`). If the multiset of fluxes Φ(F)\Phi(F) associated with FF is one of the six configurations in `FluxesTen.elemsNoExotics` (the configurations that satisfy the "no chiral exotics" and "no zero flux" conditions), then the total number of anti-chiral fermions in the U=(3ˉ,1)2/3U = (\bar{\mathbf{3}}, \mathbf{1})_{-2/3} representation for the reduced collection FreduceF_{\text{reduce}} is zero. Here, FreduceF_{\text{reduce}} is obtained by summing the fluxes of all quanta in FF that share the same U(1)U(1) charge.

theorem

The reduction of a no-exotic `TenQuanta` has 3 chiral QQ representations

#reduce_numChiralQ_of_mem_elemsNoExotics

Let FF be a collection of 10-dimensional representation quanta (a `TenQuanta`), and let FreduceF_{\text{reduce}} be its reduction obtained by summing the fluxes for each distinct U(1)U(1) charge. If the multiset of fluxes associated with FF is one of the six configurations in `elemsNoExotics` (which satisfy the "no chiral exotics" and "no zero flux" conditions), then the total number of chiral Q=(3,2)1/6Q = (3, 2)_{1/6} representations in the reduction FreduceF_{\text{reduce}} is exactly 3.

theorem

The Reduction of 10d Quanta with No Exotics has Zero Anti-Chiral QQ Contribution

#reduce_numAntiChiralQ_of_mem_elemsNoExotics

Let FF be a collection of 10-dimensional representation quanta (a `TenQuanta`) over a charge lattice Z\mathcal{Z}. If the multiset of fluxes associated with FF, denoted as F.toFluxesTenF.\text{toFluxesTen}, belongs to the set of six flux configurations elemsNoExotics\text{elemsNoExotics} that satisfy the "no chiral exotics" and "no zero flux" conditions, then the total sum of negative chiral indices for the representation Q=(3,2)1/6Q = (3, 2)_{1/6} in the reduced collection F.reduceF.\text{reduce} is zero. That is, \[ \sum_{M \in \text{chiralIndicesOfQ}(F.\text{reduce}.\text{toFluxesTen}), M < 0} M = 0 \] where F.reduceF.\text{reduce} is obtained by summing all fluxes corresponding to the same U(1)U(1) charge.

theorem

Reduced `TenQuanta` with No-Exotic Fluxes has 3 Chiral EE Representations

#reduce_numChiralE_of_mem_elemsNoExotics

Let FF be a collection of 10-dimensional representation quanta (a `TenQuanta`), consisting of pairs of U(1)U(1) charges and flux pairs (M,N)Z2(M, N) \in \mathbb{Z}^2. Suppose that the multiset of fluxes associated with FF is one of the six configurations in `elemsNoExotics` that satisfy the "no chiral exotics" condition. Then, for the reduced collection of quanta FreduceF_{\text{reduce}} (obtained by summing all fluxes corresponding to the same charge), the total number of chiral E=(1,1)1E = (1, 1)_1 representations is 3. Here, the number of chiral EE representations is defined as the sum of non-negative chiral indices χE=M+N\chi_E = M + N over the fluxes in the multiset.

theorem

The Total Anti-Chiral EE Index of a Reduced No-Exotic 10d Quanta is Zero

#reduce_numAntiChiralE_of_mem_elemsNoExotics

Let FF be a collection of 10-dimensional representation quanta (a `TenQuanta`). Suppose that the underlying multiset of fluxes associated with FF belongs to the set elemsNoExotics\text{elemsNoExotics}, which consists of the six flux configurations that satisfy the "no chiral exotics" and "no zero flux" conditions. Then, for the reduced collection FreduceF_{\text{reduce}} (obtained by summing fluxes for identical U(1)U(1) charges), the sum of all negative chiral indices χE=M+N\chi_E = M + N for the Standard Model representation E=(1,1)1E = (1, 1)_1 is zero.

theorem

Reduction of 10d Quanta from `elemsNoExotics` satisfies `NoExotics`

#reduce_noExotics_of_mem_elemsNoExotics

Let FF be a collection of 10-dimensional representation quanta (a `TenQuanta`) over a charge lattice Z\mathcal{Z}. Suppose that the multiset of fluxes associated with FF, denoted F.toFluxesTenF.\text{toFluxesTen}, is one of the six configurations in the set elemsNoExotics\text{elemsNoExotics} (the configurations of flux pairs (M,N)Z2(M, N) \in \mathbb{Z}^2 that satisfy the "no chiral exotics" and "no zero flux" conditions). Then, the reduced collection FreduceF_{\text{reduce}}, obtained by summing all fluxes corresponding to the same U(1)U(1) charge, also satisfies the `NoExotics` condition. Specifically, the total number of chiral generations is 3 and the number of anti-chiral generations is 0 for the Standard Model representations Q=(3,2)1/6Q = (3, 2)_{1/6}, U=(3ˉ,1)2/3U = (\bar{\mathbf{3}}, \mathbf{1})_{-2/3}, and E=(1,1)1E = (1, 1)_1.

theorem

Reduction of 10d Quanta Preserves Membership in `elemsNoExotics`

#reduce_mem_elemsNoExotics

Let FF be a collection of 10-dimensional representation quanta (a `TenQuanta`) over a charge lattice Z\mathcal{Z}, and let Φ(F)\Phi(F) be the multiset of its associated fluxes. Suppose that Φ(F)\Phi(F) belongs to the set elemsNoExotics\text{elemsNoExotics}, which consists of the six flux configurations (e.g., {(1,0),(1,0),(1,0)}\{(1, 0), (1, 0), (1, 0)\}, {(3,0)}\{(3, 0)\}, etc.) that satisfy the "no chiral exotics" and "no zero flux" conditions. Then, the multiset of fluxes of the reduced collection FreduceF_{\text{reduce}}, obtained by summing all fluxes corresponding to the same U(1)U(1) charge, is also an element of elemsNoExotics\text{elemsNoExotics}.

definition

Decomposition of a flux ff into basic components 1,0\langle 1, 0 \rangle and 1,±1\langle 1, \pm 1 \rangle

#decomposeFluxes

For a given flux f=M,Nf = \langle M, N \rangle (representing chirality and hypercharge fluxes), this function returns a multiset of fluxes by decomposing ff into specific basic components. The mapping is defined as follows: - 1,0{1,0}\langle 1, 0 \rangle \mapsto \{ \langle 1, 0 \rangle \} - 1,1{1,1}\langle 1, 1 \rangle \mapsto \{ \langle 1, 1 \rangle \} - 1,1{1,1}\langle 1, -1 \rangle \mapsto \{ \langle 1, -1 \rangle \} - 2,1{1,1,1,0}\langle 2, 1 \rangle \mapsto \{ \langle 1, 1 \rangle, \langle 1, 0 \rangle \} - 2,1{1,1,1,0}\langle 2, -1 \rangle \mapsto \{ \langle 1, -1 \rangle, \langle 1, 0 \rangle \} - 3,0{1,0,1,0,1,0}\langle 3, 0 \rangle \mapsto \{ \langle 1, 0 \rangle, \langle 1, 0 \rangle, \langle 1, 0 \rangle \} - 2,0{1,0,1,0}\langle 2, 0 \rangle \mapsto \{ \langle 1, 0 \rangle, \langle 1, 0 \rangle \} For any other flux ff, the function returns the singleton multiset {f}\{ f \}.

theorem

Sum of Flux Decomposition Equals ff for No-Exotic Configurations

#decomposeFluxes_sum_of_noExotics

For any flux pair f=(M,N)Z2f = (M, N) \in \mathbb{Z}^2 (representing chirality and hypercharge fluxes), if ff belongs to one of the configurations of 10-dimensional matter curve fluxes that satisfy the "no chiral exotics" and "no zero flux" conditions (i.e., fFf \in F for some FelemsNoExoticsF \in \text{elemsNoExotics}), then the sum of the basic flux components in the decomposition of ff is equal to ff. Specifically, the sum of the multiset produced by decomposeFluxes(f)\text{decomposeFluxes}(f) yields the original flux ff.

definition

Decomposition of a `TenQuanta` into basic fluxes

#decompose

Given a `TenQuanta` xx over a charge space Z\mathcal{Z}, which is a collection of pairs (q,f)(q, f) consisting of a charge qZq \in \mathcal{Z} and a flux ff, the decomposition function returns a new `TenQuanta`. This is achieved by taking each element (q,f)x(q, f) \in x and replacing it with a multiset of pairs (q,fi)(q, f_i), where {fi}\{f_i\} are the basic fluxes obtained by decomposing ff using the `decomposeFluxes` function. The resulting `TenQuanta` consists of fluxes that are only of the basic forms 1,0\langle 1, 0 \rangle or 1,±1\langle 1, \pm 1 \rangle, while maintaining the same total charge mapping when reduced.

theorem

Decomposition of `TenQuanta` distributes over addition

#decompose_add

For any two collections of 10-dimensional representation quanta xx and yy over a charge space Z\mathcal{Z}, the decomposition of their multiset sum x+yx + y into basic flux components is equal to the multiset sum of their individual decompositions. That is, (x+y).decompose=x.decompose+y.decompose(x + y).\text{decompose} = x.\text{decompose} + y.\text{decompose}.

theorem

Decomposition of `TenQuanta` Commutes with Filtering by Charge

#decompose_filter_charge

For a `TenQuanta` xx over a charge space Z\mathcal{Z} (a collection of charge-flux pairs (q,f)(q', f)) and a specific charge qZq \in \mathcal{Z}, the result of decomposing the fluxes in xx and then filtering the collection to keep only those pairs with charge qq is equal to filtering xx for charge qq first and then decomposing its fluxes. That is, (x.decompose).filter(pp.1=q)=(x.filter(pp.1=q)).decompose (x.\text{decompose}).\text{filter}(p \mapsto p.1 = q) = (x.\text{filter}(p \mapsto p.1 = q)).\text{decompose} where the `decompose` function replaces each pair (q,f)(q', f) with a multiset of pairs (q,fi)(q', f_i) using the basic flux components {fi}\{f_i\} of ff. This theorem assumes that equality of charges in Z\mathcal{Z} is decidable.

theorem

Decomposition of `TenQuanta` Preserves the Charge Map for No-Exotic Configurations

#decompose_toChargeMap

For a `TenQuanta` xx over a charge space Z\mathcal{Z} (a multiset of charge-flux pairs (q,f)(q, f)), suppose that the multiset of its fluxes x.toFluxesTenx.\text{toFluxesTen} belongs to `FluxesTen.elemsNoExotics` (the set of six flux configurations that satisfy the "no chiral exotics" and "no zero flux" conditions). Then the charge map of the decomposition of xx is equal to the charge map of xx itself. That is, for any charge zZz \in \mathcal{Z}: (x.decompose).toChargeMap(z)=x.toChargeMap(z) (x.\text{decompose}).\text{toChargeMap}(z) = x.\text{toChargeMap}(z) where the `toChargeMap` for a charge zz is the sum of all fluxes associated with zz in the collection, and the `decompose` operation replaces each flux in xx with its basic components while preserving its associated charge. This theorem assumes that equality of charges in Z\mathcal{Z} is decidable.

theorem

Decomposition of `TenQuanta` preserves the set of distinct charges

#decompose_toCharges_dedup

For a `TenQuanta` xx over a charge space Z\mathcal{Z} (a collection of charge-flux pairs (q,f)(q, f)), suppose the multiset of its fluxes x.toFluxesTenx.\text{toFluxesTen} is one of the six configurations in `FluxesTen.elemsNoExotics` (the configurations that satisfy the "no chiral exotics" and "no zero flux" conditions). Then, the set of distinct charges in the decomposition of xx is equal to the set of distinct charges in xx itself. That is, (x.decompose).toCharges.dedup=x.toCharges.dedup (x.\text{decompose}).\text{toCharges}.\text{dedup} = x.\text{toCharges}.\text{dedup} where `decompose` replaces each flux with its basic components while keeping the associated charge, and `dedup` denotes the set of unique elements in the multiset of charges.

theorem

Decomposition of `TenQuanta` preserves the reduction: (x.decompose).reduce=x.reduce(x.\text{decompose}).\text{reduce} = x.\text{reduce}

#decompose_reduce

Let xx be a `TenQuanta` over a charge space Z\mathcal{Z}, which is a collection of pairs (q,f)(q, f) consisting of a U(1)U(1) charge qZq \in \mathcal{Z} and a flux ff. Suppose that the multiset of its fluxes, x.toFluxesTenx.\text{toFluxesTen}, is an element of `FluxesTen.elemsNoExotics` (the set of six flux configurations for 10-dimensional matter curves that satisfy the "no chiral exotics" and "no zero flux" conditions). Then, the reduction of the decomposition of xx is equal to the reduction of xx itself: (x.decompose).reduce=x.reduce (x.\text{decompose}).\text{reduce} = x.\text{reduce} where the `reduce` operation sums all fluxes associated with each unique charge into a single pair, and the `decompose` operation replaces each flux in xx with its basic components while preserving its associated charge. This theorem assumes that equality of charges in Z\mathcal{Z} is decidable.

theorem

Decomposed No-Exotic 10d Fluxes are {1,0,1,0,1,0}\{\langle 1, 0 \rangle, \langle 1, 0 \rangle, \langle 1, 0 \rangle\} or {1,1,1,1,1,0}\{\langle 1, 1 \rangle, \langle 1, -1 \rangle, \langle 1, 0 \rangle\}

#decompose_toFluxesTen

Let xx be a `TenQuanta` over a charge space Z\mathcal{Z}, representing a collection of pairs (c,f)(c, f) where cZc \in \mathcal{Z} is a U(1)U(1) charge and f=M,Nf = \langle M, N \rangle is a flux. Let x.toFluxesTenx.\text{toFluxesTen} denote the multiset of fluxes associated with xx. If x.toFluxesTenx.\text{toFluxesTen} is an element of `FluxesTen.elemsNoExotics` (the set of flux configurations for 10-dimensional matter curves that satisfy the "no chiral exotics" and "no zero flux" conditions), then the multiset of fluxes of the decomposed representation, x.decompose.toFluxesTenx.\text{decompose}.\text{toFluxesTen}, is equal to either {1,0,1,0,1,0}\{\langle 1, 0 \rangle, \langle 1, 0 \rangle, \langle 1, 0 \rangle\} or {1,1,1,1,1,0}\{\langle 1, 1 \rangle, \langle 1, -1 \rangle, \langle 1, 0 \rangle\}.

definition

Lifting a set of charges cc to `TenQuanta`

#liftCharge

Given a finite set of U(1)U(1) charges cZc \subset \mathcal{Z}, the function `liftCharge(c)` constructs a multiset of `TenQuanta` that correspond to valid 10-dimensional representations without exotic fluxes, duplicate charges, or zero fluxes. The construction considers two possible configurations for the underlying fluxes ϕ\phi: 1. A configuration where three charges from cc (forming a multiset of size 3) are each paired with the flux 1,0\langle 1, 0 \rangle. 2. A configuration where three charges x,y,zcx, y, z \in c are paired with the fluxes 1,1\langle 1, 1 \rangle, 1,1\langle 1, -1 \rangle, and 1,0\langle 1, 0 \rangle respectively. In both cases, the resulting collections are filtered to ensure that the multiset of charges covers all elements in the input set cc. Finally, the `reduce` operation is applied to each collection, which sums the fluxes associated with the same charge, effectively merging duplicate charges into a single representation with a combined flux.

theorem

The set of charges of xliftCharge(c)x \in \text{liftCharge}(c) equals cc

#toCharge_toFinset_of_mem_liftCharge

Let Z\mathcal{Z} be the type of U(1)U(1) charges and cZc \subset \mathcal{Z} be a finite set. For any collection of 10-dimensional representations xx that is an element of the multiset liftCharge(c)\text{liftCharge}(c), the set of unique charges associated with xx is exactly cc.

theorem

xliftCharge(c)    Nodup(x.toCharges)x \in \text{liftCharge}(c) \implies \text{Nodup}(x.\text{toCharges})

#toCharges_nodup_of_mem_liftCharge

For any finite set of U(1)U(1) charges cZc \subset \mathcal{Z} and any `TenQuanta` xx such that xx is an element of the multiset liftCharge(c)\text{liftCharge}(c), the multiset of charges associated with xx, denoted x.toChargesx.\text{toCharges}, contains no duplicate elements.

theorem

xliftCharge(c)x \in \text{liftCharge}(c) implies existence of a precursor aa with specific charges and fluxes

#exists_toCharges_toFluxesTen_of_mem_liftCharge

Let Z\mathcal{Z} be the type of U(1)U(1) charges and cZc \subset \mathcal{Z} be a finite set of charges. For any collection of 10-dimensional representations xx that is an element of the multiset liftCharge(c)\text{liftCharge}(c), there exists a collection aa such that: 1. xx is the reduction of aa (i.e., a.reduce=xa.\text{reduce} = x), 2. the set of unique charges associated with aa is exactly cc, and 3. the multiset of fluxes associated with aa is either {1,0,1,0,1,0}\{\langle 1, 0 \rangle, \langle 1, 0 \rangle, \langle 1, 0 \rangle\} or {1,1,1,1,1,0}\{\langle 1, 1 \rangle, \langle 1, -1 \rangle, \langle 1, 0 \rangle\}.

theorem

Existence of a precursor aa with specific charges and fluxes implies xliftCharge(c)x \in \text{liftCharge}(c)

#mem_liftCharge_of_exists_toCharges_toFluxesTen

Let Z\mathcal{Z} be the type of U(1)U(1) charges and cZc \subset \mathcal{Z} be a finite set of charges. For any collection of 10-dimensional representations xx of type `TenQuanta`, if there exists a collection aa such that: 1. xx is the reduction of aa (i.e., a.reduce=xa.\text{reduce} = x), 2. the set of unique charges associated with aa is exactly cc (i.e., a.toCharges.toFinset=ca.\text{toCharges.toFinset} = c), and 3. the multiset of fluxes associated with aa is either {1,0,1,0,1,0}\{\langle 1, 0 \rangle, \langle 1, 0 \rangle, \langle 1, 0 \rangle\} or {1,1,1,1,1,0}\{\langle 1, 1 \rangle, \langle 1, -1 \rangle, \langle 1, 0 \rangle\}, then xx is an element of the multiset liftCharge(c)\text{liftCharge}(c).

theorem

xliftCharge(c)x \in \text{liftCharge}(c) iff existence of a precursor with specific charges and fluxes

#mem_liftCharge_iff_exists

Let Z\mathcal{Z} be the type of U(1)U(1) charges and cZc \subset \mathcal{Z} be a finite set of charges. For any collection of 10-dimensional representations xx of type `TenQuanta`, xx is an element of the multiset liftCharge(c)\text{liftCharge}(c) if and only if there exists a collection aa such that: 1. xx is the reduction of aa (i.e., a.reduce=xa.\text{reduce} = x), 2. the set of unique charges associated with aa is exactly cc (i.e., a.toCharges.toFinset=ca.\text{toCharges.toFinset} = c), and 3. the multiset of fluxes associated with aa is either {1,0,1,0,1,0}\{\langle 1, 0 \rangle, \langle 1, 0 \rangle, \langle 1, 0 \rangle\} or {1,1,1,1,1,0}\{\langle 1, 1 \rangle, \langle 1, -1 \rangle, \langle 1, 0 \rangle\}.

theorem

xliftCharge(c)x \in \text{liftCharge}(c) implies xx has no zero fluxes

#hasNoZero_of_mem_liftCharge

Let Z\mathcal{Z} be the type of U(1)U(1) charges and cZc \subset \mathcal{Z} be a finite set of charges. For any collection of 10-dimensional representations xx of type `TenQuanta`, if xx is an element of the multiset liftCharge(c)\text{liftCharge}(c), then the multiset of fluxes associated with xx does not contain the zero flux (0,0)(0, 0).

theorem

FliftCharge(c)    NoExotics(F)F \in \text{liftCharge}(c) \implies \text{NoExotics}(F)

#noExotics_of_mem_liftCharge

Let Z\mathcal{Z} be the type of U(1)U(1) charges and cZc \subset \mathcal{Z} be a finite set of charges. For any collection of 10-dimensional representation quanta FF (an object of type `TenQuanta`), if FF is an element of the multiset liftCharge(c)\text{liftCharge}(c), then the multiset of fluxes associated with FF, denoted F.toFluxesTenF.\text{toFluxesTen}, satisfies the `NoExotics` condition. The `NoExotics` condition implies that the configuration yields exactly 3 chiral generations and 0 anti-chiral generations for each of the Standard Model representations Q=(3,2)1/6Q = (3, 2)_{1/6}, U=(3ˉ,1)2/3U = (\bar{\mathbf{3}}, \mathbf{1})_{-2/3}, and E=(1,1)1E = (1, 1)_1.

theorem

xliftCharge(c)x \in \text{liftCharge}(c) if xx has no exotics, no zero fluxes, and distinct charges matching cc

#mem_liftCharge_of_mem_noExotics_hasNoZero

Let Z\mathcal{Z} be the type of U(1)U(1) charges and cZc \subset \mathcal{Z} be a finite set of charges. Let xx be a `TenQuanta` over Z\mathcal{Z}, representing a collection of 10-dimensional representations as pairs (q,ϕ)(q, \phi) of charges and fluxes. Suppose that: 1. The multiset of fluxes associated with xx, denoted x.toFluxesTenx.\text{toFluxesTen}, satisfies the "no chiral exotics" condition (NoExotics\text{NoExotics}). 2. The multiset of fluxes x.toFluxesTenx.\text{toFluxesTen} contains no zero flux (0,0)(0,0) (HasNoZero\text{HasNoZero}). 3. The set of unique charges associated with xx is exactly cc (x.toCharges.toFinset=cx.\text{toCharges}.\text{toFinset} = c). 4. The multiset of charges x.toChargesx.\text{toCharges} contains no duplicate elements (Nodup\text{Nodup}). Then, xx is an element of the multiset liftCharge(c)\text{liftCharge}(c), which constructs valid, reduced 10-dimensional representation configurations for the set of charges cc.

theorem

xliftCharge(c)x \in \text{liftCharge}(c) if and only if xx has valid fluxes and distinct charges matching cc

#mem_liftCharge_iff

Let Z\mathcal{Z} be the type of U(1)U(1) charges and cZc \subset \mathcal{Z} be a finite set. For any collection of 10-dimensional representation quanta xx (an object of type `TenQuanta`), xx belongs to the multiset liftCharge(c)\text{liftCharge}(c) if and only if the following three conditions are satisfied: 1. The multiset of fluxes associated with xx, denoted x.toFluxesTenx.\text{toFluxesTen}, is an element of FluxesTen.elemsNoExotics\text{FluxesTen.elemsNoExotics}. This set contains the six specific flux configurations that satisfy both the "no chiral exotics" (NoExotics\text{NoExotics}) and "no zero flux" (HasNoZero\text{HasNoZero}) conditions. 2. The set of unique U(1)U(1) charges present in xx is exactly cc (x.toCharges.toFinset=cx.\text{toCharges}.\text{toFinset} = c). 3. The multiset of charges associated with xx, x.toChargesx.\text{toCharges}, contains no duplicate elements (Nodup\text{Nodup}).

theorem

reduce(f(F))liftCharge(f(c))\text{reduce}(f(F)) \in \text{liftCharge}(f(c)) for FliftCharge(c)F \in \text{liftCharge}(c)

#map_liftCharge

Let Z\mathcal{Z} and Z1\mathcal{Z}_1 be commutative rings and f:ZZ1f: \mathcal{Z} \to \mathcal{Z}_1 be a ring homomorphism. Let cZc \subset \mathcal{Z} be a finite set of U(1)U(1) charges. If a collection of 10-dimensional representation quanta FF (an object of type `TenQuanta`) belongs to the set of valid configurations liftCharge(c)\text{liftCharge}(c), then the configuration obtained by mapping the charges of FF through ff and applying the `reduce` operation (which sums fluxes for any charges that become identical under ff) is an element of liftCharge(f(c))\text{liftCharge}(f(c)), where f(c)f(c) is the image of the set cc under ff.

definition

Anomaly coefficient (qiNi,3qi2Ni)(\sum q_i N_i, 3 \sum q_i^2 N_i) of a `TenQuanta`

#anomalyCoefficient

Given a `TenQuanta` FF over a commutative ring Z\mathcal{Z}, let each representation in the collection be associated with a U(1)U(1) charge qiq_i and a flux NiN_i. The anomaly coefficient is defined as the pair in Z×Z\mathcal{Z} \times \mathcal{Z}: \[ \left( \sum_i q_i N_i, 3 \sum_i q_i^2 N_i \right) \] The first component represents the mixed U(1)U(1)-MSSM gauge anomaly coefficient, and the second component represents the mixed U(1)YU(1)U(1)U(1)_Y-U(1)-U(1) gauge anomaly coefficient.

theorem

anomalyCoefficient(f(F))=(f,f)(anomalyCoefficient(F))\text{anomalyCoefficient}(f(F)) = (f, f) (\text{anomalyCoefficient}(F))

#anomalyCoefficient_of_map

Let Z\mathcal{Z} and Z1\mathcal{Z}_1 be commutative rings and f:ZZ1f: \mathcal{Z} \to \mathcal{Z}_1 be a ring homomorphism. Let FF be a `TenQuanta` object over Z\mathcal{Z}, representing a collection of 10d representations where each representation is associated with a U(1)U(1) charge qiq_i and a flux NiZN_i \in \mathcal{Z}. The anomaly coefficient of FF is defined as the pair (A1,A2)=(iqiNi,3iqi2Ni)(\mathcal{A}_1, \mathcal{A}_2) = (\sum_i q_i N_i, 3 \sum_i q_i^2 N_i). If we construct a new `TenQuanta` over Z1\mathcal{Z}_1 by mapping the charges and fluxes of FF through ff (i.e., qif(qi)q_i \mapsto f(q_i) and Nif(Ni)N_i \mapsto f(N_i)), then the anomaly coefficient of the mapped quanta is equal to (f(A1),f(A2))(f(\mathcal{A}_1), f(\mathcal{A}_2)).

theorem

anomalyCoefficient(F.reduce)=anomalyCoefficient(F)\text{anomalyCoefficient}(F.\text{reduce}) = \text{anomalyCoefficient}(F)

#anomalyCoefficient_of_reduce

For a collection FF of 10-dimensional representation quanta (`TenQuanta`) over a commutative ring Z\mathcal{Z} with decidable equality, let each quantum be associated with a U(1)U(1) charge qiq_i and a flux ϕi=(Mi,Ni)\phi_i = (M_i, N_i). The anomaly coefficient is defined as the pair (qiNi,3qi2Ni)\left( \sum q_i N_i, 3 \sum q_i^2 N_i \right). If F.reduceF.\text{reduce} is the collection obtained by summing the fluxes for each unique charge qq in FF, then the anomaly coefficient of the reduced collection is equal to the anomaly coefficient of the original collection: \[ \text{anomalyCoefficient}(F.\text{reduce}) = \text{anomalyCoefficient}(F) \]