Documentation Verification Report

Completions

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

Statistics

Metric	Count
Definitions `IsComplete`, `completions`, `completionsTopYukawa`, `instDecidableIsCompleteOfDecidableEq`	4
Theorems `completionsTopYukawa_nodup`, `completions_eq_completionsTopYukawa_of_mem_minimallyAllowsTermsOfFinset`, `completions_eq_singleton_of_complete`, `completions_nodup`, `exist_completions_subset_of_complete`, `isComplete_mono`, `mem_completions_iff`, `mem_completions_isComplete`, `not_isComplete_empty`, `self_mem_completions_iff_isComplete`, `self_subset_mem_completions`	11
Total	15

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`IsComplete` 📖	MathDef	9 math math: `self_mem_completions_iff_isComplete`, `not_isComplete_empty`, `map_isComplete_iff`, `FTheory.SU5.ChargeSpectrum.isComplete_of_mem_viableCharges`, `mem_completions_isComplete`, `FTheory.SU5.Quanta.isViable_iff_def`, `FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff'`, `FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff`, `FTheory.SU5.Quanta.IsViable.has_all_charges`
`completions` 📖	CompOp	6 math math: `completions_eq_completionsTopYukawa_of_mem_minimallyAllowsTermsOfFinset`, `self_mem_completions_iff_isComplete`, `exist_completions_subset_of_complete`, `mem_completions_iff`, `completions_eq_singleton_of_complete`, `completions_nodup`
`completionsTopYukawa` 📖	CompOp	2 math math: `completions_eq_completionsTopYukawa_of_mem_minimallyAllowsTermsOfFinset`, `completionsTopYukawa_nodup`
`instDecidableIsCompleteOfDecidableEq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completionsTopYukawa_nodup` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `completionsTopYukawa`	—	—
`completions_eq_completionsTopYukawa_of_mem_minimallyAllowsTermsOfFinset` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `minimallyAllowsTermsOfFinset` `SuperSymmetry.SU5.PotentialTerm.topYukawa`	`completions` `completionsTopYukawa`	—	`completions_nodup` `completionsTopYukawa_nodup`
`completions_eq_singleton_of_complete` 📖	mathematical	`IsComplete`	`completions` `SuperSymmetry.SU5.ChargeSpectrum`	—	—
`completions_nodup` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `completions`	—	—
`exist_completions_subset_of_complete` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `ofFinset` `IsComplete`	`completions`	—	`HasSubset.Subset.eq_1`
`isComplete_mono` 📖	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `IsComplete`	—	—	`subset_def`
`mem_completions_iff` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `completions` `qHd` `qHu` `Q5` `Q10`	—	`completions.eq_1`
`mem_completions_isComplete` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `completions`	`IsComplete`	—	`IsComplete.eq_1`
`not_isComplete_empty` 📖	mathematical	—	`IsComplete` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	`empty_qHd` `empty_qHu` `empty_Q5` `empty_Q10`
`self_mem_completions_iff_isComplete` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `completions` `IsComplete`	—	—
`self_subset_mem_completions` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `completions`	`hasSubset`	—	`HasSubset.Subset.eq_1`

---

← Back to Index