PhysLean Documentation

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

PhenoInsert of nonPhenoConstrainedCharges #

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

phenoInsertQ10 on nonPhenoConstrainedCharges is empty #

This result is used to help show completeness.

source
theorem FTheory.SU5U1.Charges.nonPhenoConstrainedCharges_phenoInsertQ10_card_zero_same (q10 : ℤ) :
q10 ∈ CodimensionOneConfig.same.allowedTenCharges → (Tree.phenoInsertQ10 (nonPhenoConstrainedCharges CodimensionOneConfig.same) q10).card = 0
source
theorem FTheory.SU5U1.Charges.nonPhenoConstrainedCharges_phenoInsertQ10_card_zero_nearestNeighbor (q10 : ℤ) :
q10 ∈ CodimensionOneConfig.nearestNeighbor.allowedTenCharges → (Tree.phenoInsertQ10 (nonPhenoConstrainedCharges CodimensionOneConfig.nearestNeighbor) q10).card = 0
source
theorem FTheory.SU5U1.Charges.nonPhenoConstrainedCharges_phenoInsertQ10_card_zero_nextToNearestNeighbor (q10 : ℤ) :
q10 ∈ CodimensionOneConfig.nextToNearestNeighbor.allowedTenCharges → (Tree.phenoInsertQ10 (nonPhenoConstrainedCharges CodimensionOneConfig.nextToNearestNeighbor) q10).card = 0
source
theorem FTheory.SU5U1.Charges.nonPhenoConstrainedCharges_phenoInsertQ10_card_zero (I : CodimensionOneConfig) (q10 : ℤ) :
q10 ∈ I.allowedTenCharges → (Tree.phenoInsertQ10 (nonPhenoConstrainedCharges I) q10).card = 0