PhysLean Documentation

PhysLean.StringTheory.FTheory.SU5U1.Charges.PhenoConstrained.Elems.Same

Elements of the non pheno-constrained charges for same #

For the CodimensionOneConfig, same, 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 same.allowedBarFiveCharges same.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.

Note on large definition #

A discussion about the possible consequences of large definitions like the one in this file can be found at:

https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Potential.20consequences.20of.20large.20definitions.3F/with/522326293

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

For I = same 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.
Instances For