Charges which are not pheno-constrained and do not regenerate dangerous couplings with Yukawas #
i. Overview #
WARNING: This file can take a long time to compute.
In this module, given a configuration of the sections in codimension one
fiber CodimensionOneConfig, we find the multiset of all
ℤ-valued charges which have values allowed by the configuration,
permit a top Yukawa coupling, are not phenomenologically constrained,
and do not regenerate dangerous couplings with one insertion of a Yukawa coupling.
The multiset of charge spectrum is called viableCharges.
The main proof that viableCharges contains all such charges is
using completeness_of_isPhenoClosedQ5_isPhenoClosedQ10.
Note this proof relies on us stating viableCharges and then verifying
that it has the required properties.
To make our lives easier, we first construct a multiset of charge spectrum called
viableCompletions which contains all completions of charges which minimally allow the top Yukawa,
which are not phenomenologically constrained, and do not regenerate dangerous couplings.
Again the proof that viableCompletions has these properties is done by
first stating viableCompletions and then verifying that it has the required properties,
primarily using ContainsPhenoCompletionsOfMinimallyAllows.
We also define viableChargesAdditional which are the multiset of charge spectrum
which are in viableCharges but not in viableCompletions. This helps split some of the
proofs.
Note that this file is slow to run, any improvements to the speed of this file will be very welcome. In particular working out a way to restrict by anomaly cancellation.
ii. Key results #
viableChargescontains all charges, for a givenCodimensionOneConfig,I, which permit a top Yukawa coupling, are not phenomenologically constrained, and do not regenerate dangerous couplings with one insertion of a Yukawa coupling.- The lemma
mem_viableCharges_iffexpresses membership ofviableCharges I, i.e. that it contains all charges which permit a top Yukawa coupling, are not phenomenologically constrained, and do not regenerate dangerous couplings. - The lemma
mem_viableCharges_ifffollows directly fromcompleteness_of_isPhenoClosedQ5_isPhenoClosedQ10and a number of conditions onviableChargeswhich can be proved using thedecidetactic. viableChargesitself is constructed viaviableCompletionswhich contains all completions of charges which minimally allow the top Yukawa, which are not phenomenologically constrained, and do not regenerate dangerous couplings.
iii. Table of contents #
- A. Viable completions of charges permitting a top Yukawa coupling
- A.1. Stating the multiset
viableCompletions - A.2. Cardinality of
viableCompletions - A.3. No duplicates of
viableCompletions - A.4. Elements of
viableCompletionsare not pheno-constrained - A.5. Elements of
viableCompletionsdo not regenerate dangerous couplings - A.6.
viableCompletionscontain all pheno-viable completions of top-yukawa permitting
- A.1. Stating the multiset
- B. The multiset of additional viable charges
- B.1. Stating the multiset
viableChargesAdditional - B.2.
viableChargesAdditionalhas no duplicates - B.3. Elements of
viableChargesAdditionalare not pheno-constrained - B.4. Elements of
viableChargesAdditionaldo not regenerate dangerous couplings - B.5.
viableChargesAdditionalis disjoint fromviableCompletions
- B.1. Stating the multiset
- C. The multiset of all viable charges given a configuration of sections
- C.1. Stating the multiset
viableCharges - C.2.
viableChargeshas no duplicates - C.3. Cardinality of
viableCharges - C.4. Elements of
viableChargeshave charges allowed by configuration - C.5. Elements of
viableChargesare complete - C.6. Elements of
viableChargespermit a top Yukawa coupling - C.7. Elements of
viableChargesare not pheno-constrained - C.8. Elements of
viableChargesdo not regenerate dangerous couplings - C.9. Elements of
viableChargeshave at most two 5-bar reps - C.10. Elements of
viableChargeshave at most two 10d reps - C.11.
viableChargesis phenomenologically closed under adding 5-bar charges - C.12.
viableChargesis phenomenologically closed under adding 10d charges - C.13.
viableCompletionsis a subset ofviableCharges - C.14.
viableChargescontains all pheno-viable charges given a section configuration
- C.1. Stating the multiset
iv. References #
There are no known references for the material in this section.
A. Viable completions of charges permitting a top Yukawa coupling #
A.1. Stating the multiset viableCompletions #
A.2. Cardinality of viableCompletions #
A.3. No duplicates of viableCompletions #
A.4. Elements of viableCompletions are not pheno-constrained #
A.5. Elements of viableCompletions do not regenerate dangerous couplings #
A.6. viableCompletions contain all pheno-viable completions of top-yukawa permitting #
B. The multiset of additional viable charges #
B.1. Stating the multiset viableChargesAdditional #
The charges in addition to viableCompletions which which permit a top Yukawa coupling,
are not phenomenologically constrained,
and do not regenerate dangerous couplings with one insertion of a Yukawa coupling.
These can be found with e.g.
- #eval (viableChargesMultiset same.allowedBarFiveCharges same.allowedTenCharges).toFinset
(completeMinSubset same.allowedBarFiveCharges same.allowedTenCharges).toFinset
Equations
- One or more equations did not get rendered due to their size.
Instances For
B.2. viableChargesAdditional has no duplicates #
B.3. Elements of viableChargesAdditional are not pheno-constrained #
B.4. Elements of viableChargesAdditional do not regenerate dangerous couplings #
B.5. viableChargesAdditional is disjoint from viableCompletions #
C. The multiset of all viable charges given a configuration of sections #
C.1. Stating the multiset viableCharges #
All charges, for a given CodimensionOneConfig, I,
which permit a top Yukawa coupling, are not phenomenologically constrained,
and do not regenerate dangerous couplings with one insertion of a Yukawa coupling.
These trees can be found with e.g.
#eval viableChargesExt nextToNearestNeighbor.
Equations
Instances For
C.2. viableCharges has no duplicates #
C.3. Cardinality of viableCharges #
C.4. Elements of viableCharges have charges allowed by configuration #
C.5. Elements of viableCharges are complete #
C.6. Elements of viableCharges permit a top Yukawa coupling #
C.7. Elements of viableCharges are not pheno-constrained #
C.8. Elements of viableCharges do not regenerate dangerous couplings #
C.9. Elements of viableCharges have at most two 5-bar reps #
C.10. Elements of viableCharges have at most two 10d reps #
C.11. viableCharges is phenomenologically closed under adding 5-bar charges #
We now show that adding a Q5 or a Q10 charge to an element of viableCharges I leads to a
charge which is either not phenomenologically constrained, or does not regenerate dangerous
couplings, or is already in viableCharges I.
Inserting a q5 charge into an element of viableCharges I either
- produces another element of
viableCharges I, or - produce a charge which is phenomenologically constrained or regenerates dangerous couplings with the Yukawas.
C.12. viableCharges is phenomenologically closed under adding 10d charges #
Inserting a q10 charge into an element of viableCharges I either
- produces another element of
viableCharges I, or - produce a charge which is phenomenologically constrained or regenerates dangerous couplings with the Yukawas.