PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.Charges.Completions

Completions of charges #

We say a set of charges is complete if it has all types of fields.

Given a collection of charges x in ofFinset S5 S10, the completions of x are the, minimimal charges y in ofFinset S5 S10 which are a super sets of x and are complete.

This module defines the IsComplete proposition and completions of charges and provides lemmas about them.

Completions #

A collection of charges is complete if it has all types of fields.

Equations
Instances For
    theorem SuperSymmetry.SU5.Charges.isComplete_mono {𝓩 : Type} {x y : Charges 𝓩} (h : x y) (hx : x.IsComplete) :

    Completions #

    Note the completions are not monotonic with respect to the subset relation.

    def SuperSymmetry.SU5.Charges.completions {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x : Charges 𝓩) :

    Given a collection of charges x in ofFinset S5 S10, the minimimal charges y in ofFinset S5 S10 which are a super sets of x and are complete.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem SuperSymmetry.SU5.Charges.completions_nodup {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x : Charges 𝓩) :
      (completions S5 S10 x).Nodup
      theorem SuperSymmetry.SU5.Charges.completions_eq_singleton_of_complete {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} (x : Charges 𝓩) (hcomplete : x.IsComplete) :
      completions S5 S10 x = {x}
      theorem SuperSymmetry.SU5.Charges.mem_completions_isComplete {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x y : Charges 𝓩} (hx : y completions S5 S10 x) :
      theorem SuperSymmetry.SU5.Charges.self_subset_mem_completions {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x y : Charges 𝓩) (hy : y completions S5 S10 x) :
      x y
      theorem SuperSymmetry.SU5.Charges.exist_completions_subset_of_complete {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x y : Charges 𝓩) (hsubset : x y) (hy : y ofFinset S5 S10) (hycomplete : y.IsComplete) :
      zcompletions S5 S10 x, z y

      Completions of minimal top yukawa #

      A fast version of completions for an x which is in minimallyAllowsTermsOfFinset S5 S10 .topYukawa.

      Equations
      Instances For