Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.AllowsTermPheno 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 monotonicity.
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. Phenomenological 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.
@[expose] public sectionA. Phenomenological constrained charge spectra
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}.
def IsPhenoConstrained (x : ChargeSpectrum π©) : Prop :=
x.AllowsTerm ΞΌ β¨ x.AllowsTerm Ξ² β¨ x.AllowsTerm Ξ β¨ x.AllowsTerm W2 β¨ x.AllowsTerm W4 β¨
x.AllowsTerm K1 β¨ x.AllowsTerm K2 β¨ x.AllowsTerm W1
A.1. Decidability of IsPhenoConstrained
instance decidableIsPhenoConstrained [DecidableEq π©] (x : ChargeSpectrum π©) :
Decidable x.IsPhenoConstrained :=
inferInstanceAs (Decidable (x.AllowsTerm ΞΌ β¨ x.AllowsTerm Ξ² β¨ x.AllowsTerm Ξ β¨ x.AllowsTerm W2
β¨ x.AllowsTerm W4 β¨ x.AllowsTerm K1 β¨ x.AllowsTerm K2 β¨ x.AllowsTerm W1))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]
lemma not_isPhenoConstrained_empty :
Β¬ IsPhenoConstrained (β
: ChargeSpectrum π©) := π©:Typeinstβ:AddCommGroup π©β’ Β¬β
.IsPhenoConstrained
All goals completed! π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.
lemma isPhenoConstrained_mono {x y : ChargeSpectrum π©} (h : x β y)
(hx : x.IsPhenoConstrained) : y.IsPhenoConstrained := π©:Typeinstβ:AddCommGroup π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yhx:x.IsPhenoConstrainedβ’ y.IsPhenoConstrained
π©:Typeinstβ:AddCommGroup π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yhx:x.AllowsTerm ΞΌ β¨
x.AllowsTerm Ξ² β¨
x.AllowsTerm Ξ β¨ x.AllowsTerm W2 β¨ x.AllowsTerm W4 β¨ x.AllowsTerm K1 β¨ x.AllowsTerm K2 β¨ x.AllowsTerm W1β’ y.AllowsTerm ΞΌ β¨
y.AllowsTerm Ξ² β¨
y.AllowsTerm Ξ β¨ y.AllowsTerm W2 β¨ y.AllowsTerm W4 β¨ y.AllowsTerm K1 β¨ y.AllowsTerm K2 β¨ y.AllowsTerm W1
π©:Typeinstβ:AddCommGroup π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yhr:x.AllowsTerm ΞΌβ’ y.AllowsTerm ΞΌ β¨
y.AllowsTerm Ξ² β¨
y.AllowsTerm Ξ β¨ y.AllowsTerm W2 β¨ y.AllowsTerm W4 β¨ y.AllowsTerm K1 β¨ y.AllowsTerm K2 β¨ y.AllowsTerm W1π©:Typeinstβ:AddCommGroup π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yhr:x.AllowsTerm Ξ²β’ y.AllowsTerm ΞΌ β¨
y.AllowsTerm Ξ² β¨
y.AllowsTerm Ξ β¨ y.AllowsTerm W2 β¨ y.AllowsTerm W4 β¨ y.AllowsTerm K1 β¨ y.AllowsTerm K2 β¨ y.AllowsTerm W1π©:Typeinstβ:AddCommGroup π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yhr:x.AllowsTerm Ξβ’ y.AllowsTerm ΞΌ β¨
y.AllowsTerm Ξ² β¨
y.AllowsTerm Ξ β¨ y.AllowsTerm W2 β¨ y.AllowsTerm W4 β¨ y.AllowsTerm K1 β¨ y.AllowsTerm K2 β¨ y.AllowsTerm W1π©:Typeinstβ:AddCommGroup π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yhr:x.AllowsTerm W2β’ y.AllowsTerm ΞΌ β¨
y.AllowsTerm Ξ² β¨
y.AllowsTerm Ξ β¨ y.AllowsTerm W2 β¨ y.AllowsTerm W4 β¨ y.AllowsTerm K1 β¨ y.AllowsTerm K2 β¨ y.AllowsTerm W1π©:Typeinstβ:AddCommGroup π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yhr:x.AllowsTerm W4β’ y.AllowsTerm ΞΌ β¨
y.AllowsTerm Ξ² β¨
y.AllowsTerm Ξ β¨ y.AllowsTerm W2 β¨ y.AllowsTerm W4 β¨ y.AllowsTerm K1 β¨ y.AllowsTerm K2 β¨ y.AllowsTerm W1π©:Typeinstβ:AddCommGroup π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yhr:x.AllowsTerm K1β’ y.AllowsTerm ΞΌ β¨
y.AllowsTerm Ξ² β¨
y.AllowsTerm Ξ β¨ y.AllowsTerm W2 β¨ y.AllowsTerm W4 β¨ y.AllowsTerm K1 β¨ y.AllowsTerm K2 β¨ y.AllowsTerm W1π©:Typeinstβ:AddCommGroup π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yhr:x.AllowsTerm K2β’ y.AllowsTerm ΞΌ β¨
y.AllowsTerm Ξ² β¨
y.AllowsTerm Ξ β¨ y.AllowsTerm W2 β¨ y.AllowsTerm W4 β¨ y.AllowsTerm K1 β¨ y.AllowsTerm K2 β¨ y.AllowsTerm W1π©:Typeinstβ:AddCommGroup π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yhr:x.AllowsTerm W1β’ y.AllowsTerm ΞΌ β¨
y.AllowsTerm Ξ² β¨
y.AllowsTerm Ξ β¨ y.AllowsTerm W2 β¨ y.AllowsTerm W4 β¨ y.AllowsTerm K1 β¨ y.AllowsTerm K2 β¨ y.AllowsTerm W1
all_goals
π©:Typeinstβ:AddCommGroup π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yhr:x.AllowsTerm W1h':y.AllowsTerm W1β’ y.AllowsTerm ΞΌ β¨
y.AllowsTerm Ξ² β¨
y.AllowsTerm Ξ β¨ y.AllowsTerm W2 β¨ y.AllowsTerm W4 β¨ y.AllowsTerm K1 β¨ y.AllowsTerm K2 β¨ y.AllowsTerm W1
All goals completed! πB. Charges of pheno-constraining terms in the super potential
The collection of charges of super-potential terms leading to a pheno-constrained model.
def phenoConstrainingChargesSP (x : ChargeSpectrum π©) : Multiset π© :=
x.ofPotentialTerm' ΞΌ + x.ofPotentialTerm' Ξ² + x.ofPotentialTerm' Ξ +
x.ofPotentialTerm' W2 + x.ofPotentialTerm' W4 + x.ofPotentialTerm' W1B.1. The empty charge spectrum has an empty set of pheno-constraining term charges
@[simp]
lemma phenoConstrainingChargesSP_empty :
phenoConstrainingChargesSP (β
: ChargeSpectrum π©) = β
:= π©:Typeinstβ:AddCommGroup π©β’ β
.phenoConstrainingChargesSP = β
All goals completed! πB.2. The charges of pheno-constraining terms in the SP is monotone
lemma phenoConstrainingChargesSP_mono [DecidableEq π©] {x y : ChargeSpectrum π©} (h : x β y) :
x.phenoConstrainingChargesSP β y.phenoConstrainingChargesSP := π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yβ’ x.phenoConstrainingChargesSP β y.phenoConstrainingChargesSP
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yβ’ x.ofPotentialTerm' ΞΌ + x.ofPotentialTerm' Ξ² + x.ofPotentialTerm' Ξ + x.ofPotentialTerm' W2 + x.ofPotentialTerm' W4 +
x.ofPotentialTerm' W1 β
y.ofPotentialTerm' ΞΌ + y.ofPotentialTerm' Ξ² + y.ofPotentialTerm' Ξ + y.ofPotentialTerm' W2 + y.ofPotentialTerm' W4 +
y.ofPotentialTerm' W1
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yβ’ β β¦x_1 : π©β¦,
x_1 β
x.ofPotentialTerm' ΞΌ + x.ofPotentialTerm' Ξ² + x.ofPotentialTerm' Ξ + x.ofPotentialTerm' W2 +
x.ofPotentialTerm' W4 +
x.ofPotentialTerm' W1 β
x_1 β
y.ofPotentialTerm' ΞΌ + y.ofPotentialTerm' Ξ² + y.ofPotentialTerm' Ξ + y.ofPotentialTerm' W2 +
y.ofPotentialTerm' W4 +
y.ofPotentialTerm' W1
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yz:π©β’ z β
x.ofPotentialTerm' ΞΌ + x.ofPotentialTerm' Ξ² + x.ofPotentialTerm' Ξ + x.ofPotentialTerm' W2 + x.ofPotentialTerm' W4 +
x.ofPotentialTerm' W1 β
z β
y.ofPotentialTerm' ΞΌ + y.ofPotentialTerm' Ξ² + y.ofPotentialTerm' Ξ + y.ofPotentialTerm' W2 + y.ofPotentialTerm' W4 +
y.ofPotentialTerm' W1
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yz:π©β’ z β x.ofPotentialTerm' ΞΌ β¨
z β x.ofPotentialTerm' Ξ² β¨
z β x.ofPotentialTerm' Ξ β¨ z β x.ofPotentialTerm' W2 β¨ z β x.ofPotentialTerm' W4 β¨ z β x.ofPotentialTerm' W1 β
z β y.ofPotentialTerm' ΞΌ β¨
z β y.ofPotentialTerm' Ξ² β¨
z β y.ofPotentialTerm' Ξ β¨ z β y.ofPotentialTerm' W2 β¨ z β y.ofPotentialTerm' W4 β¨ z β y.ofPotentialTerm' W1
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yz:π©hr:z β x.ofPotentialTerm' ΞΌ β¨
z β x.ofPotentialTerm' Ξ² β¨
z β x.ofPotentialTerm' Ξ β¨ z β x.ofPotentialTerm' W2 β¨ z β x.ofPotentialTerm' W4 β¨ z β x.ofPotentialTerm' W1β’ z β y.ofPotentialTerm' ΞΌ β¨
z β y.ofPotentialTerm' Ξ² β¨
z β y.ofPotentialTerm' Ξ β¨ z β y.ofPotentialTerm' W2 β¨ z β y.ofPotentialTerm' W4 β¨ z β y.ofPotentialTerm' W1
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yz:π©hr:z β x.ofPotentialTerm' ΞΌβ’ z β y.ofPotentialTerm' ΞΌ β¨
z β y.ofPotentialTerm' Ξ² β¨
z β y.ofPotentialTerm' Ξ β¨ z β y.ofPotentialTerm' W2 β¨ z β y.ofPotentialTerm' W4 β¨ z β y.ofPotentialTerm' W1π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yz:π©hr:z β x.ofPotentialTerm' Ξ²β’ z β y.ofPotentialTerm' ΞΌ β¨
z β y.ofPotentialTerm' Ξ² β¨
z β y.ofPotentialTerm' Ξ β¨ z β y.ofPotentialTerm' W2 β¨ z β y.ofPotentialTerm' W4 β¨ z β y.ofPotentialTerm' W1π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yz:π©hr:z β x.ofPotentialTerm' Ξβ’ z β y.ofPotentialTerm' ΞΌ β¨
z β y.ofPotentialTerm' Ξ² β¨
z β y.ofPotentialTerm' Ξ β¨ z β y.ofPotentialTerm' W2 β¨ z β y.ofPotentialTerm' W4 β¨ z β y.ofPotentialTerm' W1π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yz:π©hr:z β x.ofPotentialTerm' W2β’ z β y.ofPotentialTerm' ΞΌ β¨
z β y.ofPotentialTerm' Ξ² β¨
z β y.ofPotentialTerm' Ξ β¨ z β y.ofPotentialTerm' W2 β¨ z β y.ofPotentialTerm' W4 β¨ z β y.ofPotentialTerm' W1π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yz:π©hr:z β x.ofPotentialTerm' W4β’ z β y.ofPotentialTerm' ΞΌ β¨
z β y.ofPotentialTerm' Ξ² β¨
z β y.ofPotentialTerm' Ξ β¨ z β y.ofPotentialTerm' W2 β¨ z β y.ofPotentialTerm' W4 β¨ z β y.ofPotentialTerm' W1π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yz:π©hr:z β x.ofPotentialTerm' W1β’ z β y.ofPotentialTerm' ΞΌ β¨
z β y.ofPotentialTerm' Ξ² β¨
z β y.ofPotentialTerm' Ξ β¨ z β y.ofPotentialTerm' W2 β¨ z β y.ofPotentialTerm' W4 β¨ z β y.ofPotentialTerm' W1
all_goals
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yz:π©hr:z β x.ofPotentialTerm' W1h':z β y.ofPotentialTerm' W1β’ z β y.ofPotentialTerm' ΞΌ β¨
z β y.ofPotentialTerm' Ξ² β¨
z β y.ofPotentialTerm' Ξ β¨ z β y.ofPotentialTerm' W2 β¨ z β y.ofPotentialTerm' W4 β¨ z β y.ofPotentialTerm' W1
All goals completed! π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.
The proposition which is true if the addition of a charge q5 to a set of charge x leads
x to being phenomenologically constrained.
def IsPhenoConstrainedQ5 [DecidableEq π©] (x : ChargeSpectrum π©) (q5 : π©) : Prop :=
x.AllowsTermQ5 q5 ΞΌ β¨ x.AllowsTermQ5 q5 Ξ² β¨ x.AllowsTermQ5 q5 Ξ β¨ x.AllowsTermQ5 q5 W2 β¨
x.AllowsTermQ5 q5 W4 β¨
x.AllowsTermQ5 q5 K1 β¨ x.AllowsTermQ5 q5 K2 β¨ x.AllowsTermQ5 q5 W1
C.2. Reducing the condition IsPhenoConstrainedQ5
lemma isPhenoConstrainedQ5_iff [DecidableEq π©] (x : ChargeSpectrum π©) (q5 : π©) :
x.IsPhenoConstrainedQ5 q5 β
x.AllowsTermQ5 q5 Ξ² β¨ x.AllowsTermQ5 q5 Ξ β¨ x.AllowsTermQ5 q5 W4 β¨
x.AllowsTermQ5 q5 K1 β¨ x.AllowsTermQ5 q5 W1 := π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©q5:π©β’ x.IsPhenoConstrainedQ5 q5 β
x.AllowsTermQ5 q5 Ξ² β¨ x.AllowsTermQ5 q5 Ξ β¨ x.AllowsTermQ5 q5 W4 β¨ x.AllowsTermQ5 q5 K1 β¨ x.AllowsTermQ5 q5 W1
All goals completed! π
C.3. Decidability of IsPhenoConstrainedQ5
instance decidableIsPhenoConstrainedQ5 [DecidableEq π©] (x : ChargeSpectrum π©) (q5 : π©) :
Decidable (x.IsPhenoConstrainedQ5 q5) :=
decidable_of_iff _ (isPhenoConstrainedQ5_iff x q5).symm
C.4. Charge spectra with added Q5 charge is pheno-constrained iff
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 W1 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm W1β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ5 q5 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrained
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 W1β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ5 q5 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm W1β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ5 q5 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrained
all_goals
All goals completed! π
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ5 q5 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrained β
{ qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrained π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ5 q5 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedβ’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrained
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ5 q5β’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedβ’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrained
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ5 q5β’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrained π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 ΞΌ β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 Ξ² β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 Ξ β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 W2 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 W4 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 K1 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 K2 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 W1β’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrained
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 ΞΌβ’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 Ξ²β’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 Ξβ’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 W2β’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 W4β’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 K1β’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 K2β’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 W1β’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrained
all_goals
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 W1hr':{ qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.AllowsTerm W1β’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrained
All goals completed! π
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedβ’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.IsPhenoConstrained π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q5:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedβ’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 } β { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }
All goals completed! π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.
The proposition which is true if the addition of a charge q10 to a set of charges x leads
x to being phenomenologically constrained.
def IsPhenoConstrainedQ10 [DecidableEq π©] (x : ChargeSpectrum π©) (q10 : π©) : Prop :=
x.AllowsTermQ10 q10 ΞΌ β¨ x.AllowsTermQ10 q10 Ξ² β¨ x.AllowsTermQ10 q10 Ξ β¨ x.AllowsTermQ10 q10 W2 β¨
x.AllowsTermQ10 q10 W4 β¨
x.AllowsTermQ10 q10 K1 β¨ x.AllowsTermQ10 q10 K2 β¨ x.AllowsTermQ10 q10 W1
D.2. Reducing the condition IsPhenoConstrainedQ10
lemma isPhenoConstrainedQ10_iff [DecidableEq π©] (x : ChargeSpectrum π©) (q10 : π©) :
x.IsPhenoConstrainedQ10 q10 β x.AllowsTermQ10 q10 Ξ β¨ x.AllowsTermQ10 q10 W2 β¨
x.AllowsTermQ10 q10 K1 β¨ x.AllowsTermQ10 q10 K2 β¨ x.AllowsTermQ10 q10 W1 := π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©x:ChargeSpectrum π©q10:π©β’ x.IsPhenoConstrainedQ10 q10 β
x.AllowsTermQ10 q10 Ξ β¨
x.AllowsTermQ10 q10 W2 β¨ x.AllowsTermQ10 q10 K1 β¨ x.AllowsTermQ10 q10 K2 β¨ x.AllowsTermQ10 q10 W1
All goals completed! π
D.3. Decidability of IsPhenoConstrainedQ10
instance decidableIsPhenoConstrainedQ10 [DecidableEq π©] (x : ChargeSpectrum π©) (q10 : π©) :
Decidable (x.IsPhenoConstrainedQ10 q10) :=
decidable_of_iff _ (isPhenoConstrainedQ10_iff x q10).symm
D.4. Charge spectra with added Q10 charge is pheno-constrained iff
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 W1 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm W1β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ10 q10 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrained
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 W1β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ10 q10 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm W1β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ10 q10 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrained
all_goals
All goals completed! π
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ10 q10 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrained β
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrained π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ10 q10 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedβ’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrained
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ10 q10β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedβ’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrained
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedQ10 q10β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrained π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 ΞΌ β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 Ξ² β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 Ξ β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 W2 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 W4 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 K1 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 K2 β¨
{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 W1β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrained
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 ΞΌβ’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 Ξ²β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 Ξβ’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 W2β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 W4β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 K1β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 K2β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrainedπ©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 W1β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrained
all_goals
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 W1hr':{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.AllowsTerm W1β’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrained
All goals completed! π
π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedβ’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.IsPhenoConstrained π©:TypeinstβΒΉ:AddCommGroup π©instβ:DecidableEq π©qHd:Option π©qHu:Option π©Q5:Finset π©Q10:Finset π©q10:π©hr:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.IsPhenoConstrainedβ’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 } β { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }
All goals completed! π