Generation of Yukawa couplings

In this file we consider the singlets needed to regenerate the Yukawa couplings.

We ask whether these singlets regenerate a dangerous coupling in the super potential at one or two insertions of the Yukawa singlets.

We find that there are no viable Quanta which do not regenerate a dangerous coupling with at most two insertions of the Yukawa singlets.

We do not consider the Kahler potential in this file.

def FTheory.SU5U1.Quanta.yukawaSingletCharges (x : Quanta) : Multiset ℤ

The set of charges of singlets needed to regenerate all the Yukawa terms in the potential.

Equations

• x.yukawaSingletCharges = x.toCharges.ofPotentialTerm SuperSymmetry.SU5.PotentialTerm.topYukawa + x.toCharges.ofPotentialTerm SuperSymmetry.SU5.PotentialTerm.bottomYukawa

def FTheory.SU5U1.Quanta.yukawaSingletChargesInsertions (x : Quanta) : ℕ → Multiset ℤ

The set of charges of n choices of singlets which regenerate the Yukawa terms.

Equations

• x.yukawaSingletChargesInsertions 0 = {0}
• x.yukawaSingletChargesInsertions n.succ = (x.yukawaSingletChargesInsertions n).bind fun (sSum : ℤ) => Multiset.map (fun (s : ℤ) => sSum + s) x.yukawaSingletCharges

def FTheory.SU5U1.Quanta.YukawaSingletsRegenerateDangerousInsertion (x : Quanta) (n : ℕ) : Prop

The proposition which states that the singlets needed to regenerate the Yukawa couplings regenerate a dangerous coupling at n-insertions of the singlets.

Equations

• x.YukawaSingletsRegenerateDangerousInsertion n = ((x.yukawaSingletChargesInsertions n).toFinset ∩ x.toCharges.phenoConstrainingChargesSP.toFinset ≠ ∅)

instance FTheory.SU5U1.Quanta.instDecidableYukawaSingletsRegenerateDangerousInsertion {x : Quanta} {n : ℕ} : Decidable (x.YukawaSingletsRegenerateDangerousInsertion n)

Equations

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

One insertion

The viable Quanta which do not regenerate a dangerous coupling at one insertion of the Yukawa singlets.

theorem FTheory.SU5U1.Quanta.viableElems_filter_yukawaSingletsRegenerateDangerousInsertion_one_eq_of_same : Multiset.filter (fun (x : Quanta) => ¬x.YukawaSingletsRegenerateDangerousInsertion 1) (viableElems CodimensionOneConfig.same).toMultiset = {(some 2, some (-2), {(-1, 1, 2), (1, 2, -2)}, {(-1, 3, 0)}), (some 2, some (-2), {(-1, 0, 2), (1, 3, -2)}, {(-1, 3, 0)}), (some (-2), some 2, {(-1, 2, -2), (1, 1, 2)}, {(1, 3, 0)}), (some (-2), some 2, {(-1, 3, -2), (1, 0, 2)}, {(1, 3, 0)})}

theorem FTheory.SU5U1.Quanta.viableElems_filter_yukawaSingletsRegenerateDangerousInsertion_one_eq_of_NN : Multiset.filter (fun (x : Quanta) => ¬x.YukawaSingletsRegenerateDangerousInsertion 1) (viableElems CodimensionOneConfig.nearestNeighbor).toMultiset = {(some 6, some (-14), {(-9, 1, 2), (1, 2, -2)}, {(-7, 3, 0)}), (some 6, some (-14), {(-9, 0, 2), (1, 3, -2)}, {(-7, 3, 0)})}

theorem FTheory.SU5U1.Quanta.viableElems_filter_yukawaSingletsRegenerateDangerousInsertion_one_eq_of_NtoNN : Multiset.filter (fun (x : Quanta) => ¬x.YukawaSingletsRegenerateDangerousInsertion 1) (viableElems CodimensionOneConfig.nextToNearestNeighbor).toMultiset = ∅

One or two insertions

The viable Quanta which do not regenerate a dangerous coupling with one or two insertions of the Yukawa singlets.

theorem FTheory.SU5U1.Quanta.viableElems_filter_yukawaSingletsRegenerateDangerousInsertion_two_eq_of_same : Multiset.filter (fun (x : Quanta) => ¬x.YukawaSingletsRegenerateDangerousInsertion 1 ∧ ¬x.YukawaSingletsRegenerateDangerousInsertion 2) (viableElems CodimensionOneConfig.same).toMultiset = ∅

theorem FTheory.SU5U1.Quanta.viableElems_filter_yukawaSingletsRegenerateDangerousInsertion_two_eq_of_NN : Multiset.filter (fun (x : Quanta) => ¬x.YukawaSingletsRegenerateDangerousInsertion 1 ∧ ¬x.YukawaSingletsRegenerateDangerousInsertion 2) (viableElems CodimensionOneConfig.nearestNeighbor).toMultiset = ∅

theorem FTheory.SU5U1.Quanta.viableElems_filter_yukawaSingletsRegenerateDangerousInsertion_two_eq_of_NtoNN : Multiset.filter (fun (x : Quanta) => ¬x.YukawaSingletsRegenerateDangerousInsertion 1 ∧ ¬x.YukawaSingletsRegenerateDangerousInsertion 2) (viableElems CodimensionOneConfig.nextToNearestNeighbor).toMultiset = ∅