Research proof index

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.

The chiral indices of the representation E = (1,1)_{1} are less then or equal to 3. -/ lemma FluxesTen.chiralIndicesOfE_le_three_of_noExotics (F : FluxesTen) (hF : NoExotics F) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfE) : ci ≤ 3 := by have hle := Multiset.single_le_sum (fun x hx => chiralIndicesOfE_noneg_of_noExotics F hF x hx) ci hci rwa [F.chiralIndic...

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

The allowed subsets of a FluxesFive which has no exotics or zeros. -/ def noExoticsSubsets : (n : ℕ) → Finset (Multiset Fluxes) | 0 => {{}} | 1 => {{⟨0, 1⟩}, {⟨0, 2⟩}, {⟨0, 3⟩}, {⟨1, -1⟩}, {⟨1, 0⟩}, {⟨1, 1⟩}, {⟨1, 2⟩}, {⟨2, -2⟩}, {⟨2, -1⟩}, {⟨2, 0⟩}, {⟨2, 1⟩}, {⟨3, -3⟩}, {⟨3, -2⟩}, {⟨3, -1⟩}, {⟨3, 0⟩}} | 2 => {{⟨0, 1⟩, ⟨0, 1⟩}, {⟨0, 1⟩, ⟨1, -1⟩}, {⟨0, 1...

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

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.