Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.FinsetTerms

Imports

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

public import Mathlib.Tactic.FinCases
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.Basic

Minimally allows a set of terms

i. Overview

In this module we consider those charge spectra which minimally allow a finite set of potential terms. That is, they those charge spectra which allow each term in the set, but no proper subset of the charge spectra allows each term in that set.

We have special focus on those charge spectra which minimally allow a top and bottom Yukawa term.

ii. Key results

MinimallyAllowsFinsetTerms: the proposition that a charge spectrum minimally allows a given finite set of potential terms.

minTopBottom: a finite set of charge spectra which contains every charge spectrum which minimally allows a top and bottom Yukawa term, given finite sets of possible 5-bar and 10 charges.

iii. Table of contents

A. Charge spectra which minimally allow a finite set of potential terms

A.1. MinimallyAllowsFinsetTerms: Prop of minimally allowing a finset of potential terms

A.2. The prop MinimallyAllowsFinsetTerms is decidable

A.3. Every element of MinimallyAllowsFinsetTerms allows each term in the finset

A.4. MinimallyAllowsFinsetTerms for the singleton set is equivalent to MinimallyAllowsTerm

B. Minimally allowing the top and bottom Yukawa

B.1. Finset of charge spectra containing those which minimally allow top and bottom Yukawa

B.2. Every element of minTopBottom allows a top Yukawa

B.3. Every element of minTopBottom allows a bottom Yukawa

B.4. Every charge spectrum minimally allowing a top and bottom Yukawa in minTopBottom

iv. References

There are no references for this module.

@[expose] public section

A. Charge spectra which minimally allow a finite set of potential terms

We start by defining the proposition that a charge spectrum minimally allows a finite set of potential terms, and prove some basic properties there of.

A.1. `MinimallyAllowsFinsetTerms`: Prop of minimally allowing a finset of potential terms

A collection of charge spectra is said to minimally allow a finite set of potential terms Ts if it allows all terms in Ts and no strict subset of it allows all terms in Ts.

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

A.2. The prop `MinimallyAllowsFinsetTerms` is decidable

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

A.3. Every element of `MinimallyAllowsFinsetTerms` allows each term in the finset

lemma allowsTerm_of_minimallyAllowsFinsetTerms {T : PotentialTerm}
    (h : x.MinimallyAllowsFinsetTerms Ts) (hT : T ∈ Ts) : x.AllowsTerm T :=
  (h x (self_mem_powerset x)).mp rfl T hT

A.4. `MinimallyAllowsFinsetTerms` for the singleton set is equivalent to `MinimallyAllowsTerm`

@[simp]
lemma minimallyAllowsFinsetTerms_singleton {T : PotentialTerm} :
    x.MinimallyAllowsFinsetTerms {T} ↔ x.MinimallyAllowsTerm T := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩T:PotentialTerm⊢ x.MinimallyAllowsFinsetTerms {T} ↔ x.MinimallyAllowsTerm T
  simp [MinimallyAllowsFinsetTerms, MinimallyAllowsTerm]All goals completed! 🐙

B. Minimally allowing the top and bottom Yukawa

We now consider the special case of those charge spectra which minimally allow a top and bottom Yukawa term.

We construct a finite set of such charge spectra given finite sets of possible 5-bar and 10 charges which contains every charge spectrum which minimally allows a top and bottom Yukawa term.

B.1. Finset of charge spectra containing those which minimally allow top and bottom Yukawa

Here we define minTopBottom in a way which is computationally efficient.

The set of charges of the form (qHd, qHu, {q5}, {-qHd-q5, q10, qHu - q10}) This includes every charge which minimally allows for the top and bottom Yukawas.

def minTopBottom (S5 S10 : Finset 𝓩) : Multiset (ChargeSpectrum 𝓩) := Multiset.dedup <|
  (S5.val ×ˢ S5.val ×ˢ S5.val ×ˢ S10.val).map
    (fun x => ⟨x.1, x.2.1, {x.2.2.1}, {- x.1 - x.2.2.1, x.2.2.2, x.2.1 - x.2.2.2}⟩)

B.2. Every element of `minTopBottom` allows a top Yukawa

lemma allowsTerm_topYukawa_of_mem_minTopBottom {S5 S10 : Finset 𝓩}
    {x : ChargeSpectrum 𝓩} (h : x ∈ minTopBottom S5 S10) :
    x.AllowsTerm topYukawa := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h:x ∈ minTopBottom S5 S10⊢ x.AllowsTerm topYukawa
  simp [minTopBottom] at h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h:∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } = x⊢ x.AllowsTerm topYukawa
  obtain ⟨qHd, qHu, q5, q10, _, rfl⟩ := h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩q5:𝓩q10:𝓩left✝:qHd ∈ S5 ∧ qHu ∈ S5 ∧ q5 ∈ S5 ∧ q10 ∈ S10⊢ { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} }.AllowsTerm topYukawa
  simp [allowsTerm_iff_subset_allowsTermForm, allowsTermForm, subset_def]𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩q5:𝓩q10:𝓩left✝:qHd ∈ S5 ∧ qHu ∈ S5 ∧ q5 ∈ S5 ∧ q10 ∈ S10⊢ ∃ a, -a = qHu ∧ ∃ x, {x, -a - x} ⊆ {-qHd - q5, q10, qHu - q10}
  exact ⟨-qHu, by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩q5:𝓩q10:𝓩left✝:qHd ∈ S5 ∧ qHu ∈ S5 ∧ q5 ∈ S5 ∧ q10 ∈ S10⊢ - -qHu = qHu simpAll goals completed! 🐙, q10, by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩q5:𝓩q10:𝓩left✝:qHd ∈ S5 ∧ qHu ∈ S5 ∧ q5 ∈ S5 ∧ q10 ∈ S10⊢ {q10, - -qHu - q10} ⊆ {-qHd - q5, q10, qHu - q10} simpAll goals completed! 🐙⟩

B.3. Every element of `minTopBottom` allows a bottom Yukawa

lemma allowsTerm_bottomYukawa_of_mem_minTopBottom {S5 S10 : Finset 𝓩}
    {x : ChargeSpectrum 𝓩} (h : x ∈ minTopBottom S5 S10) :
    x.AllowsTerm bottomYukawa := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h:x ∈ minTopBottom S5 S10⊢ x.AllowsTerm bottomYukawa
  simp [minTopBottom] at h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩x:ChargeSpectrum 𝓩h:∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } = x⊢ x.AllowsTerm bottomYukawa
  obtain ⟨qHd, qHu, q5, q10, _, rfl⟩ := h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩q5:𝓩q10:𝓩left✝:qHd ∈ S5 ∧ qHu ∈ S5 ∧ q5 ∈ S5 ∧ q10 ∈ S10⊢ { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} }.AllowsTerm bottomYukawa
  simp [allowsTerm_iff_subset_allowsTermForm, allowsTermForm, subset_def]All goals completed! 🐙

B.4. Every charge spectrum minimally allowing a top and bottom Yukawa in `minTopBottom`



lemma mem_minTopBottom_of_minimallyAllowsFinsetTerms
    {x : ChargeSpectrum 𝓩} {S5 S10 : Finset 𝓩}
    (h : x.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa})
    (hx : x ∈ ofFinset S5 S10) :
    x ∈ minTopBottom S5 S10 := by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩h:x.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:x ∈ ofFinset S5 S10⊢ x ∈ minTopBottom S5 S10
  simp [minTopBottom]𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩h:x.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:x ∈ ofFinset S5 S10⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } = x
  have hTop : x.AllowsTerm topYukawa := allowsTerm_of_minimallyAllowsFinsetTerms h (by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩h:x.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:x ∈ ofFinset S5 S10⊢ topYukawa ∈ {topYukawa, bottomYukawa}𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩h:x.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawa⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } = x simpAll goals completed! 🐙𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩h:x.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawa⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } = x)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩h:x.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawa⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } = x
  have hBottom : x.AllowsTerm bottomYukawa := allowsTerm_of_minimallyAllowsFinsetTerms h (by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩h:x.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawa⊢ bottomYukawa ∈ {topYukawa, bottomYukawa}𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩h:x.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahBottom:x.AllowsTerm bottomYukawa⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } = x simpAll goals completed! 🐙𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩h:x.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahBottom:x.AllowsTerm bottomYukawa⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } = x)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩h:x.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:x ∈ ofFinset S5 S10hTop:x.AllowsTerm topYukawahBottom:x.AllowsTerm bottomYukawa⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } = x
  match x with
  | ⟨none, qHu, Q5, Q10⟩ =>𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := none, qHu := qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:{ qHd := none, qHu := qHu, Q5 := Q5, Q10 := Q10 } ∈ ofFinset S5 S10hTop:{ qHd := none, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm topYukawahBottom:{ qHd := none, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm bottomYukawa⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } =
      { qHd := none, qHu := qHu, Q5 := Q5, Q10 := Q10 }
    simp [allowsTerm_iff_subset_allowsTermForm, allowsTermForm, subset_def] at hBottomAll goals completed! 🐙
  | ⟨qHd, none, Q5, Q10⟩ =>𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:{ qHd := qHd, qHu := none, Q5 := Q5, Q10 := Q10 } ∈ ofFinset S5 S10hTop:{ qHd := qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.AllowsTerm topYukawahBottom:{ qHd := qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.AllowsTerm bottomYukawa⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } =
      { qHd := qHd, qHu := none, Q5 := Q5, Q10 := Q10 }
    simp [allowsTerm_iff_subset_allowsTermForm, allowsTermForm, subset_def] at hTopAll goals completed! 🐙
  | ⟨some qHd, some qHu, Q5, Q10⟩ =>𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 } ∈ ofFinset S5 S10hTop:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm topYukawahBottom:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm bottomYukawa⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } =
      { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }
  simp [allowsTerm_iff_subset_allowsTermForm, allowsTermForm, subset_def] at hTop hBottom𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 } ∈ ofFinset S5 S10hTop:∃ a, -a = qHu ∧ ∃ x, {x, -a - x} ⊆ Q10hBottom:∃ x ∈ Q5, -qHd - x ∈ Q10⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } =
      { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }
  obtain ⟨n, hn, q10, h10⟩ := hTop𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 } ∈ ofFinset S5 S10hBottom:∃ x ∈ Q5, -qHd - x ∈ Q10n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } =
      { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }
  obtain ⟨q5, h5⟩ := hBottom𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 } ∈ ofFinset S5 S10n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10⊢ ∃ a a_1 a_2 b,
  (a ∈ S5 ∧ a_1 ∈ S5 ∧ a_2 ∈ S5 ∧ b ∈ S10) ∧
    { qHd := some a, qHu := some a_1, Q5 := {a_2}, Q10 := {-a - a_2, b, a_1 - b} } =
      { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }
  use qHd, qHu, q5, q10h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}hx:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 } ∈ ofFinset S5 S10n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10⊢ (qHd ∈ S5 ∧ qHu ∈ S5 ∧ q5 ∈ S5 ∧ q10 ∈ S10) ∧
  { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} } =
    { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }
  simp [mem_ofFinset_iff] at hxh𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ (qHd ∈ S5 ∧ qHu ∈ S5 ∧ q5 ∈ S5 ∧ q10 ∈ S10) ∧
  { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} } =
    { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }
  refine ⟨⟨hx.1, hx.2.1, hx.2.2.1 h5.1, hx.2.2.2 (h10 (Finset.mem_insert_self _ _))⟩, ?_⟩h𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} } =
  { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }
  refine (h _ ?_).mpr ?_h.refine_1𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} } ∈
  { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.powerseth.refine_2𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ ∀ T ∈ {topYukawa, bottomYukawa},
  { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} }.AllowsTerm T
  ·h.refine_1𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} } ∈
  { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.powerset simp [subset_def]h.refine_1𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ q5 ∈ Q5 ∧ {-qHd - q5, q10, qHu - q10} ⊆ Q10
    exact ⟨h5.1, Finset.insert_subset h5.2 (hn ▸ h10)⟩All goals completed! 🐙
  ·h.refine_2𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ ∀ T ∈ {topYukawa, bottomYukawa},
  { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} }.AllowsTerm T intro T hTh.refine_2𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10T:PotentialTermhT:T ∈ {topYukawa, bottomYukawa}⊢ { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} }.AllowsTerm T
    fin_cases hTh.refine_2.«0»𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} }.AllowsTerm topYukawah.refine_2.«1»𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} }.AllowsTerm bottomYukawa
    ·h.refine_2.«0»𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} }.AllowsTerm topYukawa simp [allowsTerm_iff_subset_allowsTermForm, allowsTermForm, subset_def]h.refine_2.«0»𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ ∃ a, -a = qHu ∧ ∃ x, {x, -a - x} ⊆ {-qHd - q5, q10, qHu - q10}
      exact ⟨-qHu, by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ - -qHu = qHu simpAll goals completed! 🐙, q10, by𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ {q10, - -qHu - q10} ⊆ {-qHd - q5, q10, qHu - q10} simpAll goals completed! 🐙⟩
    ·h.refine_2.«1»𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩S5:Finset 𝓩S10:Finset 𝓩qHd:𝓩qHu:𝓩Q5:Finset 𝓩Q10:Finset 𝓩h:{ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa}n:𝓩hn:-n = qHuq10:𝓩h10:{q10, -n - q10} ⊆ Q10q5:𝓩h5:q5 ∈ Q5 ∧ -qHd - q5 ∈ Q10hx:qHd ∈ S5 ∧ qHu ∈ S5 ∧ Q5 ⊆ S5 ∧ Q10 ⊆ S10⊢ { qHd := some qHd, qHu := some qHu, Q5 := {q5}, Q10 := {-qHd - q5, q10, qHu - q10} }.AllowsTerm bottomYukawa simp [allowsTerm_iff_subset_allowsTermForm, allowsTermForm, subset_def]All goals completed! 🐙

Minimally allows a set of terms

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. Charge spectra which minimally allow a finite set of potential terms

A.1. MinimallyAllowsFinsetTerms: Prop of minimally allowing a finset of potential terms

A.2. The prop MinimallyAllowsFinsetTerms is decidable

A.3. Every element of MinimallyAllowsFinsetTerms allows each term in the finset

A.4. MinimallyAllowsFinsetTerms for the singleton set is equivalent to MinimallyAllowsTerm

B. Minimally allowing the top and bottom Yukawa

B.1. Finset of charge spectra containing those which minimally allow top and bottom Yukawa

B.2. Every element of minTopBottom allows a top Yukawa

B.3. Every element of minTopBottom allows a bottom Yukawa

B.4. Every charge spectrum minimally allowing a top and bottom Yukawa in minTopBottom

A.1. `MinimallyAllowsFinsetTerms`: Prop of minimally allowing a finset of potential terms

A.2. The prop `MinimallyAllowsFinsetTerms` is decidable

A.3. Every element of `MinimallyAllowsFinsetTerms` allows each term in the finset

A.4. `MinimallyAllowsFinsetTerms` for the singleton set is equivalent to `MinimallyAllowsTerm`

B.2. Every element of `minTopBottom` allows a top Yukawa

B.3. Every element of `minTopBottom` allows a bottom Yukawa

B.4. Every charge spectrum minimally allowing a top and bottom Yukawa in `minTopBottom`