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)
:
@[simp]
theorem
SuperSymmetry.SU5.Charges.self_not_mem_minimalSuperSet
{𝓩 : Type}
[DecidableEq 𝓩]
(S5 S10 : Finset 𝓩)
(x : Charges 𝓩)
:
x ∉ minimalSuperSet 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)
:
theorem
SuperSymmetry.SU5.Charges.card_of_mem_minimalSuperSet
{𝓩 : Type}
[DecidableEq 𝓩]
{S5 S10 : Finset 𝓩}
{x : Charges 𝓩}
(y : Charges 𝓩)
(hy : y ∈ minimalSuperSet S5 S10 x)
:
theorem
SuperSymmetry.SU5.Charges.insert_Q5_mem_minimalSuperSet
{𝓩 : Type}
[DecidableEq 𝓩]
{S5 S10 : Finset 𝓩}
{x : Charges 𝓩}
(z : 𝓩)
(hz : z ∈ S5)
(hznot : z ∉ x.2.2.1)
:
theorem
SuperSymmetry.SU5.Charges.insert_Q10_mem_minimalSuperSet
{𝓩 : Type}
[DecidableEq 𝓩]
{S5 S10 : Finset 𝓩}
{x : Charges 𝓩}
(z : 𝓩)
(hz : z ∈ S10)
(hznot : z ∉ x.2.2.2)
:
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)
:
∃ z ∈ minimalSuperSet 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 x → ∀ y ∈ minimalSuperSet 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 : ∀ x ∈ T, x.IsComplete)
(h10 :
∀ (q10 : { x : 𝓩 // x ∈ S10 }),
Multiset.filter (fun (y : Charges 𝓩) => y ∉ T ∧ 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 𝓩) => y ∉ T ∧ 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 ∈ T → ∀ y ∈ minimalSuperSet S5 S10 x, y ∉ T → ¬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 : ∀ x ∈ T, 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 𝓩) => y ∉ T ∧ 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 𝓩) => y ∉ T ∧ 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)
:
y ∉ T → ¬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 : ∀ x ∈ T, 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 𝓩) => y ∉ T ∧ 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 𝓩) => y ∉ T ∧ p y)
(Multiset.map (fun (x : Charges 𝓩) => (x.1, x.2.1, insert (↑q5) x.2.2.1, x.2.2.2)) 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
.