PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.Charges.PhenoConstrained

Pheno constrained charges #

We say a charge is pheno-constrained if it leads to allows proton decay or R-parity violating terms.

We are actually intrested in the charges which are not pheno-constrained.

A charge is pheno-constrained if it leads to the presence of any term causing proton decay {W1, Λ, W2, K1} or R-parity violation {β, Λ, W2, W4, K1, K2}.

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.

    The collection of charges of super-potential terms leading to a pheno-constrained model.

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

      Is Pheno constrained Q5 addition #

      def SuperSymmetry.SU5.Charges.IsPhenoConstrainedQ5 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : Charges 𝓩) (q5 : 𝓩) :

      The proposition which is true if the addition of a charge q5 to a set of charegs x leads x to being phenomenologically constrained.

      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.isPhenoConstrained_insertQ5_iff_isPhenoConstrainedQ5 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q5 : 𝓩} :
        IsPhenoConstrained (qHd, qHu, insert q5 Q5, Q10) IsPhenoConstrainedQ5 (qHd, qHu, Q5, Q10) q5 IsPhenoConstrained (qHd, qHu, Q5, Q10)
        def SuperSymmetry.SU5.Charges.IsPhenoConstrainedQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : Charges 𝓩) (q10 : 𝓩) :

        The proposition which is true if the addition of a charge q10 to a set of charegs x leads x to being phenomenologically constrained.

        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.isPhenoConstrained_insertQ10_iff_isPhenoConstrainedQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q10 : 𝓩} :
          IsPhenoConstrained (qHd, qHu, Q5, insert q10 Q10) IsPhenoConstrainedQ10 (qHd, qHu, Q5, Q10) q10 IsPhenoConstrained (qHd, qHu, Q5, Q10)