Complete of nonPhenoConstrainedCharges I

We show that the nonPhenoConstrainedCharges I is complete, that is, it contains every charge in ofFinset I.allowedBarFiveCharges I.allowedTenCharges which is not pheno-constrained, permits a top yukawa and is complete.

Method

The method of our proof is the following.

1. We define completionTopYukawa which contains all completions of elements which minimally allow the top Yukawa, which are not pheno-constrained. We show that every charge in ofFinset I.allowedBarFiveCharges I.allowedTenCharges which is not pheno-constrained and complete must contain an element of completionTopYukawaSame as a subset.
2. We show that completionTopYukawa I is a subset of nonPhenoConstrainedCharges I.
3. We then use the fact that one can not add to any charge in nonPhenoConstrainedCharges another Q5 or Q10 without remaining in nonPhenoConstrainedCharges or allowing a pheno-constraining term to be present.

This proof of completeness is more like a certification of completeness, rather than a constructive proof.

Key results

• not_isPhenoConstrained_iff_mem_nonPhenoConstrainedCharge which specifies the completeness of the tree of charges nonPhenoConstrainedCharges I.

theorem FTheory.SU5U1.Charges.nonPhenoConstrainedCharges_insertQ10_filter (I : CodimensionOneConfig) (q10 : { x : ℤ // x ∈ I.allowedTenCharges }) : Multiset.filter (fun (x : Charges) => ¬x.IsPhenoConstrained) (PhysLean.FourTree.uniqueMap4 (insert ↑q10) (nonPhenoConstrainedCharges I)).toMultiset = ∅

theorem FTheory.SU5U1.Charges.nonPhenoConstrainedCharges_insertQ5_filter (I : CodimensionOneConfig) (q5 : { x : ℤ // x ∈ I.allowedBarFiveCharges }) : Multiset.filter (fun (x : Charges) => ¬x.IsPhenoConstrained) (PhysLean.FourTree.uniqueMap3 (insert ↑q5) (nonPhenoConstrainedCharges I)).toMultiset = ∅

theorem FTheory.SU5U1.Charges.completionTopYukawa_complete_of_same (x : Charges) : x ∈ minimallyAllowsTermsOfFinset CodimensionOneConfig.same.allowedBarFiveCharges CodimensionOneConfig.same.allowedTenCharges SuperSymmetry.SU5.PotentialTerm.topYukawa → ¬x.IsPhenoConstrained → ∀ y ∈ completions CodimensionOneConfig.same.allowedBarFiveCharges CodimensionOneConfig.same.allowedTenCharges x, ¬y.IsPhenoConstrained → y ∈ FTheory.SU5U1.Charges.completionTopYukawa✝ CodimensionOneConfig.same

theorem FTheory.SU5U1.Charges.completionTopYukawa_complete_of_nearestNeighbor (x : Charges) : x ∈ minimallyAllowsTermsOfFinset CodimensionOneConfig.nearestNeighbor.allowedBarFiveCharges CodimensionOneConfig.nearestNeighbor.allowedTenCharges SuperSymmetry.SU5.PotentialTerm.topYukawa → ¬x.IsPhenoConstrained → ∀ y ∈ completions CodimensionOneConfig.nearestNeighbor.allowedBarFiveCharges CodimensionOneConfig.nearestNeighbor.allowedTenCharges x, ¬y.IsPhenoConstrained → y ∈ FTheory.SU5U1.Charges.completionTopYukawa✝ CodimensionOneConfig.nearestNeighbor

theorem FTheory.SU5U1.Charges.completionTopYukawa_complete_of_nextToNearestNeighbor (x : Charges) : x ∈ minimallyAllowsTermsOfFinset CodimensionOneConfig.nextToNearestNeighbor.allowedBarFiveCharges CodimensionOneConfig.nextToNearestNeighbor.allowedTenCharges SuperSymmetry.SU5.PotentialTerm.topYukawa → ¬x.IsPhenoConstrained → ∀ y ∈ completions CodimensionOneConfig.nextToNearestNeighbor.allowedBarFiveCharges CodimensionOneConfig.nextToNearestNeighbor.allowedTenCharges x, ¬y.IsPhenoConstrained → y ∈ FTheory.SU5U1.Charges.completionTopYukawa✝ CodimensionOneConfig.nextToNearestNeighbor

theorem FTheory.SU5U1.Charges.completionTopYukawa_complete {I : CodimensionOneConfig} (x : Charges) (hx : x ∈ minimallyAllowsTermsOfFinset I.allowedBarFiveCharges I.allowedTenCharges SuperSymmetry.SU5.PotentialTerm.topYukawa) (hPheno : ¬x.IsPhenoConstrained) (y : Charges) : y ∈ completions I.allowedBarFiveCharges I.allowedTenCharges x → ¬y.IsPhenoConstrained → y ∈ FTheory.SU5U1.Charges.completionTopYukawa✝ I

theorem FTheory.SU5U1.Charges.exists_subset_completionTopYukawa_of_not_isPhenoConstrained {I : CodimensionOneConfig} {x : Charges} (hx : ¬x.IsPhenoConstrained) (htopYukawa : x.AllowsTerm SuperSymmetry.SU5.PotentialTerm.topYukawa) (hsub : x ∈ ofFinset I.allowedBarFiveCharges I.allowedTenCharges) (hcomplete : x.IsComplete) : ∃ y ∈ FTheory.SU5U1.Charges.completionTopYukawa✝ I, y ⊆ x

theorem FTheory.SU5U1.Charges.completionTopYukawa_subset_nonPhenoConstrainedCharges {I : CodimensionOneConfig} (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (FTheory.SU5U1.Charges.completionTopYukawa✝ I).toMultiset → x ∈ nonPhenoConstrainedCharges I

theorem FTheory.SU5U1.Charges.not_isPhenoConstrained_mem_nonPhenoConstrainedCharges {I : CodimensionOneConfig} {x : Charges} (hx : ¬x.IsPhenoConstrained) (hsub : x ∈ ofFinset I.allowedBarFiveCharges I.allowedTenCharges) (hcomplete : x.IsComplete) : x ∉ nonPhenoConstrainedCharges I → ¬(¬x.IsPhenoConstrained ∧ x.AllowsTerm SuperSymmetry.SU5.PotentialTerm.topYukawa)

theorem FTheory.SU5U1.Charges.not_isPhenoConstrained_iff_mem_nonPhenoConstrainedCharge {I : CodimensionOneConfig} {x : Charges} (hsub : x ∈ ofFinset I.allowedBarFiveCharges I.allowedTenCharges) : x.AllowsTerm SuperSymmetry.SU5.PotentialTerm.topYukawa ∧ ¬x.IsPhenoConstrained ∧ x.IsComplete ↔ x ∈ nonPhenoConstrainedCharges I