Completeness of viableElems

In this module we prove that the viableElems for a given I : CodimensionOneConfig is complete, in the sense that it contains all viable Quanta for that I. This main result is contained within the lemma isViable_iff_mem_viableElems.

Comment on proof

The proof of this result is done by first obtaining elemsAnomalyFree which contains the Charges which are not phenomenologically constrained and can be lifted to Quanta that is anomaly free. We then find all anomaly-free lifts of these charges to Quanta explicitly.

def FTheory.SU5U1.Charges.elemsAnomalyFree (I : CodimensionOneConfig) : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)

For a given I :CodimensionOneConfig the Charges which are not phenomenologically constrained and can be lifted to Quanta that is anomaly free.

The Trees here can be found using e.g. #eval FourTree.fromMultiset (filterAnomalyCancellation .same (nonPhenoConstrainedCharges .same)).toMultiset

Equations

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

theorem FTheory.SU5U1.Charges.filterAnomalyCancellation_nonPhenoConstrainedCharges_subset_elemsAnomalyFree_of_same : (Tree.filterAnomalyCancellation CodimensionOneConfig.same (nonPhenoConstrainedCharges CodimensionOneConfig.same)).toMultiset ⊆ (elemsAnomalyFree CodimensionOneConfig.same).toMultiset

theorem FTheory.SU5U1.Charges.filterAnomalyCancellation_nonPhenoConstrainedCharges_subset_elemsAnomalyFree_of_NN : (Tree.filterAnomalyCancellation CodimensionOneConfig.nearestNeighbor (nonPhenoConstrainedCharges CodimensionOneConfig.nearestNeighbor)).toMultiset ⊆ (elemsAnomalyFree CodimensionOneConfig.nearestNeighbor).toMultiset

theorem FTheory.SU5U1.Charges.filterAnomalyCancellation_nonPhenoConstrainedCharges_subset_elemsAnomalyFree_of_NTNN : (Tree.filterAnomalyCancellation CodimensionOneConfig.nextToNearestNeighbor (nonPhenoConstrainedCharges CodimensionOneConfig.nextToNearestNeighbor)).toMultiset ⊆ (elemsAnomalyFree CodimensionOneConfig.nextToNearestNeighbor).toMultiset

theorem FTheory.SU5U1.Charges.filterAnomalyCancellation_nonPhenoConstrainedCharges_subset_elemsAnomalyFree {I : CodimensionOneConfig} : (Tree.filterAnomalyCancellation I (nonPhenoConstrainedCharges I)).toMultiset ⊆ (elemsAnomalyFree I).toMultiset

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

Lifting to Quanta

theorem FTheory.SU5U1.Quanta.mem_viableElems_of_ofCharges_elemsAnomalyFree_of_same (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (Charges.elemsAnomalyFree CodimensionOneConfig.same).toMultiset → ∀ y ∈ ofCharges CodimensionOneConfig.same x, AnomalyCancellation y.1 y.2.1 y.2.2.1 y.2.2.2 → y ∈ viableElems CodimensionOneConfig.same

theorem FTheory.SU5U1.Quanta.mem_viableElems_of_ofCharges_elemsAnomalyFree_of_NN (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (Charges.elemsAnomalyFree CodimensionOneConfig.nearestNeighbor).toMultiset → ∀ y ∈ ofCharges CodimensionOneConfig.nearestNeighbor x, AnomalyCancellation y.1 y.2.1 y.2.2.1 y.2.2.2 → y ∈ viableElems CodimensionOneConfig.nearestNeighbor

theorem FTheory.SU5U1.Quanta.mem_viableElems_of_ofCharges_elemsAnomalyFree_of_NTNN (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (Charges.elemsAnomalyFree CodimensionOneConfig.nextToNearestNeighbor).toMultiset → ∀ y ∈ ofCharges CodimensionOneConfig.nextToNearestNeighbor x, AnomalyCancellation y.1 y.2.1 y.2.2.1 y.2.2.2 → y ∈ viableElems CodimensionOneConfig.nextToNearestNeighbor

theorem FTheory.SU5U1.Quanta.mem_viableElems_of_ofCharges (I : CodimensionOneConfig) (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (Charges.elemsAnomalyFree I).toMultiset → ∀ y ∈ ofCharges I x, AnomalyCancellation y.1 y.2.1 y.2.2.1 y.2.2.2 → y ∈ viableElems I

theorem FTheory.SU5U1.Quanta.mem_viableElems_of_isViable (I : CodimensionOneConfig) (𝓠 : Quanta) (h : IsViable I 𝓠) : 𝓠 ∈ viableElems I

theorem FTheory.SU5U1.Quanta.isViable_iff_mem_viableElems (I : CodimensionOneConfig) (𝓠 : Quanta) : IsViable I 𝓠 ↔ 𝓠 ∈ viableElems I