FiveQuanta

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

Statistics

Metric	Count
Definitions `FiveQuanta`, `anomalyCoefficient`, `decompose`, `decomposeFluxes`, `liftCharge`, `reduce`, `toChargeMap`, `toCharges`, `toFluxesFive`	9
Theorems `anomalyCoefficient_of_map`, `anomalyCoefficient_of_reduce`, `decomposeFluxes_sum_of_noExotics`, `decompose_add`, `decompose_filter_charge`, `decompose_reduce`, `decompose_toChargeMap`, `decompose_toCharges_dedup`, `decompose_toFluxesFive`, `exists_toCharges_toFluxesFive_of_mem_liftCharge`, `hasNoZero_of_mem_liftCharge`, `map_liftCharge`, `mem_liftCharge_iff`, `mem_liftCharge_iff_exists`, `mem_liftCharge_of_exists_toCharges_toFluxesFive`, `mem_liftCharge_of_mem_noExotics_hasNoZero`, `mem_powerset_sum_of_mem_reduce_toFluxesFive`, `mem_powerset_sum_of_mem_reduce_toFluxesFive_filter`, `mem_reduce_iff`, `noExotics_of_mem_liftCharge`, `reduce_dedup`, `reduce_eq_self_of_ofCharges_nodup`, `reduce_filter`, `reduce_mem_elemsNoExotics`, `reduce_noExotics_of_mem_elemsNoExotics`, `reduce_nodup`, `reduce_numAntiChiralD_of_mem_elemsNoExotics`, `reduce_numAntiChiralL_of_mem_elemsNoExotics`, `reduce_numChiralD_of_mem_elemsNoExotics`, `reduce_numChiralL_of_mem_elemsNoExotics`, `reduce_reduce`, `reduce_sum_eq_sum_toCharges`, `reduce_toChargeMap_eq`, `reduce_toCharges`, `toChargeMap_of_not_mem`, `toCharges_nodup_of_mem_liftCharge`, `toCharges_toFinset_of_mem_liftCharge`	37
Total	46

FTheory.SU5

Definitions

Name	Category	Theorems
`FiveQuanta` 📖	CompOp	8 math math: `Quanta.mem_liftCharge_iff`, `FiveQuanta.mem_liftCharge_iff_exists`, `FiveQuanta.mem_reduce_iff`, `FiveQuanta.mem_liftCharge_of_mem_noExotics_hasNoZero`, `FiveQuanta.decompose_add`, `Quanta.quarticAnomalyCancellation_iff_mem_of_isViable`, `FiveQuanta.mem_liftCharge_of_exists_toCharges_toFluxesFive`, `FiveQuanta.mem_liftCharge_iff`

FTheory.SU5.FiveQuanta

Definitions

Name	Category	Theorems
`anomalyCoefficient` 📖	CompOp	2 math math: `anomalyCoefficient_of_map`, `anomalyCoefficient_of_reduce`
`decompose` 📖	CompOp	6 math math: `decompose_reduce`, `decompose_toChargeMap`, `decompose_filter_charge`, `decompose_add`, `decompose_toFluxesFive`, `decompose_toCharges_dedup`
`decomposeFluxes` 📖	CompOp	1 math math: `decomposeFluxes_sum_of_noExotics`
`liftCharge` 📖	CompOp	5 math math: `FTheory.SU5.Quanta.mem_liftCharge_iff`, `mem_liftCharge_iff_exists`, `mem_liftCharge_of_mem_noExotics_hasNoZero`, `mem_liftCharge_of_exists_toCharges_toFluxesFive`, `mem_liftCharge_iff`
`reduce` 📖	CompOp	20 math math: `map_liftCharge`, `reduce_numChiralL_of_mem_elemsNoExotics`, `mem_liftCharge_iff_exists`, `reduce_nodup`, `mem_reduce_iff`, `reduce_numAntiChiralL_of_mem_elemsNoExotics`, `decompose_reduce`, `reduce_noExotics_of_mem_elemsNoExotics`, `reduce_filter`, `reduce_sum_eq_sum_toCharges`, `reduce_reduce`, `reduce_toCharges`, `exists_toCharges_toFluxesFive_of_mem_liftCharge`, `anomalyCoefficient_of_reduce`, `reduce_dedup`, `reduce_toChargeMap_eq`, `reduce_numChiralD_of_mem_elemsNoExotics`, `reduce_numAntiChiralD_of_mem_elemsNoExotics`, `reduce_eq_self_of_ofCharges_nodup`, `reduce_mem_elemsNoExotics`
`toChargeMap` 📖	CompOp	3 math math: `decompose_toChargeMap`, `toChargeMap_of_not_mem`, `reduce_toChargeMap_eq`
`toCharges` 📖	CompOp	11 math math: `mem_liftCharge_iff_exists`, `mem_reduce_iff`, `toCharges_nodup_of_mem_liftCharge`, `FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges`, `FTheory.SU5.Quanta.IsViable.no_duplicate_five_bar_charges`, `reduce_toCharges`, `toCharges_toFinset_of_mem_liftCharge`, `exists_toCharges_toFluxesFive_of_mem_liftCharge`, `decompose_toCharges_dedup`, `FTheory.SU5.Quanta.isViable_iff_def`, `mem_liftCharge_iff`
`toFluxesFive` 📖	CompOp	9 math math: `mem_liftCharge_iff_exists`, `FTheory.SU5.Quanta.IsViable.no_five_bar_zero_fluxes`, `hasNoZero_of_mem_liftCharge`, `noExotics_of_mem_liftCharge`, `FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges`, `FTheory.SU5.Quanta.IsViable.no_exotics_from_five_bar`, `exists_toCharges_toFluxesFive_of_mem_liftCharge`, `FTheory.SU5.Quanta.isViable_iff_def`, `mem_liftCharge_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anomalyCoefficient_of_map` 📖	mathematical	—	`anomalyCoefficient` `FTheory.SU5.Fluxes`	—	—
`anomalyCoefficient_of_reduce` 📖	mathematical	—	`anomalyCoefficient` `reduce`	—	`reduce_sum_eq_sum_toCharges`
`decomposeFluxes_sum_of_noExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `FTheory.SU5.FluxesFive.elemsNoExotics` `FTheory.SU5.Fluxes`	`FTheory.SU5.Fluxes.instAddCommMonoid` `decomposeFluxes`	—	—
`decompose_add` 📖	mathematical	—	`decompose` `FTheory.SU5.FiveQuanta` `FTheory.SU5.Fluxes`	—	—
`decompose_filter_charge` 📖	mathematical	—	`FTheory.SU5.Fluxes` `decompose`	—	`decompose.eq_1` `decompose_add`
`decompose_reduce` 📖	mathematical	`FTheory.SU5.FluxesFive` `FTheory.SU5.FluxesFive.elemsNoExotics` `toFluxesFive`	`reduce` `decompose`	—	`reduce.eq_1` `decompose_toCharges_dedup` `decompose_toChargeMap`
`decompose_toChargeMap` 📖	mathematical	`FTheory.SU5.FluxesFive` `FTheory.SU5.FluxesFive.elemsNoExotics` `toFluxesFive`	`toChargeMap` `decompose`	—	`toChargeMap.eq_1` `decompose_filter_charge` `decomposeFluxes_sum_of_noExotics`
`decompose_toCharges_dedup` 📖	mathematical	`FTheory.SU5.FluxesFive` `FTheory.SU5.FluxesFive.elemsNoExotics` `toFluxesFive`	`toCharges` `decompose`	—	—
`decompose_toFluxesFive` 📖	mathematical	`FTheory.SU5.FluxesFive` `FTheory.SU5.FluxesFive.elemsNoExotics` `toFluxesFive`	`decompose` `FTheory.SU5.Fluxes`	—	`toFluxesFive.eq_1` `decompose.eq_1`
`exists_toCharges_toFluxesFive_of_mem_liftCharge` 📖	mathematical	`FTheory.SU5.FiveQuanta` `liftCharge`	`reduce` `toCharges` `toFluxesFive` `FTheory.SU5.Fluxes` `FTheory.SU5.FluxesFive`	—	`liftCharge.eq_1` `reduce_toCharges` `toCharges_toFinset_of_mem_liftCharge`
`hasNoZero_of_mem_liftCharge` 📖	mathematical	`FTheory.SU5.FiveQuanta` `liftCharge`	`FTheory.SU5.FluxesFive.HasNoZero` `toFluxesFive`	—	`mem_liftCharge_iff_exists` `mem_powerset_sum_of_mem_reduce_toFluxesFive_filter`
`map_liftCharge` 📖	mathematical	`FTheory.SU5.FiveQuanta` `liftCharge`	`reduce` `FTheory.SU5.Fluxes`	—	`mem_liftCharge_iff` `reduce_mem_elemsNoExotics` `reduce_toCharges`
`mem_liftCharge_iff` 📖	mathematical	—	`FTheory.SU5.FiveQuanta` `liftCharge` `FTheory.SU5.FluxesFive` `FTheory.SU5.FluxesFive.elemsNoExotics` `toFluxesFive` `toCharges`	—	`FTheory.SU5.FluxesFive.noExotics_iff_mem_elemsNoExotics` `noExotics_of_mem_liftCharge` `hasNoZero_of_mem_liftCharge` `toCharges_toFinset_of_mem_liftCharge` `toCharges_nodup_of_mem_liftCharge` `mem_liftCharge_of_mem_noExotics_hasNoZero`
`mem_liftCharge_iff_exists` 📖	mathematical	—	`FTheory.SU5.FiveQuanta` `liftCharge` `reduce` `toCharges` `toFluxesFive` `FTheory.SU5.Fluxes` `FTheory.SU5.FluxesFive`	—	`exists_toCharges_toFluxesFive_of_mem_liftCharge` `mem_liftCharge_of_exists_toCharges_toFluxesFive`
`mem_liftCharge_of_exists_toCharges_toFluxesFive` 📖	mathematical	`reduce` `toCharges` `toFluxesFive` `FTheory.SU5.Fluxes` `FTheory.SU5.FluxesFive`	`FTheory.SU5.FiveQuanta` `liftCharge`	—	`liftCharge.eq_1` `toFluxesFive.eq_1`
`mem_liftCharge_of_mem_noExotics_hasNoZero` 📖	mathematical	`FTheory.SU5.FluxesFive.NoExotics` `toFluxesFive` `FTheory.SU5.FluxesFive.HasNoZero` `toCharges`	`FTheory.SU5.FiveQuanta` `liftCharge`	—	`FTheory.SU5.FluxesFive.noExotics_iff_mem_elemsNoExotics` `mem_liftCharge_iff_exists` `decompose_reduce` `reduce_eq_self_of_ofCharges_nodup` `decompose_toCharges_dedup` `decompose_toFluxesFive`
`mem_powerset_sum_of_mem_reduce_toFluxesFive` 📖	mathematical	`FTheory.SU5.Fluxes` `FTheory.SU5.FluxesFive` `toFluxesFive` `reduce`	`FTheory.SU5.Fluxes.instAddCommMonoid`	—	`toFluxesFive.eq_1` `mem_reduce_iff`
`mem_powerset_sum_of_mem_reduce_toFluxesFive_filter` 📖	mathematical	`FTheory.SU5.Fluxes` `FTheory.SU5.FluxesFive` `toFluxesFive` `reduce`	`FTheory.SU5.Fluxes.instAddCommMonoid` `FTheory.SU5.FluxesTen.instDecidableEq`	—	`toFluxesFive.eq_1` `mem_reduce_iff` `toCharges.eq_1`
`mem_reduce_iff` 📖	mathematical	—	`FTheory.SU5.Fluxes` `FTheory.SU5.FiveQuanta` `reduce` `toCharges` `FTheory.SU5.Fluxes.instAddCommMonoid`	—	—
`noExotics_of_mem_liftCharge` 📖	mathematical	`FTheory.SU5.FiveQuanta` `liftCharge`	`FTheory.SU5.FluxesFive.NoExotics` `toFluxesFive`	—	`mem_liftCharge_iff_exists` `reduce_noExotics_of_mem_elemsNoExotics`
`reduce_dedup` 📖	mathematical	—	`FTheory.SU5.Fluxes` `FTheory.SU5.instDecidableEqFluxes` `reduce`	—	`reduce_nodup`
`reduce_eq_self_of_ofCharges_nodup` 📖	mathematical	`toCharges`	`reduce`	—	`reduce.eq_1`
`reduce_filter` 📖	mathematical	`toCharges`	`FTheory.SU5.Fluxes` `reduce` `FTheory.SU5.Fluxes.instAddCommMonoid`	—	—
`reduce_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `FTheory.SU5.FluxesFive.elemsNoExotics` `toFluxesFive`	`reduce`	—	`FTheory.SU5.FluxesFive.noExotics_iff_mem_elemsNoExotics` `reduce_noExotics_of_mem_elemsNoExotics` `mem_powerset_sum_of_mem_reduce_toFluxesFive_filter`
`reduce_noExotics_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `FTheory.SU5.FluxesFive.elemsNoExotics` `toFluxesFive`	`FTheory.SU5.FluxesFive.NoExotics` `reduce`	—	`FTheory.SU5.FluxesFive.NoExotics.eq_1` `reduce_numChiralL_of_mem_elemsNoExotics` `reduce_numAntiChiralL_of_mem_elemsNoExotics` `reduce_numChiralD_of_mem_elemsNoExotics` `reduce_numAntiChiralD_of_mem_elemsNoExotics`
`reduce_nodup` 📖	mathematical	—	`FTheory.SU5.Fluxes` `reduce`	—	—
`reduce_numAntiChiralD_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `FTheory.SU5.FluxesFive.elemsNoExotics` `toFluxesFive`	`FTheory.SU5.FluxesFive.numAntiChiralD` `reduce`	—	`FTheory.SU5.FluxesFive.numAntiChiralD.eq_1` `FTheory.SU5.FluxesFive.chiralIndicesOfD.eq_1` `mem_powerset_sum_of_mem_reduce_toFluxesFive`
`reduce_numAntiChiralL_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `FTheory.SU5.FluxesFive.elemsNoExotics` `toFluxesFive`	`FTheory.SU5.FluxesFive.numAntiChiralL` `reduce`	—	`FTheory.SU5.FluxesFive.numAntiChiralL.eq_1` `FTheory.SU5.FluxesFive.chiralIndicesOfL.eq_1` `mem_powerset_sum_of_mem_reduce_toFluxesFive`
`reduce_numChiralD_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `FTheory.SU5.FluxesFive.elemsNoExotics` `toFluxesFive`	`FTheory.SU5.FluxesFive.numChiralD` `reduce`	—	`FTheory.SU5.FluxesFive.noExotics_iff_mem_elemsNoExotics` `FTheory.SU5.FluxesFive.numChiralD.eq_1` `FTheory.SU5.FluxesFive.chiralIndicesOfD.eq_1` `mem_powerset_sum_of_mem_reduce_toFluxesFive` `toFluxesFive.eq_1` `reduce_sum_eq_sum_toCharges`
`reduce_numChiralL_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `FTheory.SU5.FluxesFive.elemsNoExotics` `toFluxesFive`	`FTheory.SU5.FluxesFive.numChiralL` `reduce`	—	`FTheory.SU5.FluxesFive.noExotics_iff_mem_elemsNoExotics` `FTheory.SU5.FluxesFive.numChiralL.eq_1` `FTheory.SU5.FluxesFive.chiralIndicesOfL.eq_1` `mem_powerset_sum_of_mem_reduce_toFluxesFive` `toFluxesFive.eq_1` `reduce_sum_eq_sum_toCharges`
`reduce_reduce` 📖	mathematical	—	`reduce`	—	`reduce_nodup` `mem_reduce_iff` `reduce_toCharges` `reduce_filter`
`reduce_sum_eq_sum_toCharges` 📖	mathematical	—	`FTheory.SU5.Fluxes` `FTheory.SU5.Fluxes.instAddCommMonoid` `reduce`	—	`reduce.eq_1`
`reduce_toChargeMap_eq` 📖	mathematical	—	`toChargeMap` `reduce`	—	`toChargeMap.eq_1` `reduce_filter` `toChargeMap_of_not_mem` `reduce_toCharges`
`reduce_toCharges` 📖	mathematical	—	`toCharges` `reduce`	—	—
`toChargeMap_of_not_mem` 📖	mathematical	`toCharges`	`toChargeMap` `FTheory.SU5.Fluxes` `FTheory.SU5.Fluxes.instZero`	—	—
`toCharges_nodup_of_mem_liftCharge` 📖	mathematical	`FTheory.SU5.FiveQuanta` `liftCharge`	`toCharges`	—	`liftCharge.eq_1` `reduce_toCharges`
`toCharges_toFinset_of_mem_liftCharge` 📖	mathematical	`FTheory.SU5.FiveQuanta` `liftCharge`	`toCharges`	—	`reduce_toCharges`

---

← Back to Index