Charges allowing terms #
The charges of representations x : Charges
allow a potential term T : PotentialTerm
if the zero charge is in the set of charges associated with that potential term.
We define this proposition AllowsTerm
and prove results about it.
We also define allowsTermForm
, which is a function that takes three integers a
, b
, and c
and a potential term T
, and returns a Charges
that allows the term T
.
We prove that any charges that allows a term T
has a
subset which can be expressed as allowsTermForm a b c T
for some integers a
, b
, and c
.
The charges of representations x : Charges
allow a potential term T : PotentialTerm
if the zero charge is in the set of charges associated with that potential term.
Equations
- x.AllowsTerm T = (0 ∈ x.ofPotentialTerm T)
Instances For
Equations
- x.instDecidableAllowsTermOfDecidableEq T = decidable_of_iff (0 ∈ x.ofPotentialTerm' T) ⋯
allowsTermForm #
A element of Charges
from three intergers a b c : ℤ
for a given potential term T
.
Defined such that allowsTermForm a b c T
always allows the potential term T
,
and if any over charge x
allows T
then it is due to a subset of the form
allowsTermForm a b c T
.
Equations
- SuperSymmetry.SU5.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.μ = (some a, some a, ∅, ∅)
- SuperSymmetry.SU5.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.β = (none, some a, {a}, ∅)
- SuperSymmetry.SU5.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.Λ = (none, none, {a, b}, {-a - b})
- SuperSymmetry.SU5.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.W1 = (none, none, {-a - b - c}, {a, b, c})
- SuperSymmetry.SU5.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.W2 = (some (-a - b - c), none, ∅, {a, b, c})
- SuperSymmetry.SU5.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.W3 = (none, some (-a), {b, -b - 2 • a}, ∅)
- SuperSymmetry.SU5.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.W4 = (some (-c - 2 • b), some (-b), {c}, ∅)
- SuperSymmetry.SU5.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.K1 = (none, none, {-a}, {b, -a - b})
- SuperSymmetry.SU5.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.K2 = (some a, some b, ∅, {-a - b})
- SuperSymmetry.SU5.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.topYukawa = (none, some (-a), ∅, {b, -a - b})
- SuperSymmetry.SU5.Charges.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.bottomYukawa = (some a, none, {b}, {-a - b})
Instances For
Insertion of Q5 #
The proposition for which says, given a charge x
adding a charge q5
permits the
existence of a potential term T
due to the addition of that charge.
Equations
- One or more equations did not get rendered due to their size.
- x.AllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.μ = (false = true)
- SuperSymmetry.SU5.Charges.AllowsTermQ5 (fst, some qHu, fst_1, snd) q5 SuperSymmetry.SU5.PotentialTerm.β = (q5 = qHu)
- x.AllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.β = (false = true)
- SuperSymmetry.SU5.Charges.AllowsTermQ5 (some qHd, some qHu, fst, snd) q5 SuperSymmetry.SU5.PotentialTerm.W4 = (q5 + qHd - qHu - qHu = 0)
- x.AllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.W4 = (false = true)
- x.AllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.K1 = (0 ∈ Multiset.map (fun (x : 𝓩 × 𝓩) => match x with | (y, z) => -q5 + y + z) (x.2.2.2.product x.2.2.2).val)
- x.AllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.W2 = (false = true)
- SuperSymmetry.SU5.Charges.AllowsTermQ5 (none, fst, fst_1, snd) q5 SuperSymmetry.SU5.PotentialTerm.bottomYukawa = (false = true)
- x.AllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.topYukawa = (false = true)
- x.AllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.K2 = (false = true)
- x.AllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.W3 = (false = true)
Instances For
Equations
- One or more equations did not get rendered due to their size.
- x.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.μ = isFalse ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ5 (fst, some qHu, fst_1, snd) q5 SuperSymmetry.SU5.PotentialTerm.β = decidable_of_iff (q5 = qHu) ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ5 (fst, none, fst_1, snd) q5 SuperSymmetry.SU5.PotentialTerm.β = isFalse ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ5 (some qHd, some qHu, fst, snd) q5 SuperSymmetry.SU5.PotentialTerm.W4 = decidable_of_iff (q5 + qHd - qHu - qHu = 0) ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ5 (some qHd, none, fst, snd) q5 SuperSymmetry.SU5.PotentialTerm.W4 = isFalse ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ5 (none, fst, fst_1, snd) q5 SuperSymmetry.SU5.PotentialTerm.W4 = isFalse ⋯
- x.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.W2 = isFalse ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ5 (none, fst, fst_1, snd) q5 SuperSymmetry.SU5.PotentialTerm.bottomYukawa = isFalse ⋯
- x.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.topYukawa = isFalse ⋯
- x.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.K2 = isFalse ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ5 (fst, none, fst_1, snd) q5 SuperSymmetry.SU5.PotentialTerm.W3 = isFalse ⋯
AllowsTermQ10 #
The proposition for which says, given a charge x
adding a charge q5
permits the
existence of a potential term T
due to the addition of that charge.
Equations
- One or more equations did not get rendered due to their size.
- x.AllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.μ = (false = true)
- x.AllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.β = (false = true)
- x.AllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.Λ = (0 ∈ Multiset.map (fun (x : 𝓩 × 𝓩) => match x with | (y, z) => y + z + q10) (x.2.2.1.product x.2.2.1).val)
- x.AllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.W4 = (false = true)
- x.AllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.W2 = (false = true)
- SuperSymmetry.SU5.Charges.AllowsTermQ10 (none, fst, fst_1, snd) q10 SuperSymmetry.SU5.PotentialTerm.bottomYukawa = (false = true)
- x.AllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.topYukawa = (false = true)
- SuperSymmetry.SU5.Charges.AllowsTermQ10 (some qHd, some qHu, fst, snd) q10 SuperSymmetry.SU5.PotentialTerm.K2 = (qHd + qHu + q10 = 0)
- x.AllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.K2 = (false = true)
- x.AllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.W3 = (false = true)
Instances For
Equations
- One or more equations did not get rendered due to their size.
- x.instDecidableAllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.μ = isFalse ⋯
- x.instDecidableAllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.β = isFalse ⋯
- x.instDecidableAllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.W4 = isFalse ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ10 (none, fst, fst_1, snd) q10 SuperSymmetry.SU5.PotentialTerm.W2 = isFalse ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ10 (none, fst, fst_1, snd) q10 SuperSymmetry.SU5.PotentialTerm.bottomYukawa = isFalse ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ10 (fst, none, fst_1, snd) q10 SuperSymmetry.SU5.PotentialTerm.topYukawa = isFalse ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ10 (some qHd, some qHu, fst, snd) q10 SuperSymmetry.SU5.PotentialTerm.K2 = decidable_of_iff (qHd + qHu + q10 = 0) ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ10 (some qHd, none, fst, snd) q10 SuperSymmetry.SU5.PotentialTerm.K2 = isFalse ⋯
- SuperSymmetry.SU5.Charges.instDecidableAllowsTermQ10 (none, fst, fst_1, snd) q10 SuperSymmetry.SU5.PotentialTerm.K2 = isFalse ⋯
- x.instDecidableAllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.W3 = isFalse ⋯