PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.Charges.MinimalSuperSet

Minimal super set #

Given a a colleciton of charges x, and two sets of charges S5 and S10, a minimal super set of x is the collection of charge y which is a super sets of x, for which the the additional charges in y are corresponding in S5 and S10, and which is minimal in this regard.

def SuperSymmetry.SU5.Charges.minimalSuperSet {𝓩 : 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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem SuperSymmetry.SU5.Charges.self_subset_mem_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x y : Charges 𝓩) (hy : y minimalSuperSet S5 S10 x) :
    x y
    @[simp]
    theorem SuperSymmetry.SU5.Charges.self_not_mem_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x : Charges 𝓩) :
    xminimalSuperSet S5 S10 x
    theorem SuperSymmetry.SU5.Charges.self_neq_mem_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x y : Charges 𝓩) (hy : y minimalSuperSet S5 S10 x) :
    x y
    theorem SuperSymmetry.SU5.Charges.card_of_mem_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x : Charges 𝓩} (y : Charges 𝓩) (hy : y minimalSuperSet S5 S10 x) :
    y.card = x.card + 1
    theorem SuperSymmetry.SU5.Charges.insert_Q5_mem_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x : Charges 𝓩} (z : 𝓩) (hz : z S5) (hznot : zx.2.2.1) :
    (x.1, x.2.1, insert z x.2.2.1, x.2.2.2) minimalSuperSet S5 S10 x
    theorem SuperSymmetry.SU5.Charges.insert_Q10_mem_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x : Charges 𝓩} (z : 𝓩) (hz : z S10) (hznot : zx.2.2.2) :
    (x.1, x.2.1, x.2.2.1, insert z x.2.2.2) minimalSuperSet S5 S10 x
    theorem SuperSymmetry.SU5.Charges.some_qHd_mem_minimalSuperSet_of_none {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x2 : Option 𝓩 × Finset 𝓩 × Finset 𝓩} (z : 𝓩) (hz : z S5) :
    theorem SuperSymmetry.SU5.Charges.some_qHu_mem_minimalSuperSet_of_none {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x1 : Option 𝓩} {x2 : Finset 𝓩 × Finset 𝓩} (z : 𝓩) (hz : z S5) :
    (x1, some z, x2) minimalSuperSet S5 S10 (x1, none, x2)
    theorem SuperSymmetry.SU5.Charges.exists_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) {x y : Charges 𝓩} (hy : y ofFinset S5 S10) (hsubset : x y) (hxneqy : x y) :
    zminimalSuperSet S5 S10 x, z y
    theorem SuperSymmetry.SU5.Charges.minimalSuperSet_induction_on_inductive {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} (p : Charges 𝓩Prop) (hp : ∀ (x : Charges 𝓩), p xyminimalSuperSet S5 S10 x, p y) (x : Charges 𝓩) (hbase : p x) (y : Charges 𝓩) (hy : y ofFinset S5 S10) (hsubset : x y) (n : ) (hn : n = y.card - x.card) :
    p y

    Inserting charges and minimal super sets #

    theorem SuperSymmetry.SU5.Charges.insert_filter_card_zero {𝓩 : Type} [DecidableEq 𝓩] (T : Multiset (Charges 𝓩)) (S5 S10 : Finset 𝓩) (p : Charges 𝓩Prop) [DecidablePred p] (hComplet : xT, x.IsComplete) (h10 : ∀ (q10 : { x : 𝓩 // x S10 }), Multiset.filter (fun (y : Charges 𝓩) => yT p y) (Multiset.map (fun (x : Charges 𝓩) => (x.1, x.2.1, x.2.2.1, insert (↑q10) x.2.2.2)) T) = ) (h5 : ∀ (q5 : { x : 𝓩 // x S5 }), Multiset.filter (fun (y : Charges 𝓩) => yT p y) (Multiset.map (fun (x : Charges 𝓩) => (x.1, x.2.1, insert (↑q5) x.2.2.1, x.2.2.2)) T) = ) (x : Charges 𝓩) :
    x TyminimalSuperSet S5 S10 x, yT¬p y
    theorem SuperSymmetry.SU5.Charges.subset_insert_filter_card_zero_inductive {𝓩 : Type} [DecidableEq 𝓩] (T : Multiset (Charges 𝓩)) (S5 S10 : Finset 𝓩) (p : Charges 𝓩Prop) [DecidablePred p] (hnotSubset : ∀ (x y : Charges 𝓩), x y¬p x¬p y) (hComplet : xT, x.IsComplete) (x : Charges 𝓩) (hx : x T) (y : Charges 𝓩) (hsubset : x y) (hy : y ofFinset S5 S10) (h10 : ∀ (q10 : { x : 𝓩 // x S10 }), Multiset.filter (fun (y : Charges 𝓩) => yT p y) (Multiset.map (fun (x : Charges 𝓩) => (x.1, x.2.1, x.2.2.1, insert (↑q10) x.2.2.2)) T) = ) (h5 : ∀ (q5 : { x : 𝓩 // x S5 }), Multiset.filter (fun (y : Charges 𝓩) => yT p y) (Multiset.map (fun (x : Charges 𝓩) => (x.1, x.2.1, insert (↑q5) x.2.2.1, x.2.2.2)) T) = ) (n : ) (hn : n = y.card - x.card) :
    yT¬p y
    theorem SuperSymmetry.SU5.Charges.subset_insert_filter_card_zero {𝓩 : Type} [DecidableEq 𝓩] (T : Multiset (Charges 𝓩)) (S5 S10 : Finset 𝓩) (p : Charges 𝓩Prop) [DecidablePred p] (hnotSubset : ∀ (x y : Charges 𝓩), x y¬p x¬p y) (hComplet : xT, x.IsComplete) (x : Charges 𝓩) (hx : x T) (y : Charges 𝓩) (hsubset : x y) (hy : y ofFinset S5 S10) (h10 : ∀ (q10 : { x : 𝓩 // x S10 }), Multiset.filter (fun (y : Charges 𝓩) => yT p y) (Multiset.map (fun (x : Charges 𝓩) => (x.1, x.2.1, x.2.2.1, insert (↑q10) x.2.2.2)) T) = ) (h5 : ∀ (q5 : { x : 𝓩 // x S5 }), Multiset.filter (fun (y : Charges 𝓩) => yT p y) (Multiset.map (fun (x : Charges 𝓩) => (x.1, x.2.1, insert (↑q5) x.2.2.1, x.2.2.2)) T) = ) :
    yT¬p y

    For a proposition p if (T.uniqueMap4 (insert q10.1)).toMultiset.filter p and (T.uniqueMap3 (insert q5.1)).toMultiset.filter p for all q5 ∈ S5 and q10 ∈ S10 then if x ∈ T and x ⊆ y if y ∉ T then ¬ p y. This assumes that all charges in T are complete, and that p satisfies x ⊆ y → ¬ p x → ¬ p y.