Quanta of 5-d representations

i. Overview

The 5-bar representations of the SU(5)×U(1) carry the quantum numbers of their U(1) charges and their fluxes.

In this module we define the data structure for these quanta and properties thereof.

ii. Key results

• FiveQuanta is the type of quanta of 5-bar representations.
• FiveQuanta.toFluxesFive is the underlying FluxesFive of a FiveQuanta.
• FiveQuanta.toCharges is the underlying Multiset charges of a FiveQuanta.
• FiveQuanta.reduce is the reduction of a FiveQuanta which adds together all the fluxes corresponding to the same charge (i.e. representation).
• FiveQuanta.liftCharges given a charge c the FiveQuanta which have charge c and no exotics or zero fluxes.
• FiveQuanta.anomalyCoefficient is the anomaly coefficient associated with a FiveQuanta.

iii. Table of contents

• A. The definition of FiveQuanta
  • A.1. The map to underlying fluxes
  • A.2. The map to underlying charges
  • A.3. The map from charges to fluxes
• B. The reduction of a FiveQuanta
  • B.1. The reduced FiveQuanta has no duplicate elements
  • B.2. The underlying charges of the reduced FiveQuanta are the deduped charges
  • B.3. Membership condition on the reduced FiveQuanta
  • B.4. Filter of the reduced FiveQuanta by a charge
  • B.5. The reduction is idempotent
  • B.6. Preservation of certain sums under reduction
  • B.7. Reduction does nothing if no duplicate charges
  • B.8. The charge map is preserved by reduction
  • B.9. A fluxes in the reduced FiveQuanta is a sum of fluxes in the original FiveQuanta
  • B.10. No exotics condition on the reduced FiveQuanta
    • B.10.1. Number of chiral L
    • B.10.2. Number of anti-chiral L
    • B.10.3. Number of chiral D
    • B.10.4. Number of anti-chiral D
    • B.10.5. The NoExotics condition on the reduced FiveQuanta
  • B.11. Reduce member of FluxesFive.elemsNoExotics
• C. Decomposition of a FiveQuanta into basic fluxes
  • C.1. Decomposition of fluxes
  • C.2. Decomposition of a FiveQuanta (with no exotics)
    • C.2.1. Decomposition distributes over addition
    • C.2.2. Decomposition commutes with filtering charges
    • C.2.3. Decomposition preserves the charge map
    • C.2.4. Decomposition preserves the charges
    • C.2.5. Decomposition preserves the reduction
    • C.2.6. Fluxes of the decomposition of a FiveQuanta
• D. Lifting charges to FiveQuanta
  • D.1. liftCharge c: multiset of five-quanta for a finite set of charges c with no exotics
  • D.2. FiveQuanta in liftCharge c have a finite set of charges c
  • D.3. FiveQuanta in liftCharge c have no duplicate charges
  • D.4. Membership in liftCharge c iff is reduction of FiveQuanta with given fluxes
  • D.5. FiveQuanta in liftCharge c do not have zero fluxes
  • D.6. FiveQuanta in liftCharge c have no exotics
  • D.7. Membership in liftCharge c iff have no exotics, no zero fluxes, and charges c
  • D.8. liftCharge c is preserved under a map if reduced
• E. Anomaly cancellation coefficients
  • E.1. Anomaly coefficients of a FiveQuanta
  • E.2. Anomaly coefficients under a map
  • E.3. Anomaly coefficients is preserved under reduce

iv. References

A reference for the anomaly cancellation conditions is arXiv:1401.5084.

A. The definition of FiveQuanta

@[reducible, inline]

abbrev FTheory.SU5.FiveQuanta (𝓩 : Type := ℤ) : Type

The quanta of 5-bar representations corresponding to a multiset of (q, M, N) for each particle. (M, N) are defined in the FluxesFive module.

Equations

• FTheory.SU5.FiveQuanta 𝓩 = Multiset (𝓩 × FTheory.SU5.Fluxes)

A.1. The map to underlying fluxes

def FTheory.SU5.FiveQuanta.toFluxesFive {𝓩 : Type} (x : FiveQuanta 𝓩) : FluxesFive

The underlying FluxesFive from a FiveQuanta.

Equations

• x.toFluxesFive = Multiset.map Prod.snd x

A.2. The map to underlying charges

def FTheory.SU5.FiveQuanta.toCharges {𝓩 : Type} (x : FiveQuanta 𝓩) : Multiset 𝓩

The underlying Multiset charges from a FiveQuanta.

Equations

• x.toCharges = Multiset.map Prod.fst x

A.3. The map from charges to fluxes

def FTheory.SU5.FiveQuanta.toChargeMap {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) : 𝓩 → Fluxes

The map which takes a charge to the overall flux it corresponds to in a FiveQuanta.

Equations

• x.toChargeMap z = (Multiset.map Prod.snd (Multiset.filter (fun (p : 𝓩 × FTheory.SU5.Fluxes) => p.1 = z) x)).sum

theorem FTheory.SU5.FiveQuanta.toChargeMap_of_not_mem {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) {z : 𝓩} (h : z ∉ x.toCharges) : x.toChargeMap z = 0

B. The reduction of a FiveQuanta

def FTheory.SU5.FiveQuanta.reduce {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) : FiveQuanta 𝓩

The reduce of FiveQuanta is a new FiveQuanta with all the fluxes corresponding to the same charge (i.e. representation) added together.

Equations

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

B.1. The reduced FiveQuanta has no duplicate elements

theorem FTheory.SU5.FiveQuanta.reduce_nodup {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) : Multiset.Nodup x.reduce

@[simp]

theorem FTheory.SU5.FiveQuanta.reduce_dedup {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) : Multiset.dedup x.reduce = x.reduce

B.2. The underlying charges of the reduced FiveQuanta are the deduped charges

theorem FTheory.SU5.FiveQuanta.reduce_toCharges {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) : x.reduce.toCharges = x.toCharges.dedup

B.3. Membership condition on the reduced FiveQuanta

theorem FTheory.SU5.FiveQuanta.mem_reduce_iff {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) (p : 𝓩 × Fluxes) : p ∈ x.reduce ↔ p.1 ∈ x.toCharges ∧ p.2 = (Multiset.map (fun (y : 𝓩 × Fluxes) => y.2) (Multiset.filter (fun (f : 𝓩 × Fluxes) => f.1 = p.1) x)).sum

B.4. Filter of the reduced FiveQuanta by a charge

theorem FTheory.SU5.FiveQuanta.reduce_filter {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) (q : 𝓩) (h : q ∈ x.toCharges) : Multiset.filter (fun (f : 𝓩 × Fluxes) => f.1 = q) x.reduce = {(q, (Multiset.map (fun (y : 𝓩 × Fluxes) => y.2) (Multiset.filter (fun (f : 𝓩 × Fluxes) => f.1 = q) x)).sum)}

B.5. The reduction is idempotent

@[simp]

theorem FTheory.SU5.FiveQuanta.reduce_reduce {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) : x.reduce.reduce = x.reduce

B.6. Preservation of certain sums under reduction

theorem FTheory.SU5.FiveQuanta.reduce_sum_eq_sum_toCharges {𝓩 : Type} [DecidableEq 𝓩] {M : Type u_1} [AddCommMonoid M] (x : FiveQuanta 𝓩) (f : 𝓩 → Fluxes →+ M) : (Multiset.map (fun (x : 𝓩 × Fluxes) => match x with | (q5, x) => (f q5) x) x.reduce).sum = (Multiset.map (fun (x : 𝓩 × Fluxes) => match x with | (q5, x) => (f q5) x) x).sum

B.7. Reduction does nothing if no duplicate charges

theorem FTheory.SU5.FiveQuanta.reduce_eq_self_of_ofCharges_nodup {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) (h : x.toCharges.Nodup) : x.reduce = x

B.8. The charge map is preserved by reduction

theorem FTheory.SU5.FiveQuanta.reduce_toChargeMap_eq {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) : x.reduce.toChargeMap = x.toChargeMap

B.9. A fluxes in the reduced FiveQuanta is a sum of fluxes in the original FiveQuanta

theorem FTheory.SU5.FiveQuanta.mem_powerset_sum_of_mem_reduce_toFluxesFive {𝓩 : Type} [DecidableEq 𝓩] {F : FiveQuanta 𝓩} {f : Fluxes} (hf : f ∈ F.reduce.toFluxesFive) : f ∈ Multiset.map (fun (s : Multiset Fluxes) => s.sum) (Multiset.powerset F.toFluxesFive)

theorem FTheory.SU5.FiveQuanta.mem_powerset_sum_of_mem_reduce_toFluxesFive_filter {𝓩 : Type} [DecidableEq 𝓩] {F : FiveQuanta 𝓩} {f : Fluxes} (hf : f ∈ F.reduce.toFluxesFive) : f ∈ Multiset.map (fun (s : Multiset Fluxes) => s.sum) (Multiset.filter (fun (s : Multiset Fluxes) => s ≠ ∅) (Multiset.powerset F.toFluxesFive))

B.10. No exotics condition on the reduced FiveQuanta

B.10.1. Number of chiral L

theorem FTheory.SU5.FiveQuanta.reduce_numChiralL_of_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : FiveQuanta 𝓩} (hx : F.toFluxesFive ∈ FluxesFive.elemsNoExotics) : F.reduce.toFluxesFive.numChiralL = 3

B.10.2. Number of anti-chiral L

theorem FTheory.SU5.FiveQuanta.reduce_numAntiChiralL_of_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : FiveQuanta 𝓩} (hx : F.toFluxesFive ∈ FluxesFive.elemsNoExotics) : F.reduce.toFluxesFive.numAntiChiralL = 0

B.10.3. Number of chiral D

theorem FTheory.SU5.FiveQuanta.reduce_numChiralD_of_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : FiveQuanta 𝓩} (hx : F.toFluxesFive ∈ FluxesFive.elemsNoExotics) : F.reduce.toFluxesFive.numChiralD = 3

B.10.4. Number of anti-chiral D

theorem FTheory.SU5.FiveQuanta.reduce_numAntiChiralD_of_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : FiveQuanta 𝓩} (hx : F.toFluxesFive ∈ FluxesFive.elemsNoExotics) : F.reduce.toFluxesFive.numAntiChiralD = 0

B.10.5. The NoExotics condition on the reduced FiveQuanta

theorem FTheory.SU5.FiveQuanta.reduce_noExotics_of_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : FiveQuanta 𝓩} (hx : F.toFluxesFive ∈ FluxesFive.elemsNoExotics) : F.reduce.toFluxesFive.NoExotics

B.11. Reduce member of FluxesFive.elemsNoExotics

theorem FTheory.SU5.FiveQuanta.reduce_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : FiveQuanta 𝓩} (hx : F.toFluxesFive ∈ FluxesFive.elemsNoExotics) : F.reduce.toFluxesFive ∈ FluxesFive.elemsNoExotics

C. Decomposition of a FiveQuanta into basic fluxes

C.1. Decomposition of fluxes

def FTheory.SU5.FiveQuanta.decomposeFluxes (f : Fluxes) : Multiset Fluxes

The decomposition of a flux into ⟨1, -1⟩ and ⟨0, 1⟩.

Equations

• FTheory.SU5.FiveQuanta.decomposeFluxes f = Multiset.replicate f.M.natAbs { M := 1, N := -1 } + Multiset.replicate (f.M + f.N).natAbs { M := 0, N := 1 }

theorem FTheory.SU5.FiveQuanta.decomposeFluxes_sum_of_noExotics (f : Fluxes) (hf : ∃ F ∈ FluxesFive.elemsNoExotics, f ∈ F) : (decomposeFluxes f).sum = f

C.2. Decomposition of a FiveQuanta (with no exotics)

def FTheory.SU5.FiveQuanta.decompose {𝓩 : Type} (x : FiveQuanta 𝓩) : FiveQuanta 𝓩

The decomposition of a FiveQuanta into a FiveQuanta which has the same reduce by has fluxes ⟨1, -1⟩ and ⟨0,1⟩ only.

Equations

• x.decompose = Multiset.bind x fun (p : 𝓩 × FTheory.SU5.Fluxes) => Multiset.map (fun (f : FTheory.SU5.Fluxes) => (p.1, f)) (FTheory.SU5.FiveQuanta.decomposeFluxes p.2)

C.2.1. Decomposition distributes over addition

theorem FTheory.SU5.FiveQuanta.decompose_add {𝓩 : Type} (x y : FiveQuanta 𝓩) : (x + y).decompose = x.decompose + y.decompose

C.2.2. Decomposition commutes with filtering charges

theorem FTheory.SU5.FiveQuanta.decompose_filter_charge {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) (q : 𝓩) : Multiset.filter (fun (p : 𝓩 × Fluxes) => p.1 = q) x.decompose = decompose (Multiset.filter (fun (p : 𝓩 × Fluxes) => p.1 = q) x)

C.2.3. Decomposition preserves the charge map

theorem FTheory.SU5.FiveQuanta.decompose_toChargeMap {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) (hx : x.toFluxesFive ∈ FluxesFive.elemsNoExotics) : x.decompose.toChargeMap = x.toChargeMap

C.2.4. Decomposition preserves the charges

theorem FTheory.SU5.FiveQuanta.decompose_toCharges_dedup {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) (hx : x.toFluxesFive ∈ FluxesFive.elemsNoExotics) : x.decompose.toCharges.dedup = x.toCharges.dedup

C.2.5. Decomposition preserves the reduction

theorem FTheory.SU5.FiveQuanta.decompose_reduce {𝓩 : Type} (x : FiveQuanta 𝓩) [DecidableEq 𝓩] (hx : x.toFluxesFive ∈ FluxesFive.elemsNoExotics) : x.decompose.reduce = x.reduce

C.2.6. Fluxes of the decomposition of a FiveQuanta

theorem FTheory.SU5.FiveQuanta.decompose_toFluxesFive {𝓩 : Type} (x : FiveQuanta 𝓩) (hx : x.toFluxesFive ∈ FluxesFive.elemsNoExotics) : x.decompose.toFluxesFive = {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}

D. Lifting charges to FiveQuanta

D.1. liftCharge c: multiset of five-quanta for a finite set of charges c with no exotics

This is an efficient definition, we will later show that it gives the correct answer

def FTheory.SU5.FiveQuanta.liftCharge {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) : Multiset (FiveQuanta 𝓩)

Given a finite set of charges c the FiveQuanta which do not have exotics, duplicate charges or zero fluxes, which map down to c.

Equations

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

D.2. FiveQuanta in liftCharge c have a finite set of charges c

theorem FTheory.SU5.FiveQuanta.toCharges_toFinset_of_mem_liftCharge {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : FiveQuanta 𝓩} (h : x ∈ liftCharge c) : x.toCharges.toFinset = c

D.3. FiveQuanta in liftCharge c have no duplicate charges

theorem FTheory.SU5.FiveQuanta.toCharges_nodup_of_mem_liftCharge {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : FiveQuanta 𝓩} (h : x ∈ liftCharge c) : x.toCharges.Nodup

D.4. Membership in liftCharge c iff is reduction of FiveQuanta with given fluxes

theorem FTheory.SU5.FiveQuanta.exists_toCharges_toFluxesFive_of_mem_liftCharge {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : FiveQuanta 𝓩} (h : x ∈ liftCharge c) : ∃ (a : FiveQuanta 𝓩), a.reduce = x ∧ a.toCharges.toFinset = c ∧ a.toFluxesFive = {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}

theorem FTheory.SU5.FiveQuanta.mem_liftCharge_of_exists_toCharges_toFluxesFive {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : FiveQuanta 𝓩} (h : ∃ (a : FiveQuanta 𝓩), a.reduce = x ∧ a.toCharges.toFinset = c ∧ a.toFluxesFive = {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}) : x ∈ liftCharge c

theorem FTheory.SU5.FiveQuanta.mem_liftCharge_iff_exists {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : FiveQuanta 𝓩} : x ∈ liftCharge c ↔ ∃ (a : FiveQuanta 𝓩), a.reduce = x ∧ a.toCharges.toFinset = c ∧ a.toFluxesFive = {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}

D.5. FiveQuanta in liftCharge c do not have zero fluxes

theorem FTheory.SU5.FiveQuanta.hasNoZero_of_mem_liftCharge {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : FiveQuanta 𝓩} (h : x ∈ liftCharge c) : x.toFluxesFive.HasNoZero

D.6. FiveQuanta in liftCharge c have no exotics

theorem FTheory.SU5.FiveQuanta.noExotics_of_mem_liftCharge {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) (F : FiveQuanta 𝓩) (h : F ∈ liftCharge c) : F.toFluxesFive.NoExotics

D.7. Membership in liftCharge c iff have no exotics, no zero fluxes, and charges c

theorem FTheory.SU5.FiveQuanta.mem_liftCharge_of_mem_noExotics_hasNoZero {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : FiveQuanta 𝓩} (h1 : x.toFluxesFive.NoExotics) (h2 : x.toFluxesFive.HasNoZero) (h3 : x.toCharges.toFinset = c) (h4 : x.toCharges.Nodup) : x ∈ liftCharge c

theorem FTheory.SU5.FiveQuanta.mem_liftCharge_iff {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) (x : FiveQuanta 𝓩) : x ∈ liftCharge c ↔ x.toFluxesFive ∈ FluxesFive.elemsNoExotics ∧ x.toCharges.toFinset = c ∧ x.toCharges.Nodup

D.8. liftCharge c is preserved under a map if reduced

theorem FTheory.SU5.FiveQuanta.map_liftCharge {𝓩 𝓩1 : Type} [DecidableEq 𝓩] [DecidableEq 𝓩1] [CommRing 𝓩] [CommRing 𝓩1] (f : 𝓩 →+* 𝓩1) (c : Finset 𝓩) (F : FiveQuanta 𝓩) (h : F ∈ liftCharge c) : reduce (Multiset.map (fun (y : 𝓩 × Fluxes) => (f y.1, y.2)) F) ∈ liftCharge (Finset.image (⇑f) c)

E. Anomaly cancellation coefficients

E.1. Anomaly coefficients of a FiveQuanta

def FTheory.SU5.FiveQuanta.anomalyCoefficient {𝓩 : Type} [CommRing 𝓩] (F : FiveQuanta 𝓩) : 𝓩 × 𝓩

The anomaly coefficient of a FiveQuanta is given by the pair of integers: (∑ᵢ qᵢ Nᵢ, ∑ᵢ qᵢ² Nᵢ).

The first components is for the mixed U(1)-MSSM, see equation (22) of arXiv:1401.5084. The second component is for the mixed U(1)Y-U(1)-U(1) gauge anomaly, see equation (23) of arXiv:1401.5084.

Equations

• F.anomalyCoefficient = ((Multiset.map (fun (x : 𝓩 × FTheory.SU5.Fluxes) => x.2.N • x.1) F).sum, (Multiset.map (fun (x : 𝓩 × FTheory.SU5.Fluxes) => x.2.N • (x.1 * x.1)) F).sum)

E.2. Anomaly coefficients under a map

@[simp]

theorem FTheory.SU5.FiveQuanta.anomalyCoefficient_of_map {𝓩 𝓩1 : Type} [CommRing 𝓩] [CommRing 𝓩1] (f : 𝓩 →+* 𝓩1) (F : FiveQuanta 𝓩) : anomalyCoefficient (Multiset.map (fun (y : 𝓩 × Fluxes) => (f y.1, y.2)) F) = (f.prodMap f) F.anomalyCoefficient

E.3. Anomaly coefficients is preserved under reduce

theorem FTheory.SU5.FiveQuanta.anomalyCoefficient_of_reduce {𝓩 : Type} [CommRing 𝓩] (F : FiveQuanta 𝓩) [DecidableEq 𝓩] : F.reduce.anomalyCoefficient = F.anomalyCoefficient