PhysLean Documentation

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

Elements of the non pheno-constrained charges #

For each CodimensionOneConfig, I, we give trees of charges which are not pheno-constrained, by combining the trees of nonPhenoConstrainedChargesSame, nonPhenoConstrainedChargesNearestNeighbor, and nonPhenoConstrainedChargesNextToNearestNeighbor.

These trees are complete in the sense that they contain all the non pheno-constrained, complete, charges which are in ofFinset I.allowedBarFiveCharges I.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.

Comment on proofs #

Note a lot of proofs related to nonPhenoConstrainedCharges depend on decide. These proofs like all proofs are still constrained by maxHeartBeats, which prevents them from being too time consuming. See e.g. https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.E2.9C.94.20count_heartbeat.20and.20decide/near/521743784

source
def FTheory.SU5U1.Charges.nonPhenoConstrainedChargesExt (I : CodimensionOneConfig) :
PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)

For a given I : CodimensionOneConfig the tree of charges containing all charges which are not phenomenlogically constrained, and which permit a top Yukawa coupling. Unlike nonPhenoConstrainedCharges, these trees are calculated and therefore not good when using decide etc.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def FTheory.SU5U1.Charges.nonPhenoConstrainedCharges (I : CodimensionOneConfig) :
    PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)

    For a given I : CodimensionOneConfig 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
    Instances For