Constraints on chiral indices from the condition of no chiral exotics

On the types FluxesFive and FluxesTen, we have the conditions NoExotics, corresponding to the non-existence of chiral exotics in the spectrum.

These conditions lead to constraints of the chiral indices of the SM representations. For example:

• They must be non-negative.
• They must be less than or equal to 3.
• The non-zero chiral indices must be one of the following multisets {1, 1, 1}, {1, 2}, {3}.

This module proves these constraints.

Constraints on the chiral indices of D = (bar 3,1)_{1/3}

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.FluxesFive.mem_chiralIndicesOfD_mem_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfD) : ci ∈ {0, 1, 2, 3}

theorem FTheory.SU5U1.FluxesFive.chiralIndicesOfD_subset_sum_le_three_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (S : Multiset (ℤ × ℤ)) (hSle : S ≤ F) : (Multiset.map (fun (x : ℤ × ℤ) => x.1) S).sum ≤ 3

Constraints on the chiral indices of L = (1,2)_{-1/2}

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.FluxesFive.mem_chiralIndicesOfL_mem_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfL) : ci ∈ {0, 1, 2, 3}

theorem FTheory.SU5U1.FluxesFive.chiralIndicesOfL_subset_sum_le_three_of_noExotics (F : FluxesFive) (hF : F.NoExotics) (S : Multiset (ℤ × ℤ)) (hSle : S ≤ F) : (Multiset.map (fun (x : ℤ × ℤ) => x.1 + x.2) S).sum ≤ 3

Constraints on the chiral indices of Q = (3,2)_{1/6}

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.FluxesTen.mem_chiralIndicesOfQ_mem_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfQ) : ci ∈ {0, 1, 2, 3}

theorem FTheory.SU5U1.FluxesTen.chiralIndicesOfQ_subset_sum_le_three_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (S : Multiset (ℤ × ℤ)) (hSle : S ≤ F) : (Multiset.map (fun (x : ℤ × ℤ) => x.1) S).sum ≤ 3

Constraints on the chiral indices of U = (bar 3,1)_{-2/3}

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.FluxesTen.mem_chiralIndicesOfU_mem_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfU) : ci ∈ {0, 1, 2, 3}

theorem FTheory.SU5U1.FluxesTen.chiralIndicesOfU_subset_sum_le_three_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (S : Multiset (ℤ × ℤ)) (hSle : S ≤ F) : (Multiset.map (fun (x : ℤ × ℤ) => x.1 - x.2) S).sum ≤ 3

Constraints on the chiral indices of E = (1,1)_{1}

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

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.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.

theorem FTheory.SU5U1.FluxesTen.mem_chiralIndicesOfE_mem_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfE) : ci ∈ {0, 1, 2, 3}

theorem FTheory.SU5U1.FluxesTen.chiralIndicesOfE_subset_sum_le_three_of_noExotics (F : FluxesTen) (hF : F.NoExotics) (S : Multiset (ℤ × ℤ)) (hSle : S ≤ F) : (Multiset.map (fun (x : ℤ × ℤ) => x.1 + x.2) S).sum ≤ 3