Documentation Verification Report

OfRationalSection

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

Statistics

MetricCount
DefinitionsCodimensionOneConfig, allowedBarFiveCharges, allowedTenCharges, instFintype, instFintypeSubtypeIntMemFinsetAllowedBarFiveCharges, instFintypeSubtypeIntMemFinsetAllowedTenCharges, instDecidableEqCodimensionOneConfig
7
Theorems0
Total7

FTheory.SU5

Definitions

NameCategoryTheorems
CodimensionOneConfig 📖CompData
2 mathmath: ChargeSpectrum.viableCompletions_card, ChargeSpectrum.viableCharges_card
instDecidableEqCodimensionOneConfig 📖CompOp
2 mathmath: ChargeSpectrum.viableCompletions_card, ChargeSpectrum.viableCharges_card

FTheory.SU5.CodimensionOneConfig

Definitions

NameCategoryTheorems
allowedBarFiveCharges 📖CompOp
6 mathmath: FTheory.SU5.ChargeSpectrum.viableCharges_mem_ofFinset, FTheory.SU5.Quanta.IsViable.charges_allowed_by_section_config, FTheory.SU5.ChargeSpectrum.containsPhenoCompletionsOfMinimallyAllows_viableCompletions, FTheory.SU5.Quanta.isViable_iff_def, FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff', FTheory.SU5.ChargeSpectrum.isPhenoClosedQ5_viableCharges
allowedTenCharges 📖CompOp
6 mathmath: FTheory.SU5.ChargeSpectrum.viableCharges_mem_ofFinset, FTheory.SU5.ChargeSpectrum.isPhenoClosedQ10_viableCharges, FTheory.SU5.Quanta.IsViable.charges_allowed_by_section_config, FTheory.SU5.ChargeSpectrum.containsPhenoCompletionsOfMinimallyAllows_viableCompletions, FTheory.SU5.Quanta.isViable_iff_def, FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff'
instFintype 📖CompOp—
instFintypeSubtypeIntMemFinsetAllowedBarFiveCharges 📖CompOp—
instFintypeSubtypeIntMemFinsetAllowedTenCharges 📖CompOp—

---

← Back to Index