Pheno constraints of nonPhenoConstrainedCharges

We prove that each charge in the trees nonPhenoConstrainedCharges I, is not pheno-constrained and permits a top Yukawa.

Each change is not pheno-constrained

theorem FTheory.SU5U1.Charges.not_isPhenoConstrained_of_mem_nonPhenoConstrainedCharges_same (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.same).toMultiset → ¬IsPhenoConstrained x

theorem FTheory.SU5U1.Charges.not_isPhenoConstrained_of_mem_nonPhenoConstrainedCharges_nearestNeighbor (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.nearestNeighbor).toMultiset → ¬IsPhenoConstrained x

theorem FTheory.SU5U1.Charges.not_isPhenoConstrained_of_mem_nonPhenoConstrainedCharges_nextToNearestNeighbor (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.nextToNearestNeighbor).toMultiset → ¬IsPhenoConstrained x

theorem FTheory.SU5U1.Charges.not_isPhenoConstrained_of_mem_nonPhenoConstrainedCharges (I : CodimensionOneConfig) (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges I).toMultiset → ¬IsPhenoConstrained x

Each change has a top Yukawa coupling

theorem FTheory.SU5U1.Charges.allowsTerm_topYukawa_of_mem_nonPhenoConstrainedCharges_same (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.same).toMultiset → AllowsTerm x SuperSymmetry.SU5.PotentialTerm.topYukawa

theorem FTheory.SU5U1.Charges.allowsTerm_topYukawa_of_mem_nonPhenoConstrainedCharges_nearestNeighbor (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.nearestNeighbor).toMultiset → AllowsTerm x SuperSymmetry.SU5.PotentialTerm.topYukawa

theorem FTheory.SU5U1.Charges.allowsTerm_topYukawa_of_mem_nonPhenoConstrainedCharges_nextToNearestNeighbor (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.nextToNearestNeighbor).toMultiset → AllowsTerm x SuperSymmetry.SU5.PotentialTerm.topYukawa

theorem FTheory.SU5U1.Charges.allowsTerm_topYukawa_of_mem_nonPhenoConstrainedCharges (I : CodimensionOneConfig) (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges I).toMultiset → AllowsTerm x SuperSymmetry.SU5.PotentialTerm.topYukawa