Anomaly cancellation

i. Overview

In this module we do two things. The first is to define a proposition IsAnomalyFree on a ChargeSpectrum which states that the charge spectrum can be lifted to an anomaly-free Quanta with fluxes which do not have exotics.

We then find all the viable charges given a configuration of the sections in codimension one fiber CodimensionOneConfig that can be lifted to an anomaly-free Quanta with fluxes which do not have exotics.

ii. Key results

• IsAnomalyFree : The proposition on a ChargeSpectrum that it can be lifted to an anomaly-free Quanta with fluxes which do not have exotics.
• viable_anomalyFree : The viable charges given a configuration of the sections in codimension one fiber CodimensionOneConfig which can be lifted to an anomaly-free Quanta with fluxes which do not have exotics.

iii. Table of contents

• A. Charge spectrum which lift to anomaly free quanta
  • A.1. Decidability of the proposition
  • A.2. The proposition is preserved under mappings of charge spectra
• B. The viable charges which lift to anomaly free quanta

iv. References

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

A. Charge spectrum which lift to anomaly free quanta

def FTheory.SU5.ChargeSpectrum.IsAnomalyFree {𝓩 : Type} [DecidableEq 𝓩] [CommRing 𝓩] (c : SuperSymmetry.SU5.ChargeSpectrum 𝓩) : Prop

The condition on a collection of charges c that it extends to an anomaly free Quanta. That anomaly free Quanta is not tracked by this proposition.

Equations

• FTheory.SU5.ChargeSpectrum.IsAnomalyFree c = ∃ x ∈ FTheory.SU5.Quanta.liftCharge c, x.LinearAnomalyCancellation

A.1. Decidability of the proposition

instance FTheory.SU5.ChargeSpectrum.instDecidableIsAnomalyFree {𝓩 : Type} [DecidableEq 𝓩] [CommRing 𝓩] {c : SuperSymmetry.SU5.ChargeSpectrum 𝓩} : Decidable (IsAnomalyFree c)

Equations

• FTheory.SU5.ChargeSpectrum.instDecidableIsAnomalyFree = Multiset.decidableExistsMultiset

A.2. The proposition is preserved under mappings of charge spectra

theorem FTheory.SU5.ChargeSpectrum.isAnomalyFree_map {𝓩 𝓩1 : Type} [DecidableEq 𝓩1] [DecidableEq 𝓩] [CommRing 𝓩1] [CommRing 𝓩] (f : 𝓩 →+* 𝓩1) {c : SuperSymmetry.SU5.ChargeSpectrum 𝓩} (h : IsAnomalyFree c) : IsAnomalyFree (SuperSymmetry.SU5.ChargeSpectrum.map f.toAddMonoidHom c)

B. The viable charges which lift to anomaly free quanta

theorem FTheory.SU5.ChargeSpectrum.viable_anomalyFree (I : CodimensionOneConfig) : Multiset.filter IsAnomalyFree (viableCharges I) = match I with | CodimensionOneConfig.same => {{ qHd := some 2, qHu := some (-2), Q5 := {-3, -1}, Q10 := {-1} }, { qHd := some 2, qHu := some (-2), Q5 := {-1, 1}, Q10 := {-1} }, { qHd := some (-2), qHu := some 2, Q5 := {-1, 1}, Q10 := {1} }, { qHd := some (-2), qHu := some 2, Q5 := {1, 3}, Q10 := {1} }} | CodimensionOneConfig.nearestNeighbor => {{ qHd := some (-4), qHu := some (-14), Q5 := {6, 11}, Q10 := {-7} }, { qHd := some 6, qHu := some (-14), Q5 := {-9, 1}, Q10 := {-7} }, { qHd := some 6, qHu := some (-14), Q5 := {1, 11}, Q10 := {-7} }, { qHd := some (-14), qHu := some 6, Q5 := {1, 11}, Q10 := {3} }} | CodimensionOneConfig.nextToNearestNeighbor => {{ qHd := some 2, qHu := some 12, Q5 := {-13, -8}, Q10 := {6} }}

The viable charges which are anomaly free.