Basic

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

Statistics

Metric	Count
Definitions `powerset`, `ChargeSpectrum`, `Q10`, `Q5`, `card`, `emptyInst`, `hasSSubset`, `hasSubset`, `instDecidableEq`, `instRepr`, `ofFinset`, `ofFinsetCard`, `powerset`, `qHd`, `qHu`, `subsetDecidable`, `toProd`	17
Theorems `mem_powerset_iff`, `toFinset_inj`, `card_empty`, `card_mono`, `empty_Q10`, `empty_Q5`, `empty_mem_powerset`, `empty_qHd`, `empty_qHu`, `empty_subset`, `eq_iff`, `eq_of_parts`, `eq_of_subset_card`, `mem_ofFinset_antitone`, `mem_ofFinset_iff`, `mem_powerset_iff`, `mem_powerset_iff_subset`, `min_exists`, `min_exists_inductive`, `ofFinset_card_eq_ofFinsetCard`, `ofFinset_subset_of_subset`, `ofFinset_univ`, `powerset_mono`, `powerset_of_empty`, `self_mem_powerset`, `subset_antisymm`, `subset_def`, `subset_of_empty_iff_empty`, `subset_refl`, `subset_trans`	30
Total	47

Option

Definitions

Name	Category	Theorems
`powerset` 📖	CompOp	2 math math: `SuperSymmetry.SU5.ChargeSpectrum.mem_powerset_iff`, `mem_powerset_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_powerset_iff` 📖	mathematical	—	`powerset`	—	—
`toFinset_inj` 📖	—	—	—	—	—

SuperSymmetry.SU5

Definitions

Name	Category	Theorems
`ChargeSpectrum` 📖	CompData	72 math math: `FTheory.SU5.ChargeSpectrum.viable_anomalyFree`, `ChargeSpectrum.not_yukawaGeneratesDangerousAtLevel_of_empty`, `ChargeSpectrum.minimallyAllowsTermOfFinset_subset_ofFinset`, `ChargeSpectrum.completeMinSubset_subset_iff_containsPhenoCompletionsOfMinimallyAllows`, `ChargeSpectrum.mem_ofFinset_iff`, `ChargeSpectrum.allowsTerm_iff_subset_allowsTermForm`, `ChargeSpectrum.ofFinset_card_eq_ofFinsetCard`, `ChargeSpectrum.minimallyAllowsTerm_iff_powerset_filter_eq`, `ChargeSpectrum.self_mem_completions_iff_isComplete`, `ChargeSpectrum.empty_mem_powerset`, `ChargeSpectrum.subset_refl`, `ChargeSpectrum.not_isComplete_empty`, `ChargeSpectrum.completeMinSubset_nodup`, `FTheory.SU5.ChargeSpectrum.viableCompletions_card`, `ChargeSpectrum.self_mem_powerset`, `ChargeSpectrum.ZModCharges_three_eq`, `ChargeSpectrum.ofFinset_subset_of_subset`, `ChargeSpectrum.not_isPhenoConstrained_empty`, `ChargeSpectrum.self_not_mem_minimalSuperSet`, `ChargeSpectrum.map_empty`, `ChargeSpectrum.insert_Q10_mem_minimalSuperSet`, `FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges`, `FTheory.SU5.ChargeSpectrum.viableChargesAdditional_nodup`, `ChargeSpectrum.preimageOfFinset_eq`, `ChargeSpectrum.mem_completions_iff`, `ChargeSpectrum.ZModCharges_six_eq`, `ChargeSpectrum.insert_Q5_mem_minimalSuperSet`, `FTheory.SU5.Quanta.IsViable.charges_allowed_by_section_config`, `ChargeSpectrum.completionsTopYukawa_nodup`, `ChargeSpectrum.preimageOfFinset_card_eq`, `ChargeSpectrum.card_empty`, `ChargeSpectrum.minimallyAllowsTermOfFinset_subset_of_subset`, `ChargeSpectrum.ofPotentialTerm_empty`, `ChargeSpectrum.completions_eq_singleton_of_complete`, `ChargeSpectrum.subset_def`, `ChargeSpectrum.empty_subset`, `ChargeSpectrum.ofPotentialTerm'_empty`, `ChargeSpectrum.allowsTerm_iff_subset_minimallyAllowsTerm`, `ChargeSpectrum.powerset_mono`, `ChargeSpectrum.empty_qHd`, `ChargeSpectrum.some_qHu_mem_minimalSuperSet_of_none`, `FTheory.SU5.Quanta.isViable_iff_def`, `ChargeSpectrum.empty_qHu`, `ChargeSpectrum.empty_Q5`, `ChargeSpectrum.some_qHd_mem_minimalSuperSet_of_none`, `ChargeSpectrum.ZModCharges_one_eq`, `ChargeSpectrum.min_exists`, `FTheory.SU5.ChargeSpectrum.viableCharges_card`, `ChargeSpectrum.minimallyAllowsTerm_iff_powerset_countP_eq_one`, `ChargeSpectrum.ofFieldLabel_empty`, `ChargeSpectrum.subset_minimallyAllowsTerm_of_allowsTerm`, `ChargeSpectrum.subset_of_empty_iff_empty`, `ChargeSpectrum.mem_powerset_iff`, `ChargeSpectrum.completions_nodup`, `FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff'`, `ChargeSpectrum.ZModCharges_five_eq`, `FTheory.SU5.Quanta.isViable_iff_filter`, `ChargeSpectrum.mem_powerset_iff_subset`, `ChargeSpectrum.ofFinset_univ`, `ChargeSpectrum.powerset_of_empty`, `FTheory.SU5.Quanta.map_to_Z2_of_isViable`, `ChargeSpectrum.ZModCharges_two_eq`, `ChargeSpectrum.containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawa`, `FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges_mem_liftCharges`, `FTheory.SU5.ChargeSpectrum.viableCompletions_disjiont_viableChargesAdditional`, `ChargeSpectrum.phenoConstrainingChargesSP_empty`, `ChargeSpectrum.allowsTermForm_subset_allowsTerm_of_allowsTerm`, `ChargeSpectrum.empty_Q10`, `FTheory.SU5.ChargeSpectrum.viableCompletions_nodup`, `ChargeSpectrum.ZModCharges_four_eq`, `ChargeSpectrum.subset_card_le_degree_allowsTerm_of_allowsTerm`, `FTheory.SU5.ChargeSpectrum.viableCharges_nodup`

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`Q10` 📖	CompOp	13 math math: `FTheory.SU5.Quanta.mem_liftCharge_iff`, `mem_ofFinset_iff`, `ofPotentialTerm'_topYukawa_finset`, `mem_completions_iff`, `insert_Q5_mem_minimalSuperSet`, `eq_iff`, `subset_def`, `FTheory.SU5.ChargeSpectrum.card_ten_le_of_mem_viableCharges`, `ofPotentialTerm'_W2_finset`, `mem_powerset_iff`, `empty_Q10`, `ofPotentialTerm'_bottomYukawa_finset`, `ofPotentialTerm'_K2_finset`
`Q5` 📖	CompOp	13 math math: `FTheory.SU5.Quanta.mem_liftCharge_iff`, `mem_ofFinset_iff`, `ofPotentialTerm'_W4_finset`, `insert_Q10_mem_minimalSuperSet`, `ofPotentialTerm'_β_finset`, `mem_completions_iff`, `eq_iff`, `subset_def`, `FTheory.SU5.ChargeSpectrum.card_five_bar_le_of_mem_viableCharges`, `ofPotentialTerm'_W3_finset`, `empty_Q5`, `mem_powerset_iff`, `ofPotentialTerm'_bottomYukawa_finset`
`card` 📖	CompOp	6 math math: `card_mono`, `card_empty`, `allowsTermForm_card_le_degree`, `card_of_mem_minimalSuperSet`, `card_le_degree_of_minimallyAllowsTerm`, `subset_card_le_degree_allowsTerm_of_allowsTerm`
`emptyInst` 📖	CompOp	17 math math: `not_yukawaGeneratesDangerousAtLevel_of_empty`, `empty_mem_powerset`, `not_isComplete_empty`, `not_isPhenoConstrained_empty`, `map_empty`, `card_empty`, `ofPotentialTerm_empty`, `empty_subset`, `ofPotentialTerm'_empty`, `empty_qHd`, `empty_qHu`, `empty_Q5`, `ofFieldLabel_empty`, `subset_of_empty_iff_empty`, `powerset_of_empty`, `phenoConstrainingChargesSP_empty`, `empty_Q10`
`hasSSubset` 📖	CompOp	—
`hasSubset` 📖	CompOp	10 math math: `allowsTerm_iff_subset_allowsTermForm`, `subset_refl`, `subset_def`, `empty_subset`, `powerset_mono`, `self_subset_mem_minimalSuperSet`, `subset_of_empty_iff_empty`, `mem_powerset_iff_subset`, `self_subset_mem_completions`, `allowsTermForm_subset_allowsTerm_of_allowsTerm`
`instDecidableEq` 📖	CompOp	5 math math: `min_exists_inductive`, `ZModCharges_six_eq`, `min_exists`, `FTheory.SU5.Quanta.map_to_Z2_of_isViable`, `ZModCharges_four_eq`
`instRepr` 📖	CompOp	—
`ofFinset` 📖	CompOp	11 math math: `minimallyAllowsTermOfFinset_subset_ofFinset`, `mem_ofFinset_iff`, `ofFinset_card_eq_ofFinsetCard`, `FTheory.SU5.ChargeSpectrum.viableCharges_mem_ofFinset`, `ofFinset_subset_of_subset`, `preimageOfFinset_eq`, `mem_ofFinset_of_mem_minimallyAllowsTermOfFinset`, `FTheory.SU5.Quanta.IsViable.charges_allowed_by_section_config`, `FTheory.SU5.Quanta.isViable_iff_def`, `FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff'`, `ofFinset_univ`
`ofFinsetCard` 📖	CompOp	1 math math: `ofFinset_card_eq_ofFinsetCard`
`powerset` 📖	CompOp	13 math math: `min_exists_inductive`, `minimallyAllowsTerm_iff_powerset_filter_eq`, `empty_mem_powerset`, `self_mem_powerset`, `allowsTerm_iff_subset_minimallyAllowsTerm`, `powerset_mono`, `min_exists`, `minimallyAllowsTerm_iff_powerset_countP_eq_one`, `subset_minimallyAllowsTerm_of_allowsTerm`, `mem_powerset_iff`, `mem_powerset_iff_subset`, `powerset_of_empty`, `subset_card_le_degree_allowsTerm_of_allowsTerm`
`qHd` 📖	CompOp	15 math math: `FTheory.SU5.Quanta.mem_liftCharge_iff`, `mem_ofFinset_iff`, `ofPotentialTerm'_W4_finset`, `insert_Q10_mem_minimalSuperSet`, `mem_completions_iff`, `insert_Q5_mem_minimalSuperSet`, `eq_iff`, `subset_def`, `empty_qHd`, `ofPotentialTerm'_W2_finset`, `mem_powerset_iff`, `FTheory.SU5.Quanta.toCharges_qHd`, `ofPotentialTerm'_μ_finset`, `ofPotentialTerm'_bottomYukawa_finset`, `ofPotentialTerm'_K2_finset`
`qHu` 📖	CompOp	16 math math: `FTheory.SU5.Quanta.mem_liftCharge_iff`, `mem_ofFinset_iff`, `ofPotentialTerm'_W4_finset`, `insert_Q10_mem_minimalSuperSet`, `ofPotentialTerm'_topYukawa_finset`, `ofPotentialTerm'_β_finset`, `mem_completions_iff`, `insert_Q5_mem_minimalSuperSet`, `eq_iff`, `subset_def`, `ofPotentialTerm'_W3_finset`, `empty_qHu`, `mem_powerset_iff`, `ofPotentialTerm'_μ_finset`, `FTheory.SU5.Quanta.toCharges_qHu`, `ofPotentialTerm'_K2_finset`
`subsetDecidable` 📖	CompOp	—
`toProd` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_empty` 📖	mathematical	—	`card` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	—
`card_mono` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset`	`card`	—	—
`empty_Q10` 📖	mathematical	—	`Q10` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	—
`empty_Q5` 📖	mathematical	—	`Q5` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	—
`empty_mem_powerset` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `powerset` `emptyInst`	—	—
`empty_qHd` 📖	mathematical	—	`qHd` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	—
`empty_qHu` 📖	mathematical	—	`qHu` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	—
`empty_subset` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `emptyInst`	—	—
`eq_iff` 📖	mathematical	—	`qHd` `qHu` `Q5` `Q10`	—	`eq_of_parts`
`eq_of_parts` 📖	—	`qHd` `qHu` `Q5` `Q10`	—	—	—
`eq_of_subset_card` 📖	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `card`	—	—	—
`mem_ofFinset_antitone` 📖	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `ofFinset`	—	—	`mem_ofFinset_iff`
`mem_ofFinset_iff` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `ofFinset` `qHd` `qHu` `Q5` `Q10`	—	—
`mem_powerset_iff` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `powerset` `Option.powerset` `qHd` `qHu` `Q5` `Q10`	—	—
`mem_powerset_iff_subset` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `powerset` `hasSubset`	—	—
`min_exists` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `instDecidableEq` `powerset`	—	`min_exists_inductive`
`min_exists_inductive` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum`	`instDecidableEq` `powerset`	—	`subset_trans` `subset_antisymm`
`ofFinset_card_eq_ofFinsetCard` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `ofFinset` `ofFinsetCard`	—	—
`ofFinset_subset_of_subset` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `ofFinset`	—	`mem_ofFinset_iff`
`ofFinset_univ` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `ofFinset`	—	`mem_ofFinset_iff`
`powerset_mono` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `powerset` `hasSubset`	—	`mem_powerset_iff_subset` `subset_trans`
`powerset_of_empty` 📖	mathematical	—	`powerset` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	—
`self_mem_powerset` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `powerset`	—	—
`subset_antisymm` 📖	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset`	—	—	`HasSubset.Subset.eq_1`
`subset_def` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `qHd` `qHu` `Q5` `Q10`	—	—
`subset_of_empty_iff_empty` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `emptyInst`	—	`subset_antisymm` `empty_subset`
`subset_refl` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset`	—	—
`subset_trans` 📖	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset`	—	—	—

---

← Back to Index