Documentation Verification Report

Permutations

📁 Source: PhysLean/Particles/BeyondTheStandardModel/RHN/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

SMRHN

Definitions

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

Theorems

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

---

← Back to Index