Documentation Verification Report

ChiralIndices

📁 Source: PhysLean/StringTheory/FTheory/SU5/Fluxes/NoExotics/ChiralIndices.lean

Statistics

Metric	Count
Definitions	0
Theorems `chiralIndicesOfD_le_three_of_noExotics`, `chiralIndicesOfD_noneg_of_noExotics`, `chiralIndicesOfD_subset_sum_le_three_of_noExotics`, `chiralIndicesOfD_sum_eq_three_of_noExotics`, `chiralIndicesOfL_le_three_of_noExotics`, `chiralIndicesOfL_noneg_of_noExotics`, `chiralIndicesOfL_subset_sum_le_three_of_noExotics`, `chiralIndicesOfL_sum_eq_three_of_noExotics`, `mem_chiralIndicesOfD_mem_of_noExotics`, `mem_chiralIndicesOfL_mem_of_noExotics`, `chiralIndicesOfE_le_three_of_noExotics`, `chiralIndicesOfE_noneg_of_noExotics`, `chiralIndicesOfE_subset_sum_le_three_of_noExotics`, `chiralIndicesOfE_sum_eq_three_of_noExotics`, `chiralIndicesOfQ_le_three_of_noExotics`, `chiralIndicesOfQ_noneg_of_noExotics`, `chiralIndicesOfQ_subset_sum_le_three_of_noExotics`, `chiralIndicesOfQ_sum_eq_three_of_noExotics`, `chiralIndicesOfU_le_three_of_noExotics`, `chiralIndicesOfU_noneg_of_noExotics`, `chiralIndicesOfU_subset_sum_le_three_of_noExotics`, `chiralIndicesOfU_sum_eq_three_of_noExotics`, `mem_chiralIndicesOfE_mem_of_noExotics`, `mem_chiralIndicesOfQ_mem_of_noExotics`, `mem_chiralIndicesOfU_mem_of_noExotics`	25
Total	25

FTheory.SU5.FluxesFive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chiralIndicesOfD_le_three_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfD`	—	—	`chiralIndicesOfD_noneg_of_noExotics` `chiralIndicesOfD_sum_eq_three_of_noExotics`
`chiralIndicesOfD_noneg_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfD`	—	—	—
`chiralIndicesOfD_subset_sum_le_three_of_noExotics` 📖	mathematical	`NoExotics` `FTheory.SU5.Fluxes`	`FTheory.SU5.Fluxes.M`	—	`chiralIndicesOfD_noneg_of_noExotics` `chiralIndicesOfD_sum_eq_three_of_noExotics` `chiralIndicesOfD.eq_1`
`chiralIndicesOfD_sum_eq_three_of_noExotics` 📖	mathematical	`NoExotics`	`chiralIndicesOfD`	—	—
`chiralIndicesOfL_le_three_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfL`	—	—	`chiralIndicesOfL_noneg_of_noExotics` `chiralIndicesOfL_sum_eq_three_of_noExotics`
`chiralIndicesOfL_noneg_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfL`	—	—	—
`chiralIndicesOfL_subset_sum_le_three_of_noExotics` 📖	mathematical	`NoExotics` `FTheory.SU5.Fluxes`	`FTheory.SU5.Fluxes.M` `FTheory.SU5.Fluxes.N`	—	`chiralIndicesOfL_noneg_of_noExotics` `chiralIndicesOfL_sum_eq_three_of_noExotics` `chiralIndicesOfL.eq_1`
`chiralIndicesOfL_sum_eq_three_of_noExotics` 📖	mathematical	`NoExotics`	`chiralIndicesOfL`	—	—
`mem_chiralIndicesOfD_mem_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfD`	—	—	`chiralIndicesOfD_le_three_of_noExotics` `chiralIndicesOfD_noneg_of_noExotics`
`mem_chiralIndicesOfL_mem_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfL`	—	—	`chiralIndicesOfL_le_three_of_noExotics` `chiralIndicesOfL_noneg_of_noExotics`

FTheory.SU5.FluxesTen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chiralIndicesOfE_le_three_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfE`	—	—	`chiralIndicesOfE_noneg_of_noExotics` `chiralIndicesOfE_sum_eq_three_of_noExotics`
`chiralIndicesOfE_noneg_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfE`	—	—	—
`chiralIndicesOfE_subset_sum_le_three_of_noExotics` 📖	mathematical	`NoExotics` `FTheory.SU5.Fluxes`	`FTheory.SU5.Fluxes.M` `FTheory.SU5.Fluxes.N`	—	`chiralIndicesOfE_noneg_of_noExotics` `chiralIndicesOfE_sum_eq_three_of_noExotics` `chiralIndicesOfE.eq_1`
`chiralIndicesOfE_sum_eq_three_of_noExotics` 📖	mathematical	`NoExotics`	`chiralIndicesOfE`	—	—
`chiralIndicesOfQ_le_three_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfQ`	—	—	`chiralIndicesOfQ_noneg_of_noExotics` `chiralIndicesOfQ_sum_eq_three_of_noExotics`
`chiralIndicesOfQ_noneg_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfQ`	—	—	—
`chiralIndicesOfQ_subset_sum_le_three_of_noExotics` 📖	mathematical	`NoExotics` `FTheory.SU5.Fluxes`	`FTheory.SU5.Fluxes.M`	—	`chiralIndicesOfQ_noneg_of_noExotics` `chiralIndicesOfQ_sum_eq_three_of_noExotics` `chiralIndicesOfQ.eq_1`
`chiralIndicesOfQ_sum_eq_three_of_noExotics` 📖	mathematical	`NoExotics`	`chiralIndicesOfQ`	—	—
`chiralIndicesOfU_le_three_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfU`	—	—	`chiralIndicesOfU_noneg_of_noExotics` `chiralIndicesOfU_sum_eq_three_of_noExotics`
`chiralIndicesOfU_noneg_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfU`	—	—	—
`chiralIndicesOfU_subset_sum_le_three_of_noExotics` 📖	mathematical	`NoExotics` `FTheory.SU5.Fluxes`	`FTheory.SU5.Fluxes.M` `FTheory.SU5.Fluxes.N`	—	`chiralIndicesOfU_noneg_of_noExotics` `chiralIndicesOfU_sum_eq_three_of_noExotics` `chiralIndicesOfU.eq_1`
`chiralIndicesOfU_sum_eq_three_of_noExotics` 📖	mathematical	`NoExotics`	`chiralIndicesOfU`	—	—
`mem_chiralIndicesOfE_mem_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfE`	—	—	`chiralIndicesOfE_le_three_of_noExotics` `chiralIndicesOfE_noneg_of_noExotics`
`mem_chiralIndicesOfQ_mem_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfQ`	—	—	`chiralIndicesOfQ_le_three_of_noExotics` `chiralIndicesOfQ_noneg_of_noExotics`
`mem_chiralIndicesOfU_mem_of_noExotics` 📖	—	`NoExotics` `chiralIndicesOfU`	—	—	`chiralIndicesOfU_le_three_of_noExotics` `chiralIndicesOfU_noneg_of_noExotics`

---

← Back to Index