Phenomenologically closed sets of charge spectra

i. Overview

The main goal of this file is to prove the lemma completeness_of_isPhenoClosedQ5_isPhenoClosedQ10, which allows us to prove that a multiset of charge spectra contains all phenomenologically viable charge spectra, given a finite set of allowed 5-bar and 10-dimensional.

This lemma relies on the multiset of charge spectra satisfying a number of conditions, which include three which are defined in this file: IsPhenoClosedQ5, IsPhenoClosedQ10 and ContainsPhenoCompletionsOfMinimallyAllows.

ii. Key results

• IsPhenoClosedQ5 : The proposition that a multiset of charges is phenomenologically closed under addition of 5-bar charges from a finite set S5.
• IsPhenoClosedQ10 : The proposition that a multiset of charges is phenomenologically closed under addition of 10-dimensional charges from a finite set S10.
• ContainsPhenoCompletionsOfMinimallyAllows : The proposition that a multiset of charges contains all phenomenologically viable completions of charge spectra which permit the top Yukawa.
• completeMinSubset : For a given S5 S10 : Finset 𝓩, the minimal multiset of charges which satisfies the condition ContainsPhenoCompletionsOfMinimallyAllows.
• completeness_of_isPhenoClosedQ5_isPhenoClosedQ10 : A lemma for simplifying the proof that a multiset contains all phenomenologically viable charge spectra.
• viableChargesMultiset : A computable multiset containing all phenomenologically viable charge spectra for a given S5 S10 : Finset 𝓩.

iii. Table of contents

• A. Phenomenologically closed under additions of 5-bar charges
  • A.1. Simplification using pheno-constrained due to additional of 5-bar charge
• B. Phenomenologically closed under additions of 10d charges
  • B.1. Simplification using pheno-constrained due to additional of 10d charge
• C. Prop for multiset containing all pheno-viable completions of charges permitting top Yukawa
  • C.1. Simplification using fast version of completions of charges permitting top Yukawa
  • C.2. Decidability of proposition
  • C.3. Monotonicity of proposition
  • C.4. completeMinSubset: Minimal multiset with viable completions of top-permitting charges
    • C.4.1. The multiset completeMinSubset has no duplicates
    • C.4.2. The multiset completeMinSubset is minimal
    • C.4.3. The multiset completeMinSubset contains all completions
• D. Multisets containing all pheno-viable charge spectra
  • D.1. Lemma for simplifying proof that a multiset contains all pheno-viable charge spectra
  • D.2. Computable multiset containing all pheno-viable charge spectra

iv. References

There are no known references for the material in this module.

A. Phenomenologically closed under additions of 5-bar charges

def SuperSymmetry.SU5.ChargeSpectrum.IsPhenoClosedQ5 {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] (S5 : Finset 𝓩) (charges : Multiset (ChargeSpectrum 𝓩)) : Prop

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.

A.1. Simplification using pheno-constrained due to additional of 5-bar charge

theorem SuperSymmetry.SU5.ChargeSpectrum.isPhenClosedQ5_of_isPhenoConstrainedQ5 {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] {S5 : Finset 𝓩} {charges : Multiset (ChargeSpectrum 𝓩)} (h : ∀ q5 ∈ S5, ∀ x ∈ charges, have y := { qHd := x.qHd, qHu := x.qHu, Q5 := insert q5 x.Q5, Q10 := x.Q10 }; x.IsPhenoConstrainedQ5 q5 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1) : IsPhenoClosedQ5 S5 charges

B. Phenomenologically closed under additions of 10d charges

def SuperSymmetry.SU5.ChargeSpectrum.IsPhenoClosedQ10 {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] (S10 : Finset 𝓩) (charges : Multiset (ChargeSpectrum 𝓩)) : Prop

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.

B.1. Simplification using pheno-constrained due to additional of 10d charge

theorem SuperSymmetry.SU5.ChargeSpectrum.isPhenClosedQ10_of_isPhenoConstrainedQ10 {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] {S10 : Finset 𝓩} {charges : Multiset (ChargeSpectrum 𝓩)} (h : ∀ q10 ∈ S10, ∀ x ∈ charges, have y := { qHd := x.qHd, qHu := x.qHu, Q5 := x.Q5, Q10 := insert q10 x.Q10 }; x.IsPhenoConstrainedQ10 q10 ∨ y ∈ charges ∨ y.YukawaGeneratesDangerousAtLevel 1) : IsPhenoClosedQ10 S10 charges

C. Prop for multiset containing all pheno-viable completions of charges permitting top Yukawa

def SuperSymmetry.SU5.ChargeSpectrum.ContainsPhenoCompletionsOfMinimallyAllows {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] (S5 S10 : Finset 𝓩) (charges : Multiset (ChargeSpectrum 𝓩)) : Prop

The proposition that for multiset set of charges charges contains all viable completions of charges which allow the top Yukawa, given allowed values of 5d and 10d charges S5 and S10.

Equations

• One or more equations did not get rendered due to their size.

C.1. Simplification using fast version of completions of charges permitting top Yukawa

theorem SuperSymmetry.SU5.ChargeSpectrum.containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawa {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] {S5 S10 : Finset 𝓩} {charges : Multiset (ChargeSpectrum 𝓩)} : ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges ↔ ∀ x ∈ minimallyAllowsTermsOfFinset S5 S10 PotentialTerm.topYukawa, ∀ y ∈ completionsTopYukawa S5 x, ¬y.IsPhenoConstrained ∧ ¬y.YukawaGeneratesDangerousAtLevel 1 → y ∈ charges

C.2. Decidability of proposition

instance SuperSymmetry.SU5.ChargeSpectrum.instDecidableContainsPhenoCompletionsOfMinimallyAllows {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {charges : Multiset (ChargeSpectrum 𝓩)} : Decidable (ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges)

Equations

• One or more equations did not get rendered due to their size.

C.3. Monotonicity of proposition

theorem SuperSymmetry.SU5.ChargeSpectrum.containsPhenoCompletionsOfMinimallyAllows_of_subset {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] {S5 S10 : Finset 𝓩} {charges charges' : Multiset (ChargeSpectrum 𝓩)} (h' : ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges) (h : ∀ x ∈ charges, x ∈ charges') : ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges'

C.4. completeMinSubset: Minimal multiset with viable completions of top-permitting charges

def SuperSymmetry.SU5.ChargeSpectrum.completeMinSubset {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] (S5 S10 : Finset 𝓩) : Multiset (ChargeSpectrum 𝓩)

For a given S5 S10 : Finset 𝓩, the minimal multiset of charges which satisfies the condition ContainsPhenoCompletionsOfMinimallyAllows. That is to say, every multiset of charges which satisfies ContainsPhenoCompletionsOfMinimallyAllows has completeMinSubset as a subset.

Equations

• One or more equations did not get rendered due to their size.

C.4.1. The multiset completeMinSubset has no duplicates

theorem SuperSymmetry.SU5.ChargeSpectrum.completeMinSubset_nodup {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] {S5 S10 : Finset 𝓩} : (completeMinSubset S5 S10).Nodup

C.4.2. The multiset completeMinSubset is minimal

theorem SuperSymmetry.SU5.ChargeSpectrum.completeMinSubset_subset_iff_containsPhenoCompletionsOfMinimallyAllows {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] (S5 S10 : Finset 𝓩) (charges : Multiset (ChargeSpectrum 𝓩)) : completeMinSubset S5 S10 ⊆ charges ↔ ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges

C.4.3. The multiset completeMinSubset contains all completions

theorem SuperSymmetry.SU5.ChargeSpectrum.completeMinSubset_containsPhenoCompletionsOfMinimallyAllows {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] (S5 S10 : Finset 𝓩) : ContainsPhenoCompletionsOfMinimallyAllows S5 S10 (completeMinSubset S5 S10)

D. Multisets containing all pheno-viable charge spectra

D.1. Lemma for simplifying proof that a multiset contains all pheno-viable charge spectra

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 is IsPhenoClosedQ5 with respect to S5,
• charges is IsPhenoClosedQ10 with respect to S10
• and satisfies ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges. The importance of this lemma is that it is only regarding properties of finite-set charges not of the whole space of possible charges.

theorem SuperSymmetry.SU5.ChargeSpectrum.completeness_of_isPhenoClosedQ5_isPhenoClosedQ10 {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] {S5 S10 : Finset 𝓩} {charges : Multiset (ChargeSpectrum 𝓩)} (charges_topYukawa : ∀ x ∈ charges, x.AllowsTerm PotentialTerm.topYukawa) (charges_not_isPhenoConstrained : ∀ x ∈ charges, ¬x.IsPhenoConstrained) (charges_yukawa : ∀ x ∈ charges, ¬x.YukawaGeneratesDangerousAtLevel 1) (charges_complete : ∀ x ∈ charges, x.IsComplete) (charges_isPhenoClosedQ5 : IsPhenoClosedQ5 S5 charges) (charges_isPhenoClosedQ10 : IsPhenoClosedQ10 S10 charges) (charges_exist : ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges) {x : ChargeSpectrum 𝓩} (hsub : x ∈ ofFinset S5 S10) : x ∈ charges ↔ x.AllowsTerm PotentialTerm.topYukawa ∧ ¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1 ∧ x.IsComplete

D.2. Computable multiset containing all pheno-viable charge spectra

unsafe def SuperSymmetry.SU5.ChargeSpectrum.viableChargesMultiset {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] (S5 S10 : Finset 𝓩) : Multiset (ChargeSpectrum 𝓩)

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 satisfies: 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.

unsafe def SuperSymmetry.SU5.ChargeSpectrum.viableChargesMultiset.aux {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] (S5 S10 : Finset 𝓩) : Multiset (ChargeSpectrum 𝓩) → Multiset (ChargeSpectrum 𝓩) → Multiset (ChargeSpectrum 𝓩)

Auxiliary recursive function to define viableChargesMultiset.

Equations

• One or more equations did not get rendered due to their size.