Pheno constrained charge spectra

i. Overview

We define a predicate IsPhenoConstrained on ChargeSpectrum 𝓩 which is true if the charge spectrum allows any super-potential or Kähler potential term leading to proton decay or R-parity violation.

We prove basic properties of this predicate including monoticity.

We define some variations of this result.

ii. Key results

• IsPhenoConstrained: The predicate defining a pheno-constrained charge spectrum as one allowing any term leading to proton decay or R-parity violation.
• phenoConstrainingChargesSP: The multiset of charges of terms in the super-potential leading to a pheno-constrained charge spectrum.
• IsPhenoConstrainedQ5: The predicate defining when a charge spectrum becomes pheno-constrained after adding a single charge to the Q5 set.
• IsPhenoConstrainedQ10: The predicate defining when a charge spectrum becomes pheno-constrained after adding a single charge to the Q10 set.

iii. Table of contents

• A. Phenomenologicall constrained charge spectra
  • A.1. Decidability of IsPhenoConstrained
  • A.2. The empty charge spectrum is not pheno-constrained
  • A.3. Monotonicity of being pheno-constrained
• B. Charges of pheno-constraining terms in the super potential
  • B.1. The empty charge spectrum has an empty set of pheno-constraining term charges
  • B.2. The charges of pheno-constraining terms in the SP is monotone
• C. Phenomenologically constrained charge spectra after adding a single Q5 charge
  • C.2. Reducing the condition IsPhenoConstrainedQ5
  • C.3. Decidability of IsPhenoConstrainedQ5
  • C.4. Charge spectra with added Q5 charge is pheno-constrained iff
• D. Phenomenologically constrained charge spectra after adding a single Q10 charge
  • D.2. Reducing the condition IsPhenoConstrainedQ10
  • D.3. Decidability of IsPhenoConstrainedQ10
  • D.4. Charge spectra with added Q10 charge is pheno-constrained iff

iv. References

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

A. Phenomenologicall constrained charge spectra

def SuperSymmetry.SU5.ChargeSpectrum.IsPhenoConstrained {𝓩 : Type} [AddCommGroup 𝓩] (x : ChargeSpectrum 𝓩) : Prop

A charge is pheno-constrained if it leads to the presence of any term causing proton decay {W1, Λ, W2, K1} or R-parity violation {β, Λ, W2, W4, K1, K2}.

Equations

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

A.1. Decidability of IsPhenoConstrained

instance SuperSymmetry.SU5.ChargeSpectrum.decidableIsPhenoConstrained {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) : Decidable x.IsPhenoConstrained

Equations

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

A.2. The empty charge spectrum is not pheno-constrained

The empty charge spectrum does not allow any terms, and so is not pheno-constrained.

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.not_isPhenoConstrained_empty {𝓩 : Type} [AddCommGroup 𝓩] : ¬∅.IsPhenoConstrained

A.3. Monotonicity of being pheno-constrained

If a charge spectrum x is pheno-constrained, then any charge spectrum y containing x is also pheno-constrained.

theorem SuperSymmetry.SU5.ChargeSpectrum.isPhenoConstrained_mono {𝓩 : Type} [AddCommGroup 𝓩] {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) (hx : x.IsPhenoConstrained) : y.IsPhenoConstrained

B. Charges of pheno-constraining terms in the super potential

def SuperSymmetry.SU5.ChargeSpectrum.phenoConstrainingChargesSP {𝓩 : Type} [AddCommGroup 𝓩] (x : ChargeSpectrum 𝓩) : Multiset 𝓩

The collection of charges of super-potential terms leading to a pheno-constrained model.

Equations

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

B.1. The empty charge spectrum has an empty set of pheno-constraining term charges

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.phenoConstrainingChargesSP_empty {𝓩 : Type} [AddCommGroup 𝓩] : ∅.phenoConstrainingChargesSP = ∅

B.2. The charges of pheno-constraining terms in the SP is monotone

theorem SuperSymmetry.SU5.ChargeSpectrum.phenoConstrainingChargesSP_mono {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) : x.phenoConstrainingChargesSP ⊆ y.phenoConstrainingChargesSP

C. Phenomenologically constrained charge spectra after adding a single Q5 charge

We now define IsPhenoConstrainedQ5 which gives the condition that a charge spectrum becomes pheno-constrained after adding a single charge to the Q5 set.

def SuperSymmetry.SU5.ChargeSpectrum.IsPhenoConstrainedQ5 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (q5 : 𝓩) : Prop

The proposition which is true if the addition of a charge q5 to a set of charegs x leads x to being phenomenologically constrained.

Equations

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

C.2. Reducing the condition IsPhenoConstrainedQ5

theorem SuperSymmetry.SU5.ChargeSpectrum.isPhenoConstrainedQ5_iff {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (q5 : 𝓩) : x.IsPhenoConstrainedQ5 q5 ↔ x.AllowsTermQ5 q5 PotentialTerm.β ∨ x.AllowsTermQ5 q5 PotentialTerm.Λ ∨ x.AllowsTermQ5 q5 PotentialTerm.W4 ∨ x.AllowsTermQ5 q5 PotentialTerm.K1 ∨ x.AllowsTermQ5 q5 PotentialTerm.W1

C.3. Decidability of IsPhenoConstrainedQ5

instance SuperSymmetry.SU5.ChargeSpectrum.decidableIsPhenoConstrainedQ5 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (q5 : 𝓩) : Decidable (x.IsPhenoConstrainedQ5 q5)

Equations

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

C.4. Charge spectra with added Q5 charge is pheno-constrained iff

theorem SuperSymmetry.SU5.ChargeSpectrum.isPhenoConstrained_insertQ5_iff_isPhenoConstrainedQ5 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q5 : 𝓩} : { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrained ↔ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ5 q5 ∨ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrained

D. Phenomenologically constrained charge spectra after adding a single Q10 charge

We now define IsPhenoConstrainedQ10 which gives the condition that a charge spectrum becomes pheno-constrained after adding a single charge to the Q10 set.

def SuperSymmetry.SU5.ChargeSpectrum.IsPhenoConstrainedQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (q10 : 𝓩) : Prop

The proposition which is true if the addition of a charge q10 to a set of charegs x leads x to being phenomenologically constrained.

Equations

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

D.2. Reducing the condition IsPhenoConstrainedQ10

theorem SuperSymmetry.SU5.ChargeSpectrum.isPhenoConstrainedQ10_iff {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (q10 : 𝓩) : x.IsPhenoConstrainedQ10 q10 ↔ x.AllowsTermQ10 q10 PotentialTerm.Λ ∨ x.AllowsTermQ10 q10 PotentialTerm.W2 ∨ x.AllowsTermQ10 q10 PotentialTerm.K1 ∨ x.AllowsTermQ10 q10 PotentialTerm.K2 ∨ x.AllowsTermQ10 q10 PotentialTerm.W1

D.3. Decidability of IsPhenoConstrainedQ10

instance SuperSymmetry.SU5.ChargeSpectrum.decidableIsPhenoConstrainedQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (q10 : 𝓩) : Decidable (x.IsPhenoConstrainedQ10 q10)

Equations

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

D.4. Charge spectra with added Q10 charge is pheno-constrained iff

theorem SuperSymmetry.SU5.ChargeSpectrum.isPhenoConstrained_insertQ10_iff_isPhenoConstrainedQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q10 : 𝓩} : { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrained ↔ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ10 q10 ∨ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrained