Documentation Verification Report

GroupActions

📁 Source: PhysLean/QFT/AnomalyCancellation/GroupActions.lean

Statistics

Metric	Count
Definitions `ACCSystemGroupAction`, `group`, `groupInst`, `instGroupGroup`, `linSolMap`, `linSolRep`, `quadSolAction`, `rep`, `solAction`	9
Theorems `cubicInvariant`, `linSolRep_apply_apply_val`, `linSolRep_quadSolAction_commute`, `linSolRep_solAction_commute`, `linearInvariant`, `quadInvariant`, `quadSolAction_solAction_commute`, `rep_linSolRep_commute`, `rep_quadSolAction_commute`, `rep_solAction_commute`	10
Total	19

ACCSystemGroupAction

Definitions

Name	Category	Theorems
`group` 📖	CompOp	19 math math: `rep_linSolRep_commute`, `PureU1.sort_perm`, `PureU1.lineInPlaneCond_perm`, `PureU1.FamilyPermutations_anomalyFreeLinear_apply`, `quadInvariant`, `cubicInvariant`, `PureU1.FamilyPermutations_charges_apply`, `PureU1.Odd.lineInCubicPerm_permute`, `linSolRep_solAction_commute`, `linSolRep_quadSolAction_commute`, `PureU1.VectorLikeEvenPlane.vectorLikeEven_in_span`, `quadSolAction_solAction_commute`, `PureU1.Even.lineInCubicPerm_permute`, `PureU1.Even.lineInCubicPerm_in_plane`, `linearInvariant`, `PureU1.constAbs_perm`, `rep_solAction_commute`, `linSolRep_apply_apply_val`, `rep_quadSolAction_commute`
`groupInst` 📖	CompOp	10 math math: `rep_linSolRep_commute`, `PureU1.sort_perm`, `quadInvariant`, `cubicInvariant`, `PureU1.FamilyPermutations_charges_apply`, `linearInvariant`, `PureU1.constAbs_perm`, `rep_solAction_commute`, `linSolRep_apply_apply_val`, `rep_quadSolAction_commute`
`instGroupGroup` 📖	CompOp	13 math math: `rep_linSolRep_commute`, `PureU1.lineInPlaneCond_perm`, `PureU1.FamilyPermutations_anomalyFreeLinear_apply`, `PureU1.Odd.lineInCubicPerm_permute`, `linSolRep_solAction_commute`, `linSolRep_quadSolAction_commute`, `PureU1.VectorLikeEvenPlane.vectorLikeEven_in_span`, `quadSolAction_solAction_commute`, `PureU1.Even.lineInCubicPerm_permute`, `PureU1.Even.lineInCubicPerm_in_plane`, `rep_solAction_commute`, `linSolRep_apply_apply_val`, `rep_quadSolAction_commute`
`linSolMap` 📖	CompOp	—
`linSolRep` 📖	CompOp	10 math math: `rep_linSolRep_commute`, `PureU1.lineInPlaneCond_perm`, `PureU1.FamilyPermutations_anomalyFreeLinear_apply`, `PureU1.Odd.lineInCubicPerm_permute`, `linSolRep_solAction_commute`, `linSolRep_quadSolAction_commute`, `PureU1.VectorLikeEvenPlane.vectorLikeEven_in_span`, `PureU1.Even.lineInCubicPerm_permute`, `PureU1.Even.lineInCubicPerm_in_plane`, `linSolRep_apply_apply_val`
`quadSolAction` 📖	CompOp	3 math math: `linSolRep_quadSolAction_commute`, `quadSolAction_solAction_commute`, `rep_quadSolAction_commute`
`rep` 📖	CompOp	10 math math: `rep_linSolRep_commute`, `PureU1.sort_perm`, `quadInvariant`, `cubicInvariant`, `PureU1.FamilyPermutations_charges_apply`, `linearInvariant`, `PureU1.constAbs_perm`, `rep_solAction_commute`, `linSolRep_apply_apply_val`, `rep_quadSolAction_commute`
`solAction` 📖	CompOp	3 math math: `linSolRep_solAction_commute`, `quadSolAction_solAction_commute`, `rep_solAction_commute`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cubicInvariant` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `ACCSystem.cubicACC` `group` `groupInst` `rep`	—	—
`linSolRep_apply_apply_val` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemLinear.LinSols` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule` `group` `instGroupGroup` `linSolRep` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `groupInst` `rep`	—	—
`linSolRep_quadSolAction_commute` 📖	mathematical	—	`ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `ACCSystemQuad.quadSolsMulAction` `ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystemLinear.linSolsAddCommGroup` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule` `ACCSystemQuad.quadSolsInclLinSols` `group` `instGroupGroup` `quadSolAction` `linSolRep`	—	—
`linSolRep_solAction_commute` 📖	mathematical	—	`ACCSystem.Sols` `ACCSystem.solsMulAction` `ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemLinear.linSolsAddCommGroup` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule` `ACCSystem.solsInclLinSols` `group` `instGroupGroup` `solAction` `linSolRep`	—	—
`linearInvariant` 📖	mathematical	—	`ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystemLinear.linearACCs` `group` `groupInst` `rep`	—	—
`quadInvariant` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `ACCSystemQuad.quadraticACCs` `group` `groupInst` `rep`	—	—
`quadSolAction_solAction_commute` 📖	mathematical	—	`ACCSystem.Sols` `ACCSystem.solsMulAction` `ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `ACCSystemQuad.quadSolsMulAction` `ACCSystem.solsInclQuadSols` `group` `instGroupGroup` `solAction` `quadSolAction`	—	—
`rep_linSolRep_commute` 📖	mathematical	—	`ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemLinear.linSolsModule` `ACCSystemCharges.chargesModule` `ACCSystemLinear.linSolsIncl` `group` `instGroupGroup` `linSolRep` `groupInst` `rep`	—	—
`rep_quadSolAction_commute` 📖	mathematical	—	`ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `ACCSystemQuad.quadSolsMulAction` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystemQuad.quadSolsIncl` `group` `instGroupGroup` `quadSolAction` `groupInst` `rep`	—	—
`rep_solAction_commute` 📖	mathematical	—	`ACCSystem.Sols` `ACCSystem.solsMulAction` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystem.solsIncl` `group` `instGroupGroup` `solAction` `groupInst` `rep`	—	—

(root)

Definitions

Name	Category	Theorems
`ACCSystemGroupAction` 📖	CompData	—

---

← Back to Index