Research proof index

The reduce of FiveQuanta is a new FiveQuanta with all the fluxes corresponding to the same charge (i.e. representation) added together. -/ def reduce (x : FiveQuanta 𝓩) : FiveQuanta 𝓩 := x.toCharges.dedup.map fun q5 => (q5, ((x.filter (fun f => f.1 = q5)).map (fun y => y.2)).sum) /-! ### B.1. The reduced FiveQuanta has no duplicate elements -/ l...

Given a finite set of charges c the FiveQuanta which do not have exotics, duplicate charges or zero fluxes, which map down to c. -/ def liftCharge (c : Finset 𝓩) : Multiset (FiveQuanta 𝓩) := /- The multisets of cardinality 3 containing 3 elements of c. -/ let S53 : Multiset (Multiset 𝓩) := toMultisetsThree c /- Pairs of multisets (s1, s2) such...

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...