Documentation Verification Report

Parameterization

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

Statistics

Metric	Count
Definitions `GenericCase`, `SpecialCase`, `parameterization`, `parameterizationAsLinear`	4
Theorems `anomalyFree_param`, `genericCase_exists`, `generic_case`, `generic_or_special`, `parameterizationAsLinear_val`, `parameterizationCharge_cube`, `specialCase_exists`, `special_case`, `special_case_lineInCubic`, `special_case_lineInCubic_perm`	10
Total	14

PureU1.Even

Definitions

Name	Category	Theorems
`GenericCase` 📖	MathDef	2 math math: `generic_or_special`, `genericCase_exists`
`SpecialCase` 📖	MathDef	2 math math: `specialCase_exists`, `generic_or_special`
`parameterization` 📖	CompOp	1 math math: `generic_case`
`parameterizationAsLinear` 📖	CompOp	2 math math: `parameterizationCharge_cube`, `parameterizationAsLinear_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anomalyFree_param` 📖	mathematical	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemCharges.chargesAddCommMonoid` `PureU1.VectorLikeEvenPlane.P` `PureU1.VectorLikeEvenPlane.P!`	`PureU1.PureU1Charges` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `PureU1.accCubeTriLinSymm`	—	`ACCSystem.Sols.cubicSol` `PureU1.VectorLikeEvenPlane.P!_accCube` `PureU1.VectorLikeEvenPlane.P_accCube` `TriLinearSymm.toCubic_add`
`genericCase_exists` 📖	mathematical	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemCharges.chargesAddCommMonoid` `PureU1.VectorLikeEvenPlane.P` `PureU1.VectorLikeEvenPlane.P!`	`GenericCase`	—	`PureU1.VectorLikeEvenPlane.Pa_eq`
`generic_case` 📖	mathematical	`GenericCase`	`parameterization`	—	`PureU1.VectorLikeEvenPlane.span_basis` `parameterizationCharge_cube` `parameterization.eq_1` `ACCSystem.Sols.ext` `parameterizationAsLinear_val` `anomalyFree_param`
`generic_or_special` 📖	mathematical	—	`GenericCase` `SpecialCase`	—	`PureU1.VectorLikeEvenPlane.span_basis` `genericCase_exists` `specialCase_exists`
`parameterizationAsLinear_val` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `parameterizationAsLinear` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `PureU1.PureU1Charges` `TriLinearSymm` `TriLinearSymm.instFun` `PureU1.accCubeTriLinSymm` `PureU1.VectorLikeEvenPlane.P!` `PureU1.VectorLikeEvenPlane.P`	—	`parameterizationAsLinear.eq_1` `PureU1.VectorLikeEvenPlane.P'_val` `PureU1.VectorLikeEvenPlane.P!'_val`
`parameterizationCharge_cube` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `PureU1.PureU1Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `PureU1.accCube` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `parameterizationAsLinear`	—	`parameterizationAsLinear_val` `HomogeneousCubic.map_smul` `TriLinearSymm.toCubic_add` `PureU1.VectorLikeEvenPlane.P_accCube` `PureU1.VectorLikeEvenPlane.P!_accCube` `TriLinearSymm.map_smul₁` `TriLinearSymm.map_smul₂` `TriLinearSymm.map_smul₃`
`specialCase_exists` 📖	mathematical	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemCharges.chargesAddCommMonoid` `PureU1.VectorLikeEvenPlane.P` `PureU1.VectorLikeEvenPlane.P!` `PureU1.PureU1Charges` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `PureU1.accCubeTriLinSymm`	`SpecialCase`	—	`PureU1.VectorLikeEvenPlane.Pa_eq`
`special_case` 📖	mathematical	`SpecialCase` `ACCSystem.Sols` `PureU1` `ACCSystemGroupAction.group` `PureU1.FamilyPermutations` `ACCSystemGroupAction.instGroupGroup` `ACCSystemGroupAction.solAction`	`ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule` `PureU1.VectorLikeEvenPlane.basis` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols`	—	`lineInCubicPerm_in_plane` `special_case_lineInCubic_perm`
`special_case_lineInCubic` 📖	mathematical	`SpecialCase`	`LineInCubic` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystem.Sols.toQuadSols`	—	`TriLinearSymm.toCubic_add` `HomogeneousCubic.map_smul` `PureU1.VectorLikeEvenPlane.P_accCube` `PureU1.VectorLikeEvenPlane.P!_accCube` `TriLinearSymm.map_smul₁` `TriLinearSymm.map_smul₂` `TriLinearSymm.map_smul₃` `anomalyFree_param`
`special_case_lineInCubic_perm` 📖	mathematical	`SpecialCase` `ACCSystem.Sols` `PureU1` `ACCSystemGroupAction.group` `PureU1.FamilyPermutations` `ACCSystemGroupAction.instGroupGroup` `ACCSystemGroupAction.solAction`	`LineInCubicPerm` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `ACCSystem.Sols.toQuadSols`	—	`special_case_lineInCubic`

---

← Back to Index