PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.Charges.PhenoClosed

Phenomenologically closed sets of charges #

In this module we define a number of propositions related to the phenomenological closure of sets of charges.

One of the key results within this module is the lemma completeness_of_isPhenoClosedQ5_isPhenoClosedQ10, which gives a quick way to check whether a set of charges contains precisely those charges which

IsPhenoClosedQ5 #

def SuperSymmetry.SU5.Charges.IsPhenoClosedQ5 {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] (S5 : Finset 𝓩) (charges : Multiset (Charges 𝓩)) :

The proposition that for multiset set of charges charges, adding individual elements of S5 to the Q5 charges of elements of charges again leads to an element in charges or a charge which is phenomenologically constrained, or regenerates dangerous couplings with one singlet insertion.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem SuperSymmetry.SU5.Charges.isPhenClosedQ5_of_isPhenoConstrainedQ5 {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] {S5 : Finset 𝓩} {charges : Multiset (Charges 𝓩)} (h : q5S5, xcharges, have y := (x.1, x.2.1, insert q5 x.2.2.1, x.2.2.2); x.IsPhenoConstrainedQ5 q5 y charges y.YukawaGeneratesDangerousAtLevel 1) :
    IsPhenoClosedQ5 S5 charges

    IsPhenoClosedQ10 #

    def SuperSymmetry.SU5.Charges.IsPhenoClosedQ10 {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] (S10 : Finset 𝓩) (charges : Multiset (Charges 𝓩)) :

    The proposition that for multiset set of charges charges, adding individual elements of S10 to the Q10 charges of elements of charges again leads to an element in charges or a charge which is phenomenologically constrained, or regenerates dangerous couplings with one singlet insertion.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem SuperSymmetry.SU5.Charges.isPhenClosedQ10_of_isPhenoConstrainedQ10 {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] {S10 : Finset 𝓩} {charges : Multiset (Charges 𝓩)} (h : q10S10, xcharges, have y := (x.1, x.2.1, x.2.2.1, insert q10 x.2.2.2); x.IsPhenoConstrainedQ10 q10 y charges y.YukawaGeneratesDangerousAtLevel 1) :
      IsPhenoClosedQ10 S10 charges

      The proposition that for multiset set of charges charges contains all viable completions of charges which allow the top Yukawa, given allowed values of 5d and 10d charges S5 and S10.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        theorem SuperSymmetry.SU5.Charges.containsPhenoCompletionsOfMinimallyAllows_of_subset {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] {S5 S10 : Finset 𝓩} {charges charges' : Multiset (Charges 𝓩)} (h' : ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges) (h : xcharges, x charges') :

        Completeness of isPhenoClosedQ5 and isPhenoClosedQ10 #

        The multiset of charges charges contains precisely those charges (given a finite set of allowed charges) which

        theorem SuperSymmetry.SU5.Charges.completeness_of_isPhenoClosedQ5_isPhenoClosedQ10 {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] {S5 S10 : Finset 𝓩} {charges : Multiset (Charges 𝓩)} (charges_topYukawa : xcharges, x.AllowsTerm PotentialTerm.topYukawa) (charges_not_isPhenoConstrained : xcharges, ¬x.IsPhenoConstrained) (charges_yukawa : xcharges, ¬x.YukawaGeneratesDangerousAtLevel 1) (charges_complete : xcharges, x.IsComplete) (charges_isPhenoClosedQ5 : IsPhenoClosedQ5 S5 charges) (charges_isPhenoClosedQ10 : IsPhenoClosedQ10 S10 charges) (charges_exist : ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges) {x : Charges 𝓩} (hsub : x ofFinset S5 S10) :

        Definitions of multisets which are phenomenologically closed #

        For a given S5 S10 : Finset 𝓩, the minimal multiset of charges which satifies the condition ContainsPhenoCompletionsOfMinimallyAllows. That is to say, every multiset of charges which satifies ContainsPhenoCompletionsOfMinimallyAllows has completeMinSubset as a subset.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          unsafe def SuperSymmetry.SU5.Charges.viableChargesMultiset {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] (S5 S10 : Finset 𝓩) :

          All charges, for a given S5 S10 : Finset 𝓩, which permit a top Yukawa coupling, are not phenomenologically constrained, and do not regenerate dangerous couplings with one insertion of a Yukawa coupling.

          This is the unique multiset without duplicates which satifies: completeness_of_isPhenoClosedQ5_isPhenoClosedQ10.

          Note this is fast for evaluation, but to slow with decide.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            unsafe def SuperSymmetry.SU5.Charges.viableChargesMultiset.aux {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] (S5 S10 : Finset 𝓩) :
            Multiset (Charges 𝓩)Multiset (Charges 𝓩)Multiset (Charges 𝓩)

            Auxillary recursive function to define viableChargesMultiset.

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