Viable Quanta

We say a term of a type Quanta is viable for a given I : CodimensionOneConfig, if it satisfies the following properties:

• It has a Hd, Hu and at leat 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 satisfies anomaly cancellation.
• The charges are allowed by the I configuration.

This somes with one caveat, the IsViable constraint enforces the anomaly cancellation condition: ∑ᵢ qᵢ² Nᵢ + 3 * ∑ₐ qₐ² Nₐ = 0 to hold, which is not always necessary, see arXiv:1401.5084.

def FTheory.SU5U1.Quanta.IsViable (I : CodimensionOneConfig) (x : Quanta) : Prop

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

Equations

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

theorem FTheory.SU5U1.Quanta.isViable_iff_expand_ofFinset (I : CodimensionOneConfig) (x : Quanta) : IsViable I x ↔ x.toCharges.IsComplete ∧ ¬x.toCharges.IsPhenoConstrained ∧ x.toCharges.AllowsTerm SuperSymmetry.SU5.PotentialTerm.topYukawa ∧ x.2.2.1.toFluxesFive.NoExotics ∧ x.2.2.1.toFluxesFive.HasNoZero ∧ x.2.2.2.toFluxesTen.NoExotics ∧ x.2.2.2.toFluxesTen.HasNoZero ∧ AnomalyCancellation x.1 x.2.1 x.2.2.1 x.2.2.2 ∧ (x.1.toFinset ⊆ I.allowedBarFiveCharges ∧ x.2.1.toFinset ⊆ I.allowedBarFiveCharges ∧ x.toCharges.2.2.1 ⊆ I.allowedBarFiveCharges ∧ x.toCharges.2.2.2 ⊆ I.allowedTenCharges) ∧ x.2.2.1.toCharges.Nodup ∧ x.2.2.2.toCharges.Nodup

instance FTheory.SU5U1.Quanta.instDecidableIsViable (I : CodimensionOneConfig) (x : Quanta) : Decidable (IsViable I x)

Equations

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

theorem FTheory.SU5U1.Quanta.toCharges_five_nodup_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.2.2.1.toCharges.Nodup

theorem FTheory.SU5U1.Quanta.toCharges_ten_nodup_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.2.2.2.toCharges.Nodup

theorem FTheory.SU5U1.Quanta.toCharges_mem_ofFinset_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.toCharges ∈ Charges.ofFinset I.allowedBarFiveCharges I.allowedTenCharges

theorem FTheory.SU5U1.Quanta.toFluxesFive_noExotics_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.2.2.1.toFluxesFive.NoExotics

theorem FTheory.SU5U1.Quanta.toFluxesTen_noExotics_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.2.2.2.toFluxesTen.NoExotics

theorem FTheory.SU5U1.Quanta.toFluxesFive_hasNoZero_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.2.2.1.toFluxesFive.HasNoZero

theorem FTheory.SU5U1.Quanta.toFluxesTen_hasNoZero_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.2.2.2.toFluxesTen.HasNoZero

theorem FTheory.SU5U1.Quanta.Q10_charges_mem_allowedBarTenCharges_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) (s : ℤ) : s ∈ x.2.2.2.toCharges → s ∈ I.allowedTenCharges

theorem FTheory.SU5U1.Quanta.Q5_charges_mem_allowedBarFiveCharges_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) (s : ℤ) : s ∈ x.2.2.1.toCharges → s ∈ I.allowedBarFiveCharges

theorem FTheory.SU5U1.Quanta.fiveQuanta_mem_ofCharges_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.2.2.1 ∈ FiveQuanta.ofCharges I x.2.2.1.toCharges

theorem FTheory.SU5U1.Quanta.tenQuanta_mem_ofCharges_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.2.2.2 ∈ TenQuanta.ofCharges I x.2.2.2.toCharges

theorem FTheory.SU5U1.Quanta.topYukawa_allowsTerm_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.toCharges.AllowsTerm SuperSymmetry.SU5.PotentialTerm.topYukawa

theorem FTheory.SU5U1.Quanta.not_isPhenoConstrained_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : ¬x.toCharges.IsPhenoConstrained

theorem FTheory.SU5U1.Quanta.toCharges_isComplete_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.toCharges.IsComplete

theorem FTheory.SU5U1.Quanta.anomalyCancellation_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : AnomalyCancellation x.1 x.2.1 x.2.2.1 x.2.2.2

toCharges mem

theorem FTheory.SU5U1.Quanta.toCharges_mem_nonPhenoConstrainedCharges_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.toCharges ∈ Charges.nonPhenoConstrainedCharges I

theorem FTheory.SU5U1.Quanta.toCharges_mem_nonPhenoConstrainedCharges_filterAnomalyCancellation_of_isViable (I : CodimensionOneConfig) (x : Quanta) (h : IsViable I x) : x.toCharges ∈ Charges.Tree.filterAnomalyCancellation I (Charges.nonPhenoConstrainedCharges I)

theorem FTheory.SU5U1.Quanta.mem_ofCharges_self_of_isViable (I : CodimensionOneConfig) (𝓠 : Quanta) (h : IsViable I 𝓠) : 𝓠 ∈ ofCharges I 𝓠.toCharges