PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.Potential

Potential of the SU(5) + U(1) GUT #

i. Overview #

In this module we will write down some of the potential terms appearing in an SU(5) SUSY GUT model, with matter in the 5-bar and 10d representations.

A future iteration of this file will include all terms, and derive them from symmetry properties.

The terms of the super-potential we will consider are: W ⊃ μ 5Hu 5̄Hd + 𝛽ᵢ 5̄Mⁱ5Hu + 𝜆ᵢⱼₖ 5̄Mⁱ 5̄Mʲ 10ᵏ + W¹ᵢⱼₖₗ 10ⁱ 10ʲ 10ᵏ 5̄Mˡ + W²ᵢⱼₖ 10ⁱ 10ʲ 10ᵏ 5̄Hd + W³ᵢⱼ 5̄Mⁱ 5̄Mʲ 5Hu 5Hu + W⁴ᵢ 5̄Mⁱ 5̄Hd 5Hu 5Hu

The terms of the Kahler potential are: K ⊃ K¹ᵢⱼₖ 10ⁱ 10ʲ 5Mᵏ + K²ᵢ 5̄Hu 5̄Hd 10ⁱ

ii. Key results #

iii. Table of contents #

iv. References #

A. The definition of PotentialTerm #

We define an inductive type with a term for each of the potential terms we are interested in, present in both the super-potential and Kahler potential.

source
inductive SuperSymmetry.SU5.PotentialTerm :
Type

Relevant terms part of the superpotential and Kahler potential of the SU(5) SUSY GUT.

  • μ : PotentialTerm

    The term μ 5Hu 5̄Hd appearing in the super-potential.

  • β : PotentialTerm

    The term 𝛽ᵢ 5̄Mⁱ5Hu appearing in the super-potential.

  • Λ : PotentialTerm

    The term 𝜆ᵢⱼₖ 5̄Mⁱ 5̄Mʲ 10ᵏ appearing in the super-potential.

  • W1 : PotentialTerm

    The term W¹ᵢⱼₖₗ 10ⁱ 10ʲ 10ᵏ 5̄Mˡ appearing in the super-potential.

  • W2 : PotentialTerm

    The term W²ᵢⱼₖ 10ⁱ 10ʲ 10ᵏ 5̄Hd appearing in the super-potential.

  • W3 : PotentialTerm

    The term W³ᵢⱼ 5̄Mⁱ 5̄Mʲ 5Hu 5Hu appearing in the super-potential.

  • W4 : PotentialTerm

    The term W⁴ᵢ 5̄Mⁱ 5̄Hd 5Hu 5Hu appearing in the super-potential.

  • K1 : PotentialTerm

    The term K¹ᵢⱼₖ 10ⁱ 10ʲ 5Mᵏ appearing in the Kahler potential.

  • K2 : PotentialTerm

    The term K²ᵢ 5̄Hu 5̄Hd 10ⁱ appearing in the Kahler potential.

  • topYukawa : PotentialTerm

    The term λᵗᵢⱼ 10ⁱ 10ʲ 5Hu appearing in the super-potential.

  • bottomYukawa : PotentialTerm

    The term λᵇᵢⱼ 10ⁱ 5̄Mʲ 5̄Hd appearing in the super-potential.

Instances For
    source
    instance SuperSymmetry.SU5.instDecidableEqPotentialTerm :
    DecidableEq PotentialTerm
    Equations
    source
    instance SuperSymmetry.SU5.instFintypePotentialTerm :
    Fintype PotentialTerm
    Equations
    • One or more equations did not get rendered due to their size.

    B. Relation to field labels #

    We map each term in the potential to the list of FieldLabels which it contains. This allows us to define various properties of the potential term in a safe way, based solely on the field content.

    source
    def SuperSymmetry.SU5.PotentialTerm.toFieldLabel :
    PotentialTerm → List FieldLabel

    The fields contained within a given term of the potential.

    Equations
    Instances For

      C. Presence in the super-potential #

      We define a predicate which is true on those terms which are members of the super-potential. We will also prove that this predicate is decidable.

      source
      def SuperSymmetry.SU5.PotentialTerm.InSuperPotential :
      PotentialTerm → Prop

      The proposition which is true on those terms which are members of the super potential.

      Equations
      Instances For
        source
        instance SuperSymmetry.SU5.PotentialTerm.instDecidableInSuperPotential (T : PotentialTerm) :
        Decidable T.InSuperPotential
        Equations

        C.1. In super potential implies no conjugate fields #

        Been in the super potential implies that the term contains no conjugate fields.

        source
        theorem SuperSymmetry.SU5.PotentialTerm.no_conjugate_in_toFieldLabel_of_inSuperPotential {T : PotentialTerm} (h : T.InSuperPotential) :
        FieldLabel.fiveMatter ∉ T.toFieldLabel ∧ FieldLabel.fiveHd ∉ T.toFieldLabel ∧ FieldLabel.fiveBarHu ∉ T.toFieldLabel

        The terms within the super-potential contain no conjugate fields.

        D. Degree of the potential term #

        We define the degree of a term in the potential to be the number of fields it contains. The degree of all terms present is less than or equal to four.

        source
        def SuperSymmetry.SU5.PotentialTerm.degree (T : PotentialTerm) :
        ℕ

        The degree of a term in the potential.

        Equations
        Instances For
          source
          theorem SuperSymmetry.SU5.PotentialTerm.degree_le_four (T : PotentialTerm) :
          T.degree ≤ 4

          E. R-parity of the potential terms #

          Based on the R-parity of the underlying fields, we define the R-parity of each term in the potential. We show that those terms which violate R-parity are exactly those which are β, Λ, W2, W4, K1, or K2.

          source
          def SuperSymmetry.SU5.PotentialTerm.RParity (T : PotentialTerm) :
          Fin 2

          The R-parity of a term in the potential.

          Equations
          Instances For
            source
            theorem SuperSymmetry.SU5.PotentialTerm.violates_RParity_iff_mem {T : PotentialTerm} :
            T.RParity = 1 ↔ T ∈ {β, Λ, W2, W4, K1, K2}

            F. Terms which violate proton decay #

            We write down the finite set of terms which contribute to proton decay. We do not at this point prove this result.

            source
            def SuperSymmetry.SU5.PotentialTerm.causeProtonDecay :
            Finset PotentialTerm

            The finite set of terms in the superpotential and Kahler potential which are involved in proton decay.

            • W¹ᵢⱼₖₗ 10ⁱ 10ʲ 10ᵏ 5̄Mˡ
            • 𝜆ᵢⱼₖ 5̄Mⁱ 5̄Mʲ 10ᵏ
            • W²ᵢⱼₖ 10ⁱ 10ʲ 10ᵏ 5̄Hd
            • K¹ᵢⱼₖ 10ⁱ 10ʲ 5Mᵏ
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For