Anomaly cancellation

In this module we define the proposition IsAnomalyFree on charges, which states that the charges can be extended to quanta which are anomaly free.

We give the viable charges which are anomaly free for each of the three codimension one configurations. This is in the lemma viable_anomalyFree.

Anomaly coefficents of charges

def FTheory.SU5.Charges.IsAnomalyFree {𝓩 : Type} [DecidableEq 𝓩] [CommRing 𝓩] (c : SuperSymmetry.SU5.Charges 𝓩) : 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.Charges.IsAnomalyFree c = ∃ x ∈ FTheory.SU5.Quanta.ofChargesExpand c, FTheory.SU5.Quanta.AnomalyCancellation x.1 x.2.1 x.2.2.1 x.2.2.2

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

Equations

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

The IsAnomalyFree condition under a map

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

The viable charges which are anomaly free.

theorem FTheory.SU5.Charges.viable_anomalyFree (I : CodimensionOneConfig) : Multiset.filter IsAnomalyFree (viableCharges I) = match I with | CodimensionOneConfig.same => {(some 2, some (-2), {-1, 1}, {-1}), (some (-2), some 2, {-1, 1}, {1})} | CodimensionOneConfig.nearestNeighbor => {(some 6, some (-14), {-9, 1}, {-7})} | CodimensionOneConfig.nextToNearestNeighbor => ∅

The viable charges which are anomaly free.