Documentation Verification Report

PhenoClosed

📁 Source: PhysLean/Particles/SuperSymmetry/SU5/ChargeSpectrum/PhenoClosed.lean

Statistics

Metric	Count
Definitions `ContainsPhenoCompletionsOfMinimallyAllows`, `IsPhenoClosedQ10`, `IsPhenoClosedQ5`, `completeMinSubset`, `instDecidableContainsPhenoCompletionsOfMinimallyAllows`, `viableChargesMultiset`, `aux`	7
Theorems `completeMinSubset_containsPhenoCompletionsOfMinimallyAllows`, `completeMinSubset_nodup`, `completeMinSubset_subset_iff_containsPhenoCompletionsOfMinimallyAllows`, `completeness_of_isPhenoClosedQ5_isPhenoClosedQ10`, `containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawa`, `containsPhenoCompletionsOfMinimallyAllows_of_subset`, `isPhenClosedQ10_of_isPhenoConstrainedQ10`, `isPhenClosedQ5_of_isPhenoConstrainedQ5`	8
Total	15

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`ContainsPhenoCompletionsOfMinimallyAllows` 📖	MathDef	4 math math: `completeMinSubset_subset_iff_containsPhenoCompletionsOfMinimallyAllows`, `completeMinSubset_containsPhenoCompletionsOfMinimallyAllows`, `FTheory.SU5.ChargeSpectrum.containsPhenoCompletionsOfMinimallyAllows_viableCompletions`, `containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawa`
`IsPhenoClosedQ10` 📖	MathDef	2 math math: `FTheory.SU5.ChargeSpectrum.isPhenoClosedQ10_viableCharges`, `isPhenClosedQ10_of_isPhenoConstrainedQ10`
`IsPhenoClosedQ5` 📖	MathDef	2 math math: `isPhenClosedQ5_of_isPhenoConstrainedQ5`, `FTheory.SU5.ChargeSpectrum.isPhenoClosedQ5_viableCharges`
`completeMinSubset` 📖	CompOp	3 math math: `completeMinSubset_subset_iff_containsPhenoCompletionsOfMinimallyAllows`, `completeMinSubset_nodup`, `completeMinSubset_containsPhenoCompletionsOfMinimallyAllows`
`instDecidableContainsPhenoCompletionsOfMinimallyAllows` 📖	CompOp	—
`viableChargesMultiset` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeMinSubset_containsPhenoCompletionsOfMinimallyAllows` 📖	mathematical	—	`ContainsPhenoCompletionsOfMinimallyAllows` `completeMinSubset`	—	`completeMinSubset_subset_iff_containsPhenoCompletionsOfMinimallyAllows`
`completeMinSubset_nodup` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `completeMinSubset`	—	—
`completeMinSubset_subset_iff_containsPhenoCompletionsOfMinimallyAllows` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `completeMinSubset` `ContainsPhenoCompletionsOfMinimallyAllows`	—	`containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawa`
`completeness_of_isPhenoClosedQ5_isPhenoClosedQ10` 📖	—	`AllowsTerm` `SuperSymmetry.SU5.PotentialTerm.topYukawa` `IsPhenoConstrained` `YukawaGeneratesDangerousAtLevel` `IsComplete` `IsPhenoClosedQ5` `IsPhenoClosedQ10` `ContainsPhenoCompletionsOfMinimallyAllows` `SuperSymmetry.SU5.ChargeSpectrum` `ofFinset`	—	—	`allowsTerm_iff_subset_minimallyAllowsTerm` `minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinset` `mem_ofFinset_antitone` `exist_completions_subset_of_complete` `isPhenoConstrained_mono` `yukawaGeneratesDangerousAtLevel_of_subset` `subset_insert_filter_card_zero`
`containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawa` 📖	mathematical	—	`ContainsPhenoCompletionsOfMinimallyAllows` `SuperSymmetry.SU5.ChargeSpectrum`	—	`ContainsPhenoCompletionsOfMinimallyAllows.eq_1` `not_isPhenoConstrained_of_minimallyAllowsTermsOfFinset_topYukawa` `completions_eq_completionsTopYukawa_of_mem_minimallyAllowsTermsOfFinset`
`containsPhenoCompletionsOfMinimallyAllows_of_subset` 📖	—	`ContainsPhenoCompletionsOfMinimallyAllows` `SuperSymmetry.SU5.ChargeSpectrum`	—	—	—
`isPhenClosedQ10_of_isPhenoConstrainedQ10` 📖	mathematical	`IsPhenoConstrainedQ10` `SuperSymmetry.SU5.ChargeSpectrum` `qHd` `qHu` `Q5` `Q10` `YukawaGeneratesDangerousAtLevel`	`IsPhenoClosedQ10`	—	`isPhenoConstrained_insertQ10_iff_isPhenoConstrainedQ10`
`isPhenClosedQ5_of_isPhenoConstrainedQ5` 📖	mathematical	`IsPhenoConstrainedQ5` `SuperSymmetry.SU5.ChargeSpectrum` `qHd` `qHu` `Q5` `Q10` `YukawaGeneratesDangerousAtLevel`	`IsPhenoClosedQ5`	—	`isPhenoConstrained_insertQ5_iff_isPhenoConstrainedQ5`

SuperSymmetry.SU5.ChargeSpectrum.viableChargesMultiset

Definitions

Name	Category	Theorems
`aux` 📖	CompOp	—

---

← Back to Index