Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `PureU1`, `PureU1Charges`, `accCube`, `accCubeTriLinSymm`, `accGrav`, `pureU1EqCharges`	6
Theorems `PureU1Charges_numberCharges`, `accCubeTriLinSymm_toFun_apply_apply`, `accCube_explicit`, `sum_of_anomaly_free_linear`, `sum_of_charges`, `PureU1_cubicACC_apply`, `PureU1_linearACCs`, `PureU1_numberCharges`, `PureU1_numberLinear`, `PureU1_numberQuadratic`, `PureU1_quadraticACCs`, `pureU1_anomalyFree_ext`, `pureU1_cube`, `pureU1_last`, `pureU1_linear`	15
Total	21

PureU1

Definitions

Name	Category	Theorems
`PureU1Charges` 📖	CompOp	39 math math: `accCubeTriLinSymm_toFun_apply_apply`, `Even.line_in_cubic_P_P_P!`, `Odd.parameterizationAsLinear_val`, `Even.lineInCubicPerm_swap`, `PureU1Charges_numberCharges`, `VectorLikeOddPlane.basis_linearACC`, `Even.parameterizationCharge_cube`, `VectorLikeEvenPlane.basis!_linearACC`, `Odd.P_P_P!_accCube'`, `VectorLikeOddPlane.P_accCube`, `VectorLikeOddPlane.P!_linearACC`, `VectorLikeEvenPlane.P_linearACC`, `ConstAbsSorted.not_hasBoundary_grav`, `Even.anomalyFree_param`, `VectorLikeOddPlane.P_P_P!_accCube`, `Odd.line_in_cubic_P_P_P!`, `Even.parameterizationAsLinear_val`, `VectorLikeEvenPlane.basis_accCube`, `VectorLikeEvenPlane.P_P_P!_accCube`, `accCube_explicit`, `Odd.anomalyFree_param`, `Odd.lineInCubic_expand`, `ConstAbsSorted.boundary_accGrav''`, `VectorLikeEvenPlane.P_accCube`, `accCube_invariant`, `VectorLikeOddPlane.P_linearACC`, `VectorLikeEvenPlane.basis!_accCube`, `accGrav_invariant`, `VectorLikeEvenPlane.P!_accCube`, `VectorLikeOddPlane.P!_accCube`, `Odd.parameterizationCharge_cube`, `PureU1_cubicACC_apply`, `Odd.lineInCubicPerm_swap`, `VectorLikeEvenPlane.P_P!_P!_accCube`, `VectorLikeOddPlane.basis!_linearACC`, `Even.P_P_P!_accCube'`, `Even.lineInCubic_expand`, `ConstAbsSorted.boundary_accGrav'`, `VectorLikeEvenPlane.basis_linearACC`
`accCube` 📖	CompOp	10 math math: `Even.parameterizationCharge_cube`, `VectorLikeOddPlane.P_accCube`, `VectorLikeEvenPlane.basis_accCube`, `accCube_explicit`, `VectorLikeEvenPlane.P_accCube`, `accCube_invariant`, `VectorLikeEvenPlane.basis!_accCube`, `VectorLikeEvenPlane.P!_accCube`, `VectorLikeOddPlane.P!_accCube`, `Odd.parameterizationCharge_cube`
`accCubeTriLinSymm` 📖	CompOp	16 math math: `accCubeTriLinSymm_toFun_apply_apply`, `Even.line_in_cubic_P_P_P!`, `Odd.parameterizationAsLinear_val`, `Even.lineInCubicPerm_swap`, `Odd.P_P_P!_accCube'`, `Even.anomalyFree_param`, `VectorLikeOddPlane.P_P_P!_accCube`, `Odd.line_in_cubic_P_P_P!`, `Even.parameterizationAsLinear_val`, `VectorLikeEvenPlane.P_P_P!_accCube`, `Odd.anomalyFree_param`, `Odd.lineInCubic_expand`, `Odd.lineInCubicPerm_swap`, `VectorLikeEvenPlane.P_P!_P!_accCube`, `Even.P_P_P!_accCube'`, `Even.lineInCubic_expand`
`accGrav` 📖	CompOp	12 math math: `VectorLikeOddPlane.basis_linearACC`, `VectorLikeEvenPlane.basis!_linearACC`, `PureU1_linearACCs`, `VectorLikeOddPlane.P!_linearACC`, `VectorLikeEvenPlane.P_linearACC`, `ConstAbsSorted.not_hasBoundary_grav`, `ConstAbsSorted.boundary_accGrav''`, `VectorLikeOddPlane.P_linearACC`, `accGrav_invariant`, `VectorLikeOddPlane.basis!_linearACC`, `ConstAbsSorted.boundary_accGrav'`, `VectorLikeEvenPlane.basis_linearACC`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`PureU1Charges_numberCharges` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `PureU1Charges`	—	—
`accCubeTriLinSymm_toFun_apply_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `PureU1Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `accCubeTriLinSymm`	—	—
`accCube_explicit` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `PureU1Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `accCube`	—	`accCube.eq_1` `TriLinearSymm.toCubic.eq_1` `accCubeTriLinSymm.eq_1`
`sum_of_anomaly_free_linear` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemLinear.LinSols` `ACCSystemLinear.linSolsAddCommMonoid`	—	—
`sum_of_charges` 📖	mathematical	—	`ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemCharges.chargesAddCommMonoid`	—	—

(root)

Definitions

Name	Category	Theorems
`PureU1` 📖	CompOp	69 math math: `PureU1.Odd.lineInCubicPerm_constAbs`, `PureU1.Odd.parameterizationAsLinear_val`, `PureU1.VectorLikeOddPlane.basis_val`, `PureU1.VectorLikeOddPlane.basis!_val`, `PureU1_quadraticACCs`, `PureU1.VectorLikeOddPlane.basis!_linear_independent`, `PureU1.VectorLikeEvenPlane.P_evenSnd_evenFst`, `PureU1.sort_perm`, `PureU1.sort_apply`, `PureU1.Even.parameterizationCharge_cube`, `pureU1_cube`, `PureU1.Three.three_sol_zero`, `PureU1.lineInPlaneCond_perm`, `PureU1.FamilyPermutations_anomalyFreeLinear_apply`, `pureU1_linear`, `PureU1.VectorLikeEvenPlane.P'_val`, `PureU1_linearACCs`, `PureU1_numberLinear`, `PureU1.BasisLinear.sum_of_vectors`, `PureU1.VectorLikeEvenPlane.basis_val`, `PureU1.sum_of_anomaly_free_linear`, `PureU1.VectorLikeOddPlane.span_basis`, `PureU1.VectorLikeOddPlane.basisa_card`, `PureU1.FamilyPermutations_charges_apply`, `PureU1.BasisLinear.asLinSols_val`, `PureU1.Odd.lineInCubicPerm_permute`, `PureU1.Three.cube_for_linSol'`, `PureU1.Odd.lineInCubicPerm_last_cond`, `PureU1.Odd.lineInCubicPerm_zero`, `PureU1.Even.parameterizationAsLinear_val`, `PureU1.VectorLikeEvenPlane.basis!_linear_independent`, `PureU1.VectorLikeOddPlane.Pa'_P'_P!'`, `PureU1.BasisLinear.finrank_AnomalyFreeLinear`, `PureU1.VectorLikeEvenPlane.P!'_val`, `PureU1.VectorLikeEvenPlane.P!_in_span`, `PureU1.linesInPlane_eq_sq`, `PureU1.Even.special_case_lineInCubic`, `PureU1.VectorLikeOddPlane.basisa_linear_independent`, `PureU1.Even.lineInCubicPerm_permute`, `PureU1.accCube_invariant`, `PureU1.One.solEqZero`, `PureU1_numberCharges`, `PureU1.accGrav_invariant`, `PureU1.VectorLikeEvenPlane.Pa'_P'_P!'`, `PureU1.chargeMap_apply`, `PureU1.Even.lineInCubicPerm_last_cond`, `PureU1.VectorLikeEvenPlane.smul_basis!AsCharges_in_span`, `PureU1.Three.cube_for_linSol`, `PureU1.linesInPlane_constAbs`, `PureU1.constAbs_perm`, `PureU1.VectorLikeEvenPlane.basisa_card`, `PureU1.VectorLikeOddPlane.P!'_val`, `PureU1.lineInPlaneCond_eq_last`, `PureU1_numberQuadratic`, `PureU1.VectorLikeEvenPlane.basis!_val`, `PureU1.Odd.parameterizationCharge_cube`, `PureU1_cubicACC_apply`, `PureU1.VectorLikeEvenPlane.basisa_linear_independent`, `PureU1.VectorLikeOddPlane.P'_val`, `PureU1.BasisLinear.instFiniteRatLinSolsSucc`, `pureU1_last`, `PureU1.sortAFL_val`, `PureU1.VectorLikeEvenPlane.span_basis`, `PureU1.sum_of_charges`, `PureU1.ConstAbsSorted.is_zero`, `PureU1.VectorLikeOddPlane.basis_linear_independent`, `PureU1.VectorLikeEvenPlane.basis_linear_independent`, `PureU1.ConstAbsSorted.boundary_accGrav'`, `PureU1.Odd.special_case_lineInCubic`
`pureU1EqCharges` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`PureU1_cubicACC_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `PureU1.PureU1Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystem.cubicACC` `PureU1`	—	—
`PureU1_linearACCs` 📖	mathematical	—	`ACCSystemLinear.linearACCs` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemCharges.Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `PureU1.accGrav`	—	—
`PureU1_numberCharges` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1`	—	—
`PureU1_numberLinear` 📖	mathematical	—	`ACCSystemLinear.numberLinear` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1`	—	—
`PureU1_numberQuadratic` 📖	mathematical	—	`ACCSystemQuad.numberQuadratic` `ACCSystem.toACCSystemQuad` `PureU1`	—	—
`PureU1_quadraticACCs` 📖	mathematical	—	`ACCSystemQuad.quadraticACCs` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemCharges.Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule`	—	—
`pureU1_anomalyFree_ext` 📖	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1`	—	—	`ACCSystemLinear.LinSols.ext` `pureU1_last`
`pureU1_cube` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols`	—	`PureU1.accCube_explicit` `ACCSystem.Sols.cubicSol`
`pureU1_last` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1`	—	`pureU1_linear`
`pureU1_linear` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1`	—	`ACCSystemLinear.LinSols.linearSol`

---

← Back to Index