TenQuanta

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

Statistics

Metric	Count
Definitions `TenQuanta`, `anomalyCoefficient`, `decompose`, `decomposeFluxes`, `liftCharge`, `reduce`, `toChargeMap`, `toCharges`, `toFluxesTen`	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_toFluxesTen`, `exists_toCharges_toFluxesTen_of_mem_liftCharge`, `hasNoZero_of_mem_liftCharge`, `map_liftCharge`, `mem_liftCharge_iff`, `mem_liftCharge_iff_exists`, `mem_liftCharge_of_exists_toCharges_toFluxesTen`, `mem_liftCharge_of_mem_noExotics_hasNoZero`, `mem_powerset_sum_of_mem_reduce_toFluxesTen`, `mem_powerset_sum_of_mem_reduce_toFluxesTen_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_numAntiChiralE_of_mem_elemsNoExotics`, `reduce_numAntiChiralQ_of_mem_elemsNoExotics`, `reduce_numAntiChiralU_of_mem_elemsNoExotics`, `reduce_numChiralE_of_mem_elemsNoExotics`, `reduce_numChiralQ_of_mem_elemsNoExotics`, `reduce_numChiralU_of_mem_elemsNoExotics`, `reduce_reduce`, `reduce_sum_eq_sum_toCharges`, `reduce_toChargeMap_eq`, `reduce_toCharges`, `toChargeMap_of_not_mem`, `toCharge_toFinset_of_mem_liftCharge`, `toCharges_nodup_of_mem_liftCharge`	39
Total	48

FTheory.SU5

Definitions

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

FTheory.SU5.TenQuanta

Definitions

Name	Category	Theorems
`anomalyCoefficient` 📖	CompOp	2 math math: `anomalyCoefficient_of_map`, `anomalyCoefficient_of_reduce`
`decompose` 📖	CompOp	6 math math: `decompose_toFluxesTen`, `decompose_filter_charge`, `decompose_reduce`, `decompose_toChargeMap`, `decompose_toCharges_dedup`, `decompose_add`
`decomposeFluxes` 📖	CompOp	1 math math: `decomposeFluxes_sum_of_noExotics`
`liftCharge` 📖	CompOp	5 math math: `FTheory.SU5.Quanta.mem_liftCharge_iff`, `mem_liftCharge_of_exists_toCharges_toFluxesTen`, `mem_liftCharge_iff`, `mem_liftCharge_of_mem_noExotics_hasNoZero`, `mem_liftCharge_iff_exists`
`reduce` 📖	CompOp	22 math math: `exists_toCharges_toFluxesTen_of_mem_liftCharge`, `map_liftCharge`, `reduce_reduce`, `reduce_toCharges`, `reduce_filter`, `mem_reduce_iff`, `decompose_reduce`, `reduce_numChiralQ_of_mem_elemsNoExotics`, `reduce_eq_self_of_ofCharges_nodup`, `reduce_sum_eq_sum_toCharges`, `reduce_numChiralE_of_mem_elemsNoExotics`, `reduce_toChargeMap_eq`, `reduce_numAntiChiralU_of_mem_elemsNoExotics`, `reduce_noExotics_of_mem_elemsNoExotics`, `reduce_numAntiChiralQ_of_mem_elemsNoExotics`, `anomalyCoefficient_of_reduce`, `reduce_nodup`, `reduce_numChiralU_of_mem_elemsNoExotics`, `reduce_mem_elemsNoExotics`, `mem_liftCharge_iff_exists`, `reduce_numAntiChiralE_of_mem_elemsNoExotics`, `reduce_dedup`
`toChargeMap` 📖	CompOp	3 math math: `toChargeMap_of_not_mem`, `decompose_toChargeMap`, `reduce_toChargeMap_eq`
`toCharges` 📖	CompOp	11 math math: `exists_toCharges_toFluxesTen_of_mem_liftCharge`, `reduce_toCharges`, `mem_reduce_iff`, `decompose_toCharges_dedup`, `toCharges_nodup_of_mem_liftCharge`, `mem_liftCharge_iff`, `FTheory.SU5.Quanta.IsViable.no_duplicate_ten_charges`, `FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges`, `toCharge_toFinset_of_mem_liftCharge`, `FTheory.SU5.Quanta.isViable_iff_def`, `mem_liftCharge_iff_exists`
`toFluxesTen` 📖	CompOp	9 math math: `exists_toCharges_toFluxesTen_of_mem_liftCharge`, `hasNoZero_of_mem_liftCharge`, `FTheory.SU5.Quanta.IsViable.no_exotics_from_ten`, `FTheory.SU5.Quanta.IsViable.no_ten_zero_fluxes`, `mem_liftCharge_iff`, `FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges`, `FTheory.SU5.Quanta.isViable_iff_def`, `noExotics_of_mem_liftCharge`, `mem_liftCharge_iff_exists`

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.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `FTheory.SU5.Fluxes`	`FTheory.SU5.Fluxes.instAddCommMonoid` `decomposeFluxes`	—	—
`decompose_add` 📖	mathematical	—	`decompose` `FTheory.SU5.TenQuanta` `FTheory.SU5.Fluxes`	—	—
`decompose_filter_charge` 📖	mathematical	—	`FTheory.SU5.Fluxes` `decompose`	—	`decompose.eq_1` `decompose_add`
`decompose_reduce` 📖	mathematical	`FTheory.SU5.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen`	`reduce` `decompose`	—	`reduce.eq_1` `decompose_toCharges_dedup` `decompose_toChargeMap`
`decompose_toChargeMap` 📖	mathematical	`FTheory.SU5.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen`	`toChargeMap` `decompose`	—	`toChargeMap.eq_1` `decompose_filter_charge` `decomposeFluxes_sum_of_noExotics`
`decompose_toCharges_dedup` 📖	mathematical	`FTheory.SU5.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen`	`toCharges` `decompose`	—	—
`decompose_toFluxesTen` 📖	mathematical	`FTheory.SU5.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen`	`decompose` `FTheory.SU5.Fluxes`	—	`toFluxesTen.eq_1` `decompose.eq_1`
`exists_toCharges_toFluxesTen_of_mem_liftCharge` 📖	mathematical	`FTheory.SU5.TenQuanta` `liftCharge`	`reduce` `toCharges` `toFluxesTen` `FTheory.SU5.Fluxes` `FTheory.SU5.FluxesTen`	—	`liftCharge.eq_1` `toCharge_toFinset_of_mem_liftCharge` `reduce_toCharges`
`hasNoZero_of_mem_liftCharge` 📖	mathematical	`FTheory.SU5.TenQuanta` `liftCharge`	`FTheory.SU5.FluxesTen.HasNoZero` `toFluxesTen`	—	`mem_liftCharge_iff_exists` `mem_powerset_sum_of_mem_reduce_toFluxesTen_filter`
`map_liftCharge` 📖	mathematical	`FTheory.SU5.TenQuanta` `liftCharge`	`reduce` `FTheory.SU5.Fluxes`	—	`mem_liftCharge_iff` `reduce_mem_elemsNoExotics` `reduce_toCharges`
`mem_liftCharge_iff` 📖	mathematical	—	`FTheory.SU5.TenQuanta` `liftCharge` `FTheory.SU5.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen` `toCharges`	—	`FTheory.SU5.FluxesTen.noExotics_iff_mem_elemsNoExotics` `noExotics_of_mem_liftCharge` `hasNoZero_of_mem_liftCharge` `toCharge_toFinset_of_mem_liftCharge` `toCharges_nodup_of_mem_liftCharge` `mem_liftCharge_of_mem_noExotics_hasNoZero`
`mem_liftCharge_iff_exists` 📖	mathematical	—	`FTheory.SU5.TenQuanta` `liftCharge` `reduce` `toCharges` `toFluxesTen` `FTheory.SU5.Fluxes` `FTheory.SU5.FluxesTen`	—	`exists_toCharges_toFluxesTen_of_mem_liftCharge` `mem_liftCharge_of_exists_toCharges_toFluxesTen`
`mem_liftCharge_of_exists_toCharges_toFluxesTen` 📖	mathematical	`reduce` `toCharges` `toFluxesTen` `FTheory.SU5.Fluxes` `FTheory.SU5.FluxesTen`	`FTheory.SU5.TenQuanta` `liftCharge`	—	`liftCharge.eq_1` `toCharges.eq_1`
`mem_liftCharge_of_mem_noExotics_hasNoZero` 📖	mathematical	`FTheory.SU5.FluxesTen.NoExotics` `toFluxesTen` `FTheory.SU5.FluxesTen.HasNoZero` `toCharges`	`FTheory.SU5.TenQuanta` `liftCharge`	—	`FTheory.SU5.FluxesTen.noExotics_iff_mem_elemsNoExotics` `mem_liftCharge_iff_exists` `decompose_reduce` `reduce_eq_self_of_ofCharges_nodup` `decompose_toCharges_dedup` `decompose_toFluxesTen`
`mem_powerset_sum_of_mem_reduce_toFluxesTen` 📖	mathematical	`FTheory.SU5.Fluxes` `FTheory.SU5.FluxesTen` `toFluxesTen` `reduce`	`FTheory.SU5.Fluxes.instAddCommMonoid`	—	`toFluxesTen.eq_1` `mem_reduce_iff`
`mem_powerset_sum_of_mem_reduce_toFluxesTen_filter` 📖	mathematical	`FTheory.SU5.Fluxes` `FTheory.SU5.FluxesTen` `toFluxesTen` `reduce`	`FTheory.SU5.Fluxes.instAddCommMonoid` `FTheory.SU5.FluxesTen.instDecidableEq`	—	`toFluxesTen.eq_1` `mem_reduce_iff`
`mem_reduce_iff` 📖	mathematical	—	`FTheory.SU5.Fluxes` `FTheory.SU5.TenQuanta` `reduce` `toCharges` `FTheory.SU5.Fluxes.instAddCommMonoid`	—	—
`noExotics_of_mem_liftCharge` 📖	mathematical	`FTheory.SU5.TenQuanta` `liftCharge`	`FTheory.SU5.FluxesTen.NoExotics` `toFluxesTen`	—	`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.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen`	`reduce`	—	`FTheory.SU5.FluxesTen.noExotics_iff_mem_elemsNoExotics` `reduce_noExotics_of_mem_elemsNoExotics` `mem_powerset_sum_of_mem_reduce_toFluxesTen_filter`
`reduce_noExotics_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen`	`FTheory.SU5.FluxesTen.NoExotics` `reduce`	—	`FTheory.SU5.FluxesTen.NoExotics.eq_1` `reduce_numChiralU_of_mem_elemsNoExotics` `reduce_numAntiChiralU_of_mem_elemsNoExotics` `reduce_numChiralQ_of_mem_elemsNoExotics` `reduce_numAntiChiralQ_of_mem_elemsNoExotics` `reduce_numChiralE_of_mem_elemsNoExotics` `reduce_numAntiChiralE_of_mem_elemsNoExotics`
`reduce_nodup` 📖	mathematical	—	`FTheory.SU5.Fluxes` `reduce`	—	—
`reduce_numAntiChiralE_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen`	`FTheory.SU5.FluxesTen.numAntiChiralE` `reduce`	—	`FTheory.SU5.FluxesTen.numAntiChiralE.eq_1` `FTheory.SU5.FluxesTen.chiralIndicesOfE.eq_1` `mem_powerset_sum_of_mem_reduce_toFluxesTen`
`reduce_numAntiChiralQ_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen`	`FTheory.SU5.FluxesTen.numAntiChiralQ` `reduce`	—	`FTheory.SU5.FluxesTen.numAntiChiralQ.eq_1` `FTheory.SU5.FluxesTen.chiralIndicesOfQ.eq_1` `mem_powerset_sum_of_mem_reduce_toFluxesTen`
`reduce_numAntiChiralU_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen`	`FTheory.SU5.FluxesTen.numAntiChiralU` `reduce`	—	`FTheory.SU5.FluxesTen.numAntiChiralU.eq_1` `FTheory.SU5.FluxesTen.chiralIndicesOfU.eq_1` `mem_powerset_sum_of_mem_reduce_toFluxesTen`
`reduce_numChiralE_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen`	`FTheory.SU5.FluxesTen.numChiralE` `reduce`	—	`FTheory.SU5.FluxesTen.noExotics_iff_mem_elemsNoExotics` `FTheory.SU5.FluxesTen.numChiralE.eq_1` `FTheory.SU5.FluxesTen.chiralIndicesOfE.eq_1` `mem_powerset_sum_of_mem_reduce_toFluxesTen` `toFluxesTen.eq_1` `reduce_sum_eq_sum_toCharges`
`reduce_numChiralQ_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen`	`FTheory.SU5.FluxesTen.numChiralQ` `reduce`	—	`FTheory.SU5.FluxesTen.noExotics_iff_mem_elemsNoExotics` `FTheory.SU5.FluxesTen.numChiralQ.eq_1` `FTheory.SU5.FluxesTen.chiralIndicesOfQ.eq_1` `mem_powerset_sum_of_mem_reduce_toFluxesTen` `toFluxesTen.eq_1` `reduce_sum_eq_sum_toCharges`
`reduce_numChiralU_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesTen` `FTheory.SU5.FluxesTen.elemsNoExotics` `toFluxesTen`	`FTheory.SU5.FluxesTen.numChiralU` `reduce`	—	`FTheory.SU5.FluxesTen.noExotics_iff_mem_elemsNoExotics` `FTheory.SU5.FluxesTen.numChiralU.eq_1` `FTheory.SU5.FluxesTen.chiralIndicesOfU.eq_1` `mem_powerset_sum_of_mem_reduce_toFluxesTen` `toFluxesTen.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`	—	—
`toCharge_toFinset_of_mem_liftCharge` 📖	mathematical	`FTheory.SU5.TenQuanta` `liftCharge`	`toCharges`	—	`liftCharge.eq_1` `reduce_toCharges`
`toCharges_nodup_of_mem_liftCharge` 📖	mathematical	`FTheory.SU5.TenQuanta` `liftCharge`	`toCharges`	—	`liftCharge.eq_1` `reduce_toCharges`

---

← Back to Index