PhysLean Documentation

PhysLean.StringTheory.FTheory.SU5U1.Quanta.IsViable.Elems

Quanta elements which are viable #

For the CodimensionOneConfig, I, we give FourTrees corresponding to Quanta which are viable. This is done in viableElems.

These trees are complete in the sense that they contain all the viable Quanta, which we prove.

That is to say, there is only finite number of viable quantum numbers one can associate to representations in a SU(5) × U(1) F-theory, and these trees contain all of them.

This is one of the results of, arXiv:1507.05961, except there the result is a calculation, whilst here it is a formal proof.

source
def FTheory.SU5U1.Quanta.viableElemsExe (I : CodimensionOneConfig) :
PhysLean.FourTree (Option ℤ) (Option ℤ) FiveQuanta TenQuanta

The FourTree of elements of Quanta for which the IsViable condition holds for a given I : CodimensionOneConfig. This is an excutable version used to generate viableElems, but not useful in proofs.

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

    The FourTree of elements of Quanta for which the IsViable condition holds for a given I : CodimensionOneConfig.

    Note, these results where calculated using e.g. set_option pp.deepTerms true #eval (viableElemsExe .nextToNearestNeighbor)

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem FTheory.SU5U1.Quanta.isViable_of_mem_viableElems (I : CodimensionOneConfig) (x : Quanta) (hx : x ∈ viableElems I) :
      IsViable I x

      Every element in viableElems IsViable.

      source
      theorem FTheory.SU5U1.Quanta.viableElems_nodups (I : CodimensionOneConfig) :
      (viableElems I).toMultiset.Nodup
      source
      theorem FTheory.SU5U1.Quanta.viableElems_same_card :
      (viableElems CodimensionOneConfig.same).card = 70
      source
      theorem FTheory.SU5U1.Quanta.viableElems_nearestNeighbor_card :
      (viableElems CodimensionOneConfig.nearestNeighbor).card = 16
      source
      theorem FTheory.SU5U1.Quanta.viableElems_nextToNearestNeighbor_card :
      (viableElems CodimensionOneConfig.nextToNearestNeighbor).card = 3