Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.Basic
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoConstrainedThe set of charges which minimally allows a potential term
i. Overview
In this module given finite sets for the 5-bar and 10d charges S5 and S10
we find the sets of charge spectra which minimally allowed a potential term T.
The set we will actually define will be a multiset, for computational
efficiency (using multisets saves Lean having to manually check for duplicates,
which can be very costly)
To do this we define some auxiliary results which create multisets of a given cardinality from a finset.
ii. Key results
minimallyAllowsTermsOfFinset S5 S10 T : the multiset of all charge spectra
with charges in S5 and S10 which minimally allow the potential term T.
minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinset : the
statement that minimallyAllowsTermsOfFinset S5 S10 T contains exactly the charge spectra
with charges in S5 and S10 which minimally allow the potential term T.
iii. Table of contents
A. Construction of set of charges which minimally allow a potential term
A.1. Preliminary: Multisets from finite sets
A.1.1. Multisets of cardinality 1
A.1.2. Multisets of cardinality 2
A.1.3. Multisets of cardinality 3
A.2. minimallyAllowsTermsOfFinset: the set of charges which minimally allow a potential term
A.3. Showing minimallyAllowsTermsOfFinset has charges in given sets
B. Proving the minimallyAllowsTermsOfFinset is set of charges which minimally allow a term
B.1. An element of minimallyAllowsTermsOfFinset is of the form allowsTermForm
B.2. Every element of minimallyAllowsTermsOfFinset allows the term
B.3. Every element of minimallyAllowsTermsOfFinset minimally allows the term
B.4. Every charge spectra which minimally allows term is in minimallyAllowsTermsOfFinset
B.5. In minimallyAllowsTermsOfFinset iff minimally allowing term
C. Other properties of minimallyAllowsTermsOfFinset
C.1. Monotonicity of minimallyAllowsTermsOfFinset in allowed sets of charges
C.2. Not phenomenologically constrained if in minimallyAllowsTermsOfFinset for topYukawa
iv. References
There are no known references for the material in this module.
@[expose] public sectionA. Construction of set of charges which minimally allow a potential term
We start with the construction of the set of charges which minimally allow a potential term,
and then later prover properties about this set.
The set we will define is minimallyAllowsTermsOfFinset, the construction of
which relies on some preliminary results.
A.1. Preliminary: Multisets from finite sets
We construct the multisets of cardinality 1, 2 and 3 which
contain elements of finite set s.
A.1.1. Multisets of cardinality 1
The multisets of cardinality 1 containing elements from a finite set s.
def toMultisetsOne (s : Finset π©) : Multiset (Multiset π©) :=
let X1 := (s.powersetCard 1).val.map fun X => X.val
X1@[simp]
lemma mem_toMultisetsOne_iff [DecidableEq π©] {s : Finset π©} (X : Multiset π©) :
X β toMultisetsOne s β X.toFinset β s β§ X.card = 1 := π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©β’ X β toMultisetsOne s β X.toFinset β s β§ X.card = 1
All goals completed! π
A.1.2. Multisets of cardinality 2
The multisets of cardinality 2 containing elements from a finite set s.
def toMultisetsTwo (s : Finset π©) : Multiset (Multiset π©) :=
let X1 := (s.powersetCard 1).val.map (fun X => X.val.bind (fun x => Multiset.replicate 2 x))
let X2 := (s.powersetCard 2).val.map fun X => X.val
X1 + X2@[simp]
lemma mem_toMultisetsTwo_iff [DecidableEq π©] {s : Finset π©} (X : Multiset π©) :
X β toMultisetsTwo s β X.toFinset β s β§ X.card = 2 := π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©β’ X β toMultisetsTwo s β X.toFinset β s β§ X.card = 2
π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©β’ (β a, (a β s β§ a.card = 1) β§ a.val + a.val.bind singleton = X) β¨ X β€ s.val β§ X.card = 2 β X.toFinset β s β§ X.card = 2
π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©β’ (β a, (a β s β§ a.card = 1) β§ a.val + a.val.bind singleton = X) β¨ X β€ s.val β§ X.card = 2 β X.toFinset β s β§ X.card = 2π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©β’ X.toFinset β s β§ X.card = 2 β (β a, (a β s β§ a.card = 1) β§ a.val + a.val.bind singleton = X) β¨ X β€ s.val β§ X.card = 2
π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©β’ (β a, (a β s β§ a.card = 1) β§ a.val + a.val.bind singleton = X) β¨ X β€ s.val β§ X.card = 2 β X.toFinset β s β§ X.card = 2 π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©h:(β a, (a β s β§ a.card = 1) β§ a.val + a.val.bind singleton = X) β¨ X β€ s.val β§ X.card = 2β’ X.toFinset β s β§ X.card = 2
π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©a:Finset π©hbind:a.val + a.val.bind singleton = Xhasub:a β shacard:a.card = 1β’ X.toFinset β s β§ X.card = 2π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©h1:X β€ s.valhcard:X.card = 2β’ X.toFinset β s β§ X.card = 2
π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©a:Finset π©hbind:a.val + a.val.bind singleton = Xhasub:a β shacard:a.card = 1β’ X.toFinset β s β§ X.card = 2 π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©a:π©hbind:{a}.val + {a}.val.bind singleton = Xhasub:{a} β shacard:{a}.card = 1β’ X.toFinset β s β§ X.card = 2
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©hasub:{a} β shacard:{a}.card = 1β’ ({a}.val + {a}.val.bind singleton).toFinset β s β§ ({a}.val + {a}.val.bind singleton).card = 2
All goals completed! π
π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©h1:X β€ s.valhcard:X.card = 2β’ X.toFinset β s β§ X.card = 2 All goals completed! π
π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©β’ X.toFinset β s β§ X.card = 2 β (β a, (a β s β§ a.card = 1) β§ a.val + a.val.bind singleton = X) β¨ X β€ s.val β§ X.card = 2 π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©hsub:X.toFinset β shcard:X.card = 2β’ (β a, (a β s β§ a.card = 1) β§ a.val + a.val.bind singleton = X) β¨ X β€ s.val β§ X.card = 2
π©:Typeinstβ:DecidableEq π©s:Finset π©X:Multiset π©hsub:X.toFinset β shcard:X.card = 2β’ (β a, (a β s β§ a.card = 1) β§ a.val + a.val.bind singleton = X) β¨ X β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hsub:{a, b}.toFinset β shcard:{a, b}.card = 2β’ (β a_1, (a_1 β s β§ a_1.card = 1) β§ a_1.val + a_1.val.bind singleton = {a, b}) β¨ {a, b} β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hsub:{a, b}.toFinset β shcard:{a, b}.card = 2hab:a = bβ’ (β a_1, (a_1 β s β§ a_1.card = 1) β§ a_1.val + a_1.val.bind singleton = {a, b}) β¨ {a, b} β€ s.valπ©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hsub:{a, b}.toFinset β shcard:{a, b}.card = 2hab:Β¬a = bβ’ (β a_1, (a_1 β s β§ a_1.card = 1) β§ a_1.val + a_1.val.bind singleton = {a, b}) β¨ {a, b} β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hsub:{a, b}.toFinset β shcard:{a, b}.card = 2hab:a = bβ’ (β a_1, (a_1 β s β§ a_1.card = 1) β§ a_1.val + a_1.val.bind singleton = {a, b}) β¨ {a, b} β€ s.val π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©hsub:{a, a}.toFinset β shcard:{a, a}.card = 2β’ (β a_1, (a_1 β s β§ a_1.card = 1) β§ a_1.val + a_1.val.bind singleton = {a, a}) β¨ {a, a} β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©hsub:{a, a}.toFinset β shcard:{a, a}.card = 2β’ β a_1, (a_1 β s β§ a_1.card = 1) β§ a_1.val + a_1.val.bind singleton = {a, a}
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©hsub:{a, a}.toFinset β shcard:{a, a}.card = 2β’ ({a} β s β§ {a}.card = 1) β§ {a}.val + {a}.val.bind singleton = {a, a}
All goals completed! π
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hsub:{a, b}.toFinset β shcard:{a, b}.card = 2hab:Β¬a = bβ’ (β a_1, (a_1 β s β§ a_1.card = 1) β§ a_1.val + a_1.val.bind singleton = {a, b}) β¨ {a, b} β€ s.val π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hsub:{a, b}.toFinset β shcard:{a, b}.card = 2hab:Β¬a = bβ’ {a, b} β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hsub:{a, b}.toFinset β shcard:{a, b}.card = 2hab:Β¬a = bβ’ {a, b}.Nodupπ©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hsub:{a, b}.toFinset β shcard:{a, b}.card = 2hab:Β¬a = bβ’ {a, b} β s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hsub:{a, b}.toFinset β shcard:{a, b}.card = 2hab:Β¬a = bβ’ {a, b}.Nodup All goals completed! π
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hsub:{a, b}.toFinset β shcard:{a, b}.card = 2hab:Β¬a = bβ’ {a, b} β s.val All goals completed! π
A.1.3. Multisets of cardinality 3
The multisets of cardinality 3 containing elements from a finite set s.
def toMultisetsThree [DecidableEq π©] (s : Finset π©) : Multiset (Multiset π©) :=
let X1 := (s.powersetCard 1).val.map (fun X => X.val.bind (fun x => Multiset.replicate 3 x))
let X2 := s.val.bind (fun x => (s \ {x}).val.map (fun y => {x} + Multiset.replicate 2 y))
let X3 := (s.powersetCard 3).val.map fun X => X.val
X1 + X2 + X3π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bβ’ (β a_1, (a_1 β s β§ a_1.card = 1) β§ a_1.val + (a_1.val + a_1.val.bind singleton) = {a, b, c}) β¨
(β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, c}) β¨ {a, b, c} β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bβ’ (β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, c}) β¨ {a, b, c} β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:a = cβ’ (β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, c}) β¨ {a, b, c} β€ s.valπ©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:Β¬a = cβ’ (β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, c}) β¨ {a, b, c} β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:a = cβ’ (β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, c}) β¨ {a, b, c} β€ s.val π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hab:Β¬a = bhsub:{a, b, a}.toFinset β shcard:{a, b, a}.card = 3β’ (β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, a}) β¨ {a, b, a} β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hab:Β¬a = bhcard:{a, b, a}.card = 3hsub:b β s β§ a β sβ’ (β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, a}) β¨ {a, b, a} β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hab:Β¬a = bhcard:{a, b, a}.card = 3hsub:b β s β§ a β sβ’ β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, a}
All goals completed! π
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:Β¬a = cβ’ (β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, c}) β¨ {a, b, c} β€ s.val π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:Β¬a = chbc:b = cβ’ (β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, c}) β¨ {a, b, c} β€ s.valπ©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:Β¬a = chbc:Β¬b = cβ’ (β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, c}) β¨ {a, b, c} β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:Β¬a = chbc:b = cβ’ (β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, c}) β¨ {a, b, c} β€ s.val π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hab:Β¬a = bhsub:{a, b, b}.toFinset β shcard:{a, b, b}.card = 3hac:Β¬a = bβ’ (β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, b}) β¨ {a, b, b} β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hab:Β¬a = bhsub:{a, b, b}.toFinset β shcard:{a, b, b}.card = 3hac:Β¬a = bβ’ β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, b}
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hab:Β¬a = bhcard:{a, b, b}.card = 3hac:Β¬a = bhsub:a β s β§ b β sβ’ β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, b}
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©hab:Β¬a = bhcard:{a, b, b}.card = 3hac:Β¬a = bhsub:a β s β§ b β sβ’ b ::β a ::β {b} = {a, b, b}
All goals completed! π
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:Β¬a = chbc:Β¬b = cβ’ (β a_1 β s, β a_2 β s.val.erase a_1, a_2 ::β a_1 ::β {a_2} = {a, b, c}) β¨ {a, b, c} β€ s.val π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:Β¬a = chbc:Β¬b = cβ’ {a, b, c} β€ s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:Β¬a = chbc:Β¬b = cβ’ {a, b, c}.Nodupπ©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:Β¬a = chbc:Β¬b = cβ’ {a, b, c} β s.val
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:Β¬a = chbc:Β¬b = cβ’ {a, b, c}.Nodup All goals completed! π
π©:Typeinstβ:DecidableEq π©s:Finset π©a:π©b:π©c:π©hsub:{a, b, c}.toFinset β shcard:{a, b, c}.card = 3hab:Β¬a = bhac:Β¬a = chbc:Β¬b = cβ’ {a, b, c} β s.val All goals completed! π
A.2. minimallyAllowsTermsOfFinset: the set of charges which minimally allow a potential term
Given the construction of the multisets above we can now define the set of charges which minimally allow a potential term.
We will prove it has the desired properties later in this module.
The multiset of all charges within ofFinset S5 S10 which minimally allow the
potential term T.
def minimallyAllowsTermsOfFinset (S5 S10 : Finset π©) :
(T : PotentialTerm) β Multiset (ChargeSpectrum π©)
| ΞΌ =>
let SqHd := S5.val
let SqHu := S5.val
let prod := SqHd ΓΛ’ (SqHu)
let Filt := prod.filter (fun x => - x.1 + x.2 = 0)
(Filt.map (fun x => β¨x.1, x.2, β
, β
β©))
| K2 =>
let SqHd := S5.val
let SqHu := S5.val
let Q10 := toMultisetsOne S10
let prod := SqHd ΓΛ’ (SqHu ΓΛ’ Q10)
let Filt := prod.filter (fun x => x.1 + x.2.1 + x.2.2.sum = 0)
(Filt.map (fun x => β¨x.1, x.2.1, β
, x.2.2.toFinsetβ©))
| K1 =>
let Q5 := toMultisetsOne S5
let Q10 := toMultisetsTwo S10
let Prod := Q5 ΓΛ’ Q10
let Filt := Prod.filter (fun x => - x.1.sum + x.2.sum = 0)
(Filt.map (fun x => β¨none, none, x.1.toFinset, x.2.toFinsetβ©))
| W4 =>
let SqHd := S5.val
let SqHu := S5.val
let Q5 := toMultisetsOne S5
let prod := SqHd ΓΛ’ (SqHu ΓΛ’ Q5)
let Filt := prod.filter (fun x => x.1 - 2 β’ x.2.1 + x.2.2.sum = 0)
(Filt.map (fun x => β¨x.1, x.2.1, x.2.2.toFinset, β
β©))
| W3 =>
let SqHu := S5.val
let Q5 := toMultisetsTwo S5
let prod := SqHu ΓΛ’ Q5
let Filt := prod.filter (fun x => - 2 β’ x.1 + x.2.sum = 0)
(Filt.map (fun x => β¨none, x.1, x.2.toFinset, β
β©))
| W2 =>
let SqHd := S5.val
let Q10 := toMultisetsThree S10
let prod := SqHd ΓΛ’ Q10
let Filt := prod.filter (fun x => x.1 + x.2.sum = 0)
(Filt.map (fun x => β¨x.1, none, β
, x.2.toFinsetβ©)).filter fun x => MinimallyAllowsTerm x W2
| W1 =>
let Q5 := toMultisetsOne S5
let Q10 := toMultisetsThree S10
let Prod := Q5 ΓΛ’ Q10
let Filt := Prod.filter (fun x => x.1.sum + x.2.sum = 0)
(Filt.map (fun x =>
β¨none, none, x.1.toFinset, x.2.toFinsetβ©)).filter fun x => MinimallyAllowsTerm x W1
| Ξ =>
let Q5 := toMultisetsTwo S5
let Q10 := toMultisetsOne S10
let Prod := Q5 ΓΛ’ Q10
let Filt := Prod.filter (fun x => x.1.sum + x.2.sum = 0)
(Filt.map (fun x => β¨none, none, x.1.toFinset, x.2.toFinsetβ©))
| Ξ² =>
let SqHu := S5.val
let Q5 := toMultisetsOne S5
let prod := SqHu ΓΛ’ Q5
let Filt := prod.filter (fun x => - x.1 + x.2.sum = 0)
(Filt.map (fun x => β¨none, x.1, x.2.toFinset, β
β©))
| topYukawa =>
let SqHu := S5.val
let Q10 := toMultisetsTwo S10
let prod := SqHu ΓΛ’ Q10
let Filt := prod.filter (fun x => - x.1 + x.2.sum = 0)
(Filt.map (fun x => β¨none, x.1, β
, x.2.toFinsetβ©))
| bottomYukawa =>
let SqHd := S5.val
let Q5 := toMultisetsOne S5
let Q10 := toMultisetsOne S10
let prod := SqHd ΓΛ’ (Q5 ΓΛ’ Q10)
let Filt := prod.filter (fun x => x.1 + x.2.1.sum + x.2.2.sum = 0)
(Filt.map (fun x => β¨x.1, none,x.2.1.toFinset, x.2.2.toFinsetβ©))
A.3. Showing minimallyAllowsTermsOfFinset has charges in given sets
We show that every element of minimallyAllowsTermsOfFinset S5 S10 T is in ofFinset S5 S10.
That is every element of minimallyAllowsTermsOfFinset S5 S10 T has charges
in the sets S5 and S10.
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©h:(a β S5 β§ b β S5) β§ -a + b = 0β’ { qHd := some a, qHu := some b, Q5 := β
, Q10 := β
}.qHd.toFinset β S5 β§
{ qHd := some a, qHu := some b, Q5 := β
, Q10 := β
}.qHu.toFinset β S5 β§
{ qHd := some a, qHu := some b, Q5 := β
, Q10 := β
}.Q5 β S5 β§
{ qHd := some a, qHu := some b, Q5 := β
, Q10 := β
}.Q10 β S10
All goals completed! πlemma minimallyAllowsTermOfFinset_subset_ofFinset {S5 S10 : Finset π©} {T : PotentialTerm} :
minimallyAllowsTermsOfFinset S5 S10 T β (ofFinset S5 S10).val :=
fun _ hx => Finset.mem_val.mpr (mem_ofFinset_of_mem_minimallyAllowsTermOfFinset hx)
B. Proving the minimallyAllowsTermsOfFinset is set of charges which minimally allow a term
We now prove that minimallyAllowsTermsOfFinset has the property
that all charges spectra with charges in the sets S5 and S10
which minimally allow the potential term T are in
minimallyAllowsTermsOfFinset S5 S10 T, and vice versa.
B.1. An element of minimallyAllowsTermsOfFinset is of the form allowsTermForm
We show that every element of minimallyAllowsTermsOfFinset S5 S10 T is of the form
allowsTermForm a b c T for some a, b and c.
lemma eq_allowsTermForm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset π©} {T : PotentialTerm}
{x : ChargeSpectrum π©} (hx : x β minimallyAllowsTermsOfFinset S5 S10 T) :
β a b c, x = allowsTermForm a b c T := π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©T:PotentialTermx:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 Tβ’ β a b c, x = allowsTermForm a b c T
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 ΞΌβ’ β a b c, x = allowsTermForm a b c ΞΌπ©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 Ξ²β’ β a b c, x = allowsTermForm a b c Ξ²π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 Ξβ’ β a b c, x = allowsTermForm a b c Ξπ©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 W1β’ β a b c, x = allowsTermForm a b c W1π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 W2β’ β a b c, x = allowsTermForm a b c W2π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 W3β’ β a b c, x = allowsTermForm a b c W3π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 W4β’ β a b c, x = allowsTermForm a b c W4π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 K1β’ β a b c, x = allowsTermForm a b c K1π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 K2β’ β a b c, x = allowsTermForm a b c K2π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 topYukawaβ’ β a b c, x = allowsTermForm a b c topYukawaπ©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 bottomYukawaβ’ β a b c, x = allowsTermForm a b c bottomYukawa
all_goals
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:β a a_1 b,
((a β S5 β§ (a_1.toFinset β S5 β§ a_1.card = 1) β§ b.toFinset β S10 β§ b.card = 1) β§ a + a_1.sum + b.sum = 0) β§
{ qHd := some a, qHu := none, Q5 := a_1.toFinset, Q10 := b.toFinset } = xβ’ β a b c, x = allowsTermForm a b c bottomYukawa
case ΞΌ π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:β a b, ((a β S5 β§ b β S5) β§ -a + b = 0) β§ { qHd := some a, qHu := some b, Q5 := β
, Q10 := β
} = xβ’ β a b c, x = allowsTermForm a b c ΞΌ
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©hsum:-a + b = 0ha:a β S5hb:b β S5β’ β a_1 b_1 c, { qHd := some a, qHu := some b, Q5 := β
, Q10 := β
} = allowsTermForm a_1 b_1 c ΞΌ
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©hsum:-a + b = 0ha:a β S5hb:b β S5β’ b = a
All goals completed! π
case Ξ² π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:β a b,
((a β S5 β§ b.toFinset β S5 β§ b.card = 1) β§ -a + b.sum = 0) β§
{ qHd := none, qHu := some a, Q5 := b.toFinset, Q10 := β
} = xβ’ β a b c, x = allowsTermForm a b c Ξ²
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:Multiset π©hsum:-a + b.sum = 0ha:a β S5hb:b.toFinset β S5hbcard:b.card = 1β’ β a_1 b_1 c, { qHd := none, qHu := some a, Q5 := b.toFinset, Q10 := β
} = allowsTermForm a_1 b_1 c Ξ²
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©hsum:-a + {c}.sum = 0hb:{c}.toFinset β S5hbcard:{c}.card = 1β’ β a_1 b c_1, { qHd := none, qHu := some a, Q5 := {c}.toFinset, Q10 := β
} = allowsTermForm a_1 b c_1 Ξ²
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©hsum:-a + c = 0hb:c β S5β’ c = a
All goals completed! π
case K1 π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:β a b,
(((a.toFinset β S5 β§ a.card = 1) β§ b.toFinset β S10 β§ b.card = 2) β§ -a.sum + b.sum = 0) β§
{ qHd := none, qHu := none, Q5 := a.toFinset, Q10 := b.toFinset } = xβ’ β a b c, x = allowsTermForm a b c K1
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:Multiset π©b:Multiset π©hsum:-a.sum + b.sum = 0ha:a.toFinset β S5hacard:a.card = 1hb:b.toFinset β S10hbcard:b.card = 2β’ β a_1 b_1 c, { qHd := none, qHu := none, Q5 := a.toFinset, Q10 := b.toFinset } = allowsTermForm a_1 b_1 c K1
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©b:Multiset π©hb:b.toFinset β S10hbcard:b.card = 2c:π©hsum:-{c}.sum + b.sum = 0ha:{c}.toFinset β S5hacard:{c}.card = 1β’ β a b_1 c_1, { qHd := none, qHu := none, Q5 := {c}.toFinset, Q10 := b.toFinset } = allowsTermForm a b_1 c_1 K1
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©c:π©ha:{c}.toFinset β S5hacard:{c}.card = 1d:π©e:π©hb:{d, e}.toFinset β S10hbcard:{d, e}.card = 2hsum:-{c}.sum + {d, e}.sum = 0β’ β a b c_1, { qHd := none, qHu := none, Q5 := {c}.toFinset, Q10 := {d, e}.toFinset } = allowsTermForm a b c_1 K1
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©c:π©d:π©e:π©ha:c β S5hb:{d, e} β S10hsum:-c + (d + e) = 0β’ β a, c = -a β§ β x, {d, e} = {x, -a - x}
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©c:π©d:π©e:π©ha:c β S5hb:{d, e} β S10hsum:-c + (d + e) = 0β’ c = - -cπ©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©c:π©d:π©e:π©ha:c β S5hb:{d, e} β S10hsum:-c + (d + e) = 0β’ {d, e} = {d, - -c - d} π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©c:π©d:π©e:π©ha:c β S5hb:{d, e} β S10hsum:-c + (d + e) = 0β’ c = - -cπ©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©c:π©d:π©e:π©ha:c β S5hb:{d, e} β S10hsum:-c + (d + e) = 0β’ {d, e} = {d, - -c - d} All goals completed! π
case Ξ π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:β a b,
(((a.toFinset β S5 β§ a.card = 2) β§ b.toFinset β S10 β§ b.card = 1) β§ a.sum + b.sum = 0) β§
{ qHd := none, qHu := none, Q5 := a.toFinset, Q10 := b.toFinset } = xβ’ β a b c, x = allowsTermForm a b c Ξ
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:Multiset π©b:Multiset π©hsum:a.sum + b.sum = 0ha:a.toFinset β S5hacard:a.card = 2hb:b.toFinset β S10hbcard:b.card = 1β’ β a_1 b_1 c, { qHd := none, qHu := none, Q5 := a.toFinset, Q10 := b.toFinset } = allowsTermForm a_1 b_1 c Ξ
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©b:Multiset π©hb:b.toFinset β S10hbcard:b.card = 1c:π©d:π©hsum:{c, d}.sum + b.sum = 0ha:{c, d}.toFinset β S5hacard:{c, d}.card = 2β’ β a b_1 c_1, { qHd := none, qHu := none, Q5 := {c, d}.toFinset, Q10 := b.toFinset } = allowsTermForm a b_1 c_1 Ξ
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©c:π©d:π©ha:{c, d}.toFinset β S5hacard:{c, d}.card = 2e:π©hb:{e}.toFinset β S10hbcard:{e}.card = 1hsum:{c, d}.sum + {e}.sum = 0β’ β a b c_1, { qHd := none, qHu := none, Q5 := {c, d}.toFinset, Q10 := {e}.toFinset } = allowsTermForm a b c_1 Ξ
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©c:π©d:π©e:π©ha:{c, d} β S5hb:e β S10hsum:c + d + e = 0β’ β a b, {c, d} = {a, b} β§ e = -a - b
All goals completed! π
case W1 π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:(β a b,
(((a.toFinset β S5 β§ a.card = 1) β§ b.toFinset β S10 β§ b.card = 3) β§ a.sum + b.sum = 0) β§
{ qHd := none, qHu := none, Q5 := a.toFinset, Q10 := b.toFinset } = x) β§
x.MinimallyAllowsTerm W1β’ β a b c, x = allowsTermForm a b c W1
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:Multiset π©b:Multiset π©hsum:a.sum + b.sum = 0ha:a.toFinset β S5hacard:a.card = 1hb:b.toFinset β S10hbcard:b.card = 3rightβ:{ qHd := none, qHu := none, Q5 := a.toFinset, Q10 := b.toFinset }.MinimallyAllowsTerm W1β’ β a_1 b_1 c, { qHd := none, qHu := none, Q5 := a.toFinset, Q10 := b.toFinset } = allowsTermForm a_1 b_1 c W1
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©b:Multiset π©hb:b.toFinset β S10hbcard:b.card = 3c:π©hsum:{c}.sum + b.sum = 0ha:{c}.toFinset β S5hacard:{c}.card = 1rightβ:{ qHd := none, qHu := none, Q5 := {c}.toFinset, Q10 := b.toFinset }.MinimallyAllowsTerm W1β’ β a b_1 c_1, { qHd := none, qHu := none, Q5 := {c}.toFinset, Q10 := b.toFinset } = allowsTermForm a b_1 c_1 W1
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©c:π©ha:{c}.toFinset β S5hacard:{c}.card = 1e:π©d:π©f:π©hb:{e, d, f}.toFinset β S10hbcard:{e, d, f}.card = 3hsum:{c}.sum + {e, d, f}.sum = 0rightβ:{ qHd := none, qHu := none, Q5 := {c}.toFinset, Q10 := {e, d, f}.toFinset }.MinimallyAllowsTerm W1β’ β a b c_1, { qHd := none, qHu := none, Q5 := {c}.toFinset, Q10 := {e, d, f}.toFinset } = allowsTermForm a b c_1 W1
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©c:π©e:π©d:π©f:π©ha:c β S5hb:{e, d, f} β S10hsum:c + (e + (d + f)) = 0rightβ:{ qHd := none, qHu := none, Q5 := {c}, Q10 := {e, d, f} }.MinimallyAllowsTerm W1β’ β a b c_1, c = -a - b - c_1 β§ {e, d, f} = {a, b, c_1}
All goals completed! π
case W2 π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:(β a b,
((a β S5 β§ b.toFinset β S10 β§ b.card = 3) β§ a + b.sum = 0) β§
{ qHd := some a, qHu := none, Q5 := β
, Q10 := b.toFinset } = x) β§
x.MinimallyAllowsTerm W2β’ β a b c, x = allowsTermForm a b c W2
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:Multiset π©hsum:a + b.sum = 0ha:a β S5hb:b.toFinset β S10hbcard:b.card = 3rightβ:{ qHd := some a, qHu := none, Q5 := β
, Q10 := b.toFinset }.MinimallyAllowsTerm W2β’ β a_1 b_1 c, { qHd := some a, qHu := none, Q5 := β
, Q10 := b.toFinset } = allowsTermForm a_1 b_1 c W2
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5e:π©d:π©f:π©hsum:a + {e, d, f}.sum = 0hb:{e, d, f}.toFinset β S10hbcard:{e, d, f}.card = 3rightβ:{ qHd := some a, qHu := none, Q5 := β
, Q10 := {e, d, f}.toFinset }.MinimallyAllowsTerm W2β’ β a_1 b c, { qHd := some a, qHu := none, Q5 := β
, Q10 := {e, d, f}.toFinset } = allowsTermForm a_1 b c W2
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5e:π©d:π©f:π©hsum:a + (e + (d + f)) = 0hb:{e, d, f} β S10rightβ:{ qHd := some a, qHu := none, Q5 := β
, Q10 := {e, d, f} }.MinimallyAllowsTerm W2β’ β a_1 b c, a = -a_1 - b - c β§ {e, d, f} = {a_1, b, c}
All goals completed! π
case W3 π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:β a b,
((a β S5 β§ b.toFinset β S5 β§ b.card = 2) β§ -(2 β’ a) + b.sum = 0) β§
{ qHd := none, qHu := some a, Q5 := b.toFinset, Q10 := β
} = xβ’ β a b c, x = allowsTermForm a b c W3
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:Multiset π©hsum:-(2 β’ a) + b.sum = 0ha:a β S5hb:b.toFinset β S5hbcard:b.card = 2β’ β a_1 b_1 c, { qHd := none, qHu := some a, Q5 := b.toFinset, Q10 := β
} = allowsTermForm a_1 b_1 c W3
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©d:π©hsum:-(2 β’ a) + {c, d}.sum = 0hb:{c, d}.toFinset β S5hbcard:{c, d}.card = 2β’ β a_1 b c_1, { qHd := none, qHu := some a, Q5 := {c, d}.toFinset, Q10 := β
} = allowsTermForm a_1 b c_1 W3
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©d:π©hsum:-(2 β’ a) + (c + d) = 0hb:{c, d} β S5β’ β a_1, a = -a_1 β§ β x, {c, d} = {x, -x - 2 β’ a_1}
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©d:π©hsum:-(2 β’ a) + (c + d) = 0hb:{c, d} β S5β’ a = - -aπ©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©d:π©hsum:-(2 β’ a) + (c + d) = 0hb:{c, d} β S5β’ {c, d} = {c, -c - 2 β’ -a} π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©d:π©hsum:-(2 β’ a) + (c + d) = 0hb:{c, d} β S5β’ a = - -aπ©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©d:π©hsum:-(2 β’ a) + (c + d) = 0hb:{c, d} β S5β’ {c, d} = {c, -c - 2 β’ -a} All goals completed! π
case W4 π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:β a a_1 b,
((a β S5 β§ a_1 β S5 β§ b.toFinset β S5 β§ b.card = 1) β§ a - 2 β’ a_1 + b.sum = 0) β§
{ qHd := some a, qHu := some a_1, Q5 := b.toFinset, Q10 := β
} = xβ’ β a b c, x = allowsTermForm a b c W4
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:Multiset π©hsum:a - 2 β’ b + c.sum = 0ha:a β S5hb:b β S5hc:c.toFinset β S5hcard:c.card = 1β’ β a_1 b_1 c_1, { qHd := some a, qHu := some b, Q5 := c.toFinset, Q10 := β
} = allowsTermForm a_1 b_1 c_1 W4
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©ha:a β S5hb:b β S5d:π©hsum:a - 2 β’ b + {d}.sum = 0hc:{d}.toFinset β S5hcard:{d}.card = 1β’ β a_1 b_1 c, { qHd := some a, qHu := some b, Q5 := {d}.toFinset, Q10 := β
} = allowsTermForm a_1 b_1 c W4
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©ha:a β S5hb:b β S5d:π©hsum:a - 2 β’ b + d = 0hc:d β S5β’ β b_1, a = -d - 2 β’ b_1 β§ b = -b_1
exact β¨-b, π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©ha:a β S5hb:b β S5d:π©hsum:a - 2 β’ b + d = 0hc:d β S5β’ a = -d - 2 β’ -b β§ b = - -b All goals completed! πβ©
case K2 π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:β a a_1 b,
((a β S5 β§ a_1 β S5 β§ b.toFinset β S10 β§ b.card = 1) β§ a + a_1 + b.sum = 0) β§
{ qHd := some a, qHu := some a_1, Q5 := β
, Q10 := b.toFinset } = xβ’ β a b c, x = allowsTermForm a b c K2
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:Multiset π©hsum:a + b + c.sum = 0ha:a β S5hb:b β S5hc:c.toFinset β S10hcard:c.card = 1β’ β a_1 b_1 c_1, { qHd := some a, qHu := some b, Q5 := β
, Q10 := c.toFinset } = allowsTermForm a_1 b_1 c_1 K2
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©ha:a β S5hb:b β S5d:π©hsum:a + b + {d}.sum = 0hc:{d}.toFinset β S10hcard:{d}.card = 1β’ β a_1 b_1 c, { qHd := some a, qHu := some b, Q5 := β
, Q10 := {d}.toFinset } = allowsTermForm a_1 b_1 c K2
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©ha:a β S5hb:b β S5d:π©hsum:a + b + d = 0hc:d β S10β’ d = -a - b
All goals completed! π
case topYukawa π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:β a b,
((a β S5 β§ b.toFinset β S10 β§ b.card = 2) β§ -a + b.sum = 0) β§
{ qHd := none, qHu := some a, Q5 := β
, Q10 := b.toFinset } = xβ’ β a b c, x = allowsTermForm a b c topYukawa
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:Multiset π©hsum:-a + b.sum = 0ha:a β S5hb:b.toFinset β S10hbcard:b.card = 2β’ β a_1 b_1 c, { qHd := none, qHu := some a, Q5 := β
, Q10 := b.toFinset } = allowsTermForm a_1 b_1 c topYukawa
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©d:π©hsum:-a + {c, d}.sum = 0hb:{c, d}.toFinset β S10hbcard:{c, d}.card = 2β’ β a_1 b c_1, { qHd := none, qHu := some a, Q5 := β
, Q10 := {c, d}.toFinset } = allowsTermForm a_1 b c_1 topYukawa
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©d:π©hsum:-a + (c + d) = 0hb:{c, d} β S10β’ β a_1, a = -a_1 β§ β x, {c, d} = {x, -a_1 - x}
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©d:π©hsum:-a + (c + d) = 0hb:{c, d} β S10β’ a = - -aπ©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©d:π©hsum:-a + (c + d) = 0hb:{c, d} β S10β’ {c, d} = {c, - -a - c} π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©d:π©hsum:-a + (c + d) = 0hb:{c, d} β S10β’ a = - -aπ©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5c:π©d:π©hsum:-a + (c + d) = 0hb:{c, d} β S10β’ {c, d} = {c, - -a - c} All goals completed! π
case bottomYukawa π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:β a a_1 b,
((a β S5 β§ (a_1.toFinset β S5 β§ a_1.card = 1) β§ b.toFinset β S10 β§ b.card = 1) β§ a + a_1.sum + b.sum = 0) β§
{ qHd := some a, qHu := none, Q5 := a_1.toFinset, Q10 := b.toFinset } = xβ’ β a b c, x = allowsTermForm a b c bottomYukawa
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:Multiset π©c:Multiset π©hsum:a + b.sum + c.sum = 0ha:a β S5hb:b.toFinset β S5hbcard:b.card = 1hc:c.toFinset β S10hcard:c.card = 1β’ β a_1 b_1 c_1,
{ qHd := some a, qHu := none, Q5 := b.toFinset, Q10 := c.toFinset } = allowsTermForm a_1 b_1 c_1 bottomYukawa
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:Multiset π©ha:a β S5hb:b.toFinset β S5hbcard:b.card = 1e:π©hsum:a + b.sum + {e}.sum = 0hc:{e}.toFinset β S10hcard:{e}.card = 1β’ β a_1 b_1 c,
{ qHd := some a, qHu := none, Q5 := b.toFinset, Q10 := {e}.toFinset } = allowsTermForm a_1 b_1 c bottomYukawa
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5e:π©hc:{e}.toFinset β S10hcard:{e}.card = 1d:π©hb:{d}.toFinset β S5hbcard:{d}.card = 1hsum:a + {d}.sum + {e}.sum = 0β’ β a_1 b c, { qHd := some a, qHu := none, Q5 := {d}.toFinset, Q10 := {e}.toFinset } = allowsTermForm a_1 b c bottomYukawa
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©ha:a β S5e:π©d:π©hc:e β S10hb:d β S5hsum:a + d + e = 0β’ e = -a - d
All goals completed! π
B.2. Every element of minimallyAllowsTermsOfFinset allows the term
We show that every element of minimallyAllowsTermsOfFinset S5 S10 T allows the term T.
lemma allowsTerm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset π©} {T : PotentialTerm}
{x : ChargeSpectrum π©} (hx : x β minimallyAllowsTermsOfFinset S5 S10 T) :
x.AllowsTerm T := π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©T:PotentialTermx:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 Tβ’ x.AllowsTerm T
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©T:PotentialTerma:π©b:π©c:π©hx:allowsTermForm a b c T β minimallyAllowsTermsOfFinset S5 S10 Tβ’ (allowsTermForm a b c T).AllowsTerm T
All goals completed! π
B.3. Every element of minimallyAllowsTermsOfFinset minimally allows the term
We make the above condition stronger, showing that every element of
minimallyAllowsTermsOfFinset S5 S10 T minimally allows the term T.
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 W1hT:Β¬(W1 β W1 β§ W1 β W2)β’ x.MinimallyAllowsTerm W1π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 W2hT:Β¬(W2 β W1 β§ W2 β W2)β’ x.MinimallyAllowsTerm W2
all_goals
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hT:Β¬(W2 β W1 β§ W2 β W2)hx:(β a b,
((a β S5 β§ b.toFinset β S10 β§ b.card = 3) β§ a + b.sum = 0) β§
{ qHd := some a, qHu := none, Q5 := β
, Q10 := b.toFinset } = x) β§
x.MinimallyAllowsTerm W2β’ x.MinimallyAllowsTerm W2
All goals completed! π
B.4. Every charge spectra which minimally allows term is in minimallyAllowsTermsOfFinset
We show that every charge spectra which minimally allows term T and has charges
in the sets S5 and S10 is in minimallyAllowsTermsOfFinset S5 S10 T.
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c bottomYukawa).MinimallyAllowsTerm bottomYukawahx:(allowsTermForm a b c bottomYukawa).qHd.toFinset β S5 β§
(allowsTermForm a b c bottomYukawa).qHu.toFinset β S5 β§
(allowsTermForm a b c bottomYukawa).Q5 β S5 β§ (allowsTermForm a b c bottomYukawa).Q10 β S10β’ β a_1 b_1,
((a β S5 β§ (a_1.toFinset β S5 β§ a_1.card = 1) β§ b_1.toFinset β S10 β§ b_1.card = 1) β§ a + a_1.sum + b_1.sum = 0) β§
a_1.toFinset = {b} β§ b_1.toFinset = {-a - b}
case ΞΌ π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c ΞΌ).MinimallyAllowsTerm ΞΌhx:(allowsTermForm a b c ΞΌ).qHd.toFinset β S5 β§
(allowsTermForm a b c ΞΌ).qHu.toFinset β S5 β§ (allowsTermForm a b c ΞΌ).Q5 β S5 β§ (allowsTermForm a b c ΞΌ).Q10 β S10β’ a β S5
All goals completed! π
case Ξ² π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c Ξ²).MinimallyAllowsTerm Ξ²hx:(allowsTermForm a b c Ξ²).qHd.toFinset β S5 β§
(allowsTermForm a b c Ξ²).qHu.toFinset β S5 β§ (allowsTermForm a b c Ξ²).Q5 β S5 β§ (allowsTermForm a b c Ξ²).Q10 β S10β’ β b, ((a β S5 β§ b.toFinset β S5 β§ b.card = 1) β§ -a + b.sum = 0) β§ b.toFinset = {a}
exact β¨{a}, π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c Ξ²).MinimallyAllowsTerm Ξ²hx:(allowsTermForm a b c Ξ²).qHd.toFinset β S5 β§
(allowsTermForm a b c Ξ²).qHu.toFinset β S5 β§ (allowsTermForm a b c Ξ²).Q5 β S5 β§ (allowsTermForm a b c Ξ²).Q10 β S10β’ ((a β S5 β§ {a}.toFinset β S5 β§ {a}.card = 1) β§ -a + {a}.sum = 0) β§ {a}.toFinset = {a} All goals completed! πβ©
case Ξ π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c Ξ).MinimallyAllowsTerm Ξhx:(allowsTermForm a b c Ξ).qHd.toFinset β S5 β§
(allowsTermForm a b c Ξ).qHu.toFinset β S5 β§ (allowsTermForm a b c Ξ).Q5 β S5 β§ (allowsTermForm a b c Ξ).Q10 β S10β’ β a_1 b_1,
(((a_1.toFinset β S5 β§ a_1.card = 2) β§ b_1.toFinset β S10 β§ b_1.card = 1) β§ a_1.sum + b_1.sum = 0) β§
a_1.toFinset = {a, b} β§ b_1.toFinset = {-a - b}
exact β¨{a, b}, {- a - b}, π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c Ξ).MinimallyAllowsTerm Ξhx:(allowsTermForm a b c Ξ).qHd.toFinset β S5 β§
(allowsTermForm a b c Ξ).qHu.toFinset β S5 β§ (allowsTermForm a b c Ξ).Q5 β S5 β§ (allowsTermForm a b c Ξ).Q10 β S10β’ ((({a, b}.toFinset β S5 β§ {a, b}.card = 2) β§ {-a - b}.toFinset β S10 β§ {-a - b}.card = 1) β§
{a, b}.sum + {-a - b}.sum = 0) β§
{a, b}.toFinset = {a, b} β§ {-a - b}.toFinset = {-a - b} All goals completed! πβ©
case W1 π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c W1).MinimallyAllowsTerm W1hx:(allowsTermForm a b c W1).qHd.toFinset β S5 β§
(allowsTermForm a b c W1).qHu.toFinset β S5 β§ (allowsTermForm a b c W1).Q5 β S5 β§ (allowsTermForm a b c W1).Q10 β S10β’ (β a_1 b_1,
(((a_1.toFinset β S5 β§ a_1.card = 1) β§ b_1.toFinset β S10 β§ b_1.card = 3) β§ a_1.sum + b_1.sum = 0) β§
a_1.toFinset = {-a - b - c} β§ b_1.toFinset = {a, b, c}) β§
{ qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} }.MinimallyAllowsTerm W1
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c W1).MinimallyAllowsTerm W1hx:(allowsTermForm a b c W1).qHd.toFinset β S5 β§
(allowsTermForm a b c W1).qHu.toFinset β S5 β§ (allowsTermForm a b c W1).Q5 β S5 β§ (allowsTermForm a b c W1).Q10 β S10β’ ((({-a - b - c}.toFinset β S5 β§ {-a - b - c}.card = 1) β§ {a, b, c}.toFinset β S10 β§ {a, b, c}.card = 3) β§
{-a - b - c}.sum + {a, b, c}.sum = 0) β§
{-a - b - c}.toFinset = {-a - b - c} β§ {a, b, c}.toFinset = {a, b, c}
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:{ qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} }.MinimallyAllowsTerm W1hx:-a - b - c β S5 β§ {a, b, c} β S10β’ -a - b - c + (a + (b + c)) = 0
All goals completed! π
case W2 π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c W2).MinimallyAllowsTerm W2hx:(allowsTermForm a b c W2).qHd.toFinset β S5 β§
(allowsTermForm a b c W2).qHu.toFinset β S5 β§ (allowsTermForm a b c W2).Q5 β S5 β§ (allowsTermForm a b c W2).Q10 β S10β’ (β b_1, ((-a - b - c β S5 β§ b_1.toFinset β S10 β§ b_1.card = 3) β§ -a - b - c + b_1.sum = 0) β§ b_1.toFinset = {a, b, c}) β§
{ qHd := some (-a - b - c), qHu := none, Q5 := β
, Q10 := {a, b, c} }.MinimallyAllowsTerm W2
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c W2).MinimallyAllowsTerm W2hx:(allowsTermForm a b c W2).qHd.toFinset β S5 β§
(allowsTermForm a b c W2).qHu.toFinset β S5 β§ (allowsTermForm a b c W2).Q5 β S5 β§ (allowsTermForm a b c W2).Q10 β S10β’ ((-a - b - c β S5 β§ {a, b, c}.toFinset β S10 β§ {a, b, c}.card = 3) β§ -a - b - c + {a, b, c}.sum = 0) β§
{a, b, c}.toFinset = {a, b, c}
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:{ qHd := some (-a - b - c), qHu := none, Q5 := β
, Q10 := {a, b, c} }.MinimallyAllowsTerm W2hx:-a - b - c β S5 β§ {a, b, c} β S10β’ -a - b - c + (a + (b + c)) = 0
All goals completed! π
case W3 π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c W3).MinimallyAllowsTerm W3hx:(allowsTermForm a b c W3).qHd.toFinset β S5 β§
(allowsTermForm a b c W3).qHu.toFinset β S5 β§ (allowsTermForm a b c W3).Q5 β S5 β§ (allowsTermForm a b c W3).Q10 β S10β’ β b_1, ((-a β S5 β§ b_1.toFinset β S5 β§ b_1.card = 2) β§ 2 β’ a + b_1.sum = 0) β§ b_1.toFinset = {b, -b - 2 β’ a}
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c W3).MinimallyAllowsTerm W3hx:(allowsTermForm a b c W3).qHd.toFinset β S5 β§
(allowsTermForm a b c W3).qHu.toFinset β S5 β§ (allowsTermForm a b c W3).Q5 β S5 β§ (allowsTermForm a b c W3).Q10 β S10β’ ((-a β S5 β§ {b, -b - 2 β’ a}.toFinset β S5 β§ {b, -b - 2 β’ a}.card = 2) β§ 2 β’ a + {b, -b - 2 β’ a}.sum = 0) β§
{b, -b - 2 β’ a}.toFinset = {b, -b - 2 β’ a}
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:{ qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β’ a}, Q10 := β
}.MinimallyAllowsTerm W3hx:-a β S5 β§ {b, -b - 2 β’ a} β S5β’ 2 β’ a + (b + (-b - 2 β’ a)) = 0
All goals completed! π
case W4 π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c W4).MinimallyAllowsTerm W4hx:(allowsTermForm a b c W4).qHd.toFinset β S5 β§
(allowsTermForm a b c W4).qHu.toFinset β S5 β§ (allowsTermForm a b c W4).Q5 β S5 β§ (allowsTermForm a b c W4).Q10 β S10β’ β b_1, ((-c - 2 β’ b β S5 β§ -b β S5 β§ b_1.toFinset β S5 β§ b_1.card = 1) β§ -c + b_1.sum = 0) β§ b_1.toFinset = {c}
exact β¨{c}, π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c W4).MinimallyAllowsTerm W4hx:(allowsTermForm a b c W4).qHd.toFinset β S5 β§
(allowsTermForm a b c W4).qHu.toFinset β S5 β§ (allowsTermForm a b c W4).Q5 β S5 β§ (allowsTermForm a b c W4).Q10 β S10β’ ((-c - 2 β’ b β S5 β§ -b β S5 β§ {c}.toFinset β S5 β§ {c}.card = 1) β§ -c + {c}.sum = 0) β§ {c}.toFinset = {c} All goals completed! πβ©
case K1 π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c K1).MinimallyAllowsTerm K1hx:(allowsTermForm a b c K1).qHd.toFinset β S5 β§
(allowsTermForm a b c K1).qHu.toFinset β S5 β§ (allowsTermForm a b c K1).Q5 β S5 β§ (allowsTermForm a b c K1).Q10 β S10β’ β a_1 b_1,
(((a_1.toFinset β S5 β§ a_1.card = 1) β§ b_1.toFinset β S10 β§ b_1.card = 2) β§ -a_1.sum + b_1.sum = 0) β§
a_1.toFinset = {-a} β§ b_1.toFinset = {b, -a - b}
exact β¨{-a}, {b, - a - b}, π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c K1).MinimallyAllowsTerm K1hx:(allowsTermForm a b c K1).qHd.toFinset β S5 β§
(allowsTermForm a b c K1).qHu.toFinset β S5 β§ (allowsTermForm a b c K1).Q5 β S5 β§ (allowsTermForm a b c K1).Q10 β S10β’ ((({-a}.toFinset β S5 β§ {-a}.card = 1) β§ {b, -a - b}.toFinset β S10 β§ {b, -a - b}.card = 2) β§
-{-a}.sum + {b, -a - b}.sum = 0) β§
{-a}.toFinset = {-a} β§ {b, -a - b}.toFinset = {b, -a - b} All goals completed! πβ©
case K2 π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c K2).MinimallyAllowsTerm K2hx:(allowsTermForm a b c K2).qHd.toFinset β S5 β§
(allowsTermForm a b c K2).qHu.toFinset β S5 β§ (allowsTermForm a b c K2).Q5 β S5 β§ (allowsTermForm a b c K2).Q10 β S10β’ β b_1, ((a β S5 β§ b β S5 β§ b_1.toFinset β S10 β§ b_1.card = 1) β§ a + b + b_1.sum = 0) β§ b_1.toFinset = {-a - b}
exact β¨{- a - b}, π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c K2).MinimallyAllowsTerm K2hx:(allowsTermForm a b c K2).qHd.toFinset β S5 β§
(allowsTermForm a b c K2).qHu.toFinset β S5 β§ (allowsTermForm a b c K2).Q5 β S5 β§ (allowsTermForm a b c K2).Q10 β S10β’ ((a β S5 β§ b β S5 β§ {-a - b}.toFinset β S10 β§ {-a - b}.card = 1) β§ a + b + {-a - b}.sum = 0) β§
{-a - b}.toFinset = {-a - b} All goals completed! πβ©
case topYukawa π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c topYukawa).MinimallyAllowsTerm topYukawahx:(allowsTermForm a b c topYukawa).qHd.toFinset β S5 β§
(allowsTermForm a b c topYukawa).qHu.toFinset β S5 β§
(allowsTermForm a b c topYukawa).Q5 β S5 β§ (allowsTermForm a b c topYukawa).Q10 β S10β’ β b_1, ((-a β S5 β§ b_1.toFinset β S10 β§ b_1.card = 2) β§ a + b_1.sum = 0) β§ b_1.toFinset = {b, -a - b}
exact β¨{b, - a - b}, π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c topYukawa).MinimallyAllowsTerm topYukawahx:(allowsTermForm a b c topYukawa).qHd.toFinset β S5 β§
(allowsTermForm a b c topYukawa).qHu.toFinset β S5 β§
(allowsTermForm a b c topYukawa).Q5 β S5 β§ (allowsTermForm a b c topYukawa).Q10 β S10β’ ((-a β S5 β§ {b, -a - b}.toFinset β S10 β§ {b, -a - b}.card = 2) β§ a + {b, -a - b}.sum = 0) β§
{b, -a - b}.toFinset = {b, -a - b} All goals completed! πβ©
case bottomYukawa π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c bottomYukawa).MinimallyAllowsTerm bottomYukawahx:(allowsTermForm a b c bottomYukawa).qHd.toFinset β S5 β§
(allowsTermForm a b c bottomYukawa).qHu.toFinset β S5 β§
(allowsTermForm a b c bottomYukawa).Q5 β S5 β§ (allowsTermForm a b c bottomYukawa).Q10 β S10β’ β a_1 b_1,
((a β S5 β§ (a_1.toFinset β S5 β§ a_1.card = 1) β§ b_1.toFinset β S10 β§ b_1.card = 1) β§ a + a_1.sum + b_1.sum = 0) β§
a_1.toFinset = {b} β§ b_1.toFinset = {-a - b}
exact β¨{b}, {- a - b}, π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©a:π©b:π©c:π©h:(allowsTermForm a b c bottomYukawa).MinimallyAllowsTerm bottomYukawahx:(allowsTermForm a b c bottomYukawa).qHd.toFinset β S5 β§
(allowsTermForm a b c bottomYukawa).qHu.toFinset β S5 β§
(allowsTermForm a b c bottomYukawa).Q5 β S5 β§ (allowsTermForm a b c bottomYukawa).Q10 β S10β’ ((a β S5 β§ ({b}.toFinset β S5 β§ {b}.card = 1) β§ {-a - b}.toFinset β S10 β§ {-a - b}.card = 1) β§
a + {b}.sum + {-a - b}.sum = 0) β§
{b}.toFinset = {b} β§ {-a - b}.toFinset = {-a - b} All goals completed! πβ©
B.5. In minimallyAllowsTermsOfFinset iff minimally allowing term
We now show the key result of this section, that a charge spectrum x
is in minimallyAllowsTermsOfFinset S5 S10 T if and only if
it minimally allows the term T, provided it is in ofFinset S5 S10.
lemma minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinset
{S5 S10 : Finset π©} {T : PotentialTerm}
{x : ChargeSpectrum π©} (hx : x β ofFinset S5 S10) :
x.MinimallyAllowsTerm T β x β minimallyAllowsTermsOfFinset S5 S10 T :=
β¨fun h => mem_minimallyAllowsTermOfFinset_of_minimallyAllowsTerm x h hx,
minimallyAllowsTerm_of_mem_minimallyAllowsTermOfFinsetβ©
C. Other properties of minimallyAllowsTermsOfFinset
We show two other properties of minimallyAllowsTermsOfFinset.
C.1. Monotonicity of minimallyAllowsTermsOfFinset in allowed sets of charges
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S5':Finset π©S10:Finset π©S10':Finset π©T:PotentialTermh5:S5' β S5h10:S10' β S10x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5' S10' Th1:x β ofFinset S5' S10'β’ x.MinimallyAllowsTerm T
All goals completed! π
C.2. Not phenomenologically constrained if in minimallyAllowsTermsOfFinset for topYukawa
We show that every term which is in minimallyAllowsTermsOfFinset S5 S10 topYukawa is not
phenomenologically constrained.
lemma not_isPhenoConstrained_of_minimallyAllowsTermsOfFinset_topYukawa
{S5 S10 : Finset π©} {x : ChargeSpectrum π©}
(hx : x β minimallyAllowsTermsOfFinset S5 S10 topYukawa) :
Β¬ x.IsPhenoConstrained := π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:x β minimallyAllowsTermsOfFinset S5 S10 topYukawaβ’ Β¬x.IsPhenoConstrained
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©x:ChargeSpectrum π©hx:β a b,
((a β S5 β§ b.toFinset β S10 β§ b.card = 2) β§ -a + b.sum = 0) β§
{ qHd := none, qHu := some a, Q5 := β
, Q10 := b.toFinset } = xβ’ Β¬x.IsPhenoConstrained
π©:TypeinstβΒΉ:DecidableEq π©instβ:AddCommGroup π©S5:Finset π©S10:Finset π©qHu:π©Q10:Multiset π©h1:(qHu β S5 β§ Q10.toFinset β S10 β§ Q10.card = 2) β§ -qHu + Q10.sum = 0β’ Β¬{ qHd := none, qHu := some qHu, Q5 := β
, Q10 := Q10.toFinset }.IsPhenoConstrained
All goals completed! π