PhysLean Documentation

PhysLean.StringTheory.FTheory.SU5U1.Charges.PhenoConstrained.Elems.PhenoInsertQ5

PhenoInsert of nonPhenoConstrainedCharges #

We prove show that the phenoInsertQ5 of nonPhenoConstrainedCharges I is empty. This result is used in the completeness proof.

phenoInsertQ5 on nonPhenoConstrainedCharges is empty #

This result is used to help show completeness.

source
theorem FTheory.SU5U1.Charges.nonPhenoConstrainedCharges_phenoInsertQ5_card_zero_same_of_neg (q5 : ℤ) :
q5 ∈ CodimensionOneConfig.same.allowedBarFiveCharges → q5 < 0 → (Tree.phenoInsertQ5 (nonPhenoConstrainedCharges CodimensionOneConfig.same) q5).card = 0
source
theorem FTheory.SU5U1.Charges.nonPhenoConstrainedCharges_phenoInsertQ5_card_zero_same_of_pos (q5 : ℤ) :
q5 ∈ CodimensionOneConfig.same.allowedBarFiveCharges → 0 ≤ q5 → (Tree.phenoInsertQ5 (nonPhenoConstrainedCharges CodimensionOneConfig.same) q5).card = 0
source
theorem FTheory.SU5U1.Charges.nonPhenoConstrainedCharges_phenoInsertQ5_card_zero_same (q5 : ℤ) :
q5 ∈ CodimensionOneConfig.same.allowedBarFiveCharges → (Tree.phenoInsertQ5 (nonPhenoConstrainedCharges CodimensionOneConfig.same) q5).card = 0
source
theorem FTheory.SU5U1.Charges.nonPhenoConstrainedCharges_phenoInsertQ5_card_zero_nearestNeighbor (q5 : ℤ) :
q5 ∈ CodimensionOneConfig.nearestNeighbor.allowedBarFiveCharges → (Tree.phenoInsertQ5 (nonPhenoConstrainedCharges CodimensionOneConfig.nearestNeighbor) q5).card = 0
source
theorem FTheory.SU5U1.Charges.nonPhenoConstrainedCharges_phenoInsertQ5_card_zero_nextToNearestNeighbor (q5 : ℤ) :
q5 ∈ CodimensionOneConfig.nextToNearestNeighbor.allowedBarFiveCharges → (Tree.phenoInsertQ5 (nonPhenoConstrainedCharges CodimensionOneConfig.nextToNearestNeighbor) q5).card = 0
source
theorem FTheory.SU5U1.Charges.nonPhenoConstrainedCharges_phenoInsertQ5_card_zero (I : CodimensionOneConfig) (q5 : ℤ) :
q5 ∈ I.allowedBarFiveCharges → (Tree.phenoInsertQ5 (nonPhenoConstrainedCharges I) q5).card = 0