PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.Basic

Charge spectrum which minimally allows terms #

i. Overview #

We can say that a charge spectrum x : ChargeSpectrum 𝓩 minimally allows a potential term T : PotentialTerm if it allows the term T and no strict subset of x allows T.

That is to say, you need all of the charges in x to allow the term T.

We show that any charge spectrum which allows T has a subset which minimally allows T.

We show that every charge spectrum which minimally allows T is of the form allowsTermForm a b c T for some a b c : 𝓩, and the reverse is true for T not equal to W1 or W2.

ii. Key results #

iii. Table of contents #

iv. References #

There are no known references for this material.

A. Charge spectra which minimally allow potential terms #

We define the predicate MinimallyAllowsTerm on charge spectra which is true if the charge spectrum allows a given potential term and no strict subset of it allows the term.

We prove properties of charge spectra which minimally allow potential terms.

source
def SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (T : PotentialTerm) :
Prop

A collection of charges x : Charges is said to minimally allow the potential term T if it allows T and no strict subset of it allows T.

Equations
Instances For

    A.1. Decidability of MinimallyAllowsTerm #

    We show that MinimallyAllowsTerm is decidable.

    source
    instance SuperSymmetry.SU5.ChargeSpectrum.instDecidableMinimallyAllowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (T : PotentialTerm) :
    Decidable (x.MinimallyAllowsTerm T)
    Equations

    A.2. A charge spectrum which minimally allows a term allows the term #

    Somewhat trivially a charge spectrum which minimally allows the term does indeed allow the term.

    source
    theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_of_minimallyAllowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : ChargeSpectrum 𝓩} (h : x.MinimallyAllowsTerm T) :
    x.AllowsTerm T

    A.3. Spectrum with a subset which minimally allows a term, allows the term #

    If a charge spectrum x has a subset which minimally allows a term T, then x allows T.

    source
    theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_of_has_minimallyAllowsTerm_subset {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : ChargeSpectrum 𝓩} (hx : ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T) :
    x.AllowsTerm T

    A.4. Minimally allows term iff only member of powerset allowing term #

    A charge spectrum x minimally allows a term T if and only if the only member of its own powerset which allows T is itself.

    source
    theorem SuperSymmetry.SU5.ChargeSpectrum.minimallyAllowsTerm_iff_powerset_filter_eq {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : ChargeSpectrum 𝓩} :
    x.MinimallyAllowsTerm T ↔ {y ∈ x.powerset | y.AllowsTerm T} = {x}

    A.5. Minimally allows term iff powerset allowing term has cardinal one #

    A charge spectrum x minimally allows a term T if and only the the number of members of its powerset which allow T is one.

    source
    theorem SuperSymmetry.SU5.ChargeSpectrum.minimallyAllowsTerm_iff_powerset_countP_eq_one {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : ChargeSpectrum 𝓩} :
    x.MinimallyAllowsTerm T ↔ Multiset.countP (fun (y : ChargeSpectrum 𝓩) => y.AllowsTerm T) x.powerset.val = 1

    A.6. A charge spectrum which allows a term has a subset which minimally allows the term #

    If a charge spectrum x allows a term T, then it has a subset which minimally allows T.

    source
    theorem SuperSymmetry.SU5.ChargeSpectrum.subset_minimallyAllowsTerm_of_allowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : ChargeSpectrum 𝓩} (hx : x.AllowsTerm T) :
    ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T

    A.7. A charge spectrum allows a term iff it has a subset which minimally allows the term #

    We combine results above to show that a charge spectrum allows a term if and only if it has a subset which minimally allows the term.

    source
    theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_iff_subset_minimallyAllowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : ChargeSpectrum 𝓩} :
    x.AllowsTerm T ↔ ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T

    A.8. Cardinality of spectrum which minimally allows term is at most degree of term #

    We show that the cardinality of a charge spectrum which minimally allows a term T is at most the degree of T.

    source
    theorem SuperSymmetry.SU5.ChargeSpectrum.card_le_degree_of_minimallyAllowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : ChargeSpectrum 𝓩} (h : x.MinimallyAllowsTerm T) :
    x.card ≤ T.degree

    B. Relation between MinimallyAllowsTerm and allowsTermForm #

    We now relate the predicate MinimallyAllowsTerm to charge spectra of the form allowsTermForm a b c T.

    B.1. A charge spectrum which minimally allows a term is of the form allowsTermForm a b c T #

    We show that any charge spectrum which minimally allows a term T is of the form allowsTermForm a b c T for some a b c : 𝓩.

    source
    theorem SuperSymmetry.SU5.ChargeSpectrum.eq_allowsTermForm_of_minimallyAllowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : ChargeSpectrum 𝓩} (h1 : x.MinimallyAllowsTerm T) :
    ∃ (a : 𝓩) (b : 𝓩) (c : 𝓩), x = allowsTermForm a b c T

    B.2. allowsTermForm a b c T minimally allows T if T is not W1 or W2 #

    We show that charge spectra of the form allowsTermForm a b c T minimally allow T provided that T is not one of W1 or W2.

    source
    theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm_minimallyAllowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {a b c : 𝓩} {T : PotentialTerm} (hT : T ≠ PotentialTerm.W1 ∧ T ≠ PotentialTerm.W2) :
    (allowsTermForm a b c T).MinimallyAllowsTerm T