Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `Quanta`, `F`, `HdAnomalyCoefficient`, `HuAnomalyCoefficient`, `LinearAnomalyCancellation`, `QuarticAnomalyCancellation`, `T`, `instDecidableEq`, `instDecidableLinearAnomalyCancellationOfDecidableEq`, `instDecidableQuarticAnomalyCancellationOfDecidableEq`, `instRepr`, `liftCharge`, `qHd`, `qHu`, `reduce`, `toCharges`	16
Theorems `HdAnomalyCoefficient_map`, `HuAnomalyCoefficient_map`, `ext`, `ext_iff`, `mem_liftCharge_iff`, `toCharges_of_mem_liftCharge`, `toCharges_qHd`, `toCharges_qHu`	8
Total	24

FTheory.SU5

Definitions

Name	Category	Theorems
`Quanta` 📖	CompData	5 math math: `Quanta.mem_liftCharge_iff`, `Quanta.quarticAnomalyCancellation_iff_mem_of_isViable`, `Quanta.isViable_iff_mem_viableElems`, `Quanta.isViable_iff_filter`, `Quanta.isViable_iff_charges_mem_viableCharges_mem_liftCharges`

FTheory.SU5.Quanta

Definitions

Name	Category	Theorems
`F` 📖	CompOp	7 math math: `mem_liftCharge_iff`, `IsViable.no_five_bar_zero_fluxes`, `isViable_iff_charges_mem_viableCharges`, `IsViable.no_exotics_from_five_bar`, `IsViable.no_duplicate_five_bar_charges`, `isViable_iff_def`, `ext_iff`
`HdAnomalyCoefficient` 📖	CompOp	1 math math: `HdAnomalyCoefficient_map`
`HuAnomalyCoefficient` 📖	CompOp	1 math math: `HuAnomalyCoefficient_map`
`LinearAnomalyCancellation` 📖	MathDef	5 math math: `IsViable.linear_anomalies`, `isViable_iff_charges_mem_viableCharges`, `isViable_iff_def`, `isViable_iff_filter`, `isViable_iff_charges_mem_viableCharges_mem_liftCharges`
`QuarticAnomalyCancellation` 📖	MathDef	1 math math: `quarticAnomalyCancellation_iff_mem_of_isViable`
`T` 📖	CompOp	7 math math: `mem_liftCharge_iff`, `IsViable.no_exotics_from_ten`, `IsViable.no_ten_zero_fluxes`, `IsViable.no_duplicate_ten_charges`, `isViable_iff_charges_mem_viableCharges`, `isViable_iff_def`, `ext_iff`
`instDecidableEq` 📖	CompOp	1 math math: `quarticAnomalyCancellation_iff_mem_of_isViable`
`instDecidableLinearAnomalyCancellationOfDecidableEq` 📖	CompOp	—
`instDecidableQuarticAnomalyCancellationOfDecidableEq` 📖	CompOp	—
`instRepr` 📖	CompOp	—
`liftCharge` 📖	CompOp	3 math math: `mem_liftCharge_iff`, `isViable_iff_filter`, `isViable_iff_charges_mem_viableCharges_mem_liftCharges`
`qHd` 📖	CompOp	3 math math: `mem_liftCharge_iff`, `ext_iff`, `toCharges_qHd`
`qHu` 📖	CompOp	3 math math: `mem_liftCharge_iff`, `ext_iff`, `toCharges_qHu`
`reduce` 📖	CompOp	—
`toCharges` 📖	CompOp	14 math math: `IsViable.not_regenerate_dangerous_couplings`, `isViable_iff_charges_mem_viableCharges`, `toCharges_of_mem_liftCharge`, `IsViable.charges_allowed_by_section_config`, `IsViable.allows_top_yukawa`, `yukawaSingletsRegenerateDangerousInsertion_two_of_isViable`, `isViable_iff_def`, `isViable_iff_filter`, `toCharges_qHd`, `IsViable.has_all_charges`, `map_to_Z2_of_isViable`, `isViable_iff_charges_mem_viableCharges_mem_liftCharges`, `toCharges_qHu`, `IsViable.not_pheno_constrained`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`HdAnomalyCoefficient_map` 📖	mathematical	—	`HdAnomalyCoefficient`	—	—
`HuAnomalyCoefficient_map` 📖	mathematical	—	`HuAnomalyCoefficient`	—	—
`ext` 📖	—	`qHd` `qHu` `F` `T`	—	—	—
`ext_iff` 📖	mathematical	—	`qHd` `qHu` `F` `T`	—	`ext`
`mem_liftCharge_iff` 📖	mathematical	—	`FTheory.SU5.Quanta` `liftCharge` `qHd` `SuperSymmetry.SU5.ChargeSpectrum.qHd` `qHu` `SuperSymmetry.SU5.ChargeSpectrum.qHu` `FTheory.SU5.FiveQuanta` `FTheory.SU5.FiveQuanta.liftCharge` `SuperSymmetry.SU5.ChargeSpectrum.Q5` `F` `FTheory.SU5.TenQuanta` `FTheory.SU5.TenQuanta.liftCharge` `SuperSymmetry.SU5.ChargeSpectrum.Q10` `T`	—	—
`toCharges_of_mem_liftCharge` 📖	mathematical	`FTheory.SU5.Quanta` `liftCharge`	`toCharges`	—	`SuperSymmetry.SU5.ChargeSpectrum.eq_of_parts` `mem_liftCharge_iff` `FTheory.SU5.FiveQuanta.mem_liftCharge_iff` `FTheory.SU5.TenQuanta.mem_liftCharge_iff`
`toCharges_qHd` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum.qHd` `toCharges` `qHd`	—	—
`toCharges_qHu` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum.qHu` `toCharges` `qHu`	—	—

---

← Back to Index