Documentation Verification Report

IsViable

📁 Source: PhysLean/StringTheory/FTheory/SU5/Quanta/IsViable.lean

Statistics

Metric	Count
Definitions `IsViable`, `viableElems`	2
Theorems `allows_top_yukawa`, `charges_allowed_by_section_config`, `has_all_charges`, `linear_anomalies`, `no_duplicate_five_bar_charges`, `no_duplicate_ten_charges`, `no_exotics_from_five_bar`, `no_exotics_from_ten`, `no_five_bar_zero_fluxes`, `no_ten_zero_fluxes`, `not_pheno_constrained`, `not_regenerate_dangerous_couplings`, `isViable_iff_charges_mem_viableCharges`, `isViable_iff_charges_mem_viableCharges_mem_liftCharges`, `isViable_iff_def`, `isViable_iff_filter`, `isViable_iff_mem_viableElems`, `isViable_of_mem_viableElems`, `map_to_Z2_of_isViable`, `quarticAnomalyCancellation_iff_mem_of_isViable`, `yukawaSingletsRegenerateDangerousInsertion_two_of_isViable`	21
Total	23

FTheory.SU5.Quanta

Definitions

Name	Category	Theorems
`IsViable` 📖	CompData	6 math math: `isViable_iff_charges_mem_viableCharges`, `isViable_iff_mem_viableElems`, `isViable_of_mem_viableElems`, `isViable_iff_def`, `isViable_iff_filter`, `isViable_iff_charges_mem_viableCharges_mem_liftCharges`
`viableElems` 📖	CompOp	1 math math: `isViable_iff_mem_viableElems`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isViable_iff_charges_mem_viableCharges` 📖	mathematical	—	`IsViable` `SuperSymmetry.SU5.ChargeSpectrum` `FTheory.SU5.ChargeSpectrum.viableCharges` `toCharges` `FTheory.SU5.FiveQuanta.toCharges` `F` `FTheory.SU5.TenQuanta.toCharges` `T` `FTheory.SU5.FluxesFive.NoExotics` `FTheory.SU5.FiveQuanta.toFluxesFive` `FTheory.SU5.FluxesFive.HasNoZero` `FTheory.SU5.FluxesTen.NoExotics` `FTheory.SU5.TenQuanta.toFluxesTen` `FTheory.SU5.FluxesTen.HasNoZero` `LinearAnomalyCancellation`	—	`isViable_iff_def` `FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff'`
`isViable_iff_charges_mem_viableCharges_mem_liftCharges` 📖	mathematical	—	`IsViable` `SuperSymmetry.SU5.ChargeSpectrum` `FTheory.SU5.ChargeSpectrum.viableCharges` `toCharges` `FTheory.SU5.Quanta` `liftCharge` `LinearAnomalyCancellation`	—	`mem_liftCharge_iff` `FTheory.SU5.FiveQuanta.mem_liftCharge_iff` `FTheory.SU5.TenQuanta.mem_liftCharge_iff` `isViable_iff_charges_mem_viableCharges` `FTheory.SU5.FluxesFive.noExotics_iff_mem_elemsNoExotics` `FTheory.SU5.FluxesTen.noExotics_iff_mem_elemsNoExotics`
`isViable_iff_def` 📖	mathematical	—	`IsViable` `SuperSymmetry.SU5.ChargeSpectrum.IsComplete` `toCharges` `SuperSymmetry.SU5.ChargeSpectrum.IsPhenoConstrained` `SuperSymmetry.SU5.ChargeSpectrum.YukawaGeneratesDangerousAtLevel` `SuperSymmetry.SU5.ChargeSpectrum` `SuperSymmetry.SU5.ChargeSpectrum.ofFinset` `FTheory.SU5.CodimensionOneConfig.allowedBarFiveCharges` `FTheory.SU5.CodimensionOneConfig.allowedTenCharges` `FTheory.SU5.FiveQuanta.toCharges` `F` `FTheory.SU5.TenQuanta.toCharges` `T` `SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm` `SuperSymmetry.SU5.PotentialTerm.topYukawa` `FTheory.SU5.FluxesFive.NoExotics` `FTheory.SU5.FiveQuanta.toFluxesFive` `FTheory.SU5.FluxesFive.HasNoZero` `FTheory.SU5.FluxesTen.NoExotics` `FTheory.SU5.TenQuanta.toFluxesTen` `FTheory.SU5.FluxesTen.HasNoZero` `LinearAnomalyCancellation`	—	—
`isViable_iff_filter` 📖	mathematical	—	`IsViable` `SuperSymmetry.SU5.ChargeSpectrum` `FTheory.SU5.ChargeSpectrum.IsAnomalyFree` `FTheory.SU5.ChargeSpectrum.instDecidableIsAnomalyFree` `FTheory.SU5.ChargeSpectrum.viableCharges` `toCharges` `FTheory.SU5.Quanta` `liftCharge` `LinearAnomalyCancellation`	—	`isViable_iff_charges_mem_viableCharges_mem_liftCharges`
`isViable_iff_mem_viableElems` 📖	mathematical	—	`IsViable` `FTheory.SU5.Quanta` `viableElems`	—	`isViable_iff_filter` `FTheory.SU5.ChargeSpectrum.viable_anomalyFree` `isViable_of_mem_viableElems`
`isViable_of_mem_viableElems` 📖	mathematical	`FTheory.SU5.Quanta` `viableElems`	`IsViable`	—	`isViable_iff_charges_mem_viableCharges_mem_liftCharges`
`map_to_Z2_of_isViable` 📖	mathematical	`IsViable`	`SuperSymmetry.SU5.ChargeSpectrum` `SuperSymmetry.SU5.ChargeSpectrum.instDecidableEq` `SuperSymmetry.SU5.ChargeSpectrum.map` `toCharges`	—	`isViable_iff_mem_viableElems`
`quarticAnomalyCancellation_iff_mem_of_isViable` 📖	mathematical	`IsViable`	`QuarticAnomalyCancellation` `FTheory.SU5.Quanta` `instDecidableEq` `FTheory.SU5.Fluxes` `FTheory.SU5.FiveQuanta` `FTheory.SU5.TenQuanta`	—	`isViable_iff_mem_viableElems`
`yukawaSingletsRegenerateDangerousInsertion_two_of_isViable` 📖	mathematical	`IsViable`	`SuperSymmetry.SU5.ChargeSpectrum.YukawaGeneratesDangerousAtLevel` `toCharges`	—	`isViable_iff_mem_viableElems`

FTheory.SU5.Quanta.IsViable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`allows_top_yukawa` 📖	mathematical	`FTheory.SU5.Quanta.IsViable`	`SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm` `FTheory.SU5.Quanta.toCharges` `SuperSymmetry.SU5.PotentialTerm.topYukawa`	—	—
`charges_allowed_by_section_config` 📖	mathematical	`FTheory.SU5.Quanta.IsViable`	`SuperSymmetry.SU5.ChargeSpectrum` `SuperSymmetry.SU5.ChargeSpectrum.ofFinset` `FTheory.SU5.CodimensionOneConfig.allowedBarFiveCharges` `FTheory.SU5.CodimensionOneConfig.allowedTenCharges` `FTheory.SU5.Quanta.toCharges`	—	—
`has_all_charges` 📖	mathematical	`FTheory.SU5.Quanta.IsViable`	`SuperSymmetry.SU5.ChargeSpectrum.IsComplete` `FTheory.SU5.Quanta.toCharges`	—	—
`linear_anomalies` 📖	mathematical	`FTheory.SU5.Quanta.IsViable`	`FTheory.SU5.Quanta.LinearAnomalyCancellation`	—	—
`no_duplicate_five_bar_charges` 📖	mathematical	`FTheory.SU5.Quanta.IsViable`	`FTheory.SU5.FiveQuanta.toCharges` `FTheory.SU5.Quanta.F`	—	—
`no_duplicate_ten_charges` 📖	mathematical	`FTheory.SU5.Quanta.IsViable`	`FTheory.SU5.TenQuanta.toCharges` `FTheory.SU5.Quanta.T`	—	—
`no_exotics_from_five_bar` 📖	mathematical	`FTheory.SU5.Quanta.IsViable`	`FTheory.SU5.FluxesFive.NoExotics` `FTheory.SU5.FiveQuanta.toFluxesFive` `FTheory.SU5.Quanta.F`	—	—
`no_exotics_from_ten` 📖	mathematical	`FTheory.SU5.Quanta.IsViable`	`FTheory.SU5.FluxesTen.NoExotics` `FTheory.SU5.TenQuanta.toFluxesTen` `FTheory.SU5.Quanta.T`	—	—
`no_five_bar_zero_fluxes` 📖	mathematical	`FTheory.SU5.Quanta.IsViable`	`FTheory.SU5.FluxesFive.HasNoZero` `FTheory.SU5.FiveQuanta.toFluxesFive` `FTheory.SU5.Quanta.F`	—	—
`no_ten_zero_fluxes` 📖	mathematical	`FTheory.SU5.Quanta.IsViable`	`FTheory.SU5.FluxesTen.HasNoZero` `FTheory.SU5.TenQuanta.toFluxesTen` `FTheory.SU5.Quanta.T`	—	—
`not_pheno_constrained` 📖	mathematical	`FTheory.SU5.Quanta.IsViable`	`SuperSymmetry.SU5.ChargeSpectrum.IsPhenoConstrained` `FTheory.SU5.Quanta.toCharges`	—	—
`not_regenerate_dangerous_couplings` 📖	mathematical	`FTheory.SU5.Quanta.IsViable`	`SuperSymmetry.SU5.ChargeSpectrum.YukawaGeneratesDangerousAtLevel` `FTheory.SU5.Quanta.toCharges`	—	—

---

← Back to Index