therefore
Sign up
Open navigation

Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 3 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

3 results

Clear filters
Project-declaredLean 4.32.0

Complete Min Subset subset iff contains Pheno Completions Of Minimally Allows

SuperSymmetry.SU5.ChargeSpectrum.completeMinSubset_subset_iff_containsPhenoCompletionsOfMinimallyAllows

Project documentation

For a given S5 S10 : Finset 𝓩, the minimal multiset of charges which satisfies the condition ContainsPhenoCompletionsOfMinimallyAllows. That is to say, every multiset of charges which satisfies ContainsPhenoCompletionsOfMinimallyAllows has completeMinSubset as a subset. -/ def completeMinSubset (S5 S10 : Finset 𝓩) : Multiset (ChargeSpectrum 𝓩)...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Completeness of is Pheno Closed Q5 is Pheno Closed Q10

SuperSymmetry.SU5.ChargeSpectrum.completeness_of_isPhenoClosedQ5_isPhenoClosedQ10

Project documentation

For a given S5 S10 : Finset 𝓩, the minimal multiset of charges which satisfies the condition ContainsPhenoCompletionsOfMinimallyAllows. That is to say, every multiset of charges which satisfies ContainsPhenoCompletionsOfMinimallyAllows has completeMinSubset as a subset. -/ def completeMinSubset (S5 S10 : Finset 𝓩) : Multiset (ChargeSpectrum 𝓩)...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Contains Pheno Completions Of Minimally Allows iff completions Top Yukawa

SuperSymmetry.SU5.ChargeSpectrum.containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawa

Project documentation

The proposition that for multiset set of charges charges contains all viable completions of charges which allow the top Yukawa, given allowed values of 5d and 10d charges S5 and S10. -/ def ContainsPhenoCompletionsOfMinimallyAllows (S5 S10 : Finset 𝓩) (charges : Multiset (ChargeSpectrum 𝓩)) : Prop := βˆ€ x ∈ (minimallyAllowsTermsOfFinset S5 S10...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record