Documentation Verification Report

LineInPlaneCond

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

Statistics

Metric	Count
Definitions `LineInPlaneCond`, `LineInPlaneProp`	2
Theorems `lineInPlaneCond_eq_last`, `lineInPlaneCond_eq_last'`, `lineInPlaneCond_perm`, `linesInPlane_constAbs`, `linesInPlane_constAbs_AF`, `linesInPlane_constAbs_four`, `linesInPlane_eq_sq`, `linesInPlane_eq_sq_four`, `linesInPlane_four`	9
Total	11

PureU1

Definitions

Name	Category	Theorems
`LineInPlaneCond` 📖	MathDef	2 math math: `Odd.lineInCubicPerm_last_perm`, `Even.lineInCubicPerm_last_perm`
`LineInPlaneProp` 📖	MathDef	2 math math: `Odd.lineInCubicPerm_last_cond`, `Even.lineInCubicPerm_last_cond`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lineInPlaneCond_eq_last` 📖	mathematical	`LineInPlaneCond`	`ConstAbsProp` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1`	—	`ConstAbsProp.eq_1` `lineInPlaneCond_eq_last'`
`lineInPlaneCond_eq_last'` 📖	—	`LineInPlaneCond` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1`	—	—	`LineInPlaneCond.eq_1` `pureU1_last`
`lineInPlaneCond_perm` 📖	mathematical	`LineInPlaneCond`	`ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule` `ACCSystemGroupAction.group` `FamilyPermutations` `ACCSystemGroupAction.instGroupGroup` `ACCSystemGroupAction.linSolRep`	—	`FamilyPermutations_anomalyFreeLinear_apply`
`linesInPlane_constAbs` 📖	mathematical	`LineInPlaneCond`	`ConstAbs` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1`	—	`linesInPlane_eq_sq`
`linesInPlane_constAbs_AF` 📖	mathematical	`LineInPlaneCond` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystem.Sols.toQuadSols`	`ConstAbs` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear`	—	`linesInPlane_constAbs_four` `linesInPlane_constAbs`
`linesInPlane_constAbs_four` 📖	mathematical	`LineInPlaneCond` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystem.Sols.toQuadSols`	`ConstAbs` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear`	—	`linesInPlane_eq_sq_four`
`linesInPlane_eq_sq` 📖	mathematical	`LineInPlaneCond`	`ConstAbsProp` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1`	—	`Prop_two` `lineInPlaneCond_eq_last` `lineInPlaneCond_perm`
`linesInPlane_eq_sq_four` 📖	mathematical	`LineInPlaneCond` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystem.Sols.toQuadSols`	`ConstAbsProp` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear`	—	`Prop_two` `lineInPlaneCond_perm` `linesInPlane_four`
`linesInPlane_four` 📖	mathematical	`LineInPlaneCond` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystem.Sols.toQuadSols`	`ConstAbsProp` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear`	—	`pureU1_linear` `pureU1_cube`

---

← Back to Index