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.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.OfFinset public import Physlib.StringTheory.FTheory.SU5.Fluxes.NoExotics.Completeness

Quanta of 5-d representations

i. Overview

The 5-bar representations of the SU(5)Γ—U(1) carry the quantum numbers of their U(1) charges and their fluxes.

In this module we define the data structure for these quanta and properties thereof.

ii. Key results

    FiveQuanta is the type of quanta of 5-bar representations.

    FiveQuanta.toFluxesFive is the underlying FluxesFive of a FiveQuanta.

    FiveQuanta.toCharges is the underlying Multiset charges of a FiveQuanta.

    FiveQuanta.reduce is the reduction of a FiveQuanta which adds together all the fluxes corresponding to the same charge (i.e. representation).

    FiveQuanta.liftCharges given a charge c the FiveQuanta which have charge c and no exotics or zero fluxes.

    FiveQuanta.anomalyCoefficient is the anomaly coefficient associated with a FiveQuanta.

iii. Table of contents

    A. The definition of FiveQuanta

      A.1. The map to underlying fluxes

      A.2. The map to underlying charges

      A.3. The map from charges to fluxes

    B. The reduction of a FiveQuanta

      B.1. The reduced FiveQuanta has no duplicate elements

      B.2. The underlying charges of the reduced FiveQuanta are the deduped charges

      B.3. Membership condition on the reduced FiveQuanta

      B.4. Filter of the reduced FiveQuanta by a charge

      B.5. The reduction is idempotent

      B.6. Preservation of certain sums under reduction

      B.7. Reduction does nothing if no duplicate charges

      B.8. The charge map is preserved by reduction

      B.9. A fluxes in the reduced FiveQuanta is a sum of fluxes in the original FiveQuanta

      B.10. No exotics condition on the reduced FiveQuanta

        B.10.1. Number of chiral L

        B.10.2. Number of anti-chiral L

        B.10.3. Number of chiral D

        B.10.4. Number of anti-chiral D

        B.10.5. The NoExotics condition on the reduced FiveQuanta

      B.11. Reduce member of FluxesFive.elemsNoExotics

    C. Decomposition of a FiveQuanta into basic fluxes

      C.1. Decomposition of fluxes

      C.2. Decomposition of a FiveQuanta (with no exotics)

        C.2.1. Decomposition distributes over addition

        C.2.2. Decomposition commutes with filtering charges

        C.2.3. Decomposition preserves the charge map

        C.2.4. Decomposition preserves the charges

        C.2.5. Decomposition preserves the reduction

        C.2.6. Fluxes of the decomposition of a FiveQuanta

    D. Lifting charges to FiveQuanta

      D.1. liftCharge c: multiset of five-quanta for a finite set of charges c with no exotics

      D.2. FiveQuanta in liftCharge c have a finite set of charges c

      D.3. FiveQuanta in liftCharge c have no duplicate charges

      D.4. Membership in liftCharge c iff is reduction of FiveQuanta with given fluxes

      D.5. FiveQuanta in liftCharge c do not have zero fluxes

      D.6. FiveQuanta in liftCharge c have no exotics

      D.7. Membership in liftCharge c iff have no exotics, no zero fluxes, and charges c

      D.8. liftCharge c is preserved under a map if reduced

    E. Anomaly cancellation coefficients

      E.1. Anomaly coefficients of a FiveQuanta

      E.2. Anomaly coefficients under a map

      E.3. Anomaly coefficients is preserved under reduce

iv. References

A reference for the anomaly cancellation conditions is arXiv:1401.5084.

@[expose] public section

A. The definition of FiveQuanta

The quanta of 5-bar representations corresponding to a multiset of (q, M, N) for each particle. (M, N) are defined in the FluxesFive module.

abbrev FiveQuanta (𝓩 : Type := β„€) : Type := Multiset (𝓩 Γ— Fluxes)

A.1. The map to underlying fluxes

The underlying FluxesFive from a FiveQuanta.

def toFluxesFive (x : FiveQuanta 𝓩) : FluxesFive := x.map Prod.snd

A.2. The map to underlying charges

The underlying Multiset charges from a FiveQuanta.

def toCharges (x : FiveQuanta 𝓩) : Multiset 𝓩 := x.map Prod.fst

A.3. The map from charges to fluxes

The map which takes a charge to the overall flux it corresponds to in a FiveQuanta.

def toChargeMap [DecidableEq 𝓩] (x : FiveQuanta 𝓩) : 𝓩 β†’ Fluxes := fun z => ((x.filter fun p => p.1 = z).map Prod.snd).sum
𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩z:𝓩h:z βˆ‰ x.toChargeshl:Multiset.filter (fun p => p.1 = z) x = 0⊒ x.toChargeMap z = 0 All goals completed! πŸ™

B. The reduction of a FiveQuanta

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

𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta π“©βŠ’ (Multiset.map (fun q5 => (q5, (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = q5) x)).sum)) x.toCharges.dedup).Nodup All goals completed! πŸ™@[simp] lemma reduce_dedup (x : FiveQuanta 𝓩) : x.reduce.dedup = x.reduce := Multiset.Nodup.dedup x.reduce_nodup

B.2. The underlying charges of the reduced FiveQuanta are the deduped charges

lemma reduce_toCharges (x : FiveQuanta 𝓩) : x.reduce.toCharges = x.toCharges.dedup := 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta π“©βŠ’ x.reduce.toCharges = x.toCharges.dedup All goals completed! πŸ™

B.3. Membership condition on the reduced FiveQuanta

lemma mem_reduce_iff (x : FiveQuanta 𝓩) (p : 𝓩 Γ— Fluxes) : p ∈ x.reduce ↔ p.1 ∈ x.toCharges ∧ p.2 = ((x.filter (fun f => f.1 = p.1)).map (fun y => y.2)).sum := 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩p:𝓩 Γ— Fluxes⊒ p ∈ x.reduce ↔ p.1 ∈ x.toCharges ∧ p.2 = (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = p.1) x)).sum 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩p:𝓩 Γ— Fluxes⊒ (βˆƒ a ∈ x.toCharges, (a, (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = a) x)).sum) = p) ↔ p.1 ∈ x.toCharges ∧ p.2 = (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = p.1) x)).sum All goals completed! πŸ™

B.4. Filter of the reduced FiveQuanta by a charge

lemma reduce_filter (x : FiveQuanta 𝓩) (q : 𝓩) (h : q ∈ x.toCharges) : x.reduce.filter (fun f => f.1 = q) = {(q, ((x.filter (fun f => f.1 = q)).map (fun y => y.2)).sum)} := 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩q:𝓩h:q ∈ x.toCharges⊒ Multiset.filter (fun f => f.1 = q) x.reduce = {(q, (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = q) x)).sum)} All goals completed! πŸ™

B.5. The reduction is idempotent

𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩p:𝓩 Γ— Fluxeshp:p.1 ∈ x.toCharges⊒ p.2 = (Multiset.map (fun y => y.2) {(p.1, (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = p.1) x)).sum)}).sum ↔ p.2 = (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = p.1) x)).sum All goals completed! πŸ™

B.6. Preservation of certain sums under reduction

𝓩:Typeinst✝¹:DecidableEq 𝓩M:Type u_1inst✝:AddCommMonoid Mx:FiveQuanta 𝓩f:𝓩 β†’ Fluxes β†’+ Mp:𝓩 Γ— Fluxesh_mem✝:p.1 βˆ‰ Multiset.map Prod.fst xh:p ∈ xh_mem:p.1 ∈ Multiset.map Prod.fst x⊒ False𝓩:Typeinst✝¹:DecidableEq 𝓩M:Type u_1inst✝:AddCommMonoid Mx:FiveQuanta 𝓩f:𝓩 β†’ Fluxes β†’+ Mp:𝓩 Γ— Fluxesh_mem:p.1 βˆ‰ Multiset.map Prod.fst x⊒ βˆ€ x_1 ∈ Multiset.map (fun y => if p.1 = y then Multiset.count p x else 0) (Multiset.map Prod.fst x).dedup, x_1 = 0 (𝓩:Typeinst:DecidableEq 𝓩M:Type u_1inst_1:AddCommMonoid Mx:FiveQuanta 𝓩f:𝓩 β†’ Fluxes β†’+ Mp:𝓩 Γ— Fluxesh_mem_1:p.1 βˆ‰ Multiset.map Prod.fst xh:p ∈ xh_mem:p.1 ∈ Multiset.map Prod.fst x⊒ False𝓩:Typeinst✝¹:DecidableEq 𝓩M:Type u_1inst✝:AddCommMonoid Mx:FiveQuanta 𝓩f:𝓩 β†’ Fluxes β†’+ Mp:𝓩 Γ— Fluxesh_mem:p.1 βˆ‰ Multiset.map Prod.fst x⊒ βˆ€ x_1 ∈ Multiset.map (fun y => if p.1 = y then Multiset.count p x else 0) (Multiset.map Prod.fst x).dedup, x_1 = 0; 𝓩:Typeinst✝¹:DecidableEq 𝓩M:Type u_1inst✝:AddCommMonoid Mx:FiveQuanta 𝓩f:𝓩 β†’ Fluxes β†’+ Mp:𝓩 Γ— Fluxesh_mem:p.1 βˆ‰ Multiset.map Prod.fst x⊒ βˆ€ x_1 ∈ Multiset.map (fun y => if p.1 = y then Multiset.count p x else 0) (Multiset.map Prod.fst x).dedup, x_1 = 0) 𝓩:Typeinst✝¹:DecidableEq 𝓩M:Type u_1inst✝:AddCommMonoid Mx:FiveQuanta 𝓩f:𝓩 β†’ Fluxes β†’+ Mp:𝓩 Γ— Fluxesh_mem:p.1 βˆ‰ Multiset.map Prod.fst xp':β„•hp:p' ∈ Multiset.map (fun y => if p.1 = y then Multiset.count p x else 0) (Multiset.map Prod.fst x).dedup⊒ p' = 0 𝓩:Typeinst✝¹:DecidableEq 𝓩M:Type u_1inst✝:AddCommMonoid Mx:FiveQuanta 𝓩f:𝓩 β†’ Fluxes β†’+ Mp:𝓩 Γ— Fluxesh_mem:p.1 βˆ‰ Multiset.map Prod.fst xp':β„•hp:βˆƒ a, (βˆƒ x_1, (a, x_1) ∈ x) ∧ (if p.1 = a then Multiset.count p x else 0) = p'⊒ p' = 0 𝓩:Typeinst✝¹:DecidableEq 𝓩M:Type u_1inst✝:AddCommMonoid Mx:FiveQuanta 𝓩f:𝓩 β†’ Fluxes β†’+ Mp:𝓩 Γ— Fluxesh_mem:p.1 βˆ‰ Multiset.map Prod.fst xp':β„•q5':𝓩hp':(if p.1 = q5' then Multiset.count p x else 0) = p'f1:Fluxeshf:(q5', f1) ∈ x⊒ p' = 0 𝓩:Typeinst✝¹:DecidableEq 𝓩M:Type u_1inst✝:AddCommMonoid Mx:FiveQuanta 𝓩f:𝓩 β†’ Fluxes β†’+ Mp:𝓩 Γ— Fluxesh_mem:p.1 βˆ‰ Multiset.map Prod.fst xp':β„•q5':𝓩hp':(if p.1 = q5' then Multiset.count p x else 0) = p'f1:Fluxeshf:(q5', f1) ∈ xh_eq:p.1 = q5'⊒ p' = 0𝓩:Typeinst✝¹:DecidableEq 𝓩M:Type u_1inst✝:AddCommMonoid Mx:FiveQuanta 𝓩f:𝓩 β†’ Fluxes β†’+ Mp:𝓩 Γ— Fluxesh_mem:p.1 βˆ‰ Multiset.map Prod.fst xp':β„•q5':𝓩hp':(if p.1 = q5' then Multiset.count p x else 0) = p'f1:Fluxeshf:(q5', f1) ∈ xh_eq:Β¬p.1 = q5'⊒ p' = 0 𝓩:Typeinst✝¹:DecidableEq 𝓩M:Type u_1inst✝:AddCommMonoid Mx:FiveQuanta 𝓩f:𝓩 β†’ Fluxes β†’+ Mp:𝓩 Γ— Fluxesh_mem:p.1 βˆ‰ Multiset.map Prod.fst xp':β„•q5':𝓩hp':(if p.1 = q5' then Multiset.count p x else 0) = p'f1:Fluxeshf:(q5', f1) ∈ xh_eq:p.1 = q5'⊒ p' = 0 All goals completed! πŸ™ 𝓩:Typeinst✝¹:DecidableEq 𝓩M:Type u_1inst✝:AddCommMonoid Mx:FiveQuanta 𝓩f:𝓩 β†’ Fluxes β†’+ Mp:𝓩 Γ— Fluxesh_mem:p.1 βˆ‰ Multiset.map Prod.fst xp':β„•q5':𝓩hp':(if p.1 = q5' then Multiset.count p x else 0) = p'f1:Fluxeshf:(q5', f1) ∈ xh_eq:Β¬p.1 = q5'⊒ p' = 0 All goals completed! πŸ™

B.7. Reduction does nothing if no duplicate charges

𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩h:βˆ€ x_1 ∈ x, βˆ€ y ∈ x, x_1.1 = y.1 β†’ x_1 = yp:𝓩 Γ— Fluxeshp:p ∈ xx_noDup:Multiset.Nodup xp':𝓩 Γ— Fluxesh1:p' ∈ xh2:p'.1 = p.1⊒ p' = p 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩h:βˆ€ x_1 ∈ x, βˆ€ y ∈ x, x_1.1 = y.1 β†’ x_1 = yp:𝓩 Γ— Fluxeshp:p ∈ xx_noDup:Multiset.Nodup xp':𝓩 Γ— Fluxesh1:p' ∈ xh2:p'.1 = p.1⊒ p' ∈ x𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩h:βˆ€ x_1 ∈ x, βˆ€ y ∈ x, x_1.1 = y.1 β†’ x_1 = yp:𝓩 Γ— Fluxeshp:p ∈ xx_noDup:Multiset.Nodup xp':𝓩 Γ— Fluxesh1:p' ∈ xh2:p'.1 = p.1⊒ p ∈ x𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩h:βˆ€ x_1 ∈ x, βˆ€ y ∈ x, x_1.1 = y.1 β†’ x_1 = yp:𝓩 Γ— Fluxeshp:p ∈ xx_noDup:Multiset.Nodup xp':𝓩 Γ— Fluxesh1:p' ∈ xh2:p'.1 = p.1⊒ p'.1 = p.1 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩h:βˆ€ x_1 ∈ x, βˆ€ y ∈ x, x_1.1 = y.1 β†’ x_1 = yp:𝓩 Γ— Fluxeshp:p ∈ xx_noDup:Multiset.Nodup xp':𝓩 Γ— Fluxesh1:p' ∈ xh2:p'.1 = p.1⊒ p' ∈ x All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩h:βˆ€ x_1 ∈ x, βˆ€ y ∈ x, x_1.1 = y.1 β†’ x_1 = yp:𝓩 Γ— Fluxeshp:p ∈ xx_noDup:Multiset.Nodup xp':𝓩 Γ— Fluxesh1:p' ∈ xh2:p'.1 = p.1⊒ p ∈ x All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩h:βˆ€ x_1 ∈ x, βˆ€ y ∈ x, x_1.1 = y.1 β†’ x_1 = yp:𝓩 Γ— Fluxeshp:p ∈ xx_noDup:Multiset.Nodup xp':𝓩 Γ— Fluxesh1:p' ∈ xh2:p'.1 = p.1⊒ p'.1 = p.1 All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩h:x.toCharges.Nodupp:𝓩 Γ— Fluxeshp:p ∈ xx_noDup:Multiset.Nodup xp':𝓩 Γ— Fluxes⊒ p' = p β†’ p' ∈ x ∧ p'.1 = p.1 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩h:x.toCharges.Nodupp:𝓩 Γ— Fluxeshp:p ∈ xx_noDup:Multiset.Nodup x⊒ p ∈ x ∧ p.1 = p.1 All goals completed! πŸ™

B.8. The charge map is preserved by reduction

𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩q:𝓩h:q βˆ‰ x.toCharges⊒ q βˆ‰ x.toCharges𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩q:𝓩h:q βˆ‰ x.toCharges⊒ q βˆ‰ x.reduce.toCharges 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩q:𝓩h:q βˆ‰ x.toCharges⊒ q βˆ‰ x.toCharges All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩q:𝓩h:q βˆ‰ x.toCharges⊒ q βˆ‰ x.reduce.toCharges All goals completed! πŸ™

B.9. A fluxes in the reduced FiveQuanta is a sum of fluxes in the original FiveQuanta

𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩q:𝓩f:Fluxeshp:(q, f).1 ∈ F.toCharges ∧ (q, f).2 = (Multiset.map (fun y => y.2) (Multiset.filter (fun f_1 => f_1.1 = (q, f).1) F)).sum⊒ (q, f).2 ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesFive) 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩q:𝓩f:Fluxeshp:q ∈ F.toCharges ∧ f = (Multiset.map (fun x => x.2) (Multiset.filter (fun x => x.1 = q) F)).sum⊒ (q, f).2 ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesFive) 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩q:𝓩hq:q ∈ F.toCharges⊒ (q, (Multiset.map (fun x => x.2) (Multiset.filter (fun x => x.1 = q) F)).sum).2 ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesFive) 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩q:𝓩hq:q ∈ F.toCharges⊒ βˆƒ a ≀ F.toFluxesFive, a.sum = (Multiset.map (fun x => x.2) (Multiset.filter (fun x => x.1 = q) F)).sum 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩q:𝓩hq:q ∈ F.toCharges⊒ Multiset.map (fun x => x.2) (Multiset.filter (fun x => x.1 = q) F) ≀ F.toFluxesFive ∧ (Multiset.map (fun x => x.2) (Multiset.filter (fun x => x.1 = q) F)).sum = (Multiset.map (fun x => x.2) (Multiset.filter (fun x => x.1 = q) F)).sum All goals completed! πŸ™π“©:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩q:𝓩hq:βˆƒ a ∈ F, a.1 = q⊒ βˆƒ x, (q, x) ∈ F 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩a:𝓩 Γ— Fluxesha:a ∈ F⊒ βˆƒ x, (a.1, x) ∈ F All goals completed! πŸ™

B.10. No exotics condition on the reduced FiveQuanta

B.10.1. Number of chiral L
𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticshE:F.toFluxesFive.NoExoticshnn:βˆ€ a ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesFive, 0 ≀ a⊒ (Multiset.map ((fun f => f.M + f.N) ∘ Prod.snd) F.reduce).sum = (Multiset.map ((fun f => f.M + f.N) ∘ Prod.snd) F).sum exact reduce_sum_eq_sum_toCharges F (fun _ => ⟨⟨fun f => f.M + f.N, 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticshE:F.toFluxesFive.NoExoticshnn:βˆ€ a ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesFive, 0 ≀ ax✝:π“©βŠ’ Fluxes.M 0 + Fluxes.N 0 = 0 All goals completed! πŸ™βŸ©, fun x y => 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticshE:F.toFluxesFive.NoExoticshnn:βˆ€ a ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesFive, 0 ≀ ax✝:𝓩x:Fluxesy:Fluxes⊒ { toFun := fun f => f.M + f.N, map_zero' := β‹― }.toFun (x + y) = { toFun := fun f => f.M + f.N, map_zero' := β‹― }.toFun x + { toFun := fun f => f.M + f.N, map_zero' := β‹― }.toFun y All goals completed! πŸ™βŸ©)
B.10.2. Number of anti-chiral L
𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExotics⊒ βˆ€ a ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesFive, Β¬a < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticsa:β„€ha:a ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesFive⊒ Β¬a < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticsf:Fluxeshf:f ∈ F.reduce.toFluxesFiveha:f.M + f.N ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesFive⊒ Β¬f.M + f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticsf:Fluxesha:f.M + f.N ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesFivehf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesFive)⊒ Β¬f.M + f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticsf:Fluxeshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesFive)⊒ Β¬f.M + f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩f:FluxesG:FluxesFivehx:G ∈ FluxesFive.elemsNoExoticshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G)⊒ Β¬f.M + f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩G:FluxesFivehx:G ∈ FluxesFive.elemsNoExotics⊒ βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), Β¬f.M + f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta π“©βŠ’ βˆ€ G ∈ FluxesFive.elemsNoExotics, βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), Β¬f.M + f.N < 0 All goals completed! πŸ™
B.10.3. Number of chiral D
𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticshE:F.toFluxesFive.NoExoticshnn:βˆ€ a ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesFive, 0 ≀ a⊒ (Multiset.map ((fun f => f.M) ∘ Prod.snd) F.reduce).sum = (Multiset.map ((fun f => f.M) ∘ Prod.snd) F).sum exact reduce_sum_eq_sum_toCharges F (fun _ => ⟨⟨fun f => f.M, 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticshE:F.toFluxesFive.NoExoticshnn:βˆ€ a ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesFive, 0 ≀ ax✝:π“©βŠ’ Fluxes.M 0 = 0 All goals completed! πŸ™βŸ©, fun x y => 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticshE:F.toFluxesFive.NoExoticshnn:βˆ€ a ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesFive, 0 ≀ ax✝:𝓩x:Fluxesy:Fluxes⊒ { toFun := fun f => f.M, map_zero' := β‹― }.toFun (x + y) = { toFun := fun f => f.M, map_zero' := β‹― }.toFun x + { toFun := fun f => f.M, map_zero' := β‹― }.toFun y All goals completed! πŸ™βŸ©)
B.10.4. Number of anti-chiral D
𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExotics⊒ βˆ€ a ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesFive, Β¬a < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticsa:β„€ha:a ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesFive⊒ Β¬a < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticsf:Fluxeshf:f ∈ F.reduce.toFluxesFiveha:f.M ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesFive⊒ Β¬f.M < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticsf:Fluxesha:f.M ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesFivehf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesFive)⊒ Β¬f.M < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticsf:Fluxeshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesFive)⊒ Β¬f.M < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩f:FluxesG:FluxesFivehx:G ∈ FluxesFive.elemsNoExoticshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G)⊒ Β¬f.M < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩G:FluxesFivehx:G ∈ FluxesFive.elemsNoExotics⊒ βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), Β¬f.M < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta π“©βŠ’ βˆ€ G ∈ FluxesFive.elemsNoExotics, βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), Β¬f.M < 0 All goals completed! πŸ™
B.10.5. The NoExotics condition on the reduced FiveQuanta
lemma reduce_noExotics_of_mem_elemsNoExotics {F : FiveQuanta 𝓩} (hx : F.toFluxesFive ∈ FluxesFive.elemsNoExotics) : F.reduce.toFluxesFive.NoExotics := 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExotics⊒ F.reduce.toFluxesFive.NoExotics All goals completed! πŸ™

B.11. Reduce member of FluxesFive.elemsNoExotics

𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExotics⊒ F.reduce.toFluxesFive.NoExotics ∧ F.reduce.toFluxesFive.HasNoZero 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticsh:0 ∈ F.reduce.toFluxesFive⊒ False 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩hx:F.toFluxesFive ∈ FluxesFive.elemsNoExoticsh:0 ∈ Multiset.map (fun s => s.sum) (Multiset.filter (fun s => s β‰  βˆ…) (Multiset.powerset F.toFluxesFive))⊒ False 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta 𝓩G:FluxesFivehx:G ∈ FluxesFive.elemsNoExoticsh:0 ∈ Multiset.map (fun s => s.sum) (Multiset.filter (fun s => s β‰  βˆ…) (Multiset.powerset G))⊒ False 𝓩:Typeinst✝:DecidableEq 𝓩F:FiveQuanta π“©βŠ’ βˆ€ G ∈ FluxesFive.elemsNoExotics, 0 ∈ Multiset.map (fun s => s.sum) (Multiset.filter (fun s => s β‰  βˆ…) (Multiset.powerset G)) β†’ False All goals completed! πŸ™

C. Decomposition of a FiveQuanta into basic fluxes

C.1. Decomposition of fluxes

The decomposition of a flux into ⟨1, -1⟩ and ⟨0, 1⟩.

def decomposeFluxes (f : Fluxes) : Multiset Fluxes := Multiset.replicate (Int.natAbs f.M) ⟨1, -1⟩ + Multiset.replicate (Int.natAbs (f.M + f.N)) ⟨0, 1⟩
lemma decomposeFluxes_sum_of_noExotics (f : Fluxes) (hf : βˆƒ F ∈ FluxesFive.elemsNoExotics, f ∈ F) : (decomposeFluxes f).sum = f := f:Fluxeshf:βˆƒ F ∈ FluxesFive.elemsNoExotics, f ∈ F⊒ (decomposeFluxes f).sum = f f:FluxesF:FluxesFivehF:F ∈ FluxesFive.elemsNoExoticshfF:f ∈ F⊒ (decomposeFluxes f).sum = f F:FluxesFivehF:F ∈ FluxesFive.elemsNoExotics⊒ βˆ€ f ∈ F, (decomposeFluxes f).sum = f ⊒ βˆ€ F ∈ FluxesFive.elemsNoExotics, βˆ€ f ∈ F, (decomposeFluxes f).sum = f All goals completed! πŸ™

C.2. Decomposition of a FiveQuanta (with no exotics)

The decomposition of a FiveQuanta into a FiveQuanta which has the same reduce by has fluxes ⟨1, -1⟩ and ⟨0,1⟩ only.

def decompose (x : FiveQuanta 𝓩) : FiveQuanta 𝓩 := x.bind fun p => (decomposeFluxes p.2).map fun f => (p.1, f)
C.2.1. Decomposition distributes over addition
lemma decompose_add (x y : FiveQuanta 𝓩) : (x + y).decompose = x.decompose + y.decompose := 𝓩:Typex:FiveQuanta 𝓩y:FiveQuanta π“©βŠ’ (x + y).decompose = x.decompose + y.decompose All goals completed! πŸ™
C.2.2. Decomposition commutes with filtering charges
All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩a:𝓩 Γ— Fluxesx:Multiset (𝓩 Γ— Fluxes)ih:Multiset.filter (fun p => p.1 = q) (x.bind fun p => Multiset.map (fun f => (p.1, f)) (decomposeFluxes p.2)) = decompose (Multiset.filter (fun p => p.1 = q) x)q':𝓩f:Fluxesh:Β¬q' = q⊒ Multiset.filter (fun p => p.1 = q) (Multiset.replicate f.M.natAbs (q', { M := 1, N := -1 })) + Multiset.filter (fun p => p.1 = q) (Multiset.replicate (f.M + f.N).natAbs (q', { M := 0, N := 1 })) = decompose (if q' = q then {(q', f)} else 0) 𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩a:𝓩 Γ— Fluxesx:Multiset (𝓩 Γ— Fluxes)ih:Multiset.filter (fun p => p.1 = q) (x.bind fun p => Multiset.map (fun f => (p.1, f)) (decomposeFluxes p.2)) = decompose (Multiset.filter (fun p => p.1 = q) x)q':𝓩f:Fluxesh:Β¬q' = q⊒ (βˆ€ (a : 𝓩) (b : Fluxes), (a, b) ∈ Multiset.replicate f.M.natAbs (q', { M := 1, N := -1 }) β†’ Β¬a = q) ∧ βˆ€ (a : 𝓩) (b : Fluxes), (a, b) ∈ Multiset.replicate (f.M + f.N).natAbs (q', { M := 0, N := 1 }) β†’ Β¬a = q 𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩a:𝓩 Γ— Fluxesx:Multiset (𝓩 Γ— Fluxes)ih:Multiset.filter (fun p => p.1 = q) (x.bind fun p => Multiset.map (fun f => (p.1, f)) (decomposeFluxes p.2)) = decompose (Multiset.filter (fun p => p.1 = q) x)q':𝓩f:Fluxesh:Β¬q' = q⊒ βˆ€ (a : 𝓩) (b : Fluxes), (a, b) ∈ Multiset.replicate f.M.natAbs (q', { M := 1, N := -1 }) β†’ Β¬a = q𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩a:𝓩 Γ— Fluxesx:Multiset (𝓩 Γ— Fluxes)ih:Multiset.filter (fun p => p.1 = q) (x.bind fun p => Multiset.map (fun f => (p.1, f)) (decomposeFluxes p.2)) = decompose (Multiset.filter (fun p => p.1 = q) x)q':𝓩f:Fluxesh:Β¬q' = q⊒ βˆ€ (a : 𝓩) (b : Fluxes), (a, b) ∈ Multiset.replicate (f.M + f.N).natAbs (q', { M := 0, N := 1 }) β†’ Β¬a = q all_goals 𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩a:𝓩 Γ— Fluxesx:Multiset (𝓩 Γ— Fluxes)ih:Multiset.filter (fun p => p.1 = q) (x.bind fun p => Multiset.map (fun f => (p.1, f)) (decomposeFluxes p.2)) = decompose (Multiset.filter (fun p => p.1 = q) x)q':𝓩f:Fluxesh:Β¬q' = q⊒ βˆ€ (a : 𝓩) (b : Fluxes), (a, b) ∈ Multiset.replicate (f.M + f.N).natAbs (q', { M := 0, N := 1 }) β†’ Β¬a = q 𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩a✝:𝓩 Γ— Fluxesx:Multiset (𝓩 Γ— Fluxes)ih:Multiset.filter (fun p => p.1 = q) (x.bind fun p => Multiset.map (fun f => (p.1, f)) (decomposeFluxes p.2)) = decompose (Multiset.filter (fun p => p.1 = q) x)q':𝓩f:Fluxesh✝:Β¬q' = qa:𝓩b:Fluxesh:(a, b) ∈ Multiset.replicate (f.M + f.N).natAbs (q', { M := 0, N := 1 })⊒ Β¬a = q 𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩a✝:𝓩 Γ— Fluxesx:Multiset (𝓩 Γ— Fluxes)ih:Multiset.filter (fun p => p.1 = q) (x.bind fun p => Multiset.map (fun f => (p.1, f)) (decomposeFluxes p.2)) = decompose (Multiset.filter (fun p => p.1 = q) x)q':𝓩f:Fluxesh✝:Β¬q' = qa:𝓩b:Fluxesh:Β¬f.M + f.N = 0 ∧ a = q' ∧ b = { M := 0, N := 1 }⊒ Β¬a = q All goals completed! πŸ™
C.2.3. Decomposition preserves the charge map
𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExoticsq:π“©βŠ’ (Multiset.map (fun a => (decomposeFluxes a.2).sum) (Multiset.filter (fun p => p.1 = q) x)).sum = (Multiset.map Prod.snd (Multiset.filter (fun p => p.1 = q) x)).sum 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExoticsq:π“©βŠ’ Multiset.map (fun a => (decomposeFluxes a.2).sum) (Multiset.filter (fun p => p.1 = q) x) = Multiset.map Prod.snd (Multiset.filter (fun p => p.1 = q) x) 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExoticsq:π“©βŠ’ Multiset.filter (fun p => p.1 = q) x = Multiset.filter (fun p => p.1 = q) x𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExoticsq:π“©βŠ’ βˆ€ x_1 ∈ Multiset.filter (fun p => p.1 = q) x, (decomposeFluxes x_1.2).sum = x_1.2 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExoticsq:π“©βŠ’ Multiset.filter (fun p => p.1 = q) x = Multiset.filter (fun p => p.1 = q) x All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExoticsq:𝓩a:𝓩 Γ— Fluxesha:a ∈ Multiset.filter (fun p => p.1 = q) x⊒ (decomposeFluxes a.2).sum = a.2 All goals completed! πŸ™
C.2.4. Decomposition preserves the charges
𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExoticsq:𝓩c:Fluxesh1:(q, c) ∈ xhn:decomposeFluxes c β‰  0⊒ βˆƒ x_1 a b, (a, b) ∈ x ∧ x_1 ∈ decomposeFluxes b ∧ a = q 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExoticsq:𝓩c:Fluxesh1:(q, c) ∈ xhn:βˆƒ a, a ∈ decomposeFluxes c⊒ βˆƒ x_1 a b, (a, b) ∈ x ∧ x_1 ∈ decomposeFluxes b ∧ a = q 𝓩:Typeinst✝:DecidableEq 𝓩x:FiveQuanta 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExoticsq:𝓩c:Fluxesh1:(q, c) ∈ xc':Fluxesh:c' ∈ decomposeFluxes c⊒ βˆƒ x_1 a b, (a, b) ∈ x ∧ x_1 ∈ decomposeFluxes b ∧ a = q All goals completed! πŸ™
C.2.5. Decomposition preserves the reduction
All goals completed! πŸ™ 𝓩:Typex:FiveQuanta 𝓩inst✝:DecidableEq 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExotics⊒ βˆ€ x_1 ∈ x.toCharges.dedup, (x_1, (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = x_1) x.decompose)).sum) = (x_1, (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = x_1) x)).sum) 𝓩:Typex:FiveQuanta 𝓩inst✝:DecidableEq 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExoticsq:𝓩hx':q ∈ x.toCharges.dedup⊒ (q, (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = q) x.decompose)).sum) = (q, (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = q) x)).sum) 𝓩:Typex:FiveQuanta 𝓩inst✝:DecidableEq 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExoticsq:𝓩hx':q ∈ x.toCharges.dedup⊒ (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = q) x.decompose)).sum = (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = q) x)).sum All goals completed! πŸ™
C.2.6. Fluxes of the decomposition of a FiveQuanta
All goals completed! πŸ™ 𝓩:Typex:FiveQuanta 𝓩hx:x.toFluxesFive ∈ FluxesFive.elemsNoExotics⊒ (Multiset.bind x.toFluxesFive fun a => decomposeFluxes a) = { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ {{ M := 0, N := 1 }} 𝓩:Typex:FiveQuanta 𝓩F:FluxesFivehx:F ∈ FluxesFive.elemsNoExotics⊒ (Multiset.bind F fun a => decomposeFluxes a) = { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ {{ M := 0, N := 1 }} 𝓩:Typex:FiveQuanta π“©βŠ’ βˆ€ F ∈ FluxesFive.elemsNoExotics, (Multiset.bind F fun a => decomposeFluxes a) = { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ {{ M := 0, N := 1 }} All goals completed! πŸ™

D. Lifting charges to FiveQuanta

D.1. liftCharge c: multiset of five-quanta for a finite set of charges c with no exotics

This is an efficient definition, we will later show that it gives the correct answer

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 that s1 and s2 are cardinality of `3` containing elements of `c` and that all elements of `c` are in `s1 + s2`. -/ let S5p : Multiset (Multiset 𝓩 Γ— Multiset 𝓩) := (S53 Γ—Λ’ S53).filter fun (s1, s2) => c.val ≀ s1 + s2 let Fp : Multiset (FiveQuanta 𝓩) := S5p.map (fun y => y.1.map (fun z => (z, ⟨1, -1⟩)) + y.2.map (fun z => (z, ⟨0, 1⟩))) Fp.map reduce

D.2. FiveQuanta in liftCharge c have a finite set of charges c

𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s1:Multiset 𝓩s2:Multiset 𝓩hsum:c.val ≀ s1 + s2s1_subset:s1.toFinset βŠ† cs1_card:s1.card = 3s2_subset:s2.toFinset βŠ† cs2_card:s2.card = 3⊒ (Multiset.map (fun z => (z, { M := 1, N := -1 })) s1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) s2).toCharges.dedup.dedup.toFinset = c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s1:Multiset 𝓩s2:Multiset 𝓩hsum:c.val ≀ s1 + s2s1_subset:s1.toFinset βŠ† cs1_card:s1.card = 3s2_subset:s2.toFinset βŠ† cs2_card:s2.card = 3⊒ (Multiset.map (fun z => (z, { M := 1, N := -1 })) s1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) s2).toCharges.toFinset = c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s1:Multiset 𝓩s2:Multiset 𝓩hsum:c.val ≀ s1 + s2s1_subset:s1.toFinset βŠ† cs1_card:s1.card = 3s2_subset:s2.toFinset βŠ† cs2_card:s2.card = 3⊒ s1.toFinset βˆͺ s2.toFinset = c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s1:Multiset 𝓩s2:Multiset 𝓩hsum:c.val ≀ s1 + s2s1_subset:s1.toFinset βŠ† cs1_card:s1.card = 3s2_subset:s2.toFinset βŠ† cs2_card:s2.card = 3a:𝓩ha:a ∈ c⊒ a ∈ s1.toFinset βˆͺ s2.toFinset All goals completed! πŸ™

D.3. FiveQuanta in liftCharge c have no duplicate charges

𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:FiveQuanta 𝓩h:βˆƒ a ∈ Multiset.map (fun y => Multiset.map (fun z => (z, { M := 1, N := -1 })) y.1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) y.2) (Multiset.filter (fun x => match x with | (s1, s2) => c.val ≀ s1 + s2) (toMultisetsThree c Γ—Λ’ toMultisetsThree c)), a.reduce = x⊒ x.toCharges.Nodup 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:FiveQuanta 𝓩h:x ∈ Multiset.map (fun y => Multiset.map (fun z => (z, { M := 1, N := -1 })) y.1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) y.2) (Multiset.filter (fun x => match x with | (s1, s2) => c.val ≀ s1 + s2) (toMultisetsThree c Γ—Λ’ toMultisetsThree c))⊒ x.reduce.toCharges.Nodup All goals completed! πŸ™

D.4. Membership in liftCharge c iff is reduction of FiveQuanta with given fluxes

𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:FiveQuanta 𝓩h:βˆƒ a ∈ Multiset.map (fun y => Multiset.map (fun z => (z, { M := 1, N := -1 })) y.1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) y.2) (Multiset.filter (fun x => match x with | (s1, s2) => c.val ≀ s1 + s2) (toMultisetsThree c Γ—Λ’ toMultisetsThree c)), a.reduce = xh':x ∈ liftCharge c⊒ βˆƒ a, a.reduce = x ∧ a.toCharges.toFinset = c ∧ a.toFluxesFive = {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }} 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:FiveQuanta 𝓩h:a ∈ Multiset.map (fun y => Multiset.map (fun z => (z, { M := 1, N := -1 })) y.1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) y.2) (Multiset.filter (fun x => match x with | (s1, s2) => c.val ≀ s1 + s2) (toMultisetsThree c Γ—Λ’ toMultisetsThree c))h':a.reduce ∈ liftCharge c⊒ βˆƒ a_1, a_1.reduce = a.reduce ∧ a_1.toCharges.toFinset = c ∧ a_1.toFluxesFive = {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }} 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:FiveQuanta 𝓩h:a ∈ Multiset.map (fun y => Multiset.map (fun z => (z, { M := 1, N := -1 })) y.1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) y.2) (Multiset.filter (fun x => match x with | (s1, s2) => c.val ≀ s1 + s2) (toMultisetsThree c Γ—Λ’ toMultisetsThree c))h':a.reduce ∈ liftCharge c⊒ a.reduce = a.reduce ∧ a.toCharges.toFinset = c ∧ a.toFluxesFive = {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }} 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:FiveQuanta 𝓩h:a ∈ Multiset.map (fun y => Multiset.map (fun z => (z, { M := 1, N := -1 })) y.1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) y.2) (Multiset.filter (fun x => match x with | (s1, s2) => c.val ≀ s1 + s2) (toMultisetsThree c Γ—Λ’ toMultisetsThree c))h':a.reduce ∈ liftCharge c⊒ a.toCharges.toFinset = c ∧ a.toFluxesFive = { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ {{ M := 0, N := 1 }} 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:FiveQuanta 𝓩h:a ∈ Multiset.map (fun y => Multiset.map (fun z => (z, { M := 1, N := -1 })) y.1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) y.2) (Multiset.filter (fun x => match x with | (s1, s2) => c.val ≀ s1 + s2) (toMultisetsThree c Γ—Λ’ toMultisetsThree c))h':a.reduce ∈ liftCharge c⊒ a.toCharges.toFinset = c𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:FiveQuanta 𝓩h:a ∈ Multiset.map (fun y => Multiset.map (fun z => (z, { M := 1, N := -1 })) y.1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) y.2) (Multiset.filter (fun x => match x with | (s1, s2) => c.val ≀ s1 + s2) (toMultisetsThree c Γ—Λ’ toMultisetsThree c))h':a.reduce ∈ liftCharge c⊒ a.toFluxesFive = { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ {{ M := 0, N := 1 }} 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:FiveQuanta 𝓩h:a ∈ Multiset.map (fun y => Multiset.map (fun z => (z, { M := 1, N := -1 })) y.1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) y.2) (Multiset.filter (fun x => match x with | (s1, s2) => c.val ≀ s1 + s2) (toMultisetsThree c Γ—Λ’ toMultisetsThree c))h':a.reduce ∈ liftCharge c⊒ a.toCharges.toFinset = c All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:FiveQuanta 𝓩h:a ∈ Multiset.map (fun y => Multiset.map (fun z => (z, { M := 1, N := -1 })) y.1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) y.2) (Multiset.filter (fun x => match x with | (s1, s2) => c.val ≀ s1 + s2) (toMultisetsThree c Γ—Λ’ toMultisetsThree c))h':a.reduce ∈ liftCharge c⊒ a.toFluxesFive = { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ {{ M := 0, N := 1 }} 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:FiveQuanta 𝓩h':a.reduce ∈ liftCharge ch:βˆƒ a_1 b, (((a_1.toFinset βŠ† c ∧ a_1.card = 3) ∧ b.toFinset βŠ† c ∧ b.card = 3) ∧ c.val ≀ a_1 + b) ∧ Multiset.map (fun z => (z, { M := 1, N := -1 })) a_1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) b = a⊒ a.toFluxesFive = { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ {{ M := 0, N := 1 }} 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s1:Multiset 𝓩s2:Multiset 𝓩hsum:c.val ≀ s1 + s2s1_subset:s1.toFinset βŠ† cs1_card:s1.card = 3s2_subset:s2.toFinset βŠ† cs2_card:s2.card = 3h':(Multiset.map (fun z => (z, { M := 1, N := -1 })) s1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) s2).reduce ∈ liftCharge c⊒ (Multiset.map (fun z => (z, { M := 1, N := -1 })) s1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) s2).toFluxesFive = { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ {{ M := 0, N := 1 }} 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s1:Multiset 𝓩s2:Multiset 𝓩hsum:c.val ≀ s1 + s2s1_subset:s1.toFinset βŠ† cs1_card:s1.card = 3s2_subset:s2.toFinset βŠ† cs2_card:s2.card = 3h':(Multiset.map (fun z => (z, { M := 1, N := -1 })) s1 + Multiset.map (fun z => (z, { M := 0, N := 1 })) s2).reduce ∈ liftCharge c⊒ { M := 0, N := 1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ {{ M := 0, N := 1 }} = { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ { M := 0, N := 1 } ::β‚˜ {{ M := 0, N := 1 }} All goals completed! πŸ™π“©:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:FiveQuanta 𝓩h:x.toCharges.toFinset = ch2:x.toFluxesFive = {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}s1:Multiset 𝓩 := Multiset.map Prod.fst (Multiset.filter (fun y => y.2 = { M := 1, N := -1 }) x)s2:Multiset 𝓩 := Multiset.map Prod.fst (Multiset.filter (fun y => y.2 = { M := 0, N := 1 }) x)hcard:βˆ€ (v : Fluxes), (Multiset.filter (fun y => y.2 = v) x).card = (Multiset.filter (fun y => y = v) x.toFluxesFive).cardhmap:βˆ€ (v : Fluxes), Multiset.map (fun y => (y.1, v)) (Multiset.filter (fun y => y.2 = v) x) = Multiset.filter (fun y => y.2 = v) xhx:Multiset.filter (fun y => y.2 = { M := 0, N := 1 }) x = Multiset.filter (fun y => Β¬y.2 = { M := 1, N := -1 }) x⊒ Multiset.filter (fun y => y.2 = { M := 1, N := -1 }) x + Multiset.filter (fun y => Β¬y.2 = { M := 1, N := -1 }) x = x All goals completed! πŸ™lemma mem_liftCharge_iff_exists (c : Finset 𝓩) {x : FiveQuanta 𝓩} : x ∈ liftCharge c ↔ βˆƒ a : FiveQuanta 𝓩, a.reduce = x ∧ a.toCharges.toFinset = c ∧ a.toFluxesFive = {⟨1, -1⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨0, 1⟩, ⟨0, 1⟩, ⟨0, 1⟩} := ⟨exists_toCharges_toFluxesFive_of_mem_liftCharge c, mem_liftCharge_of_exists_toCharges_toFluxesFive c⟩

D.5. FiveQuanta in liftCharge c do not have zero fluxes

𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:FiveQuanta 𝓩h1:x.toCharges.toFinset = ch2:x.toFluxesFive = {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}hf:0 ∈ x.reduce.toFluxesFivehx:0 ∈ Multiset.map (fun s => s.sum) (Multiset.filter (fun s => s β‰  βˆ…) (Multiset.powerset {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}))⊒ False 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:FiveQuanta 𝓩h1:x.toCharges.toFinset = ch2:x.toFluxesFive = {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}hf:0 ∈ x.reduce.toFluxesFive⊒ 0 ∈ Multiset.map (fun s => s.sum) (Multiset.filter (fun s => s β‰  βˆ…) (Multiset.powerset {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }})) β†’ False All goals completed! πŸ™

D.6. FiveQuanta in liftCharge c have no exotics

𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:FiveQuanta 𝓩h1:x.toCharges.toFinset = ch2:x.toFluxesFive = {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊒ {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }} ∈ FluxesFive.elemsNoExotics All goals completed! πŸ™

D.7. Membership in liftCharge c iff have no exotics, no zero fluxes, and charges c

All goals completed! πŸ™π“©:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:FiveQuanta 𝓩h1:x.toFluxesFive.NoExotics ∧ x.toFluxesFive.HasNoZeroh2:x.toCharges.toFinset = ch3:x.toCharges.Nodup⊒ x ∈ liftCharge c All goals completed! πŸ™

D.8. liftCharge c is preserved under a map if reduced

𝓩:Type𝓩1:Typeinst✝³:DecidableEq 𝓩inst✝²:DecidableEq 𝓩1inst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 β†’+* 𝓩1c:Finset 𝓩F:FiveQuanta 𝓩h:F.toFluxesFive ∈ FluxesFive.elemsNoExotics ∧ F.toCharges.toFinset = c ∧ F.toCharges.Nodup⊒ (toCharges (Multiset.map (fun y => (f y.1, y.2)) F)).dedup.toFinset = Finset.image (⇑f) c All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:DecidableEq 𝓩inst✝²:DecidableEq 𝓩1inst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 β†’+* 𝓩1c:Finset 𝓩F:FiveQuanta 𝓩h:F.toFluxesFive ∈ FluxesFive.elemsNoExotics ∧ F.toCharges.toFinset = c ∧ F.toCharges.Nodup⊒ (reduce (Multiset.map (fun y => (f y.1, y.2)) F)).toCharges.Nodup All goals completed! πŸ™

E. Anomaly cancellation coefficients

E.1. Anomaly coefficients of a FiveQuanta

The anomaly coefficient of a FiveQuanta is given by the pair of integers: (βˆ‘α΅’ qα΅’ Nα΅’, βˆ‘α΅’ qα΅’Β² Nα΅’).

The first components is for the mixed U(1)-MSSM, see equation (22) of arXiv:1401.5084. The second component is for the mixed U(1)Y-U(1)-U(1) gauge anomaly, see equation (23) of arXiv:1401.5084.

def anomalyCoefficient (F : FiveQuanta 𝓩) : 𝓩 Γ— 𝓩 := ((F.map fun x => x.2.2 β€’ x.1).sum, (F.map fun x => x.2.2 β€’ (x.1 * x.1)).sum)

E.2. Anomaly coefficients under a map

@[simp] lemma anomalyCoefficient_of_map {𝓩 𝓩1 : Type} [CommRing 𝓩] [CommRing 𝓩1] (f : 𝓩 β†’+* 𝓩1) (F : FiveQuanta 𝓩) : FiveQuanta.anomalyCoefficient (F.map fun y => (f y.1, y.2) : FiveQuanta 𝓩1) = (f.prodMap f) F.anomalyCoefficient := 𝓩:Type𝓩1:Typeinst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 β†’+* 𝓩1F:FiveQuanta π“©βŠ’ anomalyCoefficient (Multiset.map (fun y => (f y.1, y.2)) F) = (f.prodMap f) F.anomalyCoefficient All goals completed! πŸ™

E.3. Anomaly coefficients is preserved under reduce

𝓩:Typeinst✝¹:CommRing 𝓩F:FiveQuanta 𝓩inst✝:DecidableEq 𝓩reduce_sum_N_mul_eq:βˆ€ (h : 𝓩 β†’ 𝓩), (Multiset.map (fun x => ↑x.2.N * h x.1) F.reduce).sum = (Multiset.map (fun x => ↑x.2.N * h x.1) F).sum⊒ F.reduce.anomalyCoefficient = F.anomalyCoefficient 𝓩:Typeinst✝¹:CommRing 𝓩F:FiveQuanta 𝓩inst✝:DecidableEq 𝓩reduce_sum_N_mul_eq:βˆ€ (h : 𝓩 β†’ 𝓩), (Multiset.map (fun x => ↑x.2.N * h x.1) F.reduce).sum = (Multiset.map (fun x => ↑x.2.N * h x.1) F).sum⊒ (Multiset.map (fun x => ↑x.2.N * x.1) F.reduce).sum = (Multiset.map (fun x => ↑x.2.N * x.1) F).sum ∧ (Multiset.map (fun x => ↑x.2.N * (x.1 * x.1)) F.reduce).sum = (Multiset.map (fun x => ↑x.2.N * (x.1 * x.1)) F).sum All goals completed! πŸ™