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 10d representations

i. Overview

The 10d 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

    TenQuanta is the type of quanta of 10d representations.

    TenQuanta.toFluxesTen is the underlying FluxesTen of a TenQuanta.

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

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

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

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

iii. Table of contents

    A. The definition of TenQuanta

      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 TenQuanta

      B.1. The reduced TenQuanta has no duplicate elements

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

      B.3. Membership condition on the reduced TenQuanta

      B.4. Filter of the reduced TenQuanta 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 TenQuanta is a sum of fluxes in the original TenQuanta

      B.10. No exotics condition on the reduced TenQuanta

        B.10.1. Number of chiral U

        B.10.2. Number of anti-chiral U

        B.10.3. Number of chiral Q

        B.10.4. Number of anti-chiral Q

        B.10.5. Number of chiral E

        B.10.6. Number of anti-chiral E

        B.10.7. The NoExotics condition on the reduced TenQuanta

      B.11. Reduce member of FLuxesTen.elemsNoExotics

    C. Decomposition of a TenQuanta into basic fluxes

      C.1. Decomposition of fluxes

      C.2. Decomposition of a TenQuanta (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 TenQuanta

    D. Lifting charges to TenQuanta

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

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

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

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

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

      D.6. TenQuanta 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 TenQuanta

      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 TenQuanta

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

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

A.1. The map to underlying fluxes

The underlying FluxesTen from a TenQuanta.

def toFluxesTen (x : TenQuanta 𝓩) : FluxesTen := x.map Prod.snd

A.2. The map to underlying charges

The underlying Multiset charges from a TenQuanta.

def toCharges (x : TenQuanta 𝓩) : 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 TenQuanta.

def toChargeMap [DecidableEq 𝓩] (x : TenQuanta 𝓩) : 𝓩 β†’ Fluxes := fun z => ((x.filter fun p => p.1 = z).map Prod.snd).sum
lemma toChargeMap_of_not_mem [DecidableEq 𝓩] (x : TenQuanta 𝓩) {z : 𝓩} (h : z βˆ‰ x.toCharges) : x.toChargeMap z = 0 := 𝓩:Typeinst✝:DecidableEq 𝓩x:TenQuanta 𝓩z:𝓩h:z βˆ‰ x.toCharges⊒ x.toChargeMap z = 0 𝓩:Typeinst✝:DecidableEq 𝓩x:TenQuanta 𝓩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 TenQuanta

The reduce of TenQuanta is a new TenQuanta with all the fluxes corresponding to the same charge (i.e. representation) added together.

def reduce (x : TenQuanta 𝓩) : TenQuanta 𝓩 := x.toCharges.dedup.map fun q10 => (q10, ((x.filter (fun f => f.1 = q10)).map (fun y => y.2)).sum)

B.1. The reduced TenQuanta has no duplicate elements

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

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

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

B.3. Membership condition on the reduced TenQuanta

All goals completed! πŸ™βŸ©

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

𝓩:Typeinst✝:DecidableEq 𝓩x:TenQuanta 𝓩q:𝓩h:q ∈ x.toChargeshx:Multiset.filter (fun x => x = q) x.toCharges.dedup = {q}⊒ Multiset.map (fun q10 => (q10, (Multiset.map (fun y => y.2) (Multiset.filter (fun f => f.1 = q10) x)).sum)) {q} = {(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

All goals completed! πŸ™

B.6. Preservation of certain sums under reduction

𝓩:Typeinst✝¹:DecidableEq 𝓩M:Type u_1inst✝:AddCommMonoid Mx:TenQuanta 𝓩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:TenQuanta 𝓩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:TenQuanta 𝓩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:TenQuanta 𝓩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:TenQuanta 𝓩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:TenQuanta 𝓩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:TenQuanta 𝓩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:TenQuanta 𝓩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:TenQuanta 𝓩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:TenQuanta 𝓩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:TenQuanta 𝓩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:TenQuanta 𝓩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:TenQuanta 𝓩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 All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩x:TenQuanta 𝓩h:x.toCharges.Nodupp:𝓩 Γ— Fluxeshp:p ∈ xx_noDup:Multiset.Nodup xp':𝓩 Γ— Fluxes⊒ p' = p β†’ p' ∈ x ∧ p'.1 = p.1 𝓩:Typeinst✝:DecidableEq 𝓩x:TenQuanta 𝓩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:TenQuanta 𝓩q:𝓩h:q βˆ‰ x.toCharges⊒ q βˆ‰ x.toCharges.dedup 𝓩:Typeinst✝:DecidableEq 𝓩x:TenQuanta 𝓩q:𝓩h:q βˆ‰ x.toCharges⊒ q βˆ‰ x.toCharges All goals completed! πŸ™

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

𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩q:𝓩hq:q ∈ F.toCharges⊒ Multiset.map (fun x => x.2) (Multiset.filter (fun x => x.1 = q) F) ≀ Multiset.map Prod.snd F 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩q:𝓩hq:q ∈ F.toCharges⊒ Multiset.filter (fun x => x.1 = q) F ≀ F All goals completed! πŸ™π“©:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩q:𝓩hq:q ∈ F.toCharges⊒ Multiset.map (fun x => x.2) (Multiset.filter (fun x => x.1 = q) F) ≀ Multiset.map Prod.snd F𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩q:𝓩hq:q ∈ F.toCharges⊒ βˆƒ x x_1, βˆƒ (_ : (x, x_1) ∈ F), x = q 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩q:𝓩hq:q ∈ F.toCharges⊒ Multiset.filter (fun x => x.1 = q) F ≀ F𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩q:𝓩hq:q ∈ F.toCharges⊒ βˆƒ x x_1, βˆƒ (_ : (x, x_1) ∈ F), x = q 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩q:𝓩hq:q ∈ F.toCharges⊒ βˆƒ x x_1, βˆƒ (_ : (x, x_1) ∈ F), x = q All goals completed! πŸ™

B.10. No exotics condition on the reduced TenQuanta

B.10.1. Number of chiral U
𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralU_eq_sum:3 = (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sum⊒ (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sum = 3𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralU_eq_sum:3 = (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sum⊒ βˆ€ a ∈ Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTen, 0 ≀ a 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralU_eq_sum:3 = (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sum⊒ (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sum = 3 All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralU_eq_sum:3 = (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).suma:β„€ha:a ∈ Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTen⊒ 0 ≀ a 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralU_eq_sum:3 = (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sumf:Fluxeshf:f ∈ F.reduce.toFluxesTenha:f.M - f.N ∈ Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTen⊒ 0 ≀ f.M - f.N 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralU_eq_sum:3 = (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M - f.N) F.toFluxesTen).sumf:Fluxesha:f.M - f.N ∈ Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTenhf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesTen)⊒ 0 ≀ f.M - f.N 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsf:Fluxeshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesTen)⊒ 0 ≀ f.M - f.N 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩f:FluxesG:FluxesTenhx:G ∈ FluxesTen.elemsNoExoticshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G)⊒ 0 ≀ f.M - f.N 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩G:FluxesTenhx:G ∈ FluxesTen.elemsNoExotics⊒ βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), 0 ≀ f.M - f.N 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta π“©βŠ’ βˆ€ G ∈ FluxesTen.elemsNoExotics, βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), 0 ≀ f.M - f.N All goals completed! πŸ™
B.10.2. Number of anti-chiral U
𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExotics⊒ βˆ€ a ∈ Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTen, Β¬a < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsa:β„€ha:a ∈ Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTen⊒ Β¬a < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsf:Fluxeshf:f ∈ F.reduce.toFluxesTenha:f.M - f.N ∈ Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTen⊒ Β¬f.M - f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsf:Fluxesha:f.M - f.N ∈ Multiset.map (fun f => f.M - f.N) F.reduce.toFluxesTenhf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesTen)⊒ Β¬f.M - f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsf:Fluxeshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesTen)⊒ Β¬f.M - f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩f:FluxesG:FluxesTenhx:G ∈ FluxesTen.elemsNoExoticshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G)⊒ Β¬f.M - f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩G:FluxesTenhx:G ∈ FluxesTen.elemsNoExotics⊒ βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), Β¬f.M - f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta π“©βŠ’ βˆ€ G ∈ FluxesTen.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 Q
𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralQ_eq_sum:3 = (Multiset.map (fun f => f.M) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M) F.toFluxesTen).sum⊒ (Multiset.map (fun f => f.M) F.toFluxesTen).sum = 3𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralQ_eq_sum:3 = (Multiset.map (fun f => f.M) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M) F.toFluxesTen).sum⊒ βˆ€ a ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesTen, 0 ≀ a 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralQ_eq_sum:3 = (Multiset.map (fun f => f.M) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M) F.toFluxesTen).sum⊒ (Multiset.map (fun f => f.M) F.toFluxesTen).sum = 3 All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralQ_eq_sum:3 = (Multiset.map (fun f => f.M) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M) F.toFluxesTen).suma:β„€ha:a ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesTen⊒ 0 ≀ a 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralQ_eq_sum:3 = (Multiset.map (fun f => f.M) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M) F.toFluxesTen).sumf:Fluxeshf:f ∈ F.reduce.toFluxesTenha:f.M ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesTen⊒ 0 ≀ f.M 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralQ_eq_sum:3 = (Multiset.map (fun f => f.M) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M) F.toFluxesTen).sumf:Fluxesha:f.M ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesTenhf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesTen)⊒ 0 ≀ f.M 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsf:Fluxeshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesTen)⊒ 0 ≀ f.M 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩f:FluxesG:FluxesTenhx:G ∈ FluxesTen.elemsNoExoticshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G)⊒ 0 ≀ f.M 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩G:FluxesTenhx:G ∈ FluxesTen.elemsNoExotics⊒ βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), 0 ≀ f.M 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta π“©βŠ’ βˆ€ G ∈ FluxesTen.elemsNoExotics, βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), 0 ≀ f.M All goals completed! πŸ™
B.10.4. Number of anti-chiral Q
𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExotics⊒ βˆ€ a ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesTen, Β¬a < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsa:β„€ha:a ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesTen⊒ Β¬a < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsf:Fluxeshf:f ∈ F.reduce.toFluxesTenha:f.M ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesTen⊒ Β¬f.M < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsf:Fluxesha:f.M ∈ Multiset.map (fun f => f.M) F.reduce.toFluxesTenhf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesTen)⊒ Β¬f.M < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsf:Fluxeshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesTen)⊒ Β¬f.M < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩f:FluxesG:FluxesTenhx:G ∈ FluxesTen.elemsNoExoticshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G)⊒ Β¬f.M < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩G:FluxesTenhx:G ∈ FluxesTen.elemsNoExotics⊒ βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), Β¬f.M < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta π“©βŠ’ βˆ€ G ∈ FluxesTen.elemsNoExotics, βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), Β¬f.M < 0 All goals completed! πŸ™
B.10.5. Number of chiral E
𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralE_eq_sum:3 = (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sum⊒ (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sum = 3𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralE_eq_sum:3 = (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sum⊒ βˆ€ a ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTen, 0 ≀ a 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralE_eq_sum:3 = (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sum⊒ (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sum = 3 All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralE_eq_sum:3 = (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).suma:β„€ha:a ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTen⊒ 0 ≀ a 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralE_eq_sum:3 = (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sumf:Fluxeshf:f ∈ F.reduce.toFluxesTenha:f.M + f.N ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTen⊒ 0 ≀ f.M + f.N 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticshE:F.toFluxesTen.NoExoticsnumChiralE_eq_sum:3 = (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sumhmap:(Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTen).sum = (Multiset.map (fun f => f.M + f.N) F.toFluxesTen).sumf:Fluxesha:f.M + f.N ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTenhf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesTen)⊒ 0 ≀ f.M + f.N 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsf:Fluxeshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesTen)⊒ 0 ≀ f.M + f.N 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩f:FluxesG:FluxesTenhx:G ∈ FluxesTen.elemsNoExoticshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G)⊒ 0 ≀ f.M + f.N 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩G:FluxesTenhx:G ∈ FluxesTen.elemsNoExotics⊒ βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), 0 ≀ f.M + f.N 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta π“©βŠ’ βˆ€ G ∈ FluxesTen.elemsNoExotics, βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), 0 ≀ f.M + f.N All goals completed! πŸ™
B.10.6. Number of anti-chiral E
𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExotics⊒ βˆ€ a ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTen, Β¬a < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsa:β„€ha:a ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTen⊒ Β¬a < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsf:Fluxeshf:f ∈ F.reduce.toFluxesTenha:f.M + f.N ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTen⊒ Β¬f.M + f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsf:Fluxesha:f.M + f.N ∈ Multiset.map (fun f => f.M + f.N) F.reduce.toFluxesTenhf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesTen)⊒ Β¬f.M + f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExoticsf:Fluxeshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset F.toFluxesTen)⊒ Β¬f.M + f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩f:FluxesG:FluxesTenhx:G ∈ FluxesTen.elemsNoExoticshf:f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G)⊒ Β¬f.M + f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩G:FluxesTenhx:G ∈ FluxesTen.elemsNoExotics⊒ βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), Β¬f.M + f.N < 0 𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta π“©βŠ’ βˆ€ G ∈ FluxesTen.elemsNoExotics, βˆ€ f ∈ Multiset.map (fun s => s.sum) (Multiset.powerset G), Β¬f.M + f.N < 0 All goals completed! πŸ™
B.10.7. The NoExotics condition on the reduced TenQuanta
𝓩:Typeinst✝:DecidableEq 𝓩F:TenQuanta 𝓩hx:F.toFluxesTen ∈ FluxesTen.elemsNoExotics⊒ 3 = 3 ∧ 0 = 0 ∧ 3 = 3 ∧ 0 = 0 ∧ 3 = 3 ∧ 0 = 0 All goals completed! πŸ™

B.11. Reduce member of FLuxesTen.elemsNoExotics

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

C. Decomposition of a TenQuanta into basic fluxes

C.1. Decomposition of fluxes

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

def decomposeFluxes (f : Fluxes) : Multiset Fluxes := if f = ⟨1, 0⟩ then {⟨1, 0⟩} else if f = ⟨1, 1⟩ then {⟨1, 1⟩} else if f = ⟨1, -1⟩ then {⟨1, -1⟩} else if f = ⟨2, 1⟩ then {⟨1, 1⟩, ⟨1, 0⟩} else if f = ⟨2, -1⟩ then {⟨1, -1⟩, ⟨1, 0⟩} else if f = ⟨3, 0⟩ then {⟨1, 0⟩, ⟨1, 0⟩, ⟨1, 0⟩} else if f = ⟨2, 0⟩ then {⟨1, 0⟩, ⟨1, 0⟩} else {f}
lemma decomposeFluxes_sum_of_noExotics (f : Fluxes) (hf : βˆƒ F ∈ FluxesTen.elemsNoExotics, f ∈ F) : (decomposeFluxes f).sum = f := f:Fluxeshf:βˆƒ F ∈ FluxesTen.elemsNoExotics, f ∈ F⊒ (decomposeFluxes f).sum = f f:FluxesF:FluxesTenhF:F ∈ FluxesTen.elemsNoExoticshfF:f ∈ F⊒ (decomposeFluxes f).sum = f F:FluxesTenhF:F ∈ FluxesTen.elemsNoExotics⊒ βˆ€ f ∈ F, (decomposeFluxes f).sum = f ⊒ βˆ€ F ∈ FluxesTen.elemsNoExotics, βˆ€ f ∈ F, (decomposeFluxes f).sum = f All goals completed! πŸ™

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

The decomposition of a TenQuanta into a TenQuanta which has the same reduce by has fluxes {⟨1, 0⟩, ⟨1, 0⟩, ⟨1, 0⟩} or {⟨1, 1⟩, ⟨1, -1⟩, ⟨1, 0⟩} only.

This only works for fluxes which have no exotics or zeros.

def decompose (x : TenQuanta 𝓩) : TenQuanta 𝓩 := 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 : TenQuanta 𝓩) : (x + y).decompose = x.decompose + y.decompose := 𝓩:Typex:TenQuanta 𝓩y:TenQuanta π“©βŠ’ (x + y).decompose = x.decompose + y.decompose All goals completed! πŸ™
C.2.2. Decomposition commutes with filtering charges
𝓩: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)⊒ Multiset.filter (fun p => p.1 = q) (Multiset.map (fun f => (a.1, f)) (decomposeFluxes a.2)) + decompose (Multiset.filter (fun p => p.1 = q) x) = decompose (if a.1 = q then {a} else 0) + decompose (Multiset.filter (fun p => p.1 = q) x) 𝓩: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)⊒ Multiset.filter (fun p => p.1 = q) (Multiset.map (fun f => (a.1, f)) (decomposeFluxes a.2)) = decompose (if a.1 = q then {a} else 0) 𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩x: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:Fluxes⊒ Multiset.filter (fun p => p.1 = q) (Multiset.map (fun f_1 => ((q', f).1, f_1)) (decomposeFluxes (q', f).2)) = decompose (if (q', f).1 = q then {(q', f)} else 0) 𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩x: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:Fluxes⊒ Multiset.filter (fun p => p.1 = q) (Multiset.map (fun x => (q', x)) (if f = { M := 1, N := 0 } then {{ M := 1, N := 0 }} else if f = { M := 1, N := 1 } then {{ M := 1, N := 1 }} else if f = { M := 1, N := -1 } then {{ M := 1, N := -1 }} else if f = { M := 2, N := 1 } then { M := 1, N := 1 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 2, N := -1 } then { M := 1, N := -1 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 3, N := 0 } then { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 2, N := 0 } then { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} else {f})) = decompose (if q' = q then {(q', f)} else 0) 𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩x: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.map (fun x => (q', x)) (if f = { M := 1, N := 0 } then {{ M := 1, N := 0 }} else if f = { M := 1, N := 1 } then {{ M := 1, N := 1 }} else if f = { M := 1, N := -1 } then {{ M := 1, N := -1 }} else if f = { M := 2, N := 1 } then { M := 1, N := 1 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 2, N := -1 } then { M := 1, N := -1 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 3, N := 0 } then { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 2, N := 0 } then { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} else {f})) = decompose (if q' = q then {(q', f)} else 0)𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩x: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.map (fun x => (q', x)) (if f = { M := 1, N := 0 } then {{ M := 1, N := 0 }} else if f = { M := 1, N := 1 } then {{ M := 1, N := 1 }} else if f = { M := 1, N := -1 } then {{ M := 1, N := -1 }} else if f = { M := 2, N := 1 } then { M := 1, N := 1 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 2, N := -1 } then { M := 1, N := -1 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 3, N := 0 } then { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 2, N := 0 } then { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} else {f})) = decompose (if q' = q then {(q', f)} else 0) 𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩x: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.map (fun x => (q', x)) (if f = { M := 1, N := 0 } then {{ M := 1, N := 0 }} else if f = { M := 1, N := 1 } then {{ M := 1, N := 1 }} else if f = { M := 1, N := -1 } then {{ M := 1, N := -1 }} else if f = { M := 2, N := 1 } then { M := 1, N := 1 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 2, N := -1 } then { M := 1, N := -1 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 3, N := 0 } then { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 2, N := 0 } then { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} else {f})) = decompose (if q' = q then {(q', f)} else 0) 𝓩:Typeinst✝:DecidableEq 𝓩x:Multiset (𝓩 Γ— Fluxes)q':𝓩f:Fluxesih: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)⊒ Multiset.filter (fun p => p.1 = q') (Multiset.map (fun x => (q', x)) (if f = { M := 1, N := 0 } then {{ M := 1, N := 0 }} else if f = { M := 1, N := 1 } then {{ M := 1, N := 1 }} else if f = { M := 1, N := -1 } then {{ M := 1, N := -1 }} else if f = { M := 2, N := 1 } then { M := 1, N := 1 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 2, N := -1 } then { M := 1, N := -1 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 3, N := 0 } then { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 2, N := 0 } then { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} else {f})) = decompose (if q' = q' then {(q', f)} else 0) All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩q:𝓩x: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.map (fun x => (q', x)) (if f = { M := 1, N := 0 } then {{ M := 1, N := 0 }} else if f = { M := 1, N := 1 } then {{ M := 1, N := 1 }} else if f = { M := 1, N := -1 } then {{ M := 1, N := -1 }} else if f = { M := 2, N := 1 } then { M := 1, N := 1 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 2, N := -1 } then { M := 1, N := -1 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 3, N := 0 } then { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} else if f = { M := 2, N := 0 } then { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} else {f})) = decompose (if q' = q then {(q', f)} else 0) All goals completed! πŸ™
C.2.3. Decomposition preserves the charge map
𝓩:Typeinst✝:DecidableEq 𝓩x:TenQuanta 𝓩hx:x.toFluxesTen ∈ FluxesTen.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:TenQuanta 𝓩hx:x.toFluxesTen ∈ FluxesTen.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:TenQuanta 𝓩hx:x.toFluxesTen ∈ FluxesTen.elemsNoExoticsq:𝓩a:𝓩 Γ— Fluxesha:a ∈ Multiset.filter (fun p => p.1 = q) x⊒ (decomposeFluxes a.2).sum = a.2 𝓩:Typeinst✝:DecidableEq 𝓩x:TenQuanta 𝓩hx:x.toFluxesTen ∈ FluxesTen.elemsNoExoticsq:𝓩a:𝓩 Γ— Fluxesha:a ∈ Multiset.filter (fun p => p.1 = q) x⊒ βˆƒ F ∈ FluxesTen.elemsNoExotics, a.2 ∈ F 𝓩:Typeinst✝:DecidableEq 𝓩x:TenQuanta 𝓩hx:x.toFluxesTen ∈ FluxesTen.elemsNoExoticsq:𝓩a:𝓩 Γ— Fluxesha:a ∈ Multiset.filter (fun p => p.1 = q) x⊒ x.toFluxesTen ∈ FluxesTen.elemsNoExotics ∧ a.2 ∈ x.toFluxesTen 𝓩:Typeinst✝:DecidableEq 𝓩x:TenQuanta 𝓩q:𝓩a:𝓩 Γ— Fluxeshx:Multiset.map Prod.snd x ∈ FluxesTen.elemsNoExoticsha:a ∈ x ∧ a.1 = q⊒ βˆƒ a_1, (a_1, a.2) ∈ x 𝓩:Typeinst✝:DecidableEq 𝓩x:TenQuanta 𝓩q:𝓩a:𝓩 Γ— Fluxeshx:Multiset.map Prod.snd x ∈ FluxesTen.elemsNoExoticsha:a ∈ x ∧ a.1 = q⊒ (a.1, a.2) ∈ x All goals completed! πŸ™
C.2.4. Decomposition preserves the charges
𝓩:Typeinst✝:DecidableEq 𝓩x:TenQuanta 𝓩hx:x.toFluxesTen ∈ FluxesTen.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:TenQuanta 𝓩hx:x.toFluxesTen ∈ FluxesTen.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:TenQuanta 𝓩hx:x.toFluxesTen ∈ FluxesTen.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! πŸ™
C.2.6. Fluxes of the decomposition of a TenQuanta
𝓩:Typex:TenQuanta 𝓩hx✝:x.toFluxesTen ∈ FluxesTen.elemsNoExoticshx:(Multiset.bind x fun a => decomposeFluxes a.2) = Multiset.bind x.toFluxesTen fun a => decomposeFluxes a⊒ (Multiset.bind x.toFluxesTen fun a => decomposeFluxes a) = { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} ∨ (Multiset.bind x.toFluxesTen fun a => decomposeFluxes a) = { M := 1, N := 1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ {{ M := 1, N := 0 }} 𝓩:Typex:TenQuanta 𝓩hx:x.toFluxesTen ∈ FluxesTen.elemsNoExotics⊒ (Multiset.bind x.toFluxesTen fun a => decomposeFluxes a) = { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} ∨ (Multiset.bind x.toFluxesTen fun a => decomposeFluxes a) = { M := 1, N := 1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ {{ M := 1, N := 0 }} 𝓩:Typex:TenQuanta 𝓩F:FluxesTenhx:F ∈ FluxesTen.elemsNoExotics⊒ (Multiset.bind F fun a => decomposeFluxes a) = { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} ∨ (Multiset.bind F fun a => decomposeFluxes a) = { M := 1, N := 1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ {{ M := 1, N := 0 }} 𝓩:Typex:TenQuanta π“©βŠ’ βˆ€ F ∈ FluxesTen.elemsNoExotics, (Multiset.bind F fun a => decomposeFluxes a) = { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} ∨ (Multiset.bind F fun a => decomposeFluxes a) = { M := 1, N := 1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ {{ M := 1, N := 0 }} All goals completed! πŸ™

D. Lifting charges to TenQuanta

D.1. liftCharge c: multiset of ten-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 TenQuanta which do not have exotics, duplicate charges or zero fluxes, which map down to c. This is defined to be as efficient as possible.

def liftCharge (c : Finset 𝓩) : Multiset (TenQuanta 𝓩) := /- The {(1, 0), (1, 0), (1, 0)} case. -/ /- The multisets of cardinality 3 containing 3 elements of `c`. -/ let S10 : Multiset (Multiset 𝓩) := toMultisetsThree c let F1 : Multiset (TenQuanta 𝓩) := (S10.map (fun s => s.map (fun z => (z, ⟨1, 0⟩)))).filter (fun s => c.val ≀ s.toCharges) /- The {(1, 1), (1, -1), (1, 0)} case. -/ let F2 : Multiset (TenQuanta 𝓩) := ((c.product <| c.product <| c).val.map fun (x, y, z) => {(x, ⟨1, 1⟩), (y, ⟨1, -1⟩), (z, ⟨1, 0⟩)}).filter (fun s => c.val ≀ s.toCharges) /- All together-/ (F1 + F2).map reduce

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

𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:TenQuanta 𝓩h:a ∈ Multiset.filter (fun s => c.val ≀ s.toCharges) (Multiset.map (fun s => Multiset.map (fun z => (z, { M := 1, N := 0 })) s) (toMultisetsThree c)) + Multiset.filter (fun s => c.val ≀ s.toCharges) (Multiset.map (fun x => match x with | (x, y, z) => {(x, { M := 1, N := 1 }), (y, { M := 1, N := -1 }), (z, { M := 1, N := 0 })}) (c.product (c.product c)).val)⊒ a.toCharges.dedup.toFinset = c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:TenQuanta 𝓩h:(βˆƒ a_1, (a_1.toFinset βŠ† c ∧ a_1.card = 3) ∧ Multiset.map (fun z => (z, { M := 1, N := 0 })) a_1 = a) ∧ c.val ≀ a.toCharges ∨ (βˆƒ a_1 a_2 b, (a_1 ∈ c ∧ a_2 ∈ c ∧ b ∈ c) ∧ (a_1, { M := 1, N := 1 }) ::β‚˜ (a_2, { M := 1, N := -1 }) ::β‚˜ {(b, { M := 1, N := 0 })} = a) ∧ c.val ≀ a.toCharges⊒ a.toCharges.dedup.toFinset = c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:TenQuanta 𝓩h:(βˆƒ a_1, (a_1.toFinset βŠ† c ∧ a_1.card = 3) ∧ Multiset.map (fun z => (z, { M := 1, N := 0 })) a_1 = a) ∧ c.val ≀ a.toCharges⊒ a.toCharges.dedup.toFinset = c𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:TenQuanta 𝓩h:(βˆƒ a_1 a_2 b, (a_1 ∈ c ∧ a_2 ∈ c ∧ b ∈ c) ∧ (a_1, { M := 1, N := 1 }) ::β‚˜ (a_2, { M := 1, N := -1 }) ::β‚˜ {(b, { M := 1, N := 0 })} = a) ∧ c.val ≀ a.toCharges⊒ a.toCharges.dedup.toFinset = c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:TenQuanta 𝓩h:(βˆƒ a_1, (a_1.toFinset βŠ† c ∧ a_1.card = 3) ∧ Multiset.map (fun z => (z, { M := 1, N := 0 })) a_1 = a) ∧ c.val ≀ a.toCharges⊒ a.toCharges.dedup.toFinset = c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s:Multiset 𝓩h:s.toFinset βŠ† c ∧ s.card = 3h':c.val ≀ toCharges (Multiset.map (fun z => (z, { M := 1, N := 0 })) s)⊒ (toCharges (Multiset.map (fun z => (z, { M := 1, N := 0 })) s)).dedup.toFinset = c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s:Multiset 𝓩h:s.toFinset βŠ† c ∧ s.card = 3h':c.val ≀ s⊒ s.toFinset = c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s:Multiset 𝓩h:s.toFinset βŠ† c ∧ s.card = 3h':c.val ≀ sa:π“©βŠ’ a ∈ s.toFinset ↔ a ∈ c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s:Multiset 𝓩h:s.toFinset βŠ† c ∧ s.card = 3h':c.val ≀ sa:π“©βŠ’ a ∈ s ↔ a ∈ c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s:Multiset 𝓩h:s.toFinset βŠ† c ∧ s.card = 3h':c.val ≀ sa:π“©βŠ’ a ∈ s β†’ a ∈ c𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s:Multiset 𝓩h:s.toFinset βŠ† c ∧ s.card = 3h':c.val ≀ sa:π“©βŠ’ a ∈ c β†’ a ∈ s 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s:Multiset 𝓩h:s.toFinset βŠ† c ∧ s.card = 3h':c.val ≀ sa:π“©βŠ’ a ∈ s β†’ a ∈ c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s:Multiset 𝓩h:s.toFinset βŠ† c ∧ s.card = 3h':c.val ≀ sa:𝓩hr:a ∈ s⊒ a ∈ c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s:Multiset 𝓩h:s.toFinset βŠ† c ∧ s.card = 3h':c.val ≀ sa:𝓩hr:a ∈ s⊒ a ∈ s.toFinset All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s:Multiset 𝓩h:s.toFinset βŠ† c ∧ s.card = 3h':c.val ≀ sa:π“©βŠ’ a ∈ c β†’ a ∈ s 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s:Multiset 𝓩h:s.toFinset βŠ† c ∧ s.card = 3h':c.val ≀ sa:𝓩hr:a ∈ c⊒ a ∈ s All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:TenQuanta 𝓩h:(βˆƒ a_1 a_2 b, (a_1 ∈ c ∧ a_2 ∈ c ∧ b ∈ c) ∧ (a_1, { M := 1, N := 1 }) ::β‚˜ (a_2, { M := 1, N := -1 }) ::β‚˜ {(b, { M := 1, N := 0 })} = a) ∧ c.val ≀ a.toCharges⊒ a.toCharges.dedup.toFinset = c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩q3:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ toCharges ((q1, { M := 1, N := 1 }) ::β‚˜ (q2, { M := 1, N := -1 }) ::β‚˜ {(q3, { M := 1, N := 0 })})⊒ (toCharges ((q1, { M := 1, N := 1 }) ::β‚˜ (q2, { M := 1, N := -1 }) ::β‚˜ {(q3, { M := 1, N := 0 })})).dedup.toFinset = c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩q3:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ q1 ::β‚˜ q2 ::β‚˜ {q3}⊒ {q1, q2, q3} = c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩q3:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ q1 ::β‚˜ q2 ::β‚˜ {q3}⊒ βˆ€ (a : 𝓩), a ∈ c ↔ a ∈ {q1, q2, q3} 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩q3:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ q1 ::β‚˜ q2 ::β‚˜ {q3}a:π“©βŠ’ a ∈ c ↔ a ∈ {q1, q2, q3} 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩q3:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ q1 ::β‚˜ q2 ::β‚˜ {q3}a:π“©βŠ’ a ∈ c β†’ a ∈ {q1, q2, q3}𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩q3:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ q1 ::β‚˜ q2 ::β‚˜ {q3}a:π“©βŠ’ a ∈ {q1, q2, q3} β†’ a ∈ c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩q3:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ q1 ::β‚˜ q2 ::β‚˜ {q3}a:π“©βŠ’ a ∈ c β†’ a ∈ {q1, q2, q3} 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩q3:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ q1 ::β‚˜ q2 ::β‚˜ {q3}a:𝓩hr:a ∈ c⊒ a ∈ {q1, q2, q3} All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩q3:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ q1 ::β‚˜ q2 ::β‚˜ {q3}a:π“©βŠ’ a ∈ {q1, q2, q3} β†’ a ∈ c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩q3:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ q1 ::β‚˜ q2 ::β‚˜ {q3}a:𝓩hr:a ∈ {q1, q2, q3}⊒ a ∈ c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩q3:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ q1 ::β‚˜ q2 ::β‚˜ {q3}a:𝓩hr:a = q1 ∨ a = q2 ∨ a = q3⊒ a ∈ c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q2:𝓩q3:𝓩a:𝓩h:a ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ a ::β‚˜ q2 ::β‚˜ {q3}⊒ a ∈ c𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q3:𝓩a:𝓩h:q1 ∈ c ∧ a ∈ c ∧ q3 ∈ ch':c.val ≀ q1 ::β‚˜ a ::β‚˜ {q3}⊒ a ∈ c𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩a:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ a ∈ ch':c.val ≀ q1 ::β‚˜ q2 ::β‚˜ {a}⊒ a ∈ c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q2:𝓩q3:𝓩a:𝓩h:a ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch':c.val ≀ a ::β‚˜ q2 ::β‚˜ {q3}⊒ a ∈ c All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q3:𝓩a:𝓩h:q1 ∈ c ∧ a ∈ c ∧ q3 ∈ ch':c.val ≀ q1 ::β‚˜ a ::β‚˜ {q3}⊒ a ∈ c All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩a:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ a ∈ ch':c.val ≀ q1 ::β‚˜ q2 ::β‚˜ {a}⊒ a ∈ c All goals completed! πŸ™

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

𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta 𝓩h:x ∈ Multiset.filter (fun s => c.val ≀ s.toCharges) (Multiset.map (fun s => Multiset.map (fun z => (z, { M := 1, N := 0 })) s) (toMultisetsThree c)) + Multiset.filter (fun s => c.val ≀ s.toCharges) (Multiset.map (fun x => match x with | (x, y, z) => {(x, { M := 1, N := 1 }), (y, { M := 1, N := -1 }), (z, { M := 1, N := 0 })}) (c.product (c.product c)).val)⊒ x.toCharges.dedup.Nodup All goals completed! πŸ™

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

𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩s:Multiset 𝓩h:s.toFinset βŠ† c ∧ s.card = 3h'✝:reduce (Multiset.map (fun z => (z, { M := 1, N := 0 })) s) ∈ liftCharge ch':c.val ≀ toCharges (Multiset.map (fun z => (z, { M := 1, N := 0 })) s)⊒ Multiset.replicate 3 { M := 1, N := 0 } = { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩a:TenQuanta 𝓩h':a.reduce ∈ liftCharge ch:(βˆƒ a_1 a_2 b, (a_1 ∈ c ∧ a_2 ∈ c ∧ b ∈ c) ∧ (a_1, { M := 1, N := 1 }) ::β‚˜ (a_2, { M := 1, N := -1 }) ::β‚˜ {(b, { M := 1, N := 0 })} = a) ∧ c.val ≀ a.toCharges⊒ a.toFluxesTen = { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} ∨ a.toFluxesTen = { M := 1, N := 1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ {{ M := 1, N := 0 }} 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩q1:𝓩q2:𝓩q3:𝓩h:q1 ∈ c ∧ q2 ∈ c ∧ q3 ∈ ch'✝:reduce ((q1, { M := 1, N := 1 }) ::β‚˜ (q2, { M := 1, N := -1 }) ::β‚˜ {(q3, { M := 1, N := 0 })}) ∈ liftCharge ch':c.val ≀ toCharges ((q1, { M := 1, N := 1 }) ::β‚˜ (q2, { M := 1, N := -1 }) ::β‚˜ {(q3, { M := 1, N := 0 })})⊒ toFluxesTen ((q1, { M := 1, N := 1 }) ::β‚˜ (q2, { M := 1, N := -1 }) ::β‚˜ {(q3, { M := 1, N := 0 })}) = { M := 1, N := 0 } ::β‚˜ { M := 1, N := 0 } ::β‚˜ {{ M := 1, N := 0 }} ∨ toFluxesTen ((q1, { M := 1, N := 1 }) ::β‚˜ (q2, { M := 1, N := -1 }) ::β‚˜ {(q3, { M := 1, N := 0 })}) = { M := 1, N := 1 } ::β‚˜ { M := 1, N := -1 } ::β‚˜ {{ M := 1, N := 0 }} All goals completed! πŸ™π“©:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta 𝓩h:x.toCharges.toFinset = ch2':x.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }}p1:𝓩 Γ— Fluxeshp1:p1 ∈ xhp1_2:p1.2 = { M := 1, N := 1 }p2:𝓩 Γ— Fluxeshp2:p2 ∈ Multiset.erase x p1hp2_2:p2.2 = { M := 1, N := -1 }p3:𝓩 Γ— Fluxeshp3:(Multiset.erase x p1).erase p2 = {p3}hp3_2:p3.2 = { M := 1, N := 0 }⊒ x.toCharges.toFinset.val ≀ x.toCharges 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta 𝓩h:x.toCharges.toFinset = ch2':x.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }}p1:𝓩 Γ— Fluxeshp1:p1 ∈ xhp1_2:p1.2 = { M := 1, N := 1 }p2:𝓩 Γ— Fluxeshp2:p2 ∈ Multiset.erase x p1hp2_2:p2.2 = { M := 1, N := -1 }p3:𝓩 Γ— Fluxeshp3:(Multiset.erase x p1).erase p2 = {p3}hp3_2:p3.2 = { M := 1, N := 0 }⊒ x.toCharges.dedup ≀ x.toCharges All goals completed! πŸ™lemma mem_liftCharge_iff_exists (c : Finset 𝓩) {x : TenQuanta 𝓩} : x ∈ liftCharge c ↔ βˆƒ a : TenQuanta 𝓩, a.reduce = x ∧ a.toCharges.toFinset = c ∧ (a.toFluxesTen = {⟨1, 0⟩, ⟨1, 0⟩, ⟨1, 0⟩} ∨ a.toFluxesTen = {⟨1, 1⟩, ⟨1, -1⟩, ⟨1, 0⟩}) := 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta π“©βŠ’ x ∈ liftCharge c ↔ βˆƒ a, a.reduce = x ∧ a.toCharges.toFinset = c ∧ (a.toFluxesTen = {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }} ∨ a.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }}) 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta π“©βŠ’ x ∈ liftCharge c β†’ βˆƒ a, a.reduce = x ∧ a.toCharges.toFinset = c ∧ (a.toFluxesTen = {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }} ∨ a.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }})𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta π“©βŠ’ (βˆƒ a, a.reduce = x ∧ a.toCharges.toFinset = c ∧ (a.toFluxesTen = {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }} ∨ a.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }})) β†’ x ∈ liftCharge c 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta π“©βŠ’ x ∈ liftCharge c β†’ βˆƒ a, a.reduce = x ∧ a.toCharges.toFinset = c ∧ (a.toFluxesTen = {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }} ∨ a.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }}) All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta π“©βŠ’ (βˆƒ a, a.reduce = x ∧ a.toCharges.toFinset = c ∧ (a.toFluxesTen = {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }} ∨ a.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }})) β†’ x ∈ liftCharge c All goals completed! πŸ™

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

𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta 𝓩h1:x.toCharges.toFinset = chf:0 ∈ x.reduce.toFluxesTenhx:0 ∈ Multiset.map (fun s => s.sum) (Multiset.filter (fun s => s β‰  0) (Multiset.powerset {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }}))h2:x.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }}⊒ False 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta 𝓩h1:x.toCharges.toFinset = chf:0 ∈ x.reduce.toFluxesTenh2:x.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }}⊒ 0 ∈ Multiset.map (fun s => s.sum) (Multiset.filter (fun s => s β‰  0) (Multiset.powerset {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }})) β†’ False All goals completed! πŸ™

D.6. TenQuanta in liftCharge c have no exotics

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

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

𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta 𝓩h1:x.toFluxesTen.NoExoticsh2:x.toFluxesTen.HasNoZeroh3:x.toCharges.toFinset = ch4:x.toCharges.Noduphf:x.toFluxesTen ∈ FluxesTen.elemsNoExotics⊒ x.toCharges.dedup.toFinset = x.toCharges.toFinset All goals completed! πŸ™ 𝓩:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta 𝓩h1:x.toFluxesTen.NoExoticsh2:x.toFluxesTen.HasNoZeroh3:x.toCharges.toFinset = ch4:x.toCharges.Noduphf:x.toFluxesTen ∈ FluxesTen.elemsNoExotics⊒ x.decompose.toFluxesTen = {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }} ∨ x.decompose.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }} All goals completed! πŸ™π“©:Typeinst✝:DecidableEq 𝓩c:Finset 𝓩x:TenQuanta 𝓩h1:x.toFluxesTen.NoExotics ∧ x.toFluxesTen.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:TenQuanta 𝓩h:F.toFluxesTen ∈ FluxesTen.elemsNoExotics ∧ F.toCharges.toFinset = c ∧ F.toCharges.Nodup⊒ (toCharges (Multiset.map (fun y => (f y.1, y.2)) F)).dedup.Nodup All goals completed! πŸ™

E. Anomaly cancellation coefficients

E.1. Anomaly coefficients of a TenQuanta

The anomaly coefficient of a TenQuanta is given by the pair of integers: (βˆ‘α΅’ qα΅’ Nα΅’, 3 * βˆ‘α΅’ 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 : TenQuanta 𝓩) : 𝓩 Γ— 𝓩 := ((F.map fun x => x.2.2 β€’ x.1).sum, 3 * (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 : TenQuanta 𝓩) : TenQuanta.anomalyCoefficient (F.map fun y => (f y.1, y.2) : TenQuanta 𝓩1) = (f.prodMap f) F.anomalyCoefficient := 𝓩:Type𝓩1:Typeinst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 β†’+* 𝓩1F:TenQuanta π“©βŠ’ 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 𝓩inst✝:DecidableEq 𝓩F:TenQuanta 𝓩weighted_N_sum_eq:βˆ€ (w : 𝓩 β†’ 𝓩), (Multiset.map (fun x => ↑x.2.N * w x.1) F.reduce).sum = (Multiset.map (fun x => ↑x.2.N * w x.1) F).sum⊒ F.reduce.anomalyCoefficient = F.anomalyCoefficient 𝓩:Typeinst✝¹:CommRing 𝓩inst✝:DecidableEq 𝓩F:TenQuanta 𝓩weighted_N_sum_eq:βˆ€ (w : 𝓩 β†’ 𝓩), (Multiset.map (fun x => ↑x.2.N * w x.1) F.reduce).sum = (Multiset.map (fun x => ↑x.2.N * w 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 ∧ 3 * (Multiset.map (fun x => ↑x.2.N * (x.1 * x.1)) F.reduce).sum = 3 * (Multiset.map (fun x => ↑x.2.N * (x.1 * x.1)) F).sum All goals completed! πŸ™