Documentation Verification Report

Yukawa

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

Statistics

Metric	Count
Definitions `YukawaGeneratesDangerousAtLevel`, `instDecidableYukawaGeneratesDangerousAtLevel`, `ofYukawaTerms`, `ofYukawaTermsNSum`	4
Theorems `YukawaGeneratesDangerousAtLevel_iff_inter`, `not_yukawaGeneratesDangerousAtLevel_of_empty`, `ofYukawaTermsNSum_subset_of_subset`, `ofYukawaTerms_subset_of_subset`, `yukawaGeneratesDangerousAtLevel_add_of_left`, `yukawaGeneratesDangerousAtLevel_iff_toFinset`, `yukawaGeneratesDangerousAtLevel_of_le`, `yukawaGeneratesDangerousAtLevel_of_subset`, `yukawaGeneratesDangerousAtLevel_succ`	9
Total	13

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`YukawaGeneratesDangerousAtLevel` 📖	MathDef	11 math math: `not_yukawaGeneratesDangerousAtLevel_of_empty`, `FTheory.SU5.Quanta.IsViable.not_regenerate_dangerous_couplings`, `YukawaGeneratesDangerousAtLevel_iff_inter`, `FTheory.SU5.ChargeSpectrum.viableCompletions_yukawaGeneratesDangerousAtLevel_one`, `FTheory.SU5.ChargeSpectrum.not_yukawaGeneratesDangerousAtLevel_one_of_mem_viableCharges`, `yukawaGeneratesDangerousAtLevel_iff_toFinset`, `FTheory.SU5.Quanta.yukawaSingletsRegenerateDangerousInsertion_two_of_isViable`, `FTheory.SU5.Quanta.isViable_iff_def`, `FTheory.SU5.ChargeSpectrum.yukawaGeneratesDangerousAtLevel_one_of_mem_viableChargesAdditional`, `FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff'`, `FTheory.SU5.ChargeSpectrum.mem_viableCharges_iff`
`instDecidableYukawaGeneratesDangerousAtLevel` 📖	CompOp	—
`ofYukawaTerms` 📖	CompOp	3 math math: `map_ofYukawaTerms_toFinset`, `mem_map_ofYukawaTerms_iff`, `ofYukawaTerms_subset_of_subset`
`ofYukawaTermsNSum` 📖	CompOp	3 math math: `ofYukawaTermsNSum_subset_of_subset`, `map_ofYukawaTermsNSum_toFinset`, `mem_map_ofYukawaTermsNSum_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`YukawaGeneratesDangerousAtLevel_iff_inter` 📖	mathematical	—	`YukawaGeneratesDangerousAtLevel`	—	—
`not_yukawaGeneratesDangerousAtLevel_of_empty` 📖	mathematical	—	`YukawaGeneratesDangerousAtLevel` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	`phenoConstrainingChargesSP_empty`
`ofYukawaTermsNSum_subset_of_subset` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset`	`ofYukawaTermsNSum`	—	`ofYukawaTerms_subset_of_subset`
`ofYukawaTerms_subset_of_subset` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset`	`ofYukawaTerms`	—	`ofPotentialTerm'_mono`
`yukawaGeneratesDangerousAtLevel_add_of_left` 📖	—	`YukawaGeneratesDangerousAtLevel`	—	—	`yukawaGeneratesDangerousAtLevel_succ`
`yukawaGeneratesDangerousAtLevel_iff_toFinset` 📖	mathematical	—	`YukawaGeneratesDangerousAtLevel`	—	—
`yukawaGeneratesDangerousAtLevel_of_le` 📖	—	`YukawaGeneratesDangerousAtLevel`	—	—	`yukawaGeneratesDangerousAtLevel_add_of_left`
`yukawaGeneratesDangerousAtLevel_of_subset` 📖	—	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `YukawaGeneratesDangerousAtLevel`	—	—	`phenoConstrainingChargesSP_mono` `ofYukawaTermsNSum_subset_of_subset`
`yukawaGeneratesDangerousAtLevel_succ` 📖	—	`YukawaGeneratesDangerousAtLevel`	—	—	—

---

← Back to Index