Elements of the non pheno-constrained charges for nearestNeighbor

For the CodimensionOneConfig, nearestNeighbor, we give trees of charges which are not pheno-constrained, and prove properties about them.

These trees are complete in the sense that they contain all the non pheno-constrained, complete, charges which are in ofFinset nearestNeighbor.allowedBarFiveCharges nearestNeighbor.allowedTenCharges. We use the FourTree type here for efficiency.

We break the properties of these trees into smaller modules, to aid in speed of building.

def FTheory.SU5U1.Charges.nonPhenoConstrainedChargesNearestNeighbor : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)

For I = nearestNeighbor the tree of charges containing all charges which are not phenomenlogically constrained, and which permit a top Yukawa coupling.

These trees can be found with e.g. #eval nonPhenoConstrainedChargesExt nextToNearestNeighbor.

Equations

• One or more equations did not get rendered due to their size.