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

Completions of charges

i. Overview

Recall that a charge spectrum has optional Hu and Hd charges, and can have an empty set of 5-bar or 10 charges.

We say a charge spectrum is complete if it has all types of fields present, i.e. the Hd and Hu charges are present, and the sets of 5-bar and 10 charges are non-empty.

Given a non-complete charge spectrum x we can find all the completions of x, which charges in given subsets. That is, all charge spectra y which are a super set of x, are complete, and have their charges in the given subsets.

ii. Key results

    IsComplete : A predicate saying a charge spectrum is complete.

    completions : Given a charge spectrum x and finite sets of charges S5 and S10, the multiset of completions of x with charges in S5 and S10.

    completionsTopYukawa : A fast version of completions for an x which is in minimallyAllowsTermsOfFinset S5 S10 .topYukawa, or in other words has a qHu charge, a non-empty set of 10 charges, but does not have a qHd charge or any 5-bar charges.

iii. Table of contents

    A. The IsComplete predicate

      A.1. The empty spectrum is not complete

      A.2. The predicate IsCompelete is monotonic

    B. Multiset of completions

      B.1. A membership condition

      B.2. No duplicate condition

      B.3. Completions of a complete charge spectrum

      B.4. Membership of own completions

      B.5. Completeness of members of completions

      B.6. Subset of members of completions

    C. Completions for top Yukawa

      C.1. No duplicates in completionsTopYukawa

      C.2. Equivalence of completions and completionsTopYukawa

iv. References

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

@[expose] public section

A. The IsComplete predicate

We say a charge spectrum is complete if it has all types of fields present, i.e. the Hd and Hu charges are present, and the sets of 5-bar and 10 charges are non-empty.

A charge spectrum is complete if it has all types of fields.

def IsComplete (x : ChargeSpectrum 𝓩) : Prop := x.qHd.isSome ∧ x.qHu.isSome ∧ x.Q5 ≠ ∅ ∧ x.Q10 ≠ ∅
instance [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) : Decidable (IsComplete x) := inferInstanceAs (Decidable (x.qHd.isSome ∧ x.qHu.isSome ∧ x.Q5 ≠ ∅ ∧ x.Q10 ≠ ∅))

A.1. The empty spectrum is not complete

The empty charge spectrum is not complete, since it has no charges present.

@[simp] lemma not_isComplete_empty : ¬ IsComplete (∅ : ChargeSpectrum 𝓩) := 𝓩:Type⊢ ¬∅.IsComplete All goals completed! 🐙

A.2. The predicate IsCompelete is monotonic

The predicate IsComplete is monotonic with respect to the subset relation. That is, if x is a subset of y and x is complete, then y is also complete.

𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hd:x.qHd.toFinset ⊆ y.qHd.toFinseth5:x.Q5 ⊆ y.Q5h10:x.Q10 ⊆ y.Q10hxd:x.qHd.isSome = truehxu:x.qHu.isSome = truehx5:x.Q5 ≠ ∅hx10:x.Q10 ≠ ∅a:𝓩hu:a ∈ y.qHuha:x.qHu = some a⊢ y.qHu.isSome = true All goals completed! 🐙 𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hd:x.qHd.toFinset ⊆ y.qHd.toFinsethu:x.qHu.toFinset ⊆ y.qHu.toFinseth5:x.Q5 ⊆ y.Q5h10:x.Q10 ⊆ y.Q10hxd:x.qHd.isSome = truehxu:x.qHu.isSome = truehx5:x.Q5 ≠ ∅hx10:x.Q10 ≠ ∅⊢ y.Q5 ≠ ∅ All goals completed! 🐙 𝓩:Typex:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hd:x.qHd.toFinset ⊆ y.qHd.toFinsethu:x.qHu.toFinset ⊆ y.qHu.toFinseth5:x.Q5 ⊆ y.Q5h10:x.Q10 ⊆ y.Q10hxd:x.qHd.isSome = truehxu:x.qHu.isSome = truehx5:x.Q5 ≠ ∅hx10:x.Q10 ≠ ∅⊢ y.Q10 ≠ ∅ All goals completed! 🐙

B. Multiset of completions

The completions of a charge spectrum x with charges in given finite sets S5 and S10 are all the charge spectra y which are a super set of x, are complete, and have their charges in S5 and S10.

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 and are complete.

def completions (S5 S10 : Finset 𝓩) (x : ChargeSpectrum 𝓩) : Multiset (ChargeSpectrum 𝓩) := let SqHd := if x.qHd.isSome then {x.qHd} else S5.val.map fun y => some y let SqHu := if x.qHu.isSome then {x.qHu} else S5.val.map fun y => some y let SQ5 := if x.Q5 ≠ ∅ then {x.Q5} else S5.val.map fun y => {y} let SQ10 := if x.Q10 ≠ ∅ then {x.Q10} else S10.val.map fun y => {y} (SqHd ×ˢ SqHu ×ˢ SQ5 ×ˢ SQ10).map (toProd).symm

B.1. A membership condition

A simple relation for membership of a charge spectrum in the completions of another.

𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩a:Option 𝓩 × Option 𝓩 × Finset 𝓩 × Finset 𝓩h:a ∈ (if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 ≠ ∅ then {x.Q5} else Multiset.map (fun y => {y}) S5.val) ×ˢ if x.Q10 ≠ ∅ then {x.Q10} else Multiset.map (fun y => {y}) S10.valhy:toProd.symm a = yha:a = toProd y⊢ (y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 ≠ ∅ then {x.Q5} else Multiset.map (fun y => {y}) S5.val) ∧ y.Q10 ∈ if x.Q10 ≠ ∅ then {x.Q10} else Multiset.map (fun y => {y}) S10.val 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:toProd y ∈ (if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 ≠ ∅ then {x.Q5} else Multiset.map (fun y => {y}) S5.val) ×ˢ if x.Q10 ≠ ∅ then {x.Q10} else Multiset.map (fun y => {y}) S10.valhy:toProd.symm (toProd y) = y⊢ (y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 ≠ ∅ then {x.Q5} else Multiset.map (fun y => {y}) S5.val) ∧ y.Q10 ∈ if x.Q10 ≠ ∅ then {x.Q10} else Multiset.map (fun y => {y}) S10.val All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩⊢ ((y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 ≠ ∅ then {x.Q5} else Multiset.map (fun y => {y}) S5.val) ∧ y.Q10 ∈ if x.Q10 ≠ ∅ then {x.Q10} else Multiset.map (fun y => {y}) S10.val) → ∃ a ∈ (if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 ≠ ∅ then {x.Q5} else Multiset.map (fun y => {y}) S5.val) ×ˢ if x.Q10 ≠ ∅ then {x.Q10} else Multiset.map (fun y => {y}) S10.val, toProd.symm a = y 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 ≠ ∅ then {x.Q5} else Multiset.map (fun y => {y}) S5.val) ∧ y.Q10 ∈ if x.Q10 ≠ ∅ then {x.Q10} else Multiset.map (fun y => {y}) S10.val⊢ ∃ a ∈ (if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 ≠ ∅ then {x.Q5} else Multiset.map (fun y => {y}) S5.val) ×ˢ if x.Q10 ≠ ∅ then {x.Q10} else Multiset.map (fun y => {y}) S10.val, toProd.symm a = y 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 ≠ ∅ then {x.Q5} else Multiset.map (fun y => {y}) S5.val) ∧ y.Q10 ∈ if x.Q10 ≠ ∅ then {x.Q10} else Multiset.map (fun y => {y}) S10.val⊢ (toProd y ∈ (if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 ≠ ∅ then {x.Q5} else Multiset.map (fun y => {y}) S5.val) ×ˢ if x.Q10 ≠ ∅ then {x.Q10} else Multiset.map (fun y => {y}) S10.val) ∧ toProd.symm (toProd y) = y All goals completed! 🐙

B.2. No duplicate condition

For speed we define completions to be a multiset, but in fact it has no duplicates, so it could be defined as a finite set.

lemma completions_nodup (S5 S10 : Finset 𝓩) (x : ChargeSpectrum 𝓩) : (completions S5 S10 x).Nodup := 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩⊢ (completions S5 S10 x).Nodup 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩⊢ (Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10})).Nodup 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:x.qHd.isSome = trueh✝²:x.qHu.isSome = trueh✝¹:x.Q5 = ∅h✝:x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) ({x.qHd} ×ˢ {x.qHu} ×ˢ Multiset.map (fun y => {y}) S5.val ×ˢ Multiset.map (fun y => {y}) S10.val)).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:x.qHd.isSome = trueh✝²:x.qHu.isSome = trueh✝¹:x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) ({x.qHd} ×ˢ {x.qHu} ×ˢ Multiset.map (fun y => {y}) S5.val ×ˢ {x.Q10})).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:x.qHd.isSome = trueh✝²:x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) ({x.qHd} ×ˢ {x.qHu} ×ˢ {x.Q5} ×ˢ Multiset.map (fun y => {y}) S10.val)).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:x.qHd.isSome = trueh✝²:x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) ({x.qHd} ×ˢ {x.qHu} ×ˢ {x.Q5} ×ˢ {x.Q10})).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:x.Q5 = ∅h✝:x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) ({x.qHd} ×ˢ Multiset.map (fun y => some y) S5.val ×ˢ Multiset.map (fun y => {y}) S5.val ×ˢ Multiset.map (fun y => {y}) S10.val)).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) ({x.qHd} ×ˢ Multiset.map (fun y => some y) S5.val ×ˢ Multiset.map (fun y => {y}) S5.val ×ˢ {x.Q10})).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) ({x.qHd} ×ˢ Multiset.map (fun y => some y) S5.val ×ˢ {x.Q5} ×ˢ Multiset.map (fun y => {y}) S10.val)).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) ({x.qHd} ×ˢ Multiset.map (fun y => some y) S5.val ×ˢ {x.Q5} ×ˢ {x.Q10})).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:x.qHu.isSome = trueh✝¹:x.Q5 = ∅h✝:x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) (Multiset.map (fun y => some y) S5.val ×ˢ {x.qHu} ×ˢ Multiset.map (fun y => {y}) S5.val ×ˢ Multiset.map (fun y => {y}) S10.val)).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:x.qHu.isSome = trueh✝¹:x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) (Multiset.map (fun y => some y) S5.val ×ˢ {x.qHu} ×ˢ Multiset.map (fun y => {y}) S5.val ×ˢ {x.Q10})).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) (Multiset.map (fun y => some y) S5.val ×ˢ {x.qHu} ×ˢ {x.Q5} ×ˢ Multiset.map (fun y => {y}) S10.val)).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) (Multiset.map (fun y => some y) S5.val ×ˢ {x.qHu} ×ˢ {x.Q5} ×ˢ {x.Q10})).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:x.Q5 = ∅h✝:x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) (Multiset.map (fun y => some y) S5.val ×ˢ Multiset.map (fun y => some y) S5.val ×ˢ Multiset.map (fun y => {y}) S5.val ×ˢ Multiset.map (fun y => {y}) S10.val)).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) (Multiset.map (fun y => some y) S5.val ×ˢ Multiset.map (fun y => some y) S5.val ×ˢ Multiset.map (fun y => {y}) S5.val ×ˢ {x.Q10})).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) (Multiset.map (fun y => some y) S5.val ×ˢ Multiset.map (fun y => some y) S5.val ×ˢ {x.Q5} ×ˢ Multiset.map (fun y => {y}) S10.val)).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ (Multiset.map (fun x => toProd.symm x) (Multiset.map (fun y => some y) S5.val ×ˢ Multiset.map (fun y => some y) S5.val ×ˢ {x.Q5} ×ˢ {x.Q10})).Nodup all_goals 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ (Multiset.map (fun y => some y) S5.val ×ˢ Multiset.map (fun y => some y) S5.val ×ˢ {x.Q5} ×ˢ {x.Q10}).Nodup 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ (Multiset.map (fun y => some y) S5.val).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ (Multiset.map (fun y => some y) S5.val).Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ {x.Q5}.Nodup𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ {x.Q10}.Nodup any_goals All goals completed! 🐙 any_goals exact Finset.nodup_map_iff_injOn.mpr (𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h✝³:¬x.qHd.isSome = trueh✝²:¬x.qHu.isSome = trueh✝¹:¬x.Q5 = ∅h✝:¬x.Q10 = ∅⊢ Set.InjOn (fun y => some y) ↑S5 All goals completed! 🐙)

B.3. Completions of a complete charge spectrum

The completions of a complete charge spectrum is just the singleton containing itself.

lemma completions_eq_singleton_of_complete {S5 S10 : Finset 𝓩} (x : ChargeSpectrum 𝓩) (hcomplete : IsComplete x) : completions S5 S10 x = {x} := 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.IsComplete⊢ completions S5 S10 x = {x} 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.IsComplete⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x} 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x} 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅h1:x.qHd.isSome = true⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x}𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅h1:¬x.qHd.isSome = true⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x} case' neg 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅h1:¬x.qHd.isSome = true⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x} All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅h1:x.qHd.isSome = trueh2:x.qHu.isSome = true⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x}𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅h1:x.qHd.isSome = trueh2:¬x.qHu.isSome = true⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x} case' neg 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅h1:x.qHd.isSome = trueh2:¬x.qHu.isSome = true⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x} All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:x.Q5 ≠ ∅⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x}𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:¬x.Q5 ≠ ∅⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x} case' neg 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:¬x.Q5 ≠ ∅⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x} All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:x.Q5 ≠ ∅h4:x.Q10 ≠ ∅⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x}𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:x.Q5 ≠ ∅h4:¬x.Q10 ≠ ∅⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x} case' neg 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩hcomplete:x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:x.Q5 ≠ ∅h4:¬x.Q10 ≠ ∅⊢ Multiset.map (fun x => toProd.symm x) ((if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ×ˢ (if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ×ˢ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) = {x} All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:¬x.Q5 = ∅h4:¬x.Q10 = ∅⊢ toProd.symm (x.qHd, x.qHu, x.Q5, x.Q10) = x All goals completed! 🐙

B.4. Membership of own completions

If a charge spectrum x is a member of its own completion then it is complete, and vice versa.

@[simp] lemma self_mem_completions_iff_isComplete {S5 S10 : Finset 𝓩} (x : ChargeSpectrum 𝓩) : x ∈ completions S5 S10 x ↔ IsComplete x := 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩⊢ x ∈ completions S5 S10 x ↔ x.IsComplete 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:x.qHd.isSome = true⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:¬x.qHd.isSome = true⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅ case neg 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:¬x.qHd.isSome = true⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅ All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:x.qHd.isSome = trueh2:x.qHu.isSome = true⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:x.qHd.isSome = trueh2:¬x.qHu.isSome = true⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅ case' neg 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:x.qHd.isSome = trueh2:¬x.qHu.isSome = true⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅ All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:x.Q5 ≠ ∅⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:¬x.Q5 ≠ ∅⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅ case' neg 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:¬x.Q5 ≠ ∅⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅ All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:x.Q5 ≠ ∅h4:x.Q10 ≠ ∅⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:x.Q5 ≠ ∅h4:¬x.Q10 ≠ ∅⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅ case' neg 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h1:x.qHd.isSome = trueh2:x.qHu.isSome = trueh3:x.Q5 ≠ ∅h4:¬x.Q10 ≠ ∅⊢ ((x.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (x.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (x.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ x.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}) ↔ x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ ¬x.Q5 = ∅ ∧ ¬x.Q10 = ∅ All goals completed! 🐙 All goals completed! 🐙

B.5. Completeness of members of completions

We now show that any member of the completions of a charge spectrum is complete.

A charge spectrum which is a member of the completions of another charge spectrum is complete.

𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd.isSome = true ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu.isSome = true ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ≠ ∅ ∧ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 ≠ ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd.isSome = true𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu.isSome = true𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ≠ ∅𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 ≠ ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHd.isSome = true 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ qHd.isSome = true 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:x1.isSome = true⊢ qHd.isSome = true𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:¬x1.isSome = true⊢ qHd.isSome = true 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:x1.isSome = true⊢ qHd.isSome = true All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:¬x1.isSome = true⊢ qHd.isSome = true 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(∃ a ∈ S5, some a = qHd) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:x1 = none⊢ qHd.isSome = true 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hs:x1 = nonea:𝓩h:a ∈ S5hx:(∃ a_1 ∈ S5, some a_1 = some a) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ (some a).isSome = true All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.qHu.isSome = true 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ qHu.isSome = true 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:x2.isSome = true⊢ qHu.isSome = true𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:¬x2.isSome = true⊢ qHu.isSome = true 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:x2.isSome = true⊢ qHu.isSome = true All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:¬x2.isSome = true⊢ qHu.isSome = true 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (∃ a ∈ S5, some a = qHu) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:x2 = none⊢ qHu.isSome = true 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hs:x2 = nonea:𝓩h:a ∈ S5hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (∃ a_1 ∈ S5, some a_1 = some a) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ (some a).isSome = true All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q5 ≠ ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ ¬Q5 = ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:x3 ≠ ∅⊢ ¬Q5 = ∅𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:¬x3 ≠ ∅⊢ ¬Q5 = ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:x3 ≠ ∅⊢ ¬Q5 = ∅ All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:¬x3 ≠ ∅⊢ ¬Q5 = ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (∃ a ∈ S5, {a} = Q5) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:x3 = ∅⊢ ¬Q5 = ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hs:x3 = ∅a:𝓩h:a ∈ S5hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (∃ a_1 ∈ S5, {a_1} = {a}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ ¬{a} = ∅ All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.Q10 ≠ ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}⊢ ¬Q10 = ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:x4 ≠ ∅⊢ ¬Q10 = ∅𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:¬x4 ≠ ∅⊢ ¬Q10 = ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:x4 ≠ ∅⊢ ¬Q10 = ∅ All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ Q10 ∈ if x4 = ∅ then Multiset.map (fun y => {y}) S10.val else {x4}hs:¬x4 ≠ ∅⊢ ¬Q10 = ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ ∃ a ∈ S10, {a} = Q10hs:x4 = ∅⊢ ¬Q10 = ∅ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩hs:x4 = ∅a:𝓩h:a ∈ S10hx:(qHd ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.val) ∧ (qHu ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val) ∧ (Q5 ∈ if x3 = ∅ then Multiset.map (fun y => {y}) S5.val else {x3}) ∧ ∃ a_1 ∈ S10, {a_1} = {a}⊢ ¬{a} = ∅ All goals completed! 🐙

B.6. Subset of members of completions

We show that any member of the completions of a charge spectrum is a super set of that charge spectrum.

If y is in the completions of x then x ⊆ y.

𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}⊢ hasSubset.1 x y 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}⊢ x.qHd.toFinset ⊆ y.qHd.toFinset ∧ x.qHu.toFinset ⊆ y.qHu.toFinset ∧ x.Q5 ⊆ y.Q5 ∧ x.Q10 ⊆ y.Q10 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}⊢ x.qHd.toFinset ⊆ y.qHd.toFinset𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}⊢ x.qHu.toFinset ⊆ y.qHu.toFinset𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}⊢ x.Q5 ⊆ y.Q5𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}⊢ x.Q10 ⊆ y.Q10 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}⊢ x.qHd.toFinset ⊆ y.qHd.toFinset 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:x.qHd.isSome = true⊢ x.qHd.toFinset ⊆ y.qHd.toFinset𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:¬x.qHd.isSome = true⊢ x.qHd.toFinset ⊆ y.qHd.toFinset 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:x.qHd.isSome = true⊢ x.qHd.toFinset ⊆ y.qHd.toFinset All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:¬x.qHd.isSome = true⊢ x.qHd.toFinset ⊆ y.qHd.toFinset All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}⊢ x.qHu.toFinset ⊆ y.qHu.toFinset 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:x.qHu.isSome = true⊢ x.qHu.toFinset ⊆ y.qHu.toFinset𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:¬x.qHu.isSome = true⊢ x.qHu.toFinset ⊆ y.qHu.toFinset 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:x.qHu.isSome = true⊢ x.qHu.toFinset ⊆ y.qHu.toFinset All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:¬x.qHu.isSome = true⊢ x.qHu.toFinset ⊆ y.qHu.toFinset All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}⊢ x.Q5 ⊆ y.Q5 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:x.Q5 ≠ ∅⊢ x.Q5 ⊆ y.Q5𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:¬x.Q5 ≠ ∅⊢ x.Q5 ⊆ y.Q5 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:x.Q5 ≠ ∅⊢ x.Q5 ⊆ y.Q5 All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:¬x.Q5 ≠ ∅⊢ x.Q5 ⊆ y.Q5 All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}⊢ x.Q10 ⊆ y.Q10 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:x.Q10 ≠ ∅⊢ x.Q10 ⊆ y.Q10𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:¬x.Q10 ≠ ∅⊢ x.Q10 ⊆ y.Q10 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:x.Q10 ≠ ∅⊢ x.Q10 ⊆ y.Q10 All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hy:(y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun y => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun y => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 = ∅ then Multiset.map (fun y => {y}) S5.val else {x.Q5}) ∧ y.Q10 ∈ if x.Q10 = ∅ then Multiset.map (fun y => {y}) S10.val else {x.Q10}h:¬x.Q10 ≠ ∅⊢ x.Q10 ⊆ y.Q10 All goals completed! 🐙

If x is a subset of y and y is complete, then there is a completion of x which is also a subset of y.

𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val⊢ hasSubset.1 { qHd := some y1, qHu := some y2, Q5 := if x3 = ∅ then {z3} else x3, Q10 := if x4 = ∅ then {z4} else x4 } { qHd := some y1, qHu := some y2, Q5 := y3, Q10 := y4 } 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val⊢ {y1} ⊆ {y1} ∧ {y2} ⊆ {y2} ∧ (if x3 = ∅ then {z3} else x3) ⊆ y3 ∧ (if x4 = ∅ then {z4} else x4) ⊆ y4 refine ⟨𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val⊢ {y1} ⊆ {y1} All goals completed! 🐙, 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val⊢ {y2} ⊆ {y2} All goals completed! 🐙, ?_, ?_⟩ 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val⊢ (if x3 = ∅ then {z3} else x3) ⊆ y3 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.valh3:x3 = ∅⊢ {z3} ⊆ y3𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.valh3:¬x3 = ∅⊢ x3 ⊆ y3 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.valh3:x3 = ∅⊢ {z3} ⊆ y3𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.valh3:¬x3 = ∅⊢ x3 ⊆ y3 All goals completed! 🐙 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.val⊢ (if x4 = ∅ then {z4} else x4) ⊆ y4 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.valh4:x4 = ∅⊢ {z4} ⊆ y4𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.valh4:¬x4 = ∅⊢ x4 ⊆ y4 𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.valh4:x4 = ∅⊢ {z4} ⊆ y4𝓩:Typeinst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩x1:Option 𝓩x2:Option 𝓩x3:Finset 𝓩x4:Finset 𝓩y3:Finset 𝓩y4:Finset 𝓩hx:¬{ qHd := x1, qHu := x2, Q5 := x3, Q10 := x4 }.IsCompletey1:𝓩y2:𝓩z3:𝓩z4:𝓩hsubset:(x1.toFinset = ∅ ∨ x1.toFinset = {y1}) ∧ (x2.toFinset = ∅ ∨ x2.toFinset = {y2}) ∧ x3 ⊆ y3 ∧ x4 ⊆ y4hycomplete:(∃ x, x ∈ y3) ∧ ∃ x, x ∈ y4hz3:z3 ∈ y3hz4:z4 ∈ y4hy:y1 ∈ S5 ∧ y2 ∈ S5 ∧ y3 ⊆ S5 ∧ y4 ⊆ S10hz3Mem:z3 ∈ S5hz4Mem:z4 ∈ S10hy1':some y1 ∈ if x1.isSome = true then {x1} else Multiset.map (fun y => some y) S5.valhy2':some y2 ∈ if x2.isSome = true then {x2} else Multiset.map (fun y => some y) S5.valh4:¬x4 = ∅⊢ x4 ⊆ y4 All goals completed! 🐙

C. Completions for top Yukawa

We give a fast version of completions in the case when x has a qHu charge, and a non-empty set of 10 charges, but does not have a qHd charge or any 5-bar charges. Here we only need to specify the allowed 5-bar charges, not the allowed 10 charges.

This is the case for charges which minimally allow the top Yukawa coupling.

These definitions are primarily for speed, as this is the most common case we will look at.

A fast version of completions for an x which is in minimallyAllowsTermsOfFinset S5 S10 .topYukawa.

def completionsTopYukawa (S5 : Finset 𝓩) (x : ChargeSpectrum 𝓩) : Multiset (ChargeSpectrum 𝓩) := (S5.val ×ˢ S5.val).map fun (qHd, q5) => ⟨qHd, x.qHu, {q5}, x.Q10⟩

C.1. No duplicates in completionsTopYukawa

Like for completions, we define completionsTopYukawa as a multiset for speed, however, we can show it has no duplicates.

The multiset completionsTopYukawa S5 x has no duplicates.

omit [DecidableEq 𝓩] inlemma completionsTopYukawa_nodup {S5 : Finset 𝓩} (x : ChargeSpectrum 𝓩) : (completionsTopYukawa S5 x).Nodup := 𝓩:TypeS5:Finset 𝓩x:ChargeSpectrum 𝓩⊢ (completionsTopYukawa S5 x).Nodup 𝓩:TypeS5:Finset 𝓩x:ChargeSpectrum 𝓩⊢ (Multiset.map (fun x_1 => { qHd := some x_1.1, qHu := x.qHu, Q5 := {x_1.2}, Q10 := x.Q10 }) (S5.val ×ˢ S5.val)).Nodup 𝓩:TypeS5:Finset 𝓩x:ChargeSpectrum 𝓩⊢ ∀ x_1 ∈ S5.val ×ˢ S5.val, ∀ y ∈ S5.val ×ˢ S5.val, { qHd := some x_1.1, qHu := x.qHu, Q5 := {x_1.2}, Q10 := x.Q10 } = { qHd := some y.1, qHu := x.qHu, Q5 := {y.2}, Q10 := x.Q10 } → x_1 = y𝓩:TypeS5:Finset 𝓩x:ChargeSpectrum 𝓩⊢ (S5.val ×ˢ S5.val).Nodup 𝓩:TypeS5:Finset 𝓩x:ChargeSpectrum 𝓩z1:𝓩z2:𝓩hz:(z1, z2) ∈ S5.val ×ˢ S5.valy1:𝓩y2:𝓩hy:(y1, y2) ∈ S5.val ×ˢ S5.valh:{ qHd := some (z1, z2).1, qHu := x.qHu, Q5 := {(z1, z2).2}, Q10 := x.Q10 } = { qHd := some (y1, y2).1, qHu := x.qHu, Q5 := {(y1, y2).2}, Q10 := x.Q10 }⊢ (z1, z2) = (y1, y2)𝓩:TypeS5:Finset 𝓩x:ChargeSpectrum 𝓩⊢ (S5.val ×ˢ S5.val).Nodup 𝓩:TypeS5:Finset 𝓩x:ChargeSpectrum 𝓩z1:𝓩z2:𝓩hz:(z1, z2) ∈ S5.val ×ˢ S5.valy1:𝓩y2:𝓩hy:(y1, y2) ∈ S5.val ×ˢ S5.valh:z1 = y1 ∧ z2 = y2⊢ (z1, z2) = (y1, y2)𝓩:TypeS5:Finset 𝓩x:ChargeSpectrum 𝓩⊢ (S5.val ×ˢ S5.val).Nodup 𝓩:TypeS5:Finset 𝓩x:ChargeSpectrum 𝓩⊢ (S5.val ×ˢ S5.val).Nodup All goals completed! 🐙

C.2. Equivalence of completions and completionsTopYukawa

For charges x which are in minimallyAllowsTermsOfFinset S5 S10 .topYukawa, we show that completions S5 S10 x and completionsTopYukawa S5 x are equal multisets.

The multisets completions S5 S10 x and completionsTopYukawa S5 x are equivalent if x minimally allows the top Yukawa.

𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩a:ChargeSpectrum 𝓩qHu:𝓩Q10:Multiset 𝓩h3:-qHu + Q10.sum = 0h1:qHu ∈ S5h2:Q10.toFinset ⊆ S10hcard:Q10.card = 2Q10_ne_zero:Q10 ≠ 0⊢ (∃ b a_1 a_2, (a_2 ∈ S5 ∧ a_1 ∈ S5 ∧ b ∈ if Q10 = 0 then Multiset.map (fun y => {y}) S10.val else {Q10.toFinset}) ∧ toProd.symm (some a_2, some qHu, {a_1}, b) = a) ↔ ∃ a_1 b, (a_1 ∈ S5 ∧ b ∈ S5) ∧ { qHd := some a_1, qHu := some qHu, Q5 := {b}, Q10 := Q10.toFinset } = a 𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩a:ChargeSpectrum 𝓩qHu:𝓩Q10:Multiset 𝓩h3:-qHu + Q10.sum = 0h1:qHu ∈ S5h2:Q10.toFinset ⊆ S10hcard:Q10.card = 2Q10_ne_zero:Q10 ≠ 0⊢ (∃ a_1 a_2, (a_2 ∈ S5 ∧ a_1 ∈ S5) ∧ toProd.symm (some a_2, some qHu, {a_1}, Q10.toFinset) = a) ↔ ∃ a_1 b, (a_1 ∈ S5 ∧ b ∈ S5) ∧ { qHd := some a_1, qHu := some qHu, Q5 := {b}, Q10 := Q10.toFinset } = a match a with 𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩a:ChargeSpectrum 𝓩qHu:𝓩Q10:Multiset 𝓩h3:-qHu + Q10.sum = 0h1:qHu ∈ S5h2:Q10.toFinset ⊆ S10hcard:Q10.card = 2Q10_ne_zero:Q10 ≠ 0xqHd:Option 𝓩xqHu:Option 𝓩xQ5:Finset 𝓩xQ10:Finset 𝓩⊢ (∃ a a_1, (a_1 ∈ S5 ∧ a ∈ S5) ∧ toProd.symm (some a_1, some qHu, {a}, Q10.toFinset) = { qHd := xqHd, qHu := xqHu, Q5 := xQ5, Q10 := xQ10 }) ↔ ∃ a b, (a ∈ S5 ∧ b ∈ S5) ∧ { qHd := some a, qHu := some qHu, Q5 := {b}, Q10 := Q10.toFinset } = { qHd := xqHd, qHu := xqHu, Q5 := xQ5, Q10 := xQ10 } 𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩a:ChargeSpectrum 𝓩qHu:𝓩Q10:Multiset 𝓩h3:-qHu + Q10.sum = 0h1:qHu ∈ S5h2:Q10.toFinset ⊆ S10hcard:Q10.card = 2Q10_ne_zero:Q10 ≠ 0xqHd:Option 𝓩xqHu:Option 𝓩xQ5:Finset 𝓩xQ10:Finset 𝓩⊢ (∃ a a_1, (a_1 ∈ S5 ∧ a ∈ S5) ∧ (toProd.symm (some a_1, some qHu, {a}, Q10.toFinset)).qHd = xqHd ∧ (toProd.symm (some a_1, some qHu, {a}, Q10.toFinset)).qHu = xqHu ∧ (toProd.symm (some a_1, some qHu, {a}, Q10.toFinset)).Q5 = xQ5 ∧ (toProd.symm (some a_1, some qHu, {a}, Q10.toFinset)).Q10 = xQ10) ↔ ∃ a b, (a ∈ S5 ∧ b ∈ S5) ∧ some a = xqHd ∧ some qHu = xqHu ∧ {b} = xQ5 ∧ Q10.toFinset = xQ10 All goals completed! 🐙