Phenomenologically closed sets of charges #
In this module we define a number of propositions related to the phenomenological closure of sets of charges.
One of the key results within this module is the lemma
completeness_of_isPhenoClosedQ5_isPhenoClosedQ10
, which gives a quick way to
check whether a set of charges contains precisely those charges which
- allow the top Yukawa term,
- are not phenomenologically constrained,
- do not generate dangerous couplings with one singlet insertion,
- and are complete,
given allowed values of
5
d and10
d chargesS5
andS10
. This result can be used for specific sets of chargesS5
andS10
, along with some results proved bydecide
.
IsPhenoClosedQ5 #
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
IsPhenoClosedQ10 #
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposition that for multiset set of charges charges
contains all
viable completions of charges which allow the top Yukawa, given allowed values
of 5
d and 10
d charges S5
and S10
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Completeness of isPhenoClosedQ5 and isPhenoClosedQ10 #
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
isIsPhenoClosedQ5
with respect toS5
,charges
isIsPhenoClosedQ10
with respect toS10
- and satisfies
ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges
. The importance of this lemma is that it is only regarding properties of finite-setcharges
not of the whole space of possible charges.
Definitions of multisets which are phenomenologically closed #
For a given S5 S10 : Finset 𝓩
, the minimal multiset of charges which satifies
the condition ContainsPhenoCompletionsOfMinimallyAllows
.
That is to say, every multiset of charges which satifies
ContainsPhenoCompletionsOfMinimallyAllows
has completeMinSubset
as a subset.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 satifies:
completeness_of_isPhenoClosedQ5_isPhenoClosedQ10
.
Note this is fast for evaluation, but to slow with decide
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Auxillary recursive function to define viableChargesMultiset
.
Equations
- One or more equations did not get rendered due to their size.