Documentation Verification Report

PhenoConstrained

📁 Source: PhysLean/Particles/SuperSymmetry/SU5/ChargeSpectrum/PhenoConstrained.lean

Statistics

Metric	Count
Definitions `IsPhenoConstrained`, `IsPhenoConstrainedQ10`, `IsPhenoConstrainedQ5`, `decidableIsPhenoConstrained`, `decidableIsPhenoConstrainedQ10`, `decidableIsPhenoConstrainedQ5`, `phenoConstrainingChargesSP`	7
Theorems `isPhenoConstrainedQ10_iff`, `isPhenoConstrainedQ5_iff`, `isPhenoConstrained_insertQ10_iff_isPhenoConstrainedQ10`, `isPhenoConstrained_insertQ5_iff_isPhenoConstrainedQ5`, `isPhenoConstrained_mono`, `not_isPhenoConstrained_empty`, `phenoConstrainingChargesSP_empty`, `phenoConstrainingChargesSP_mono`	8
Total	15

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`IsPhenoConstrained` 📖	MathDef	11 math math: `not_isPhenoConstrained_of_minimallyAllowsTermsOfFinset_topYukawa`, `not_isPhenoConstrained_empty`, `isPhenoConstrained_insertQ10_iff_isPhenoConstrainedQ10`, `isPhenoConstrained_insertQ5_iff_isPhenoConstrainedQ5`, `FTheory.SU5.ChargeSpectrum.not_isPhenoConstrained_of_mem_viableChargesAdditional`, `FTheory.SU5.Quanta.isViable_iff_def`, `FTheory.SU5.ChargeSpectrum.not_isPhenoConstrained_of_mem_viableCharges`, `FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff'`, `FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff`, `FTheory.SU5.Quanta.IsViable.not_pheno_constrained`, `FTheory.SU5.ChargeSpectrum.viableCompletions_isPhenoConstrained`
`IsPhenoConstrainedQ10` 📖	MathDef	2 math math: `isPhenoConstrained_insertQ10_iff_isPhenoConstrainedQ10`, `isPhenoConstrainedQ10_iff`
`IsPhenoConstrainedQ5` 📖	MathDef	2 math math: `isPhenoConstrainedQ5_iff`, `isPhenoConstrained_insertQ5_iff_isPhenoConstrainedQ5`
`decidableIsPhenoConstrained` 📖	CompOp	—
`decidableIsPhenoConstrainedQ10` 📖	CompOp	—
`decidableIsPhenoConstrainedQ5` 📖	CompOp	—
`phenoConstrainingChargesSP` 📖	CompOp	3 math math: `map_phenoConstrainingChargesSP_toFinset`, `phenoConstrainingChargesSP_mono`, `phenoConstrainingChargesSP_empty`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPhenoConstrainedQ10_iff` 📖	mathematical	—	`IsPhenoConstrainedQ10` `AllowsTermQ10` `SuperSymmetry.SU5.PotentialTerm.Λ` `SuperSymmetry.SU5.PotentialTerm.W2` `SuperSymmetry.SU5.PotentialTerm.K1` `SuperSymmetry.SU5.PotentialTerm.K2` `SuperSymmetry.SU5.PotentialTerm.W1`	—	—
`isPhenoConstrainedQ5_iff` 📖	mathematical	—	`IsPhenoConstrainedQ5` `AllowsTermQ5` `SuperSymmetry.SU5.PotentialTerm.β` `SuperSymmetry.SU5.PotentialTerm.Λ` `SuperSymmetry.SU5.PotentialTerm.W4` `SuperSymmetry.SU5.PotentialTerm.K1` `SuperSymmetry.SU5.PotentialTerm.W1`	—	—
`isPhenoConstrained_insertQ10_iff_isPhenoConstrainedQ10` 📖	mathematical	—	`IsPhenoConstrained` `IsPhenoConstrainedQ10`	—	`allowsTerm_insertQ10_iff_allowsTermQ10` `allowsTerm_insertQ10_of_allowsTermQ10` `isPhenoConstrained_mono`
`isPhenoConstrained_insertQ5_iff_isPhenoConstrainedQ5` 📖	mathematical	—	`IsPhenoConstrained` `IsPhenoConstrainedQ5`	—	`allowsTerm_insertQ5_iff_allowsTermQ5` `allowsTerm_insertQ5_of_allowsTermQ5` `isPhenoConstrained_mono`
`isPhenoConstrained_mono` 📖	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `IsPhenoConstrained`	—	—	`allowsTerm_mono`
`not_isPhenoConstrained_empty` 📖	mathematical	—	`IsPhenoConstrained` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	`ofPotentialTerm_empty`
`phenoConstrainingChargesSP_empty` 📖	mathematical	—	`phenoConstrainingChargesSP` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	`ofPotentialTerm'_empty`
`phenoConstrainingChargesSP_mono` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset`	`phenoConstrainingChargesSP`	—	`ofPotentialTerm'_mono`

---

← Back to Index