Documentation Verification Report

LineInCubic

📁 Source: PhysLean/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean

Statistics

Metric	Count
Definitions `LineInCubic`, `LineInCubicPerm`	2
Theorems `P_P_P!_accCube'`, `lineInCubicPerm_constAbs`, `lineInCubicPerm_in_plane`, `lineInCubicPerm_last_cond`, `lineInCubicPerm_last_perm`, `lineInCubicPerm_permute`, `lineInCubicPerm_self`, `lineInCubicPerm_swap`, `lineInCubicPerm_vectorLike`, `lineInCubic_expand`, `line_in_cubic_P_P_P!`	11
Total	13

PureU1.Even

Definitions

Name	Category	Theorems
`LineInCubic` 📖	MathDef	2 math math: `lineInCubicPerm_self`, `special_case_lineInCubic`
`LineInCubicPerm` 📖	MathDef	1 math math: `special_case_lineInCubic_perm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`P_P_P!_accCube'` 📖	mathematical	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `PureU1.VectorLikeEvenPlane.Pa`	`ACCSystemCharges.Charges` `PureU1.PureU1Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `PureU1.accCubeTriLinSymm` `PureU1.VectorLikeEvenPlane.P` `PureU1.VectorLikeEvenPlane.basis!AsCharges` `PureU1.VectorLikeEvenPlane.evenShiftSnd` `PureU1.VectorLikeEvenPlane.evenShiftFst` `PureU1.VectorLikeEvenPlane.evenShiftLast`	—	`PureU1.VectorLikeEvenPlane.P_P_P!_accCube` `PureU1.VectorLikeEvenPlane.Pa_evenShiftLast` `PureU1.VectorLikeEvenPlane.Pa_evenShiftFst` `PureU1.VectorLikeEvenPlane.Pa_evenShiftSnd`
`lineInCubicPerm_constAbs` 📖	mathematical	`LineInCubicPerm` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystem.Sols.toQuadSols`	`PureU1.ConstAbs` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear`	—	`PureU1.linesInPlane_constAbs_AF` `lineInCubicPerm_last_perm`
`lineInCubicPerm_in_plane` 📖	mathematical	`LineInCubicPerm` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystem.Sols.toQuadSols`	`ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule` `PureU1.VectorLikeEvenPlane.basis` `ACCSystemGroupAction.group` `PureU1.FamilyPermutations` `ACCSystemGroupAction.instGroupGroup` `ACCSystemGroupAction.linSolRep`	—	`PureU1.VectorLikeEvenPlane.vectorLikeEven_in_span` `lineInCubicPerm_vectorLike`
`lineInCubicPerm_last_cond` 📖	mathematical	`LineInCubicPerm`	`PureU1.LineInPlaneProp` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `PureU1.VectorLikeEvenPlane.evenShiftSnd` `PureU1.VectorLikeEvenPlane.evenShiftFst` `PureU1.VectorLikeEvenPlane.evenShiftLast`	—	`PureU1.VectorLikeEvenPlane.span_basis` `lineInCubicPerm_swap` `P_P_P!_accCube'`
`lineInCubicPerm_last_perm` 📖	mathematical	`LineInCubicPerm`	`PureU1.LineInPlaneCond`	—	`PureU1.Prop_three` `PureU1.VectorLikeEvenPlane.n_cond₂` `lineInCubicPerm_last_cond` `lineInCubicPerm_permute`
`lineInCubicPerm_permute` 📖	mathematical	`LineInCubicPerm`	`ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule` `ACCSystemGroupAction.group` `PureU1.FamilyPermutations` `ACCSystemGroupAction.instGroupGroup` `ACCSystemGroupAction.linSolRep`	—	`LineInCubicPerm.eq_1`
`lineInCubicPerm_self` 📖	mathematical	`LineInCubicPerm`	`LineInCubic`	—	—
`lineInCubicPerm_swap` 📖	mathematical	`LineInCubicPerm` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `PureU1.VectorLikeEvenPlane.Pa`	`PureU1.VectorLikeEvenPlane.evenShiftSnd` `PureU1.VectorLikeEvenPlane.evenShiftFst` `ACCSystemCharges.Charges` `PureU1.PureU1Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `PureU1.accCubeTriLinSymm` `PureU1.VectorLikeEvenPlane.P` `PureU1.VectorLikeEvenPlane.basis!AsCharges`	—	`PureU1.VectorLikeEvenPlane.span_basis_swap!` `line_in_cubic_P_P_P!` `lineInCubicPerm_self` `lineInCubicPerm_permute` `TriLinearSymm.map_smul₃` `TriLinearSymm.map_add₃`
`lineInCubicPerm_vectorLike` 📖	mathematical	`LineInCubicPerm` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystem.Sols.toQuadSols`	`PureU1.VectorLikeEven` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear`	—	`PureU1.ConstAbs.boundary_value_even` `lineInCubicPerm_constAbs`
`lineInCubic_expand` 📖	mathematical	`LineInCubic` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `PureU1.VectorLikeEvenPlane.Pa`	`ACCSystemCharges.Charges` `PureU1.PureU1Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `PureU1.accCubeTriLinSymm` `PureU1.VectorLikeEvenPlane.P` `PureU1.VectorLikeEvenPlane.P!`	—	`PureU1.VectorLikeEvenPlane.P!_accCube` `PureU1.VectorLikeEvenPlane.P_accCube` `HomogeneousCubic.map_smul` `TriLinearSymm.map_smul₁` `TriLinearSymm.map_smul₂` `TriLinearSymm.map_smul₃` `TriLinearSymm.toCubic_add`
`line_in_cubic_P_P_P!` 📖	mathematical	`LineInCubic` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemCharges.chargesAddCommMonoid` `PureU1.VectorLikeEvenPlane.P` `PureU1.VectorLikeEvenPlane.P!`	`PureU1.PureU1Charges` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `PureU1.accCubeTriLinSymm`	—	`lineInCubic_expand`

---

← Back to Index