Documentation Verification Report

Sorts

📁 Source: PhysLean/QFT/QED/AnomalyCancellation/Sorts.lean

Statistics

Metric	Count
Definitions `Sorted`, `sort`, `sortAFL`	3
Theorems `sortAFL_val`, `sortAFL_zero`, `sort_apply`, `sort_perm`, `sort_projection`, `sort_sorted`, `sort_zero`	7
Total	10

PureU1

Definitions

Name	Category	Theorems
`Sorted` 📖	MathDef	1 math math: `sort_sorted`
`sort` 📖	CompOp	6 math math: `sort_perm`, `sort_apply`, `constAbs_sort`, `sort_sorted`, `sort_projection`, `sortAFL_val`
`sortAFL` 📖	CompOp	1 math math: `sortAFL_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sortAFL_val` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `sortAFL` `sort`	—	—
`sortAFL_zero` 📖	—	`sortAFL` `ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemLinear.linSolsAddCommGroup`	—	—	`ACCSystemLinear.LinSols.ext` `sortAFL_val` `sort_zero`
`sort_apply` 📖	mathematical	—	`sort` `ACCSystemCharges.numberCharges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1`	—	—
`sort_perm` 📖	mathematical	—	`sort` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystemGroupAction.group` `FamilyPermutations` `ACCSystemGroupAction.groupInst` `ACCSystemGroupAction.rep`	—	—
`sort_projection` 📖	mathematical	—	`sort`	—	`sort_perm`
`sort_sorted` 📖	mathematical	—	`Sorted` `sort`	—	—
`sort_zero` 📖	—	`sort` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemCharges.ChargesAddCommGroup`	—	—	`sort_apply`

---

← Back to Index