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.OfPotentialTerm

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.

@[expose] public section

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.

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.

def AllowsTerm (x : ChargeSpectrum 𝓩) (T : PotentialTerm) : Prop := 0 ∈ ofPotentialTerm x 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.

lemma allowsTerm_iff_zero_mem_ofPotentialTerm' [DecidableEq 𝓩] {x : ChargeSpectrum 𝓩} {T : PotentialTerm} : x.AllowsTerm T ↔ 0 ∈ x.ofPotentialTerm' T := mem_ofPotentialTerm_iff_mem_ofPotentialTerminstance [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (T : PotentialTerm) : Decidable (x.AllowsTerm T) := decidable_of_iff (0 ∈ x.ofPotentialTerm' T) allowsTerm_iff_zero_mem_ofPotentialTerm'.symm

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.

lemma allowsTerm_mono {T : PotentialTerm} {y x : ChargeSpectrum 𝓩} (h : y βŠ† x) (hy : y.AllowsTerm T) : x.AllowsTerm T := ofPotentialTerm_mono h T hy

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.

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.

def allowsTermForm (a b c : 𝓩) : (T : PotentialTerm) β†’ ChargeSpectrum 𝓩 | .ΞΌ => ⟨some a, some a, βˆ…, βˆ…βŸ© | .Ξ² => ⟨none, some a, {a}, βˆ…βŸ© | .Ξ› => ⟨none, none, {a, b}, {- a - b}⟩ | .W1 => ⟨none, none, {- a - b - c}, {a, b, c}⟩ | .W2 => ⟨some (- a - b - c), none, βˆ…, {a, b, c}⟩ | .W3 => ⟨none, some (- a), {b, - b - 2 β€’ a}, βˆ…βŸ© | .W4 => ⟨some (- c - 2 β€’ b), some (- b), {c}, βˆ…βŸ© | .K1 => ⟨none, none, {-a}, {b, - a - b}⟩ | .K2 => ⟨some a, some b, βˆ…, {- a - b}⟩ | .topYukawa => ⟨none, some (-a), βˆ…, {b, - a - b}⟩ | .bottomYukawa => ⟨some a, none, {b}, {- 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.

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

lemma allowsTermForm_allowsTerm {a b c : 𝓩} {T : PotentialTerm} : (allowsTermForm a b c T).AllowsTerm T := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:𝓩T:PotentialTerm⊒ (allowsTermForm a b c T).AllowsTerm T 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:𝓩T:PotentialTerm⊒ 0 ∈ List.foldl (fun a b => Multiset.map (fun x => x.1 + x.2) (a Γ—Λ’ b)) {0} (List.map (fun F => ((match T with | PotentialTerm.ΞΌ => { qHd := some a, qHu := some a, Q5 := βˆ…, Q10 := βˆ… } | PotentialTerm.Ξ² => { qHd := none, qHu := some a, Q5 := {a}, Q10 := βˆ… } | PotentialTerm.Ξ› => { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} } | PotentialTerm.W1 => { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} } | PotentialTerm.W2 => { qHd := some (-a - b - c), qHu := none, Q5 := βˆ…, Q10 := {a, b, c} } | PotentialTerm.W3 => { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β€’ a}, Q10 := βˆ… } | PotentialTerm.W4 => { qHd := some (-c - 2 β€’ b), qHu := some (-b), Q5 := {c}, Q10 := βˆ… } | PotentialTerm.K1 => { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} } | PotentialTerm.K2 => { qHd := some a, qHu := some b, Q5 := βˆ…, Q10 := {-a - b} } | PotentialTerm.topYukawa => { qHd := none, qHu := some (-a), Q5 := βˆ…, Q10 := {b, -a - b} } | PotentialTerm.bottomYukawa => { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }).ofFieldLabel F).val) T.toFieldLabel) 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 0 ∈ List.foldl (fun a b => Multiset.map (fun x => x.1 + x.2) (a Γ—Λ’ b)) {0} (List.map (fun F => ((match PotentialTerm.ΞΌ with | PotentialTerm.ΞΌ => { qHd := some a, qHu := some a, Q5 := βˆ…, Q10 := βˆ… } | PotentialTerm.Ξ² => { qHd := none, qHu := some a, Q5 := {a}, Q10 := βˆ… } | PotentialTerm.Ξ› => { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} } | PotentialTerm.W1 => { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} } | PotentialTerm.W2 => { qHd := some (-a - b - c), qHu := none, Q5 := βˆ…, Q10 := {a, b, c} } | PotentialTerm.W3 => { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β€’ a}, Q10 := βˆ… } | PotentialTerm.W4 => { qHd := some (-c - 2 β€’ b), qHu := some (-b), Q5 := {c}, Q10 := βˆ… } | PotentialTerm.K1 => { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} } | PotentialTerm.K2 => { qHd := some a, qHu := some b, Q5 := βˆ…, Q10 := {-a - b} } | PotentialTerm.topYukawa => { qHd := none, qHu := some (-a), Q5 := βˆ…, Q10 := {b, -a - b} } | PotentialTerm.bottomYukawa => { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }).ofFieldLabel F).val) PotentialTerm.ΞΌ.toFieldLabel)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 0 ∈ List.foldl (fun a b => Multiset.map (fun x => x.1 + x.2) (a Γ—Λ’ b)) {0} (List.map (fun F => ((match PotentialTerm.Ξ² with | PotentialTerm.ΞΌ => { qHd := some a, qHu := some a, Q5 := βˆ…, Q10 := βˆ… } | PotentialTerm.Ξ² => { qHd := none, qHu := some a, Q5 := {a}, Q10 := βˆ… } | PotentialTerm.Ξ› => { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} } | PotentialTerm.W1 => { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} } | PotentialTerm.W2 => { qHd := some (-a - b - c), qHu := none, Q5 := βˆ…, Q10 := {a, b, c} } | PotentialTerm.W3 => { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β€’ a}, Q10 := βˆ… } | PotentialTerm.W4 => { qHd := some (-c - 2 β€’ b), qHu := some (-b), Q5 := {c}, Q10 := βˆ… } | PotentialTerm.K1 => { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} } | PotentialTerm.K2 => { qHd := some a, qHu := some b, Q5 := βˆ…, Q10 := {-a - b} } | PotentialTerm.topYukawa => { qHd := none, qHu := some (-a), Q5 := βˆ…, Q10 := {b, -a - b} } | PotentialTerm.bottomYukawa => { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }).ofFieldLabel F).val) PotentialTerm.Ξ².toFieldLabel)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 0 ∈ List.foldl (fun a b => Multiset.map (fun x => x.1 + x.2) (a Γ—Λ’ b)) {0} (List.map (fun F => ((match PotentialTerm.Ξ› with | PotentialTerm.ΞΌ => { qHd := some a, qHu := some a, Q5 := βˆ…, Q10 := βˆ… } | PotentialTerm.Ξ² => { qHd := none, qHu := some a, Q5 := {a}, Q10 := βˆ… } | PotentialTerm.Ξ› => { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} } | PotentialTerm.W1 => { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} } | PotentialTerm.W2 => { qHd := some (-a - b - c), qHu := none, Q5 := βˆ…, Q10 := {a, b, c} } | PotentialTerm.W3 => { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β€’ a}, Q10 := βˆ… } | PotentialTerm.W4 => { qHd := some (-c - 2 β€’ b), qHu := some (-b), Q5 := {c}, Q10 := βˆ… } | PotentialTerm.K1 => { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} } | PotentialTerm.K2 => { qHd := some a, qHu := some b, Q5 := βˆ…, Q10 := {-a - b} } | PotentialTerm.topYukawa => { qHd := none, qHu := some (-a), Q5 := βˆ…, Q10 := {b, -a - b} } | PotentialTerm.bottomYukawa => { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }).ofFieldLabel F).val) PotentialTerm.Ξ›.toFieldLabel)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 0 ∈ List.foldl (fun a b => Multiset.map (fun x => x.1 + x.2) (a Γ—Λ’ b)) {0} (List.map (fun F => ((match PotentialTerm.W1 with | PotentialTerm.ΞΌ => { qHd := some a, qHu := some a, Q5 := βˆ…, Q10 := βˆ… } | PotentialTerm.Ξ² => { qHd := none, qHu := some a, Q5 := {a}, Q10 := βˆ… } | PotentialTerm.Ξ› => { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} } | PotentialTerm.W1 => { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} } | PotentialTerm.W2 => { qHd := some (-a - b - c), qHu := none, Q5 := βˆ…, Q10 := {a, b, c} } | PotentialTerm.W3 => { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β€’ a}, Q10 := βˆ… } | PotentialTerm.W4 => { qHd := some (-c - 2 β€’ b), qHu := some (-b), Q5 := {c}, Q10 := βˆ… } | PotentialTerm.K1 => { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} } | PotentialTerm.K2 => { qHd := some a, qHu := some b, Q5 := βˆ…, Q10 := {-a - b} } | PotentialTerm.topYukawa => { qHd := none, qHu := some (-a), Q5 := βˆ…, Q10 := {b, -a - b} } | PotentialTerm.bottomYukawa => { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }).ofFieldLabel F).val) PotentialTerm.W1.toFieldLabel)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 0 ∈ List.foldl (fun a b => Multiset.map (fun x => x.1 + x.2) (a Γ—Λ’ b)) {0} (List.map (fun F => ((match PotentialTerm.W2 with | PotentialTerm.ΞΌ => { qHd := some a, qHu := some a, Q5 := βˆ…, Q10 := βˆ… } | PotentialTerm.Ξ² => { qHd := none, qHu := some a, Q5 := {a}, Q10 := βˆ… } | PotentialTerm.Ξ› => { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} } | PotentialTerm.W1 => { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} } | PotentialTerm.W2 => { qHd := some (-a - b - c), qHu := none, Q5 := βˆ…, Q10 := {a, b, c} } | PotentialTerm.W3 => { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β€’ a}, Q10 := βˆ… } | PotentialTerm.W4 => { qHd := some (-c - 2 β€’ b), qHu := some (-b), Q5 := {c}, Q10 := βˆ… } | PotentialTerm.K1 => { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} } | PotentialTerm.K2 => { qHd := some a, qHu := some b, Q5 := βˆ…, Q10 := {-a - b} } | PotentialTerm.topYukawa => { qHd := none, qHu := some (-a), Q5 := βˆ…, Q10 := {b, -a - b} } | PotentialTerm.bottomYukawa => { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }).ofFieldLabel F).val) PotentialTerm.W2.toFieldLabel)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 0 ∈ List.foldl (fun a b => Multiset.map (fun x => x.1 + x.2) (a Γ—Λ’ b)) {0} (List.map (fun F => ((match PotentialTerm.W3 with | PotentialTerm.ΞΌ => { qHd := some a, qHu := some a, Q5 := βˆ…, Q10 := βˆ… } | PotentialTerm.Ξ² => { qHd := none, qHu := some a, Q5 := {a}, Q10 := βˆ… } | PotentialTerm.Ξ› => { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} } | PotentialTerm.W1 => { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} } | PotentialTerm.W2 => { qHd := some (-a - b - c), qHu := none, Q5 := βˆ…, Q10 := {a, b, c} } | PotentialTerm.W3 => { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β€’ a}, Q10 := βˆ… } | PotentialTerm.W4 => { qHd := some (-c - 2 β€’ b), qHu := some (-b), Q5 := {c}, Q10 := βˆ… } | PotentialTerm.K1 => { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} } | PotentialTerm.K2 => { qHd := some a, qHu := some b, Q5 := βˆ…, Q10 := {-a - b} } | PotentialTerm.topYukawa => { qHd := none, qHu := some (-a), Q5 := βˆ…, Q10 := {b, -a - b} } | PotentialTerm.bottomYukawa => { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }).ofFieldLabel F).val) PotentialTerm.W3.toFieldLabel)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 0 ∈ List.foldl (fun a b => Multiset.map (fun x => x.1 + x.2) (a Γ—Λ’ b)) {0} (List.map (fun F => ((match PotentialTerm.W4 with | PotentialTerm.ΞΌ => { qHd := some a, qHu := some a, Q5 := βˆ…, Q10 := βˆ… } | PotentialTerm.Ξ² => { qHd := none, qHu := some a, Q5 := {a}, Q10 := βˆ… } | PotentialTerm.Ξ› => { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} } | PotentialTerm.W1 => { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} } | PotentialTerm.W2 => { qHd := some (-a - b - c), qHu := none, Q5 := βˆ…, Q10 := {a, b, c} } | PotentialTerm.W3 => { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β€’ a}, Q10 := βˆ… } | PotentialTerm.W4 => { qHd := some (-c - 2 β€’ b), qHu := some (-b), Q5 := {c}, Q10 := βˆ… } | PotentialTerm.K1 => { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} } | PotentialTerm.K2 => { qHd := some a, qHu := some b, Q5 := βˆ…, Q10 := {-a - b} } | PotentialTerm.topYukawa => { qHd := none, qHu := some (-a), Q5 := βˆ…, Q10 := {b, -a - b} } | PotentialTerm.bottomYukawa => { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }).ofFieldLabel F).val) PotentialTerm.W4.toFieldLabel)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 0 ∈ List.foldl (fun a b => Multiset.map (fun x => x.1 + x.2) (a Γ—Λ’ b)) {0} (List.map (fun F => ((match PotentialTerm.K1 with | PotentialTerm.ΞΌ => { qHd := some a, qHu := some a, Q5 := βˆ…, Q10 := βˆ… } | PotentialTerm.Ξ² => { qHd := none, qHu := some a, Q5 := {a}, Q10 := βˆ… } | PotentialTerm.Ξ› => { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} } | PotentialTerm.W1 => { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} } | PotentialTerm.W2 => { qHd := some (-a - b - c), qHu := none, Q5 := βˆ…, Q10 := {a, b, c} } | PotentialTerm.W3 => { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β€’ a}, Q10 := βˆ… } | PotentialTerm.W4 => { qHd := some (-c - 2 β€’ b), qHu := some (-b), Q5 := {c}, Q10 := βˆ… } | PotentialTerm.K1 => { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} } | PotentialTerm.K2 => { qHd := some a, qHu := some b, Q5 := βˆ…, Q10 := {-a - b} } | PotentialTerm.topYukawa => { qHd := none, qHu := some (-a), Q5 := βˆ…, Q10 := {b, -a - b} } | PotentialTerm.bottomYukawa => { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }).ofFieldLabel F).val) PotentialTerm.K1.toFieldLabel)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 0 ∈ List.foldl (fun a b => Multiset.map (fun x => x.1 + x.2) (a Γ—Λ’ b)) {0} (List.map (fun F => ((match PotentialTerm.K2 with | PotentialTerm.ΞΌ => { qHd := some a, qHu := some a, Q5 := βˆ…, Q10 := βˆ… } | PotentialTerm.Ξ² => { qHd := none, qHu := some a, Q5 := {a}, Q10 := βˆ… } | PotentialTerm.Ξ› => { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} } | PotentialTerm.W1 => { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} } | PotentialTerm.W2 => { qHd := some (-a - b - c), qHu := none, Q5 := βˆ…, Q10 := {a, b, c} } | PotentialTerm.W3 => { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β€’ a}, Q10 := βˆ… } | PotentialTerm.W4 => { qHd := some (-c - 2 β€’ b), qHu := some (-b), Q5 := {c}, Q10 := βˆ… } | PotentialTerm.K1 => { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} } | PotentialTerm.K2 => { qHd := some a, qHu := some b, Q5 := βˆ…, Q10 := {-a - b} } | PotentialTerm.topYukawa => { qHd := none, qHu := some (-a), Q5 := βˆ…, Q10 := {b, -a - b} } | PotentialTerm.bottomYukawa => { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }).ofFieldLabel F).val) PotentialTerm.K2.toFieldLabel)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 0 ∈ List.foldl (fun a b => Multiset.map (fun x => x.1 + x.2) (a Γ—Λ’ b)) {0} (List.map (fun F => ((match PotentialTerm.topYukawa with | PotentialTerm.ΞΌ => { qHd := some a, qHu := some a, Q5 := βˆ…, Q10 := βˆ… } | PotentialTerm.Ξ² => { qHd := none, qHu := some a, Q5 := {a}, Q10 := βˆ… } | PotentialTerm.Ξ› => { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} } | PotentialTerm.W1 => { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} } | PotentialTerm.W2 => { qHd := some (-a - b - c), qHu := none, Q5 := βˆ…, Q10 := {a, b, c} } | PotentialTerm.W3 => { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β€’ a}, Q10 := βˆ… } | PotentialTerm.W4 => { qHd := some (-c - 2 β€’ b), qHu := some (-b), Q5 := {c}, Q10 := βˆ… } | PotentialTerm.K1 => { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} } | PotentialTerm.K2 => { qHd := some a, qHu := some b, Q5 := βˆ…, Q10 := {-a - b} } | PotentialTerm.topYukawa => { qHd := none, qHu := some (-a), Q5 := βˆ…, Q10 := {b, -a - b} } | PotentialTerm.bottomYukawa => { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }).ofFieldLabel F).val) PotentialTerm.topYukawa.toFieldLabel)𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 0 ∈ List.foldl (fun a b => Multiset.map (fun x => x.1 + x.2) (a Γ—Λ’ b)) {0} (List.map (fun F => ((match PotentialTerm.bottomYukawa with | PotentialTerm.ΞΌ => { qHd := some a, qHu := some a, Q5 := βˆ…, Q10 := βˆ… } | PotentialTerm.Ξ² => { qHd := none, qHu := some a, Q5 := {a}, Q10 := βˆ… } | PotentialTerm.Ξ› => { qHd := none, qHu := none, Q5 := {a, b}, Q10 := {-a - b} } | PotentialTerm.W1 => { qHd := none, qHu := none, Q5 := {-a - b - c}, Q10 := {a, b, c} } | PotentialTerm.W2 => { qHd := some (-a - b - c), qHu := none, Q5 := βˆ…, Q10 := {a, b, c} } | PotentialTerm.W3 => { qHd := none, qHu := some (-a), Q5 := {b, -b - 2 β€’ a}, Q10 := βˆ… } | PotentialTerm.W4 => { qHd := some (-c - 2 β€’ b), qHu := some (-b), Q5 := {c}, Q10 := βˆ… } | PotentialTerm.K1 => { qHd := none, qHu := none, Q5 := {-a}, Q10 := {b, -a - b} } | PotentialTerm.K2 => { qHd := some a, qHu := some b, Q5 := βˆ…, Q10 := {-a - b} } | PotentialTerm.topYukawa => { qHd := none, qHu := some (-a), Q5 := βˆ…, Q10 := {b, -a - b} } | PotentialTerm.bottomYukawa => { qHd := some a, qHu := none, Q5 := {b}, Q10 := {-a - b} }).ofFieldLabel F).val) PotentialTerm.bottomYukawa.toFieldLabel) all_goals All goals completed! πŸ™ case Ξ› 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ βˆƒ a_1 b_1, ((a_1 = a ∨ a_1 = b) ∧ (b_1 = a ∨ b_1 = b)) ∧ a_1 + b_1 + (-a - b) = 0 exact ⟨a, b, 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ ((a = a ∨ a = b) ∧ (b = a ∨ b = b)) ∧ a + b + (-a - b) = 0 All goals completed! πŸ™βŸ© case K1 | topYukawa 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ βˆƒ a_1 b_1, ((a_1 = b ∨ a_1 = -a - b) ∧ (b_1 = b ∨ b_1 = -a - b)) ∧ a_1 + b_1 + a = 0 exact ⟨b, - a - b, 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ ((b = b ∨ b = -a - b) ∧ (-a - b = b ∨ -a - b = -a - b)) ∧ b + (-a - b) + a = 0 All goals completed! πŸ™βŸ© case W3 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ βˆƒ a_1 b_1, ((a_1 = b ∨ a_1 = -b - 2 β€’ a) ∧ (b_1 = b ∨ b_1 = -b - 2 β€’ a)) ∧ a_1 + b_1 + a + a = 0 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ ((b = b ∨ b = -b - 2 β€’ a) ∧ (-b - 2 β€’ a = b ∨ -b - 2 β€’ a = -b - 2 β€’ a)) ∧ b + (-b - 2 β€’ a) + a + a = 0 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ b + (-b - 2 β€’ a) + a + a = 0 All goals completed! πŸ™ case W1 | W2 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ βˆƒ b_1 a_1 b_2, (((a_1 = a ∨ a_1 = b ∨ a_1 = c) ∧ (b_2 = a ∨ b_2 = b ∨ b_2 = c)) ∧ (b_1 = a ∨ b_1 = b ∨ b_1 = c)) ∧ a_1 + b_2 + b_1 + (-a - b - c) = 0 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ (((b = a ∨ b = b ∨ b = c) ∧ (c = a ∨ c = b ∨ c = c)) ∧ (a = a ∨ a = b ∨ a = c)) ∧ b + c + a + (-a - b - c) = 0 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ b + c + a + (-a - b - c) = 0 All goals completed! πŸ™ all_goals All goals completed! πŸ™
lemma allowsTerm_of_eq_allowsTermForm {T : PotentialTerm} (x : ChargeSpectrum 𝓩) (h : βˆƒ a b c, x = allowsTermForm a b c T) : x.AllowsTerm T := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:βˆƒ a b c, x = allowsTermForm a b c T⊒ x.AllowsTerm T 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTerma:𝓩b:𝓩c:π“©βŠ’ (allowsTermForm a b c T).AllowsTerm T All goals completed! πŸ™

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.

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.

lemma allowsTermForm_card_le_degree {a b c : 𝓩} {T : PotentialTerm} : (allowsTermForm a b c T).card ≀ T.degree := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:𝓩T:PotentialTerm⊒ (allowsTermForm a b c T).card ≀ T.degree 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ (allowsTermForm a b c PotentialTerm.ΞΌ).card ≀ PotentialTerm.ΞΌ.degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ (allowsTermForm a b c PotentialTerm.Ξ²).card ≀ PotentialTerm.Ξ².degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ (allowsTermForm a b c PotentialTerm.Ξ›).card ≀ PotentialTerm.Ξ›.degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ (allowsTermForm a b c PotentialTerm.W1).card ≀ PotentialTerm.W1.degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ (allowsTermForm a b c PotentialTerm.W2).card ≀ PotentialTerm.W2.degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ (allowsTermForm a b c PotentialTerm.W3).card ≀ PotentialTerm.W3.degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ (allowsTermForm a b c PotentialTerm.W4).card ≀ PotentialTerm.W4.degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ (allowsTermForm a b c PotentialTerm.K1).card ≀ PotentialTerm.K1.degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ (allowsTermForm a b c PotentialTerm.K2).card ≀ PotentialTerm.K2.degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ (allowsTermForm a b c PotentialTerm.topYukawa).card ≀ PotentialTerm.topYukawa.degree𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ (allowsTermForm a b c PotentialTerm.bottomYukawa).card ≀ PotentialTerm.bottomYukawa.degree all_goals All goals completed! πŸ™ case' Ξ› 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ {a, b}.card ≀ 2 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:𝓩h1:{a, b}.card ≀ 2⊒ {a, b}.card ≀ 2 All goals completed! πŸ™ case' W3 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 1 + {b, -b - 2 β€’ a}.card ≀ 4 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:𝓩h1:{b, -b - 2 β€’ a}.card ≀ 2⊒ 1 + {b, -b - 2 β€’ a}.card ≀ 4 All goals completed! πŸ™ case' K1 | topYukawa 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:π“©βŠ’ 1 + {b, -a - b}.card ≀ 3 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:𝓩h1:{b, -a - b}.card ≀ 2⊒ 1 + {b, -a - b}.card ≀ 3 All goals completed! πŸ™ all_goals 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩a:𝓩b:𝓩c:𝓩h1:{a, b, c}.card ≀ 3⊒ 1 + {a, b, c}.card ≀ 4 All goals completed! πŸ™

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.

𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩f2:𝓩f4:𝓩f2_mem:x.qHu = some (-f2)f4_mem:x.qHd = some f4f1_add_f2_eq_zero:f4 + f2 = 0⊒ f4 = -(f2 - (f4 + f2)) All goals completed! πŸ™

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.

lemma allowsTerm_iff_subset_allowsTermForm {T : PotentialTerm} {x : ChargeSpectrum 𝓩} : x.AllowsTerm T ↔ βˆƒ a b c, allowsTermForm a b c T βŠ† x := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum π“©βŠ’ x.AllowsTerm T ↔ βˆƒ a b c, allowsTermForm a b c T βŠ† x 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x.AllowsTerm T⊒ βˆƒ a b c, allowsTermForm a b c T βŠ† x 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x.AllowsTerm Ta:𝓩b:𝓩c:𝓩h1:allowsTermForm a b c T βŠ† x⊒ βˆƒ a b c, allowsTermForm a b c T βŠ† x All goals completed! πŸ™

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.

lemma subset_card_le_degree_allowsTerm_of_allowsTerm {T : PotentialTerm} {x : ChargeSpectrum 𝓩} (h : x.AllowsTerm T) : βˆƒ y ∈ x.powerset, y.card ≀ T.degree ∧ y.AllowsTerm T := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x.AllowsTerm T⊒ βˆƒ y ∈ x.powerset, y.card ≀ T.degree ∧ y.AllowsTerm T 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermx:ChargeSpectrum 𝓩h:x.AllowsTerm Ta:𝓩b:𝓩c:𝓩h1:allowsTermForm a b c T βŠ† xh2:(allowsTermForm a b c T).AllowsTerm T⊒ βˆƒ y ∈ x.powerset, y.card ≀ T.degree ∧ y.AllowsTerm T All goals completed! πŸ™

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.

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.

def AllowsTermQ5 (x : ChargeSpectrum 𝓩) (q5 : 𝓩) (T : PotentialTerm) : Prop := match T with | .ΞΌ => false | .Ξ² => match x with | ⟨_, some qHu, _, _⟩ => q5 = qHu | _ => false | .Ξ› => (0 : 𝓩) ∈ ((insert q5 x.Q5).product x.Q10).val.map (fun (q1, q2) => (q1 + q5 + q2)) | .W4 => match x with | ⟨some qHd, some qHu, _, _⟩ => q5 + qHd - qHu - qHu = 0 | _ => false | .K1 => (0 : 𝓩) ∈ (x.Q10.product x.Q10).val.map (fun (y, z) => -q5 + y + z) | .W1 => (0 : 𝓩) ∈ (x.Q10.product (x.Q10.product x.Q10)).val.map (fun (q1, q2, q3) => q5 + q1 + q2 + q3) | .W2 => false | .bottomYukawa => match x with | ⟨none, _, _, _⟩ => false | ⟨some qHd, _, _, _⟩ => (0 : 𝓩) ∈ x.Q10.val.map (fun y => y + q5 + qHd) | .topYukawa => false | .K2 => false | .W3 => match x with | ⟨_, some qHu, _, _⟩ => (0 : 𝓩) ∈ (insert q5 x.Q5).val.map (fun y => y + q5 - qHu - qHu) | _ => false

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 (x : ChargeSpectrum 𝓩) (q5 : 𝓩) (T : PotentialTerm) : Decidable (AllowsTermQ5 x q5 T) := match T with | .ΞΌ => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermh:x.AllowsTermQ5 q5 PotentialTerm.μ⊒ False All goals completed! πŸ™ | .Ξ² => match x with | ⟨_, some qHu, _, _⟩ => decidable_of_iff (q5 = qHu) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermqHd✝:Option 𝓩qHu:𝓩Q5✝:Finset 𝓩Q10✝:Finset π“©βŠ’ q5 = qHu ↔ { qHd := qHd✝, qHu := some qHu, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ5 q5 PotentialTerm.Ξ² All goals completed! πŸ™) | ⟨_, none, _, _⟩ => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermqHd✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩h:{ qHd := qHd✝, qHu := none, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ5 q5 PotentialTerm.β⊒ False All goals completed! πŸ™ | .Ξ› => decidable_of_iff ((0 : 𝓩) ∈ ((insert q5 x.Q5).product x.Q10).val.map (fun (q1, q2) => (q1 + q5 + q2))) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTerm⊒ 0 ∈ Multiset.map (fun x => match x with | (q1, q2) => q1 + q5 + q2) ((insert q5 x.Q5).product x.Q10).val ↔ x.AllowsTermQ5 q5 PotentialTerm.Ξ› All goals completed! πŸ™) | .W4 => match x with | ⟨some qHd, some qHu, _, _⟩ => decidable_of_iff (q5 + qHd - qHu - qHu = 0) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermqHd:𝓩qHu:𝓩Q5✝:Finset 𝓩Q10✝:Finset π“©βŠ’ q5 + qHd - qHu - qHu = 0 ↔ { qHd := some qHd, qHu := some qHu, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ5 q5 PotentialTerm.W4 All goals completed! πŸ™) | ⟨some qHd, none, _, _⟩ => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermqHd:𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩h:{ qHd := some qHd, qHu := none, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ5 q5 PotentialTerm.W4⊒ False All goals completed! πŸ™ | ⟨none, _, _, _⟩ => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermqHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩h:{ qHd := none, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ5 q5 PotentialTerm.W4⊒ False All goals completed! πŸ™ | .K1 => decidable_of_iff ((0 : 𝓩) ∈ (x.Q10.product x.Q10).val.map (fun (y, z) => -q5 + y + z)) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTerm⊒ 0 ∈ Multiset.map (fun x => match x with | (y, z) => -q5 + y + z) (x.Q10.product x.Q10).val ↔ x.AllowsTermQ5 q5 PotentialTerm.K1 All goals completed! πŸ™) | .W1 => decidable_of_iff ((0 : 𝓩) ∈ (x.Q10.product (x.Q10.product x.Q10)).val.map (fun (q1, q2, q3) => q5 + q1 + q2 + q3)) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTerm⊒ 0 ∈ Multiset.map (fun x => match x with | (q1, q2, q3) => q5 + q1 + q2 + q3) (x.Q10.product (x.Q10.product x.Q10)).val ↔ x.AllowsTermQ5 q5 PotentialTerm.W1 All goals completed! πŸ™) | .W2 => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermh:x.AllowsTermQ5 q5 PotentialTerm.W2⊒ False All goals completed! πŸ™ | .bottomYukawa => match x with | ⟨none, _, _, _⟩ => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermqHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩h:{ qHd := none, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ5 q5 PotentialTerm.bottomYukawa⊒ False All goals completed! πŸ™ | ⟨some qHd, _, _, Q10⟩ => decidable_of_iff ((0 : 𝓩) ∈ Q10.val.map (fun y => y + q5 + qHd)) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermqHd:𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10:Finset π“©βŠ’ 0 ∈ Multiset.map (fun y => y + q5 + qHd) Q10.val ↔ { qHd := some qHd, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10 }.AllowsTermQ5 q5 PotentialTerm.bottomYukawa All goals completed! πŸ™) | .topYukawa => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermh:x.AllowsTermQ5 q5 PotentialTerm.topYukawa⊒ False All goals completed! πŸ™ | .K2 => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermh:x.AllowsTermQ5 q5 PotentialTerm.K2⊒ False All goals completed! πŸ™ | .W3 => match x with | ⟨_, some qHu, Q5, _⟩ => decidable_of_iff ((0 : 𝓩) ∈ (insert q5 Q5).val.map (fun y => y + q5 - qHu - qHu)) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermqHd✝:Option 𝓩qHu:𝓩Q5:Finset 𝓩Q10✝:Finset π“©βŠ’ 0 ∈ Multiset.map (fun y => y + q5 - qHu - qHu) (insert q5 Q5).val ↔ { qHd := qHd✝, qHu := some qHu, Q5 := Q5, Q10 := Q10✝ }.AllowsTermQ5 q5 PotentialTerm.W3 All goals completed! πŸ™) | ⟨_, none, _, _⟩ => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q5:𝓩T:PotentialTermqHd✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩h:{ qHd := qHd✝, qHu := none, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ5 q5 PotentialTerm.W3⊒ False All goals completed! πŸ™

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.

𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd✝:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩a1:𝓩a2:𝓩hsum:qHd + a1 + a2 = 0h2:a2 ∈ Q10⊒ a2 + a1 + qHd = qHd + a1 + a2 All goals completed! πŸ™ 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd✝:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q5:𝓩qHd:𝓩a1:𝓩a2:𝓩hsum:qHd + a1 + a2 = 0h2:a2 ∈ Q10h1:a1 ∈ Q5⊒ (βˆƒ a ∈ Q10, a + q5 + qHd = 0) ∨ βˆƒ a b, (a ∈ Q5 ∧ b ∈ Q10) ∧ qHd + a + b = 0 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd✝:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q5:𝓩qHd:𝓩a1:𝓩a2:𝓩hsum:qHd + a1 + a2 = 0h2:a2 ∈ Q10h1:a1 ∈ Q5⊒ βˆƒ a b, (a ∈ Q5 ∧ b ∈ Q10) ∧ qHd + a + b = 0 All goals completed! πŸ™

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.

𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd✝:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q5:𝓩qHd:𝓩q1:𝓩h1:q1 ∈ Q10hsum:q1 + q5 + qHd = 0⊒ qHd + q5 + q1 = q1 + q5 + qHd All goals completed! πŸ™

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.

lemma allowsTerm_insertQ5_iff_allowsTermQ5 {qHd qHu : Option 𝓩} {Q5 Q10: Finset 𝓩} {q5 : 𝓩} (T : PotentialTerm) : AllowsTerm ⟨qHd, qHu, insert q5 Q5, Q10⟩ T ↔ AllowsTermQ5 ⟨qHd, qHu, Q5, Q10⟩ q5 T ∨ AllowsTerm ⟨qHd, qHu, Q5, Q10⟩ T := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩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 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q5:𝓩T:PotentialTerm⊒ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 T ∨ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm T β†’ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.AllowsTerm T 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q5:𝓩T:PotentialTermh:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 T⊒ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.AllowsTerm T𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q5:𝓩T:PotentialTermh:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm T⊒ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.AllowsTerm T 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q5:𝓩T:PotentialTermh:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ5 q5 T⊒ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.AllowsTerm T All goals completed! πŸ™ 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q5:𝓩T:PotentialTermh:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm T⊒ { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 }.AllowsTerm T exact allowsTerm_mono (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q5:𝓩T:PotentialTermh:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm T⊒ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 } βŠ† { qHd := qHd, qHu := qHu, Q5 := insert q5 Q5, Q10 := Q10 } All goals completed! πŸ™) h

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.

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.

def AllowsTermQ10 (x : ChargeSpectrum 𝓩) (q10 : 𝓩) (T : PotentialTerm) : Prop := match T with | .ΞΌ => false | .Ξ² => false | .Ξ› => (0 : 𝓩) ∈ (x.Q5.product x.Q5).val.map (fun (y, z) => y + z + q10) | .W4 => false | .K1 => (0 : 𝓩) ∈ (x.Q5.product (insert q10 x.Q10)).val.map (fun (q5, q2) => -q5 + q2+ q10) | .W1 => (0 : 𝓩) ∈ (x.Q5.product ((insert q10 x.Q10).product (insert q10 x.Q10))).val.map (fun (q5, q2, q3) => q5 + q2 + q3 + q10) | .W2 => match x with | ⟨some qHd, _, _, _⟩ => (0 : 𝓩) ∈ (((insert q10 x.Q10).product (insert q10 x.Q10))).val.map (fun (q2, q3) => qHd + q2 + q3 + q10) | _ => false | .bottomYukawa => match x with | ⟨none, _, _, _⟩ => false | ⟨some qHd, _, _, _⟩ => (0 : 𝓩) ∈ x.Q5.val.map (fun y => q10 + y + qHd) | .topYukawa => match x with | ⟨_, some qHu, _, _⟩ => (0 : 𝓩) ∈ (insert q10 x.Q10).val.map (fun y => q10 + y - qHu) | _ => false | .K2 => match x with | ⟨some qHd, some qHu, _, _⟩ => qHd + qHu + q10 = 0 | _ => false | .W3 => false

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 (x : ChargeSpectrum 𝓩) (q10 : 𝓩) (T : PotentialTerm) : Decidable (AllowsTermQ10 x q10 T) := match T with | .ΞΌ => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermh:x.AllowsTermQ10 q10 PotentialTerm.μ⊒ False All goals completed! πŸ™ | .Ξ² => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermh:x.AllowsTermQ10 q10 PotentialTerm.β⊒ False All goals completed! πŸ™ | .Ξ› => decidable_of_iff ((0 : 𝓩) ∈ (x.Q5.product x.Q5).val.map (fun (y, z) => y + z + q10)) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTerm⊒ 0 ∈ Multiset.map (fun x => match x with | (y, z) => y + z + q10) (x.Q5.product x.Q5).val ↔ x.AllowsTermQ10 q10 PotentialTerm.Ξ› All goals completed! πŸ™) | .W4 => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermh:x.AllowsTermQ10 q10 PotentialTerm.W4⊒ False All goals completed! πŸ™ | .K1 => decidable_of_iff ((0 : 𝓩) ∈ (x.Q5.product (insert q10 x.Q10)).val.map (fun (q5, q2) => -q5 + q2 + q10)) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTerm⊒ 0 ∈ Multiset.map (fun x => match x with | (q5, q2) => -q5 + q2 + q10) (x.Q5.product (insert q10 x.Q10)).val ↔ x.AllowsTermQ10 q10 PotentialTerm.K1 All goals completed! πŸ™) | .W1 => decidable_of_iff ((0 : 𝓩) ∈ (x.Q5.product ((insert q10 x.Q10).product (insert q10 x.Q10))).val.map (fun (q5, q2, q3) => q5 + q2 + q3 + q10)) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTerm⊒ 0 ∈ Multiset.map (fun x => match x with | (q5, q2, q3) => q5 + q2 + q3 + q10) (x.Q5.product ((insert q10 x.Q10).product (insert q10 x.Q10))).val ↔ x.AllowsTermQ10 q10 PotentialTerm.W1 All goals completed! πŸ™) | .W2 => match x with | ⟨some qHd, _, _, Q10⟩ => decidable_of_iff ((0 : 𝓩) ∈ (((insert q10 Q10).product (insert q10 Q10))).val.map (fun (q2, q3) => qHd + q2 + q3 + q10)) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermqHd:𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10:Finset π“©βŠ’ 0 ∈ Multiset.map (fun x => match x with | (q2, q3) => qHd + q2 + q3 + q10) ((insert q10 Q10).product (insert q10 Q10)).val ↔ { qHd := some qHd, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10 }.AllowsTermQ10 q10 PotentialTerm.W2 All goals completed! πŸ™) | ⟨none, _, _, _⟩ => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermqHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩h:{ qHd := none, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ10 q10 PotentialTerm.W2⊒ False All goals completed! πŸ™ | .bottomYukawa => match x with | ⟨none, _, _, _⟩ => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermqHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩h:{ qHd := none, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ10 q10 PotentialTerm.bottomYukawa⊒ False All goals completed! πŸ™ | ⟨some qHd, _, Q5, _⟩ => decidable_of_iff ((0 : 𝓩) ∈ Q5.val.map (fun y => q10 + y + qHd)) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermqHd:𝓩qHu✝:Option 𝓩Q5:Finset 𝓩Q10✝:Finset π“©βŠ’ 0 ∈ Multiset.map (fun y => q10 + y + qHd) Q5.val ↔ { qHd := some qHd, qHu := qHu✝, Q5 := Q5, Q10 := Q10✝ }.AllowsTermQ10 q10 PotentialTerm.bottomYukawa All goals completed! πŸ™) | .topYukawa => match x with | ⟨_, some qHu, _, Q10⟩ => decidable_of_iff ((0 : 𝓩) ∈ (insert q10 Q10).val.map (fun y => q10 + y - qHu)) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermqHd✝:Option 𝓩qHu:𝓩Q5✝:Finset 𝓩Q10:Finset π“©βŠ’ 0 ∈ Multiset.map (fun y => q10 + y - qHu) (insert q10 Q10).val ↔ { qHd := qHd✝, qHu := some qHu, Q5 := Q5✝, Q10 := Q10 }.AllowsTermQ10 q10 PotentialTerm.topYukawa All goals completed! πŸ™) | ⟨_, none, _, _⟩ => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermqHd✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩h:{ qHd := qHd✝, qHu := none, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ10 q10 PotentialTerm.topYukawa⊒ False All goals completed! πŸ™ | .K2 => match x with | ⟨some qHd, some qHu, _, _⟩ => decidable_of_iff (qHd + qHu + q10 = 0) (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermqHd:𝓩qHu:𝓩Q5✝:Finset 𝓩Q10✝:Finset π“©βŠ’ qHd + qHu + q10 = 0 ↔ { qHd := some qHd, qHu := some qHu, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ10 q10 PotentialTerm.K2 All goals completed! πŸ™) | ⟨some qHd, none, _, _⟩ => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermqHd:𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩h:{ qHd := some qHd, qHu := none, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ10 q10 PotentialTerm.K2⊒ False All goals completed! πŸ™ | ⟨none, _, _, _⟩ => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermqHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩h:{ qHd := none, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.AllowsTermQ10 q10 PotentialTerm.K2⊒ False All goals completed! πŸ™ | .W3 => isFalse fun h => 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩q10:𝓩T:PotentialTermh:x.AllowsTermQ10 q10 PotentialTerm.W3⊒ False All goals completed! πŸ™

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.

𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd✝:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩a1:𝓩a2:𝓩hsum:qHd + a1 + a2 = 0h1:a1 ∈ Q5⊒ a2 + a1 + qHd = qHd + a1 + a2 All goals completed! πŸ™ 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd✝:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q10:𝓩qHd:𝓩a1:𝓩a2:𝓩hsum:qHd + a1 + a2 = 0h1:a1 ∈ Q5h2:a2 ∈ Q10⊒ βˆƒ a b, (a ∈ Q5 ∧ b ∈ Q10) ∧ qHd + a + b = 0 All goals completed! πŸ™

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.

𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd✝:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q10:𝓩qHd:𝓩a1:𝓩h1:a1 ∈ Q5hsum:q10 + a1 + qHd = 0⊒ qHd + a1 + q10 = q10 + a1 + qHd All goals completed! πŸ™

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.

lemma allowsTerm_insertQ10_iff_allowsTermQ10 {qHd qHu : Option 𝓩} {Q5 Q10: Finset 𝓩} {q10 : 𝓩} (T : PotentialTerm) : AllowsTerm ⟨qHd, qHu, Q5, insert q10 Q10⟩ T ↔ AllowsTermQ10 ⟨qHd, qHu, Q5, Q10⟩ q10 T ∨ AllowsTerm ⟨qHd, qHu, Q5, Q10⟩ T := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩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 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q10:𝓩T:PotentialTerm⊒ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 T ∨ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm T β†’ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.AllowsTerm T 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q10:𝓩T:PotentialTermh:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 T⊒ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.AllowsTerm T𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q10:𝓩T:PotentialTermh:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm T⊒ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.AllowsTerm T 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q10:𝓩T:PotentialTermh:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTermQ10 q10 T⊒ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.AllowsTerm T All goals completed! πŸ™ 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q10:𝓩T:PotentialTermh:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm T⊒ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 }.AllowsTerm T exact allowsTerm_mono (𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩q10:𝓩T:PotentialTermh:{ qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 }.AllowsTerm T⊒ { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := Q10 } βŠ† { qHd := qHd, qHu := qHu, Q5 := Q5, Q10 := insert q10 Q10 } All goals completed! πŸ™) h