Charges associated with a potential term

i. Overview

In this module we give the multiset of charges associated with a given type of potential term, given a charge spectrum.

We will define two versions of this, one based on the underlying fields on the potentials, and the charges that they carry, and one more explicit version which is faster to compute with. The former is ofPotentialTerm, and the latter is ofPotentialTerm'.

We will show that these two multisets have the same elements.

ii. Key results

• ofPotentialTerm : The multiset of charges associated with a potential term, defined in terms of the fields making up that potential term, given a charge spectrum.
• ofPotentialTerm' : The multiset of charges associated with a potential term, defined explicitly, given a charge spectrum.

iii. Table of contents

• A. Charges of a potential term from field labels
  • A.1. Monotonicity of ofPotentialTerm
  • A.2. Charges of potential terms for the empty charge spectrum
• B. Explicit construction of charges of a potential term
  • B.1. Explicit multisets for ofPotentialTerm'
  • B.2. ofPotentialTerm' on the empty charge spectrum
• C. Relation between two constructions of charges of potential terms
  • C.1. Showing that ofPotentialTerm is a subset of ofPotentialTerm'
  • C.2. Showing that ofPotentialTerm' is a subset of ofPotentialTerm
  • C.3. Equivalence of elements of ofPotentialTerm and ofPotentialTerm'
  • C.4. Induced monoticity of ofPotentialTerm'

iv. References

There are no known references for this material.

A. Charges of a potential term from field labels

We first define ofPotentialTerm, and prover properites of it. This is slow to compute in practice.

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

Given a charges x : Charges associated to the representations, and a potential term T, the charges associated with instances of that potential term.

Equations

• One or more equations did not get rendered due to their size.

A.1. Monotonicity of ofPotentialTerm

We show that ofPotentialTerm is monotone in its charge spectrum argument. That is if x ⊆ y then ofPotentialTerm x T ⊆ ofPotentialTerm y T.

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

A.2. Charges of potential terms for the empty charge spectrum

For the empty charge spectrum, the charges associated with any potential term is empty.

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm_empty {𝓩 : Type} [AddCommGroup 𝓩] (T : PotentialTerm) : ∅.ofPotentialTerm T = ∅

B. Explicit construction of charges of a potential term

We now turn to a more explicit construction of the charges associated with a potential term. This is faster to compute with, but less obviously connected to the underlying fields.

def SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm' {𝓩 : Type} [AddCommGroup 𝓩] (y : ChargeSpectrum 𝓩) (T : PotentialTerm) : Multiset 𝓩

Given a charges x : ChargeSpectrum associated to the representations, and a potential term T, the charges associated with instances of that potential term.

This is a more explicit form of PotentialTerm, which has the benifit that it is quick with decide, but it is not defined based on more fundamental concepts, like ofPotentialTerm is.

Equations

• One or more equations did not get rendered due to their size.
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.μ = match y.qHd, y.qHu with | none, x => ∅ | x, none => ∅ | some qHd, some qHu => {qHd - qHu}
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.β = match y.qHu with | none => ∅ | some qHu => Multiset.map (fun (x : 𝓩) => -qHu + x) y.Q5.val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.Λ = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => x.1 + x.2.1 + x.2.2) (y.Q5.product (y.Q5.product y.Q10)).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.W1 = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩 × 𝓩) => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) (y.Q5.product (y.Q10.product (y.Q10.product y.Q10))).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.W3 = match y.qHu with | none => ∅ | some qHu => Multiset.map (fun (x : 𝓩 × 𝓩) => -qHu - qHu + x.1 + x.2) (y.Q5.product y.Q5).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.K1 = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => -x.1 + x.2.1 + x.2.2) (y.Q5.product (y.Q10.product y.Q10)).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.K2 = match y.qHd, y.qHu with | none, x => ∅ | x, none => ∅ | some qHd, some qHu => Multiset.map (fun (x : 𝓩) => qHd + qHu + x) y.Q10.val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.topYukawa = match y.qHu with | none => ∅ | some qHu => Multiset.map (fun (x : 𝓩 × 𝓩) => -qHu + x.1 + x.2) (y.Q10.product y.Q10).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.bottomYukawa = match y.qHd with | none => ∅ | some qHd => Multiset.map (fun (x : 𝓩 × 𝓩) => qHd + x.1 + x.2) (y.Q5.product y.Q10).val

B.1. Explicit multisets for ofPotentialTerm'

For each potential term, we give an explicit form of the multiset ofPotentialTerm'.

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm'_μ_finset {𝓩 : Type} [AddCommGroup 𝓩] {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' PotentialTerm.μ = Multiset.map (fun (x : 𝓩 × 𝓩) => x.1 - x.2) (x.qHd.toFinset.product x.qHu.toFinset).val

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm'_β_finset {𝓩 : Type} [AddCommGroup 𝓩] {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' PotentialTerm.β = Multiset.map (fun (x : 𝓩 × 𝓩) => -x.1 + x.2) (x.qHu.toFinset.product x.Q5).val

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm'_W2_finset {𝓩 : Type} [AddCommGroup 𝓩] {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' PotentialTerm.W2 = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩 × 𝓩) => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) (x.qHd.toFinset.product (x.Q10.product (x.Q10.product x.Q10))).val

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm'_W3_finset {𝓩 : Type} [AddCommGroup 𝓩] {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' PotentialTerm.W3 = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => -x.1 - x.1 + x.2.1 + x.2.2) (x.qHu.toFinset.product (x.Q5.product x.Q5)).val

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm'_W4_finset {𝓩 : Type} [AddCommGroup 𝓩] {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' PotentialTerm.W4 = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => x.1 - x.2.1 - x.2.1 + x.2.2) (x.qHd.toFinset.product (x.qHu.toFinset.product x.Q5)).val

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm'_K2_finset {𝓩 : Type} [AddCommGroup 𝓩] {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' PotentialTerm.K2 = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => x.1 + x.2.1 + x.2.2) (x.qHd.toFinset.product (x.qHu.toFinset.product x.Q10)).val

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm'_topYukawa_finset {𝓩 : Type} [AddCommGroup 𝓩] {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' PotentialTerm.topYukawa = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => -x.1 + x.2.1 + x.2.2) (x.qHu.toFinset.product (x.Q10.product x.Q10)).val

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm'_bottomYukawa_finset {𝓩 : Type} [AddCommGroup 𝓩] {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' PotentialTerm.bottomYukawa = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => x.1 + x.2.1 + x.2.2) (x.qHd.toFinset.product (x.Q5.product x.Q10)).val

B.2. ofPotentialTerm' on the empty charge spectrum

We show that for the empty charge spectrum, the charges associated with any potential term is empty, as defined through ofPotentialTerm'.

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm'_empty {𝓩 : Type} [AddCommGroup 𝓩] (T : PotentialTerm) : ∅.ofPotentialTerm' T = ∅

C. Relation between two constructions of charges of potential terms

We now give the relation between ofPotentialTerm and ofPotentialTerm'. We show that they have the same elements, by showing that they are subsets of each other.

The prove of some of these results are rather long since they involve explicit case analysis for each potential term, due to the nature of the definition of ofPotentialTerm'.

C.1. Showing that ofPotentialTerm is a subset of ofPotentialTerm'

We first show that ofPotentialTerm is a subset of ofPotentialTerm'.

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm_subset_ofPotentialTerm' {𝓩 : Type} [AddCommGroup 𝓩] {x : ChargeSpectrum 𝓩} (T : PotentialTerm) : x.ofPotentialTerm T ⊆ x.ofPotentialTerm' T

C.2. Showing that ofPotentialTerm' is a subset of ofPotentialTerm

We now show the other direction of the subset relation, that ofPotentialTerm' is a subset of ofPotentialTerm.

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm'_subset_ofPotentialTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x : ChargeSpectrum 𝓩} (T : PotentialTerm) : x.ofPotentialTerm' T ⊆ x.ofPotentialTerm T

C.3. Equivalence of elements of ofPotentialTerm and ofPotentialTerm'

We now show that a charge is in ofPotentialTerm if and only if it is in ofPotentialTerm'. I.e. their underlying finite sets are equal. We do not say anything about the multiplicity of elements within the multisets, which is not important for us.

theorem SuperSymmetry.SU5.ChargeSpectrum.mem_ofPotentialTerm_iff_mem_ofPotentialTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {n : 𝓩} {y : ChargeSpectrum 𝓩} : n ∈ y.ofPotentialTerm T ↔ n ∈ y.ofPotentialTerm' T

C.4. Induced monoticity of ofPotentialTerm'

Due to the equivalence of elements of ofPotentialTerm and ofPotentialTerm', we can now also show that ofPotentialTerm' is monotone in its charge spectrum argument.

theorem SuperSymmetry.SU5.ChargeSpectrum.ofPotentialTerm'_mono {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) (T : PotentialTerm) : x.ofPotentialTerm' T ⊆ y.ofPotentialTerm' T