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.FiveQuanta
public import Physlib.StringTheory.FTheory.SU5.Quanta.TenQuantaQuanta of representations
i. Overview
In SU(5) × U(1) F-theory theory, each 5-bar and 10d representation carries with it 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
Quanta : The structure containing the quantum numbers of the 5-bar and 10d
representations, as well as the charges of the Hd and Hu particles.
Quanta.liftCharge : Lifting a ChargeSpectrum to a multiset of Quanta
which have no chiral exotics and no zero fluxes.
Quanta.AnomalyCancellation : The anomaly cancellation conditions on a Quanta.
iii. Table of contents
A. The Quanta structure
A.1. Repr instance on Quanta
A.2. Extensionality lemma
A.3. Decidable equality instance
A.4. Map to the underlying ChargeSpectrum
B. The reduction of a Quanta
C. Lifting a charge spectrum to quanta with no exotics or zero fluxes
C.1. Simplification of membership in the liftCharge multiset
C.2. Charge spectrum of a lifted quanta
D. Anomaly cancellation conditions
D.1. The anomaly coefficient of Hd
D.2. The anomaly coefficient of Hu
D.3. The anomaly cancellation condition propositions
D.3.1. The propositions are decidable
iv. References
A reference for the anomaly cancellation conditions is arXiv:1401.5084 equation 22.
@[expose] public sectionA. The Quanta structure
The quanta associated with the representations in a SU(5) x U(1) F-theory.
This contains the value of the charges and the flux integers (M, N) for the
5-bar matter content and the 10d matter content, and the charges of the Hd and
Hu particles (there values of (M,N) are not included as they are
forced to be (0, 1) and (0, -1) respectively.
The charge of the Hd matter field.
The negative charge of the Hu matter field. In other words the charge of the Hu considered as a 5-bar field.
The quanta carried by the 5-bar matter fields.
The quanta carried by the 10d matter fields.
structure Quanta (𝓩 : Type := ℤ) where qHd : Option 𝓩 qHu : Option 𝓩 F : FiveQuanta 𝓩 T : TenQuanta 𝓩
A.1. Repr instance on Quanta
unsafe instance [Repr 𝓩] : Repr (Quanta 𝓩) where
reprPrec x _ := "⟨" ++
repr x.qHd ++ ", " ++
repr x.qHu ++ ", " ++
repr x.F ++ ", " ++
repr x.T ++
"⟩"A.2. Extensionality lemma
@[ext]
lemma ext {𝓩 : Type} {x y : Quanta 𝓩} (h1 : x.qHd = y.qHd) (h2 : x.qHu = y.qHu)
(h3 : x.F = y.F) (h4 : x.T = y.T) : x = y := 𝓩:Typex:Quanta 𝓩y:Quanta 𝓩h1:x.qHd = y.qHdh2:x.qHu = y.qHuh3:x.F = y.Fh4:x.T = y.T⊢ x = y
𝓩:Typey:Quanta 𝓩qHd✝:Option 𝓩qHu✝:Option 𝓩F✝:FiveQuanta 𝓩T✝:TenQuanta 𝓩h1:{ qHd := qHd✝, qHu := qHu✝, F := F✝, T := T✝ }.qHd = y.qHdh2:{ qHd := qHd✝, qHu := qHu✝, F := F✝, T := T✝ }.qHu = y.qHuh3:{ qHd := qHd✝, qHu := qHu✝, F := F✝, T := T✝ }.F = y.Fh4:{ qHd := qHd✝, qHu := qHu✝, F := F✝, T := T✝ }.T = y.T⊢ { qHd := qHd✝, qHu := qHu✝, F := F✝, T := T✝ } = y; 𝓩:TypeqHd✝¹:Option 𝓩qHu✝¹:Option 𝓩F✝¹:FiveQuanta 𝓩T✝¹:TenQuanta 𝓩qHd✝:Option 𝓩qHu✝:Option 𝓩F✝:FiveQuanta 𝓩T✝:TenQuanta 𝓩h1:{ qHd := qHd✝¹, qHu := qHu✝¹, F := F✝¹, T := T✝¹ }.qHd = { qHd := qHd✝, qHu := qHu✝, F := F✝, T := T✝ }.qHdh2:{ qHd := qHd✝¹, qHu := qHu✝¹, F := F✝¹, T := T✝¹ }.qHu = { qHd := qHd✝, qHu := qHu✝, F := F✝, T := T✝ }.qHuh3:{ qHd := qHd✝¹, qHu := qHu✝¹, F := F✝¹, T := T✝¹ }.F = { qHd := qHd✝, qHu := qHu✝, F := F✝, T := T✝ }.Fh4:{ qHd := qHd✝¹, qHu := qHu✝¹, F := F✝¹, T := T✝¹ }.T = { qHd := qHd✝, qHu := qHu✝, F := F✝, T := T✝ }.T⊢ { qHd := qHd✝¹, qHu := qHu✝¹, F := F✝¹, T := T✝¹ } = { qHd := qHd✝, qHu := qHu✝, F := F✝, T := T✝ };
All goals completed! 🐙A.3. Decidable equality instance
instance [DecidableEq 𝓩] : DecidableEq (Quanta 𝓩) := fun x y =>
decidable_of_iff (x.qHd = y.qHd ∧ x.qHu = y.qHu ∧ x.F = y.F ∧ x.T = y.T) Quanta.ext_iff.symm
A.4. Map to the underlying ChargeSpectrum
The underlying ChargeSpectrum of a Quanta.
def toCharges [DecidableEq 𝓩] (x : Quanta 𝓩) : ChargeSpectrum 𝓩 where
qHd := x.qHd
qHu := x.qHu
Q5 := x.F.toCharges.toFinset
Q10 := x.T.toCharges.toFinsetlemma toCharges_qHd [DecidableEq 𝓩] (x : Quanta 𝓩) : (toCharges x).qHd = x.qHd := rfllemma toCharges_qHu [DecidableEq 𝓩] (x : Quanta 𝓩) : (toCharges x).qHu = x.qHu := rfl
B. The reduction of a Quanta
The reduce of Quanta is a new Quanta with all the fluxes corresponding to the same
charge (i.e. representation) added together.
def reduce [DecidableEq 𝓩] (x : Quanta 𝓩) : Quanta 𝓩 where
qHd := x.qHd
qHu := x.qHu
F := x.F.reduce
T := x.T.reduceC. Lifting a charge spectrum to quanta with no exotics or zero fluxes
Lifting a charge spectrum to quanta which do not have exotics and which have no zero flux.
def liftCharge [DecidableEq 𝓩] (c : ChargeSpectrum 𝓩) : Multiset (Quanta 𝓩) :=
let Q5s := FiveQuanta.liftCharge c.Q5
let Q10s := TenQuanta.liftCharge c.Q10
Q5s.bind <| fun Q5 =>
Q10s.map <| fun Q10 =>
⟨c.qHd, c.qHu, Q5, Q10⟩C.1. Simplification of membership in the liftCharge multiset
All goals completed! 🐙⟩C.2. Charge spectrum of a lifted quanta
𝓩:Typeinst✝:DecidableEq 𝓩c:ChargeSpectrum 𝓩x:Quanta 𝓩h1:x.qHd = c.qHdh2:x.qHu = c.qHuh3:x.F.toFluxesFive ∈ FluxesFive.elemsNoExotics ∧ x.F.toCharges.toFinset = c.Q5 ∧ x.F.toCharges.Noduph4:x.T.toFluxesTen ∈ FluxesTen.elemsNoExotics ∧ x.T.toCharges.toFinset = c.Q10 ∧ x.T.toCharges.Nodup⊢ x.toCharges = c
All goals completed! 🐙D. Anomaly cancellation conditions
There are two anomaly cancellation conditions in the SU(5)×U(1) model which involve the
U(1) charges. These are
∑ᵢ qᵢ Nᵢ + ∑ₐ qₐ Nₐ = 0 where the first sum is over all 5-bar representations and the second
is over all 10d representations.
∑ᵢ qᵢ² Nᵢ + 3 * ∑ₐ qₐ² Nₐ = 0 where the first sum is over all 5-bar representations and the
second is over all 10d representations.
According to arXiv:1401.5084 it is unclear whether this second condition should necessarily be imposed.
D.1. The anomaly coefficient of Hd
The pair of anomaly cancellation coefficients associated with the Hd particle.
def HdAnomalyCoefficient [CommRing 𝓩] (qHd : Option 𝓩) : 𝓩 × 𝓩 :=
match qHd with
| none => (0, 0)
| some qHd => (qHd, qHd ^ 2)@[simp]
lemma HdAnomalyCoefficient_map {𝓩 𝓩1 : Type} [CommRing 𝓩] [CommRing 𝓩1]
(f : 𝓩 →+* 𝓩1) (qHd : Option 𝓩) :
HdAnomalyCoefficient (qHd.map f) = (f.prodMap f) (HdAnomalyCoefficient qHd) := 𝓩:Type𝓩1:Typeinst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 →+* 𝓩1qHd:Option 𝓩⊢ HdAnomalyCoefficient (Option.map (⇑f) qHd) = (f.prodMap f) (HdAnomalyCoefficient qHd)
𝓩:Type𝓩1:Typeinst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 →+* 𝓩1⊢ HdAnomalyCoefficient (Option.map (⇑f) none) = (f.prodMap f) (HdAnomalyCoefficient none)𝓩:Type𝓩1:Typeinst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 →+* 𝓩1val✝:𝓩⊢ HdAnomalyCoefficient (Option.map (⇑f) (some val✝)) = (f.prodMap f) (HdAnomalyCoefficient (some val✝)) 𝓩:Type𝓩1:Typeinst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 →+* 𝓩1⊢ HdAnomalyCoefficient (Option.map (⇑f) none) = (f.prodMap f) (HdAnomalyCoefficient none)𝓩:Type𝓩1:Typeinst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 →+* 𝓩1val✝:𝓩⊢ HdAnomalyCoefficient (Option.map (⇑f) (some val✝)) = (f.prodMap f) (HdAnomalyCoefficient (some val✝)) All goals completed! 🐙D.2. The anomaly coefficient of Hu
The pair of anomaly cancellation coefficients associated with the Hu particle.
def HuAnomalyCoefficient [CommRing 𝓩] (qHu : Option 𝓩) : 𝓩 × 𝓩 :=
match qHu with
| none => (0, 0)
| some qHu => (-qHu, -qHu ^ 2)@[simp]
lemma HuAnomalyCoefficient_map {𝓩 𝓩1 : Type} [CommRing 𝓩] [CommRing 𝓩1]
(f : 𝓩 →+* 𝓩1) (qHu : Option 𝓩) :
HuAnomalyCoefficient (qHu.map f) = (f.prodMap f) (HuAnomalyCoefficient qHu) := 𝓩:Type𝓩1:Typeinst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 →+* 𝓩1qHu:Option 𝓩⊢ HuAnomalyCoefficient (Option.map (⇑f) qHu) = (f.prodMap f) (HuAnomalyCoefficient qHu)
𝓩:Type𝓩1:Typeinst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 →+* 𝓩1⊢ HuAnomalyCoefficient (Option.map (⇑f) none) = (f.prodMap f) (HuAnomalyCoefficient none)𝓩:Type𝓩1:Typeinst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 →+* 𝓩1val✝:𝓩⊢ HuAnomalyCoefficient (Option.map (⇑f) (some val✝)) = (f.prodMap f) (HuAnomalyCoefficient (some val✝)) 𝓩:Type𝓩1:Typeinst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 →+* 𝓩1⊢ HuAnomalyCoefficient (Option.map (⇑f) none) = (f.prodMap f) (HuAnomalyCoefficient none)𝓩:Type𝓩1:Typeinst✝¹:CommRing 𝓩inst✝:CommRing 𝓩1f:𝓩 →+* 𝓩1val✝:𝓩⊢ HuAnomalyCoefficient (Option.map (⇑f) (some val✝)) = (f.prodMap f) (HuAnomalyCoefficient (some val✝)) All goals completed! 🐙D.3. The anomaly cancellation condition propositions
The linear anomaly cancellation condition, corresponding to
∑ᵢ qᵢ Nᵢ + ∑ₐ qₐ Nₐ = 0 where the first sum is over all 5-bar representations and the second
is over all 10d representations.
def LinearAnomalyCancellation [CommRing 𝓩] (Q : Quanta 𝓩) : Prop :=
(HdAnomalyCoefficient Q.qHd).1 + (HuAnomalyCoefficient Q.qHu).1 + Q.F.anomalyCoefficient.1 +
Q.T.anomalyCoefficient.1 = 0
The quartic anomaly cancellation condition, corresponding to
∑ᵢ qᵢ² Nᵢ + 3 * ∑ₐ qₐ² Nₐ = 0 where the first sum is over all 5-bar representations and the
second is over all 10d representations.
def QuarticAnomalyCancellation [CommRing 𝓩] (Q : Quanta 𝓩) :
Prop :=
(HdAnomalyCoefficient Q.qHd).2 + (HuAnomalyCoefficient Q.qHu).2 + Q.F.anomalyCoefficient.2 +
Q.T.anomalyCoefficient.2 = 0D.3.1. The propositions are decidable
instance [CommRing 𝓩] [DecidableEq 𝓩] (Q : Quanta 𝓩) : Decidable Q.LinearAnomalyCancellation :=
inferInstanceAs (Decidable ((HdAnomalyCoefficient Q.qHd).1 +
(HuAnomalyCoefficient Q.qHu).1 + Q.F.anomalyCoefficient.1 + Q.T.anomalyCoefficient.1 = 0))instance [CommRing 𝓩] [DecidableEq 𝓩] (Q : Quanta 𝓩) : Decidable Q.QuarticAnomalyCancellation :=
inferInstanceAs (Decidable ((HdAnomalyCoefficient Q.qHd).2 +
(HuAnomalyCoefficient Q.qHu).2 + Q.F.anomalyCoefficient.2 + Q.T.anomalyCoefficient.2 = 0))