Completions of charges

i. Overview

Recall that a charge spectrum has optional Hu and Hd charges, and can have an empty set of 5-bar or 10 charges.

We say a charge spectrum is complete if it has all types of fields present, i.e. the Hd and Hu charges are present, and the sets of 5-bar and 10 charges are non-empty.

Given a non-complete charge spectrum x we can find all the completions of x, which charges in given subsets. That is, all charge spectra y which are a super set of x, are complete, and have their charges in the given subsets.

ii. Key results

• IsComplete : A predicate saying a charge spectrum is complete.
• completions : Given a charge spectrum x and finite sets of charges S5 and S10, the multiset of completions of x with charges in S5 and S10.
• completionsTopYukawa : A fast version of completions for an x which is in minimallyAllowsTermsOfFinset S5 S10 .topYukawa, or in other words has a qHu charge, a non-empty set of 10 charges, but does not have a qHd charge or any 5-bar charges.

iii. Table of contents

• A. The IsComplete predicate
  • A.1. The empty spectrum is not complete
  • A.2. The predicate IsCompelete is monotonic
• B. Multiset of completions
  • B.1. A membership condition
  • B.2. No duplicate condition
  • B.3. Completions of a complete charge spectrum
  • B.4. Membership of own completions
  • B.5. Completeness of members of completions
  • B.6. Subset of members of completions
• C. Completions for top Yukawa
  • C.1. No duplicates in completionsTopYukawa
  • C.2. Equivalence of completions and completionsTopYukawa

iv. References

There are no known references for the material in this module.

A. The IsComplete predicate

We say a charge spectrum is complete if it has all types of fields present, i.e. the Hd and Hu charges are present, and the sets of 5-bar and 10 charges are non-empty.

def SuperSymmetry.SU5.ChargeSpectrum.IsComplete {𝓩 : Type} (x : ChargeSpectrum 𝓩) : Prop

A charge spectrum is complete if it has all types of fields.

Equations

• x.IsComplete = (x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ x.Q5 ≠ ∅ ∧ x.Q10 ≠ ∅)

instance SuperSymmetry.SU5.ChargeSpectrum.instDecidableIsCompleteOfDecidableEq {𝓩 : Type} [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) : Decidable x.IsComplete

Equations

• x.instDecidableIsCompleteOfDecidableEq = inferInstanceAs (Decidable (x.qHd.isSome = true ∧ x.qHu.isSome = true ∧ x.Q5 ≠ ∅ ∧ x.Q10 ≠ ∅))

A.1. The empty spectrum is not complete

The empty charge spectrum is not complete, since it has no charges present.

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.not_isComplete_empty {𝓩 : Type} : ¬∅.IsComplete

A.2. The predicate IsCompelete is monotonic

The predicate IsComplete is monotonic with respect to the subset relation. That is, if x is a subset of y and x is complete, then y is also complete.

theorem SuperSymmetry.SU5.ChargeSpectrum.isComplete_mono {𝓩 : Type} {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) (hx : x.IsComplete) : y.IsComplete

B. Multiset of completions

The completions of a charge spectrum x with charges in given finite sets S5 and S10 are all the charge spectra y which are a super set of x, are complete, and have their charges in S5 and S10.

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

Given a collection of charges x in ofFinset S5 S10, the minimal charges y in ofFinset S5 S10 which are a super sets of x and are complete.

Equations

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

B.1. A membership condition

A simple relation for membership of a charge spectrum in the completions of another.

theorem SuperSymmetry.SU5.ChargeSpectrum.mem_completions_iff {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x y : ChargeSpectrum 𝓩} : y ∈ completions S5 S10 x ↔ (y.qHd ∈ if x.qHd.isSome = true then {x.qHd} else Multiset.map (fun (y : 𝓩) => some y) S5.val) ∧ (y.qHu ∈ if x.qHu.isSome = true then {x.qHu} else Multiset.map (fun (y : 𝓩) => some y) S5.val) ∧ (y.Q5 ∈ if x.Q5 ≠ ∅ then {x.Q5} else Multiset.map (fun (y : 𝓩) => {y}) S5.val) ∧ y.Q10 ∈ if x.Q10 ≠ ∅ then {x.Q10} else Multiset.map (fun (y : 𝓩) => {y}) S10.val

B.2. No duplicate condition

theorem SuperSymmetry.SU5.ChargeSpectrum.completions_nodup {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x : ChargeSpectrum 𝓩) : (completions S5 S10 x).Nodup

For speed we define completions to be a multiset, but in fact it has no duplicates, so it could be defined as a finite set.

B.3. Completions of a complete charge spectrum

theorem SuperSymmetry.SU5.ChargeSpectrum.completions_eq_singleton_of_complete {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} (x : ChargeSpectrum 𝓩) (hcomplete : x.IsComplete) : completions S5 S10 x = {x}

The completions of a complete charge spectrum is just the singleton containing itself.

B.4. Membership of own completions

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.self_mem_completions_iff_isComplete {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} (x : ChargeSpectrum 𝓩) : x ∈ completions S5 S10 x ↔ x.IsComplete

If a charge spectrum x is a member of its own completion then it is complete, and vice versa.

B.5. Completeness of members of completions

We now show that any member of the completions of a charge spectrum is complete.

theorem SuperSymmetry.SU5.ChargeSpectrum.mem_completions_isComplete {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x y : ChargeSpectrum 𝓩} (hx : y ∈ completions S5 S10 x) : y.IsComplete

A charge spectrum which is a member of the completions of another charge spectrum is complete.

B.6. Subset of members of completions

We show that any member of the completions of a charge spectrum is a super set of that charge spectrum.

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

If y is in the completions of x then x ⊆ y.

theorem SuperSymmetry.SU5.ChargeSpectrum.exist_completions_subset_of_complete {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x y : ChargeSpectrum 𝓩) (hsubset : x ⊆ y) (hy : y ∈ ofFinset S5 S10) (hycomplete : y.IsComplete) : ∃ z ∈ completions S5 S10 x, z ⊆ y

C. Completions for top Yukawa

We give a fast version of completions in the case when x has a qHu charge, and a non-empty set of 10 charges, but does not have a qHd charge or any 5-bar charges. Here we only need to specify the allowed 5-bar charges, not the allowed 10 charges.

This is the case for charges which minimally allow the top Yukawa coupling.

These definitions are primarily for speed, as this is the most common case we will look at.

def SuperSymmetry.SU5.ChargeSpectrum.completionsTopYukawa {𝓩 : Type} (S5 : Finset 𝓩) (x : ChargeSpectrum 𝓩) : Multiset (ChargeSpectrum 𝓩)

A fast version of completions for an x which is in minimallyAllowsTermsOfFinset S5 S10 .topYukawa.

Equations

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

C.1. No duplicates in completionsTopYukawa

Like for completions, we define completionsTopYukawa as a multiset for speed, however, we can show it has no duplicates.

theorem SuperSymmetry.SU5.ChargeSpectrum.completionsTopYukawa_nodup {𝓩 : Type} {S5 : Finset 𝓩} (x : ChargeSpectrum 𝓩) : (completionsTopYukawa S5 x).Nodup

The multiset completionsTopYukawa S5 x has no duplicates.

C.2. Equivalence of completions and completionsTopYukawa

For charges x which are in minimallyAllowsTermsOfFinset S5 S10 .topYukawa, we show that completions S5 S10 x and completionsTopYukawa S5 x are equal multisets.

theorem SuperSymmetry.SU5.ChargeSpectrum.completions_eq_completionsTopYukawa_of_mem_minimallyAllowsTermsOfFinset {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩] {S5 S10 : Finset 𝓩} (x : ChargeSpectrum 𝓩) (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 PotentialTerm.topYukawa) : completions S5 S10 x = completionsTopYukawa S5 x

The multisets completions S5 S10 x and completionsTopYukawa S5 x are equivalent if x minimally allows the top Yukawa.