Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoClosed

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.Yukawa
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimalSuperSet
public import Physlib.Meta.TODO.Basic

Phenomenologically closed sets of charge spectra

i. Overview

The main goal of this file is to prove the lemma completeness_of_isPhenoClosedQ5_isPhenoClosedQ10, which allows us to prove that a multiset of charge spectra contains all phenomenologically viable charge spectra, given a finite set of allowed 5-bar and 10-dimensional.

This lemma relies on the multiset of charge spectra satisfying a number of conditions, which include three which are defined in this file: IsPhenoClosedQ5, IsPhenoClosedQ10 and ContainsPhenoCompletionsOfMinimallyAllows.

ii. Key results

IsPhenoClosedQ5 : The proposition that a multiset of charges is phenomenologically closed under addition of 5-bar charges from a finite set S5.

IsPhenoClosedQ10 : The proposition that a multiset of charges is phenomenologically closed under addition of 10-dimensional charges from a finite set S10.

ContainsPhenoCompletionsOfMinimallyAllows : The proposition that a multiset of charges contains all phenomenologically viable completions of charge spectra which permit the top Yukawa.

completeMinSubset : For a given S5 S10 : Finset 𝓩, the minimal multiset of charges which satisfies the condition ContainsPhenoCompletionsOfMinimallyAllows.

completeness_of_isPhenoClosedQ5_isPhenoClosedQ10 : A lemma for simplifying the proof that a multiset contains all phenomenologically viable charge spectra.

viableChargesMultiset : A computable multiset containing all phenomenologically viable charge spectra for a given S5 S10 : Finset 𝓩.

iii. Table of contents

A. Phenomenologically closed under additions of 5-bar charges

A.1. Simplification using pheno-constrained due to additional of 5-bar charge

B. Phenomenologically closed under additions of 10d charges

B.1. Simplification using pheno-constrained due to additional of 10d charge

C. Prop for multiset containing all pheno-viable completions of charges permitting top Yukawa

C.1. Simplification using fast version of completions of charges permitting top Yukawa

C.2. Decidability of proposition

C.3. Monotonicity of proposition

C.4. completeMinSubset: Minimal multiset with viable completions of top-permitting charges

C.4.1. The multiset completeMinSubset has no duplicates

C.4.2. The multiset completeMinSubset is minimal

C.4.3. The multiset completeMinSubset contains all completions

D. Multisets containing all pheno-viable charge spectra

D.1. Lemma for simplifying proof that a multiset contains all pheno-viable charge spectra

D.2. Computable multiset containing all pheno-viable charge spectra

iv. References

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

@[expose] public section

A. Phenomenologically closed under additions of 5-bar charges

The proposition that for multiset set of charges charges, adding individual elements of S5 to the Q5 charges of elements of charges again leads to an element in charges or a charge which is phenomenologically constrained, or regenerates dangerous couplings with one singlet insertion.

def IsPhenoClosedQ5 (S5 : Finset 𝓩) (charges : Multiset (ChargeSpectrum 𝓩)) : Prop :=
  ∀ q5 ∈ S5, ∀ x ∈ charges,
    let y : ChargeSpectrum 𝓩 := ⟨x.qHd, x.qHu, insert q5 x.Q5, x.Q10⟩
    IsPhenoConstrained y ∨ y ∈ charges ∨ YukawaGeneratesDangerousAtLevel y 1

A.1. Simplification using pheno-constrained due to additional of 5-bar charge



lemma isPhenClosedQ5_of_isPhenoConstrainedQ5 {S5 : Finset 𝓩} {charges : Multiset (ChargeSpectrum 𝓩)}
    (h : ∀ q5 ∈ S5, ∀ x ∈ charges,
      let y : ChargeSpectrum 𝓩 := ⟨x.qHd, x.qHu, insert q5 x.Q5, x.Q10⟩
      IsPhenoConstrainedQ5 x q5 ∨ y ∈ charges ∨ YukawaGeneratesDangerousAtLevel y 1) :
    IsPhenoClosedQ5 S5 charges := by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1⊢ IsPhenoClosedQ5 S5 charges
  intro q5 hq5 x hx𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q5:𝓩hq5:q5 ∈ S5x:ChargeSpectrum 𝓩hx:x ∈ charges⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1
  rcases h q5 hq5 x hx with h'| h' | h'inl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q5:𝓩hq5:q5 ∈ S5x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ5 q5⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1inr.inl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q5:𝓩hq5:q5 ∈ S5x:ChargeSpectrum 𝓩hx:x ∈ chargesh':{ qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 } ∈ charges⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1inr.inr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q5:𝓩hq5:q5 ∈ S5x:ChargeSpectrum 𝓩hx:x ∈ chargesh':{ qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 }.YukawaGeneratesDangerousAtLevel 1⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1
  ·inl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q5:𝓩hq5:q5 ∈ S5x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ5 q5⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1 leftinl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q5:𝓩hq5:q5 ∈ S5x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ5 q5⊢ { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 }.IsPhenoConstrained
    rw [isPhenoConstrained_insertQ5_iff_isPhenoConstrainedQ5inl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q5:𝓩hq5:q5 ∈ S5x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ5 q5⊢ { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrainedQ5 q5 ∨
  { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrainedinl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q5:𝓩hq5:q5 ∈ S5x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ5 q5⊢ { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrainedQ5 q5 ∨
  { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrained]inl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q5:𝓩hq5:q5 ∈ S5x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ5 q5⊢ { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrainedQ5 q5 ∨
  { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrained
    leftinl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q5:𝓩hq5:q5 ∈ S5x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ5 q5⊢ { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrainedQ5 q5
    exact h'All goals completed! 🐙
  ·inr.inl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q5:𝓩hq5:q5 ∈ S5x:ChargeSpectrum 𝓩hx:x ∈ chargesh':{ qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 } ∈ charges⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1 simp_allAll goals completed! 🐙
  ·inr.inr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q5 ∈ S5,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
    x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q5:𝓩hq5:q5 ∈ S5x:ChargeSpectrum 𝓩hx:x ∈ chargesh':{ qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 }.YukawaGeneratesDangerousAtLevel 1⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1 simp_allAll goals completed! 🐙

B. Phenomenologically closed under additions of 10d charges

The proposition that for multiset set of charges charges, adding individual elements of S10 to the Q10 charges of elements of charges again leads to an element in charges or a charge which is phenomenologically constrained, or regenerates dangerous couplings with one singlet insertion.

def IsPhenoClosedQ10 (S10 : Finset 𝓩) (charges : Multiset (ChargeSpectrum 𝓩)) : Prop :=
  ∀ q10 ∈ S10, ∀ x ∈ charges,
    let y : ChargeSpectrum 𝓩 := ⟨x.qHd, x.qHu, x.Q5, insert q10 x.Q10⟩
    IsPhenoConstrained y ∨ y ∈ charges ∨ YukawaGeneratesDangerousAtLevel y 1

B.1. Simplification using pheno-constrained due to additional of 10d charge



lemma isPhenClosedQ10_of_isPhenoConstrainedQ10 {S10 : Finset 𝓩}
    {charges : Multiset (ChargeSpectrum 𝓩)}
    (h : ∀ q10 ∈ S10, ∀ x ∈ charges,
      let y : ChargeSpectrum 𝓩 := ⟨x.qHd, x.qHu, x.Q5, insert q10 x.Q10⟩
      IsPhenoConstrainedQ10 x q10 ∨ y ∈ charges ∨ YukawaGeneratesDangerousAtLevel y 1) :
    IsPhenoClosedQ10 S10 charges := by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1⊢ IsPhenoClosedQ10 S10 charges
  intro q10 hq10 x hx𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q10:𝓩hq10:q10 ∈ S10x:ChargeSpectrum 𝓩hx:x ∈ charges⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1
  rcases h q10 hq10 x hx with h'| h' | h'inl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q10:𝓩hq10:q10 ∈ S10x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ10 q10⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1inr.inl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q10:𝓩hq10:q10 ∈ S10x:ChargeSpectrum 𝓩hx:x ∈ chargesh':{ qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 } ∈ charges⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1inr.inr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q10:𝓩hq10:q10 ∈ S10x:ChargeSpectrum 𝓩hx:x ∈ chargesh':{ qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 }.YukawaGeneratesDangerousAtLevel 1⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1
  ·inl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q10:𝓩hq10:q10 ∈ S10x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ10 q10⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1 leftinl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q10:𝓩hq10:q10 ∈ S10x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ10 q10⊢ { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 }.IsPhenoConstrained
    rw [isPhenoConstrained_insertQ10_iff_isPhenoConstrainedQ10inl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q10:𝓩hq10:q10 ∈ S10x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ10 q10⊢ { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrainedQ10 q10 ∨
  { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrainedinl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q10:𝓩hq10:q10 ∈ S10x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ10 q10⊢ { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrainedQ10 q10 ∨
  { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrained]inl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q10:𝓩hq10:q10 ∈ S10x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ10 q10⊢ { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrainedQ10 q10 ∨
  { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrained
    leftinl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q10:𝓩hq10:q10 ∈ S10x:ChargeSpectrum 𝓩hx:x ∈ chargesh':x.IsPhenoConstrainedQ10 q10⊢ { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := x.Q10 }.IsPhenoConstrainedQ10 q10
    exact h'All goals completed! 🐙
  ·inr.inl𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q10:𝓩hq10:q10 ∈ S10x:ChargeSpectrum 𝓩hx:x ∈ chargesh':{ qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 } ∈ charges⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1 simp_allAll goals completed! 🐙
  ·inr.inr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ q10 ∈ S10,
  ∀ x ∈ charges,
    let y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
    x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1q10:𝓩hq10:q10 ∈ S10x:ChargeSpectrum 𝓩hx:x ∈ chargesh':{ qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 }.YukawaGeneratesDangerousAtLevel 1⊢ have y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1 simp_allAll goals completed! 🐙

C. Prop for multiset containing all pheno-viable completions of charges permitting top Yukawa

The proposition that for multiset set of charges charges contains all viable completions of charges which allow the top Yukawa, given allowed values of 5d and 10d charges S5 and S10.

def ContainsPhenoCompletionsOfMinimallyAllows (S5 S10 : Finset 𝓩)
    (charges : Multiset (ChargeSpectrum 𝓩)) : Prop :=
  ∀ x ∈ (minimallyAllowsTermsOfFinset S5 S10 topYukawa),
      ¬ x.IsPhenoConstrained → ∀ y ∈ completions S5 S10 x, ¬ y.IsPhenoConstrained
      ∧ ¬ y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges

C.1. Simplification using fast version of completions of charges permitting top Yukawa



lemma containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawa {S5 S10 : Finset 𝓩}
    {charges : Multiset (ChargeSpectrum 𝓩)} :
    ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges ↔
    ∀ x ∈ (minimallyAllowsTermsOfFinset S5 S10 topYukawa),
    ∀ y ∈ completionsTopYukawa S5 x, ¬ y.IsPhenoConstrained
      ∧ ¬ y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges := by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)⊢ ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges ↔
  ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges
  rw [ContainsPhenoCompletionsOfMinimallyAllows𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)⊢ (∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ¬x.IsPhenoConstrained →
      ∀ y ∈ completions S5 S10 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges) ↔
  ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)⊢ (∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ¬x.IsPhenoConstrained →
      ∀ y ∈ completions S5 S10 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges) ↔
  ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges]𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)⊢ (∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ¬x.IsPhenoConstrained →
      ∀ y ∈ completions S5 S10 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges) ↔
  ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges
  have h1 (x : ChargeSpectrum 𝓩) (hx : x ∈ (minimallyAllowsTermsOfFinset S5 S10 topYukawa)) :
    ¬ x.IsPhenoConstrained ↔ True := by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)⊢ ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges ↔
  ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h1:∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, ¬x.IsPhenoConstrained ↔ True⊢ (∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ¬x.IsPhenoConstrained →
      ∀ y ∈ completions S5 S10 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges) ↔
  ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges
    simp only [iff_true]𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)x:ChargeSpectrum 𝓩hx:x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa⊢ ¬x.IsPhenoConstrained𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h1:∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, ¬x.IsPhenoConstrained ↔ True⊢ (∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ¬x.IsPhenoConstrained →
      ∀ y ∈ completions S5 S10 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges) ↔
  ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges
    exact not_isPhenoConstrained_of_minimallyAllowsTermsOfFinset_topYukawa hx𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h1:∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, ¬x.IsPhenoConstrained ↔ True⊢ (∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ¬x.IsPhenoConstrained →
      ∀ y ∈ completions S5 S10 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges) ↔
  ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h1:∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, ¬x.IsPhenoConstrained ↔ True⊢ (∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ¬x.IsPhenoConstrained →
      ∀ y ∈ completions S5 S10 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges) ↔
  ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
    ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges
  conv_lhs =>
    enter [x, hx]𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h1:∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, ¬x.IsPhenoConstrained ↔ Truex:ChargeSpectrum 𝓩hx:x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa| ¬x.IsPhenoConstrained →
  ∀ y ∈ completions S5 S10 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges
    rw [completions_eq_completionsTopYukawa_of_mem_minimallyAllowsTermsOfFinset x hx]𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h1:∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, ¬x.IsPhenoConstrained ↔ Truex:ChargeSpectrum 𝓩hx:x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa| ¬x.IsPhenoConstrained →
  ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges
    rw [h1 x hx]𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h1:∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, ¬x.IsPhenoConstrained ↔ Truex:ChargeSpectrum 𝓩hx:x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa| True → ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges
  simpAll goals completed! 🐙

C.2. Decidability of proposition

instance {S5 S10 : Finset 𝓩} {charges : Multiset (ChargeSpectrum 𝓩)} :
    Decidable (ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges) :=
  decidable_of_iff _ (containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawa).symm

C.3. Monotonicity of proposition

lemma containsPhenoCompletionsOfMinimallyAllows_of_subset {S5 S10 : Finset 𝓩}
    {charges charges' : Multiset (ChargeSpectrum 𝓩)}
    (h' : ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges)
    (h : ∀ x ∈ charges, x ∈ charges') :
    ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges' :=
  fun x hx hnot y h3 h4 => h y <| h' x hx hnot y h3 h4

C.4. `completeMinSubset`: Minimal multiset with viable completions of top-permitting charges

For a given S5 S10 : Finset 𝓩, the minimal multiset of charges which satisfies the condition ContainsPhenoCompletionsOfMinimallyAllows. That is to say, every multiset of charges which satisfies ContainsPhenoCompletionsOfMinimallyAllows has completeMinSubset as a subset.

def completeMinSubset (S5 S10 : Finset 𝓩) : Multiset (ChargeSpectrum 𝓩) :=
  ((minimallyAllowsTermsOfFinset S5 S10 topYukawa).bind <|
      completionsTopYukawa S5).dedup.filter
    fun x => ¬ IsPhenoConstrained x ∧ ¬ YukawaGeneratesDangerousAtLevel x 1

C.4.1. The multiset `completeMinSubset` has no duplicates

lemma completeMinSubset_nodup {S5 S10 : Finset 𝓩} :
    (completeMinSubset S5 S10).Nodup := by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩⊢ (completeMinSubset S5 S10).Nodup
  simp [completeMinSubset]𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩⊢ (Multiset.filter (fun x => ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1)
    ((minimallyAllowsTermsOfFinset S5 S10 topYukawa).bind (completionsTopYukawa S5)).dedup).Nodup
  apply Multiset.Nodup.filter𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩⊢ ((minimallyAllowsTermsOfFinset S5 S10 topYukawa).bind (completionsTopYukawa S5)).dedup.Nodup
  exact Multiset.nodup_dedup
      ((minimallyAllowsTermsOfFinset S5 S10 topYukawa).bind (completionsTopYukawa S5))All goals completed! 🐙

C.4.2. The multiset `completeMinSubset` is minimal



lemma completeMinSubset_subset_iff_containsPhenoCompletionsOfMinimallyAllows
    (S5 S10 : Finset 𝓩) (charges : Multiset (ChargeSpectrum 𝓩)) :
    completeMinSubset S5 S10 ⊆ charges ↔
    ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges := by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)⊢ completeMinSubset S5 S10 ⊆ charges ↔ ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges
  constructormp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)⊢ completeMinSubset S5 S10 ⊆ charges → ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)⊢ ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges → completeMinSubset S5 S10 ⊆ charges
  ·mp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)⊢ completeMinSubset S5 S10 ⊆ charges → ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges intro hmp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:completeMinSubset S5 S10 ⊆ charges⊢ ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges
    rw [containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawamp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:completeMinSubset S5 S10 ⊆ charges⊢ ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
  ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ chargesmp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:completeMinSubset S5 S10 ⊆ charges⊢ ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
  ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges]mp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:completeMinSubset S5 S10 ⊆ charges⊢ ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
  ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges
    rw [Multiset.subset_iffmp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ ⦃x : ChargeSpectrum 𝓩⦄, x ∈ completeMinSubset S5 S10 → x ∈ charges⊢ ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
  ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ chargesmp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ ⦃x : ChargeSpectrum 𝓩⦄, x ∈ completeMinSubset S5 S10 → x ∈ charges⊢ ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
  ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges] at hmp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ ⦃x : ChargeSpectrum 𝓩⦄, x ∈ completeMinSubset S5 S10 → x ∈ charges⊢ ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
  ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges
    intro x hx y hy1 hy2mp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ ⦃x : ChargeSpectrum 𝓩⦄, x ∈ completeMinSubset S5 S10 → x ∈ chargesx:ChargeSpectrum 𝓩hx:x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukaway:ChargeSpectrum 𝓩hy1:y ∈ completionsTopYukawa S5 xhy2:¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1⊢ y ∈ charges
    apply hmp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ ⦃x : ChargeSpectrum 𝓩⦄, x ∈ completeMinSubset S5 S10 → x ∈ chargesx:ChargeSpectrum 𝓩hx:x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukaway:ChargeSpectrum 𝓩hy1:y ∈ completionsTopYukawa S5 xhy2:¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1⊢ y ∈ completeMinSubset S5 S10
    simp [completeMinSubset]mp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ ⦃x : ChargeSpectrum 𝓩⦄, x ∈ completeMinSubset S5 S10 → x ∈ chargesx:ChargeSpectrum 𝓩hx:x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukaway:ChargeSpectrum 𝓩hy1:y ∈ completionsTopYukawa S5 xhy2:¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1⊢ (∃ a ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, y ∈ completionsTopYukawa S5 a) ∧
  ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1
    simp_allmp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ ⦃x : ChargeSpectrum 𝓩⦄, x ∈ completeMinSubset S5 S10 → x ∈ chargesx:ChargeSpectrum 𝓩hx:x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukaway:ChargeSpectrum 𝓩hy1:y ∈ completionsTopYukawa S5 xhy2:¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1⊢ ∃ a ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, y ∈ completionsTopYukawa S5 a
    use xAll goals completed! 🐙
  ·mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)⊢ ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges → completeMinSubset S5 S10 ⊆ charges intro h y hympr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesy:ChargeSpectrum 𝓩hy:y ∈ completeMinSubset S5 S10⊢ y ∈ charges
    simp [completeMinSubset] at hympr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesy:ChargeSpectrum 𝓩hy:(∃ a ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, y ∈ completionsTopYukawa S5 a) ∧
  ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1⊢ y ∈ charges
    obtain ⟨⟨x, hx, hyx⟩, hy2⟩ := hympr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesy:ChargeSpectrum 𝓩hy2:¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1x:ChargeSpectrum 𝓩hx:x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahyx:y ∈ completionsTopYukawa S5 x⊢ y ∈ charges
    rw [containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawampr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
  ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ chargesy:ChargeSpectrum 𝓩hy2:¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1x:ChargeSpectrum 𝓩hx:x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahyx:y ∈ completionsTopYukawa S5 x⊢ y ∈ chargesmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
  ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ chargesy:ChargeSpectrum 𝓩hy2:¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1x:ChargeSpectrum 𝓩hx:x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahyx:y ∈ completionsTopYukawa S5 x⊢ y ∈ charges] at hmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)h:∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa,
  ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ chargesy:ChargeSpectrum 𝓩hy2:¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1x:ChargeSpectrum 𝓩hx:x ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahyx:y ∈ completionsTopYukawa S5 x⊢ y ∈ charges
    exact h x hx y hyx hy2All goals completed! 🐙

C.4.3. The multiset `completeMinSubset` contains all completions



lemma completeMinSubset_containsPhenoCompletionsOfMinimallyAllows (S5 S10 : Finset 𝓩) :
    ContainsPhenoCompletionsOfMinimallyAllows S5 S10 (completeMinSubset S5 S10) := by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩⊢ ContainsPhenoCompletionsOfMinimallyAllows S5 S10 (completeMinSubset S5 S10)
  rw [← completeMinSubset_subset_iff_containsPhenoCompletionsOfMinimallyAllows𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩⊢ completeMinSubset S5 S10 ⊆ completeMinSubset S5 S10𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩⊢ completeMinSubset S5 S10 ⊆ completeMinSubset S5 S10]𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩⊢ completeMinSubset S5 S10 ⊆ completeMinSubset S5 S10
  simpAll goals completed! 🐙

D. Multisets containing all pheno-viable charge spectra

D.1. Lemma for simplifying proof that a multiset contains all pheno-viable charge spectra

The multiset of charges charges contains precisely those charges (given a finite set of allowed charges) which

allow the top Yukawa term,

are not phenomenologically constrained,

do not generate dangerous couplings with one singlet insertion,

and are complete, if the following conditions hold:

every element of charges allows the top Yukawa term,

every element of charges is not phenomenologically constrained,

every element of charges does not generate dangerous couplings with one singlet insertion,

every element of charges is complete,

charges is IsPhenoClosedQ5 with respect to S5,

charges is IsPhenoClosedQ10 with respect to S10

and satisfies ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges. The importance of this lemma is that it is only regarding properties of finite-set charges not of the whole space of possible charges.


lemma completeness_of_isPhenoClosedQ5_isPhenoClosedQ10
    {S5 S10 : Finset 𝓩} {charges : Multiset (ChargeSpectrum 𝓩)}
    (charges_topYukawa : ∀ x ∈ charges, x.AllowsTerm .topYukawa)
    (charges_not_isPhenoConstrained : ∀ x ∈ charges, ¬ x.IsPhenoConstrained)
    (charges_yukawa : ∀ x ∈ charges, ¬ x.YukawaGeneratesDangerousAtLevel 1)
    (charges_complete : ∀ x ∈ charges, x.IsComplete)
    (charges_isPhenoClosedQ5 : IsPhenoClosedQ5 S5 charges)
    (charges_isPhenoClosedQ10 : IsPhenoClosedQ10 S10 charges)
    (charges_exist : ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges)
    {x : ChargeSpectrum 𝓩} (hsub : x ∈ ofFinset S5 S10) :
    x ∈ charges ↔ AllowsTerm x .topYukawa ∧
    ¬ IsPhenoConstrained x ∧ ¬ YukawaGeneratesDangerousAtLevel x 1 ∧ IsComplete x := by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10⊢ x ∈ charges ↔ x.AllowsTerm topYukawa ∧ ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1 ∧ x.IsComplete
  constructormp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10⊢ x ∈ charges → x.AllowsTerm topYukawa ∧ ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1 ∧ x.IsCompletempr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10⊢ x.AllowsTerm topYukawa ∧ ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1 ∧ x.IsComplete → x ∈ charges
  ·mp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10⊢ x ∈ charges → x.AllowsTerm topYukawa ∧ ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1 ∧ x.IsComplete /- Showing that if `x ∈ Charges` it satisfies the conditions. -/
    intro hmp𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10h:x ∈ charges⊢ x.AllowsTerm topYukawa ∧ ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1 ∧ x.IsComplete
    exact ⟨charges_topYukawa x h, charges_not_isPhenoConstrained x h, charges_yukawa x h,
      charges_complete x h⟩All goals completed! 🐙
  ·mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10⊢ x.AllowsTerm topYukawa ∧ ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1 ∧ x.IsComplete → x ∈ charges intro ⟨hTop, hPheno, hY, hComplete⟩mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ x ∈ charges
    /- Showing that if `x ∉ charges` and `AllowsTerm x .topYukawa`,
      `¬ IsPhenoConstrained x`, ``¬ YukawaGeneratesDangerousAtLevel x 1`, `IsComplete x`,
      then `False`. -/
    by_contra hnmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletehn:¬x ∈ charges⊢ False
    suffices hnot : ¬ ((¬ IsPhenoConstrained x ∧ ¬ YukawaGeneratesDangerousAtLevel x 1) ∧
        AllowsTerm x topYukawa) by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletehn:¬x ∈ chargeshnot:¬((¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1) ∧ x.AllowsTerm topYukawa)⊢ Falsempr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletehn:¬x ∈ charges⊢ ¬((¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1) ∧ x.AllowsTerm topYukawa)
      simp_allmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletehn:¬x ∈ charges⊢ ¬((¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1) ∧ x.AllowsTerm topYukawa)mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletehn:¬x ∈ charges⊢ ¬((¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1) ∧ x.AllowsTerm topYukawa)
    revert hnmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ¬x ∈ charges → ¬((¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1) ∧ x.AllowsTerm topYukawa)
    rw [not_andmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ¬x ∈ charges → ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1 → ¬x.AllowsTerm topYukawampr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ¬x ∈ charges → ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1 → ¬x.AllowsTerm topYukawa]mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ¬x ∈ charges → ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1 → ¬x.AllowsTerm topYukawa
    simp only [hTop, not_true_eq_false, imp_false]mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ¬x ∈ charges → ¬(¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1)
    suffices hmem : ∃ y ∈ charges, y ⊆ x by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletehmem:∃ y ∈ charges, y ⊆ x⊢ ¬x ∈ charges → ¬(¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1)mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
      obtain ⟨y, y_mem, hyx⟩ := hmem𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ x⊢ ¬x ∈ charges → ¬(¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1)mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
      refine subset_insert_filter_card_zero charges S5 S10 (fun x =>
        (¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1))
        ?_ ?_ y ?_ x hyx hsub ?_ ?_refine_1𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ x⊢ ∀ (x y : ChargeSpectrum 𝓩),
  x ⊆ y →
    ¬(¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1) →
      ¬(¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)refine_2𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ x⊢ ∀ x ∈ charges, x.IsCompleterefine_3𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ x⊢ y ∈ chargesrefine_4𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ x⊢ ∀ (q10 : ↥S10),
  Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
      (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) charges) =
    ∅refine_5𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ x⊢ ∀ (q5 : ↥S5),
  Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
      (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) charges) =
    ∅mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
      ·refine_1𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ x⊢ ∀ (x y : ChargeSpectrum 𝓩),
  x ⊆ y →
    ¬(¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1) →
      ¬(¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x simpa using fun x y hxy h1 h2 => yukawaGeneratesDangerousAtLevel_of_subset hxy <| h1
          fun hn => h2 <| isPhenoConstrained_mono hxy hnAll goals completed! 🐙mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
      ·refine_2𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ x⊢ ∀ x ∈ charges, x.IsCompletempr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x intro xrefine_2𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx✝:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xx:ChargeSpectrum 𝓩⊢ x ∈ charges → x.IsCompletempr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
        exact fun a => charges_complete x aAll goals completed! 🐙mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
      ·refine_3𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ x⊢ y ∈ chargesmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x exact y_memAll goals completed! 🐙mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
      ·refine_4𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ x⊢ ∀ (q10 : ↥S10),
  Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
      (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) charges) =
    ∅mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x intro q10refine_4𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq10:↥S10⊢ Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
    (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) charges) =
  ∅mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
        rw [Multiset.empty_eq_zero,refine_4𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq10:↥S10⊢ Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
    (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) charges) =
  0refine_4𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq10:↥S10⊢ ∀ (a : ChargeSpectrum 𝓩),
  a ∉
    Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
      (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) charges)mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x Multiset.eq_zero_iff_forall_notMemrefine_4𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq10:↥S10⊢ ∀ (a : ChargeSpectrum 𝓩),
  a ∉
    Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
      (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) charges)refine_4𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq10:↥S10⊢ ∀ (a : ChargeSpectrum 𝓩),
  a ∉
    Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
      (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) charges)mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x]refine_4𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq10:↥S10⊢ ∀ (a : ChargeSpectrum 𝓩),
  a ∉
    Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
      (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert (↑q10) x.Q10 }) charges)mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
        simp only [Multiset.mem_filter, Multiset.mem_map, not_and, Decidable.not_not,
          forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]refine_4𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq10:↥S10⊢ ∀ a ∈ charges,
  { qHd := a.qHd, qHu := a.qHu, Q5 := a.Q5, Q10 := insert (↑q10) a.Q10 } ∉ charges →
    ¬{ qHd := a.qHd, qHu := a.qHu, Q5 := a.Q5, Q10 := insert (↑q10) a.Q10 }.IsPhenoConstrained →
      { qHd := a.qHd, qHu := a.qHu, Q5 := a.Q5, Q10 := insert (↑q10) a.Q10 }.YukawaGeneratesDangerousAtLevel 1mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
        intro z hz hzP h2refine_4𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq10:↥S10z:ChargeSpectrum 𝓩hz:z ∈ chargeshzP:{ qHd := z.qHd, qHu := z.qHu, Q5 := z.Q5, Q10 := insert (↑q10) z.Q10 } ∉ chargesh2:¬{ qHd := z.qHd, qHu := z.qHu, Q5 := z.Q5, Q10 := insert (↑q10) z.Q10 }.IsPhenoConstrained⊢ { qHd := z.qHd, qHu := z.qHu, Q5 := z.Q5, Q10 := insert (↑q10) z.Q10 }.YukawaGeneratesDangerousAtLevel 1mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
        have h1 := charges_isPhenoClosedQ10 q10 q10.2 z hzrefine_4𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq10:↥S10z:ChargeSpectrum 𝓩hz:z ∈ chargeshzP:{ qHd := z.qHd, qHu := z.qHu, Q5 := z.Q5, Q10 := insert (↑q10) z.Q10 } ∉ chargesh2:¬{ qHd := z.qHd, qHu := z.qHu, Q5 := z.Q5, Q10 := insert (↑q10) z.Q10 }.IsPhenoConstrainedh1:have y := { qHd := z.qHd, qHu := z.qHu, Q5 := z.Q5, Q10 := insert (↑q10) z.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1⊢ { qHd := z.qHd, qHu := z.qHu, Q5 := z.Q5, Q10 := insert (↑q10) z.Q10 }.YukawaGeneratesDangerousAtLevel 1mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
        simp_allAll goals completed! 🐙mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
      ·refine_5𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ x⊢ ∀ (q5 : ↥S5),
  Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
      (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) charges) =
    ∅mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x intro q5refine_5𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq5:↥S5⊢ Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
    (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) charges) =
  ∅mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
        rw [Multiset.empty_eq_zero,refine_5𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq5:↥S5⊢ Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
    (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) charges) =
  0refine_5𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq5:↥S5⊢ ∀ (a : ChargeSpectrum 𝓩),
  a ∉
    Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
      (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) charges)mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x Multiset.eq_zero_iff_forall_notMemrefine_5𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq5:↥S5⊢ ∀ (a : ChargeSpectrum 𝓩),
  a ∉
    Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
      (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) charges)refine_5𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq5:↥S5⊢ ∀ (a : ChargeSpectrum 𝓩),
  a ∉
    Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
      (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) charges)mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x]refine_5𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq5:↥S5⊢ ∀ (a : ChargeSpectrum 𝓩),
  a ∉
    Multiset.filter (fun y => y ∉ charges ∧ ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1)
      (Multiset.map (fun x => { qHd := x.qHd, qHu := x.qHu, Q5 := insert (↑q5) x.Q5, Q10 := x.Q10 }) charges)mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
        simp only [Multiset.mem_filter, Multiset.mem_map, not_and, Decidable.not_not,
          forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]refine_5𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq5:↥S5⊢ ∀ a ∈ charges,
  { qHd := a.qHd, qHu := a.qHu, Q5 := insert (↑q5) a.Q5, Q10 := a.Q10 } ∉ charges →
    ¬{ qHd := a.qHd, qHu := a.qHu, Q5 := insert (↑q5) a.Q5, Q10 := a.Q10 }.IsPhenoConstrained →
      { qHd := a.qHd, qHu := a.qHu, Q5 := insert (↑q5) a.Q5, Q10 := a.Q10 }.YukawaGeneratesDangerousAtLevel 1mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
        intro z hz hzP h2refine_5𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq5:↥S5z:ChargeSpectrum 𝓩hz:z ∈ chargeshzP:{ qHd := z.qHd, qHu := z.qHu, Q5 := insert (↑q5) z.Q5, Q10 := z.Q10 } ∉ chargesh2:¬{ qHd := z.qHd, qHu := z.qHu, Q5 := insert (↑q5) z.Q5, Q10 := z.Q10 }.IsPhenoConstrained⊢ { qHd := z.qHd, qHu := z.qHu, Q5 := insert (↑q5) z.Q5, Q10 := z.Q10 }.YukawaGeneratesDangerousAtLevel 1mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
        have h1 := charges_isPhenoClosedQ5 q5 q5.2 z hzrefine_5𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩y_mem:y ∈ chargeshyx:y ⊆ xq5:↥S5z:ChargeSpectrum 𝓩hz:z ∈ chargeshzP:{ qHd := z.qHd, qHu := z.qHu, Q5 := insert (↑q5) z.Q5, Q10 := z.Q10 } ∉ chargesh2:¬{ qHd := z.qHd, qHu := z.qHu, Q5 := insert (↑q5) z.Q5, Q10 := z.Q10 }.IsPhenoConstrainedh1:have y := { qHd := z.qHd, qHu := z.qHu, Q5 := insert (↑q5) z.Q5, Q10 := z.Q10 };
y.IsPhenoConstrained ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1⊢ { qHd := z.qHd, qHu := z.qHu, Q5 := insert (↑q5) z.Q5, Q10 := z.Q10 }.YukawaGeneratesDangerousAtLevel 1mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
        simp_allmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ xmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ charges, y ⊆ x
    /- Getting the subset of `x` which minimally allows the top Yukawa. -/
    obtain ⟨y, hyMem, hysubsetx⟩ : ∃ y ∈ (minimallyAllowsTermsOfFinset S5 S10 topYukawa),
        y ⊆ x := by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, y ⊆ xmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x
      rw [allowsTerm_iff_subset_minimallyAllowsTerm𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:∃ y ∈ x.powerset, y.MinimallyAllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, y ⊆ x𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:∃ y ∈ x.powerset, y.MinimallyAllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, y ⊆ xmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x] at hTop𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:∃ y ∈ x.powerset, y.MinimallyAllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsComplete⊢ ∃ y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, y ⊆ xmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x
      obtain ⟨y, hPower, hIrre⟩ := hTop𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ ∃ y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa, y ⊆ xmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x
      use yh𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawa ∧ y ⊆ xmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x
      constructorh.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawah.right𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y ⊆ xmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x
      ·h.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawampr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x rw [← minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinseth.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y.MinimallyAllowsTerm topYukawah.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y ∈ ofFinset S5 S10h.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y.MinimallyAllowsTerm topYukawah.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y ∈ ofFinset S5 S10mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x]h.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y.MinimallyAllowsTerm topYukawah.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y ∈ ofFinset S5 S10mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x
        ·h.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y.MinimallyAllowsTerm topYukawampr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x exact hIrreAll goals completed! 🐙mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x
        ·h.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y ∈ ofFinset S5 S10mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x exact mem_ofFinset_antitone S5 S10 (by𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y ⊆ xmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x simpa using hPowerAll goals completed! 🐙mpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x) hsub
      ·h.right𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hPower:y ∈ x.powersethIrre:y.MinimallyAllowsTerm topYukawa⊢ y ⊆ xmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x simpa using hPowermpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ xmpr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ x⊢ ∃ y ∈ charges, y ⊆ x
    obtain ⟨z, hz1, hz2⟩ := exist_completions_subset_of_complete S5 S10 y x hysubsetx hsub hCompletempr𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ ∃ y ∈ charges, y ⊆ x
    use zh𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ z ∈ charges ∧ z ⊆ x
    constructorh.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ z ∈ chargesh.right𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ z ⊆ x
    ·h.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ z ∈ charges refine charges_exist y hyMem ?_ z hz1 ?_h.left.refine_1𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ ¬y.IsPhenoConstrainedh.left.refine_2𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ ¬z.IsPhenoConstrained ∧ ¬z.YukawaGeneratesDangerousAtLevel 1
      ·h.left.refine_1𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ ¬y.IsPhenoConstrained by_contra hnh.left.refine_1𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ xhn:y.IsPhenoConstrained⊢ False
        have := isPhenoConstrained_mono hysubsetx hnh.left.refine_1𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ xhn:y.IsPhenoConstrainedthis:x.IsPhenoConstrained⊢ False
        simp_allAll goals completed! 🐙
      ·h.left.refine_2𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ ¬z.IsPhenoConstrained ∧ ¬z.YukawaGeneratesDangerousAtLevel 1 apply And.introh.left.refine_2.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ ¬z.IsPhenoConstrainedh.left.refine_2.right𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ ¬z.YukawaGeneratesDangerousAtLevel 1
        ·h.left.refine_2.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ ¬z.IsPhenoConstrained by_contra hnh.left.refine_2.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ xhn:z.IsPhenoConstrained⊢ False
          have := isPhenoConstrained_mono hz2 hnh.left.refine_2.left𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ xhn:z.IsPhenoConstrainedthis:x.IsPhenoConstrained⊢ False
          simp_allAll goals completed! 🐙
        ·h.left.refine_2.right𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ ¬z.YukawaGeneratesDangerousAtLevel 1 by_contra hnh.left.refine_2.right𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ xhn:z.YukawaGeneratesDangerousAtLevel 1⊢ False
          have := yukawaGeneratesDangerousAtLevel_of_subset hz2 hnh.left.refine_2.right𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ xhn:z.YukawaGeneratesDangerousAtLevel 1this:x.YukawaGeneratesDangerousAtLevel 1⊢ False
          simp_allAll goals completed! 🐙
    ·h.right𝓩:Typeinst✝¹:DecidableEq 𝓩inst✝:AddCommGroup 𝓩S5:Finset 𝓩S10:Finset 𝓩charges:Multiset (ChargeSpectrum 𝓩)charges_topYukawa:∀ x ∈ charges, x.AllowsTerm topYukawacharges_not_isPhenoConstrained:∀ x ∈ charges, ¬x.IsPhenoConstrainedcharges_yukawa:∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1charges_complete:∀ x ∈ charges, x.IsCompletecharges_isPhenoClosedQ5:IsPhenoClosedQ5 S5 chargescharges_isPhenoClosedQ10:IsPhenoClosedQ10 S10 chargescharges_exist:ContainsPhenoCompletionsOfMinimallyAllows S5 S10 chargesx:ChargeSpectrum 𝓩hsub:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahPheno:¬x.IsPhenoConstrainedhY:¬x.YukawaGeneratesDangerousAtLevel 1hComplete:x.IsCompletey:ChargeSpectrum 𝓩hyMem:y ∈ minimallyAllowsTermsOfFinset S5 S10 topYukawahysubsetx:y ⊆ xz:ChargeSpectrum 𝓩hz1:z ∈ completions S5 S10 yhz2:z ⊆ x⊢ z ⊆ x simp_allAll goals completed! 🐙

D.2. Computable multiset containing all pheno-viable charge spectra

TODO "Make the result `viableChargesMultiset` a safe definition, that is to
  say proof that the recursion terminates."

All charges, for a given S5 S10 : Finset 𝓩, which permit a top Yukawa coupling, are not phenomenologically constrained, and do not regenerate dangerous couplings with one insertion of a Yukawa coupling.

This is the unique multiset without duplicates which satisfies: completeness_of_isPhenoClosedQ5_isPhenoClosedQ10.

Note this is fast for evaluation, but to slow with decide.

Auxiliary recursive function to define viableChargesMultiset.

unsafe def viableChargesMultiset (S5 S10 : Finset 𝓩) :
    Multiset (ChargeSpectrum 𝓩) := (aux (completeMinSubset S5 S10) (completeMinSubset S5 S10)).dedup
where

  aux : Multiset (ChargeSpectrum 𝓩) → Multiset (ChargeSpectrum 𝓩) → Multiset (ChargeSpectrum 𝓩) :=
    fun all add =>
      /- Note that aux terminates since that every iteration the size of `all` increases,
        unless it terminates that round, but `all` is bounded in size by the number
        of allowed charges given `S5` and `S10`. -/
      if add = ∅ then all else
      let s := add.bind fun x => (minimalSuperSet S5 S10 x).val
      let s2 := s.filter fun y => y ∉ all ∧
        ¬ IsPhenoConstrained y ∧ ¬ YukawaGeneratesDangerousAtLevel y 1
      aux (all + s2) s2

Phenomenologically closed sets of charge spectra

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. Phenomenologically closed under additions of 5-bar charges

A.1. Simplification using pheno-constrained due to additional of 5-bar charge

B. Phenomenologically closed under additions of 10d charges

B.1. Simplification using pheno-constrained due to additional of 10d charge

C. Prop for multiset containing all pheno-viable completions of charges permitting top Yukawa

C.1. Simplification using fast version of completions of charges permitting top Yukawa

C.2. Decidability of proposition

C.3. Monotonicity of proposition

C.4. completeMinSubset: Minimal multiset with viable completions of top-permitting charges

C.4.1. The multiset completeMinSubset has no duplicates

C.4.2. The multiset completeMinSubset is minimal

C.4.3. The multiset completeMinSubset contains all completions

D. Multisets containing all pheno-viable charge spectra

D.1. Lemma for simplifying proof that a multiset contains all pheno-viable charge spectra

D.2. Computable multiset containing all pheno-viable charge spectra

C.4. `completeMinSubset`: Minimal multiset with viable completions of top-permitting charges

C.4.1. The multiset `completeMinSubset` has no duplicates

C.4.2. The multiset `completeMinSubset` is minimal

C.4.3. The multiset `completeMinSubset` contains all completions