Documentation Verification Report

LineInCubic

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

Statistics

Metric	Count
Definitions `LineInCubic`, `LineInCubicPerm`	2
Theorems `P_P_P!_accCube'`, `lineInCubicPerm_constAbs`, `lineInCubicPerm_last_cond`, `lineInCubicPerm_last_perm`, `lineInCubicPerm_permute`, `lineInCubicPerm_self`, `lineInCubicPerm_swap`, `lineInCubicPerm_zero`, `lineInCubic_expand`, `line_in_cubic_P_P_P!`	10
Total	12

PureU1.Odd

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.VectorLikeOddPlane.Pa`	`ACCSystemCharges.Charges` `PureU1.PureU1Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `PureU1.accCubeTriLinSymm` `PureU1.VectorLikeOddPlane.P` `PureU1.VectorLikeOddPlane.basis!AsCharges` `PureU1.VectorLikeOddPlane.oddShiftFst` `PureU1.VectorLikeOddPlane.oddShiftSnd` `PureU1.VectorLikeOddPlane.oddShiftZero`	—	`PureU1.VectorLikeOddPlane.P_P_P!_accCube` `PureU1.VectorLikeOddPlane.Pa_oddShiftShiftZero` `PureU1.VectorLikeOddPlane.P_oddFst` `PureU1.VectorLikeOddPlane.Pa_oddShiftShiftSnd` `PureU1.VectorLikeOddPlane.Pa_oddShiftShiftFst` `PureU1.VectorLikeOddPlane.oddShiftShiftSnd_eq_oddShiftSnd` `PureU1.VectorLikeOddPlane.oddShiftShiftZero_eq_oddShiftZero`
`lineInCubicPerm_constAbs` 📖	mathematical	`LineInCubicPerm`	`PureU1.ConstAbs` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1`	—	`PureU1.linesInPlane_constAbs` `lineInCubicPerm_last_perm`
`lineInCubicPerm_last_cond` 📖	mathematical	`LineInCubicPerm`	`PureU1.LineInPlaneProp` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `PureU1.VectorLikeOddPlane.oddShiftSnd` `PureU1.VectorLikeOddPlane.oddShiftFst` `PureU1.VectorLikeOddPlane.oddShiftZero`	—	`PureU1.VectorLikeOddPlane.span_basis` `lineInCubicPerm_swap` `P_P_P!_accCube'`
`lineInCubicPerm_last_perm` 📖	mathematical	`LineInCubicPerm`	`PureU1.LineInPlaneCond`	—	`PureU1.Prop_three` `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_self` 📖	mathematical	`LineInCubicPerm`	`LineInCubic`	—	—
`lineInCubicPerm_swap` 📖	mathematical	`LineInCubicPerm` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `PureU1.VectorLikeOddPlane.Pa`	`PureU1.VectorLikeOddPlane.oddShiftSnd` `PureU1.VectorLikeOddPlane.oddShiftFst` `ACCSystemCharges.Charges` `PureU1.PureU1Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `PureU1.accCubeTriLinSymm` `PureU1.VectorLikeOddPlane.P` `PureU1.VectorLikeOddPlane.basis!AsCharges`	—	`PureU1.VectorLikeOddPlane.span_basis_swap!` `line_in_cubic_P_P_P!` `lineInCubicPerm_self` `lineInCubicPerm_permute` `TriLinearSymm.map_smul₃` `TriLinearSymm.map_add₃`
`lineInCubicPerm_zero` 📖	mathematical	`LineInCubicPerm`	`ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemLinear.linSolsAddCommGroup`	—	`PureU1.ConstAbs.boundary_value_odd` `lineInCubicPerm_constAbs`
`lineInCubic_expand` 📖	mathematical	`LineInCubic` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemCharges.chargesAddCommMonoid` `PureU1.VectorLikeOddPlane.P` `PureU1.VectorLikeOddPlane.P!`	`PureU1.PureU1Charges` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `PureU1.accCubeTriLinSymm`	—	`PureU1.VectorLikeOddPlane.P!_accCube` `PureU1.VectorLikeOddPlane.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.VectorLikeOddPlane.P` `PureU1.VectorLikeOddPlane.P!`	`PureU1.PureU1Charges` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `PureU1.accCubeTriLinSymm`	—	`lineInCubic_expand`

---

← Back to Index