Charge Spectrum

i. Overview

In this module we define the charge spectrum of a SU(5) SUSY GUT theory with additional charges (usually U(1)) valued in 𝓩 satisfying the condition of:

• The optional existence of a Hd particle in the bar 5 representation.
• The optional existence of a Hu particle in the 5 representation.
• The optional existence of matter in the bar 5 representation.
• The optional existence of matter in the 10 representation.

The charge spectrum contains the information of the unique charges of each type of particle present in theory. Importantly, the charge spectrum does not contain information about the multiplicity of those charges.

With just the charge spectrum of the theory it is possible to put a number of constraints on the theory, most notably phenomenological constraints.

By keeping the presence of Hd and Hu optional, we can define a number of useful properties of the charge spectrum, which can help in searching for viable theories.

ii. Key results

• ChargeSpectrum 𝓩 : The type of charge spectra with charges of type 𝓩, which is usually ℤ.

iii. Table of contents

• A. The definition of the charge spectrum
  • A.1. Extensionality properties
  • A.2. Relation to products
  • A.3. Rendering
• B. The subset relation
• C. The empty charge spectrum
• D. The cardinality of a charge spectrum
• E. The power set of a charge spectrum
• F. Finite sets of charge spectra with values

iv. References

There are no known references for charge spectra in the literature. They were created specifically for the purpose of PhysLean.

A. The definition of the charge spectrum

structure SuperSymmetry.SU5.ChargeSpectrum (𝓩 : Type := ℤ) : Type

The type such that an element corresponds to the collection of charges associated with the matter content of the theory. The order of charges is implicitly taken to be qHd, qHu, Q5, Q10.

The Q5 and Q10 charges are represented by Finset rather than Multiset, so multiplicity is not included.

This is defined for a general type 𝓩, which could be e.g.

• ℤ in the case of U(1),
• ℤ × ℤ in the case of U(1) × U(1),
• Fin 2 in the case of ℤ₂ etc.

• qHd : Option 𝓩

  The charge of the Hd particle.

• qHu : Option 𝓩

  The negative of the charge of the Hu particle. That is to say, the charge of the Hu when considered in the 5-bar representation.

• Q5 : Finset 𝓩

  The finite set of charges of the matter fields in the Q5 representation.

• Q10 : Finset 𝓩

  The finite set of charges of the matter fields in the Q10 representation.

A.1. Extensionality properties

We prove extensionality properties for ChargeSpectrum 𝓩, that is conditions of when two elements of ChargeSpectrum 𝓩 are equal. We also show that when 𝓩 has decidable equality, so does ChargeSpectrum 𝓩.

theorem SuperSymmetry.SU5.ChargeSpectrum.eq_of_parts {𝓩 : Type} {x y : ChargeSpectrum 𝓩} (h1 : x.qHd = y.qHd) (h2 : x.qHu = y.qHu) (h3 : x.Q5 = y.Q5) (h4 : x.Q10 = y.Q10) : x = y

theorem SuperSymmetry.SU5.ChargeSpectrum.eq_iff {𝓩 : Type} {x y : ChargeSpectrum 𝓩} : x = y ↔ x.qHd = y.qHd ∧ x.qHu = y.qHu ∧ x.Q5 = y.Q5 ∧ x.Q10 = y.Q10

instance SuperSymmetry.SU5.ChargeSpectrum.instDecidableEq {𝓩 : Type} [DecidableEq 𝓩] : DecidableEq (ChargeSpectrum 𝓩)

Equations

• x✝¹.instDecidableEq x✝ = decidable_of_iff (x✝¹.qHd = x✝.qHd ∧ x✝¹.qHu = x✝.qHu ∧ x✝¹.Q5 = x✝.Q5 ∧ x✝¹.Q10 = x✝.Q10) ⋯

A.2. Relation to products

We show that ChargeSpectrum 𝓩 is equivalent to the product Option 𝓩 × Option 𝓩 × Finset 𝓩 × Fin 𝓩.

In an old implementation this was definitionally true, it is not so now.

def SuperSymmetry.SU5.ChargeSpectrum.toProd {𝓩 : Type} : ChargeSpectrum 𝓩 ≃ Option 𝓩 × Option 𝓩 × Finset 𝓩 × Finset 𝓩

The explicit casting of a term of type Charges 𝓩 to a term of Option 𝓩 × Option 𝓩 × Finset 𝓩 × Finset 𝓩.

Equations

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

A.3. Rendering

unsafe instance SuperSymmetry.SU5.ChargeSpectrum.instRepr {𝓩 : Type} [Repr 𝓩] : Repr (ChargeSpectrum 𝓩)

Equations

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

B. The subset relation

We define a HasSubset and HasSSubset instance on ChargeSpectrum 𝓩.

instance SuperSymmetry.SU5.ChargeSpectrum.hasSubset {𝓩 : Type} : HasSubset (ChargeSpectrum 𝓩)

Equations

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

instance SuperSymmetry.SU5.ChargeSpectrum.hasSSubset {𝓩 : Type} : HasSSubset (ChargeSpectrum 𝓩)

Equations

• SuperSymmetry.SU5.ChargeSpectrum.hasSSubset = { SSubset := fun (x y : SuperSymmetry.SU5.ChargeSpectrum 𝓩) => x ⊆ y ∧ x ≠ y }

instance SuperSymmetry.SU5.ChargeSpectrum.subsetDecidable {𝓩 : Type} [DecidableEq 𝓩] (x y : ChargeSpectrum 𝓩) : Decidable (x ⊆ y)

Equations

• x.subsetDecidable y = instDecidableAnd

theorem SuperSymmetry.SU5.ChargeSpectrum.subset_def {𝓩 : Type} {x y : ChargeSpectrum 𝓩} : x ⊆ y ↔ x.qHd.toFinset ⊆ y.qHd.toFinset ∧ x.qHu.toFinset ⊆ y.qHu.toFinset ∧ x.Q5 ⊆ y.Q5 ∧ x.Q10 ⊆ y.Q10

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.subset_refl {𝓩 : Type} (x : ChargeSpectrum 𝓩) : x ⊆ x

theorem Option.toFinset_inj {𝓩 : Type} {x y : Option 𝓩} : x = y ↔ x.toFinset = y.toFinset

theorem SuperSymmetry.SU5.ChargeSpectrum.subset_trans {𝓩 : Type} {x y z : ChargeSpectrum 𝓩} (hxy : x ⊆ y) (hyz : y ⊆ z) : x ⊆ z

theorem SuperSymmetry.SU5.ChargeSpectrum.subset_antisymm {𝓩 : Type} {x y : ChargeSpectrum 𝓩} (hxy : x ⊆ y) (hyx : y ⊆ x) : x = y

C. The empty charge spectrum

instance SuperSymmetry.SU5.ChargeSpectrum.emptyInst {𝓩 : Type} : EmptyCollection (ChargeSpectrum 𝓩)

Equations

• SuperSymmetry.SU5.ChargeSpectrum.emptyInst = { emptyCollection := { qHd := none, qHu := none, Q5 := ∅, Q10 := ∅ } }

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.empty_subset {𝓩 : Type} (x : ChargeSpectrum 𝓩) : ∅ ⊆ x

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.subset_of_empty_iff_empty {𝓩 : Type} {x : ChargeSpectrum 𝓩} : x ⊆ ∅ ↔ x = ∅

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.empty_qHd {𝓩 : Type} : ∅.qHd = none

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.empty_qHu {𝓩 : Type} : ∅.qHu = none

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.empty_Q5 {𝓩 : Type} : ∅.Q5 = ∅

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.empty_Q10 {𝓩 : Type} : ∅.Q10 = ∅

D. The cardinality of a charge spectrum

def SuperSymmetry.SU5.ChargeSpectrum.card {𝓩 : Type} (x : ChargeSpectrum 𝓩) : ℕ

The cardinality of a Charges is defined to be the sum of the cardinalities of each of the underlying finite sets of charges, with Option ℤ turned to finsets.

Equations

• x.card = x.qHu.toFinset.card + x.qHd.toFinset.card + x.Q5.card + x.Q10.card

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.card_empty {𝓩 : Type} : ∅.card = 0

theorem SuperSymmetry.SU5.ChargeSpectrum.card_mono {𝓩 : Type} {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) : x.card ≤ y.card

theorem SuperSymmetry.SU5.ChargeSpectrum.eq_of_subset_card {𝓩 : Type} {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) (hcard : x.card = y.card) : x = y

E. The power set of a charge spectrum

def Option.powerset {𝓩 : Type} [DecidableEq 𝓩] (x : Option 𝓩) : Finset (Option 𝓩)

The powerset of x : Option 𝓩 defined as {none} if x is none and {none, some y} is x is some y.

Equations

• none.powerset = {none}
• (some x_2).powerset = {none, some x_2}

@[simp]

theorem Option.mem_powerset_iff {𝓩 : Type} [DecidableEq 𝓩] {x : Option 𝓩} (y : Option 𝓩) : y ∈ x.powerset ↔ y.toFinset ⊆ x.toFinset

def SuperSymmetry.SU5.ChargeSpectrum.powerset {𝓩 : Type} [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) : Finset (ChargeSpectrum 𝓩)

The powerset of a charge . Given a charge x : Charges it's powerset is the finite set of all Charges which are subsets of x.

Equations

• x.powerset = Finset.map SuperSymmetry.SU5.ChargeSpectrum.toProd.symm.toEmbedding (x.qHd.powerset.product (x.qHu.powerset.product (x.Q5.powerset.product x.Q10.powerset)))

theorem SuperSymmetry.SU5.ChargeSpectrum.mem_powerset_iff {𝓩 : Type} [DecidableEq 𝓩] {x y : ChargeSpectrum 𝓩} : x ∈ y.powerset ↔ x.qHd ∈ y.qHd.powerset ∧ x.qHu ∈ y.qHu.powerset ∧ x.Q5 ∈ y.Q5.powerset ∧ x.Q10 ∈ y.Q10.powerset

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.mem_powerset_iff_subset {𝓩 : Type} [DecidableEq 𝓩] {x y : ChargeSpectrum 𝓩} : x ∈ y.powerset ↔ x ⊆ y

theorem SuperSymmetry.SU5.ChargeSpectrum.self_mem_powerset {𝓩 : Type} [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) : x ∈ x.powerset

theorem SuperSymmetry.SU5.ChargeSpectrum.empty_mem_powerset {𝓩 : Type} [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) : ∅ ∈ x.powerset

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.powerset_of_empty {𝓩 : Type} [DecidableEq 𝓩] : ∅.powerset = {∅}

theorem SuperSymmetry.SU5.ChargeSpectrum.powerset_mono {𝓩 : Type} [DecidableEq 𝓩] {x y : ChargeSpectrum 𝓩} : x.powerset ⊆ y.powerset ↔ x ⊆ y

theorem SuperSymmetry.SU5.ChargeSpectrum.min_exists_inductive {𝓩 : Type} [DecidableEq 𝓩] (S : Finset (ChargeSpectrum 𝓩)) (hS : S ≠ ∅) (n : ℕ) (hn : S.card = n) : ∃ y ∈ S, y.powerset ∩ S = {y}

theorem SuperSymmetry.SU5.ChargeSpectrum.min_exists {𝓩 : Type} [DecidableEq 𝓩] (S : Finset (ChargeSpectrum 𝓩)) (hS : S ≠ ∅) : ∃ y ∈ S, y.powerset ∩ S = {y}

F. Finite sets of charge spectra with values

We define the finite set of ChargeSpectrum with 5-bar and 10d representation charges in a given finite set.

def SuperSymmetry.SU5.ChargeSpectrum.ofFinset {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) : Finset (ChargeSpectrum 𝓩)

Given S5 S10 : Finset 𝓩 the finite set of charges associated with for which the 5-bar representation charges sit in S5 and the 10d representation charges sit in S10.

Equations

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

theorem SuperSymmetry.SU5.ChargeSpectrum.mem_ofFinset_iff {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x : ChargeSpectrum 𝓩} : x ∈ ofFinset S5 S10 ↔ x.qHd.toFinset ⊆ S5 ∧ x.qHu.toFinset ⊆ S5 ∧ x.Q5 ⊆ S5 ∧ x.Q10 ⊆ S10

theorem SuperSymmetry.SU5.ChargeSpectrum.mem_ofFinset_antitone {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) (hy : y ∈ ofFinset S5 S10) : x ∈ ofFinset S5 S10

theorem SuperSymmetry.SU5.ChargeSpectrum.ofFinset_subset_of_subset {𝓩 : Type} [DecidableEq 𝓩] {S5 S5' S10 S10' : Finset 𝓩} (h5 : S5 ⊆ S5') (h10 : S10 ⊆ S10') : ofFinset S5 S10 ⊆ ofFinset S5' S10'

theorem SuperSymmetry.SU5.ChargeSpectrum.ofFinset_univ {𝓩 : Type} [DecidableEq 𝓩] [Fintype 𝓩] (x : ChargeSpectrum 𝓩) : x ∈ ofFinset Finset.univ Finset.univ