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.StringTheory.FTheory.SU5.Quanta.Basic
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Map
public import Physlib.StringTheory.FTheory.SU5.Charges.ViableAnomaly 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.
@[expose] public sectionA. Charge spectrum which lift to anomaly free quanta
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.
def IsAnomalyFree [DecidableEq 𝓩] [CommRing 𝓩] (c : ChargeSpectrum 𝓩) : Prop :=
∃ x ∈ Quanta.liftCharge c, x.LinearAnomalyCancellationA.1. Decidability of the proposition
instance [DecidableEq 𝓩] [CommRing 𝓩] {c : ChargeSpectrum 𝓩} : Decidable (IsAnomalyFree c) :=
Multiset.decidableExistsMultisetA.2. The proposition is preserved under mappings of charge spectra
𝓩:Type𝓩1:Typeinst✝³:DecidableEq 𝓩1inst✝²:DecidableEq 𝓩inst✝¹:CommRing 𝓩1inst✝:CommRing 𝓩f:𝓩 →+* 𝓩1c:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩F5:FiveQuanta 𝓩F10:TenQuanta 𝓩h1:{ qHd := qHd, qHu := qHu, F := F5, T := F10 } ∈ Quanta.liftCharge ch2:(Quanta.HdAnomalyCoefficient { qHd := qHd, qHu := qHu, F := F5, T := F10 }.qHd).1 +
(Quanta.HuAnomalyCoefficient { qHd := qHd, qHu := qHu, F := F5, T := F10 }.qHu).1 +
{ qHd := qHd, qHu := qHu, F := F5, T := F10 }.F.anomalyCoefficient.1 +
{ qHd := qHd, qHu := qHu, F := F5, T := F10 }.T.anomalyCoefficient.1 =
0QM:Quanta 𝓩1 :=
{ qHd := Option.map (⇑f) qHd, qHu := Option.map (⇑f) qHu, F := Multiset.map (fun y => (f y.1, y.2)) F5,
T := Multiset.map (fun y => (f y.1, y.2)) F10 }⊢ QM.reduce.LinearAnomalyCancellation
All goals completed! 🐙B. The viable charges which lift to anomaly free quanta
The viable charges which are anomaly free.
set_option maxRecDepth 2000 inlemma viable_anomalyFree (I : CodimensionOneConfig) :
(viableCharges I).filter IsAnomalyFree =
(match I with
| .same => {⟨some 2, some (-2), {-3, -1}, {-1}⟩,
⟨some 2, some (-2), {-1, 1}, {-1}⟩,
⟨some (-2), some 2, {-1, 1}, {1}⟩,
⟨some (-2), some 2, {1, 3}, {1}⟩}
| .nearestNeighbor => {⟨some (-4), some (-14), {6, 11}, {-7}⟩,
⟨some 6, some (-14), {-9, 1}, {-7}⟩,
⟨some 6, some (-14), {1, 11}, {-7}⟩,
⟨some (-14), some 6, {1, 11}, {3}⟩}
| .nextToNearestNeighbor => {⟨some 2, some 12, {-13, -8}, {6}⟩}) := I:CodimensionOneConfig⊢ Multiset.filter IsAnomalyFree (viableCharges I) =
match I with
| 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} }}
| 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} }}
| nextToNearestNeighbor => {{ qHd := some 2, qHu := some 12, Q5 := {-13, -8}, Q10 := {6} }}
⊢ ∀ (I : CodimensionOneConfig),
Multiset.filter IsAnomalyFree (viableCharges I) =
match I with
| 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} }}
| 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} }}
| nextToNearestNeighbor => {{ qHd := some 2, qHu := some 12, Q5 := {-13, -8}, Q10 := {6} }}
All goals completed! 🐙