Viable

📁 Source: PhysLean/StringTheory/FTheory/SU5/Charges/Viable.lean

Statistics

Metric	Count
Definitions `viableCharges`, `viableChargesAdditional`	2
Theorems `allowsTerm_topYukawa_of_mem_viableCharges`, `card_five_bar_le_of_mem_viableCharges`, `card_ten_le_of_mem_viableCharges`, `containsPhenoCompletionsOfMinimallyAllows_viableCompletions`, `isComplete_of_mem_viableCharges`, `isPhenoClosedQ10_viableCharges`, `isPhenoClosedQ5_viableCharges`, `mem_viableCharges_iff`, `mem_viableCharges_iff'`, `not_isPhenoConstrained_of_mem_viableCharges`, `not_isPhenoConstrained_of_mem_viableChargesAdditional`, `not_yukawaGeneratesDangerousAtLevel_one_of_mem_viableCharges`, `viableChargesAdditional_nodup`, `viableCharges_card`, `viableCharges_mem_ofFinset`, `viableCharges_nodup`, `viableCompletions_card`, `viableCompletions_disjiont_viableChargesAdditional`, `viableCompletions_isPhenoConstrained`, `viableCompletions_nodup`, `viableCompletions_subset_viableCharges`, `viableCompletions_yukawaGeneratesDangerousAtLevel_one`, `yukawaGeneratesDangerousAtLevel_one_of_mem_viableChargesAdditional`	23
Total	25

FTheory.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`viableCharges` 📖	CompOp	11 math math: `viable_anomalyFree`, `viableCompletions_subset_viableCharges`, `isPhenoClosedQ10_viableCharges`, `FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges`, `viableCharges_card`, `mem_viableCharges_iff'`, `FTheory.SU5.Quanta.isViable_iff_filter`, `mem_viableCharges_iff`, `isPhenoClosedQ5_viableCharges`, `FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges_mem_liftCharges`, `viableCharges_nodup`
`viableChargesAdditional` 📖	CompOp	2 math math: `viableChargesAdditional_nodup`, `viableCompletions_disjiont_viableChargesAdditional`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`allowsTerm_topYukawa_of_mem_viableCharges` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `viableCharges`	`SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm` `SuperSymmetry.SU5.PotentialTerm.topYukawa`	—	—
`card_five_bar_le_of_mem_viableCharges` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `viableCharges`	`SuperSymmetry.SU5.ChargeSpectrum.Q5`	—	—
`card_ten_le_of_mem_viableCharges` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `viableCharges`	`SuperSymmetry.SU5.ChargeSpectrum.Q10`	—	—
`containsPhenoCompletionsOfMinimallyAllows_viableCompletions` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum.ContainsPhenoCompletionsOfMinimallyAllows` `FTheory.SU5.CodimensionOneConfig.allowedBarFiveCharges` `FTheory.SU5.CodimensionOneConfig.allowedTenCharges`	—	—
`isComplete_of_mem_viableCharges` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `viableCharges`	`SuperSymmetry.SU5.ChargeSpectrum.IsComplete`	—	—
`isPhenoClosedQ10_viableCharges` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum.IsPhenoClosedQ10` `FTheory.SU5.CodimensionOneConfig.allowedTenCharges` `viableCharges`	—	`SuperSymmetry.SU5.ChargeSpectrum.isPhenClosedQ10_of_isPhenoConstrainedQ10`
`isPhenoClosedQ5_viableCharges` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum.IsPhenoClosedQ5` `FTheory.SU5.CodimensionOneConfig.allowedBarFiveCharges` `viableCharges`	—	`SuperSymmetry.SU5.ChargeSpectrum.isPhenClosedQ5_of_isPhenoConstrainedQ5`
`mem_viableCharges_iff` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `SuperSymmetry.SU5.ChargeSpectrum.ofFinset` `FTheory.SU5.CodimensionOneConfig.allowedBarFiveCharges` `FTheory.SU5.CodimensionOneConfig.allowedTenCharges`	`viableCharges` `SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm` `SuperSymmetry.SU5.PotentialTerm.topYukawa` `SuperSymmetry.SU5.ChargeSpectrum.IsPhenoConstrained` `SuperSymmetry.SU5.ChargeSpectrum.YukawaGeneratesDangerousAtLevel` `SuperSymmetry.SU5.ChargeSpectrum.IsComplete`	—	`SuperSymmetry.SU5.ChargeSpectrum.completeness_of_isPhenoClosedQ5_isPhenoClosedQ10` `allowsTerm_topYukawa_of_mem_viableCharges` `not_isPhenoConstrained_of_mem_viableCharges` `not_yukawaGeneratesDangerousAtLevel_one_of_mem_viableCharges` `isComplete_of_mem_viableCharges` `isPhenoClosedQ5_viableCharges` `isPhenoClosedQ10_viableCharges` `SuperSymmetry.SU5.ChargeSpectrum.containsPhenoCompletionsOfMinimallyAllows_of_subset` `containsPhenoCompletionsOfMinimallyAllows_viableCompletions` `viableCompletions_subset_viableCharges`
`mem_viableCharges_iff'` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `viableCharges` `SuperSymmetry.SU5.ChargeSpectrum.ofFinset` `FTheory.SU5.CodimensionOneConfig.allowedBarFiveCharges` `FTheory.SU5.CodimensionOneConfig.allowedTenCharges` `SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm` `SuperSymmetry.SU5.PotentialTerm.topYukawa` `SuperSymmetry.SU5.ChargeSpectrum.IsPhenoConstrained` `SuperSymmetry.SU5.ChargeSpectrum.YukawaGeneratesDangerousAtLevel` `SuperSymmetry.SU5.ChargeSpectrum.IsComplete`	—	`viableCharges_mem_ofFinset` `mem_viableCharges_iff`
`not_isPhenoConstrained_of_mem_viableCharges` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `viableCharges`	`SuperSymmetry.SU5.ChargeSpectrum.IsPhenoConstrained`	—	`viableCharges.eq_1` `viableCompletions_isPhenoConstrained` `not_isPhenoConstrained_of_mem_viableChargesAdditional`
`not_isPhenoConstrained_of_mem_viableChargesAdditional` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `viableChargesAdditional`	`SuperSymmetry.SU5.ChargeSpectrum.IsPhenoConstrained`	—	—
`not_yukawaGeneratesDangerousAtLevel_one_of_mem_viableCharges` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `viableCharges`	`SuperSymmetry.SU5.ChargeSpectrum.YukawaGeneratesDangerousAtLevel`	—	`viableCharges.eq_1` `viableCompletions_yukawaGeneratesDangerousAtLevel_one` `yukawaGeneratesDangerousAtLevel_one_of_mem_viableChargesAdditional`
`viableChargesAdditional_nodup` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `viableChargesAdditional`	—	—
`viableCharges_card` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `viableCharges` `FTheory.SU5.CodimensionOneConfig` `FTheory.SU5.CodimensionOneConfig.same` `FTheory.SU5.instDecidableEqCodimensionOneConfig` `FTheory.SU5.CodimensionOneConfig.nearestNeighbor`	—	—
`viableCharges_mem_ofFinset` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `viableCharges`	`SuperSymmetry.SU5.ChargeSpectrum.ofFinset` `FTheory.SU5.CodimensionOneConfig.allowedBarFiveCharges` `FTheory.SU5.CodimensionOneConfig.allowedTenCharges`	—	—
`viableCharges_nodup` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `viableCharges`	—	`viableCompletions_nodup` `viableChargesAdditional_nodup` `viableCompletions_disjiont_viableChargesAdditional`
`viableCompletions_card` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `FTheory.SU5.CodimensionOneConfig` `FTheory.SU5.CodimensionOneConfig.same` `FTheory.SU5.instDecidableEqCodimensionOneConfig` `FTheory.SU5.CodimensionOneConfig.nearestNeighbor`	—	—
`viableCompletions_disjiont_viableChargesAdditional` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `viableChargesAdditional`	—	—
`viableCompletions_isPhenoConstrained` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum`	`SuperSymmetry.SU5.ChargeSpectrum.IsPhenoConstrained`	—	—
`viableCompletions_nodup` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum`	—	—
`viableCompletions_subset_viableCharges` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum`	`viableCharges`	—	`viableCharges.eq_1`
`viableCompletions_yukawaGeneratesDangerousAtLevel_one` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum`	`SuperSymmetry.SU5.ChargeSpectrum.YukawaGeneratesDangerousAtLevel`	—	—
`yukawaGeneratesDangerousAtLevel_one_of_mem_viableChargesAdditional` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `viableChargesAdditional`	`SuperSymmetry.SU5.ChargeSpectrum.YukawaGeneratesDangerousAtLevel`	—	—

---

← Back to Index