Minimally allows terms #
Given a set of charges x : Charges
corresponding to charges of the representations
present in the theory, and a potential term T : PotentialTerm
, we say that x
minimally allows T
if it allows the term T
and no proper subset of x
allows T
.
def
SuperSymmetry.SU5.Charges.MinimallyAllowsTerm
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
(x : Charges 𝓩)
(T : PotentialTerm)
:
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
- x.MinimallyAllowsTerm T = ∀ y ∈ x.powerset, y = x ↔ y.AllowsTerm T
Instances For
instance
SuperSymmetry.SU5.Charges.instDecidableMinimallyAllowsTerm
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
(x : Charges 𝓩)
(T : PotentialTerm)
:
Decidable (x.MinimallyAllowsTerm T)
Equations
- x.instDecidableMinimallyAllowsTerm T = inferInstanceAs (Decidable (∀ y ∈ x.powerset, y = x ↔ y.AllowsTerm T))
theorem
SuperSymmetry.SU5.Charges.allowsTerm_of_minimallyAllowsTerm
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{T : PotentialTerm}
{x : Charges 𝓩}
(h : x.MinimallyAllowsTerm T)
:
x.AllowsTerm T
theorem
SuperSymmetry.SU5.Charges.allowsTerm_of_has_minimallyAllowsTerm_subset
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{T : PotentialTerm}
{x : Charges 𝓩}
(hx : ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T)
:
x.AllowsTerm T
theorem
SuperSymmetry.SU5.Charges.minimallyAllowsTerm_iff_powerset_filter_eq
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{T : PotentialTerm}
{x : Charges 𝓩}
:
theorem
SuperSymmetry.SU5.Charges.minimallyAllowsTerm_iff_powerset_countP_eq_one
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{T : PotentialTerm}
{x : Charges 𝓩}
:
x.MinimallyAllowsTerm T ↔ Multiset.countP (fun (y : Charges 𝓩) => y.AllowsTerm T) x.powerset.val = 1
theorem
SuperSymmetry.SU5.Charges.subset_minimallyAllowsTerm_of_allowsTerm
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{T : PotentialTerm}
{x : Charges 𝓩}
(hx : x.AllowsTerm T)
:
∃ y ∈ x.powerset, y.MinimallyAllowsTerm T
theorem
SuperSymmetry.SU5.Charges.allowsTerm_iff_subset_minimallyAllowsTerm
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{T : PotentialTerm}
{x : Charges 𝓩}
:
theorem
SuperSymmetry.SU5.Charges.card_le_degree_of_minimallyAllowsTerm
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{T : PotentialTerm}
{x : Charges 𝓩}
(h : x.MinimallyAllowsTerm T)
:
theorem
SuperSymmetry.SU5.Charges.eq_allowsTermForm_of_minimallyAllowsTerm
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{T : PotentialTerm}
{x : Charges 𝓩}
(h1 : x.MinimallyAllowsTerm T)
:
∃ (a : 𝓩) (b : 𝓩) (c : 𝓩), x = allowsTermForm a b c T
theorem
SuperSymmetry.SU5.Charges.allowsTermForm_minimallyAllowsTerm
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{a b c : 𝓩}
{T : PotentialTerm}
(hT : T ≠ PotentialTerm.W1 ∧ T ≠ PotentialTerm.W2)
:
(allowsTermForm a b c T).MinimallyAllowsTerm T