Documentation Verification Report

Permutations

📁 Source: PhysLean/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Permutations.lean

Statistics

Metric	Count
Definitions `PermGroup`, `chargeMap`, `instGroupPermGroup`, `repCharges`	4
Theorems `Hd_invariant`, `Hu_invariant`, `accCube_invariant`, `accGrav_invariant`, `accQuad_invariant`, `accSU2_invariant`, `accSU3_invariant`, `accYY_invariant`, `chargeMap_apply`, `chargeMap_toSpecies`, `repCharges_toSMSpecies`, `toSpecies_sum_invariant`	12
Total	16

MSSM

Definitions

Name	Category	Theorems
`PermGroup` 📖	CompOp	10 math math: `accSU2_invariant`, `accSU3_invariant`, `accCube_invariant`, `Hu_invariant`, `accQuad_invariant`, `accGrav_invariant`, `repCharges_toSMSpecies`, `toSpecies_sum_invariant`, `accYY_invariant`, `Hd_invariant`
`chargeMap` 📖	CompOp	2 math math: `chargeMap_apply`, `chargeMap_toSpecies`
`instGroupPermGroup` 📖	CompOp	10 math math: `accSU2_invariant`, `accSU3_invariant`, `accCube_invariant`, `Hu_invariant`, `accQuad_invariant`, `accGrav_invariant`, `repCharges_toSMSpecies`, `toSpecies_sum_invariant`, `accYY_invariant`, `Hd_invariant`
`repCharges` 📖	CompOp	10 math math: `accSU2_invariant`, `accSU3_invariant`, `accCube_invariant`, `Hu_invariant`, `accQuad_invariant`, `accGrav_invariant`, `repCharges_toSMSpecies`, `toSpecies_sum_invariant`, `accYY_invariant`, `Hd_invariant`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Hd_invariant` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMCharges.Hd` `PermGroup` `instGroupPermGroup` `repCharges`	—	—
`Hu_invariant` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMCharges.Hu` `PermGroup` `instGroupPermGroup` `repCharges`	—	—
`accCube_invariant` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `MSSMACCs.accCube` `PermGroup` `instGroupPermGroup` `repCharges`	—	`MSSMACCs.accCube_ext` `toSpecies_sum_invariant` `Hd_invariant` `Hu_invariant`
`accGrav_invariant` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMACCs.accGrav` `PermGroup` `instGroupPermGroup` `repCharges`	—	`MSSMACCs.accGrav_ext` `toSpecies_sum_invariant` `Hd_invariant` `Hu_invariant`
`accQuad_invariant` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `MSSMACCs.accQuad` `PermGroup` `instGroupPermGroup` `repCharges`	—	`MSSMACCs.accQuad_ext` `toSpecies_sum_invariant` `Hd_invariant` `Hu_invariant`
`accSU2_invariant` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMACCs.accSU2` `PermGroup` `instGroupPermGroup` `repCharges`	—	`MSSMACCs.accSU2_ext` `toSpecies_sum_invariant` `Hd_invariant` `Hu_invariant`
`accSU3_invariant` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMACCs.accSU3` `PermGroup` `instGroupPermGroup` `repCharges`	—	`MSSMACCs.accSU3_ext` `toSpecies_sum_invariant`
`accYY_invariant` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMACCs.accYY` `PermGroup` `instGroupPermGroup` `repCharges`	—	`MSSMACCs.accYY_ext` `toSpecies_sum_invariant` `Hd_invariant` `Hu_invariant`
`chargeMap_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `chargeMap` `MSSMCharges.toSMPlusH` `MSSMCharges.splitSMPlusH` `MSSMCharges.toSpeciesMaps'` `MSSMSpecies` `MSSMCharges.toSMSpecies`	—	—
`chargeMap_toSpecies` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `MSSMSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMCharges.toSMSpecies` `chargeMap` `ACCSystemCharges.numberCharges`	—	`MSSMCharges.toSMSpecies_toSpecies_inv`
`repCharges_toSMSpecies` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `MSSMSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMCharges.toSMSpecies` `PermGroup` `instGroupPermGroup` `repCharges` `ACCSystemCharges.numberCharges`	—	`MSSMCharges.toSMSpecies_toSpecies_inv`
`toSpecies_sum_invariant` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `MSSMSpecies` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMCharges.toSMSpecies` `PermGroup` `instGroupPermGroup` `repCharges`	—	`repCharges_toSMSpecies`

---

← Back to Index