Physlib.StringTheory.FTheory.SU5.Fluxes.NoExotics.ChiralIndices

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.StringTheory.FTheory.SU5.Fluxes.Basic

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:

Each chiral index is non-negative, FluxesFive.chiralIndicesOfD_noneg_of_noExotics.

The sum of the chiral indices is equal to three, FluxesFive.chiralIndicesOfD_sum_eq_three_of_noExotics.

Each chiral index is less then or equal to three, FluxesFive.chiralIndicesOfD_le_three_of_noExotics.

Each chiral index is 0, 1, 2 or 3, FluxesFive.mem_chiralIndicesOfD_mem_of_noExotics

The sum of a subset of the chiral indices is less then or equal to three, FluxesFive.chiralIndicesOfD_subset_sum_le_three_of_noExotics.

iii. Table of contents

A. Positivity of the chiral indices given no exotics

B. Chiral indices sum to three given no exotics

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

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

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

iv. References

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

@[expose] public section

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.

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.


lemma FluxesFive.chiralIndicesOfD_noneg_of_noExotics (F : FluxesFive) (hF : NoExotics F)
    (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfD) : 0 ≤ ci := byF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfD⊢ 0 ≤ ci
  by_contra hnF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:¬0 ≤ ci⊢ False
  simp only [not_le] at hnF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0⊢ False
  have hF1 := hF.2.2.2F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0hF1:F.numAntiChiralD = 0⊢ False
  simp [numAntiChiralD] at hF1F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum = 0⊢ False
  have h1 := Multiset.sum_le_card_nsmul
    (Multiset.filter (fun x => x < 0) F.chiralIndicesOfD) (-1)
    (fun x hx => byF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum = 0x:ℤhx:x ∈ Multiset.filter (fun x => x < 0) F.chiralIndicesOfD⊢ x ≤ -1F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).card • -1⊢ False
      have := (Multiset.mem_filter.mp hx).2F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum = 0x:ℤhx:x ∈ Multiset.filter (fun x => x < 0) F.chiralIndicesOfDthis:x < 0⊢ x ≤ -1F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).card • -1⊢ False
      omegaAll goals completed! 🐙F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).card • -1⊢ False)F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).card • -1⊢ False
  rw [nsmul_eq_mulF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).card * -1⊢ FalseF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).card * -1⊢ False] at h1F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).card * -1⊢ False
  have h2 : 0 < Multiset.card (Multiset.filter (fun x => x < 0) F.chiralIndicesOfD) :=
    Multiset.card_pos_iff_exists_mem.mpr ⟨ci, Multiset.mem_filter.mpr ⟨hci, hn⟩⟩F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).card * -1h2:0 < (Multiset.filter (fun x => x < 0) F.chiralIndicesOfD).card⊢ False
  omegaAll goals completed! 🐙

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


lemma FluxesFive.chiralIndicesOfL_noneg_of_noExotics (F : FluxesFive) (hF : NoExotics F)
    (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfL) : 0 ≤ ci := byF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfL⊢ 0 ≤ ci
  by_contra hnF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:¬0 ≤ ci⊢ False
  simp only [not_le] at hnF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0⊢ False
  have hF1 := hF.2.1F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0hF1:F.numAntiChiralL = 0⊢ False
  simp [numAntiChiralL] at hF1F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum = 0⊢ False
  have h1 := Multiset.sum_le_card_nsmul
    (Multiset.filter (fun x => x < 0) F.chiralIndicesOfL) (-1)
    (fun x hx => byF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum = 0x:ℤhx:x ∈ Multiset.filter (fun x => x < 0) F.chiralIndicesOfL⊢ x ≤ -1F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).card • -1⊢ False
      have := (Multiset.mem_filter.mp hx).2F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum = 0x:ℤhx:x ∈ Multiset.filter (fun x => x < 0) F.chiralIndicesOfLthis:x < 0⊢ x ≤ -1F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).card • -1⊢ False
      omegaAll goals completed! 🐙F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).card • -1⊢ False)F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).card • -1⊢ False
  rw [nsmul_eq_mulF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).card * -1⊢ FalseF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).card * -1⊢ False] at h1F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).card * -1⊢ False
  have h2 : 0 < Multiset.card (Multiset.filter (fun x => x < 0) F.chiralIndicesOfL) :=
    Multiset.card_pos_iff_exists_mem.mpr ⟨ci, Multiset.mem_filter.mpr ⟨hci, hn⟩⟩F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).card * -1h2:0 < (Multiset.filter (fun x => x < 0) F.chiralIndicesOfL).card⊢ False
  omegaAll goals completed! 🐙

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


lemma FluxesTen.chiralIndicesOfQ_noneg_of_noExotics (F : FluxesTen) (hF : NoExotics F)
    (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfQ) : 0 ≤ ci := byF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQ⊢ 0 ≤ ci
  by_contra hnF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:¬0 ≤ ci⊢ False
  simp only [not_le] at hnF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0⊢ False
  have hF1 := hF.2.1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0hF1:F.numAntiChiralQ = 0⊢ False
  simp [numAntiChiralQ] at hF1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum = 0⊢ False
  have h1 := Multiset.sum_le_card_nsmul
    (Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ) (-1)
    (fun x hx => byF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum = 0x:ℤhx:x ∈ Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ⊢ x ≤ -1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).card • -1⊢ False
      have := (Multiset.mem_filter.mp hx).2F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum = 0x:ℤhx:x ∈ Multiset.filter (fun x => x < 0) F.chiralIndicesOfQthis:x < 0⊢ x ≤ -1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).card • -1⊢ False
      omegaAll goals completed! 🐙F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).card • -1⊢ False)F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).card • -1⊢ False
  rw [nsmul_eq_mulF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).card * -1⊢ FalseF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).card * -1⊢ False] at h1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).card * -1⊢ False
  have h2 : 0 < Multiset.card (Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ) :=
    Multiset.card_pos_iff_exists_mem.mpr ⟨ci, Multiset.mem_filter.mpr ⟨hci, hn⟩⟩F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).card * -1h2:0 < (Multiset.filter (fun x => x < 0) F.chiralIndicesOfQ).card⊢ False
  omegaAll goals completed! 🐙

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.


lemma FluxesTen.chiralIndicesOfU_noneg_of_noExotics (F : FluxesTen) (hF : NoExotics F)
    (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfU) : 0 ≤ ci := byF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfU⊢ 0 ≤ ci
  by_contra hnF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:¬0 ≤ ci⊢ False
  simp only [not_le] at hnF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0⊢ False
  have hF1 := hF.2.2.2F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0hF1:F.numAntiChiralU = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0⊢ False
  simp [numAntiChiralU] at hF1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0⊢ False
  have h1 := Multiset.sum_le_card_nsmul
    (Multiset.filter (fun x => x < 0) F.chiralIndicesOfU) (-1)
    (fun x hx => byF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0x:ℤhx:x ∈ Multiset.filter (fun x => x < 0) F.chiralIndicesOfU⊢ x ≤ -1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).card • -1⊢ False
      have := (Multiset.mem_filter.mp hx).2F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0x:ℤhx:x ∈ Multiset.filter (fun x => x < 0) F.chiralIndicesOfUthis:x < 0⊢ x ≤ -1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).card • -1⊢ False
      omegaAll goals completed! 🐙F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).card • -1⊢ False)F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).card • -1⊢ False
  rw [nsmul_eq_mulF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).card * -1⊢ FalseF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).card * -1⊢ False] at h1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).card * -1⊢ False
  have h2 : 0 < Multiset.card (Multiset.filter (fun x => x < 0) F.chiralIndicesOfU) :=
    Multiset.card_pos_iff_exists_mem.mpr ⟨ci, Multiset.mem_filter.mpr ⟨hci, hn⟩⟩F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum = 0 ∧ F.numChiralE = 3 ∧ F.numAntiChiralE = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).card * -1h2:0 < (Multiset.filter (fun x => x < 0) F.chiralIndicesOfU).card⊢ False
  omegaAll goals completed! 🐙



lemma FluxesTen.chiralIndicesOfE_noneg_of_noExotics (F : FluxesTen) (hF : NoExotics F)
    (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfE) : 0 ≤ ci := byF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfE⊢ 0 ≤ ci
  by_contra hnF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:¬0 ≤ ci⊢ False
  simp only [not_le] at hnF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0⊢ False
  have hF1 := hF.2.2.2.2.2F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0hF1:F.numAntiChiralE = 0⊢ False
  simp [numAntiChiralE] at hF1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum = 0⊢ False
  have h1 := Multiset.sum_le_card_nsmul
    (Multiset.filter (fun x => x < 0) F.chiralIndicesOfE) (-1)
    (fun x hx => byF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum = 0x:ℤhx:x ∈ Multiset.filter (fun x => x < 0) F.chiralIndicesOfE⊢ x ≤ -1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).card • -1⊢ False
      have := (Multiset.mem_filter.mp hx).2F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum = 0x:ℤhx:x ∈ Multiset.filter (fun x => x < 0) F.chiralIndicesOfEthis:x < 0⊢ x ≤ -1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).card • -1⊢ False
      omegaAll goals completed! 🐙F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).card • -1⊢ False)F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum ≤
  (Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).card • -1⊢ False
  rw [nsmul_eq_mulF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).card * -1⊢ FalseF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).card * -1⊢ False] at h1F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).card * -1⊢ False
  have h2 : 0 < Multiset.card (Multiset.filter (fun x => x < 0) F.chiralIndicesOfE) :=
    Multiset.card_pos_iff_exists_mem.mpr ⟨ci, Multiset.mem_filter.mpr ⟨hci, hn⟩⟩F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhn:ci < 0hF1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum = 0h1:(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).sum ≤
  ↑(Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).card * -1h2:0 < (Multiset.filter (fun x => x < 0) F.chiralIndicesOfE).card⊢ False
  omegaAll goals completed! 🐙

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.

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.


lemma FluxesFive.chiralIndicesOfD_sum_eq_three_of_noExotics (F : FluxesFive) (hF : NoExotics F) :
    F.chiralIndicesOfD.sum = 3 := byF:FluxesFivehF:F.NoExotics⊢ F.chiralIndicesOfD.sum = 3
  have h := F.numChiralD_eq_sum_sub_numAntiChiralDF:FluxesFivehF:F.NoExoticsh:F.numChiralD = F.chiralIndicesOfD.sum - F.numAntiChiralD⊢ F.chiralIndicesOfD.sum = 3
  rw [hF.2.2.2,F:FluxesFivehF:F.NoExoticsh:F.numChiralD = F.chiralIndicesOfD.sum - 0⊢ F.chiralIndicesOfD.sum = 3F:FluxesFivehF:F.NoExoticsh:3 = F.chiralIndicesOfD.sum - 0⊢ F.chiralIndicesOfD.sum = 3 hF.2.2.1F:FluxesFivehF:F.NoExoticsh:3 = F.chiralIndicesOfD.sum - 0⊢ F.chiralIndicesOfD.sum = 3F:FluxesFivehF:F.NoExoticsh:3 = F.chiralIndicesOfD.sum - 0⊢ F.chiralIndicesOfD.sum = 3] at hF:FluxesFivehF:F.NoExoticsh:3 = F.chiralIndicesOfD.sum - 0⊢ F.chiralIndicesOfD.sum = 3
  omegaAll goals completed! 🐙

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


lemma FluxesFive.chiralIndicesOfL_sum_eq_three_of_noExotics (F : FluxesFive) (hF : NoExotics F) :
    F.chiralIndicesOfL.sum = 3 := byF:FluxesFivehF:F.NoExotics⊢ F.chiralIndicesOfL.sum = 3
  have h := F.numChiralL_eq_sum_sub_numAntiChiralLF:FluxesFivehF:F.NoExoticsh:F.numChiralL = F.chiralIndicesOfL.sum - F.numAntiChiralL⊢ F.chiralIndicesOfL.sum = 3
  rw [hF.2.1,F:FluxesFivehF:F.NoExoticsh:F.numChiralL = F.chiralIndicesOfL.sum - 0⊢ F.chiralIndicesOfL.sum = 3F:FluxesFivehF:F.NoExoticsh:3 = F.chiralIndicesOfL.sum - 0⊢ F.chiralIndicesOfL.sum = 3 hF.1F:FluxesFivehF:F.NoExoticsh:3 = F.chiralIndicesOfL.sum - 0⊢ F.chiralIndicesOfL.sum = 3F:FluxesFivehF:F.NoExoticsh:3 = F.chiralIndicesOfL.sum - 0⊢ F.chiralIndicesOfL.sum = 3] at hF:FluxesFivehF:F.NoExoticsh:3 = F.chiralIndicesOfL.sum - 0⊢ F.chiralIndicesOfL.sum = 3
  omegaAll goals completed! 🐙

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


lemma FluxesTen.chiralIndicesOfQ_sum_eq_three_of_noExotics (F : FluxesTen) (hF : NoExotics F) :
    F.chiralIndicesOfQ.sum = 3 := byF:FluxesTenhF:F.NoExotics⊢ F.chiralIndicesOfQ.sum = 3
  have h := F.numChiralQ_eq_sum_sub_numAntiChiralQF:FluxesTenhF:F.NoExoticsh:F.numChiralQ = F.chiralIndicesOfQ.sum - F.numAntiChiralQ⊢ F.chiralIndicesOfQ.sum = 3
  rw [hF.2.1,F:FluxesTenhF:F.NoExoticsh:F.numChiralQ = F.chiralIndicesOfQ.sum - 0⊢ F.chiralIndicesOfQ.sum = 3F:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfQ.sum - 0⊢ F.chiralIndicesOfQ.sum = 3 hF.1F:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfQ.sum - 0⊢ F.chiralIndicesOfQ.sum = 3F:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfQ.sum - 0⊢ F.chiralIndicesOfQ.sum = 3] at hF:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfQ.sum - 0⊢ F.chiralIndicesOfQ.sum = 3
  omegaAll goals completed! 🐙

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.


lemma FluxesTen.chiralIndicesOfU_sum_eq_three_of_noExotics (F : FluxesTen) (hF : NoExotics F) :
    F.chiralIndicesOfU.sum = 3 := byF:FluxesTenhF:F.NoExotics⊢ F.chiralIndicesOfU.sum = 3
  have h := F.numChiralU_eq_sum_sub_numAntiChiralUF:FluxesTenhF:F.NoExoticsh:F.numChiralU = F.chiralIndicesOfU.sum - F.numAntiChiralU⊢ F.chiralIndicesOfU.sum = 3
  rw [hF.2.2.2.1,F:FluxesTenhF:F.NoExoticsh:F.numChiralU = F.chiralIndicesOfU.sum - 0⊢ F.chiralIndicesOfU.sum = 3F:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfU.sum - 0⊢ F.chiralIndicesOfU.sum = 3 hF.2.2.1F:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfU.sum - 0⊢ F.chiralIndicesOfU.sum = 3F:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfU.sum - 0⊢ F.chiralIndicesOfU.sum = 3] at hF:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfU.sum - 0⊢ F.chiralIndicesOfU.sum = 3
  omegaAll goals completed! 🐙

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


lemma FluxesTen.chiralIndicesOfE_sum_eq_three_of_noExotics (F : FluxesTen) (hF : NoExotics F) :
    F.chiralIndicesOfE.sum = 3 := byF:FluxesTenhF:F.NoExotics⊢ F.chiralIndicesOfE.sum = 3
  have h := F.numChiralE_eq_sum_sub_numAntiChiralEF:FluxesTenhF:F.NoExoticsh:F.numChiralE = F.chiralIndicesOfE.sum - F.numAntiChiralE⊢ F.chiralIndicesOfE.sum = 3
  rw [hF.2.2.2.2.1,F:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfE.sum - F.numAntiChiralE⊢ F.chiralIndicesOfE.sum = 3F:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfE.sum - 0⊢ F.chiralIndicesOfE.sum = 3 hF.2.2.2.2.2F:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfE.sum - 0⊢ F.chiralIndicesOfE.sum = 3F:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfE.sum - 0⊢ F.chiralIndicesOfE.sum = 3] at hF:FluxesTenhF:F.NoExoticsh:3 = F.chiralIndicesOfE.sum - 0⊢ F.chiralIndicesOfE.sum = 3
  omegaAll goals completed! 🐙

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

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

lemma FluxesFive.chiralIndicesOfD_le_three_of_noExotics (F : FluxesFive) (hF : NoExotics F)
    (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfD) : ci ≤ 3 := byF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfD⊢ ci ≤ 3
  have hle := Multiset.single_le_sum
    (fun x hx => chiralIndicesOfD_noneg_of_noExotics F hF x hx) ci hciF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhle:ci ≤ F.chiralIndicesOfD.sum⊢ ci ≤ 3
  rwa [F.chiralIndicesOfD_sum_eq_three_of_noExotics hFF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhle:ci ≤ 3⊢ ci ≤ 3]F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDhle:ci ≤ 3⊢ ci ≤ 3 at hle

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

lemma FluxesFive.chiralIndicesOfL_le_three_of_noExotics (F : FluxesFive) (hF : NoExotics F)
    (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfL) : ci ≤ 3 := byF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfL⊢ ci ≤ 3
  have hle := Multiset.single_le_sum
    (fun x hx => chiralIndicesOfL_noneg_of_noExotics F hF x hx) ci hciF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhle:ci ≤ F.chiralIndicesOfL.sum⊢ ci ≤ 3
  rwa [F.chiralIndicesOfL_sum_eq_three_of_noExotics hFF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhle:ci ≤ 3⊢ ci ≤ 3]F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLhle:ci ≤ 3⊢ ci ≤ 3 at hle

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

lemma FluxesTen.chiralIndicesOfQ_le_three_of_noExotics (F : FluxesTen) (hF : NoExotics F)
    (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfQ) : ci ≤ 3 := byF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQ⊢ ci ≤ 3
  have hle := Multiset.single_le_sum
    (fun x hx => chiralIndicesOfQ_noneg_of_noExotics F hF x hx) ci hciF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhle:ci ≤ F.chiralIndicesOfQ.sum⊢ ci ≤ 3
  rwa [F.chiralIndicesOfQ_sum_eq_three_of_noExotics hFF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhle:ci ≤ 3⊢ ci ≤ 3]F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQhle:ci ≤ 3⊢ ci ≤ 3 at hle

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

lemma FluxesTen.chiralIndicesOfU_le_three_of_noExotics (F : FluxesTen) (hF : NoExotics F)
    (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfU) : ci ≤ 3 := byF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfU⊢ ci ≤ 3
  have hle := Multiset.single_le_sum
    (fun x hx => chiralIndicesOfU_noneg_of_noExotics F hF x hx) ci hciF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhle:ci ≤ F.chiralIndicesOfU.sum⊢ ci ≤ 3
  rwa [F.chiralIndicesOfU_sum_eq_three_of_noExotics hFF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhle:ci ≤ 3⊢ ci ≤ 3]F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUhle:ci ≤ 3⊢ ci ≤ 3 at hle

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 := byF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfE⊢ ci ≤ 3
  have hle := Multiset.single_le_sum
    (fun x hx => chiralIndicesOfE_noneg_of_noExotics F hF x hx) ci hciF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhle:ci ≤ F.chiralIndicesOfE.sum⊢ ci ≤ 3
  rwa [F.chiralIndicesOfE_sum_eq_three_of_noExotics hFF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhle:ci ≤ 3⊢ ci ≤ 3]F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEhle:ci ≤ 3⊢ ci ≤ 3 at hle

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

              lemma FluxesFive.mem_chiralIndicesOfD_mem_of_noExotics (F : FluxesFive)
    (hF : NoExotics F) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfD) :
    ci ∈ ({0, 1, 2, 3} : Finset ℤ) := byF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfD⊢ ci ∈ {0, 1, 2, 3}
  have h0 := F.chiralIndicesOfD_le_three_of_noExotics hF ci hciF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDh0:ci ≤ 3⊢ ci ∈ {0, 1, 2, 3}
  have h1 := chiralIndicesOfD_noneg_of_noExotics F hF ci hciF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDh0:ci ≤ 3h1:0 ≤ ci⊢ ci ∈ {0, 1, 2, 3}
  simp only [Finset.mem_insert, Finset.mem_singleton]F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfDh0:ci ≤ 3h1:0 ≤ ci⊢ ci = 0 ∨ ci = 1 ∨ ci = 2 ∨ ci = 3
  omegaAll goals completed! 🐙lemma FluxesFive.mem_chiralIndicesOfL_mem_of_noExotics (F : FluxesFive)
    (hF : NoExotics F) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfL) :
    ci ∈ ({0, 1, 2, 3} : Finset ℤ) := byF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfL⊢ ci ∈ {0, 1, 2, 3}
  have h0 := F.chiralIndicesOfL_le_three_of_noExotics hF ci hciF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLh0:ci ≤ 3⊢ ci ∈ {0, 1, 2, 3}
  have h1 := chiralIndicesOfL_noneg_of_noExotics F hF ci hciF:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLh0:ci ≤ 3h1:0 ≤ ci⊢ ci ∈ {0, 1, 2, 3}
  simp only [Finset.mem_insert, Finset.mem_singleton]F:FluxesFivehF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfLh0:ci ≤ 3h1:0 ≤ ci⊢ ci = 0 ∨ ci = 1 ∨ ci = 2 ∨ ci = 3
  omegaAll goals completed! 🐙lemma FluxesTen.mem_chiralIndicesOfQ_mem_of_noExotics (F : FluxesTen)
    (hF : NoExotics F) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfQ) :
    ci ∈ ({0, 1, 2, 3} : Finset ℤ) := byF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQ⊢ ci ∈ {0, 1, 2, 3}
  have h0 := F.chiralIndicesOfQ_le_three_of_noExotics hF ci hciF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQh0:ci ≤ 3⊢ ci ∈ {0, 1, 2, 3}
  have h1 := chiralIndicesOfQ_noneg_of_noExotics F hF ci hciF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQh0:ci ≤ 3h1:0 ≤ ci⊢ ci ∈ {0, 1, 2, 3}
  simp only [Finset.mem_insert, Finset.mem_singleton]F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfQh0:ci ≤ 3h1:0 ≤ ci⊢ ci = 0 ∨ ci = 1 ∨ ci = 2 ∨ ci = 3
  omegaAll goals completed! 🐙lemma FluxesTen.mem_chiralIndicesOfU_mem_of_noExotics (F : FluxesTen)
    (hF : NoExotics F) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfU) :
    ci ∈ ({0, 1, 2, 3} : Finset ℤ) := byF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfU⊢ ci ∈ {0, 1, 2, 3}
  have h0 := F.chiralIndicesOfU_le_three_of_noExotics hF ci hciF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUh0:ci ≤ 3⊢ ci ∈ {0, 1, 2, 3}
  have h1 := chiralIndicesOfU_noneg_of_noExotics F hF ci hciF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUh0:ci ≤ 3h1:0 ≤ ci⊢ ci ∈ {0, 1, 2, 3}
  simp only [Finset.mem_insert, Finset.mem_singleton]F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfUh0:ci ≤ 3h1:0 ≤ ci⊢ ci = 0 ∨ ci = 1 ∨ ci = 2 ∨ ci = 3
  omegaAll goals completed! 🐙lemma FluxesTen.mem_chiralIndicesOfE_mem_of_noExotics (F : FluxesTen)
    (hF : NoExotics F) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfE) :
    ci ∈ ({0, 1, 2, 3} : Finset ℤ) := byF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfE⊢ ci ∈ {0, 1, 2, 3}
  have h0 := F.chiralIndicesOfE_le_three_of_noExotics hF ci hciF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEh0:ci ≤ 3⊢ ci ∈ {0, 1, 2, 3}
  have h1 := chiralIndicesOfE_noneg_of_noExotics F hF ci hciF:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEh0:ci ≤ 3h1:0 ≤ ci⊢ ci ∈ {0, 1, 2, 3}
  simp only [Finset.mem_insert, Finset.mem_singleton]F:FluxesTenhF:F.NoExoticsci:ℤhci:ci ∈ F.chiralIndicesOfEh0:ci ≤ 3h1:0 ≤ ci⊢ ci = 0 ∨ ci = 1 ∨ ci = 2 ∨ ci = 3
  omegaAll goals completed! 🐙

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

              

lemma FluxesFive.chiralIndicesOfD_subset_sum_le_three_of_noExotics (F : FluxesFive)
    (hF : NoExotics F) (S : Multiset Fluxes)
    (hSle : S ≤ F) : (S.map (fun x => x.1)).sum ≤ 3 := byF:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ F⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3
  have hs : S.map (fun x => x.1) ≤ F.chiralIndicesOfD := Multiset.map_le_map hSleF:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfD⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3
  have hpos : 0 ≤ (F.chiralIndicesOfD - S.map (fun x => x.1)).sum :=
    Multiset.sum_nonneg fun x hx =>
      chiralIndicesOfD_noneg_of_noExotics F hF x (Multiset.mem_of_le tsub_le_self hx)F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfDhpos:0 ≤ (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sum⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3
  have sum_add_compl_eq_three : (S.map (fun x => x.1)).sum +
      (F.chiralIndicesOfD - S.map (fun x => x.1)).sum = 3 := by
    rw [← Multiset.sum_add,F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfDhpos:0 ≤ (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sum⊢ (Multiset.map (fun x => x.M) S + (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S)).sum = 3F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfDhpos:0 ≤ (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M) S).sum + (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sum = 3⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3 add_tsub_cancel_of_le hs,F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfDhpos:0 ≤ (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sum⊢ F.chiralIndicesOfD.sum = 3F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfDhpos:0 ≤ (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M) S).sum + (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sum = 3⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3
      F.chiralIndicesOfD_sum_eq_three_of_noExotics hFF:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfDhpos:0 ≤ (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sum⊢ 3 = 3F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfDhpos:0 ≤ (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M) S).sum + (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sum = 3⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3]F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfDhpos:0 ≤ (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M) S).sum + (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sum = 3⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfDhpos:0 ≤ (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M) S).sum + (F.chiralIndicesOfD - Multiset.map (fun x => x.M) S).sum = 3⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3
  omegaAll goals completed! 🐙

lemma FluxesFive.chiralIndicesOfL_subset_sum_le_three_of_noExotics (F : FluxesFive)
    (hF : NoExotics F) (S : Multiset Fluxes)
    (hSle : S ≤ F) : (S.map (fun x => (x.1 + x.2))).sum ≤ 3 := byF:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ F⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3
  have hs : S.map (fun x => (x.1 + x.2)) ≤ F.chiralIndicesOfL := Multiset.map_le_map hSleF:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfL⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3
  have hpos : 0 ≤ (F.chiralIndicesOfL - S.map (fun x => (x.1 + x.2))).sum :=
    Multiset.sum_nonneg fun x hx =>
      chiralIndicesOfL_noneg_of_noExotics F hF x (Multiset.mem_of_le tsub_le_self hx)F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfLhpos:0 ≤ (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sum⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3
  have sum_add_compl_eq_three : (S.map (fun x => (x.1 + x.2))).sum +
      (F.chiralIndicesOfL - S.map (fun x => (x.1 + x.2))).sum = 3 := by
    rw [← Multiset.sum_add,F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfLhpos:0 ≤ (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sum⊢ (Multiset.map (fun x => x.M + x.N) S + (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S)).sum = 3F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfLhpos:0 ≤ (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M + x.N) S).sum + (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3 add_tsub_cancel_of_le hs,F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfLhpos:0 ≤ (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sum⊢ F.chiralIndicesOfL.sum = 3F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfLhpos:0 ≤ (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M + x.N) S).sum + (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3
      F.chiralIndicesOfL_sum_eq_three_of_noExotics hFF:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfLhpos:0 ≤ (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sum⊢ 3 = 3F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfLhpos:0 ≤ (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M + x.N) S).sum + (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3]F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfLhpos:0 ≤ (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M + x.N) S).sum + (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3F:FluxesFivehF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfLhpos:0 ≤ (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M + x.N) S).sum + (F.chiralIndicesOfL - Multiset.map (fun x => x.M + x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3
  omegaAll goals completed! 🐙

lemma FluxesTen.chiralIndicesOfQ_subset_sum_le_three_of_noExotics (F : FluxesTen)
    (hF : NoExotics F) (S : Multiset Fluxes)
    (hSle : S ≤ F) : (S.map (fun x => x.1)).sum ≤ 3 := byF:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ F⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3
  have hs : S.map (fun x => x.1) ≤ F.chiralIndicesOfQ := Multiset.map_le_map hSleF:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfQ⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3
  have hpos : 0 ≤ (F.chiralIndicesOfQ - S.map (fun x => x.1)).sum :=
    Multiset.sum_nonneg fun x hx =>
      chiralIndicesOfQ_noneg_of_noExotics F hF x (Multiset.mem_of_le tsub_le_self hx)F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfQhpos:0 ≤ (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sum⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3
  have sum_add_compl_eq_three : (S.map (fun x => x.1)).sum +
      (F.chiralIndicesOfQ - S.map (fun x => x.1)).sum = 3 := by
    rw [← Multiset.sum_add,F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfQhpos:0 ≤ (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sum⊢ (Multiset.map (fun x => x.M) S + (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S)).sum = 3F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfQhpos:0 ≤ (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M) S).sum + (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sum = 3⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3 add_tsub_cancel_of_le hs,F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfQhpos:0 ≤ (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sum⊢ F.chiralIndicesOfQ.sum = 3F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfQhpos:0 ≤ (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M) S).sum + (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sum = 3⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3
      F.chiralIndicesOfQ_sum_eq_three_of_noExotics hFF:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfQhpos:0 ≤ (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sum⊢ 3 = 3F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfQhpos:0 ≤ (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M) S).sum + (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sum = 3⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3]F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfQhpos:0 ≤ (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M) S).sum + (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sum = 3⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M) S ≤ F.chiralIndicesOfQhpos:0 ≤ (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M) S).sum + (F.chiralIndicesOfQ - Multiset.map (fun x => x.M) S).sum = 3⊢ (Multiset.map (fun x => x.M) S).sum ≤ 3
  omegaAll goals completed! 🐙

lemma FluxesTen.chiralIndicesOfU_subset_sum_le_three_of_noExotics (F : FluxesTen)
    (hF : NoExotics F) (S : Multiset Fluxes)
    (hSle : S ≤ F) : (S.map (fun x => (x.1 - x.2))).sum ≤ 3 := byF:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ F⊢ (Multiset.map (fun x => x.M - x.N) S).sum ≤ 3
  have hs : S.map (fun x => (x.1 - x.2)) ≤ F.chiralIndicesOfU := Multiset.map_le_map hSleF:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M - x.N) S ≤ F.chiralIndicesOfU⊢ (Multiset.map (fun x => x.M - x.N) S).sum ≤ 3
  have hpos : 0 ≤ (F.chiralIndicesOfU - S.map (fun x => (x.1 - x.2))).sum :=
    Multiset.sum_nonneg fun x hx =>
      chiralIndicesOfU_noneg_of_noExotics F hF x (Multiset.mem_of_le tsub_le_self hx)F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M - x.N) S ≤ F.chiralIndicesOfUhpos:0 ≤ (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sum⊢ (Multiset.map (fun x => x.M - x.N) S).sum ≤ 3
  have sum_add_compl_eq_three : (S.map (fun x => (x.1 - x.2))).sum +
      (F.chiralIndicesOfU - S.map (fun x => (x.1 - x.2))).sum = 3 := by
    rw [← Multiset.sum_add,F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M - x.N) S ≤ F.chiralIndicesOfUhpos:0 ≤ (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sum⊢ (Multiset.map (fun x => x.M - x.N) S + (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S)).sum = 3F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M - x.N) S ≤ F.chiralIndicesOfUhpos:0 ≤ (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M - x.N) S).sum + (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M - x.N) S).sum ≤ 3 add_tsub_cancel_of_le hs,F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M - x.N) S ≤ F.chiralIndicesOfUhpos:0 ≤ (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sum⊢ F.chiralIndicesOfU.sum = 3F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M - x.N) S ≤ F.chiralIndicesOfUhpos:0 ≤ (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M - x.N) S).sum + (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M - x.N) S).sum ≤ 3
      F.chiralIndicesOfU_sum_eq_three_of_noExotics hFF:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M - x.N) S ≤ F.chiralIndicesOfUhpos:0 ≤ (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sum⊢ 3 = 3F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M - x.N) S ≤ F.chiralIndicesOfUhpos:0 ≤ (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M - x.N) S).sum + (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M - x.N) S).sum ≤ 3]F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M - x.N) S ≤ F.chiralIndicesOfUhpos:0 ≤ (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M - x.N) S).sum + (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M - x.N) S).sum ≤ 3F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M - x.N) S ≤ F.chiralIndicesOfUhpos:0 ≤ (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M - x.N) S).sum + (F.chiralIndicesOfU - Multiset.map (fun x => x.M - x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M - x.N) S).sum ≤ 3
  omegaAll goals completed! 🐙

lemma FluxesTen.chiralIndicesOfE_subset_sum_le_three_of_noExotics (F : FluxesTen)
    (hF : NoExotics F) (S : Multiset Fluxes)
    (hSle : S ≤ F) : (S.map (fun x => (x.1 + x.2))).sum ≤ 3 := byF:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ F⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3
  have hs : S.map (fun x => (x.1 + x.2)) ≤ F.chiralIndicesOfE := Multiset.map_le_map hSleF:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfE⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3
  have hpos : 0 ≤ (F.chiralIndicesOfE - S.map (fun x => (x.1 + x.2))).sum :=
    Multiset.sum_nonneg fun x hx =>
      chiralIndicesOfE_noneg_of_noExotics F hF x (Multiset.mem_of_le tsub_le_self hx)F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfEhpos:0 ≤ (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sum⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3
  have sum_add_compl_eq_three : (S.map (fun x => (x.1 + x.2))).sum +
      (F.chiralIndicesOfE - S.map (fun x => (x.1 + x.2))).sum = 3 := by
    rw [← Multiset.sum_add,F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfEhpos:0 ≤ (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sum⊢ (Multiset.map (fun x => x.M + x.N) S + (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S)).sum = 3F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfEhpos:0 ≤ (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M + x.N) S).sum + (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3 add_tsub_cancel_of_le hs,F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfEhpos:0 ≤ (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sum⊢ F.chiralIndicesOfE.sum = 3F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfEhpos:0 ≤ (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M + x.N) S).sum + (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3
      F.chiralIndicesOfE_sum_eq_three_of_noExotics hFF:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfEhpos:0 ≤ (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sum⊢ 3 = 3F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfEhpos:0 ≤ (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M + x.N) S).sum + (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3]F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfEhpos:0 ≤ (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M + x.N) S).sum + (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3F:FluxesTenhF:F.NoExoticsS:Multiset FluxeshSle:S ≤ Fhs:Multiset.map (fun x => x.M + x.N) S ≤ F.chiralIndicesOfEhpos:0 ≤ (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sumsum_add_compl_eq_three:(Multiset.map (fun x => x.M + x.N) S).sum + (F.chiralIndicesOfE - Multiset.map (fun x => x.M + x.N) S).sum = 3⊢ (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3
  omegaAll goals completed! 🐙