PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.Potential

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

This file contains properties of the potential terms of the SU(5) SUSY.

The terms from the superpotential considered are (arXiv:0912.0853) : 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 (arXiv:0912.0853) : K ⊃ K¹ᵢⱼₖ 10ⁱ 10ʲ 5Mᵏ + K²ᵢ 5̄Hu 5̄Hd 10ⁱ

Important results #

Previous versions #

A previous version of this code was replaced in PR #569.

source
inductive SuperSymmetry.SU5.PotentialTerm :
Type

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

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.
    source
    def SuperSymmetry.SU5.PotentialTerm.toFieldLabel :
    PotentialTerm → List FieldLabel

    The fields contained within a given term of the potential.

    Equations
    Instances For
      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
        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.

        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
          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}
            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