1. Physlib
  2. Particles
  3. SuperSymmetry
  4. SU5
  5. ChargeSpectrum
  6. MinimalSuperSet
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.Completions

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.

@[expose] public section

A. The minimal super set

We define the minimal super set.

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.

def minimalSuperSet (S5 S10 : Finset 𝓩) (x : ChargeSpectrum 𝓩) : Finset (ChargeSpectrum 𝓩) := let SqHd := if x.qHd.isSome then ∅ else S5.map ⟨fun y => ⟨some y, x.qHu, x.Q5, x.Q10⟩, 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩⊢ Function.Injective fun y => { qHd := some y, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 } 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y1:𝓩y2:𝓩⊢ (fun y => { qHd := some y, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }) y1 = (fun y => { qHd := some y, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }) y2 → y1 = y2; All goals completed! 🐙⟩ let SqHu := if x.qHu.isSome then ∅ else S5.image fun y => ⟨x.qHd, some y, x.Q5, x.Q10⟩ let SQ5 := (S5 \ x.Q5).image (fun y => ⟨x.qHd, x.qHu, insert y x.Q5, x.Q10⟩) let SQ10 := (S10 \ x.Q10).image (fun y => ⟨x.qHd, x.qHu, x.Q5, insert y x.Q10⟩) (SqHd ∪ SqHu ∪ SQ5 ∪ SQ10).erase x

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.

𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩qHd✝:Option 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10:Finset 𝓩a:𝓩ha:a ∈ S10 ∧ a ∉ Q10hy1:¬{ qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := insert a Q10 } = { qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10 }⊢ hasSubset.1 { qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10 } { qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := insert a Q10 } All goals completed! 🐙

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] lemma self_not_mem_minimalSuperSet (S5 S10 : Finset 𝓩) (x : ChargeSpectrum 𝓩) : x ∉ minimalSuperSet S5 S10 x := 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩⊢ x ∉ minimalSuperSet S5 S10 x All goals completed! 🐙lemma self_ne_mem_minimalSuperSet (S5 S10 : Finset 𝓩) (x y : ChargeSpectrum 𝓩) (hy : y ∈ minimalSuperSet S5 S10 x) : x ≠ y := 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ∈ minimalSuperSet S5 S10 x⊢ x ≠ y 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:y ∈ minimalSuperSet S5 S10 xh:x = y⊢ False 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hy:x ∈ minimalSuperSet S5 S10 x⊢ False All goals completed! 🐙

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.

𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩qHd✝:Option 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10:Finset 𝓩a:𝓩ha:a ∈ S10 ∧ a ∉ Q10hy1:¬{ qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10 } = { qHd := qHd✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10 }h:a ∈ Q10⊢ False All goals completed! 🐙

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.

lemma insert_Q5_mem_minimalSuperSet {S5 S10 : Finset 𝓩} {x : ChargeSpectrum 𝓩} (z : 𝓩) (hz : z ∈ S5) (hznot : z ∉ x.Q5) : ⟨x.qHd, x.qHu, insert z x.Q5, x.Q10⟩ ∈ minimalSuperSet S5 S10 x := 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S5hznot:z ∉ x.Q5⊢ { qHd := x.qHd, qHu := x.qHu, Q5 := insert z x.Q5, Q10 := x.Q10 } ∈ minimalSuperSet S5 S10 x 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S5hznot:z ∉ x.Q5⊢ ¬{ qHd := x.qHd, qHu := x.qHu, Q5 := insert z x.Q5, Q10 := x.Q10 } = x ∧ (({ qHd := x.qHd, qHu := x.qHu, Q5 := insert z x.Q5, Q10 := x.Q10 } ∈ if x.qHd.isSome = true then ∅ else Finset.map { toFun := fun y => { qHd := some y, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }, inj' := ⋯ } S5) ∨ ({ qHd := x.qHd, qHu := x.qHu, Q5 := insert z x.Q5, Q10 := x.Q10 } ∈ if x.qHu.isSome = true then ∅ else Finset.image (fun y => { qHd := x.qHd, qHu := some y, Q5 := x.Q5, Q10 := x.Q10 }) S5) ∨ (∃ a, (a ∈ S5 ∧ a ∉ x.Q5) ∧ insert a x.Q5 = insert z x.Q5) ∨ ∃ a, (a ∈ S10 ∧ a ∉ x.Q10) ∧ x.Q5 = insert z x.Q5 ∧ a ∈ x.Q10) match x with 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S5qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5⊢ ¬{ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } = { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 } ∧ (({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd.isSome = true then ∅ else Finset.map { toFun := fun y => { qHd := some y, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }, inj' := ⋯ } S5) ∨ ({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu.isSome = true then ∅ else Finset.image (fun y => { qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := some y, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }) S5) ∨ (∃ a, (a ∈ S5 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∧ insert a { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∨ ∃ a, (a ∈ S10 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ∧ a ∈ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S5qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5⊢ ¬{ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } = { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S5qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5⊢ ({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd.isSome = true then ∅ else Finset.map { toFun := fun y => { qHd := some y, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }, inj' := ⋯ } S5) ∨ ({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu.isSome = true then ∅ else Finset.image (fun y => { qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := some y, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }) S5) ∨ (∃ a, (a ∈ S5 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∧ insert a { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∨ ∃ a, (a ∈ S10 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ∧ a ∈ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S5qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5⊢ ¬{ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } = { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 } All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S5qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5⊢ ({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd.isSome = true then ∅ else Finset.map { toFun := fun y => { qHd := some y, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }, inj' := ⋯ } S5) ∨ ({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu.isSome = true then ∅ else Finset.image (fun y => { qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := some y, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }) S5) ∨ (∃ a, (a ∈ S5 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∧ insert a { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∨ ∃ a, (a ∈ S10 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ∧ a ∈ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S5qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5⊢ ({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu.isSome = true then ∅ else Finset.image (fun y => { qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := some y, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }) S5) ∨ (∃ a, (a ∈ S5 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∧ insert a { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∨ ∃ a, (a ∈ S10 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ∧ a ∈ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S5qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5⊢ (∃ a, (a ∈ S5 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∧ insert a { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∨ ∃ a, (a ∈ S10 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ∧ a ∈ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S5qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5⊢ ∃ a, (a ∈ S5 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∧ insert a { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 All goals completed! 🐙lemma insert_Q10_mem_minimalSuperSet {S5 S10 : Finset 𝓩} {x : ChargeSpectrum 𝓩} (z : 𝓩) (hz : z ∈ S10) (hznot : z ∉ x.Q10) : ⟨x.qHd, x.qHu, x.Q5, insert z x.Q10⟩ ∈ minimalSuperSet S5 S10 x := 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S10hznot:z ∉ x.Q10⊢ { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert z x.Q10 } ∈ minimalSuperSet S5 S10 x 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S10hznot:z ∉ x.Q10⊢ ¬{ qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert z x.Q10 } = x ∧ (({ qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert z x.Q10 } ∈ if x.qHd.isSome = true then ∅ else Finset.map { toFun := fun y => { qHd := some y, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }, inj' := ⋯ } S5) ∨ ({ qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert z x.Q10 } ∈ if x.qHu.isSome = true then ∅ else Finset.image (fun y => { qHd := x.qHd, qHu := some y, Q5 := x.Q5, Q10 := x.Q10 }) S5) ∨ (∃ a, (a ∈ S5 ∧ a ∉ x.Q5) ∧ a ∈ x.Q5 ∧ x.Q10 = insert z x.Q10) ∨ ∃ a, (a ∈ S10 ∧ a ∉ x.Q10) ∧ insert a x.Q10 = insert z x.Q10) match x with 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S10qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10⊢ ¬{ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } = { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 } ∧ (({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd.isSome = true then ∅ else Finset.map { toFun := fun y => { qHd := some y, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }, inj' := ⋯ } S5) ∨ ({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu.isSome = true then ∅ else Finset.image (fun y => { qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := some y, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }) S5) ∨ (∃ a, (a ∈ S5 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∧ a ∈ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∨ ∃ a, (a ∈ S10 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∧ insert a { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S10qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10⊢ ¬{ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } = { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S10qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10⊢ ({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd.isSome = true then ∅ else Finset.map { toFun := fun y => { qHd := some y, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }, inj' := ⋯ } S5) ∨ ({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu.isSome = true then ∅ else Finset.image (fun y => { qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := some y, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }) S5) ∨ (∃ a, (a ∈ S5 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∧ a ∈ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∨ ∃ a, (a ∈ S10 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∧ insert a { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S10qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10⊢ ¬{ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } = { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 } All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S10qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10⊢ ({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd.isSome = true then ∅ else Finset.map { toFun := fun y => { qHd := some y, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }, inj' := ⋯ } S5) ∨ ({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu.isSome = true then ∅ else Finset.image (fun y => { qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := some y, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }) S5) ∨ (∃ a, (a ∈ S5 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∧ a ∈ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∨ ∃ a, (a ∈ S10 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∧ insert a { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S10qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10⊢ ({ qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 } ∈ if { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu.isSome = true then ∅ else Finset.image (fun y => { qHd := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd, qHu := some y, Q5 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5, Q10 := { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 }) S5) ∨ (∃ a, (a ∈ S5 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∧ a ∈ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∨ ∃ a, (a ∈ S10 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∧ insert a { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S10qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10⊢ (∃ a, (a ∈ S5 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5) ∧ a ∈ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∨ ∃ a, (a ∈ S10 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∧ insert a { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩z:𝓩hz:z ∈ S10qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩hznot:z ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10⊢ ∃ a, (a ∈ S10 ∧ a ∉ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10) ∧ insert a { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 = insert z { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 All goals completed! 🐙lemma some_qHd_mem_minimalSuperSet_of_none {S5 S10 : Finset 𝓩} {x2 : Option 𝓩 × Finset 𝓩 × Finset 𝓩} (z : 𝓩) (hz : z ∈ S5) : ⟨some z, x2.1, x2.2.1, x2.2.2⟩ ∈ minimalSuperSet S5 S10 ⟨none, x2.1, x2.2.1, x2.2.2⟩ := 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩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 } All goals completed! 🐙lemma some_qHu_mem_minimalSuperSet_of_none {S5 S10 : Finset 𝓩} {x1 : Option 𝓩} {x2 : Finset 𝓩 × Finset 𝓩} (z : 𝓩) (hz : z ∈ S5) : ⟨x1, some z, x2.1,x2.2⟩ ∈ minimalSuperSet S5 S10 ⟨x1, none, x2.1, x2.2⟩ := 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩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 } All goals completed! 🐙

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.

𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1✝:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y1✝:Option 𝓩y2✝:Option 𝓩x1:Option 𝓩y1:Option 𝓩y2:𝓩hxneqy:x1 = y1 → ¬none = some y2hy:y1.toFinset ⊆ S5 ∧ (some y2).toFinset ⊆ S5 ∧ x3 ⊆ S5 ∧ x4 ⊆ S10hsubset:x1.toFinset ⊆ y1.toFinseth0:{ qHd := x1, qHu := some y2, Q5 := (x3, x4).1, Q10 := (x3, x4).2 } ∈ minimalSuperSet S5 S10 { qHd := x1, qHu := none, Q5 := (x3, x4).1, Q10 := (x3, x4).2 }⊢ { qHd := x1, qHu := some y2, Q5 := x3, Q10 := x4 } ∈ minimalSuperSet S5 S10 { qHd := x1, qHu := none, Q5 := x3, Q10 := x4 } All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1✝:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y1✝:Option 𝓩y2✝:Option 𝓩x1:Option 𝓩y1:Option 𝓩y2:𝓩hxneqy:x1 = y1 → ¬none = some y2hy:y1.toFinset ⊆ S5 ∧ (some y2).toFinset ⊆ S5 ∧ x3 ⊆ S5 ∧ x4 ⊆ S10hsubset:x1.toFinset ⊆ y1.toFinset⊢ { qHd := x1, qHu := some y2, Q5 := x3, Q10 := x4 } ⊆ { qHd := y1, qHu := some y2, Q5 := x3, Q10 := x4 } All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y1:Option 𝓩y2:Option 𝓩hsubset:none.toFinset ⊆ none.toFinset ∧ none.toFinset ⊆ none.toFinsethxneqy:none = none → ¬none = nonehy:none.toFinset ⊆ S5 ∧ none.toFinset ⊆ S5 ∧ x3 ⊆ S5 ∧ x4 ⊆ S10⊢ ∃ z ∈ minimalSuperSet S5 S10 { qHd := none, qHu := none, Q5 := x3, Q10 := x4 }, z ⊆ { qHd := none, qHu := none, Q5 := x3, Q10 := x4 } All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1✝:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y1✝:Option 𝓩y2:Option 𝓩x1:𝓩y1:𝓩hsubset:(some x1).toFinset ⊆ (some y1).toFinset ∧ none.toFinset ⊆ none.toFinsethxneqy:some x1 = some y1 → ¬none = nonehy:(some y1).toFinset ⊆ S5 ∧ none.toFinset ⊆ S5 ∧ x3 ⊆ S5 ∧ x4 ⊆ S10⊢ ∃ z ∈ minimalSuperSet S5 S10 { qHd := some x1, qHu := none, Q5 := x3, Q10 := x4 }, z ⊆ { qHd := some y1, qHu := none, Q5 := x3, Q10 := x4 } All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2✝:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y1:Option 𝓩y2✝:Option 𝓩x2:𝓩y2:𝓩hsubset:none.toFinset ⊆ none.toFinset ∧ (some x2).toFinset ⊆ (some y2).toFinsethxneqy:none = none → ¬some x2 = some y2hy:none.toFinset ⊆ S5 ∧ (some y2).toFinset ⊆ S5 ∧ x3 ⊆ S5 ∧ x4 ⊆ S10⊢ ∃ z ∈ minimalSuperSet S5 S10 { qHd := none, qHu := some x2, Q5 := x3, Q10 := x4 }, z ⊆ { qHd := none, qHu := some y2, Q5 := x3, Q10 := x4 } All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1✝:Option 𝓩x2✝:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y1✝:Option 𝓩y2✝:Option 𝓩x1:𝓩y1:𝓩x2:𝓩y2:𝓩hsubset:(some x1).toFinset ⊆ (some y1).toFinset ∧ (some x2).toFinset ⊆ (some y2).toFinsethxneqy:some x1 = some y1 → ¬some x2 = some y2hy:(some y1).toFinset ⊆ S5 ∧ (some y2).toFinset ⊆ S5 ∧ x3 ⊆ S5 ∧ x4 ⊆ S10⊢ ∃ z ∈ minimalSuperSet S5 S10 { qHd := some x1, qHu := some x2, Q5 := x3, Q10 := x4 }, z ⊆ { qHd := some y1, qHu := some y2, Q5 := x3, Q10 := x4 } All goals completed! 🐙

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.

𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Prophp:∀ (x : ChargeSpectrum 𝓩), p x → ∀ y ∈ minimalSuperSet S5 S10 x, p yx:ChargeSpectrum 𝓩hbase:p xy:ChargeSpectrum 𝓩hy:y ∈ ofFinset S5 S10hsubset:x ⊆ yn:ℕhn:n.succ = y.card - x.cardhxy:x ≠ yz:ChargeSpectrum 𝓩hz:z ∈ minimalSuperSet S5 S10 xhsubsetz:z ⊆ y⊢ n = y.card - (x.card + 1) All goals completed! 🐙

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.

𝓩:Typeinst✝¹:DecidableEq 𝓩T:Multiset (ChargeSpectrum 𝓩)S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Propinst✝:DecidablePred phComplet:∀ x ∈ T, x.IsCompleteh10:∀ (q10 : ↥S10), Multiset.filter (fun y => y ∉ T ∧ p y) (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) T) = ∅h5:∀ (q5 : ↥S5), Multiset.filter (fun y => y ∉ T ∧ p y) (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) T) = ∅xqHu:Option 𝓩xQ5:Finset 𝓩xQ10:Finset 𝓩y:ChargeSpectrum 𝓩y_not_in_T:y ∉ TxqHd:𝓩x_mem_T:{ qHd := some xqHd, qHu := xqHu, Q5 := xQ5, Q10 := xQ10 } ∈ Ty_mem_minimalSuperSet:y ∈ minimalSuperSet S5 S10 { qHd := some xqHd, qHu := xqHu, Q5 := xQ5, Q10 := xQ10 }x_isComplete:{ qHd := some xqHd, qHu := xqHu, Q5 := xQ5, Q10 := xQ10 }.IsCompletexqHu_isSome:∃ a, xqHu = some a⊢ ¬p y 𝓩:Typeinst✝¹:DecidableEq 𝓩T:Multiset (ChargeSpectrum 𝓩)S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Propinst✝:DecidablePred phComplet:∀ x ∈ T, x.IsCompleteh10:∀ (q10 : ↥S10), Multiset.filter (fun y => y ∉ T ∧ p y) (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) T) = ∅h5:∀ (q5 : ↥S5), Multiset.filter (fun y => y ∉ T ∧ p y) (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) T) = ∅xQ5:Finset 𝓩xQ10:Finset 𝓩y:ChargeSpectrum 𝓩y_not_in_T:y ∉ TxqHd:𝓩xqHu:𝓩x_mem_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := xQ10 } ∈ Ty_mem_minimalSuperSet:y ∈ minimalSuperSet S5 S10 { qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := xQ10 }x_isComplete:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := xQ10 }.IsComplete⊢ ¬p y 𝓩:Typeinst✝¹:DecidableEq 𝓩T:Multiset (ChargeSpectrum 𝓩)S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Propinst✝:DecidablePred phComplet:∀ x ∈ T, x.IsCompleteh10:∀ (q10 : ↥S10), Multiset.filter (fun y => y ∉ T ∧ p y) (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) T) = ∅h5:∀ (q5 : ↥S5), Multiset.filter (fun y => y ∉ T ∧ p y) (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) T) = ∅xQ5:Finset 𝓩xQ10:Finset 𝓩y:ChargeSpectrum 𝓩y_not_in_T:y ∉ TxqHd:𝓩xqHu:𝓩x_mem_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := xQ10 } ∈ Tx_isComplete:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := xQ10 }.IsCompletey_mem_minimalSuperSet:(∃ a, (a ∈ S5 ∧ a ∉ xQ5) ∧ { qHd := some xqHd, qHu := some xqHu, Q5 := insert a xQ5, Q10 := xQ10 } = y) ∨ ∃ a, (a ∈ S10 ∧ a ∉ xQ10) ∧ { qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := insert a xQ10 } = y⊢ ¬p y 𝓩:Typeinst✝¹:DecidableEq 𝓩T:Multiset (ChargeSpectrum 𝓩)S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Propinst✝:DecidablePred phComplet:∀ x ∈ T, x.IsCompletexQ5:Finset 𝓩xQ10:Finset 𝓩y:ChargeSpectrum 𝓩xqHd:𝓩xqHu:𝓩h10:∀ a ∈ S10, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 }h5:∀ a ∈ S5, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 }y_not_in_T:y ∉ Tx_mem_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := xQ10 } ∈ Ty_mem_minimalSuperSet:(∃ a, (a ∈ S5 ∧ a ∉ xQ5) ∧ { qHd := some xqHd, qHu := some xqHu, Q5 := insert a xQ5, Q10 := xQ10 } = y) ∨ ∃ a, (a ∈ S10 ∧ a ∉ xQ10) ∧ { qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := insert a xQ10 } = y⊢ ¬p y 𝓩:Typeinst✝¹:DecidableEq 𝓩T:Multiset (ChargeSpectrum 𝓩)S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Propinst✝:DecidablePred phComplet:∀ x ∈ T, x.IsCompletexQ5:Finset 𝓩xQ10:Finset 𝓩xqHd:𝓩xqHu:𝓩h10:∀ a ∈ S10, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 }h5:∀ a ∈ S5, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 }x_mem_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := xQ10 } ∈ Tq5:𝓩q5_mem_S5:q5 ∈ S5 ∧ q5 ∉ xQ5y_not_in_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := insert q5 xQ5, Q10 := xQ10 } ∉ T⊢ ¬p { qHd := some xqHd, qHu := some xqHu, Q5 := insert q5 xQ5, Q10 := xQ10 }𝓩:Typeinst✝¹:DecidableEq 𝓩T:Multiset (ChargeSpectrum 𝓩)S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Propinst✝:DecidablePred phComplet:∀ x ∈ T, x.IsCompletexQ5:Finset 𝓩xQ10:Finset 𝓩xqHd:𝓩xqHu:𝓩h10:∀ a ∈ S10, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 }h5:∀ a ∈ S5, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 }x_mem_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := xQ10 } ∈ Tq10:𝓩q10_mem_S10:q10 ∈ S10 ∧ q10 ∉ xQ10y_not_in_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := insert q10 xQ10 } ∉ T⊢ ¬p { qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := insert q10 xQ10 } 𝓩:Typeinst✝¹:DecidableEq 𝓩T:Multiset (ChargeSpectrum 𝓩)S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Propinst✝:DecidablePred phComplet:∀ x ∈ T, x.IsCompletexQ5:Finset 𝓩xQ10:Finset 𝓩xqHd:𝓩xqHu:𝓩h10:∀ a ∈ S10, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 }h5:∀ a ∈ S5, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 }x_mem_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := xQ10 } ∈ Tq5:𝓩q5_mem_S5:q5 ∈ S5 ∧ q5 ∉ xQ5y_not_in_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := insert q5 xQ5, Q10 := xQ10 } ∉ T⊢ ¬p { qHd := some xqHd, qHu := some xqHu, Q5 := insert q5 xQ5, Q10 := xQ10 } 𝓩:Typeinst✝¹:DecidableEq 𝓩T:Multiset (ChargeSpectrum 𝓩)S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Propinst✝:DecidablePred phComplet:∀ x ∈ T, x.IsCompletexQ5:Finset 𝓩xQ10:Finset 𝓩xqHd:𝓩xqHu:𝓩h10:∀ a ∈ S10, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 }h5:∀ a ∈ S5, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 }x_mem_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := xQ10 } ∈ Tq5:𝓩q5_mem_S5:q5 ∈ S5 ∧ q5 ∉ xQ5y_not_in_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := insert q5 xQ5, Q10 := xQ10 } ∉ Th5':∀ a ∈ T, { qHd := a.qHd, qHu := a.qHu, Q5 := insert q5 a.Q5, Q10 := a.Q10 } ∉ T → ¬p { qHd := a.qHd, qHu := a.qHu, Q5 := insert q5 a.Q5, Q10 := a.Q10 }⊢ ¬p { qHd := some xqHd, qHu := some xqHu, Q5 := insert q5 xQ5, Q10 := xQ10 } All goals completed! 🐙 𝓩:Typeinst✝¹:DecidableEq 𝓩T:Multiset (ChargeSpectrum 𝓩)S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Propinst✝:DecidablePred phComplet:∀ x ∈ T, x.IsCompletexQ5:Finset 𝓩xQ10:Finset 𝓩xqHd:𝓩xqHu:𝓩h10:∀ a ∈ S10, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 }h5:∀ a ∈ S5, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 }x_mem_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := xQ10 } ∈ Tq10:𝓩q10_mem_S10:q10 ∈ S10 ∧ q10 ∉ xQ10y_not_in_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := insert q10 xQ10 } ∉ T⊢ ¬p { qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := insert q10 xQ10 } 𝓩:Typeinst✝¹:DecidableEq 𝓩T:Multiset (ChargeSpectrum 𝓩)S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Propinst✝:DecidablePred phComplet:∀ x ∈ T, x.IsCompletexQ5:Finset 𝓩xQ10:Finset 𝓩xqHd:𝓩xqHu:𝓩h10:∀ a ∈ S10, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := a_1.Q5, Q10 := insert a a_1.Q10 }h5:∀ a ∈ S5, ∀ a_1 ∈ T, { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 } ∉ T → ¬p { qHd := a_1.qHd, qHu := a_1.qHu, Q5 := insert a a_1.Q5, Q10 := a_1.Q10 }x_mem_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := xQ10 } ∈ Tq10:𝓩q10_mem_S10:q10 ∈ S10 ∧ q10 ∉ xQ10y_not_in_T:{ qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := insert q10 xQ10 } ∉ Th10':∀ a ∈ T, { qHd := a.qHd, qHu := a.qHu, Q5 := a.Q5, Q10 := insert q10 a.Q10 } ∉ T → ¬p { qHd := a.qHd, qHu := a.qHu, Q5 := a.Q5, Q10 := insert q10 a.Q10 }⊢ ¬p { qHd := some xqHd, qHu := some xqHu, Q5 := xQ5, Q10 := insert q10 xQ10 } All goals completed! 🐙

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.

𝓩:Typeinst✝¹:DecidableEq 𝓩T:Multiset (ChargeSpectrum 𝓩)S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Propinst✝:DecidablePred phnotSubset:∀ (x y : ChargeSpectrum 𝓩), x ⊆ y → ¬p x → ¬p yhComplet:∀ x ∈ T, x.IsCompletex:ChargeSpectrum 𝓩hx:x ∈ Ty:ChargeSpectrum 𝓩hsubset:x ⊆ yhy:y ∈ ofFinset S5 S10h10:∀ (q10 : ↥S10), Multiset.filter (fun y => y ∉ T ∧ p y) (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) T) = ∅h5:∀ (q5 : ↥S5), Multiset.filter (fun y => y ∉ T ∧ p y) (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) T) = ∅n:ℕhn:n.succ = y.card - x.cardhnot_in_T:y ∉ Thxy:x ≠ yz:ChargeSpectrum 𝓩hz:z ∈ minimalSuperSet S5 S10 xhsubsetz:z ⊆ yhz':z ∉ T → ¬p zhz_not_in_T:¬z ∉ T⊢ n = y.card - (x.card + 1) All goals completed! 🐙 𝓩:Typeinst✝¹:DecidableEq 𝓩T:Multiset (ChargeSpectrum 𝓩)S5:Finset 𝓩S10:Finset 𝓩p:ChargeSpectrum 𝓩 → Propinst✝:DecidablePred phnotSubset:∀ (x y : ChargeSpectrum 𝓩), x ⊆ y → ¬p x → ¬p yhComplet:∀ x ∈ T, x.IsCompletex:ChargeSpectrum 𝓩hx:x ∈ Ty:ChargeSpectrum 𝓩hsubset:x ⊆ yhy:y ∈ ofFinset S5 S10h10:∀ (q10 : ↥S10), Multiset.filter (fun y => y ∉ T ∧ p y) (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) T) = ∅h5:∀ (q5 : ↥S5), Multiset.filter (fun y => y ∉ T ∧ p y) (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) T) = ∅n:ℕhn:n.succ = y.card - x.cardhnot_in_T:y ∉ Thxy:x ≠ yz:ChargeSpectrum 𝓩hz:z ∈ minimalSuperSet S5 S10 xhsubsetz:z ⊆ yhz':z ∉ T → ¬p zhz_not_in_T:¬z ∉ T⊢ y ∉ T All goals completed! 🐙

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.

lemma subset_insert_filter_card_zero (T : Multiset (ChargeSpectrum 𝓩)) (S5 S10 : Finset 𝓩) (p : ChargeSpectrum 𝓩 → Prop) [DecidablePred p] (hnotSubset : ∀ (x y : ChargeSpectrum 𝓩), x ⊆ y → ¬ p x → ¬ p y) (hComplet : ∀ x ∈ T, IsComplete x) (x : ChargeSpectrum 𝓩) (hx : x ∈ T) (y : ChargeSpectrum 𝓩) (hsubset : x ⊆ y) (hy : y ∈ ofFinset S5 S10) (h10 : ∀ q10 : S10, ((T.map fun x => ⟨x.qHd, x.qHu, x.Q5, insert q10.1 x.Q10⟩).filter fun y => (y ∉ T ∧ p y)) = ∅) (h5 : ∀ q5 : S5, ((T.map fun x => ⟨x.qHd, x.qHu, insert q5.1 x.Q5, x.Q10⟩).filter fun y => (y ∉ T ∧ p y)) = ∅) : y ∉ T → ¬ p y := subset_insert_filter_card_zero_inductive T S5 S10 p hnotSubset hComplet x hx y hsubset hy h10 h5 (y.card - x.card) rfl