Documentation Verification Report

Potential

📁 Source: PhysLean/Particles/SuperSymmetry/SU5/Potential.lean

Statistics

Metric	Count
Definitions `PotentialTerm`, `InSuperPotential`, `RParity`, `causeProtonDecay`, `degree`, `instDecidableInSuperPotential`, `toFieldLabel`, `instDecidableEqPotentialTerm`, `instFintypePotentialTerm`	9
Theorems `degree_le_four`, `no_conjugate_in_toFieldLabel_of_inSuperPotential`, `violates_RParity_iff_mem`	3
Total	12

SuperSymmetry.SU5

Definitions

Name	Category	Theorems
`PotentialTerm` 📖	CompData	2 math math: `PotentialTerm.violates_RParity_iff_mem`, `ChargeSpectrum.minimallyAllowsFinsetTerms_singleton`
`instDecidableEqPotentialTerm` 📖	CompOp	1 math math: `PotentialTerm.violates_RParity_iff_mem`
`instFintypePotentialTerm` 📖	CompOp	—

SuperSymmetry.SU5.PotentialTerm

Definitions

Name	Category	Theorems
`InSuperPotential` 📖	MathDef	—
`RParity` 📖	CompOp	1 math math: `violates_RParity_iff_mem`
`causeProtonDecay` 📖	CompOp	—
`degree` 📖	CompOp	4 math math: `degree_le_four`, `SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm_card_le_degree`, `SuperSymmetry.SU5.ChargeSpectrum.card_le_degree_of_minimallyAllowsTerm`, `SuperSymmetry.SU5.ChargeSpectrum.subset_card_le_degree_allowsTerm_of_allowsTerm`
`instDecidableInSuperPotential` 📖	CompOp	—
`toFieldLabel` 📖	CompOp	1 math math: `no_conjugate_in_toFieldLabel_of_inSuperPotential`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degree_le_four` 📖	mathematical	—	`degree`	—	—
`no_conjugate_in_toFieldLabel_of_inSuperPotential` 📖	mathematical	`InSuperPotential`	`SuperSymmetry.SU5.FieldLabel` `toFieldLabel` `SuperSymmetry.SU5.FieldLabel.fiveMatter` `SuperSymmetry.SU5.FieldLabel.fiveHd` `SuperSymmetry.SU5.FieldLabel.fiveBarHu`	—	—
`violates_RParity_iff_mem` 📖	mathematical	—	`RParity` `SuperSymmetry.SU5.PotentialTerm` `SuperSymmetry.SU5.instDecidableEqPotentialTerm` `β` `Λ` `W2` `W4` `K1` `K2`	—	—

---

← Back to Index