Fluxes of representations

i. Overview

Associated with each matter curve Σ are G₄-fluxes and hypercharge fluxes.

For a given matter curve Σ, and a Standard Model representation R, these two fluxes contribute to the chiral index χ(R) of the representation (eq 17 of [1]).

The chiral index is equal to the difference the number of left-handed minus the number of right-handed fermions Σ leads to in the representation R. Thus, for example, if χ(R) = 0, then all fermions in the representation R arising from Σ arise in vector-like pairs, and can be given a mass term without the presence of a Higgs like-particle.

For a 10d representation matter curve the non-zero chiral indices can be parameterized in terms of two integers M : ℤ and N : ℤ. For the SM representation

• Q = (3,2)_{1/6} the chirality index is M
• U = (bar 3,1)_{-2/3} the chirality index is M - N
• E = (1,1)_{1} the chirality index is M + N We call refer to M as the chirality flux of the 10d representation, and N as the hypercharge flux. There exact definitions are given in (eq 19 of [1]).

Similarly, for the 5-bar representation matter curve the non-zero chiral indices can be likewise be parameterized in terms of two integers M : ℤ and N : ℤ. For the SM representation

• D = (bar 3,1)_{1/3} the chirality index is M
• L = (1,2)_{-1/2} the chirality index is M + N We again refer to M as the chirality flux of the 5-bar representation, and N as the hypercharge flux. The exact definitions are given in (eq 19 of [1]).

If one wishes to put the condition of no chiral exotics in the spectrum, then we must ensure that the chiral indices above give the chiral content of the MSSM. These correspond to the following conditions:

1. The two higgs Hu and Hd must arise from different 5d-matter curves. Otherwise they will give a μ-term.
2. The matter curve containing Hu must give one anti-chiral (1,2)_{-1/2} and no (bar 3,1)_{1/3}. Thus N = -1 and M = 0.
3. The matter curve containing Hd must give one chiral (1,2)_{-1/2} and no (bar 3,1)_{1/3}. Thus N = 1 and M = 0.
4. We should have no anti-chiral (3,2)_{1/6} and anti-chiral (bar 3,1)_{-2/3}. Thus 0 ≤ M for all 10d-matter curves and 5d matter curves.
5. For the 10d-matter curves we should have no anti-chiral (bar 3,1)_{-2/3} and no anti-chiral (1,1)_{1}. Thus -M ≤ N ≤ M for all 10d-matter curves.
6. For the 5d-matter curves we should have no anti-chiral (1,2)_{-1/2} (the only anti-chiral one present is the one from Hu) and thus -M ≤ N for all 5d-matter curves.
7. To ensure we have 3-families of fermions we must have that ∑ M = 3 and ∑ N = 0 for the matter 10d and 5bar matter curves, and in addition ∑ (M + N) = 3 for the matter 5d matter curves. See the conditions in equation 26 - 28 of [1].

ii. Key results

The above theory is implemented by defining two data structures:

• Fluxes : The data of the fluxes (M, N) carried by a matter field.
• FluxesTen of type Multiset Fluxes which contains the chirality M and hypercharge fluxes N of the 10d-matter curves.
• FluxesFive of type Multiset Fluxes which contains the chirality M and hypercharge fluxes N of the 5-bar-matter curves (excluding the higgses).

Note: Neither FluxesTen or FluxesFive are fundamental to the theory, they can be derived from other data structures.

iii. Table of contents

• A. Fluxes
  • A.1. Repr instance on Fluxes
  • A.2. Extensionality lemma for the fluxes
  • A.3. The zero flux
  • A.4. Addition of fluxes
  • A.5. The instance of an additive commutative monoid on fluxes
• B. Fluxes of the 5d matter representation
  • B.1. Decidability instance on FluxesFive
  • B.2. The proposition for no element to be zero
  • B.3. The SM representation D = (bar 3,1)_{1/3}
    • B.3.1. Chiral indices of D
    • B.3.2. The number of chiral D
    • B.3.3. The number of anti-chiral D
    • B.3.4. Relation between number of chiral and anti-chiral D
  • B.4. The SM representation L = (1,2)_{-1/2}
    • B.4.1. Chiral indices of L
    • B.4.2. The number of chiral L
    • B.4.3. The number of anti-chiral L
    • B.4.4. Relation between number of chiral and anti-chiral L
  • B.5. No exotics from the 5-bar matter fields
• C. Fluxes of the 10d matter representation
  • C.1. Decidability instance on FluxesTen
  • C.2. The proposition for no element to be zero
  • C.3. The SM representation Q = (3,2)_{1/6}
    • C.3.1. Chiral indices of Q
    • C.3.2. The number of chiral Q
    • C.3.3. The number of anti-chiral Q
    • C.3.4. Relation between number of chiral and anti-chiral Q
  • C.4. The SM representation U = (bar 3,1)_{-2/3}
    • C.4.1. Chiral indices of U
    • C.4.2. The number of chiral U
    • C.4.3. The number of anti-chiral U
    • C.4.4. Relation between number of chiral and anti-chiral Q
  • C.5. The SM representation E = (1,1)_{1}
    • C.5.1. Chiral indices of E
    • C.5.2. The number of chiral E
    • C.5.3. The number of anti-chiral E
    • C.5.4. Relation between number of chiral and anti-chiral E
  • C.6. No exotics from the 10d matter fields

iv. References

• [1] arXiv:1401.5084
• For an old version of the material in this module see PR #569.

A. Fluxes

To each matter curve we associate a pair of integers (M, N), the former of which is the chirality flux and the latter the hypercharge flux.

structure FTheory.SU5.Fluxes : Type

The data of the fluxes carried by a matter field.

• M : ℤ

  The chirality flux.

• N : ℤ

  The hypercharge flux.

def FTheory.SU5.instDecidableEqFluxes.decEq (x✝ x✝¹ : Fluxes) : Decidable (x✝ = x✝¹)

Equations

• FTheory.SU5.instDecidableEqFluxes.decEq { M := a, N := a_1 } { M := b, N := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance FTheory.SU5.instDecidableEqFluxes : DecidableEq Fluxes

Equations

• FTheory.SU5.instDecidableEqFluxes = FTheory.SU5.instDecidableEqFluxes.decEq

A.1. Repr instance on Fluxes

instance FTheory.SU5.Fluxes.instRepr : Repr Fluxes

Equations

• FTheory.SU5.Fluxes.instRepr = { reprPrec := fun (x : FTheory.SU5.Fluxes) (x_1 : ℕ) => Std.Format.text "⟨" ++ repr x.M ++ Std.Format.text ", " ++ repr x.N ++ Std.Format.text "⟩" }

A.2. Extensionality lemma for the fluxes

theorem FTheory.SU5.Fluxes.ext_iff {f1 f2 : Fluxes} : f1 = f2 ↔ f1.M = f2.M ∧ f1.N = f2.N

instance FTheory.SU5.Fluxes.instZero : Zero Fluxes

Equations

• FTheory.SU5.Fluxes.instZero = { zero := { M := 0, N := 0 } }

A.3. The zero flux

@[simp]

theorem FTheory.SU5.Fluxes.zero_M : M 0 = 0

@[simp]

theorem FTheory.SU5.Fluxes.zero_N : N 0 = 0

A.4. Addition of fluxes

instance FTheory.SU5.Fluxes.instAdd : Add Fluxes

Equations

• FTheory.SU5.Fluxes.instAdd = { add := fun (f1 f2 : FTheory.SU5.Fluxes) => { M := f1.M + f2.M, N := f1.N + f2.N } }

@[simp]

theorem FTheory.SU5.Fluxes.add_M (f1 f2 : Fluxes) : (f1 + f2).M = f1.M + f2.M

@[simp]

theorem FTheory.SU5.Fluxes.add_N (f1 f2 : Fluxes) : (f1 + f2).N = f1.N + f2.N

A.5. The instance of an additive commutative monoid on fluxes

instance FTheory.SU5.Fluxes.instAddCommMonoid : AddCommMonoid Fluxes

Equations

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

B. Fluxes of the 5d matter representation

@[reducible, inline]

abbrev FTheory.SU5.FluxesFive : Type

The fluxes (M, N) of the 5-bar matter curves of a theory.

Equations

• FTheory.SU5.FluxesFive = Multiset FTheory.SU5.Fluxes

B.1. Decidability instance on FluxesFive

instance FTheory.SU5.FluxesFive.instDecidableEq : DecidableEq FluxesFive

Equations

• FTheory.SU5.FluxesFive.instDecidableEq = inferInstanceAs (DecidableEq (Multiset FTheory.SU5.Fluxes))

B.2. The proposition for no element to be zero

@[reducible, inline]

abbrev FTheory.SU5.FluxesFive.HasNoZero (F : FluxesFive) : Prop

The proposition on FluxesFive such that (0, 0) is not in F and as such each component in F leads to chiral matter.

Equations

• F.HasNoZero = (0 ∉ F)

B.3. The SM representation D = (bar 3,1)_{1/3}

B.3.1. Chiral indices of D

def FTheory.SU5.FluxesFive.chiralIndicesOfD (F : FluxesFive) : Multiset ℤ

The multiset of chiral indices of the representation D = (bar 3,1)_{1/3} arising from the matter 5d representations.

Equations

• F.chiralIndicesOfD = Multiset.map (fun (f : FTheory.SU5.Fluxes) => f.M) F

B.3.2. The number of chiral D

def FTheory.SU5.FluxesFive.numChiralD (F : FluxesFive) : ℤ

The total number of chiral D representations arising from the matter 5d representations.

Equations

• F.numChiralD = (Multiset.filter (fun (x : ℤ) => 0 ≤ x) F.chiralIndicesOfD).sum

B.3.3. The number of anti-chiral D

def FTheory.SU5.FluxesFive.numAntiChiralD (F : FluxesFive) : ℤ

The total number of anti-chiral D representations arising from the matter 5d representations.

Equations

• F.numAntiChiralD = (Multiset.filter (fun (x : ℤ) => x < 0) F.chiralIndicesOfD).sum

B.3.4. Relation between number of chiral and anti-chiral D

theorem FTheory.SU5.FluxesFive.numChiralD_eq_sum_sub_numAntiChiralD (F : FluxesFive) : F.numChiralD = F.chiralIndicesOfD.sum - F.numAntiChiralD

B.4. The SM representation L = (1,2)_{-1/2}

B.4.1. Chiral indices of L

def FTheory.SU5.FluxesFive.chiralIndicesOfL (F : FluxesFive) : Multiset ℤ

The multiset of chiral indices of the representation L = (1,2)_{-1/2} arising from the matter 5d representations.

Equations

• F.chiralIndicesOfL = Multiset.map (fun (f : FTheory.SU5.Fluxes) => f.M + f.N) F

B.4.2. The number of chiral L

def FTheory.SU5.FluxesFive.numChiralL (F : FluxesFive) : ℤ

The total number of chiral L representations arising from the matter 5d representations.

Equations

• F.numChiralL = (Multiset.filter (fun (x : ℤ) => 0 ≤ x) F.chiralIndicesOfL).sum

B.4.3. The number of anti-chiral L

def FTheory.SU5.FluxesFive.numAntiChiralL (F : FluxesFive) : ℤ

The total number of anti-chiral L representations arising from the matter 5d representations.

Equations

• F.numAntiChiralL = (Multiset.filter (fun (x : ℤ) => x < 0) F.chiralIndicesOfL).sum

B.4.4. Relation between number of chiral and anti-chiral L

theorem FTheory.SU5.FluxesFive.numChiralL_eq_sum_sub_numAntiChiralL (F : FluxesFive) : F.numChiralL = F.chiralIndicesOfL.sum - F.numAntiChiralL

B.5. No exotics from the 5-bar matter fields

def FTheory.SU5.FluxesFive.NoExotics (F : FluxesFive) : Prop

The condition that the 5d-matter representations do not lead to exotic chiral matter in the MSSM spectrum. This corresponds to the conditions that:

• There are 3 chiral L representations and no anti-chiral L representations.
• There are 3 chiral D representations and no anti-chiral D representations.

Equations

• F.NoExotics = (F.numChiralL = 3 ∧ F.numAntiChiralL = 0 ∧ F.numChiralD = 3 ∧ F.numAntiChiralD = 0)

instance FTheory.SU5.FluxesFive.instDecidableNoExotics (F : FluxesFive) : Decidable F.NoExotics

Equations

• F.instDecidableNoExotics = instDecidableAnd

C. Fluxes of the 10d matter representation

@[reducible, inline]

abbrev FTheory.SU5.FluxesTen : Type

The fluxes (M, N) of the 10d matter curves of a theory.

Equations

• FTheory.SU5.FluxesTen = Multiset FTheory.SU5.Fluxes

C.1. Decidability instance on FluxesTen

instance FTheory.SU5.FluxesTen.instDecidableEq : DecidableEq FluxesTen

Equations

• FTheory.SU5.FluxesTen.instDecidableEq = inferInstanceAs (DecidableEq (Multiset FTheory.SU5.Fluxes))

C.2. The proposition for no element to be zero

@[reducible, inline]

abbrev FTheory.SU5.FluxesTen.HasNoZero (F : FluxesTen) : Prop

The proposition on FluxesTen such that (0, 0) is not in F and as such each component in F leads to chiral matter.

Equations

• F.HasNoZero = (0 ∉ F)

C.3. The SM representation Q = (3,2)_{1/6}

C.3.1. Chiral indices of Q

def FTheory.SU5.FluxesTen.chiralIndicesOfQ (F : FluxesTen) : Multiset ℤ

The multiset of chiral indices of the representation Q = (3,2)_{1/6} arising from the matter 10d representations, corresponding to M.

Equations

• F.chiralIndicesOfQ = Multiset.map (fun (f : FTheory.SU5.Fluxes) => f.M) F

C.3.2. The number of chiral Q

def FTheory.SU5.FluxesTen.numChiralQ (F : FluxesTen) : ℤ

The total number of chiral Q representations arising from the matter 10d representations.

Equations

• F.numChiralQ = (Multiset.filter (fun (x : ℤ) => 0 ≤ x) F.chiralIndicesOfQ).sum

C.3.3. The number of anti-chiral Q

def FTheory.SU5.FluxesTen.numAntiChiralQ (F : FluxesTen) : ℤ

The total number of anti-chiral Q representations arising from the matter 10d representations.

Equations

• F.numAntiChiralQ = (Multiset.filter (fun (x : ℤ) => x < 0) F.chiralIndicesOfQ).sum

C.3.4. Relation between number of chiral and anti-chiral Q

theorem FTheory.SU5.FluxesTen.numChiralQ_eq_sum_sub_numAntiChiralQ (F : FluxesTen) : F.numChiralQ = F.chiralIndicesOfQ.sum - F.numAntiChiralQ

C.4. The SM representation U = (bar 3,1)_{-2/3}

C.4.1. Chiral indices of U

def FTheory.SU5.FluxesTen.chiralIndicesOfU (F : FluxesTen) : Multiset ℤ

The multiset of chiral indices of the representation U = (bar 3,1)_{-2/3} arising from the matter 10d representations, corresponding to M - N

Equations

• F.chiralIndicesOfU = Multiset.map (fun (f : FTheory.SU5.Fluxes) => f.M - f.N) F

C.4.2. The number of chiral U

def FTheory.SU5.FluxesTen.numChiralU (F : FluxesTen) : ℤ

The total number of chiral U representations arising from the matter 10d representations.

Equations

• F.numChiralU = (Multiset.filter (fun (x : ℤ) => 0 ≤ x) F.chiralIndicesOfU).sum

C.4.3. The number of anti-chiral U

def FTheory.SU5.FluxesTen.numAntiChiralU (F : FluxesTen) : ℤ

The total number of anti-chiral U representations arising from the matter 10d representations.

Equations

• F.numAntiChiralU = (Multiset.filter (fun (x : ℤ) => x < 0) F.chiralIndicesOfU).sum

theorem FTheory.SU5.FluxesTen.numChiralU_eq_sum_sub_numAntiChiralU (F : FluxesTen) : F.numChiralU = F.chiralIndicesOfU.sum - F.numAntiChiralU

C.5. The SM representation E = (1,1)_{1}

C.5.1. Chiral indices of E

def FTheory.SU5.FluxesTen.chiralIndicesOfE (F : FluxesTen) : Multiset ℤ

The multiset of chiral indices of the representation E = (1,1)_{1} arising from the matter 10d representations, corresponding to M + N

Equations

• F.chiralIndicesOfE = Multiset.map (fun (f : FTheory.SU5.Fluxes) => f.M + f.N) F

C.5.2. The number of chiral E

def FTheory.SU5.FluxesTen.numChiralE (F : FluxesTen) : ℤ

The total number of chiral E representations arising from the matter 10d representations.

Equations

• F.numChiralE = (Multiset.filter (fun (x : ℤ) => 0 ≤ x) F.chiralIndicesOfE).sum

C.5.3. The number of anti-chiral E

def FTheory.SU5.FluxesTen.numAntiChiralE (F : FluxesTen) : ℤ

The total number of anti-chiral E representations arising from the matter 10d representations.

Equations

• F.numAntiChiralE = (Multiset.filter (fun (x : ℤ) => x < 0) F.chiralIndicesOfE).sum

C.5.4. Relation between number of chiral and anti-chiral E

theorem FTheory.SU5.FluxesTen.numChiralE_eq_sum_sub_numAntiChiralE (F : FluxesTen) : F.numChiralE = F.chiralIndicesOfE.sum - F.numAntiChiralE

C.6. No exotics from the 10d matter fields

def FTheory.SU5.FluxesTen.NoExotics (F : FluxesTen) : Prop

The condition that the 10d-matter representations do not lead to exotic chiral matter in the MSSM spectrum. This corresponds to the conditions that:

• There are 3 chiral Q representations and no anti-chiral Q representations.
• There are 3 chiral U representations and no anti-chiral U representations.
• There are 3 chiral E representations and no anti-chiral E representations.

Equations

• F.NoExotics = (F.numChiralQ = 3 ∧ F.numAntiChiralQ = 0 ∧ F.numChiralU = 3 ∧ F.numAntiChiralU = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0)

instance FTheory.SU5.FluxesTen.instDecidableNoExotics (F : FluxesTen) : Decidable F.NoExotics

Equations

• F.instDecidableNoExotics = instDecidableAnd