Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `Fluxes`, `M`, `N`, `instAdd`, `instAddCommMonoid`, `instRepr`, `instZero`, `FluxesFive`, `HasNoZero`, `NoExotics`, `chiralIndicesOfD`, `chiralIndicesOfL`, `instDecidableEq`, `instDecidableNoExotics`, `numAntiChiralD`, `numAntiChiralL`, `numChiralD`, `numChiralL`, `FluxesTen`, `HasNoZero`, `NoExotics`, `chiralIndicesOfE`, `chiralIndicesOfQ`, `chiralIndicesOfU`, `instDecidableEq`, `instDecidableNoExotics`, `numAntiChiralE`, `numAntiChiralQ`, `numAntiChiralU`, `numChiralE`, `numChiralQ`, `numChiralU`, `instDecidableEqFluxes`, `decEq`	34
Theorems `add_M`, `add_N`, `ext_iff`, `zero_M`, `zero_N`, `numChiralD_eq_sum_sub_numAntiChiralD`, `numChiralL_eq_sum_sub_numAntiChiralL`, `numChiralE_eq_sum_sub_numAntiChiralE`, `numChiralQ_eq_sum_sub_numAntiChiralQ`, `numChiralU_eq_sum_sub_numAntiChiralU`	10
Total	44

FTheory.SU5

Definitions

Name	Category	Theorems
`Fluxes` 📖	CompData	40 math math: `TenQuanta.exists_toCharges_toFluxesTen_of_mem_liftCharge`, `FiveQuanta.map_liftCharge`, `TenQuanta.decompose_toFluxesTen`, `FiveQuanta.mem_liftCharge_iff_exists`, `FluxesTen.card_le_three_of_noExotics`, `FluxesFive.card_mem_range_seven_of_noExotics`, `TenQuanta.map_liftCharge`, `FiveQuanta.reduce_nodup`, `FiveQuanta.mem_reduce_iff`, `TenQuanta.decompose_filter_charge`, `TenQuanta.reduce_filter`, `TenQuanta.mem_reduce_iff`, `TenQuanta.toChargeMap_of_not_mem`, `Fluxes.zero_M`, `FluxesTen.sum_of_mem_elemsNoExotics`, `FiveQuanta.reduce_filter`, `FiveQuanta.decompose_filter_charge`, `FluxesTen.card_mem_range_four_of_noExotics`, `FiveQuanta.decompose_add`, `FiveQuanta.reduce_sum_eq_sum_toCharges`, `TenQuanta.anomalyCoefficient_of_map`, `Quanta.quarticAnomalyCancellation_iff_mem_of_isViable`, `TenQuanta.decompose_add`, `FiveQuanta.decompose_toFluxesFive`, `Fluxes.add_M`, `FluxesFive.toFinset_card_le_four_mem_elemsNoExotics`, `TenQuanta.reduce_sum_eq_sum_toCharges`, `FiveQuanta.exists_toCharges_toFluxesFive_of_mem_liftCharge`, `FiveQuanta.toChargeMap_of_not_mem`, `FiveQuanta.anomalyCoefficient_of_map`, `FiveQuanta.reduce_dedup`, `Fluxes.add_N`, `FluxesFive.sum_of_mem_elemsNoExotics`, `TenQuanta.reduce_nodup`, `FluxesFive.card_le_six_mem_elemsNoExotics`, `FluxesTen.toFinset_card_le_three_mem_elemsNoExotics`, `Fluxes.zero_N`, `TenQuanta.mem_liftCharge_iff_exists`, `FluxesFive.card_le_six_of_noExotics`, `TenQuanta.reduce_dedup`
`FluxesFive` 📖	CompOp	7 math math: `FluxesFive.noExotics_iff_mem_elemsNoExotics`, `FiveQuanta.mem_liftCharge_iff_exists`, `FluxesFive.elemsNoExotics_card`, `FluxesFive.mem_elemsNoExotics_of_noExotics`, `FiveQuanta.exists_toCharges_toFluxesFive_of_mem_liftCharge`, `FiveQuanta.mem_liftCharge_iff`, `FluxesFive.elemsNoExotics_nodup`
`FluxesTen` 📖	CompOp	7 math math: `TenQuanta.exists_toCharges_toFluxesTen_of_mem_liftCharge`, `FluxesTen.elemsNoExotics_card`, `TenQuanta.mem_liftCharge_iff`, `FluxesTen.mem_elemsNoExotics_of_noExotics`, `FluxesTen.noExotics_iff_mem_elemsNoExotics`, `FluxesTen.elemsNoExotics_nodup`, `TenQuanta.mem_liftCharge_iff_exists`
`instDecidableEqFluxes` 📖	CompOp	6 math math: `FluxesFive.mem_mem_finset_of_noExotics`, `FluxesTen.mem_mem_finset_of_noExotics`, `FluxesFive.toFinset_card_le_four_mem_elemsNoExotics`, `FiveQuanta.reduce_dedup`, `FluxesTen.toFinset_card_le_three_mem_elemsNoExotics`, `TenQuanta.reduce_dedup`

FTheory.SU5.Fluxes

Definitions

Name	Category	Theorems
`M` 📖	CompOp	9 math math: `FTheory.SU5.FluxesFive.chiralIndicesOfL_subset_sum_le_three_of_noExotics`, `FTheory.SU5.FluxesTen.chiralIndicesOfE_subset_sum_le_three_of_noExotics`, `ext_iff`, `zero_M`, `FTheory.SU5.FluxesFive.map_sum_add_of_mem_powerset_elemsNoExotics`, `FTheory.SU5.FluxesFive.chiralIndicesOfD_subset_sum_le_three_of_noExotics`, `add_M`, `FTheory.SU5.FluxesTen.chiralIndicesOfU_subset_sum_le_three_of_noExotics`, `FTheory.SU5.FluxesTen.chiralIndicesOfQ_subset_sum_le_three_of_noExotics`
`N` 📖	CompOp	7 math math: `FTheory.SU5.FluxesFive.chiralIndicesOfL_subset_sum_le_three_of_noExotics`, `FTheory.SU5.FluxesTen.chiralIndicesOfE_subset_sum_le_three_of_noExotics`, `ext_iff`, `FTheory.SU5.FluxesFive.map_sum_add_of_mem_powerset_elemsNoExotics`, `FTheory.SU5.FluxesTen.chiralIndicesOfU_subset_sum_le_three_of_noExotics`, `add_N`, `zero_N`
`instAdd` 📖	CompOp	3 math math: `FTheory.SU5.FluxesFive.map_sum_add_of_mem_powerset_elemsNoExotics`, `add_M`, `add_N`
`instAddCommMonoid` 📖	CompOp	15 math math: `FTheory.SU5.TenQuanta.mem_powerset_sum_of_mem_reduce_toFluxesTen_filter`, `FTheory.SU5.FiveQuanta.mem_reduce_iff`, `FTheory.SU5.TenQuanta.reduce_filter`, `FTheory.SU5.TenQuanta.mem_reduce_iff`, `FTheory.SU5.FluxesTen.sum_of_mem_elemsNoExotics`, `FTheory.SU5.FluxesFive.map_sum_add_of_mem_powerset_elemsNoExotics`, `FTheory.SU5.FiveQuanta.decomposeFluxes_sum_of_noExotics`, `FTheory.SU5.FiveQuanta.reduce_filter`, `FTheory.SU5.FiveQuanta.reduce_sum_eq_sum_toCharges`, `FTheory.SU5.FiveQuanta.mem_powerset_sum_of_mem_reduce_toFluxesFive`, `FTheory.SU5.TenQuanta.reduce_sum_eq_sum_toCharges`, `FTheory.SU5.TenQuanta.decomposeFluxes_sum_of_noExotics`, `FTheory.SU5.FluxesFive.sum_of_mem_elemsNoExotics`, `FTheory.SU5.TenQuanta.mem_powerset_sum_of_mem_reduce_toFluxesTen`, `FTheory.SU5.FiveQuanta.mem_powerset_sum_of_mem_reduce_toFluxesFive_filter`
`instRepr` 📖	CompOp	—
`instZero` 📖	CompOp	4 math math: `FTheory.SU5.TenQuanta.toChargeMap_of_not_mem`, `zero_M`, `FTheory.SU5.FiveQuanta.toChargeMap_of_not_mem`, `zero_N`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_M` 📖	mathematical	—	`M` `FTheory.SU5.Fluxes` `instAdd`	—	—
`add_N` 📖	mathematical	—	`N` `FTheory.SU5.Fluxes` `instAdd`	—	—
`ext_iff` 📖	mathematical	—	`M` `N`	—	—
`zero_M` 📖	mathematical	—	`M` `FTheory.SU5.Fluxes` `instZero`	—	—
`zero_N` 📖	mathematical	—	`N` `FTheory.SU5.Fluxes` `instZero`	—	—

FTheory.SU5.FluxesFive

Definitions

Name	Category	Theorems
`HasNoZero` 📖	MathDef	6 math math: `noExotics_iff_mem_elemsNoExotics`, `FTheory.SU5.Quanta.IsViable.no_five_bar_zero_fluxes`, `FTheory.SU5.FiveQuanta.hasNoZero_of_mem_liftCharge`, `FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges`, `FTheory.SU5.Quanta.isViable_iff_def`, `hasNoZero_of_mem_elemsNoExotics`
`NoExotics` 📖	MathDef	7 math math: `noExotics_iff_mem_elemsNoExotics`, `FTheory.SU5.FiveQuanta.reduce_noExotics_of_mem_elemsNoExotics`, `FTheory.SU5.FiveQuanta.noExotics_of_mem_liftCharge`, `FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges`, `FTheory.SU5.Quanta.IsViable.no_exotics_from_five_bar`, `FTheory.SU5.Quanta.isViable_iff_def`, `noExotics_of_mem_elemsNoExotics`
`chiralIndicesOfD` 📖	CompOp	2 math math: `chiralIndicesOfD_sum_eq_three_of_noExotics`, `numChiralD_eq_sum_sub_numAntiChiralD`
`chiralIndicesOfL` 📖	CompOp	2 math math: `chiralIndicesOfL_sum_eq_three_of_noExotics`, `numChiralL_eq_sum_sub_numAntiChiralL`
`instDecidableEq` 📖	CompOp	—
`instDecidableNoExotics` 📖	CompOp	—
`numAntiChiralD` 📖	CompOp	2 math math: `numChiralD_eq_sum_sub_numAntiChiralD`, `FTheory.SU5.FiveQuanta.reduce_numAntiChiralD_of_mem_elemsNoExotics`
`numAntiChiralL` 📖	CompOp	2 math math: `FTheory.SU5.FiveQuanta.reduce_numAntiChiralL_of_mem_elemsNoExotics`, `numChiralL_eq_sum_sub_numAntiChiralL`
`numChiralD` 📖	CompOp	2 math math: `FTheory.SU5.FiveQuanta.reduce_numChiralD_of_mem_elemsNoExotics`, `numChiralD_eq_sum_sub_numAntiChiralD`
`numChiralL` 📖	CompOp	2 math math: `FTheory.SU5.FiveQuanta.reduce_numChiralL_of_mem_elemsNoExotics`, `numChiralL_eq_sum_sub_numAntiChiralL`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`numChiralD_eq_sum_sub_numAntiChiralD` 📖	mathematical	—	`numChiralD` `chiralIndicesOfD` `numAntiChiralD`	—	—
`numChiralL_eq_sum_sub_numAntiChiralL` 📖	mathematical	—	`numChiralL` `chiralIndicesOfL` `numAntiChiralL`	—	—

FTheory.SU5.FluxesTen

Definitions

Name	Category	Theorems
`HasNoZero` 📖	MathDef	6 math math: `FTheory.SU5.TenQuanta.hasNoZero_of_mem_liftCharge`, `FTheory.SU5.Quanta.IsViable.no_ten_zero_fluxes`, `FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges`, `noExotics_iff_mem_elemsNoExotics`, `FTheory.SU5.Quanta.isViable_iff_def`, `hasNoZero_of_mem_elemsNoExotics`
`NoExotics` 📖	MathDef	7 math math: `FTheory.SU5.Quanta.IsViable.no_exotics_from_ten`, `FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges`, `noExotics_iff_mem_elemsNoExotics`, `FTheory.SU5.Quanta.isViable_iff_def`, `FTheory.SU5.TenQuanta.reduce_noExotics_of_mem_elemsNoExotics`, `FTheory.SU5.TenQuanta.noExotics_of_mem_liftCharge`, `noExotics_of_mem_elemsNoExotics`
`chiralIndicesOfE` 📖	CompOp	2 math math: `numChiralE_eq_sum_sub_numAntiChiralE`, `chiralIndicesOfE_sum_eq_three_of_noExotics`
`chiralIndicesOfQ` 📖	CompOp	2 math math: `numChiralQ_eq_sum_sub_numAntiChiralQ`, `chiralIndicesOfQ_sum_eq_three_of_noExotics`
`chiralIndicesOfU` 📖	CompOp	2 math math: `numChiralU_eq_sum_sub_numAntiChiralU`, `chiralIndicesOfU_sum_eq_three_of_noExotics`
`instDecidableEq` 📖	CompOp	2 math math: `FTheory.SU5.TenQuanta.mem_powerset_sum_of_mem_reduce_toFluxesTen_filter`, `FTheory.SU5.FiveQuanta.mem_powerset_sum_of_mem_reduce_toFluxesFive_filter`
`instDecidableNoExotics` 📖	CompOp	—
`numAntiChiralE` 📖	CompOp	2 math math: `numChiralE_eq_sum_sub_numAntiChiralE`, `FTheory.SU5.TenQuanta.reduce_numAntiChiralE_of_mem_elemsNoExotics`
`numAntiChiralQ` 📖	CompOp	2 math math: `numChiralQ_eq_sum_sub_numAntiChiralQ`, `FTheory.SU5.TenQuanta.reduce_numAntiChiralQ_of_mem_elemsNoExotics`
`numAntiChiralU` 📖	CompOp	2 math math: `numChiralU_eq_sum_sub_numAntiChiralU`, `FTheory.SU5.TenQuanta.reduce_numAntiChiralU_of_mem_elemsNoExotics`
`numChiralE` 📖	CompOp	2 math math: `numChiralE_eq_sum_sub_numAntiChiralE`, `FTheory.SU5.TenQuanta.reduce_numChiralE_of_mem_elemsNoExotics`
`numChiralQ` 📖	CompOp	2 math math: `numChiralQ_eq_sum_sub_numAntiChiralQ`, `FTheory.SU5.TenQuanta.reduce_numChiralQ_of_mem_elemsNoExotics`
`numChiralU` 📖	CompOp	2 math math: `numChiralU_eq_sum_sub_numAntiChiralU`, `FTheory.SU5.TenQuanta.reduce_numChiralU_of_mem_elemsNoExotics`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`numChiralE_eq_sum_sub_numAntiChiralE` 📖	mathematical	—	`numChiralE` `chiralIndicesOfE` `numAntiChiralE`	—	—
`numChiralQ_eq_sum_sub_numAntiChiralQ` 📖	mathematical	—	`numChiralQ` `chiralIndicesOfQ` `numAntiChiralQ`	—	—
`numChiralU_eq_sum_sub_numAntiChiralU` 📖	mathematical	—	`numChiralU` `chiralIndicesOfU` `numAntiChiralU`	—	—

FTheory.SU5.instDecidableEqFluxes

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index