Charges allowing terms

i. Overview

To each charge spectrum x : ChargeSpectrum 𝓩 we say it allows the potential term T : PotentialTerm, if one of the charges associated with that potential term is zero.

What this means, is that there is a choice of charges from the charge spectrum x that can be assigned to the fields in the potential term T such that the total charge is zero, and therefore that the term is present in the potential. The presence of absence of certain terms is of phenomenological importance.

This concept is captured by the proposition AllowsTerm.

In addition to this, for each potential term T, we define a function allowsTermForm which takes three elements of 𝓩, a, b, and c and returns a charge spectrum which allows the term T. We will show in allowsTerm_iff_subset_allowsTermForm that any charge spectrum that allows a term T has a subset which can be expressed as allowsTermForm a b c T for some a, b, and c.

We also define the propositions AllowsTermQ5 x q5 T and AllowsTermQ10 x q10 T which correspond to the condition that adding a charge q5 to the Q5 charges of the charge spectrum x, or adding a charge q10 to the Q10 charges of the charge spectrum x, leads to a zero charge in the charges of potential term T.

ii. Key results

• AllowsTerm : The proposition that a charge spectrum allows a potential term.
• allowsTermForm : A function which for each potential term T and three charges a, b, and c returns a charge spectrum which allows the term T, and such that any charge spectrum allowing T has a subset of this form.
• AllowsTermQ5 : The proposition that adding a charge q5 to the Q5 charges of a charge spectrum x allows the potential term T due to the addition of that charge.
• AllowsTermQ10 : The proposition that adding a charge q10 to the Q10 charges of a charge spectrum x allows the potential term T due to the addition of that charge.

iii. Table of contents

• A. Charge spectrums allowing potential terms
  • A.1. Decidability of AllowsTerm
  • A.2. Monotonicity of AllowsTerm
• B. Forms of charges which allow potential terms
  • B.1. allowsTermForm allows the potential term
  • B.2. Subset relations for allowsTermForm
  • B.3. Card of allowsTermForm
  • B.4. If AllowsTerm then subset equal to allowsTermForm a b c T
  • B.5. AllowsTerm if and only if subset equal to allowsTermForm a b c T
  • B.6. Cardinality of subset allowing potential term
• C. Allowing a potential term by insertion of a Q5 charge
  • C.1. Decidability of AllowsTermQ5
  • C.2. AllowsTermQ5 or AllowsTerm from AllowsTerm with inserted of Q5 charge
  • C.3. AllowsTerm with inserted of Q5 charge from AllowsTermQ5
  • C.4. AllowsTerm with inserted of Q5 charge iff AllowsTermQ5 or AllowsTerm
• D. Allowing a potential term by insertion of a Q10 charge
  • D.1. Decidability of AllowsTermQ5
  • D.2. AllowsTermQ10 or AllowsTerm from AllowsTerm with inserted of Q10 charge
  • D.3. AllowsTerm with inserted of Q10 charge from AllowsTermQ5
  • D.4. AllowsTerm with inserted of Q10 charge iff AllowsTermQ10 or AllowsTerm

iv. References

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

A. Charge spectrums allowing potential terms

We first define the proposition AllowsTerm, which for a charge spectrum x : ChargeSpectrum 𝓩 and a potential term T : PotentialTerm, is true if the zero charge is in the set of charges associated with that potential term.

That is, if there is some choice of representations present in the theory which will allow that potential term via symmetry.

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

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)

A.1. Decidability of AllowsTerm

We define the decidability of AllowsTerm through ofPotentialTerm' rather than ofPotentialTerm due to the speed of the former compared to the latter.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_iff_zero_mem_ofPotentialTerm' {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x : ChargeSpectrum 𝓩} {T : PotentialTerm} : x.AllowsTerm T ↔ 0 ∈ x.ofPotentialTerm' T

instance SuperSymmetry.SU5.ChargeSpectrum.instDecidableAllowsTermOfDecidableEq {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (T : PotentialTerm) : Decidable (x.AllowsTerm T)

Equations

• x.instDecidableAllowsTermOfDecidableEq T = decidable_of_iff (0 ∈ x.ofPotentialTerm' T) ⋯

A.2. Monotonicity of AllowsTerm

The proposition AllowsTerm is monotone in its charge spectrum argument. That is if a charge spectrum y is a subset of a charge spectrum x, and y allows a potential term T, then x also allows that potential term T.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_mono {𝓩 : Type} [AddCommGroup 𝓩] {T : PotentialTerm} {y x : ChargeSpectrum 𝓩} (h : y ⊆ x) (hy : y.AllowsTerm T) : x.AllowsTerm T

B. Forms of charges which allow potential terms

We now define the function allowsTermForm which for each potential term T and three charges a, b, and c returns a charge spectrum which allows the term T.

These charges are in a minimal form, in the sense that any charge spectrum allowing T has a subset of this form.

def SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (a b c : 𝓩) (T : PotentialTerm) : ChargeSpectrum 𝓩

A element of Charges from three integers 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.ChargeSpectrum.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.μ = { qHd := some a, qHu := some a, Q5 := ∅, Q10 := ∅ }
• SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.β = { qHd := none, qHu := some a, Q5 := {a}, Q10 := ∅ }
• SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.Λ = { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} }
• SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.W1 = { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} }
• SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.W2 = { qHd := some (-a - b - c), qHu := none, Q5 := ∅, Q10 := {a, b, c} }
• SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.W3 = { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 • a}, Q10 := ∅ }
• SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.W4 = { qHd := some (-c - 2 • b), qHu := some (-b), Q5 := {c}, Q10 := ∅ }
• SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.K1 = { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} }
• SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.K2 = { qHd := some a, qHu := some b, Q5 := ∅, Q10 := {-a - b} }
• SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.topYukawa = { qHd := none, qHu := some (-a), Q5 := ∅, Q10 := {b, -a - b} }
• SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm a b c SuperSymmetry.SU5.PotentialTerm.bottomYukawa = { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }

B.1. allowsTermForm allows the potential term

Any charge spectrum of the form allowsTermForm a b c T allows the potential term T.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm_allowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {a b c : 𝓩} {T : PotentialTerm} : (allowsTermForm a b c T).AllowsTerm T

The charge spectrum allowsTermForm a b c T allows the potential term T.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_of_eq_allowsTermForm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} (x : ChargeSpectrum 𝓩) (h : ∃ (a : 𝓩) (b : 𝓩) (c : 𝓩), x = allowsTermForm a b c T) : x.AllowsTerm T

B.2. Subset relations for allowsTermForm

For any potential term T except for W¹ᵢⱼₖₗ 10ⁱ 10ʲ 10ᵏ 5̄Mˡ or W²ᵢⱼₖ 10ⁱ 10ʲ 10ᵏ 5̄Hd, a charge spectrum allowsTermForm a b c T is a subset of another charge spectrum allowsTermForm a' b' c' T if they are equal.

The reason this does not work for W1 an W2 is due to the presence of three charges in the 10d representation.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm_eq_of_subset {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {a b c a' b' c' : 𝓩} {T : PotentialTerm} (h : allowsTermForm a b c T ⊆ allowsTermForm a' b' c' T) (hT : T ≠ PotentialTerm.W1 ∧ T ≠ PotentialTerm.W2) : allowsTermForm a b c T = allowsTermForm a' b' c' T

B.3. Card of allowsTermForm

The cardinality of the charge spectrum allowsTermForm a b c T is always less than or equal to the degree of the potential term T.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm_card_le_degree {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {a b c : 𝓩} {T : PotentialTerm} : (allowsTermForm a b c T).card ≤ T.degree

B.4. If AllowsTerm then subset equal to allowsTermForm a b c T

We now show one of the more important properties of allowsTermForm. Namely that if a charge spectrum x allows a potential term T, then there exists charges a, b, and c such that allowsTermForm a b c T ⊆ x.

The proof of this result is rather long, relying on case-by-case analysis of each of the potential terms of interest.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm_subset_allowsTerm_of_allowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : ChargeSpectrum 𝓩} (h : x.AllowsTerm T) : ∃ (a : 𝓩) (b : 𝓩) (c : 𝓩), allowsTermForm a b c T ⊆ x ∧ (allowsTermForm a b c T).AllowsTerm T

B.5. AllowsTerm if and only if subset equal to allowsTermForm a b c T

We now lift the previous result to show that a charge spectrum x allows a potential term T if and only if there exists charges a, b, and c such that allowsTermForm a b c T ⊆ x.

Given what has already been shown, this result is now trivial.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_iff_subset_allowsTermForm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : ChargeSpectrum 𝓩} : x.AllowsTerm T ↔ ∃ (a : 𝓩) (b : 𝓩) (c : 𝓩), allowsTermForm a b c T ⊆ x

B.6. Cardinality of subset allowing potential term

We show that if a charge spectrum x allows a potential term T, then there exists a subset of x which allows T and whose cardinality is less than or equal to the degree of T.

This follows from the fact that allowsTermForm a b c T always has cardinality less than or equal to the degree of T.

theorem SuperSymmetry.SU5.ChargeSpectrum.subset_card_le_degree_allowsTerm_of_allowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : ChargeSpectrum 𝓩} (h : x.AllowsTerm T) : ∃ y ∈ x.powerset, y.card ≤ T.degree ∧ y.AllowsTerm T

C. Allowing a potential term by insertion of a Q5 charge

We now study what happens when we add a charge q5 to the Q5 charges of a charge spectrum x. We define the proposition AllowsTermQ5 x q5 T which is true if adding the charge q5 to the Q5 charges of x allows the potential term T due to the addition of that charge.

We prove a number of properties of this proposition, including its relation to AllowsTerm and its decidability.

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

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)
• { qHd := qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.β = (q5 = qHu)
• x.AllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.β = (false = true)
• { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 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.Q10.product x.Q10).val)
• x.AllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.W2 = (false = true)
• { qHd := none, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 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)

C.1. Decidability of AllowsTermQ5

We show that if the type 𝓩 has decidable equality, then the proposition AllowsTermQ5 x q5 T is decidable for any charge spectrum x, charge q5, and potential term T.

instance SuperSymmetry.SU5.ChargeSpectrum.instDecidableAllowsTermQ5 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (q5 : 𝓩) (T : PotentialTerm) : Decidable (x.AllowsTermQ5 q5 T)

Equations

• One or more equations did not get rendered due to their size.
• x.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.μ = isFalse ⋯
• { qHd := qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.β = decidable_of_iff (q5 = qHu) ⋯
• { qHd := qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.β = isFalse ⋯
• { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.W4 = decidable_of_iff (q5 + qHd - qHu - qHu = 0) ⋯
• { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.W4 = isFalse ⋯
• { qHd := none, qHu := qHu, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.W4 = isFalse ⋯
• x.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.W2 = isFalse ⋯
• { qHd := none, qHu := qHu, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.bottomYukawa = isFalse ⋯
• x.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.topYukawa = isFalse ⋯
• x.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.K2 = isFalse ⋯
• { qHd := qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ5 q5 SuperSymmetry.SU5.PotentialTerm.W3 = isFalse ⋯

C.2. AllowsTermQ5 or AllowsTerm from AllowsTerm with inserted of Q5 charge

We show that if a charge spectrum x with an inserted charge q5 allows a potential term T, then either the charge spectrum x allows that potential term T due to the addition of that charge, or the charge spectrum x already allows that potential term T.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTermQ5_or_allowsTerm_of_allowsTerm_insertQ5 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q5 : 𝓩} (T : PotentialTerm) (h : { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.AllowsTerm T) : { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 T ∨ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm T

C.3. AllowsTerm with inserted of Q5 charge from AllowsTermQ5

We show that if a charge spectrum x allows a potential term T due to the addition of a charge q5, then the charge spectrum x with that charge inserted allows that potential term T.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_insertQ5_of_allowsTermQ5 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q5 : 𝓩} (T : PotentialTerm) (h : { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 T) : { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.AllowsTerm T

C.4. AllowsTerm with inserted of Q5 charge iff AllowsTermQ5 or AllowsTerm

We show that the charge spectrum x with that charge inserted allows that potential term T if and only if either the charge spectrum x allows that potential term T due to the addition of that charge, or the charge spectrum x already allows that potential term T.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_insertQ5_iff_allowsTermQ5 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q5 : 𝓩} (T : PotentialTerm) : { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.AllowsTerm T ↔ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 T ∨ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm T

D. Allowing a potential term by insertion of a Q10 charge

We now replicate the previous section, but for the insertion of a Q10 charge, rather than a Q5 charge.

We study what happens when we add a charge q10 to the Q10 charges of a charge spectrum x. We define the proposition AllowsTermQ10 x q10 T which is true if adding the charge q10 to the Q10 charges of x allows the potential term T due to the addition of that charge.

We prove a number of properties of this proposition, including its relation to AllowsTerm and its decidability.

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

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.Q5.product x.Q5).val)
• x.AllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.W4 = (false = true)
• x.AllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.W2 = (false = true)
• { qHd := none, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.bottomYukawa = (false = true)
• x.AllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.topYukawa = (false = true)
• { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 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)

D.1. Decidability of AllowsTermQ5

We show that if the type 𝓩 has decidable equality, then the proposition AllowsTermQ10 x q10 T is decidable for any charge spectrum x, charge q10, and potential term T.

instance SuperSymmetry.SU5.ChargeSpectrum.instDecidableAllowsTermQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (q10 : 𝓩) (T : PotentialTerm) : Decidable (x.AllowsTermQ10 q10 T)

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 ⋯
• { qHd := none, qHu := qHu, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.W2 = isFalse ⋯
• { qHd := none, qHu := qHu, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.bottomYukawa = isFalse ⋯
• { qHd := qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.topYukawa = isFalse ⋯
• { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.K2 = decidable_of_iff (qHd + qHu + q10 = 0) ⋯
• { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.K2 = isFalse ⋯
• { qHd := none, qHu := qHu, Q5 := Q5, Q10 := Q10 }.instDecidableAllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.K2 = isFalse ⋯
• x.instDecidableAllowsTermQ10 q10 SuperSymmetry.SU5.PotentialTerm.W3 = isFalse ⋯

D.2. AllowsTermQ10 or AllowsTerm from AllowsTerm with inserted of Q10 charge

We show that if a charge spectrum x with an inserted charge q10 allows a potential term T, then either the charge spectrum x allows that potential term T due to the addition of that charge, or the charge spectrum x already allows that potential term T.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTermQ10_or_allowsTerm_of_allowsTerm_insertQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q10 : 𝓩} (T : PotentialTerm) (h : { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.AllowsTerm T) : { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 T ∨ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm T

D.3. AllowsTerm with inserted of Q10 charge from AllowsTermQ5

We show that if a charge spectrum x allows a potential term T due to the addition of a charge q10, then the charge spectrum x with that charge inserted allows that potential term T.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_insertQ10_of_allowsTermQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q10 : 𝓩} (T : PotentialTerm) (h : { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 T) : { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.AllowsTerm T

D.4. AllowsTerm with inserted of Q10 charge iff AllowsTermQ10 or AllowsTerm

We show that the charge spectrum x with that charge inserted allows that potential term T if and only if either the charge spectrum x allows that potential term T due to the addition of that charge, or the charge spectrum x already allows that potential term T.

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTerm_insertQ10_iff_allowsTermQ10 {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {qHd qHu : Option 𝓩} {Q5 Q10 : Finset 𝓩} {q10 : 𝓩} (T : PotentialTerm) : { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.AllowsTerm T ↔ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 T ∨ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm T