Documentation Verification Report

AllowsTerm

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

Statistics

Metric	Count
Definitions `AllowsTerm`, `AllowsTermQ10`, `AllowsTermQ5`, `allowsTermForm`, `instDecidableAllowsTermOfDecidableEq`, `instDecidableAllowsTermQ10`, `instDecidableAllowsTermQ5`	7
Theorems `allowsTermForm_allowsTerm`, `allowsTermForm_card_le_degree`, `allowsTermForm_eq_of_subset`, `allowsTermForm_subset_allowsTerm_of_allowsTerm`, `allowsTermQ10_or_allowsTerm_of_allowsTerm_insertQ10`, `allowsTermQ5_or_allowsTerm_of_allowsTerm_insertQ5`, `allowsTerm_iff_subset_allowsTermForm`, `allowsTerm_iff_zero_mem_ofPotentialTerm'`, `allowsTerm_insertQ10_iff_allowsTermQ10`, `allowsTerm_insertQ10_of_allowsTermQ10`, `allowsTerm_insertQ5_iff_allowsTermQ5`, `allowsTerm_insertQ5_of_allowsTermQ5`, `allowsTerm_mono`, `allowsTerm_of_eq_allowsTermForm`, `subset_card_le_degree_allowsTerm_of_allowsTerm`	15
Total	22

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`AllowsTerm` 📖	MathDef	22 math math: `allowsTerm_iff_subset_allowsTermForm`, `minimallyAllowsTerm_iff_powerset_filter_eq`, `FTheory.SU5.ChargeSpectrum.allowsTerm_topYukawa_of_mem_viableCharges`, `allowsTermForm_allowsTerm`, `allowsTerm_of_minimallyAllowsFinsetTerms`, `allowsTerm_of_minimallyAllowsTerm`, `allowsTerm_insertQ5_of_allowsTermQ5`, `allowsTerm_topYukawa_of_mem_minTopBottom`, `allowsTerm_of_has_minimallyAllowsTerm_subset`, `allowsTerm_bottomYukawa_of_mem_minTopBottom`, `allowsTerm_iff_zero_mem_ofPotentialTerm'`, `allowsTerm_of_mem_minimallyAllowsTermOfFinset`, `allowsTerm_insertQ10_of_allowsTermQ10`, `allowsTerm_iff_subset_minimallyAllowsTerm`, `FTheory.SU5.Quanta.IsViable.allows_top_yukawa`, `FTheory.SU5.Quanta.isViable_iff_def`, `minimallyAllowsTerm_iff_powerset_countP_eq_one`, `FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff'`, `FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff`, `allowsTerm_of_eq_allowsTermForm`, `allowsTerm_insertQ10_iff_allowsTermQ10`, `allowsTerm_insertQ5_iff_allowsTermQ5`
`AllowsTermQ10` 📖	MathDef	3 math math: `isPhenoConstrainedQ10_iff`, `allowsTerm_insertQ10_iff_allowsTermQ10`, `allowsTermQ10_or_allowsTerm_of_allowsTerm_insertQ10`
`AllowsTermQ5` 📖	MathDef	3 math math: `isPhenoConstrainedQ5_iff`, `allowsTermQ5_or_allowsTerm_of_allowsTerm_insertQ5`, `allowsTerm_insertQ5_iff_allowsTermQ5`
`allowsTermForm` 📖	CompOp	8 math math: `allowsTerm_iff_subset_allowsTermForm`, `allowsTermForm_allowsTerm`, `allowsTermForm_minimallyAllowsTerm`, `eq_allowsTermForm_of_mem_minimallyAllowsTermOfFinset`, `allowsTermForm_map`, `eq_allowsTermForm_of_minimallyAllowsTerm`, `allowsTermForm_subset_allowsTerm_of_allowsTerm`, `allowsTermForm_card_le_degree`
`instDecidableAllowsTermOfDecidableEq` 📖	CompOp	2 math math: `minimallyAllowsTerm_iff_powerset_filter_eq`, `minimallyAllowsTerm_iff_powerset_countP_eq_one`
`instDecidableAllowsTermQ10` 📖	CompOp	—
`instDecidableAllowsTermQ5` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`allowsTermForm_allowsTerm` 📖	mathematical	—	`AllowsTerm` `allowsTermForm`	—	—
`allowsTermForm_card_le_degree` 📖	mathematical	—	`card` `allowsTermForm` `SuperSymmetry.SU5.PotentialTerm.degree`	—	—
`allowsTermForm_eq_of_subset` 📖	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `allowsTermForm`	—	—	`subset_def`
`allowsTermForm_subset_allowsTerm_of_allowsTerm` 📖	mathematical	`AllowsTerm`	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `allowsTermForm`	—	`subset_def`
`allowsTermQ10_or_allowsTerm_of_allowsTerm_insertQ10` 📖	mathematical	`AllowsTerm`	`AllowsTermQ10`	—	—
`allowsTermQ5_or_allowsTerm_of_allowsTerm_insertQ5` 📖	mathematical	`AllowsTerm`	`AllowsTermQ5`	—	—
`allowsTerm_iff_subset_allowsTermForm` 📖	mathematical	—	`AllowsTerm` `SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `allowsTermForm`	—	`allowsTermForm_subset_allowsTerm_of_allowsTerm` `allowsTerm_mono` `allowsTermForm_allowsTerm`
`allowsTerm_iff_zero_mem_ofPotentialTerm'` 📖	mathematical	—	`AllowsTerm` `ofPotentialTerm'`	—	`AllowsTerm.eq_1` `mem_ofPotentialTerm_iff_mem_ofPotentialTerm`
`allowsTerm_insertQ10_iff_allowsTermQ10` 📖	mathematical	—	`AllowsTerm` `AllowsTermQ10`	—	`allowsTermQ10_or_allowsTerm_of_allowsTerm_insertQ10` `allowsTerm_insertQ10_of_allowsTermQ10` `allowsTerm_mono`
`allowsTerm_insertQ10_of_allowsTermQ10` 📖	mathematical	`AllowsTermQ10`	`AllowsTerm`	—	—
`allowsTerm_insertQ5_iff_allowsTermQ5` 📖	mathematical	—	`AllowsTerm` `AllowsTermQ5`	—	`allowsTermQ5_or_allowsTerm_of_allowsTerm_insertQ5` `allowsTerm_insertQ5_of_allowsTermQ5` `allowsTerm_mono`
`allowsTerm_insertQ5_of_allowsTermQ5` 📖	mathematical	`AllowsTermQ5`	`AllowsTerm`	—	—
`allowsTerm_mono` 📖	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `AllowsTerm`	—	—	`ofPotentialTerm_mono`
`allowsTerm_of_eq_allowsTermForm` 📖	mathematical	`allowsTermForm`	`AllowsTerm`	—	`allowsTermForm_allowsTerm`
`subset_card_le_degree_allowsTerm_of_allowsTerm` 📖	mathematical	`AllowsTerm`	`SuperSymmetry.SU5.ChargeSpectrum` `powerset` `card` `SuperSymmetry.SU5.PotentialTerm.degree`	—	`allowsTermForm_subset_allowsTerm_of_allowsTerm` `allowsTermForm_card_le_degree`

---

← Back to Index