Anomaly cancellation

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 represenations and the second is over all 10d representations.
• ∑ᵢ qᵢ² Nᵢ + 3 * ∑ₐ qₐ² Nₐ = 0 where the first sum is over all 5-bar represenations and the second is over all 10d representations.

According to arXiv:1401.5084 it is unclear whether this second condition should necessarily be imposed.

def FTheory.SU5U1.FiveQuanta.anomalyCoefficent (F : FiveQuanta) : ℤ × ℤ

The anomaly coefficent of a FiveQuanta is given by the pair of integers: (∑ᵢ qᵢ Nᵢ, ∑ᵢ 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.

Equations

• F.anomalyCoefficent = ((Multiset.map (fun (x : ℤ × ℤ × ℤ) => x.1 * x.2.2) F).sum, (Multiset.map (fun (x : ℤ × ℤ × ℤ) => x.1 * x.1 * x.2.2) F).sum)

def FTheory.SU5U1.TenQuanta.anomalyCoefficent (F : TenQuanta) : ℤ × ℤ

The anomaly coefficent 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.

Equations

• F.anomalyCoefficent = ((Multiset.map (fun (x : ℤ × ℤ × ℤ) => x.1 * x.2.2) F).sum, 3 * (Multiset.map (fun (x : ℤ × ℤ × ℤ) => x.1 * x.1 * x.2.2) F).sum)

Anomaly cancellation conditions

def FTheory.SU5U1.HdAnomalyCoefficent (qHd : Option ℤ) : ℤ × ℤ

The pair of anomaly cancellation coefficents associated with the Hd particle.

Equations

• FTheory.SU5U1.HdAnomalyCoefficent none = (0, 0)
• FTheory.SU5U1.HdAnomalyCoefficent (some qHd_2) = (qHd_2, qHd_2 ^ 2)

def FTheory.SU5U1.HuAnomalyCoefficent (qHu : Option ℤ) : ℤ × ℤ

The pair of anomaly cancellation coefficents associated with the Hu particle.

Equations

• FTheory.SU5U1.HuAnomalyCoefficent none = (0, 0)
• FTheory.SU5U1.HuAnomalyCoefficent (some qHd_1) = (-qHd_1, -qHd_1 ^ 2)

def FTheory.SU5U1.AnomalyCancellation (qHd qHu : Option ℤ) (F : FiveQuanta) (T : TenQuanta) : Prop

The anomaly cancellation conditions on quanta making up the fields present in the theory. This corresponds to the conditions that:

• ∑ᵢ qᵢ Nᵢ + ∑ₐ qₐ Nₐ = 0 where the first sum is over all 5-bar represenations and the second is over all 10d representations.
• ∑ᵢ qᵢ² Nᵢ + 3 * ∑ₐ qₐ² Nₐ = 0 where the first sum is over all 5-bar represenations and the second is over all 10d representations.

Equations

• FTheory.SU5U1.AnomalyCancellation qHd qHu F T = (FTheory.SU5U1.HdAnomalyCoefficent qHd + FTheory.SU5U1.HuAnomalyCoefficent qHu + F.anomalyCoefficent + T.anomalyCoefficent = (0, 0))

instance FTheory.SU5U1.instDecidableAnomalyCancellation {qHd qHu : Option ℤ} {F : FiveQuanta} {T : TenQuanta} : Decidable (AnomalyCancellation qHd qHu F T)

Equations

• One or more equations did not get rendered due to their size.

theorem FTheory.SU5U1.anomalyCoefficent_snd_eq_zero_of_anomalyCancellation {qHd qHu : Option ℤ} {F : FiveQuanta} {T : TenQuanta} (h : AnomalyCancellation qHd qHu F T) : (HdAnomalyCoefficent qHd).2 + (HuAnomalyCoefficent qHu).2 + F.anomalyCoefficent.2 + T.anomalyCoefficent.2 = 0

theorem FTheory.SU5U1.five_anomalyCoefficent_mod_three_zero_of_anomalyCancellation {qHd qHu : Option ℤ} {F : FiveQuanta} {T : TenQuanta} (h : AnomalyCancellation qHd qHu F T) : ((HdAnomalyCoefficent qHd).2 + (HuAnomalyCoefficent qHu).2 + F.anomalyCoefficent.2) % 3 = 0

Anomaly cancellation on charges tree

def FTheory.SU5U1.Charges.Tree.Twig.filterAnomalyCancellation (I : CodimensionOneConfig) (qHd qHu : Option ℤ) : PhysLean.FourTree.Twig (Finset ℤ) (Finset ℤ) → PhysLean.FourTree.Twig (Finset ℤ) (Finset ℤ)

Given charges qHd and qHu filters a twig of Q5 and Q10 charges by the anomaly cancellation condition.

Equations

• One or more equations did not get rendered due to their size.

def FTheory.SU5U1.Charges.Tree.Branch.filterAnomalyCancellation (I : CodimensionOneConfig) (qHd : Option ℤ) : PhysLean.FourTree.Branch (Option ℤ) (Finset ℤ) (Finset ℤ) → PhysLean.FourTree.Branch (Option ℤ) (Finset ℤ) (Finset ℤ)

Given charges qHd filters a branch of qHu, Q5 and Q10 charges by the anomaly cancellation condition.

Equations

• One or more equations did not get rendered due to their size.

def FTheory.SU5U1.Charges.Tree.Trunk.filterAnomalyCancellation (I : CodimensionOneConfig) : PhysLean.FourTree.Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ) → PhysLean.FourTree.Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)

Filters a trunk of qHd, qHu, Q5 and Q10 charges by the anomaly cancellation condition.

Equations

• One or more equations did not get rendered due to their size.

def FTheory.SU5U1.Charges.Tree.filterAnomalyCancellation (I : CodimensionOneConfig) : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ) → PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)

Filters a tree of qHd, qHu, Q5 and Q10 charges by the anomaly cancellation condition.

Equations

• One or more equations did not get rendered due to their size.

theorem FTheory.SU5U1.Charges.Tree.mem_filterAnomalyCancellation_iff {I : CodimensionOneConfig} {T : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)} {x : Charges} : x ∈ filterAnomalyCancellation I T ↔ x ∈ T ∧ ∃ (F : FiveQuanta) (T : TenQuanta), F ∈ FiveQuanta.ofCharges I x.2.2.1.val ∧ T ∈ TenQuanta.ofCharges I x.2.2.2.val ∧ AnomalyCancellation x.1 x.2.1 F T