Pheno constrained charges #
We say a charge is pheno-constrained if it leads to allows proton decay or R-parity violating terms.
We are actually intrested in the charges which are not pheno-constrained.
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.
Instances For
instance
SuperSymmetry.SU5.Charges.decidableIsPhenoConstrained
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
(x : Charges 𝓩)
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
SuperSymmetry.SU5.Charges.isPhenoConstrained_mono
{𝓩 : Type}
[AddCommGroup 𝓩]
{x y : Charges 𝓩}
(h : x ⊆ y)
(hx : x.IsPhenoConstrained)
:
def
SuperSymmetry.SU5.Charges.phenoConstrainingChargesSP
{𝓩 : Type}
[AddCommGroup 𝓩]
(x : Charges 𝓩)
:
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.
Instances For
@[simp]
theorem
SuperSymmetry.SU5.Charges.phenoConstrainingChargesSP_mono
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{x y : Charges 𝓩}
(h : x ⊆ y)
:
Is Pheno constrained Q5 addition #
def
SuperSymmetry.SU5.Charges.IsPhenoConstrainedQ5
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
(x : Charges 𝓩)
(q5 : 𝓩)
:
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.
Instances For
theorem
SuperSymmetry.SU5.Charges.isPhenoConstrainedQ5_iff
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
(x : Charges 𝓩)
(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
instance
SuperSymmetry.SU5.Charges.decidableIsPhenoConstrainedQ5
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
(x : Charges 𝓩)
(q5 : 𝓩)
:
Decidable (x.IsPhenoConstrainedQ5 q5)
Equations
- One or more equations did not get rendered due to their size.
theorem
SuperSymmetry.SU5.Charges.isPhenoConstrained_insertQ5_iff_isPhenoConstrainedQ5
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{qHd qHu : Option 𝓩}
{Q5 Q10 : Finset 𝓩}
{q5 : 𝓩}
:
def
SuperSymmetry.SU5.Charges.IsPhenoConstrainedQ10
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
(x : Charges 𝓩)
(q10 : 𝓩)
:
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.
Instances For
theorem
SuperSymmetry.SU5.Charges.isPhenoConstrainedQ10_iff
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
(x : Charges 𝓩)
(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
instance
SuperSymmetry.SU5.Charges.decidableIsPhenoConstrainedQ10
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
(x : Charges 𝓩)
(q10 : 𝓩)
:
Decidable (x.IsPhenoConstrainedQ10 q10)
Equations
- One or more equations did not get rendered due to their size.
theorem
SuperSymmetry.SU5.Charges.isPhenoConstrained_insertQ10_iff_isPhenoConstrainedQ10
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{qHd qHu : Option 𝓩}
{Q5 Q10 : Finset 𝓩}
{q10 : 𝓩}
: