Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.Basic

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm

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

MinimallyAllowsTerm : Predicate on charge spectra which is true if the charge spectrum minimally allows a potential term.

allowsTerm_iff_subset_minimallyAllowsTerm : A charge spectrum which allows a term has a subset which minimally allows the term, and vice versa.

eq_allowsTermForm_of_minimallyAllowsTerm : Any charge spectrum which minimally allows a term is of the form allowsTermForm a b c T for some a b c : 𝓩.

iii. Table of contents

A. Charge spectra which minimally allow potential terms

A.1. Decidability of MinimallyAllowsTerm

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

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

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

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

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

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

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

B. Relation between MinimallyAllowsTerm and allowsTermForm

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

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

iv. References

There are no known references for this material.

@[expose] public section

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.

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.

def MinimallyAllowsTerm (x : ChargeSpectrum 𝓩) (T : PotentialTerm) : Prop :=
  ∀ y ∈ x.powerset, y = x ↔ y.AllowsTerm T

A.1. Decidability of `MinimallyAllowsTerm`

We show that MinimallyAllowsTerm is decidable.

instance (x : ChargeSpectrum 𝓩) (T : PotentialTerm) : Decidable (x.MinimallyAllowsTerm T) :=
  inferInstanceAs (Decidable (∀ y ∈ powerset x, y = x ↔ y.AllowsTerm T))

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.

lemma allowsTerm_of_minimallyAllowsTerm (h : x.MinimallyAllowsTerm T) : x.AllowsTerm T := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x.MinimallyAllowsTerm T⊢ x.AllowsTerm T
  simp only [MinimallyAllowsTerm] at h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:∀ y ∈ x.powerset, y = x ↔ y.AllowsTerm T⊢ x.AllowsTerm T
  simpa using h x (self_mem_powerset x)All goals completed! 🐙

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.

lemma allowsTerm_of_has_minimallyAllowsTerm_subset
    (hx : ∃ y ∈ powerset x, y.MinimallyAllowsTerm T) : x.AllowsTerm T := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:∃ y ∈ x.powerset, y.MinimallyAllowsTerm T⊢ x.AllowsTerm T
  obtain ⟨y, hy⟩ := hx𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ∈ x.powerset ∧ y.MinimallyAllowsTerm T⊢ x.AllowsTerm T
  simp only [mem_powerset_iff_subset] at hy𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ x ∧ y.MinimallyAllowsTerm T⊢ x.AllowsTerm T
  apply allowsTerm_mono hy.1𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ x ∧ y.MinimallyAllowsTerm T⊢ y.AllowsTerm T
  exact allowsTerm_of_minimallyAllowsTerm hy.2All goals completed! 🐙

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.



lemma minimallyAllowsTerm_iff_powerset_filter_eq :
    x.MinimallyAllowsTerm T ↔ x.powerset.filter (fun y => y.AllowsTerm T) = {x} := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ x.MinimallyAllowsTerm T ↔ {y ∈ x.powerset | y.AllowsTerm T} = {x}
  constructormp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ x.MinimallyAllowsTerm T → {y ∈ x.powerset | y.AllowsTerm T} = {x}mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x} → x.MinimallyAllowsTerm T
  ·mp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ x.MinimallyAllowsTerm T → {y ∈ x.powerset | y.AllowsTerm T} = {x} intro hmp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x.MinimallyAllowsTerm T⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
    ext ymp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x.MinimallyAllowsTerm Ty:ChargeSpectrum 𝓩⊢ y ∈ {y ∈ x.powerset | y.AllowsTerm T} ↔ y ∈ {x}
    simp only [Finset.mem_filter, mem_powerset_iff_subset, Finset.mem_singleton]mp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x.MinimallyAllowsTerm Ty:ChargeSpectrum 𝓩⊢ y ⊆ x ∧ y.AllowsTerm T ↔ y = x
    simp [MinimallyAllowsTerm] at hmp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:∀ y ⊆ x, y = x ↔ y.AllowsTerm T⊢ y ⊆ x ∧ y.AllowsTerm T ↔ y = x
    constructormp.mp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:∀ y ⊆ x, y = x ↔ y.AllowsTerm T⊢ y ⊆ x ∧ y.AllowsTerm T → y = xmp.mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:∀ y ⊆ x, y = x ↔ y.AllowsTerm T⊢ y = x → y ⊆ x ∧ y.AllowsTerm T
    ·mp.mp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:∀ y ⊆ x, y = x ↔ y.AllowsTerm T⊢ y ⊆ x ∧ y.AllowsTerm T → y = x exact fun ⟨h1, h2⟩ => (h y h1).mpr h2All goals completed! 🐙
    ·mp.mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:∀ y ⊆ x, y = x ↔ y.AllowsTerm T⊢ y = x → y ⊆ x ∧ y.AllowsTerm T intro h1mp.mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:∀ y ⊆ x, y = x ↔ y.AllowsTerm Th1:y = x⊢ y ⊆ x ∧ y.AllowsTerm T
      subst h1mp.mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermy:ChargeSpectrum 𝓩h:∀ y_1 ⊆ y, y_1 = y ↔ y_1.AllowsTerm T⊢ y ⊆ y ∧ y.AllowsTerm T
      simpmp.mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermy:ChargeSpectrum 𝓩h:∀ y_1 ⊆ y, y_1 = y ↔ y_1.AllowsTerm T⊢ y.AllowsTerm T
      exact (h y (by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermy:ChargeSpectrum 𝓩h:∀ y_1 ⊆ y, y_1 = y ↔ y_1.AllowsTerm T⊢ y ⊆ y simpAll goals completed! 🐙)).mp rfl
  ·mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x} → x.MinimallyAllowsTerm T intro hmpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}⊢ x.MinimallyAllowsTerm T
    simp [MinimallyAllowsTerm]mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}⊢ ∀ y ⊆ x, y = x ↔ y.AllowsTerm T
    intro y hympr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}y:ChargeSpectrum 𝓩hy:y ⊆ x⊢ y = x ↔ y.AllowsTerm T
    rw [Finset.eq_singleton_iff_unique_memmpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x ∈ {y ∈ x.powerset | y.AllowsTerm T} ∧ ∀ x_1 ∈ {y ∈ x.powerset | y.AllowsTerm T}, x_1 = xy:ChargeSpectrum 𝓩hy:y ⊆ x⊢ y = x ↔ y.AllowsTerm Tmpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x ∈ {y ∈ x.powerset | y.AllowsTerm T} ∧ ∀ x_1 ∈ {y ∈ x.powerset | y.AllowsTerm T}, x_1 = xy:ChargeSpectrum 𝓩hy:y ⊆ x⊢ y = x ↔ y.AllowsTerm T] at hmpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x ∈ {y ∈ x.powerset | y.AllowsTerm T} ∧ ∀ x_1 ∈ {y ∈ x.powerset | y.AllowsTerm T}, x_1 = xy:ChargeSpectrum 𝓩hy:y ⊆ x⊢ y = x ↔ y.AllowsTerm T
    simp at hmpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ xh:x.AllowsTerm T ∧ ∀ x_1 ⊆ x, x_1.AllowsTerm T → x_1 = x⊢ y = x ↔ y.AllowsTerm T
    constructormpr.mp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ xh:x.AllowsTerm T ∧ ∀ x_1 ⊆ x, x_1.AllowsTerm T → x_1 = x⊢ y = x → y.AllowsTerm Tmpr.mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ xh:x.AllowsTerm T ∧ ∀ x_1 ⊆ x, x_1.AllowsTerm T → x_1 = x⊢ y.AllowsTerm T → y = x
    ·mpr.mp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ xh:x.AllowsTerm T ∧ ∀ x_1 ⊆ x, x_1.AllowsTerm T → x_1 = x⊢ y = x → y.AllowsTerm T intro h1mpr.mp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ xh:x.AllowsTerm T ∧ ∀ x_1 ⊆ x, x_1.AllowsTerm T → x_1 = xh1:y = x⊢ y.AllowsTerm T
      subst h1mpr.mp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermy:ChargeSpectrum 𝓩hy:y ⊆ yh:y.AllowsTerm T ∧ ∀ x ⊆ y, x.AllowsTerm T → x = y⊢ y.AllowsTerm T
      exact h.1All goals completed! 🐙
    ·mpr.mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ xh:x.AllowsTerm T ∧ ∀ x_1 ⊆ x, x_1.AllowsTerm T → x_1 = x⊢ y.AllowsTerm T → y = x intro h1mpr.mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ xh:x.AllowsTerm T ∧ ∀ x_1 ⊆ x, x_1.AllowsTerm T → x_1 = xh1:y.AllowsTerm T⊢ y = x
      apply h.2mpr.mpr.a𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ xh:x.AllowsTerm T ∧ ∀ x_1 ⊆ x, x_1.AllowsTerm T → x_1 = xh1:y.AllowsTerm T⊢ y ⊆ xmpr.mpr.a𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ xh:x.AllowsTerm T ∧ ∀ x_1 ⊆ x, x_1.AllowsTerm T → x_1 = xh1:y.AllowsTerm T⊢ y.AllowsTerm T
      ·mpr.mpr.a𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ xh:x.AllowsTerm T ∧ ∀ x_1 ⊆ x, x_1.AllowsTerm T → x_1 = xh1:y.AllowsTerm T⊢ y ⊆ x exact hyAll goals completed! 🐙
      ·mpr.mpr.a𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ⊆ xh:x.AllowsTerm T ∧ ∀ x_1 ⊆ x, x_1.AllowsTerm T → x_1 = xh1:y.AllowsTerm T⊢ y.AllowsTerm T exact h1All goals completed! 🐙

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.



lemma minimallyAllowsTerm_iff_powerset_countP_eq_one :
    x.MinimallyAllowsTerm T ↔ x.powerset.val.countP (fun y => y.AllowsTerm T) = 1 := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ x.MinimallyAllowsTerm T ↔ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1
  rw [minimallyAllowsTerm_iff_powerset_filter_eq𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x} ↔ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x} ↔ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1]𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x} ↔ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1
  constructormp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x} → Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1 → {y ∈ x.powerset | y.AllowsTerm T} = {x}
  ·mp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x} → Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1 intro hmp𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}⊢ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1
    trans (Finset.filter (fun y => y.AllowsTerm T) x.powerset).card𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}⊢ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = {y ∈ x.powerset | y.AllowsTerm T}.card𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}⊢ {y ∈ x.powerset | y.AllowsTerm T}.card = 1
    ·𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}⊢ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = {y ∈ x.powerset | y.AllowsTerm T}.card change _ = (Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val).card𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}⊢ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val =
  (Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val).card
      exact Multiset.countP_eq_card_filter (fun y => y.AllowsTerm T) x.powerset.valAll goals completed! 🐙
    ·𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}⊢ {y ∈ x.powerset | y.AllowsTerm T}.card = 1 rw [h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}⊢ {x}.card = 1𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}⊢ {x}.card = 1]𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}⊢ {x}.card = 1
      simpAll goals completed! 🐙
  ·mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1 → {y ∈ x.powerset | y.AllowsTerm T} = {x} intro hmpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
    have h1 : (Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val).card = 1 := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ x.MinimallyAllowsTerm T ↔ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1h1:(Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val).card = 1⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
      rw [← h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1⊢ (Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val).card =
  Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1⊢ (Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val).card =
  Multiset.countP (fun y => y.AllowsTerm T) x.powerset.valmpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1h1:(Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val).card = 1⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}]𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1⊢ (Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val).card =
  Multiset.countP (fun y => y.AllowsTerm T) x.powerset.valmpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1h1:(Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val).card = 1⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
      exact Eq.symm (Multiset.countP_eq_card_filter (fun y => y.AllowsTerm T) x.powerset.val)mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1h1:(Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val).card = 1⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1h1:(Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val).card = 1⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
    rw [Multiset.card_eq_onempr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1h1:∃ a, Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1h1:∃ a, Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}] at h1mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1h1:∃ a, Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
    obtain ⟨a, ha⟩ := h1mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1a:ChargeSpectrum 𝓩ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
    have haMem : a ∈ Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ x.MinimallyAllowsTerm T ↔ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1a:ChargeSpectrum 𝓩ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}haMem:a ∈ Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
      simp [ha]mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1a:ChargeSpectrum 𝓩ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}haMem:a ∈ Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1a:ChargeSpectrum 𝓩ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}haMem:a ∈ Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
    simp at haMemmpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1a:ChargeSpectrum 𝓩ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}haMem:a ⊆ x ∧ a.AllowsTerm T⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
    have hxMem : x ∈ Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩⊢ x.MinimallyAllowsTerm T ↔ Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1a:ChargeSpectrum 𝓩ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}haMem:a ⊆ x ∧ a.AllowsTerm ThxMem:x ∈ Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
      simpa using allowsTerm_mono haMem.1 haMem.2mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1a:ChargeSpectrum 𝓩ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}haMem:a ⊆ x ∧ a.AllowsTerm ThxMem:x ∈ Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1a:ChargeSpectrum 𝓩ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}haMem:a ⊆ x ∧ a.AllowsTerm ThxMem:x ∈ Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
    rw [hampr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1a:ChargeSpectrum 𝓩ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}haMem:a ⊆ x ∧ a.AllowsTerm ThxMem:x ∈ {a}⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}mpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1a:ChargeSpectrum 𝓩ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}haMem:a ⊆ x ∧ a.AllowsTerm ThxMem:x ∈ {a}⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}] at hxMemmpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1a:ChargeSpectrum 𝓩ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}haMem:a ⊆ x ∧ a.AllowsTerm ThxMem:x ∈ {a}⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
    simp at hxMemmpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1a:ChargeSpectrum 𝓩ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {a}haMem:a ⊆ x ∧ a.AllowsTerm ThxMem:x = a⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
    subst hxMemmpr𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:Multiset.countP (fun y => y.AllowsTerm T) x.powerset.val = 1ha:Multiset.filter (fun y => y.AllowsTerm T) x.powerset.val = {x}haMem:x ⊆ x ∧ x.AllowsTerm T⊢ {y ∈ x.powerset | y.AllowsTerm T} = {x}
    exact Finset.val_inj.mp haAll goals completed! 🐙

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.



lemma subset_minimallyAllowsTerm_of_allowsTerm
    (hx : x.AllowsTerm T) : ∃ y ∈ powerset x, y.MinimallyAllowsTerm T := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm T⊢ ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T
  have hPresent : (x.powerset.filter (fun y => y.AllowsTerm T)) ≠ ∅ := by
    rw [← @Finset.nonempty_iff_ne_empty𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm T⊢ {y ∈ x.powerset | y.AllowsTerm T}.Nonempty𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm T⊢ {y ∈ x.powerset | y.AllowsTerm T}.Nonempty𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm ThPresent:{y ∈ x.powerset | y.AllowsTerm T} ≠ ∅⊢ ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T]𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm T⊢ {y ∈ x.powerset | y.AllowsTerm T}.Nonempty𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm ThPresent:{y ∈ x.powerset | y.AllowsTerm T} ≠ ∅⊢ ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T
    use xh𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm T⊢ x ∈ {y ∈ x.powerset | y.AllowsTerm T}𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm ThPresent:{y ∈ x.powerset | y.AllowsTerm T} ≠ ∅⊢ ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T
    simp [hx]𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm ThPresent:{y ∈ x.powerset | y.AllowsTerm T} ≠ ∅⊢ ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm ThPresent:{y ∈ x.powerset | y.AllowsTerm T} ≠ ∅⊢ ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T
  obtain ⟨y, h1, h2⟩ := min_exists (x.powerset.filter (fun y => y.AllowsTerm T)) hPresent𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm ThPresent:{y ∈ x.powerset | y.AllowsTerm T} ≠ ∅y:ChargeSpectrum 𝓩h1:y ∈ {y ∈ x.powerset | y.AllowsTerm T}h2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}⊢ ∃ y ∈ x.powerset, y.MinimallyAllowsTerm T
  use yh𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm ThPresent:{y ∈ x.powerset | y.AllowsTerm T} ≠ ∅y:ChargeSpectrum 𝓩h1:y ∈ {y ∈ x.powerset | y.AllowsTerm T}h2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}⊢ y ∈ x.powerset ∧ y.MinimallyAllowsTerm T
  simp at h1h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm ThPresent:{y ∈ x.powerset | y.AllowsTerm T} ≠ ∅y:ChargeSpectrum 𝓩h2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}h1:y ⊆ x ∧ y.AllowsTerm T⊢ y ∈ x.powerset ∧ y.MinimallyAllowsTerm T
  simp_allh𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm Ty:ChargeSpectrum 𝓩hPresent:∃ x_1 ⊆ x, x_1.AllowsTerm Th2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}h1:y ⊆ x ∧ y.AllowsTerm T⊢ y.MinimallyAllowsTerm T
  rw [minimallyAllowsTerm_iff_powerset_filter_eqh𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm Ty:ChargeSpectrum 𝓩hPresent:∃ x_1 ⊆ x, x_1.AllowsTerm Th2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}h1:y ⊆ x ∧ y.AllowsTerm T⊢ {y ∈ y.powerset | y.AllowsTerm T} = {y}h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm Ty:ChargeSpectrum 𝓩hPresent:∃ x_1 ⊆ x, x_1.AllowsTerm Th2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}h1:y ⊆ x ∧ y.AllowsTerm T⊢ {y ∈ y.powerset | y.AllowsTerm T} = {y}]h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm Ty:ChargeSpectrum 𝓩hPresent:∃ x_1 ⊆ x, x_1.AllowsTerm Th2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}h1:y ⊆ x ∧ y.AllowsTerm T⊢ {y ∈ y.powerset | y.AllowsTerm T} = {y}
  rw [← h2h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm Ty:ChargeSpectrum 𝓩hPresent:∃ x_1 ⊆ x, x_1.AllowsTerm Th2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}h1:y ⊆ x ∧ y.AllowsTerm T⊢ {y ∈ y.powerset | y.AllowsTerm T} = y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T}h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm Ty:ChargeSpectrum 𝓩hPresent:∃ x_1 ⊆ x, x_1.AllowsTerm Th2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}h1:y ⊆ x ∧ y.AllowsTerm T⊢ {y ∈ y.powerset | y.AllowsTerm T} = y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T}]h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm Ty:ChargeSpectrum 𝓩hPresent:∃ x_1 ⊆ x, x_1.AllowsTerm Th2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}h1:y ⊆ x ∧ y.AllowsTerm T⊢ {y ∈ y.powerset | y.AllowsTerm T} = y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T}
  ext zh𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm Ty:ChargeSpectrum 𝓩hPresent:∃ x_1 ⊆ x, x_1.AllowsTerm Th2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}h1:y ⊆ x ∧ y.AllowsTerm Tz:ChargeSpectrum 𝓩⊢ z ∈ {y ∈ y.powerset | y.AllowsTerm T} ↔ z ∈ y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T}
  simp only [Finset.mem_filter, mem_powerset_iff_subset, Finset.mem_inter, and_congr_right_iff,
    iff_and_self]h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm Ty:ChargeSpectrum 𝓩hPresent:∃ x_1 ⊆ x, x_1.AllowsTerm Th2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}h1:y ⊆ x ∧ y.AllowsTerm Tz:ChargeSpectrum 𝓩⊢ z ⊆ y → z.AllowsTerm T → z ⊆ x
  intro hzy hzpresh𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩hx:x.AllowsTerm Ty:ChargeSpectrum 𝓩hPresent:∃ x_1 ⊆ x, x_1.AllowsTerm Th2:y.powerset ∩ {y ∈ x.powerset | y.AllowsTerm T} = {y}h1:y ⊆ x ∧ y.AllowsTerm Tz:ChargeSpectrum 𝓩hzy:z ⊆ yhzpres:z.AllowsTerm T⊢ z ⊆ x
  exact subset_trans hzy h1.1All goals completed! 🐙

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.

lemma allowsTerm_iff_subset_minimallyAllowsTerm :
    x.AllowsTerm T ↔ ∃ y ∈ powerset x, y.MinimallyAllowsTerm T :=
  ⟨fun h => subset_minimallyAllowsTerm_of_allowsTerm h, fun h =>
    allowsTerm_of_has_minimallyAllowsTerm_subset h⟩

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.



lemma card_le_degree_of_minimallyAllowsTerm (h : x.MinimallyAllowsTerm T) :
    x.card ≤ T.degree := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x.MinimallyAllowsTerm T⊢ x.card ≤ T.degree
  obtain ⟨y, y_mem_power, y_card,y_present⟩ :=
    subset_card_le_degree_allowsTerm_of_allowsTerm (allowsTerm_of_minimallyAllowsTerm h)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x.MinimallyAllowsTerm Ty:ChargeSpectrum 𝓩y_mem_power:y ∈ x.powersety_card:y.card ≤ T.degreey_present:y.AllowsTerm T⊢ x.card ≤ T.degree
  have hy : y ∈ x.powerset.filter (fun y => y.AllowsTerm T) := by
    simp_all𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x.MinimallyAllowsTerm Ty:ChargeSpectrum 𝓩y_mem_power:y ∈ x.powersety_card:y.card ≤ T.degreey_present:y.AllowsTerm Thy:y ∈ {y ∈ x.powerset | y.AllowsTerm T}⊢ x.card ≤ T.degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x.MinimallyAllowsTerm Ty:ChargeSpectrum 𝓩y_mem_power:y ∈ x.powersety_card:y.card ≤ T.degreey_present:y.AllowsTerm Thy:y ∈ {y ∈ x.powerset | y.AllowsTerm T}⊢ x.card ≤ T.degree
  rw [minimallyAllowsTerm_iff_powerset_filter_eq𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}y:ChargeSpectrum 𝓩y_mem_power:y ∈ x.powersety_card:y.card ≤ T.degreey_present:y.AllowsTerm Thy:y ∈ {y ∈ x.powerset | y.AllowsTerm T}⊢ x.card ≤ T.degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}y:ChargeSpectrum 𝓩y_mem_power:y ∈ x.powersety_card:y.card ≤ T.degreey_present:y.AllowsTerm Thy:y ∈ {y ∈ x.powerset | y.AllowsTerm T}⊢ x.card ≤ T.degree] at h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}y:ChargeSpectrum 𝓩y_mem_power:y ∈ x.powersety_card:y.card ≤ T.degreey_present:y.AllowsTerm Thy:y ∈ {y ∈ x.powerset | y.AllowsTerm T}⊢ x.card ≤ T.degree
  rw [h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}y:ChargeSpectrum 𝓩y_mem_power:y ∈ x.powersety_card:y.card ≤ T.degreey_present:y.AllowsTerm Thy:y ∈ {x}⊢ x.card ≤ T.degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}y:ChargeSpectrum 𝓩y_mem_power:y ∈ x.powersety_card:y.card ≤ T.degreey_present:y.AllowsTerm Thy:y ∈ {x}⊢ x.card ≤ T.degree] at hy𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}y:ChargeSpectrum 𝓩y_mem_power:y ∈ x.powersety_card:y.card ≤ T.degreey_present:y.AllowsTerm Thy:y ∈ {x}⊢ x.card ≤ T.degree
  simp at hy𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:{y ∈ x.powerset | y.AllowsTerm T} = {x}y:ChargeSpectrum 𝓩y_mem_power:y ∈ x.powersety_card:y.card ≤ T.degreey_present:y.AllowsTerm Thy:y = x⊢ x.card ≤ T.degree
  subst hy𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermy:ChargeSpectrum 𝓩y_card:y.card ≤ T.degreey_present:y.AllowsTerm Th:{y ∈ y.powerset | y.AllowsTerm T} = {y}y_mem_power:y ∈ y.powerset⊢ y.card ≤ T.degree
  exact y_cardAll goals completed! 🐙

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 : 𝓩.



lemma eq_allowsTermForm_of_minimallyAllowsTerm (h1 : x.MinimallyAllowsTerm T) :
    ∃ a b c, x = allowsTermForm a b c T := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:x.MinimallyAllowsTerm T⊢ ∃ a b c, x = allowsTermForm a b c T
  obtain ⟨a, b, c, h2, h3⟩ := allowsTermForm_subset_allowsTerm_of_allowsTerm
    (allowsTerm_of_minimallyAllowsTerm h1)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:x.MinimallyAllowsTerm Ta:𝓩b:𝓩c:𝓩h2:allowsTermForm a b c T ⊆ xh3:(allowsTermForm a b c T).AllowsTerm T⊢ ∃ a b c, x = allowsTermForm a b c T
  use a, b, ch𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:x.MinimallyAllowsTerm Ta:𝓩b:𝓩c:𝓩h2:allowsTermForm a b c T ⊆ xh3:(allowsTermForm a b c T).AllowsTerm T⊢ x = allowsTermForm a b c T
  have hy : allowsTermForm a b c T ∈ x.powerset.filter (fun y => y.AllowsTerm T) := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:x.MinimallyAllowsTerm T⊢ ∃ a b c, x = allowsTermForm a b c Th𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:x.MinimallyAllowsTerm Ta:𝓩b:𝓩c:𝓩h2:allowsTermForm a b c T ⊆ xh3:(allowsTermForm a b c T).AllowsTerm Thy:allowsTermForm a b c T ∈ {y ∈ x.powerset | y.AllowsTerm T}⊢ x = allowsTermForm a b c T
    simp_allh𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:x.MinimallyAllowsTerm Ta:𝓩b:𝓩c:𝓩h2:allowsTermForm a b c T ⊆ xh3:(allowsTermForm a b c T).AllowsTerm Thy:allowsTermForm a b c T ∈ {y ∈ x.powerset | y.AllowsTerm T}⊢ x = allowsTermForm a b c Th𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:x.MinimallyAllowsTerm Ta:𝓩b:𝓩c:𝓩h2:allowsTermForm a b c T ⊆ xh3:(allowsTermForm a b c T).AllowsTerm Thy:allowsTermForm a b c T ∈ {y ∈ x.powerset | y.AllowsTerm T}⊢ x = allowsTermForm a b c T
  rw [minimallyAllowsTerm_iff_powerset_filter_eqh𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:{y ∈ x.powerset | y.AllowsTerm T} = {x}a:𝓩b:𝓩c:𝓩h2:allowsTermForm a b c T ⊆ xh3:(allowsTermForm a b c T).AllowsTerm Thy:allowsTermForm a b c T ∈ {y ∈ x.powerset | y.AllowsTerm T}⊢ x = allowsTermForm a b c Th𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:{y ∈ x.powerset | y.AllowsTerm T} = {x}a:𝓩b:𝓩c:𝓩h2:allowsTermForm a b c T ⊆ xh3:(allowsTermForm a b c T).AllowsTerm Thy:allowsTermForm a b c T ∈ {y ∈ x.powerset | y.AllowsTerm T}⊢ x = allowsTermForm a b c T] at h1h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:{y ∈ x.powerset | y.AllowsTerm T} = {x}a:𝓩b:𝓩c:𝓩h2:allowsTermForm a b c T ⊆ xh3:(allowsTermForm a b c T).AllowsTerm Thy:allowsTermForm a b c T ∈ {y ∈ x.powerset | y.AllowsTerm T}⊢ x = allowsTermForm a b c T
  rw [h1h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:{y ∈ x.powerset | y.AllowsTerm T} = {x}a:𝓩b:𝓩c:𝓩h2:allowsTermForm a b c T ⊆ xh3:(allowsTermForm a b c T).AllowsTerm Thy:allowsTermForm a b c T ∈ {x}⊢ x = allowsTermForm a b c Th𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:{y ∈ x.powerset | y.AllowsTerm T} = {x}a:𝓩b:𝓩c:𝓩h2:allowsTermForm a b c T ⊆ xh3:(allowsTermForm a b c T).AllowsTerm Thy:allowsTermForm a b c T ∈ {x}⊢ x = allowsTermForm a b c T] at hyh𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:{y ∈ x.powerset | y.AllowsTerm T} = {x}a:𝓩b:𝓩c:𝓩h2:allowsTermForm a b c T ⊆ xh3:(allowsTermForm a b c T).AllowsTerm Thy:allowsTermForm a b c T ∈ {x}⊢ x = allowsTermForm a b c T
  simp at hyh𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h1:{y ∈ x.powerset | y.AllowsTerm T} = {x}a:𝓩b:𝓩c:𝓩h2:allowsTermForm a b c T ⊆ xh3:(allowsTermForm a b c T).AllowsTerm Thy:allowsTermForm a b c T = x⊢ x = allowsTermForm a b c T
  exact hy.symmAll goals completed! 🐙

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.

Charge spectrum which minimally allows terms

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. Charge spectra which minimally allow potential terms

A.1. Decidability of MinimallyAllowsTerm

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

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

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

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

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

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

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

B. Relation between MinimallyAllowsTerm and allowsTermForm

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

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

A.1. Decidability of `MinimallyAllowsTerm`

B. Relation between `MinimallyAllowsTerm` and `allowsTermForm`

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

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