PhysLean Documentation

PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.ChiralIndices

Constraints on chiral indices from the condition of no chiral exotics #

i. Overview #

The chiral indices of each of the standard model representations satisfy certain constraints if there are no chiral exotics in the spectrum. We give prove these constraints in this file.

ii. Key results #

Each of the following results holds for each of the standard model representations, we state them for the representation D = (bar 3,1)_{1/3} only:

iii. Table of contents #

iv. References #

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

A. Positivity of the chiral indices given no exotics #

The chiral indices of all the SM representations are non-negative if there are no chiral exotics.

source
theorem FTheory.SU5.FluxesFive.chiralIndicesOfD_noneg_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfD) :
0 ≤ ci

The chiral indices of the representations D = (bar 3,1)_{1/3} are all non-negative if there are no chiral exotics in the spectrum.

source
theorem FTheory.SU5.FluxesFive.chiralIndicesOfL_noneg_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfL) :
0 ≤ ci

The chiral indices of the representations L = (1,2)_{-1/2} are all non-negative if there are no chiral exotics in the spectrum.

source
theorem FTheory.SU5.FluxesTen.chiralIndicesOfQ_noneg_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfQ) :
0 ≤ ci

The chiral indices of the representations Q = (3,2)_{1/6} are all non-negative if there are no chiral exotics in the spectrum.

source
theorem FTheory.SU5.FluxesTen.chiralIndicesOfU_noneg_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfU) :
0 ≤ ci

The chiral indices of the representations U = (bar 3,1)_{-2/3} are all non-negative if there are no chiral exotics in the spectrum.

source
theorem FTheory.SU5.FluxesTen.chiralIndicesOfE_noneg_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfE) :
0 ≤ ci

B. Chiral indices sum to three given no exotics #

The sum of the chiral indices of each representation is equal to three if there are no chiral exotics.

source
theorem FTheory.SU5.FluxesFive.chiralIndicesOfD_sum_eq_three_of_noExotics (F : FluxesFive) (hF : F.NoExotics) :
F.chiralIndicesOfD.sum = 3

The sum of the chiral indices of the representations D = (bar 3,1)_{1/3} is equal to 3 in the presences of no exotics.

source
theorem FTheory.SU5.FluxesFive.chiralIndicesOfL_sum_eq_three_of_noExotics (F : FluxesFive) (hF : F.NoExotics) :
F.chiralIndicesOfL.sum = 3

The sum of the chiral indices of the representations L = (1,2)_{-1/2} is equal to 3 in the presences of no exotics.

source
theorem FTheory.SU5.FluxesTen.chiralIndicesOfQ_sum_eq_three_of_noExotics (F : FluxesTen) (hF : F.NoExotics) :
F.chiralIndicesOfQ.sum = 3

The sum of the chiral indices of the representations Q = (3,2)_{1/6} is equal to 3 in the presences of no exotics.

source
theorem FTheory.SU5.FluxesTen.chiralIndicesOfU_sum_eq_three_of_noExotics (F : FluxesTen) (hF : F.NoExotics) :
F.chiralIndicesOfU.sum = 3

The sum of the chiral indices of the representations U = (bar 3,1)_{-2/3} is equal to 3 in the presences of no exotics.

source
theorem FTheory.SU5.FluxesTen.chiralIndicesOfE_sum_eq_three_of_noExotics (F : FluxesTen) (hF : F.NoExotics) :
F.chiralIndicesOfE.sum = 3

The sum of the chiral indices of the representations E = (1,1)_{1} is equal to 3 in the presences of no exotics.

C. Each chiral index is less then or equal to three given no exotics #

source
theorem FTheory.SU5.FluxesFive.chiralIndicesOfD_le_three_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfD) :
ci ≤ 3

The chiral indices of the representation D = (bar 3,1)_{1/3} are less then or equal to 3.

source
theorem FTheory.SU5.FluxesFive.chiralIndicesOfL_le_three_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfL) :
ci ≤ 3

The chiral indices of the representation L = (1,2)_{-1/2} are less then or equal to 3.

source
theorem FTheory.SU5.FluxesTen.chiralIndicesOfQ_le_three_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfQ) :
ci ≤ 3

The chiral indices of the representation Q = (3,2)_{1/6} are less then or equal to 3.

source
theorem FTheory.SU5.FluxesTen.chiralIndicesOfU_le_three_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfU) :
ci ≤ 3

The chiral indices of the representation U = (bar 3,1)_{-2/3} are less then or equal to 3.

source
theorem FTheory.SU5.FluxesTen.chiralIndicesOfE_le_three_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfE) :
ci ≤ 3

The chiral indices of the representation E = (1,1)_{1} are less then or equal to 3.

D. Each chiral index is 0, 1, 2, or 3 given no exotics #

source
theorem FTheory.SU5.FluxesFive.mem_chiralIndicesOfD_mem_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfD) :
ci ∈ {0, 1, 2, 3}
source
theorem FTheory.SU5.FluxesFive.mem_chiralIndicesOfL_mem_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfL) :
ci ∈ {0, 1, 2, 3}
source
theorem FTheory.SU5.FluxesTen.mem_chiralIndicesOfQ_mem_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfQ) :
ci ∈ {0, 1, 2, 3}
source
theorem FTheory.SU5.FluxesTen.mem_chiralIndicesOfU_mem_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfU) :
ci ∈ {0, 1, 2, 3}
source
theorem FTheory.SU5.FluxesTen.mem_chiralIndicesOfE_mem_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfE) :
ci ∈ {0, 1, 2, 3}

E. Sum of a subset of chiral indices is less then or equal to 3 given no exotics #

source
theorem FTheory.SU5.FluxesFive.chiralIndicesOfD_subset_sum_le_three_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (S : Multiset Fluxes) (hSle : S ≤ F) :
(Multiset.map (fun (x : Fluxes) => x.M) S).sum ≤ 3
source
theorem FTheory.SU5.FluxesFive.chiralIndicesOfL_subset_sum_le_three_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (S : Multiset Fluxes) (hSle : S ≤ F) :
(Multiset.map (fun (x : Fluxes) => x.M + x.N) S).sum ≤ 3
source
theorem FTheory.SU5.FluxesTen.chiralIndicesOfQ_subset_sum_le_three_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (S : Multiset Fluxes) (hSle : S ≤ F) :
(Multiset.map (fun (x : Fluxes) => x.M) S).sum ≤ 3
source
theorem FTheory.SU5.FluxesTen.chiralIndicesOfU_subset_sum_le_three_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (S : Multiset Fluxes) (hSle : S ≤ F) :
(Multiset.map (fun (x : Fluxes) => x.M - x.N) S).sum ≤ 3
source
theorem FTheory.SU5.FluxesTen.chiralIndicesOfE_subset_sum_le_three_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (S : Multiset Fluxes) (hSle : S ≤ F) :
(Multiset.map (fun (x : Fluxes) => x.M + x.N) S).sum ≤ 3