Examples of matter content and show that they satisfy certain conditions

The examples in this module correspond to those in:

Krippendorf, Schafer-Nameki and Wong. Froggatt-Nielson meets Mordell-Weil: A Phenomenological Survey of Global F-theory GUTs with U(1)s https://arxiv.org/pdf/1507.05961.

We copy the notational convention used there. For example I14a corresponds to the first (a) example with 1 10d representation and 4 5-bar representations.

One 10d representation and four 5-bar representations

These examples come from Table 1 of arXiv:1507.05961

def FTheory.SU5U1.MatterContent.mkOneTenFourFiveBar (I : CodimensionOneConfig) (M : ChiralityFlux) (N : HyperChargeFlux) (q10 qHu qHd q5₁ q5₂ : ℤ) (hq10 : q10 ∈ I.allowedTenCharges := by decide) (hqHu : -qHu ∈ I.allowedBarFiveCharges := by decide) (hqHd : qHd ∈ I.allowedBarFiveCharges := by decide) (hq5₁ : q5₁ ∈ I.allowedBarFiveCharges := by decide) (hq5₂ : q5₂ ∈ I.allowedBarFiveCharges := by decide) (h5 : ∀ a ∈ {(0, -1, ⟨-qHu, hqHu⟩), (0, 1, ⟨qHd, hqHd⟩), (M, N, ⟨q5₁, hq5₁⟩), (3 - M, -N, ⟨q5₂, hq5₂⟩)}, a.M = 0 → a.N ≠ 0 := by decide) (h10 : ∀ a ∈ {(3, 0, ⟨q10, hq10⟩)}, a.M = 0 → a.N ≠ 0 := by decide) : MatterContent I

The construction of matter content given a CodimensionOneConfig from a value of M, N and the charges of the representations.

The charge of qHu is the charge of the 5 not the 5-bar representation.

This parameterizaton comes from Section 3.1.2 of arXiv:1507.05961.

Equations

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

def FTheory.SU5U1.MatterContent.exampleI14a : MatterContent CodimensionOneConfig.same

An example of matter content with one 10d representation and 4 5-bar representations. This corresponds to example I.1.4.a in table 1 of arXiv:1507.05961.

Equations

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

theorem FTheory.SU5U1.MatterContent.exampleI14a_anomalyFree : exampleI14a.AnomalyFree

theorem FTheory.SU5U1.MatterContent.exampleI14a_validMatterSpectrum : exampleI14a.ValidMatterSpectrum

def FTheory.SU5U1.MatterContent.exampleI14b : MatterContent CodimensionOneConfig.same

An example of matter content with one 10d representation and 4 5-bar representations. This corresponds to example I.1.4.b in table 1 of arXiv:1507.05961.

Equations

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

theorem FTheory.SU5U1.MatterContent.exampleI14b_anomalyFree : exampleI14b.AnomalyFree

theorem FTheory.SU5U1.MatterContent.exampleI14b_validMatterSpectrum : exampleI14b.ValidMatterSpectrum

def FTheory.SU5U1.MatterContent.exampleI14c : MatterContent CodimensionOneConfig.nearestNeighbor

An example of matter content with one 10d representation and 4 5-bar representations. This corresponds to one-version of example I.1.4.c in table 1 of arXiv:1507.05961.

Equations

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

theorem FTheory.SU5U1.MatterContent.exampleI14c_anomalyFree : exampleI14c.AnomalyFree

theorem FTheory.SU5U1.MatterContent.exampleI14c_validMatterSpectrum : exampleI14c.ValidMatterSpectrum

def FTheory.SU5U1.MatterContent.exampleI14c' : MatterContent CodimensionOneConfig.nearestNeighbor

An example of matter content with one 10d representation and 4 5-bar representations. This corresponds to one-version of example I.1.4.c in table 1 of arXiv:1507.05961.

Equations

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

theorem FTheory.SU5U1.MatterContent.exampleI14c'_anomalyFree : exampleI14c.AnomalyFree

theorem FTheory.SU5U1.MatterContent.exampleI14c'_validMatterSpectrum : exampleI14c.ValidMatterSpectrum

def FTheory.SU5U1.MatterContent.exampleI14d : MatterContent CodimensionOneConfig.same

An example of matter content with one 10d representation and 4 5-bar representations. This corresponds to example I.1.4.d in table 1 of arXiv:1507.05961.

Equations

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

theorem FTheory.SU5U1.MatterContent.exampleI14d_anomalyFree : exampleI14d.AnomalyFree

theorem FTheory.SU5U1.MatterContent.exampleI14d_validMatterSpectrum : exampleI14d.ValidMatterSpectrum

def FTheory.SU5U1.MatterContent.exampleI14e : MatterContent CodimensionOneConfig.nearestNeighbor

An example of matter content with one 10d representation and 4 5-bar representations. This corresponds to example I.1.4.e in table 1 of arXiv:1507.05961.

Equations

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

theorem FTheory.SU5U1.MatterContent.exampleI14e_anomalyFree : exampleI14e.AnomalyFree

theorem FTheory.SU5U1.MatterContent.exampleI14e_validMatterSpectrum : exampleI14e.ValidMatterSpectrum

def FTheory.SU5U1.MatterContent.exampleI14f : MatterContent CodimensionOneConfig.nextToNearestNeighbor

An example of matter content with one 10d representation and 4 5-bar representations. This corresponds to example I.1.4.f in table 1 of arXiv:1507.05961.

Equations

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

theorem FTheory.SU5U1.MatterContent.exampleI14f_anomalyFree : exampleI14f.AnomalyFree

theorem FTheory.SU5U1.MatterContent.exampleI14f_validMatterSpectrum : exampleI14f.ValidMatterSpectrum