Documentation Verification Report

Permutations

📁 Source: PhysLean/Particles/StandardModel/AnomalyCancellation/Permutations.lean

Statistics

Metric	Count
Definitions `PermGroup`, `chargeMap`, `instGroupPermGroup`, `repCharges`	4
Theorems `accCube_invariant`, `accGrav_invariant`, `accQuad_invariant`, `accSU2_invariant`, `accSU3_invariant`, `accYY_invariant`, `chargeMap_apply`, `repCharges_toSpecies`, `toSpecies_sum_invariant`	9
Total	13

SM

Definitions

Name	Category	Theorems
`PermGroup` 📖	CompOp	8 math math: `toSpecies_sum_invariant`, `accSU2_invariant`, `accQuad_invariant`, `accCube_invariant`, `accGrav_invariant`, `repCharges_toSpecies`, `accYY_invariant`, `accSU3_invariant`
`chargeMap` 📖	CompOp	1 math math: `chargeMap_apply`
`instGroupPermGroup` 📖	CompOp	8 math math: `toSpecies_sum_invariant`, `accSU2_invariant`, `accQuad_invariant`, `accCube_invariant`, `accGrav_invariant`, `repCharges_toSpecies`, `accYY_invariant`, `accSU3_invariant`
`repCharges` 📖	CompOp	8 math math: `toSpecies_sum_invariant`, `accSU2_invariant`, `accQuad_invariant`, `accCube_invariant`, `accGrav_invariant`, `repCharges_toSpecies`, `accYY_invariant`, `accSU3_invariant`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`accCube_invariant` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `SMACCs.accCube` `PermGroup` `instGroupPermGroup` `repCharges`	—	`SMACCs.accCube_ext` `toSpecies_sum_invariant`
`accGrav_invariant` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMACCs.accGrav` `PermGroup` `instGroupPermGroup` `repCharges`	—	`SMACCs.accGrav_ext` `toSpecies_sum_invariant`
`accQuad_invariant` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `SMACCs.accQuad` `PermGroup` `instGroupPermGroup` `repCharges`	—	`SMACCs.accQuad_ext` `toSpecies_sum_invariant`
`accSU2_invariant` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMACCs.accSU2` `PermGroup` `instGroupPermGroup` `repCharges`	—	`SMACCs.accSU2_ext` `toSpecies_sum_invariant`
`accSU3_invariant` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMACCs.accSU3` `PermGroup` `instGroupPermGroup` `repCharges`	—	`SMACCs.accSU3_ext` `toSpecies_sum_invariant`
`accYY_invariant` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMACCs.accYY` `PermGroup` `instGroupPermGroup` `repCharges`	—	`SMACCs.accYY_ext` `toSpecies_sum_invariant`
`chargeMap_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `chargeMap` `SMCharges.toSpeciesEquiv` `SMSpecies` `SMCharges.toSpecies`	—	—
`repCharges_toSpecies` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `SMSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMCharges.toSpecies` `PermGroup` `instGroupPermGroup` `repCharges` `ACCSystemCharges.numberCharges`	—	`SMCharges.toSMSpecies_toSpecies_inv`
`toSpecies_sum_invariant` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `SMSpecies` `ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMCharges.toSpecies` `PermGroup` `instGroupPermGroup` `repCharges`	—	`repCharges_toSpecies`

---

← Back to Index