PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.Charges.AllowsTerm

Charges allowing terms #

The charges of representations x : Charges allow a potential term T : PotentialTerm if the zero charge is in the set of charges associated with that potential term.

We define this proposition AllowsTerm and prove results about it.

We also define allowsTermForm, which is a function that takes three integers a, b, and c and a potential term T, and returns a Charges that allows the term T. We prove that any charges that allows a term T has a subset which can be expressed as allowsTermForm a b c T for some integers a, b, and c.

The charges of representations x : Charges allow a potential term T : PotentialTerm if the zero charge is in the set of charges associated with that potential term.

Equations
Instances For
    theorem SuperSymmetry.SU5.Charges.allowsTerm_mono {𝓩 : Type} [AddCommGroup 𝓩] {T : PotentialTerm} {y x : Charges 𝓩} (h : y x) (hy : y.AllowsTerm T) :

    allowsTermForm #

    def SuperSymmetry.SU5.Charges.allowsTermForm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (a b c : 𝓩) (T : PotentialTerm) :
    Charges 𝓩

    A element of Charges from three intergers a b c : ℤ for a given potential term T. Defined such that allowsTermForm a b c T always allows the potential term T, and if any over charge x allows T then it is due to a subset of the form allowsTermForm a b c T.

    Equations
    Instances For
      theorem SuperSymmetry.SU5.Charges.allowsTerm_of_eq_allowsTermForm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} (x : Charges 𝓩) (h : ∃ (a : 𝓩) (b : 𝓩) (c : 𝓩), x = allowsTermForm a b c T) :
      theorem SuperSymmetry.SU5.Charges.allowsTermForm_subset_allowsTerm_of_allowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : Charges 𝓩} (h : x.AllowsTerm T) :
      ∃ (a : 𝓩) (b : 𝓩) (c : 𝓩), allowsTermForm a b c T x (allowsTermForm a b c T).AllowsTerm T
      theorem SuperSymmetry.SU5.Charges.allowsTerm_iff_subset_allowsTermForm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : Charges 𝓩} :
      x.AllowsTerm T ∃ (a : 𝓩) (b : 𝓩) (c : 𝓩), allowsTermForm a b c T x

      Insertion of Q5 #

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

      The proposition for which says, given a charge x adding a charge q5 permits the existence of a potential term T due to the addition of that charge.

      Equations
      Instances For
        Equations
        theorem SuperSymmetry.SU5.Charges.allowsTermQ5_or_allowsTerm_of_allowsTerm_insertQ5 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q5 : 𝓩} (T : PotentialTerm) (h : AllowsTerm (qHd, qHu, insert q5 Q5, Q10) T) :
        AllowsTermQ5 (qHd, qHu, Q5, Q10) q5 T AllowsTerm (qHd, qHu, Q5, Q10) T
        theorem SuperSymmetry.SU5.Charges.allowsTerm_insertQ5_of_allowsTermQ5 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q5 : 𝓩} (T : PotentialTerm) (h : AllowsTermQ5 (qHd, qHu, Q5, Q10) q5 T) :
        AllowsTerm (qHd, qHu, insert q5 Q5, Q10) T
        theorem SuperSymmetry.SU5.Charges.allowsTerm_insertQ5_iff_allowsTermQ5 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q5 : 𝓩} (T : PotentialTerm) :
        AllowsTerm (qHd, qHu, insert q5 Q5, Q10) T AllowsTermQ5 (qHd, qHu, Q5, Q10) q5 T AllowsTerm (qHd, qHu, Q5, Q10) T

        AllowsTermQ10 #

        def SuperSymmetry.SU5.Charges.AllowsTermQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : Charges 𝓩) (q10 : 𝓩) (T : PotentialTerm) :

        The proposition for which says, given a charge x adding a charge q5 permits the existence of a potential term T due to the addition of that charge.

        Equations
        Instances For
          theorem SuperSymmetry.SU5.Charges.allowsTermQ10_or_allowsTerm_of_allowsTerm_insertQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q10 : 𝓩} (T : PotentialTerm) (h : AllowsTerm (qHd, qHu, Q5, insert q10 Q10) T) :
          AllowsTermQ10 (qHd, qHu, Q5, Q10) q10 T AllowsTerm (qHd, qHu, Q5, Q10) T
          theorem SuperSymmetry.SU5.Charges.allowsTerm_insertQ10_of_allowsTermQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q10 : 𝓩} (T : PotentialTerm) (h : AllowsTermQ10 (qHd, qHu, Q5, Q10) q10 T) :
          AllowsTerm (qHd, qHu, Q5, insert q10 Q10) T
          theorem SuperSymmetry.SU5.Charges.allowsTerm_insertQ10_iff_allowsTermQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q10 : 𝓩} (T : PotentialTerm) :
          AllowsTerm (qHd, qHu, Q5, insert q10 Q10) T AllowsTermQ10 (qHd, qHu, Q5, Q10) q10 T AllowsTerm (qHd, qHu, Q5, Q10) T