Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.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 Mathlib.Data.Finset.Powerset
public import Mathlib.Data.Finset.Prod
public import Mathlib.Data.Finset.Sort
public import Mathlib.Data.Finset.Option

Charge Spectrum

i. Overview

In this module we define the charge spectrum of a SU(5) SUSY GUT theory with additional charges (usually U(1)) valued in 𝓩 satisfying the condition of:

The optional existence of a Hd particle in the bar 5 representation.

The optional existence of a Hu particle in the 5 representation.

The optional existence of matter in the bar 5 representation.

The optional existence of matter in the 10 representation.

The charge spectrum contains the information of the unique charges of each type of particle present in theory. Importantly, the charge spectrum does not contain information about the multiplicity of those charges.

With just the charge spectrum of the theory it is possible to put a number of constraints on the theory, most notably phenomenological constraints.

By keeping the presence of Hd and Hu optional, we can define a number of useful properties of the charge spectrum, which can help in searching for viable theories.

ii. Key results

ChargeSpectrum 𝓩 : The type of charge spectra with charges of type 𝓩, which is usually ℤ.

iii. Table of contents

A. The definition of the charge spectrum

A.1. Extensionality properties

A.2. Relation to products

A.3. Rendering

B. The subset relation

C. The empty charge spectrum

D. The cardinality of a charge spectrum

E. The power set of a charge spectrum

F. Finite sets of charge spectra with values

F.1. Cardinality of finite sets of charge spectra with values

iv. References

There are no known references for charge spectra in the literature. They were created specifically for the purpose of Physlib.

@[expose] public section

A. The definition of the charge spectrum

The type such that an element corresponds to the collection of charges associated with the matter content of the theory. The order of charges is implicitly taken to be qHd, qHu, Q5, Q10.

The Q5 and Q10 charges are represented by Finset rather than Multiset, so multiplicity is not included.

This is defined for a general type 𝓩, which could be e.g.

ℤ in the case of U(1),

ℤ × ℤ in the case of U(1) × U(1),

Fin 2 in the case of ℤ₂ etc.

The charge of the Hd particle.

The negative of the charge of the Hu particle. That is to say, the charge of the Hu when considered in the 5-bar representation.

The finite set of charges of the matter fields in the Q5 representation.

The finite set of charges of the matter fields in the Q10 representation.

              structure ChargeSpectrum (𝓩 : Type := ℤ) where  qHd : Option 𝓩  qHu : Option 𝓩  Q5 : Finset 𝓩  Q10 : Finset 𝓩

A.1. Extensionality properties

We prove extensionality properties for ChargeSpectrum 𝓩, that is conditions of when two elements of ChargeSpectrum 𝓩 are equal. We also show that when 𝓩 has decidable equality, so does ChargeSpectrum 𝓩.

              lemma eq_of_parts {x y : ChargeSpectrum 𝓩} (h1 : x.qHd = y.qHd) (h2 : x.qHu = y.qHu)
    (h3 : x.Q5 = y.Q5) (h4 : x.Q10 = y.Q10) : x = y := by𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h1:x.qHd = y.qHdh2:x.qHu = y.qHuh3:x.Q5 = y.Q5h4:x.Q10 = y.Q10⊢ x = y
  cases xmk𝓩:Typey:ChargeSpectrum 𝓩qHd✝:Option 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩h1:{ qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd = y.qHdh2:{ qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHu = y.qHuh3:{ qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5 = y.Q5h4:{ qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10 = y.Q10⊢ { qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ } = y
  cases ymk.mk𝓩:TypeqHd✝¹:Option 𝓩qHu✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHd✝:Option 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩h1:{ qHd := qHd✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd = { qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHdh2:{ qHd := qHd✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu = { qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHuh3:{ qHd := qHd✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 = { qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5h4:{ qHd := qHd✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 = { qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊢ { qHd := qHd✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ } = { qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }
  simp_allAll goals completed! 🐙lemma eq_iff {x y : ChargeSpectrum 𝓩} :
    x = y ↔ x.qHd = y.qHd ∧ x.qHu = y.qHu ∧ x.Q5 = y.Q5 ∧ x.Q10 = y.Q10 :=
  ⟨fun h => ⟨congrArg qHd h, congrArg qHu h, congrArg Q5 h, congrArg Q10 h⟩,
    fun ⟨h1, h2, h3, h4⟩ => eq_of_parts h1 h2 h3 h4⟩instance [DecidableEq 𝓩] : DecidableEq (ChargeSpectrum 𝓩) := fun _ _ =>
  decidable_of_iff _ eq_iff.symm

A.2. Relation to products

We show that ChargeSpectrum 𝓩 is equivalent to the product Option 𝓩 × Option 𝓩 × Finset 𝓩 × Fin 𝓩.

In an old implementation this was definitionally true, it is not so now.

The explicit casting of a term of type Charges 𝓩 to a term of Option 𝓩 × Option 𝓩 × Finset 𝓩 × Finset 𝓩.

def toProd : ChargeSpectrum 𝓩 ≃ Option 𝓩 × Option 𝓩 × Finset 𝓩 × Finset 𝓩 where
  toFun x := (x.qHd, x.qHu, x.Q5, x.Q10)
  invFun x := ⟨x.1, x.2.1, x.2.2.1, x.2.2.2⟩
  left_inv x := by𝓩:Typex:ChargeSpectrum 𝓩⊢ (fun x => { qHd := x.1, qHu := x.2.1, Q5 := x.2.2.1, Q10 := x.2.2.2 }) ((fun x => (x.qHd, x.qHu, x.Q5, x.Q10)) x) = x cases xmk𝓩:TypeqHd✝:Option 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩⊢ (fun x => { qHd := x.1, qHu := x.2.1, Q5 := x.2.2.1, Q10 := x.2.2.2 })
    ((fun x => (x.qHd, x.qHu, x.Q5, x.Q10)) { qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }) =
  { qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }; rflAll goals completed! 🐙
  right_inv x := by𝓩:Typex:Option 𝓩 × Option 𝓩 × Finset 𝓩 × Finset 𝓩⊢ (fun x => (x.qHd, x.qHu, x.Q5, x.Q10)) ((fun x => { qHd := x.1, qHu := x.2.1, Q5 := x.2.2.1, Q10 := x.2.2.2 }) x) = x cases xmk𝓩:Typefst✝:Option 𝓩snd✝:Option 𝓩 × Finset 𝓩 × Finset 𝓩⊢ (fun x => (x.qHd, x.qHu, x.Q5, x.Q10))
    ((fun x => { qHd := x.1, qHu := x.2.1, Q5 := x.2.2.1, Q10 := x.2.2.2 }) (fst✝, snd✝)) =
  (fst✝, snd✝); rflAll goals completed! 🐙

A.3. Rendering

unsafe instance [Repr 𝓩] : Repr (ChargeSpectrum 𝓩) where
  reprPrec x _ := match x with
    | ⟨qHd, qHu, Q5, Q10⟩ =>
      let s1 := reprStr qHd
      let s2 := reprStr qHu
      let s5 := reprStr Q5
      let s10 := reprStr Q10
      s!"⟨{s1}, {s2}, {s5}, {s10}⟩"

B. The subset relation

We define a HasSubset and HasSSubset instance on ChargeSpectrum 𝓩.

              instance hasSubset : HasSubset (ChargeSpectrum 𝓩) where
  Subset x y :=
    x.qHd.toFinset ⊆ y.qHd.toFinset ∧
    x.qHu.toFinset ⊆ y.qHu.toFinset ∧
    x.Q5 ⊆ y.Q5 ∧
    x.Q10 ⊆ y.Q10instance hasSSubset : HasSSubset (ChargeSpectrum 𝓩) where
  SSubset x y := x ⊆ y ∧ x ≠ yinstance subsetDecidable [DecidableEq 𝓩] (x y : ChargeSpectrum 𝓩) : Decidable (x ⊆ y) :=
  instDecidableAndlemma subset_def {x y : ChargeSpectrum 𝓩} : x ⊆ y ↔ x.qHd.toFinset ⊆ y.qHd.toFinset ∧
    x.qHu.toFinset ⊆ y.qHu.toFinset ∧ x.Q5 ⊆ y.Q5 ∧ x.Q10 ⊆ y.Q10 := by𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩⊢ x ⊆ y ↔ x.qHd.toFinset ⊆ y.qHd.toFinset ∧ x.qHu.toFinset ⊆ y.qHu.toFinset ∧ x.Q5 ⊆ y.Q5 ∧ x.Q10 ⊆ y.Q10
  rflAll goals completed! 🐙@[simp, refl]
lemma subset_refl (x : ChargeSpectrum 𝓩) : x ⊆ x := ⟨by𝓩:Typex:ChargeSpectrum 𝓩⊢ x.qHd.toFinset ⊆ x.qHd.toFinset rflAll goals completed! 🐙, by𝓩:Typex:ChargeSpectrum 𝓩⊢ x.qHu.toFinset ⊆ x.qHu.toFinset rflAll goals completed! 🐙, by𝓩:Typex:ChargeSpectrum 𝓩⊢ x.Q5 ⊆ x.Q5 rflAll goals completed! 🐙, by𝓩:Typex:ChargeSpectrum 𝓩⊢ x.Q10 ⊆ x.Q10 rflAll goals completed! 🐙⟩lemma _root_.Option.toFinset_inj {x y : Option 𝓩} :
    x = y ↔ x.toFinset = y.toFinset := by𝓩:Typex:Option 𝓩y:Option 𝓩⊢ x = y ↔ x.toFinset = y.toFinset
  cases xnone𝓩:Typey:Option 𝓩⊢ none = y ↔ none.toFinset = y.toFinsetsome𝓩:Typey:Option 𝓩val✝:𝓩⊢ some val✝ = y ↔ (some val✝).toFinset = y.toFinset <;>none𝓩:Typey:Option 𝓩⊢ none = y ↔ none.toFinset = y.toFinsetsome𝓩:Typey:Option 𝓩val✝:𝓩⊢ some val✝ = y ↔ (some val✝).toFinset = y.toFinset cases ysome.none𝓩:Typeval✝:𝓩⊢ some val✝ = none ↔ (some val✝).toFinset = none.toFinsetsome.some𝓩:Typeval✝¹:𝓩val✝:𝓩⊢ some val✝¹ = some val✝ ↔ (some val✝¹).toFinset = (some val✝).toFinset <;>none.none𝓩:Type⊢ none = none ↔ none.toFinset = none.toFinsetnone.some𝓩:Typeval✝:𝓩⊢ none = some val✝ ↔ none.toFinset = (some val✝).toFinsetsome.none𝓩:Typeval✝:𝓩⊢ some val✝ = none ↔ (some val✝).toFinset = none.toFinsetsome.some𝓩:Typeval✝¹:𝓩val✝:𝓩⊢ some val✝¹ = some val✝ ↔ (some val✝¹).toFinset = (some val✝).toFinset simp [Option.toFinset]All goals completed! 🐙

lemma subset_trans {x y z : ChargeSpectrum 𝓩} (hxy : x ⊆ y) (hyz : y ⊆ z) : x ⊆ z := by𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩z:ChargeSpectrum 𝓩hxy:x ⊆ yhyz:y ⊆ z⊢ x ⊆ z
  rw [subset_def𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩z:ChargeSpectrum 𝓩hxy:x.qHd.toFinset ⊆ y.qHd.toFinset ∧ x.qHu.toFinset ⊆ y.qHu.toFinset ∧ x.Q5 ⊆ y.Q5 ∧ x.Q10 ⊆ y.Q10hyz:y.qHd.toFinset ⊆ z.qHd.toFinset ∧ y.qHu.toFinset ⊆ z.qHu.toFinset ∧ y.Q5 ⊆ z.Q5 ∧ y.Q10 ⊆ z.Q10⊢ x.qHd.toFinset ⊆ z.qHd.toFinset ∧ x.qHu.toFinset ⊆ z.qHu.toFinset ∧ x.Q5 ⊆ z.Q5 ∧ x.Q10 ⊆ z.Q10𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩z:ChargeSpectrum 𝓩hxy:x.qHd.toFinset ⊆ y.qHd.toFinset ∧ x.qHu.toFinset ⊆ y.qHu.toFinset ∧ x.Q5 ⊆ y.Q5 ∧ x.Q10 ⊆ y.Q10hyz:y.qHd.toFinset ⊆ z.qHd.toFinset ∧ y.qHu.toFinset ⊆ z.qHu.toFinset ∧ y.Q5 ⊆ z.Q5 ∧ y.Q10 ⊆ z.Q10⊢ x.qHd.toFinset ⊆ z.qHd.toFinset ∧ x.qHu.toFinset ⊆ z.qHu.toFinset ∧ x.Q5 ⊆ z.Q5 ∧ x.Q10 ⊆ z.Q10] at hxy hyz ⊢𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩z:ChargeSpectrum 𝓩hxy:x.qHd.toFinset ⊆ y.qHd.toFinset ∧ x.qHu.toFinset ⊆ y.qHu.toFinset ∧ x.Q5 ⊆ y.Q5 ∧ x.Q10 ⊆ y.Q10hyz:y.qHd.toFinset ⊆ z.qHd.toFinset ∧ y.qHu.toFinset ⊆ z.qHu.toFinset ∧ y.Q5 ⊆ z.Q5 ∧ y.Q10 ⊆ z.Q10⊢ x.qHd.toFinset ⊆ z.qHd.toFinset ∧ x.qHu.toFinset ⊆ z.qHu.toFinset ∧ x.Q5 ⊆ z.Q5 ∧ x.Q10 ⊆ z.Q10
  exact ⟨Finset.Subset.trans hxy.1 hyz.1, Finset.Subset.trans hxy.2.1 hyz.2.1,
    Finset.Subset.trans hxy.2.2.1 hyz.2.2.1, Finset.Subset.trans hxy.2.2.2 hyz.2.2.2⟩All goals completed! 🐙lemma subset_antisymm {x y : ChargeSpectrum 𝓩} (hxy : x ⊆ y) (hyx : y ⊆ x) : x = y :=
  eq_of_parts
    (Option.toFinset_inj.mpr (Finset.Subset.antisymm hxy.1 hyx.1))
    (Option.toFinset_inj.mpr (Finset.Subset.antisymm hxy.2.1 hyx.2.1))
    (Finset.Subset.antisymm hxy.2.2.1 hyx.2.2.1)
    (Finset.Subset.antisymm hxy.2.2.2 hyx.2.2.2)

C. The empty charge spectrum

              instance emptyInst : EmptyCollection (ChargeSpectrum 𝓩) where
  emptyCollection := ⟨none, none, {}, {}⟩lemma empty_eq : (∅ : ChargeSpectrum 𝓩) = ⟨none, none, {}, {}⟩ := rfl@[simp]
lemma empty_subset (x : ChargeSpectrum 𝓩) : ∅ ⊆ x := by𝓩:Typex:ChargeSpectrum 𝓩⊢ ∅ ⊆ x
  simp [Subset, empty_eq]All goals completed! 🐙@[simp]
lemma subset_of_empty_iff_empty {x : ChargeSpectrum 𝓩} :
    x ⊆ ∅ ↔ x = ∅ := by𝓩:Typex:ChargeSpectrum 𝓩⊢ x ⊆ ∅ ↔ x = ∅
  refine ⟨fun h => subset_antisymm h (empty_subset x), ?_⟩𝓩:Typex:ChargeSpectrum 𝓩⊢ x = ∅ → x ⊆ ∅
  rintro rfl𝓩:Type⊢ ∅ ⊆ ∅
  simpAll goals completed! 🐙@[simp]
lemma empty_qHd : (∅ : ChargeSpectrum 𝓩).qHd = none := by𝓩:Type⊢ ∅.qHd = none
  simp [empty_eq]All goals completed! 🐙@[simp]
lemma empty_qHu : (∅ : ChargeSpectrum 𝓩).qHu = none := by𝓩:Type⊢ ∅.qHu = none
  simp [empty_eq]All goals completed! 🐙@[simp]
lemma empty_Q5 : (∅ : ChargeSpectrum 𝓩).Q5 = ∅ := by𝓩:Type⊢ ∅.Q5 = ∅
  simp [empty_eq]All goals completed! 🐙@[simp]
lemma empty_Q10 : (∅ : ChargeSpectrum 𝓩).Q10 = ∅ := by𝓩:Type⊢ ∅.Q10 = ∅
  simp [empty_eq]All goals completed! 🐙

D. The cardinality of a charge spectrum

The cardinality of a Charges is defined to be the sum of the cardinalities of each of the underlying finite sets of charges, with Option ℤ turned to finsets.

def card (x : ChargeSpectrum 𝓩) : Nat :=
  x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card

              @[simp]
lemma card_empty : card (∅ : ChargeSpectrum 𝓩) = 0 := by𝓩:Type⊢ ∅.card = 0
  simp [card, empty_eq]All goals completed! 🐙lemma card_mono {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) : card x ≤ card y := by𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ y⊢ x.card ≤ y.card
  have h1 := Finset.card_le_card h.1𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yh1:x.qHd.toFinset.card ≤ y.qHd.toFinset.card⊢ x.card ≤ y.card
  have h2 := Finset.card_le_card h.2.1𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yh1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardh2:x.qHu.toFinset.card ≤ y.qHu.toFinset.card⊢ x.card ≤ y.card
  have h3 := Finset.card_le_card h.2.2.1𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yh1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardh2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardh3:x.Q5.card ≤ y.Q5.card⊢ x.card ≤ y.card
  have h4 := Finset.card_le_card h.2.2.2𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yh1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardh2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardh3:x.Q5.card ≤ y.Q5.cardh4:x.Q10.card ≤ y.Q10.card⊢ x.card ≤ y.card
  simp only [card]𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yh1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardh2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardh3:x.Q5.card ≤ y.Q5.cardh4:x.Q10.card ≤ y.Q10.card⊢ x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card ≤
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.card
  omegaAll goals completed! 🐙lemma eq_of_subset_card {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) (hcard : card x = card y) : x = y := by𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.card = y.card⊢ x = y
  simp only [card] at hcard𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.card⊢ x = y
  have c1 := Finset.card_le_card h.1𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.card⊢ x = y
  have c2 := Finset.card_le_card h.2.1𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.card⊢ x = y
  have c3 := Finset.card_le_card h.2.2.1𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.card⊢ x = y
  have c4 := Finset.card_le_card h.2.2.2𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ x = y
  refine eq_of_parts (Option.toFinset_inj.mpr ?_) (Option.toFinset_inj.mpr ?_) ?_ ?_refine_1𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ x.qHd.toFinset = y.qHd.toFinsetrefine_2𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ x.qHu.toFinset = y.qHu.toFinsetrefine_3𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ x.Q5 = y.Q5refine_4𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ x.Q10 = y.Q10
  ·refine_1𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ x.qHd.toFinset = y.qHd.toFinset exact Finset.eq_of_subset_of_card_le h.1 (by𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ y.qHd.toFinset.card ≤ x.qHd.toFinset.card omegaAll goals completed! 🐙)
  ·refine_2𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ x.qHu.toFinset = y.qHu.toFinset exact Finset.eq_of_subset_of_card_le h.2.1 (by𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ y.qHu.toFinset.card ≤ x.qHu.toFinset.card omegaAll goals completed! 🐙)
  ·refine_3𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ x.Q5 = y.Q5 exact Finset.eq_of_subset_of_card_le h.2.2.1 (by𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ y.Q5.card ≤ x.Q5.card omegaAll goals completed! 🐙)
  ·refine_4𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ x.Q10 = y.Q10 exact Finset.eq_of_subset_of_card_le h.2.2.2 (by𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhcard:x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card =
  y.qHu.toFinset.card + y.qHd.toFinset.card + y.Q5.card + y.Q10.cardc1:x.qHd.toFinset.card ≤ y.qHd.toFinset.cardc2:x.qHu.toFinset.card ≤ y.qHu.toFinset.cardc3:x.Q5.card ≤ y.Q5.cardc4:x.Q10.card ≤ y.Q10.card⊢ y.Q10.card ≤ x.Q10.card omegaAll goals completed! 🐙)

E. The power set of a charge spectrum

The powerset of x : Option 𝓩 defined as {none} if x is none and {none, some y} is x is some y.

def _root_.Option.powerset (x : Option 𝓩) : Finset (Option 𝓩) :=
  match x with
  | none => {none}
  | some x => {none, some x}

@[simp]
lemma _root_.Option.mem_powerset_iff {x : Option 𝓩} (y : Option 𝓩) :
    y ∈ x.powerset ↔ y.toFinset ⊆ x.toFinset := by𝓩:Typeinst✝:DecidableEq 𝓩x:Option 𝓩y:Option 𝓩⊢ y ∈ x.powerset ↔ y.toFinset ⊆ x.toFinset
  cases xnone𝓩:Typeinst✝:DecidableEq 𝓩y:Option 𝓩⊢ y ∈ none.powerset ↔ y.toFinset ⊆ none.toFinsetsome𝓩:Typeinst✝:DecidableEq 𝓩y:Option 𝓩val✝:𝓩⊢ y ∈ (some val✝).powerset ↔ y.toFinset ⊆ (some val✝).toFinset <;>none𝓩:Typeinst✝:DecidableEq 𝓩y:Option 𝓩⊢ y ∈ none.powerset ↔ y.toFinset ⊆ none.toFinsetsome𝓩:Typeinst✝:DecidableEq 𝓩y:Option 𝓩val✝:𝓩⊢ y ∈ (some val✝).powerset ↔ y.toFinset ⊆ (some val✝).toFinset cases ysome.none𝓩:Typeinst✝:DecidableEq 𝓩val✝:𝓩⊢ none ∈ (some val✝).powerset ↔ none.toFinset ⊆ (some val✝).toFinsetsome.some𝓩:Typeinst✝:DecidableEq 𝓩val✝¹:𝓩val✝:𝓩⊢ some val✝ ∈ (some val✝¹).powerset ↔ (some val✝).toFinset ⊆ (some val✝¹).toFinset <;>none.none𝓩:Typeinst✝:DecidableEq 𝓩⊢ none ∈ none.powerset ↔ none.toFinset ⊆ none.toFinsetnone.some𝓩:Typeinst✝:DecidableEq 𝓩val✝:𝓩⊢ some val✝ ∈ none.powerset ↔ (some val✝).toFinset ⊆ none.toFinsetsome.none𝓩:Typeinst✝:DecidableEq 𝓩val✝:𝓩⊢ none ∈ (some val✝).powerset ↔ none.toFinset ⊆ (some val✝).toFinsetsome.some𝓩:Typeinst✝:DecidableEq 𝓩val✝¹:𝓩val✝:𝓩⊢ some val✝ ∈ (some val✝¹).powerset ↔ (some val✝).toFinset ⊆ (some val✝¹).toFinset simp [Option.powerset]All goals completed! 🐙

The powerset of a charge . Given a charge x : Charges it's powerset is the finite set of all Charges which are subsets of x.

def powerset (x : ChargeSpectrum 𝓩) : Finset (ChargeSpectrum 𝓩) :=
  (x.qHd.powerset.product <| x.qHu.powerset.product <| x.Q5.powerset.product <|
    x.Q10.powerset).map toProd.symm.toEmbedding

              lemma mem_powerset_iff {x y : ChargeSpectrum 𝓩} :
    x ∈ powerset y ↔
    x.qHd ∈ y.qHd.powerset ∧
    x.qHu ∈ y.qHu.powerset ∧
    x.Q5 ∈ y.Q5.powerset ∧
    x.Q10 ∈ y.Q10.powerset := by𝓩:Typeinst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩⊢ x ∈ y.powerset ↔ x.qHd ∈ y.qHd.powerset ∧ x.qHu ∈ y.qHu.powerset ∧ x.Q5 ∈ y.Q5.powerset ∧ x.Q10 ∈ y.Q10.powerset
  simp [powerset, Finset.mem_product, toProd]All goals completed! 🐙@[simp]
lemma mem_powerset_iff_subset {x y : ChargeSpectrum 𝓩} :
    x ∈ powerset y ↔ x ⊆ y := by𝓩:Typeinst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩⊢ x ∈ y.powerset ↔ x ⊆ y
  simp [mem_powerset_iff, subset_def]All goals completed! 🐙lemma self_mem_powerset (x : ChargeSpectrum 𝓩) :
    x ∈ powerset x := by𝓩:Typeinst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩⊢ x ∈ x.powerset simpAll goals completed! 🐙lemma empty_mem_powerset (x : ChargeSpectrum 𝓩) :
    ∅ ∈ powerset x := by𝓩:Typeinst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩⊢ ∅ ∈ x.powerset simpAll goals completed! 🐙@[simp]
lemma powerset_of_empty :
    powerset (∅ : ChargeSpectrum 𝓩) = {∅} := by𝓩:Typeinst✝:DecidableEq 𝓩⊢ ∅.powerset = {∅}
  ext x𝓩:Typeinst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩⊢ x ∈ ∅.powerset ↔ x ∈ {∅}
  simpAll goals completed! 🐙lemma powerset_mono {x y : ChargeSpectrum 𝓩} :
    powerset x ⊆ powerset y ↔ x ⊆ y := by𝓩:Typeinst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩⊢ x.powerset ⊆ y.powerset ↔ x ⊆ y
  constructormp𝓩:Typeinst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩⊢ x.powerset ⊆ y.powerset → x ⊆ ympr𝓩:Typeinst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩⊢ x ⊆ y → x.powerset ⊆ y.powerset
  ·mp𝓩:Typeinst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩⊢ x.powerset ⊆ y.powerset → x ⊆ y intro hmp𝓩:Typeinst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.powerset ⊆ y.powerset⊢ x ⊆ y
    exact mem_powerset_iff_subset.mp (h (self_mem_powerset x))All goals completed! 🐙
  ·mpr𝓩:Typeinst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩⊢ x ⊆ y → x.powerset ⊆ y.powerset intro h z hzmpr𝓩:Typeinst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yz:ChargeSpectrum 𝓩hz:z ∈ x.powerset⊢ z ∈ y.powerset
    exact mem_powerset_iff_subset.mpr (subset_trans (mem_powerset_iff_subset.mp hz) h)All goals completed! 🐙-- `unusedArguments` (newly flagged under v4.32.0): `hn` names the induction
-- target but the proof discharges it directly via `exists_min_image`.
@[nolint unusedArguments]
lemma min_exists_inductive (S : Finset (ChargeSpectrum 𝓩)) (hS : S ≠ ∅) :
    (n : ℕ) → (hn : S.card = n) →
    ∃ y ∈ S, powerset y ∩ S = {y} := by𝓩:Typeinst✝:DecidableEq 𝓩S:Finset (ChargeSpectrum 𝓩)hS:S ≠ ∅⊢ ∀ (n : ℕ), S.card = n → ∃ y ∈ S, y.powerset ∩ S = {y}
  intro _ _𝓩:Typeinst✝:DecidableEq 𝓩S:Finset (ChargeSpectrum 𝓩)hS:S ≠ ∅n✝:ℕhn✝:S.card = n✝⊢ ∃ y ∈ S, y.powerset ∩ S = {y}
  obtain ⟨y, hyS, hy⟩ := S.exists_min_image card (Finset.nonempty_iff_ne_empty.mpr hS)𝓩:Typeinst✝:DecidableEq 𝓩S:Finset (ChargeSpectrum 𝓩)hS:S ≠ ∅n✝:ℕhn✝:S.card = n✝y:ChargeSpectrum 𝓩hyS:y ∈ Shy:∀ x' ∈ S, y.card ≤ x'.card⊢ ∃ y ∈ S, y.powerset ∩ S = {y}
  refine ⟨y, hyS, ?_⟩𝓩:Typeinst✝:DecidableEq 𝓩S:Finset (ChargeSpectrum 𝓩)hS:S ≠ ∅n✝:ℕhn✝:S.card = n✝y:ChargeSpectrum 𝓩hyS:y ∈ Shy:∀ x' ∈ S, y.card ≤ x'.card⊢ y.powerset ∩ S = {y}
  ext z𝓩:Typeinst✝:DecidableEq 𝓩S:Finset (ChargeSpectrum 𝓩)hS:S ≠ ∅n✝:ℕhn✝:S.card = n✝y:ChargeSpectrum 𝓩hyS:y ∈ Shy:∀ x' ∈ S, y.card ≤ x'.cardz:ChargeSpectrum 𝓩⊢ z ∈ y.powerset ∩ S ↔ z ∈ {y}
  simp only [Finset.mem_inter, mem_powerset_iff_subset, Finset.mem_singleton]𝓩:Typeinst✝:DecidableEq 𝓩S:Finset (ChargeSpectrum 𝓩)hS:S ≠ ∅n✝:ℕhn✝:S.card = n✝y:ChargeSpectrum 𝓩hyS:y ∈ Shy:∀ x' ∈ S, y.card ≤ x'.cardz:ChargeSpectrum 𝓩⊢ z ⊆ y ∧ z ∈ S ↔ z = y
  constructormp𝓩:Typeinst✝:DecidableEq 𝓩S:Finset (ChargeSpectrum 𝓩)hS:S ≠ ∅n✝:ℕhn✝:S.card = n✝y:ChargeSpectrum 𝓩hyS:y ∈ Shy:∀ x' ∈ S, y.card ≤ x'.cardz:ChargeSpectrum 𝓩⊢ z ⊆ y ∧ z ∈ S → z = ympr𝓩:Typeinst✝:DecidableEq 𝓩S:Finset (ChargeSpectrum 𝓩)hS:S ≠ ∅n✝:ℕhn✝:S.card = n✝y:ChargeSpectrum 𝓩hyS:y ∈ Shy:∀ x' ∈ S, y.card ≤ x'.cardz:ChargeSpectrum 𝓩⊢ z = y → z ⊆ y ∧ z ∈ S
  ·mp𝓩:Typeinst✝:DecidableEq 𝓩S:Finset (ChargeSpectrum 𝓩)hS:S ≠ ∅n✝:ℕhn✝:S.card = n✝y:ChargeSpectrum 𝓩hyS:y ∈ Shy:∀ x' ∈ S, y.card ≤ x'.cardz:ChargeSpectrum 𝓩⊢ z ⊆ y ∧ z ∈ S → z = y rintro ⟨hzy, hzS⟩mp𝓩:Typeinst✝:DecidableEq 𝓩S:Finset (ChargeSpectrum 𝓩)hS:S ≠ ∅n✝:ℕhn✝:S.card = n✝y:ChargeSpectrum 𝓩hyS:y ∈ Shy:∀ x' ∈ S, y.card ≤ x'.cardz:ChargeSpectrum 𝓩hzy:z ⊆ yhzS:z ∈ S⊢ z = y
    exact eq_of_subset_card hzy (le_antisymm (card_mono hzy) (hy z hzS))All goals completed! 🐙
  ·mpr𝓩:Typeinst✝:DecidableEq 𝓩S:Finset (ChargeSpectrum 𝓩)hS:S ≠ ∅n✝:ℕhn✝:S.card = n✝y:ChargeSpectrum 𝓩hyS:y ∈ Shy:∀ x' ∈ S, y.card ≤ x'.cardz:ChargeSpectrum 𝓩⊢ z = y → z ⊆ y ∧ z ∈ S rintro rflmpr𝓩:Typeinst✝:DecidableEq 𝓩S:Finset (ChargeSpectrum 𝓩)hS:S ≠ ∅n✝:ℕhn✝:S.card = n✝z:ChargeSpectrum 𝓩hyS:z ∈ Shy:∀ x' ∈ S, z.card ≤ x'.card⊢ z ⊆ z ∧ z ∈ S
    exact ⟨subset_refl z, hyS⟩All goals completed! 🐙lemma min_exists (S : Finset (ChargeSpectrum 𝓩)) (hS : S ≠ ∅) :
    ∃ y ∈ S, powerset y ∩ S = {y} := min_exists_inductive S hS S.card rfl

F. Finite sets of charge spectra with values

We define the finite set of ChargeSpectrum with 5-bar and 10d representation charges in a given finite set.

Given S5 S10 : Finset 𝓩 the finite set of charges associated with for which the 5-bar representation charges sit in S5 and the 10d representation charges sit in S10.

def ofFinset (S5 S10 : Finset 𝓩) : Finset (ChargeSpectrum 𝓩) :=
  let SqHd := {none} ∪ S5.map ⟨Option.some, Option.some_injective 𝓩⟩
  let SqHu := {none} ∪ S5.map ⟨Option.some, Option.some_injective 𝓩⟩
  let SQ5 := S5.powerset
  let SQ10 := S10.powerset
  (SqHd.product (SqHu.product (SQ5.product SQ10))).map toProd.symm.toEmbedding

              

lemma mem_ofFinset_iff {S5 S10 : Finset 𝓩} {x : ChargeSpectrum 𝓩} :
    x ∈ ofFinset S5 S10 ↔ x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧
      x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10 := by𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩⊢ x ∈ ofFinset S5 S10 ↔ x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧ x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10
  have hoption (a : Option 𝓩) (S : Finset 𝓩) :
      a ∈ ({none} : Finset (Option 𝓩)) ∪ S.map ⟨Option.some, Option.some_injective 𝓩⟩ ↔
      a.toFinset ⊆ S := by cases anone𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩S:Finset 𝓩⊢ none ∈ {none} ∪ Finset.map { toFun := some, inj' := ⋯ } S ↔ none.toFinset ⊆ Ssome𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩S:Finset 𝓩val✝:𝓩⊢ some val✝ ∈ {none} ∪ Finset.map { toFun := some, inj' := ⋯ } S ↔ (some val✝).toFinset ⊆ S𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hoption:∀ (a : Option 𝓩) (S : Finset 𝓩), a ∈ {none} ∪ Finset.map { toFun := some, inj' := ⋯ } S ↔ a.toFinset ⊆ S⊢ x ∈ ofFinset S5 S10 ↔ x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧ x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10 <;>none𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩S:Finset 𝓩⊢ none ∈ {none} ∪ Finset.map { toFun := some, inj' := ⋯ } S ↔ none.toFinset ⊆ Ssome𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩S:Finset 𝓩val✝:𝓩⊢ some val✝ ∈ {none} ∪ Finset.map { toFun := some, inj' := ⋯ } S ↔ (some val✝).toFinset ⊆ S𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hoption:∀ (a : Option 𝓩) (S : Finset 𝓩), a ∈ {none} ∪ Finset.map { toFun := some, inj' := ⋯ } S ↔ a.toFinset ⊆ S⊢ x ∈ ofFinset S5 S10 ↔ x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧ x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10 simp𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hoption:∀ (a : Option 𝓩) (S : Finset 𝓩), a ∈ {none} ∪ Finset.map { toFun := some, inj' := ⋯ } S ↔ a.toFinset ⊆ S⊢ x ∈ ofFinset S5 S10 ↔ x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧ x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hoption:∀ (a : Option 𝓩) (S : Finset 𝓩), a ∈ {none} ∪ Finset.map { toFun := some, inj' := ⋯ } S ↔ a.toFinset ⊆ S⊢ x ∈ ofFinset S5 S10 ↔ x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧ x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10
  simp only [ofFinset, Finset.mem_map_equiv, Equiv.symm_symm, toProd, Equiv.coe_fn_mk,
    Finset.product_eq_sprod, Finset.mem_product, hoption, Finset.mem_powerset]All goals completed! 🐙

lemma mem_ofFinset_antitone (S5 S10 : Finset 𝓩)
    {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) (hy : y ∈ ofFinset S5 S10) :
    x ∈ ofFinset S5 S10 := by𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhy:y ∈ ofFinset S5 S10⊢ x ∈ ofFinset S5 S10
  rw [mem_ofFinset_iff𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhy:y.qHd.toFinset ⊆ S5 ∧ y.qHu.toFinset ⊆ S5 ∧ y.Q5 ⊆ S5 ∧ y.Q10 ⊆ S10⊢ x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧ x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhy:y.qHd.toFinset ⊆ S5 ∧ y.qHu.toFinset ⊆ S5 ∧ y.Q5 ⊆ S5 ∧ y.Q10 ⊆ S10⊢ x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧ x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10] at hy ⊢𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yhy:y.qHd.toFinset ⊆ S5 ∧ y.qHu.toFinset ⊆ S5 ∧ y.Q5 ⊆ S5 ∧ y.Q10 ⊆ S10⊢ x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧ x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10
  exact ⟨h.1.trans hy.1, h.2.1.trans hy.2.1, h.2.2.1.trans hy.2.2.1, h.2.2.2.trans hy.2.2.2⟩All goals completed! 🐙

lemma ofFinset_subset_of_subset {S5 S5' S10 S10' : Finset 𝓩}
    (h5 : S5 ⊆ S5') (h10 : S10 ⊆ S10') :
    ofFinset S5 S10 ⊆ ofFinset S5' S10' := by𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S5':Finset 𝓩S10:Finset 𝓩S10':Finset 𝓩h5:S5 ⊆ S5'h10:S10 ⊆ S10'⊢ ofFinset S5 S10 ⊆ ofFinset S5' S10'
  intro x hx𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S5':Finset 𝓩S10:Finset 𝓩S10':Finset 𝓩h5:S5 ⊆ S5'h10:S10 ⊆ S10'x:ChargeSpectrum 𝓩hx:x ∈ ofFinset S5 S10⊢ x ∈ ofFinset S5' S10'
  rw [mem_ofFinset_iff𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S5':Finset 𝓩S10:Finset 𝓩S10':Finset 𝓩h5:S5 ⊆ S5'h10:S10 ⊆ S10'x:ChargeSpectrum 𝓩hx:x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧ x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10⊢ x.qHd.toFinset ⊆ S5' ∧ x.qHu.toFinset ⊆ S5' ∧ x.Q5 ⊆ S5' ∧ x.Q10 ⊆ S10'𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S5':Finset 𝓩S10:Finset 𝓩S10':Finset 𝓩h5:S5 ⊆ S5'h10:S10 ⊆ S10'x:ChargeSpectrum 𝓩hx:x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧ x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10⊢ x.qHd.toFinset ⊆ S5' ∧ x.qHu.toFinset ⊆ S5' ∧ x.Q5 ⊆ S5' ∧ x.Q10 ⊆ S10'] at hx ⊢𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S5':Finset 𝓩S10:Finset 𝓩S10':Finset 𝓩h5:S5 ⊆ S5'h10:S10 ⊆ S10'x:ChargeSpectrum 𝓩hx:x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧ x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10⊢ x.qHd.toFinset ⊆ S5' ∧ x.qHu.toFinset ⊆ S5' ∧ x.Q5 ⊆ S5' ∧ x.Q10 ⊆ S10'
  exact ⟨hx.1.trans h5, hx.2.1.trans h5, hx.2.2.1.trans h5, hx.2.2.2.trans h10⟩All goals completed! 🐙

lemma ofFinset_univ [Fintype 𝓩] (x : ChargeSpectrum 𝓩) :
    x ∈ ofFinset (Finset.univ : Finset 𝓩) (Finset.univ : Finset 𝓩) := by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:Fintype 𝓩x:ChargeSpectrum 𝓩⊢ x ∈ ofFinset Finset.univ Finset.univ
  rw [mem_ofFinset_iff𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:Fintype 𝓩x:ChargeSpectrum 𝓩⊢ x.qHd.toFinset ⊆ Finset.univ ∧ x.qHu.toFinset ⊆ Finset.univ ∧ x.Q5 ⊆ Finset.univ ∧ x.Q10 ⊆ Finset.univ𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:Fintype 𝓩x:ChargeSpectrum 𝓩⊢ x.qHd.toFinset ⊆ Finset.univ ∧ x.qHu.toFinset ⊆ Finset.univ ∧ x.Q5 ⊆ Finset.univ ∧ x.Q10 ⊆ Finset.univ]𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:Fintype 𝓩x:ChargeSpectrum 𝓩⊢ x.qHd.toFinset ⊆ Finset.univ ∧ x.qHu.toFinset ⊆ Finset.univ ∧ x.Q5 ⊆ Finset.univ ∧ x.Q10 ⊆ Finset.univ
  simpAll goals completed! 🐙

F.1. Cardinality of finite sets of charge spectra with values

The cardinality of ofFinset S5 S10.

def ofFinsetCard (S5 S10 : Finset 𝓩) : ℕ :=
    (S5.card + 1) * (S5.card + 1) * (2 ^ S5.card : ℕ) * (2 ^ S10.card : ℕ)

lemma ofFinset_card_eq_ofFinsetCard (S5 S10 : Finset 𝓩) :
    (ofFinset S5 S10).card = ofFinsetCard S5 S10 := by𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩⊢ (ofFinset S5 S10).card = ofFinsetCard S5 S10
  simp [ofFinset, Finset.card_map, Finset.card_product, Finset.card_powerset, ofFinsetCard]𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩⊢ (S5.card + 1) * ((S5.card + 1) * (2 ^ S5.card * 2 ^ S10.card)) =
  (S5.card + 1) * (S5.card + 1) * 2 ^ S5.card * 2 ^ S10.card
  grindAll goals completed! 🐙