Viable Quanta with Yukawa

i. Overview

We say a term of a type Quanta is viable if it satisfies the following properties:

• It has a Hd, Hu and at least one matter particle in the 5 and 10 representation.
• It has no exotic chiral particles.
• It leads to a top Yukawa coupling.
• It does not lead to a pheno constraining terms.
• It does not lead to a dangerous Yukawa coupling at one insertion of the Yukawa singlets.
• It satisfies linear anomaly cancellation.
• The charges are allowed by an I configuration.

We also write down the explicit set of viable quanta, and prove that this set is complete.

One can view the dependencies of this module with:

lake exe graph --from
  PhysLean.StringTheory.FTheory.SU5.Fluxes.Basic,PhysLean.Particles.SuperSymmetry.SU5.FieldLabels
  my_graph.pdf

ii. Key results

• Quanta.IsViable : The proposition on a Quanta that it is viable.
• Quanta.viableElems : The multiset of viable quanta.
• Quanta.isViable_iff_mem_viableElems : A quanta is viable if and only if it is in the Quanta.viableElems.

iii. Table of contents

• A. The condition for a Quanta to be viable
  • A.1. Simplification of the prop to use the set of viable charges viableCharges I
  • A.2. Further simplification of the prop to use the set of viable charges Quanta.liftCharge
  • A.3. Further simplification of the prop to use the anomaly free set of viable charges
• B. The multiset of viable quanta
  • B.1. Every element of the multiset is viable
  • B.2. A quanta is viable if and only if it is in the multiset
  • B.3. Every element of the multiset regenerates Yukawa at two insertions of the Yukawa singlets
  • B.4. Those quanta which satisfy the quartic anomaly cancellation condition
  • B.5. Map down to Z2

iv. References

The key reference for the material in this module is: arXiv:1507.05961.

A. The condition for a Quanta to be viable

structure FTheory.SU5.Quanta.IsViable (x : Quanta) : Prop

For a given I : CodimensionOneConfig the condition on a Quanta for it to be phenomenologically viable.

• has_all_charges : x.toCharges.IsComplete

  There is a Hd, Hu, 5-bar matter and 10d matter.

• not_pheno_constrained : ¬x.toCharges.IsPhenoConstrained

  The charges do not lead to any phenomenologically constraining terms.

• not_regenerate_dangerous_couplings : ¬x.toCharges.YukawaGeneratesDangerousAtLevel 1

  The charges are such that dangerous couplings in the super potential are not regenerated with the Yukawa terms.

• charges_allowed_by_section_config : ∃ (I : CodimensionOneConfig), x.toCharges ∈ SuperSymmetry.SU5.ChargeSpectrum.ofFinset I.allowedBarFiveCharges I.allowedTenCharges

  The charges are such that they are allowed by a configuration of sections on the co-dimension 1 fiber.

• no_duplicate_five_bar_charges : (x.F ℤ).toCharges.Nodup

  Within the 5-bar matter, there is at most one entry for each charge.

• no_duplicate_ten_charges : (x.T ℤ).toCharges.Nodup

  Within the 10d matter, there is at most one entry for each charge.

• allows_top_yukawa : x.toCharges.AllowsTerm SuperSymmetry.SU5.PotentialTerm.topYukawa

  The charges permit at least one Top-Yukawa coupling.

• no_exotics_from_five_bar : (x.F ℤ).toFluxesFive.NoExotics

  The fluxes of the 5-bar matter fields do not lead to any exotic chiral particles.

• no_five_bar_zero_fluxes : (x.F ℤ).toFluxesFive.HasNoZero

  There are 5-bar matter fields where both fluxes are zero (these are not being counted here).

• no_exotics_from_ten : (x.T ℤ).toFluxesTen.NoExotics

  The fluxes of the 10d matter fields do not lead to any exotic chiral particles.

• no_ten_zero_fluxes : (x.T ℤ).toFluxesTen.HasNoZero

  There are 10d matter fields where both fluxes are zero (these are not being counted here).

• linear_anomalies : x.LinearAnomalyCancellation

  The quanta satisfy the linear anomaly cancellation conditions.

theorem FTheory.SU5.Quanta.isViable_iff_def (x : Quanta) : x.IsViable ↔ x.toCharges.IsComplete ∧ ¬x.toCharges.IsPhenoConstrained ∧ ¬x.toCharges.YukawaGeneratesDangerousAtLevel 1 ∧ (∃ (I : CodimensionOneConfig), x.toCharges ∈ SuperSymmetry.SU5.ChargeSpectrum.ofFinset I.allowedBarFiveCharges I.allowedTenCharges) ∧ (x.F ℤ).toCharges.Nodup ∧ (x.T ℤ).toCharges.Nodup ∧ x.toCharges.AllowsTerm SuperSymmetry.SU5.PotentialTerm.topYukawa ∧ (x.F ℤ).toFluxesFive.NoExotics ∧ (x.F ℤ).toFluxesFive.HasNoZero ∧ (x.T ℤ).toFluxesTen.NoExotics ∧ (x.T ℤ).toFluxesTen.HasNoZero ∧ x.LinearAnomalyCancellation

A.1. Simplification of the prop to use the set of viable charges viableCharges I

theorem FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges (x : Quanta) : x.IsViable ↔ (∃ (I : CodimensionOneConfig), x.toCharges ∈ ChargeSpectrum.viableCharges I) ∧ (x.F ℤ).toCharges.Nodup ∧ (x.T ℤ).toCharges.Nodup ∧ (x.F ℤ).toFluxesFive.NoExotics ∧ (x.F ℤ).toFluxesFive.HasNoZero ∧ (x.T ℤ).toFluxesTen.NoExotics ∧ (x.T ℤ).toFluxesTen.HasNoZero ∧ x.LinearAnomalyCancellation

A.2. Further simplification of the prop to use the set of viable charges Quanta.liftCharge

theorem FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges_mem_liftCharges (x : Quanta) : x.IsViable ↔ (∃ (I : CodimensionOneConfig), x.toCharges ∈ ChargeSpectrum.viableCharges I) ∧ x ∈ liftCharge x.toCharges ∧ x.LinearAnomalyCancellation

A.3. Further simplification of the prop to use the anomaly free set of viable charges

theorem FTheory.SU5.Quanta.isViable_iff_filter (x : Quanta) : x.IsViable ↔ (∃ (I : CodimensionOneConfig), x.toCharges ∈ Multiset.filter ChargeSpectrum.IsAnomalyFree (ChargeSpectrum.viableCharges I)) ∧ x ∈ liftCharge x.toCharges ∧ x.LinearAnomalyCancellation

B. The multiset of viable quanta

We find all the viable quanta. This can be evaluated with

  ((((viableCharges .same ∪ viableCharges .nearestNeighbor ∪
  viableCharges .nextToNearestNeighbor).filter IsAnomalyFree).bind
    Quanta.liftCharge).filter LinearAnomalyCancellation)

def FTheory.SU5.Quanta.viableElems : Multiset Quanta

Given a CodimensionOneConfig the Quanta which satisfy the condition IsViable.

Equations

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

B.1. Every element of the multiset is viable

theorem FTheory.SU5.Quanta.isViable_of_mem_viableElems (x : Quanta) (h : x ∈ viableElems) : x.IsViable

B.2. A quanta is viable if and only if it is in the multiset

theorem FTheory.SU5.Quanta.isViable_iff_mem_viableElems (x : Quanta) : x.IsViable ↔ x ∈ viableElems

B.3. Every element of the multiset regenerates Yukawa at two insertions of the Yukawa singlets

theorem FTheory.SU5.Quanta.yukawaSingletsRegenerateDangerousInsertion_two_of_isViable (x : Quanta) (h : x.IsViable) : x.toCharges.YukawaGeneratesDangerousAtLevel 2

Every viable Quanta regenerates a dangerous coupling at two insertions of the Yukawa singlets.

B.4. Those quanta which satisfy the quartic anomaly cancellation condition

theorem FTheory.SU5.Quanta.quarticAnomalyCancellation_iff_mem_of_isViable (x : Quanta) (h : x.IsViable) : x.QuarticAnomalyCancellation ↔ x ∈ {{ qHd := some 2, qHu := some (-2), F := {(-1, { M := 1, N := 2 }), (1, { M := 2, N := -2 })}, T := {(-1, { M := 3, N := 0 })} }, { qHd := some 2, qHu := some (-2), F := {(-1, { M := 0, N := 2 }), (1, { M := 3, N := -2 })}, T := {(-1, { M := 3, N := 0 })} }, { qHd := some (-2), qHu := some 2, F := {(-1, { M := 2, N := -2 }), (1, { M := 1, N := 2 })}, T := {(1, { M := 3, N := 0 })} }, { qHd := some (-2), qHu := some 2, F := {(-1, { M := 3, N := -2 }), (1, { M := 0, N := 2 })}, T := {(1, { M := 3, N := 0 })} }, { qHd := some 6, qHu := some (-14), F := {(-9, { M := 1, N := 2 }), (1, { M := 2, N := -2 })}, T := {(-7, { M := 3, N := 0 })} }, { qHd := some 6, qHu := some (-14), F := {(-9, { M := 0, N := 2 }), (1, { M := 3, N := -2 })}, T := {(-7, { M := 3, N := 0 })} }}

B.5. Map down to Z2

theorem FTheory.SU5.Quanta.map_to_Z2_of_isViable (x : Quanta) (h : x.IsViable) : SuperSymmetry.SU5.ChargeSpectrum.map (Int.castAddHom (ZMod 2)) x.toCharges ∈ {{ qHd := some 0, qHu := some 0, Q5 := {1}, Q10 := {1} }, { qHd := some 0, qHu := some 0, Q5 := {0, 1}, Q10 := {1} }, { qHd := some 0, qHu := some 0, Q5 := {0, 1}, Q10 := {0} }}