Minimal super set

i. Overview

The minimally super set of a spectrum of charges x is the finite set of spectrums of charges y such that x ⊆ y and there is no z such that x ⊆ z ⊂ y. The minimal super set is defined using a finite set of possible charges in the 5-bar and 10 representations of su(5). This is to ensure that the minimal super set is itself finite.

In this file we define the minimal super set and prove some basic properties of it.

ii. Key results

• minimalSuperSet: the minimal super set of a charge spectrum.
• exists_minimalSuperSet: the existence of a member of the minimal super set between two charge spectra.
• subset_insert_filter_card_zero: a statement related to closure properties of multisets of charge spectra under a proposition p satisfying certain properties. The proof of this result relies on induction on minimal super sets.

iii. Table of contents

• A. The minimal super set
  • A.1. Members of the minimal super set are super sets
  • A.2. Self is not a member of the minimal super set
  • A.3. Cardinality of member of the minimal super set
  • A.4. Inserting charges and minimal super sets
  • A.5. Existence of a minimal super set member between two charges
• B. Induction properties on the minimal super set
  • B.1. Lifting propositions from minimal super sets to super sets
  • B.2. Closure of multisets based on proposition for minimal super sets
  • B.3. Closure of multisets based on propositions

iv. References

There are no known references for the material in this file.

A. The minimal super set

We define the minimal super set.

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

Given a collection of charges x in ofFinset S5 S10, the minimal 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.

A.1. Members of the minimal super set are super sets

We show the basic property of a member y ∈ minimalSuperSet S5 S10 x, that is that they are indeed super sets, namely x ⊆ y.

theorem SuperSymmetry.SU5.ChargeSpectrum.self_subset_mem_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x y : ChargeSpectrum 𝓩) (hy : y ∈ minimalSuperSet S5 S10 x) : x ⊆ y

A.2. Self is not a member of the minimal super set

A charge spectrum is not a member of its own minimal super set. We give two different forms of this result.

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.self_not_mem_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x : ChargeSpectrum 𝓩) : x ∉ minimalSuperSet S5 S10 x

theorem SuperSymmetry.SU5.ChargeSpectrum.self_neq_mem_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x y : ChargeSpectrum 𝓩) (hy : y ∈ minimalSuperSet S5 S10 x) : x ≠ y

A.3. Cardinality of member of the minimal super set

We show that any member y of the minimal super set of x has cardinality one more than that of x. I.e. it contains exactly one more unique charge.

theorem SuperSymmetry.SU5.ChargeSpectrum.card_of_mem_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x : ChargeSpectrum 𝓩} (y : ChargeSpectrum 𝓩) (hy : y ∈ minimalSuperSet S5 S10 x) : y.card = x.card + 1

A.4. Inserting charges and minimal super sets

We show that inserting a charge from S5 or S10 into x's Q5 or Q10 respectively which is not already present in x gives a member of the minimal super set.

Likewise we show that if x has no qHd or qHu charge, then inserting a charge from S5 into qHd or qHu respectively gives a member of the minimal super set.

theorem SuperSymmetry.SU5.ChargeSpectrum.insert_Q5_mem_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x : ChargeSpectrum 𝓩} (z : 𝓩) (hz : z ∈ S5) (hznot : z ∉ x.Q5) : { qHd := x.qHd, qHu := x.qHu, Q5 := insert z x.Q5, Q10 := x.Q10 } ∈ minimalSuperSet S5 S10 x

theorem SuperSymmetry.SU5.ChargeSpectrum.insert_Q10_mem_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x : ChargeSpectrum 𝓩} (z : 𝓩) (hz : z ∈ S10) (hznot : z ∉ x.Q10) : { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert z x.Q10 } ∈ minimalSuperSet S5 S10 x

theorem SuperSymmetry.SU5.ChargeSpectrum.some_qHd_mem_minimalSuperSet_of_none {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x2 : Option 𝓩 × Finset 𝓩 × Finset 𝓩} (z : 𝓩) (hz : z ∈ S5) : { qHd := some z, qHu := x2.1, Q5 := x2.2.1, Q10 := x2.2.2 } ∈ minimalSuperSet S5 S10 { qHd := none, qHu := x2.1, Q5 := x2.2.1, Q10 := x2.2.2 }

theorem SuperSymmetry.SU5.ChargeSpectrum.some_qHu_mem_minimalSuperSet_of_none {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x1 : Option 𝓩} {x2 : Finset 𝓩 × Finset 𝓩} (z : 𝓩) (hz : z ∈ S5) : { qHd := x1, qHu := some z, Q5 := x2.1, Q10 := x2.2 } ∈ minimalSuperSet S5 S10 { qHd := x1, qHu := none, Q5 := x2.1, Q10 := x2.2 }

A.5. Existence of a minimal super set member between two charges

We show that if y has charges from S5 and S10 and is a super set of x but not equal to x then there is a z in the minimal super set of x which is a subset of y.

This shows, in a sense, that minimalSuperSet is "minimal", although it does not go all the way to doing that. In particular, it does show that every minimal super set is a member of minimalSuperSet.

theorem SuperSymmetry.SU5.ChargeSpectrum.exists_minimalSuperSet {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) {x y : ChargeSpectrum 𝓩} (hy : y ∈ ofFinset S5 S10) (hsubset : x ⊆ y) (hxneqy : x ≠ y) : ∃ z ∈ minimalSuperSet S5 S10 x, z ⊆ y

B. Induction properties on the minimal super set

We now prove a number of induction properties related to minimal super sets.

B.1. Lifting propositions from minimal super sets to super sets

We show that for a proposition p on charge spectra with the property that it is true on all minimal super sets of x if it true on x itself, then it is true on all super sets of x if it is true for x itself.

theorem SuperSymmetry.SU5.ChargeSpectrum.minimalSuperSet_induction_on_inductive {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} (p : ChargeSpectrum 𝓩 → Prop) (hp : ∀ (x : ChargeSpectrum 𝓩), p x → ∀ y ∈ minimalSuperSet S5 S10 x, p y) (x : ChargeSpectrum 𝓩) (hbase : p x) (y : ChargeSpectrum 𝓩) (hy : y ∈ ofFinset S5 S10) (hsubset : x ⊆ y) (n : ℕ) (hn : n = y.card - x.card) : p y

B.2. Closure of multisets based on proposition for minimal super sets

We show that for a predicate p on charge spectrum, if a multiset T of complete charge spectra has the property that

• all insertions of a q10 charge either ends in T or fails p.
• all insertions of a q5 charge either ends in T or fails p. Then if x is in T then all members of the minimal super set of x either are in T or fail p.

theorem SuperSymmetry.SU5.ChargeSpectrum.insert_filter_card_zero {𝓩 : Type} [DecidableEq 𝓩] (T : Multiset (ChargeSpectrum 𝓩)) (S5 S10 : Finset 𝓩) (p : ChargeSpectrum 𝓩 → Prop) [DecidablePred p] (hComplet : ∀ x ∈ T, x.IsComplete) (h10 : ∀ (q10 : ↥S10), Multiset.filter (fun (y : ChargeSpectrum 𝓩) => y ∉ T ∧ p y) (Multiset.map (fun (x : ChargeSpectrum 𝓩) => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) T) = ∅) (h5 : ∀ (q5 : ↥S5), Multiset.filter (fun (y : ChargeSpectrum 𝓩) => y ∉ T ∧ p y) (Multiset.map (fun (x : ChargeSpectrum 𝓩) => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) T) = ∅) (x : ChargeSpectrum 𝓩) : x ∈ T → ∀ y ∈ minimalSuperSet S5 S10 x, y ∉ T → ¬p y

B.3. Closure of multisets based on propositions

We show that for a predicate p on charge spectrum which if false on a charge spectrum is also false on all its super sets, if a multiset T of complete charge spectra has the property that

• all insertions of a q10 charge either ends in T or fails p.
• all insertions of a q5 charge either ends in T or fails p. Then if y is not in T then it does not satisfy p.

We first prove this with an explicit induction argument, n, and then we prove it in a more user friendly way.

theorem SuperSymmetry.SU5.ChargeSpectrum.subset_insert_filter_card_zero_inductive {𝓩 : Type} [DecidableEq 𝓩] (T : Multiset (ChargeSpectrum 𝓩)) (S5 S10 : Finset 𝓩) (p : ChargeSpectrum 𝓩 → Prop) [DecidablePred p] (hnotSubset : ∀ (x y : ChargeSpectrum 𝓩), x ⊆ y → ¬p x → ¬p y) (hComplet : ∀ x ∈ T, x.IsComplete) (x : ChargeSpectrum 𝓩) (hx : x ∈ T) (y : ChargeSpectrum 𝓩) (hsubset : x ⊆ y) (hy : y ∈ ofFinset S5 S10) (h10 : ∀ (q10 : ↥S10), Multiset.filter (fun (y : ChargeSpectrum 𝓩) => y ∉ T ∧ p y) (Multiset.map (fun (x : ChargeSpectrum 𝓩) => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) T) = ∅) (h5 : ∀ (q5 : ↥S5), Multiset.filter (fun (y : ChargeSpectrum 𝓩) => y ∉ T ∧ p y) (Multiset.map (fun (x : ChargeSpectrum 𝓩) => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) T) = ∅) (n : ℕ) (hn : n = y.card - x.card) : y ∉ T → ¬p y

theorem SuperSymmetry.SU5.ChargeSpectrum.subset_insert_filter_card_zero {𝓩 : Type} [DecidableEq 𝓩] (T : Multiset (ChargeSpectrum 𝓩)) (S5 S10 : Finset 𝓩) (p : ChargeSpectrum 𝓩 → Prop) [DecidablePred p] (hnotSubset : ∀ (x y : ChargeSpectrum 𝓩), x ⊆ y → ¬p x → ¬p y) (hComplet : ∀ x ∈ T, x.IsComplete) (x : ChargeSpectrum 𝓩) (hx : x ∈ T) (y : ChargeSpectrum 𝓩) (hsubset : x ⊆ y) (hy : y ∈ ofFinset S5 S10) (h10 : ∀ (q10 : ↥S10), Multiset.filter (fun (y : ChargeSpectrum 𝓩) => y ∉ T ∧ p y) (Multiset.map (fun (x : ChargeSpectrum 𝓩) => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) T) = ∅) (h5 : ∀ (q5 : ↥S5), Multiset.filter (fun (y : ChargeSpectrum 𝓩) => y ∉ T ∧ p y) (Multiset.map (fun (x : ChargeSpectrum 𝓩) => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) T) = ∅) : y ∉ T → ¬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.