Note this file takes a long time to compile.

Charges which are not pheno-constrained and do not regenerate dangerous couplings with Yukawas

In this module we give a multiset of ℤ-valued charges which have values allowed by a CodimensionOneConfig, I, which permit a top Yukawa coupling, are not phenomenologically constrained, and do not regenerate dangerous couplings with one insertion of a Yuakawa coupling.

Key results

• viableCharges contains 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.
• The lemma mem_viableCharges_iff expresses membership of viableCharges 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_iff follows directly from completeness_of_isPhenoClosedQ5_isPhenoClosedQ10 and a number of conditions on viableCharges which can be proved using the decide tactic.
• viableCharges itself is constructed via viableCompletions which contains all completions of charges which minimally allow the top Yukawa, which are not phenomenologically constrained, and do not regenerate dangerous couplings.

Implementation details

• 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.

Viable completions

theorem FTheory.SU5.Charges.viableCompletions_card (I : CodimensionOneConfig) : (FTheory.SU5.Charges.viableCompletions✝ I).card = if I = CodimensionOneConfig.same then 70 else if I = CodimensionOneConfig.nearestNeighbor then 48 else 37

theorem FTheory.SU5.Charges.viableCompletions_nodup (I : CodimensionOneConfig) : (FTheory.SU5.Charges.viableCompletions✝ I).Nodup

theorem FTheory.SU5.Charges.viableCompletions_isPhenoConstrained (I : CodimensionOneConfig) (x : SuperSymmetry.SU5.Charges) : x ∈ FTheory.SU5.Charges.viableCompletions✝ I → ¬x.IsPhenoConstrained

theorem FTheory.SU5.Charges.viableCompletions_yukawaGeneratesDangerousAtLevel_one (I : CodimensionOneConfig) (x : SuperSymmetry.SU5.Charges) : x ∈ FTheory.SU5.Charges.viableCompletions✝ I → ¬x.YukawaGeneratesDangerousAtLevel 1

theorem FTheory.SU5.Charges.containsPhenoCompletionsOfMinimallyAllows_viableCompletions (I : CodimensionOneConfig) : SuperSymmetry.SU5.Charges.ContainsPhenoCompletionsOfMinimallyAllows I.allowedBarFiveCharges I.allowedTenCharges (FTheory.SU5.Charges.viableCompletions✝ I)

The multisets of viable charges.

def FTheory.SU5.Charges.viableChargesAdditional : CodimensionOneConfig → Multiset SuperSymmetry.SU5.Charges

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.

theorem FTheory.SU5.Charges.viableChargesAdditional_nodup (I : CodimensionOneConfig) : (viableChargesAdditional I).Nodup

theorem FTheory.SU5.Charges.not_isPhenoConstrained_of_mem_viableChargesAdditional (I : CodimensionOneConfig) (x : SuperSymmetry.SU5.Charges) : x ∈ viableChargesAdditional I → ¬x.IsPhenoConstrained

theorem FTheory.SU5.Charges.yukawaGeneratesDangerousAtLevel_one_of_mem_viableChargesAdditional (I : CodimensionOneConfig) (x : SuperSymmetry.SU5.Charges) : x ∈ viableChargesAdditional I → ¬x.YukawaGeneratesDangerousAtLevel 1

theorem FTheory.SU5.Charges.viableCompletions_disjiont_viableChargesAdditional (I : CodimensionOneConfig) : Disjoint (FTheory.SU5.Charges.viableCompletions✝ I) (viableChargesAdditional I)

def FTheory.SU5.Charges.viableCharges (I : CodimensionOneConfig) : Multiset SuperSymmetry.SU5.Charges

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

• FTheory.SU5.Charges.viableCharges I = FTheory.SU5.Charges.viableCompletions✝ I + FTheory.SU5.Charges.viableChargesAdditional I

Basic properties

theorem FTheory.SU5.Charges.viableCharges_nodup (I : CodimensionOneConfig) : (viableCharges I).Nodup

theorem FTheory.SU5.Charges.viableCharges_card (I : CodimensionOneConfig) : (viableCharges I).card = if I = CodimensionOneConfig.same then 102 else if I = CodimensionOneConfig.nearestNeighbor then 71 else 51

theorem FTheory.SU5.Charges.isComplete_of_mem_viableCharges (I : CodimensionOneConfig) (x : SuperSymmetry.SU5.Charges) : x ∈ viableCharges I → x.IsComplete

theorem FTheory.SU5.Charges.allowsTerm_topYukawa_of_mem_viableCharges (I : CodimensionOneConfig) (x : SuperSymmetry.SU5.Charges) : x ∈ viableCharges I → x.AllowsTerm SuperSymmetry.SU5.PotentialTerm.topYukawa

theorem FTheory.SU5.Charges.not_isPhenoConstrained_of_mem_viableCharges (I : CodimensionOneConfig) (x : SuperSymmetry.SU5.Charges) : x ∈ viableCharges I → ¬x.IsPhenoConstrained

theorem FTheory.SU5.Charges.not_yukawaGeneratesDangerousAtLevel_one_of_mem_viableCharges (I : CodimensionOneConfig) (x : SuperSymmetry.SU5.Charges) : x ∈ viableCharges I → ¬x.YukawaGeneratesDangerousAtLevel 1

theorem FTheory.SU5.Charges.card_five_bar_le_of_mem_viableCharges (I : CodimensionOneConfig) (x : SuperSymmetry.SU5.Charges) : x ∈ viableCharges I → x.2.2.1.card ≤ 2

theorem FTheory.SU5.Charges.card_ten_le_of_mem_viableCharges (I : CodimensionOneConfig) (x : SuperSymmetry.SU5.Charges) : x ∈ viableCharges I → x.2.2.2.card ≤ 2

Closed under inserting 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.

theorem FTheory.SU5.Charges.isPhenoClosedQ5_viableCharges (I : CodimensionOneConfig) : SuperSymmetry.SU5.Charges.IsPhenoClosedQ5 I.allowedBarFiveCharges (viableCharges I)

Inserting a q5 charge into an element of viableCharges I either

1. produces another element of viableCharges I, or
2. produce a charge which is phenomenolically constrained or regenerates dangourous couplings with the Yukawas.

theorem FTheory.SU5.Charges.isPhenoClosedQ10_viableCharges (I : CodimensionOneConfig) : SuperSymmetry.SU5.Charges.IsPhenoClosedQ10 I.allowedTenCharges (viableCharges I)

Inserting a q10 charge into an element of viableCharges I either

1. produces another element of viableCharges I, or
2. produce a charge which is phenomenolically constrained or regenerates dangourous couplings with the Yukawas.

Proof of completeness.

theorem FTheory.SU5.Charges.viableCompletions_subset_viableCharges (I : CodimensionOneConfig) (x : SuperSymmetry.SU5.Charges) : x ∈ FTheory.SU5.Charges.viableCompletions✝ I → x ∈ viableCharges I

theorem FTheory.SU5.Charges.mem_viableCharges_iff {I : CodimensionOneConfig} {x : SuperSymmetry.SU5.Charges} (hsub : x ∈ SuperSymmetry.SU5.Charges.ofFinset I.allowedBarFiveCharges I.allowedTenCharges) : x ∈ viableCharges I ↔ x.AllowsTerm SuperSymmetry.SU5.PotentialTerm.topYukawa ∧ ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1 ∧ x.IsComplete