Documentation Verification Report

Completeness

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

Statistics

Metric	Count
Definitions `noExoticsSubsets`, `noExoticsSubsets`	2
Theorems `card_le_six_of_noExotics`, `card_mem_range_seven_of_noExotics`, `mem_elemsNoExotics_of_noExotics`, `mem_mem_finset_of_noExotics`, `noExotics_iff_mem_elemsNoExotics`, `subset_le_mem_of_card_eq_succ`, `subset_of_fluxesFive_mem_noExoticsSubsets_of_noExotics`, `recS`, `card_le_three_of_noExotics`, `card_mem_range_four_of_noExotics`, `mem_elemsNoExotics_of_noExotics`, `mem_mem_finset_of_noExotics`, `noExotics_iff_mem_elemsNoExotics`, `subset_le_mem_of_card_eq_succ`, `subset_of_fluxesTen_mem_noExoticsSubsets_of_noExotics`, `recS`	16
Total	18

FTheory.SU5.FluxesFive

Definitions

Name	Category	Theorems
`noExoticsSubsets` 📖	CompOp	2 math math: `subset_of_fluxesFive_mem_noExoticsSubsets_of_noExotics`, `subset_of_fluxesFive_mem_noExoticsSubsets_of_noExotics.recS`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_six_of_noExotics` 📖	mathematical	`NoExotics` `HasNoZero`	`FTheory.SU5.Fluxes`	—	`subset_of_fluxesFive_mem_noExoticsSubsets_of_noExotics`
`card_mem_range_seven_of_noExotics` 📖	mathematical	`NoExotics` `HasNoZero`	`FTheory.SU5.Fluxes`	—	`card_le_six_of_noExotics`
`mem_elemsNoExotics_of_noExotics` 📖	mathematical	`NoExotics` `HasNoZero`	`FTheory.SU5.FluxesFive` `elemsNoExotics`	—	`card_mem_range_seven_of_noExotics` `subset_of_fluxesFive_mem_noExoticsSubsets_of_noExotics`
`mem_mem_finset_of_noExotics` 📖	mathematical	`NoExotics` `HasNoZero` `FTheory.SU5.Fluxes` `FTheory.SU5.FluxesFive`	`FTheory.SU5.instDecidableEqFluxes`	—	`mem_chiralIndicesOfL_mem_of_noExotics` `mem_chiralIndicesOfD_mem_of_noExotics`
`noExotics_iff_mem_elemsNoExotics` 📖	mathematical	—	`NoExotics` `HasNoZero` `FTheory.SU5.FluxesFive` `elemsNoExotics`	—	`mem_elemsNoExotics_of_noExotics` `noExotics_of_mem_elemsNoExotics` `hasNoZero_of_mem_elemsNoExotics`
`subset_le_mem_of_card_eq_succ` 📖	—	`NoExotics` `HasNoZero` `FTheory.SU5.Fluxes`	—	—	`chiralIndicesOfL_subset_sum_le_three_of_noExotics` `chiralIndicesOfD_subset_sum_le_three_of_noExotics` `mem_mem_finset_of_noExotics`
`subset_of_fluxesFive_mem_noExoticsSubsets_of_noExotics` 📖	mathematical	`NoExotics` `HasNoZero` `FTheory.SU5.Fluxes`	`noExoticsSubsets`	—	`subset_of_fluxesFive_mem_noExoticsSubsets_of_noExotics.recS`

FTheory.SU5.FluxesFive.subset_of_fluxesFive_mem_noExoticsSubsets_of_noExotics

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`recS` 📖	mathematical	`FTheory.SU5.FluxesFive.NoExotics` `FTheory.SU5.FluxesFive.HasNoZero` `FTheory.SU5.Fluxes`	`FTheory.SU5.FluxesFive.noExoticsSubsets`	—	`FTheory.SU5.FluxesFive.subset_le_mem_of_card_eq_succ`

FTheory.SU5.FluxesTen

Definitions

Name	Category	Theorems
`noExoticsSubsets` 📖	CompOp	2 math math: `subset_of_fluxesTen_mem_noExoticsSubsets_of_noExotics`, `subset_of_fluxesTen_mem_noExoticsSubsets_of_noExotics.recS`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_three_of_noExotics` 📖	mathematical	`NoExotics` `HasNoZero`	`FTheory.SU5.Fluxes`	—	`subset_of_fluxesTen_mem_noExoticsSubsets_of_noExotics`
`card_mem_range_four_of_noExotics` 📖	mathematical	`NoExotics` `HasNoZero`	`FTheory.SU5.Fluxes`	—	`card_le_three_of_noExotics`
`mem_elemsNoExotics_of_noExotics` 📖	mathematical	`NoExotics` `HasNoZero`	`FTheory.SU5.FluxesTen` `elemsNoExotics`	—	`card_mem_range_four_of_noExotics` `subset_of_fluxesTen_mem_noExoticsSubsets_of_noExotics`
`mem_mem_finset_of_noExotics` 📖	mathematical	`NoExotics` `HasNoZero` `FTheory.SU5.Fluxes` `FTheory.SU5.FluxesTen`	`FTheory.SU5.instDecidableEqFluxes`	—	`mem_chiralIndicesOfQ_mem_of_noExotics` `mem_chiralIndicesOfU_mem_of_noExotics` `mem_chiralIndicesOfE_mem_of_noExotics`
`noExotics_iff_mem_elemsNoExotics` 📖	mathematical	—	`NoExotics` `HasNoZero` `FTheory.SU5.FluxesTen` `elemsNoExotics`	—	`mem_elemsNoExotics_of_noExotics` `noExotics_of_mem_elemsNoExotics` `hasNoZero_of_mem_elemsNoExotics`
`subset_le_mem_of_card_eq_succ` 📖	—	`NoExotics` `HasNoZero` `FTheory.SU5.Fluxes`	—	—	`chiralIndicesOfQ_subset_sum_le_three_of_noExotics` `chiralIndicesOfU_subset_sum_le_three_of_noExotics` `chiralIndicesOfE_subset_sum_le_three_of_noExotics` `mem_mem_finset_of_noExotics`
`subset_of_fluxesTen_mem_noExoticsSubsets_of_noExotics` 📖	mathematical	`NoExotics` `HasNoZero` `FTheory.SU5.Fluxes`	`noExoticsSubsets`	—	`subset_of_fluxesTen_mem_noExoticsSubsets_of_noExotics.recS`

FTheory.SU5.FluxesTen.subset_of_fluxesTen_mem_noExoticsSubsets_of_noExotics

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`recS` 📖	mathematical	`FTheory.SU5.FluxesTen.NoExotics` `FTheory.SU5.FluxesTen.HasNoZero` `FTheory.SU5.Fluxes`	`FTheory.SU5.FluxesTen.noExoticsSubsets`	—	`FTheory.SU5.FluxesTen.subset_le_mem_of_card_eq_succ`

---

← Back to Index