Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `ACCSystem`, `Hom`, `anomalyFree`, `charges`, `comp`, `IsSolution`, `Sols`, `toQuadSols`, `cubicACC`, `solsIncl`, `solsInclLinSols`, `solsInclQuadSols`, `solsMulAction`, `toACCSystemQuad`, `ACCSystemCharges`, `Charges`, `ChargesAddCommGroup`, `chargesAddCommMonoid`, `chargesModule`, `numberCharges`, `ACCSystemChargesMk`, `ACCSystemLinear`, `LinSols`, `val`, `linSolsAddCommGroup`, `linSolsAddCommMonoid`, `linSolsIncl`, `linSolsModule`, `linearACCs`, `numberLinear`, `toACCSystemCharges`, `ACCSystemQuad`, `QuadSols`, `toLinSols`, `linSolsInclQuadSolsZero`, `numberQuadratic`, `quadSolsIncl`, `quadSolsInclLinSols`, `quadSolsMulAction`, `quadraticACCs`, `toACCSystemLinear`	41
Theorems `commute`, `cubicSol`, `ext`, `solsInclLinSols_injective`, `solsInclQuadSols_injective`, `solsIncl_injective`, `chargesAddCommMonoid_add`, `chargesAddCommMonoid_nsmul`, `chargesAddCommMonoid_zero_den`, `chargesAddCommMonoid_zero_num`, `chargesModule_smul`, `instFiniteRatCharges`, `ext`, `ext_iff`, `linearSol`, `linSolsAddCommMonoid_add_val`, `linSolsAddCommMonoid_nsmul_val`, `linSolsAddCommMonoid_zero_val`, `linSolsIncl_injective`, `linSolsModule_smul_val`, `ext`, `ext_iff`, `quadSol`, `quadSolsInclLinSols_injective`, `quadSolsIncl_injective`	25
Total	66
⚠️ With sorry `linSolsIncl_injective`	1

ACCSystem

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—
`IsSolution` 📖	MathDef	2 math math: `SMRHN.SM.PlaneSeven.B_sum_is_sol`, `SMRHN.SM.seven_dim_plane_exists`
`Sols` 📖	CompData	24 math math: `MSSMACC.AnomalyFreePerp.toSol_inQuadCube`, `solsIncl_injective`, `MSSMACC.AnomalyFreePerp.inQuadCubeToSol_proj`, `MSSMACC.AnomalyFreePerp.inLineEqTo_smul`, `Hom.commute`, `MSSMACC.AnomalyFreePerp.toSol_surjective`, `MSSMACC.AnomalyFreePerp.toSolNS_proj`, `SMRHN.PlusU1.QuadSolToSol.generic_on_AF`, `MSSMACC.AnomalyFreePerp.inQuadToSol_proj`, `MSSMACC.AnomalyFreePerp.toSol_inLineEq`, `SMRHN.PlusU1.QuadSolToSol.generic_on_AF_α₁_ne_zero`, `ACCSystemGroupAction.linSolRep_solAction_commute`, `solsInclQuadSols_injective`, `ACCSystemGroupAction.quadSolAction_solAction_commute`, `SMRHN.PlusU1.quadSolToSolInv_rightInverse`, `SMRHN.PlusU1.quadSolToSolInv_generic`, `MSSMACC.AnomalyFreePerp.inLineEqToSol_proj`, `MSSMACC.AnomalyFreePerp.inQuadCubeToSol_smul`, `MSSMACC.AnomalyFreePerp.inQuadToSol_smul`, `MSSMACC.AnomalyFreePerp.toSol_inQuad`, `MSSMACC.AnomalyFreePerp.toSol_toSolNSProj`, `ACCSystemGroupAction.rep_solAction_commute`, `SMRHN.PlusU1.quadSolToSol_surjective`, `solsInclLinSols_injective`
`cubicACC` 📖	CompOp	10 math math: `SM.SMNoGrav_cubicACC_apply`, `MSSMACC_cubicACC_apply`, `ACCSystemGroupAction.cubicInvariant`, `PureU1.Three.cube_for_linSol'`, `SMRHN.SMNoGrav_cubicACC_apply`, `SMRHN.PlusU1_cubicACC_apply`, `PureU1.Three.cube_for_linSol`, `SMRHN.SM_cubicACC_apply`, `PureU1_cubicACC_apply`, `Sols.cubicSol`
`solsIncl` 📖	CompOp	3 math math: `solsIncl_injective`, `Hom.commute`, `ACCSystemGroupAction.rep_solAction_commute`
`solsInclLinSols` 📖	CompOp	2 math math: `ACCSystemGroupAction.linSolRep_solAction_commute`, `solsInclLinSols_injective`
`solsInclQuadSols` 📖	CompOp	2 math math: `solsInclQuadSols_injective`, `ACCSystemGroupAction.quadSolAction_solAction_commute`
`solsMulAction` 📖	CompOp	13 math math: `solsIncl_injective`, `MSSMACC.AnomalyFreePerp.inLineEqTo_smul`, `Hom.commute`, `SMRHN.PlusU1.QuadSolToSol.generic_on_AF`, `SMRHN.PlusU1.QuadSolToSol.generic_on_AF_α₁_ne_zero`, `ACCSystemGroupAction.linSolRep_solAction_commute`, `solsInclQuadSols_injective`, `ACCSystemGroupAction.quadSolAction_solAction_commute`, `SMRHN.PlusU1.quadSolToSolInv_generic`, `MSSMACC.AnomalyFreePerp.inQuadCubeToSol_smul`, `MSSMACC.AnomalyFreePerp.inQuadToSol_smul`, `ACCSystemGroupAction.rep_solAction_commute`, `solsInclLinSols_injective`
`toACCSystemQuad` 📖	CompOp	229 math math: `MSSMACC.α₃_proj`, `PureU1.Odd.lineInCubicPerm_constAbs`, `SMRHN.SMNoGrav_quadraticACCs`, `ACCSystemGroupAction.rep_linSolRep_commute`, `SM.SMNoGrav_linearACCs`, `solsIncl_injective`, `PureU1.Odd.parameterizationAsLinear_val`, `SMRHN.SM.PlaneSeven.basis_linear_independent`, `SMRHN.PlusU1.QuadSol.toQuadInv_fst`, `PureU1.VectorLikeOddPlane.basis_val`, `PureU1.VectorLikeOddPlane.basis!_val`, `PureU1_quadraticACCs`, `MSSMACC.AnomalyFreePerp.perpB₃`, `SMRHN.PlusU1_numberQuadratic`, `PureU1.VectorLikeOddPlane.basis!_linear_independent`, `SM.SMNoGrav_numberQuadratic`, `PureU1.VectorLikeEvenPlane.P_evenSnd_evenFst`, `SMRHN.PlusU1.BL.on_cubeTriLin`, `MSSMACC.lineCube_smul`, `PureU1.sort_perm`, `PureU1.sort_apply`, `SM.SMNoGrav.One.accGrav_Q_neq_zero`, `SMRHN.SM_numberCharges`, `SMRHN.PlusU1.Y.on_quadBiLin_AFL`, `MSSMACC.AnomalyFreePerp.inQuadSolProp_iff_proj_inQuadProp`, `SMRHN.SMNoGrav_linearACCs`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube`, `SM.SMNoGrav.SU3Sol`, `PureU1.Even.parameterizationCharge_cube`, `pureU1_cube`, `PureU1.Three.three_sol_zero`, `PureU1.lineInPlaneCond_perm`, `SMRHN.PlusU1.BL.addQuad_zero`, `PureU1.FamilyPermutations_anomalyFreeLinear_apply`, `SMRHN.SM_numberQuadratic`, `pureU1_linear`, `SMRHN.SM_linearACCs`, `SMRHN.PlusU1.QuadSol.toQuadInv_generic`, `SMRHN.PlusU1_linearACCs`, `SMRHN.PlusU1.Y.addQuad_zero`, `SMRHN.SM.cubeSol`, `SMRHN.SM_numberLinear`, `Hom.commute`, `PureU1.VectorLikeEvenPlane.P'_val`, `PureU1_linearACCs`, `MSSMACC.proj_val`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_eq_planeY₃B₃_on_α`, `MSSMACC_numberQuadratic`, `SMRHN.PlusU1.quadSolToSolInv_α₁_α₂_neq_zero`, `SMRHN.PlusU1.ElevenPlane.on_accQuad`, `SMRHN.PlusU1.eleven_dim_plane_of_no_sols_exists`, `ACCSystemGroupAction.quadInvariant`, `ACCSystemGroupAction.cubicInvariant`, `SM.SMNoGrav_quadraticACCs`, `MSSMACC_numberLinear`, `SMRHN.PlusU1.BL₁_val`, `SMRHN.PlusU1.Y_val`, `MSSMACC.planeY₃B₃_val`, `SMRHN.SM.gravSol`, `MSSMACC.α₁_proj`, `PureU1_numberLinear`, `PureU1.BasisLinear.sum_of_vectors`, `PureU1.VectorLikeEvenPlane.basis_val`, `PureU1.sum_of_anomaly_free_linear`, `SMRHN.SM.SU3Sol`, `PureU1.VectorLikeOddPlane.span_basis`, `MSSMACC.doublePoint_Y₃_B₃`, `MSSMACC.α₂_proj`, `SMRHN.PlusU1.BL.add_quad`, `PureU1.VectorLikeOddPlane.basisa_card`, `PureU1.FamilyPermutations_charges_apply`, `PureU1.BasisLinear.asLinSols_val`, `SMRHN.PlusU1.Y.on_quadBiLin`, `MSSMACC.AnomalyFreePerp.linEqPropSol_iff_proj_linEqProp`, `PureU1.Odd.lineInCubicPerm_permute`, `SMRHN.SM_quadraticACCs`, `SM.SMNoGrav.One.accGravSatisfied`, `PureU1.Three.cube_for_linSol'`, `MSSMACC.B₃_val`, `SMRHN.PlusU1.BL.on_quadBiLin_AFL`, `PureU1.Odd.lineInCubicPerm_last_cond`, `PureU1.Odd.lineInCubicPerm_zero`, `PureU1.Even.parameterizationAsLinear_val`, `SM.SMNoGrav.One.E_zero_iff_Q_zero`, `SMRHN.SMNoGrav_numberQuadratic`, `MSSMACC.planeY₃B₃_cubic`, `SMRHN.SM.PlaneSeven.B_in_accCube`, `PureU1.VectorLikeEvenPlane.basis!_linear_independent`, `MSSMACC.lineY₃B₃_doublePoint`, `SMRHN.PlusU1.Y.on_cubeTriLin`, `MSSMACC.AnomalyFreeMk_val`, `PureU1.VectorLikeOddPlane.Pa'_P'_P!'`, `SMRHN.SM.PlaneSeven.B_sum_is_sol`, `PureU1.BasisLinear.finrank_AnomalyFreeLinear`, `SM.SMNoGrav_numberLinear`, `SMRHN.PlusU1.QuadSol.genericToQuad_neq_zero`, `ACCSystemGroupAction.linSolRep_solAction_commute`, `MSSMACC.AnomalyFreePerp.perpY₃`, `SMRHN.PlusU1.Y.on_cubeTriLin'`, `PureU1.VectorLikeEvenPlane.P!'_val`, `SMRHN.SMNoGrav.SU2Sol`, `MSSMACC.planeY₃B₃_smul`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_AF`, `MSSMACC.Y₃_val`, `ACCSystemGroupAction.linSolRep_quadSolAction_commute`, `SMRHN.PlusU1.gravSol`, `SMRHN.PlusU1.QuadSol.α₂_AFQ`, `PureU1.VectorLikeEvenPlane.P!_in_span`, `MSSMACC.lineQuadAFL_quad`, `MSSMACC.planeY₃B₃_quad`, `PureU1.linesInPlane_eq_sq`, `SMRHN.PlusU1.Y.add_AF_cube`, `SMRHN.PlusU1.BL_val`, `PureU1.Even.special_case_lineInCubic`, `MSSMACC.lineQuad_cube`, `PureU1.VectorLikeOddPlane.basisa_linear_independent`, `MSSMACC.cube_proj_proj_B₃`, `MSSMACC.lineQuad_smul`, `solsInclQuadSols_injective`, `MSSMACC.cube_proj_proj_Y₃`, `ACCSystemGroupAction.quadSolAction_solAction_commute`, `SMRHN.PlusU1.quadSolToSolInv_rightInverse`, `MSSMACC.lineCube_quad`, `SM.SMNoGrav.SU2Sol`, `PureU1.Even.lineInCubicPerm_permute`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `MSSMACC_linearACCs`, `PureU1.accCube_invariant`, `SMRHN.PlusU1.QuadSol.genericToQuad_on_quad`, `SM.SMNoGrav_numberCharges`, `PureU1.One.solEqZero`, `PureU1_numberCharges`, `SMRHN.SM.SU2Sol`, `SMRHN.PlusU1.Y.add_AFL_quad`, `MSSMACC.doublePoint_Y₃_Y₃`, `PureU1.accGrav_invariant`, `SMRHN.PlusU1.BL.add_AFL_cube`, `SMRHN.PlusU1.quadSolToSolInv_generic`, `PureU1.VectorLikeEvenPlane.Pa'_P'_P!'`, `PureU1.chargeMap_apply`, `PureU1.Even.lineInCubicPerm_last_cond`, `PureU1.VectorLikeEvenPlane.smul_basis!AsCharges_in_span`, `MSSMACC.quadSol`, `SMRHN.PlusU1.YYsol`, `SMRHN.PlusU1.ElevenPlane.basis_linear_independent`, `SMRHN.PlusU1.ElevenPlane.Bi_sum_quad`, `ACCSystemGroupAction.linearInvariant`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `PureU1.Three.cube_for_linSol`, `SMRHN.PlusU1.Y.add_AFL_cube`, `SMRHN.PlusU1.quadSolToSolInv_1`, `PureU1.Even.special_case_lineInCubic_perm`, `PureU1.linesInPlane_constAbs`, `SMRHN.PlusU1.quadSolToSolInv_special`, `MSSMACC_quadraticACCs`, `SMRHN.PlusU1.QuadSol.toQuad_surjective`, `SMRHN.PlusU1.QuadSol.toQuad_rightInverse`, `MSSMACC.quad_self_proj`, `PureU1.constAbs_perm`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_cube`, `SMRHN.PlusU1_quadraticACCs`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `SMRHN.SMNoGrav_numberCharges`, `SMRHN.PlusU1.Y₁_val`, `PureU1.VectorLikeEvenPlane.basisa_card`, `SM.SMNoGrav.One.linearParametersQENeqZero.grav`, `PureU1.VectorLikeOddPlane.P!'_val`, `PureU1.lineInPlaneCond_eq_last`, `SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero`, `PureU1_numberQuadratic`, `PureU1.Odd.special_case_lineInCubic_perm`, `SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ`, `MSSMACC.lineY₃B₃Charges_cubic`, `PureU1.VectorLikeEvenPlane.basis!_val`, `SMRHN.PlusU1.cubeSol`, `PureU1.Odd.parameterizationCharge_cube`, `SMRHN.PlusU1.SU2Sol`, `MSSMACC.lineY₃B₃Charges_quad`, `MSSMACC.AnomalyFreePerp.inCubeSolProp_iff_proj_inCubeProp`, `SMRHN.SMNoGrav.SU3Sol`, `MSSMACC.quad_B₃_proj`, `SMRHN.SM.seven_dim_plane_exists`, `SM.SMNoGrav.One.linearParameters.asLinear_val`, `SMRHN.PlusU1.exists_plane_exists_basis`, `MSSMACC_numberCharges`, `PureU1.Even.special_case`, `PureU1.VectorLikeEvenPlane.basisa_linear_independent`, `SMRHN.SMNoGrav.cubeSol`, `SMRHN.PlusU1.BL.add_AFL_quad`, `ACCSystemGroupAction.rep_solAction_commute`, `MSSMACC.cube_proj_proj_self`, `SMRHN.PlusU1.Y.add_AFQ_cube`, `PureU1.VectorLikeOddPlane.P'_val`, `ACCSystemGroupAction.linSolRep_apply_apply_val`, `SMRHN.PlusU1_numberCharges`, `MSSMACC.cube_proj`, `PureU1.BasisLinear.instFiniteRatLinSolsSucc`, `pureU1_last`, `SMRHN.PlusU1_numberLinear`, `MSSMACC.doublePoint_B₃_B₃`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `SM.SMNoGrav.cubeSol`, `PureU1.Odd.special_case`, `SMRHN.PlusU1.BL.on_quadBiLin`, `SMRHN.PlusU1.Y.on_cubeTriLin_AFL`, `SMRHN.PlusU1.quadSolToSol_surjective`, `SMRHN.PlusU1.quadSolToSolInv_α₁_α₂_zero`, `PureU1.sortAFL_val`, `PureU1.VectorLikeEvenPlane.span_basis`, `PureU1.sum_of_charges`, `SMRHN.PlusU1.BL.on_cubeTriLin_AFL`, `SMRHN.SMNoGrav_numberLinear`, `PureU1.ConstAbsSorted.is_zero`, `Sols.cubicSol`, `ACCSystemGroupAction.rep_quadSolAction_commute`, `SMRHN.PlusU1.SU3Sol`, `SMRHN.PlusU1.QuadSol.toQuadInv_α₁_α₂`, `PureU1.VectorLikeOddPlane.basis_linear_independent`, `SMRHN.PlusU1.Y.add_quad`, `MSSMACC.quad_proj`, `solsInclLinSols_injective`, `PureU1.VectorLikeEvenPlane.basis_linear_independent`, `PureU1.ConstAbsSorted.boundary_accGrav'`, `PureU1.Odd.special_case_lineInCubic`, `SMRHN.PlusU1.quadSol`, `MSSMACC.lineCube_cube`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`solsInclLinSols_injective` 📖	mathematical	—	`Sols` `ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `toACCSystemQuad` `solsMulAction` `ACCSystemLinear.linSolsAddCommGroup` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule` `solsInclLinSols`	—	`ACCSystemQuad.quadSolsInclLinSols_injective` `solsInclQuadSols_injective`
`solsInclQuadSols_injective` 📖	mathematical	—	`Sols` `ACCSystemQuad.QuadSols` `toACCSystemQuad` `solsMulAction` `ACCSystemQuad.quadSolsMulAction` `solsInclQuadSols`	—	`Sols.ext`
`solsIncl_injective` 📖	mathematical	—	`Sols` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `toACCSystemQuad` `solsMulAction` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `solsIncl`	—	`ACCSystemQuad.quadSolsIncl_injective` `solsInclQuadSols_injective`

ACCSystem.Hom

Definitions

Name	Category	Theorems
`anomalyFree` 📖	CompOp	1 math math: `commute`
`charges` 📖	CompOp	1 math math: `commute`
`comp` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute` 📖	mathematical	—	`ACCSystem.Sols` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `charges` `ACCSystem.solsMulAction` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystem.solsIncl` `anomalyFree`	—	—

ACCSystem.Sols

Definitions

Name	Category	Theorems
`toQuadSols` 📖	CompOp	75 math math: `MSSMACC.α₃_proj`, `MSSMACC.AnomalyFreePerp.perpB₃`, `SMRHN.PlusU1.BL.on_cubeTriLin`, `SM.SMNoGrav.One.accGrav_Q_neq_zero`, `SMRHN.PlusU1.Y.on_quadBiLin_AFL`, `MSSMACC.AnomalyFreePerp.inQuadSolProp_iff_proj_inQuadProp`, `pureU1_cube`, `PureU1.Three.three_sol_zero`, `SMRHN.SM.cubeSol`, `MSSMACC.proj_val`, `SMRHN.PlusU1.BL₁_val`, `SMRHN.PlusU1.Y_val`, `MSSMACC.planeY₃B₃_val`, `MSSMACC.α₁_proj`, `SMRHN.PlusU1.QuadSolToSol.generic_on_AF`, `MSSMACC.doublePoint_Y₃_B₃`, `MSSMACC.α₂_proj`, `SMRHN.PlusU1.BL.add_quad`, `SMRHN.PlusU1.Y.on_quadBiLin`, `MSSMACC.AnomalyFreePerp.linEqPropSol_iff_proj_linEqProp`, `SM.SMNoGrav.One.accGravSatisfied`, `MSSMACC.B₃_val`, `SMRHN.PlusU1.BL.on_quadBiLin_AFL`, `SM.SMNoGrav.One.E_zero_iff_Q_zero`, `MSSMACC.planeY₃B₃_cubic`, `MSSMACC.lineY₃B₃_doublePoint`, `SMRHN.PlusU1.Y.on_cubeTriLin`, `SMRHN.PlusU1.QuadSolToSol.generic_on_AF_α₁_ne_zero`, `MSSMACC.AnomalyFreeMk_val`, `MSSMACC.AnomalyFreePerp.perpY₃`, `SMRHN.PlusU1.Y.on_cubeTriLin'`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_AF`, `MSSMACC.Y₃_val`, `MSSMACC.planeY₃B₃_quad`, `SMRHN.PlusU1.Y.add_AF_cube`, `SMRHN.PlusU1.BL_val`, `PureU1.Even.special_case_lineInCubic`, `MSSMACC.lineQuad_cube`, `MSSMACC.cube_proj_proj_B₃`, `MSSMACC.cube_proj_proj_Y₃`, `MSSMACC.lineCube_quad`, `SMRHN.PlusU1.Y.add_AFL_quad`, `MSSMACC.doublePoint_Y₃_Y₃`, `SMRHN.PlusU1.BL.add_AFL_cube`, `SMRHN.PlusU1.Y.add_AFL_cube`, `SMRHN.PlusU1.quadSolToSolInv_1`, `PureU1.Even.special_case_lineInCubic_perm`, `MSSMACC.quad_self_proj`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `SMRHN.PlusU1.Y₁_val`, `PureU1.Odd.special_case_lineInCubic_perm`, `SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ`, `SMRHN.PlusU1.cubeSol`, `MSSMACC.AnomalyFreePerp.inCubeSolProp_iff_proj_inCubeProp`, `MSSMACC.quad_B₃_proj`, `SMRHN.PlusU1.QuadSolToSol.α₂_AF`, `PureU1.Even.special_case`, `SMRHN.SMNoGrav.cubeSol`, `SMRHN.PlusU1.BL.add_AFL_quad`, `MSSMACC.cube_proj_proj_self`, `SMRHN.PlusU1.Y.add_AFQ_cube`, `MSSMACC.AnomalyFreeMk''_val`, `MSSMACC.cube_proj`, `MSSMACC.doublePoint_B₃_B₃`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `SM.SMNoGrav.cubeSol`, `PureU1.Odd.special_case`, `SMRHN.PlusU1.BL.on_quadBiLin`, `SMRHN.PlusU1.Y.on_cubeTriLin_AFL`, `SMRHN.PlusU1.BL.on_cubeTriLin_AFL`, `cubicSol`, `SMRHN.PlusU1.Y.add_quad`, `MSSMACC.quad_proj`, `PureU1.Odd.special_case_lineInCubic`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cubicSol` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `ACCSystem.cubicACC` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.QuadSols.toLinSols` `toQuadSols`	—	—
`ext` 📖	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemQuad.QuadSols.toLinSols` `toQuadSols`	—	—	`ACCSystemQuad.QuadSols.ext`

ACCSystemCharges

Definitions

Name	Category	Theorems
`Charges` 📖	CompOp	292 math math: `SMRHN.sum_familyUniversal_one`, `SMRHN.SM.PlaneSeven.Bi_Bj_ne_cubic`, `SMRHN.accSU3_invariant`, `MSSMACC.α₃_proj`, `SMRHN.toSpecies_familyUniversal`, `SMRHN.SMNoGrav_quadraticACCs`, `SMACCs.quadBiLin_toFun_apply`, `SM.toSpecies_sum_invariant`, `MSSMCharges.toSMSpecies_toSpecies_inv`, `PureU1.accCubeTriLinSymm_toFun_apply_apply`, `ACCSystemGroupAction.rep_linSolRep_commute`, `MSSM.accSU2_invariant`, `ACCSystemLinear.linSolsIncl_injective`, `SM.SMNoGrav_linearACCs`, `ACCSystemLinear.LinSols.linearSol`, `ACCSystem.solsIncl_injective`, `PureU1.Odd.parameterizationAsLinear_val`, `MSSMCharges.Hu_apply`, `SMRHN.SM.PlaneSeven.basis_linear_independent`, `PureU1.Even.lineInCubicPerm_swap`, `SMRHN.sum_familyUniversal_three`, `MSSMCharges.toSpecies_apply`, `PureU1_quadraticACCs`, `SMRHN.SM.PlaneSeven.B₄_Bi_cubic`, `SMνCharges.toSpeciesEquiv_apply`, `MSSMACC.AnomalyFreePerp.perpB₃`, `SMRHN.familyUniversal_quadBiLin`, `MSSMCharges.toSMPlusH_apply`, `SMRHN.PlusU1.BL.on_cubeTriLin`, `PureU1.sort_perm`, `SMRHN.repCharges_toSpecies`, `SM.SMNoGrav.One.accGrav_Q_neq_zero`, `MSSM.accSU3_invariant`, `SMRHN.PlusU1.ElevenPlane.Bi_Bj_quad`, `SMRHN.PlusU1.Y.on_quadBiLin_AFL`, `MSSM.accCube_invariant`, `SMRHN.SMNoGrav_linearACCs`, `MSSM.Hu_invariant`, `MSSM.accQuad_invariant`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube`, `SMRHN.SM.PlaneSeven.B₅_Bi_cubic`, `SMRHN.accSU2_invariant`, `PureU1.VectorLikeOddPlane.basis_linearACC`, `SM.SMNoGrav.SU3Sol`, `SMνACCs.accCube_decomp`, `PureU1.Even.parameterizationCharge_cube`, `SMRHN.familyUniversal_accSU2`, `PureU1.VectorLikeEvenPlane.basis!_linearACC`, `SMCharges.charges_eq_toSpecies_eq`, `SMνACCs.quadBiLin_decomp`, `SM.SMNoGrav_cubicACC_apply`, `SMRHN.SM_linearACCs`, `SMνACCs.accSU3_decomp`, `SMRHN.PlusU1_linearACCs`, `SMRHN.SM.cubeSol`, `MSSMACC_cubicACC_apply`, `ACCSystem.Hom.commute`, `MSSMACCs.cubeTriLinToFun_map_smul₁`, `SMνCharges.toSMSpecies_toSpecies_inv`, `PureU1.Odd.P_P_P!_accCube'`, `SMRHN.accGrav_invariant`, `PureU1.VectorLikeOddPlane.P_accCube`, `PureU1_linearACCs`, `PureU1.VectorLikeOddPlane.P!_linearACC`, `MSSMACC.proj_val`, `PureU1.VectorLikeEvenPlane.P_linearACC`, `SMνCharges.toSpecies_one`, `SMRHN.PlusU1.ElevenPlane.on_accQuad`, `SMRHN.PlusU1.eleven_dim_plane_of_no_sols_exists`, `ACCSystemGroupAction.quadInvariant`, `PureU1.ConstAbsSorted.not_hasBoundary_grav`, `ACCSystemGroupAction.cubicInvariant`, `SMRHN.SM.PlaneSeven.Bi_Bi_Bj_cubic`, `SM.SMNoGrav_quadraticACCs`, `ACCSystemLinear.linSolsAddCommMonoid_zero_val`, `SMRHN.SM.PlaneSeven.B₃_cubic`, `SMRHN.PlusU1.Y_val`, `chargesModule_smul`, `SMνACCs.cubeTriLin_decomp`, `MSSMACC.planeY₃B₃_val`, `SMRHN.SM.gravSol`, `chargesAddCommMonoid_nsmul`, `MSSMACC.α₁_proj`, `SM.accSU2_invariant`, `MSSMCharges.Hd_toSpecies_inv`, `SMRHN.SM.PlaneSeven.Bi_Bj_Bk_cubic`, `SMRHN.SM.SU3Sol`, `PureU1.VectorLikeOddPlane.span_basis`, `MSSMACC.doublePoint_Y₃_B₃`, `MSSMACC.α₂_proj`, `SM.chargesMapOfSpeciesMap_apply`, `SMRHN.PlusU1.BL.add_quad`, `MSSMACCs.cubeTriLinToFun_swap2`, `PureU1.FamilyPermutations_charges_apply`, `SMRHN.PlusU1.Y.on_quadBiLin`, `SMRHN.SM.PlaneSeven.B₆_Bi_cubic`, `SM.SMNoGrav.One.linearParameters.grav`, `PureU1.VectorLikeOddPlane.P_P_P!_accCube`, `SMRHN.SM_quadraticACCs`, `SM.SMNoGrav.One.accGravSatisfied`, `SMRHN.speciesFamilyProj_apply`, `SMACCs.cubeTriLin_toFun_apply_apply`, `PureU1.Three.cube_for_linSol'`, `SMRHN.PlusU1.BL.on_quadBiLin_AFL`, `MSSMCharges.toSplitSMPlusH_apply`, `PureU1.Even.parameterizationAsLinear_val`, `SM.SMNoGrav.One.E_zero_iff_Q_zero`, `SM.accQuad_invariant`, `MSSMACC.planeY₃B₃_cubic`, `SMRHN.SM.PlaneSeven.B_in_accCube`, `MSSMACC.lineY₃B₃_doublePoint`, `SMRHN.PlusU1.Y.on_cubeTriLin`, `SMRHN.SM.PlaneSeven.B_sum_is_sol`, `SMRHN.SM.PlaneSeven.B₅_cubic`, `PureU1.VectorLikeEvenPlane.basis_accCube`, `SMνACCs.accQuad_decomp`, `SMRHN.SMNoGrav_cubicACC_apply`, `SMνACCs.quadBiLin_toFun_apply`, `MSSMCharges.toSplitSMPlusH_symm_apply`, `MSSM.accGrav_invariant`, `MSSMACC.dot_toFun_apply`, `MSSMCharges.Hd_apply`, `SM.accCube_invariant`, `MSSMACC.AnomalyFreePerp.perpY₃`, `SMRHN.chargesMapOfSpeciesMap_toSpecies`, `SM.chargeMap_apply`, `ACCSystemQuad.QuadSols.quadSol`, `SMRHN.PlusU1.Y.on_cubeTriLin'`, `SMRHN.SMNoGrav.SU2Sol`, `PureU1.VectorLikeEvenPlane.P_P_P!_accCube`, `SM.speciesFamilyUniversial_apply`, `PureU1.VectorLikeOddPlane.swap!_as_add`, `MSSMCharges.toSMSpecies_apply`, `PureU1.accCube_explicit`, `SMRHN.PlusU1.gravSol`, `PureU1.VectorLikeEvenPlane.P!_in_span`, `MSSMACC.lineQuadAFL_quad`, `SMRHN.PlusU1_cubicACC_apply`, `MSSMACC.planeY₃B₃_quad`, `SMRHN.PlusU1.Y.add_AF_cube`, `SMRHN.PlusU1.BL_val`, `SM.accGrav_invariant`, `MSSMACC.lineQuad_cube`, `MSSMACC.cube_proj_proj_B₃`, `SMRHN.SM.PlaneSeven.B₃_Bi_cubic`, `MSSMACC.cube_proj_proj_Y₃`, `SMCharges.toSpeciesEquiv_symm_apply`, `SMRHN.speciesEmbed_apply`, `MSSMACC.lineCube_quad`, `MSSMACCs.cubeTriLinToFun_swap1`, `SM.SMNoGrav.SU2Sol`, `MSSM.repCharges_toSMSpecies`, `PureU1.ConstAbsSorted.boundary_accGrav''`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `MSSMACC_linearACCs`, `PureU1.VectorLikeEvenPlane.P_accCube`, `PureU1.accCube_invariant`, `SMRHN.toSpecies_sum_invariant`, `SMRHN.familyUniversal_accCube`, `SMRHN.SM.PlaneSeven.B₆_cubic`, `PureU1.VectorLikeOddPlane.P_linearACC`, `MSSMCharges.Hu_toSpecies_inv`, `SMνCharges.charges_eq_toSpecies_eq`, `SMRHN.SM.SU2Sol`, `MSSM.chargeMap_apply`, `SMRHN.PlusU1.Y.add_AFL_quad`, `MSSMACC.doublePoint_Y₃_Y₃`, `PureU1.VectorLikeEvenPlane.basis!_accCube`, `SMRHN.chargeMap_apply`, `PureU1.accGrav_invariant`, `SMRHN.PlusU1.BL.add_AFL_cube`, `SMRHN.SM.PlaneSeven.B₀_cubic`, `SMRHN.SM.PlaneSeven.B₁_Bi_cubic`, `PureU1.chargeMap_apply`, `SMRHN.accQuad_invariant`, `SM.speciesEmbed_apply`, `PureU1.VectorLikeEvenPlane.smul_basis!AsCharges_in_span`, `MSSMACC.quadSol`, `SMRHN.PlusU1.YYsol`, `chargesAddCommMonoid_add`, `SMRHN.PlusU1.ElevenPlane.basis_linear_independent`, `SMRHN.PlusU1.ElevenPlane.Bi_sum_quad`, `ACCSystemGroupAction.linearInvariant`, `SMRHN.familyUniversal_accGrav`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `PureU1.Three.cube_for_linSol`, `SMRHN.PlusU1.Y.add_AFL_cube`, `SMRHN.chargesMapOfSpeciesMap_apply`, `MSSMCharges.toSpecies_symm_apply`, `PureU1.VectorLikeEvenPlane.swap!_as_add`, `MSSMACC_quadraticACCs`, `MSSMACC.quad_self_proj`, `PureU1.constAbs_perm`, `SMRHN.SM.PlaneSeven.B₀_Bi_cubic`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_cube`, `SMRHN.PlusU1_quadraticACCs`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `SMRHN.SM.PlaneSeven.B₂_cubic`, `chargesAddCommMonoid_zero_num`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `SMRHN.speciesFamilyUniversial_apply`, `ACCSystemLinear.linSolsModule_smul_val`, `SMRHN.sum_familyUniversal`, `SM.SMNoGrav.One.linearParametersQENeqZero.grav`, `SM.repCharges_toSpecies`, `MSSM.toSpecies_sum_invariant`, `instFiniteRatCharges`, `SM.SMNoGrav.One.linearParameters.speciesVal`, `PureU1.VectorLikeEvenPlane.P!_accCube`, `SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero`, `SMRHN.PlusU1.ElevenPlane.quadCoeff_eq_bilinear`, `SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ`, `SMRHN.SM.PlaneSeven.B₂_Bi_cubic`, `SMνCharges.toSpeciesEquiv_symm_apply`, `MSSMACC.lineY₃B₃Charges_cubic`, `PureU1.VectorLikeOddPlane.P!_accCube`, `SMRHN.PlusU1.cubeSol`, `SM.accYY_invariant`, `SMRHN.SM.PlaneSeven.B₄_cubic`, `PureU1.Odd.parameterizationCharge_cube`, `SMRHN.SM_cubicACC_apply`, `SMRHN.PlusU1.SU2Sol`, `PureU1_cubicACC_apply`, `SM.speciesFamilyProj_apply`, `MSSMACC.lineY₃B₃Charges_quad`, `MSSMACCs.quadBiLin_toFun_apply`, `SMCharges.toSpeciesEquiv_apply`, `PureU1.Odd.lineInCubicPerm_swap`, `SMRHN.SMNoGrav.SU3Sol`, `MSSMACC.quad_B₃_proj`, `SMRHN.SM.seven_dim_plane_exists`, `SMRHN.PlusU1.exists_plane_exists_basis`, `SMνACCs.accSU2_decomp`, `ACCSystemLinear.linSolsAddCommMonoid_add_val`, `SM.accSU3_invariant`, `ACCSystemLinear.linSolsAddCommMonoid_nsmul_val`, `SMRHN.SMNoGrav.cubeSol`, `SMRHN.PlusU1.BL.add_AFL_quad`, `ACCSystemGroupAction.rep_solAction_commute`, `MSSMACC.cube_proj_proj_self`, `SMνACCs.cubeTriLin_toFun_apply_apply`, `SMRHN.PlusU1.Y.add_AFQ_cube`, `ACCSystemGroupAction.linSolRep_apply_apply_val`, `MSSMCharges.charges_eq_toSpecies_eq`, `MSSMACC.cube_proj`, `chargesAddCommMonoid_zero_den`, `MSSMACC.doublePoint_B₃_B₃`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `ACCSystemQuad.quadSolsIncl_injective`, `SMCharges.toSpecies_apply`, `SMνACCs.accGrav_decomp`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `SM.SMNoGrav.cubeSol`, `SMRHN.sum_familyUniversal_two`, `PureU1.VectorLikeEvenPlane.P_P!_P!_accCube`, `MSSM.accYY_invariant`, `SMRHN.SM.PlaneSeven.B₁_cubic`, `SMRHN.PlusU1.BL.on_quadBiLin`, `SMRHN.familyUniversal_accQuad`, `SMRHN.familyUniversal_accSU3`, `SMRHN.PlusU1.Y.on_cubeTriLin_AFL`, `PureU1.VectorLikeOddPlane.basis!_linearACC`, `PureU1.Even.P_P_P!_accCube'`, `MSSMACCs.cubeTriLin_toFun_apply_apply`, `SMRHN.familyUniversal_cubeTriLin'`, `PureU1.VectorLikeEvenPlane.span_basis`, `MSSMACCs.cubeTriLinToFun_map_add₁`, `SMνCharges.toSpecies_apply`, `PureU1.sum_of_charges`, `SMRHN.accCube_invariant`, `SMRHN.accYY_invariant`, `SMRHN.PlusU1.BL.on_cubeTriLin_AFL`, `PureU1.Even.lineInCubic_expand`, `PureU1.ConstAbsSorted.is_zero`, `ACCSystem.Sols.cubicSol`, `ACCSystemGroupAction.rep_quadSolAction_commute`, `SMRHN.PlusU1.SU3Sol`, `MSSM.Hd_invariant`, `SMRHN.familyUniversal_accYY`, `SMRHN.PlusU1.Y.add_quad`, `MSSMACC.quad_proj`, `MSSMCharges.toSMPlusH_symm_apply`, `SMRHN.familyUniversal_cubeTriLin`, `PureU1.ConstAbsSorted.boundary_accGrav'`, `SMCharges.toSMSpecies_toSpecies_inv`, `PureU1.VectorLikeEvenPlane.basis_linearACC`, `SM.SMNoGrav.One.linearParameters.cubic`, `SMνACCs.accYY_decomp`, `MSSM.chargeMap_toSpecies`, `SMRHN.PlusU1.quadSol`, `MSSMACC.lineCube_cube`
`ChargesAddCommGroup` 📖	CompOp	34 math math: `ACCSystem.solsIncl_injective`, `PureU1.Odd.parameterizationAsLinear_val`, `ACCSystem.Hom.commute`, `MSSMACCs.cubeTriLinToFun_map_smul₁`, `MSSMACC.proj_val`, `SMRHN.PlusU1.ElevenPlane.on_accQuad`, `SMRHN.PlusU1.eleven_dim_plane_of_no_sols_exists`, `MSSMACC.planeY₃B₃_val`, `SMRHN.PlusU1.BL.add_quad`, `PureU1.Even.parameterizationAsLinear_val`, `SMRHN.SM.PlaneSeven.B_in_accCube`, `SMRHN.SM.PlaneSeven.B_sum_is_sol`, `PureU1.VectorLikeOddPlane.swap!_as_add`, `SMRHN.PlusU1.Y.add_AF_cube`, `SMRHN.PlusU1.Y.add_AFL_quad`, `PureU1.VectorLikeEvenPlane.span_basis_swap!`, `SMRHN.PlusU1.BL.add_AFL_cube`, `PureU1.VectorLikeEvenPlane.smul_basis!AsCharges_in_span`, `SMRHN.PlusU1.ElevenPlane.Bi_sum_quad`, `SMRHN.PlusU1.Y.add_AFL_cube`, `PureU1.VectorLikeEvenPlane.swap!_as_add`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `ACCSystemLinear.linSolsModule_smul_val`, `SMRHN.SM.seven_dim_plane_exists`, `ACCSystemLinear.linSolsAddCommMonoid_nsmul_val`, `SMRHN.PlusU1.BL.add_AFL_quad`, `ACCSystemGroupAction.rep_solAction_commute`, `SMRHN.PlusU1.Y.add_AFQ_cube`, `PureU1.VectorLikeOddPlane.span_basis_swap!`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `ACCSystemQuad.quadSolsIncl_injective`, `PureU1.ConstAbsSorted.is_zero`, `ACCSystemGroupAction.rep_quadSolAction_commute`, `SMRHN.PlusU1.Y.add_quad`
`chargesAddCommMonoid` 📖	CompOp	278 math math: `SMRHN.sum_familyUniversal_one`, `SMRHN.SM.PlaneSeven.Bi_Bj_ne_cubic`, `SMRHN.accSU3_invariant`, `MSSMACC.α₃_proj`, `SMRHN.toSpecies_familyUniversal`, `SMRHN.SMNoGrav_quadraticACCs`, `SMACCs.quadBiLin_toFun_apply`, `SM.toSpecies_sum_invariant`, `MSSMCharges.toSMSpecies_toSpecies_inv`, `PureU1.accCubeTriLinSymm_toFun_apply_apply`, `ACCSystemGroupAction.rep_linSolRep_commute`, `MSSM.accSU2_invariant`, `ACCSystemLinear.linSolsIncl_injective`, `SM.SMNoGrav_linearACCs`, `ACCSystemLinear.LinSols.linearSol`, `ACCSystem.solsIncl_injective`, `PureU1.Odd.parameterizationAsLinear_val`, `MSSMCharges.Hu_apply`, `SMRHN.SM.PlaneSeven.basis_linear_independent`, `PureU1.Even.lineInCubicPerm_swap`, `SMRHN.sum_familyUniversal_three`, `PureU1_quadraticACCs`, `SMRHN.SM.PlaneSeven.B₄_Bi_cubic`, `MSSMACC.AnomalyFreePerp.perpB₃`, `SMRHN.familyUniversal_quadBiLin`, `SMRHN.PlusU1.BL.on_cubeTriLin`, `PureU1.sort_perm`, `SMRHN.repCharges_toSpecies`, `SM.SMNoGrav.One.accGrav_Q_neq_zero`, `MSSM.accSU3_invariant`, `SMRHN.PlusU1.ElevenPlane.Bi_Bj_quad`, `SMRHN.PlusU1.Y.on_quadBiLin_AFL`, `MSSM.accCube_invariant`, `SMRHN.SMNoGrav_linearACCs`, `MSSM.Hu_invariant`, `MSSM.accQuad_invariant`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube`, `SMRHN.SM.PlaneSeven.B₅_Bi_cubic`, `SMRHN.accSU2_invariant`, `PureU1.VectorLikeOddPlane.basis_linearACC`, `SM.SMNoGrav.SU3Sol`, `SMνACCs.accCube_decomp`, `PureU1.Even.parameterizationCharge_cube`, `SMRHN.familyUniversal_accSU2`, `PureU1.VectorLikeEvenPlane.basis!_linearACC`, `SMCharges.charges_eq_toSpecies_eq`, `SMνACCs.quadBiLin_decomp`, `SM.SMNoGrav_cubicACC_apply`, `SMRHN.SM_linearACCs`, `SMνACCs.accSU3_decomp`, `SMRHN.PlusU1_linearACCs`, `SMRHN.SM.cubeSol`, `MSSMACC_cubicACC_apply`, `ACCSystem.Hom.commute`, `MSSMACCs.cubeTriLinToFun_map_smul₁`, `SMνCharges.toSMSpecies_toSpecies_inv`, `PureU1.Odd.P_P_P!_accCube'`, `SMRHN.accGrav_invariant`, `PureU1.VectorLikeOddPlane.P_accCube`, `PureU1_linearACCs`, `PureU1.VectorLikeOddPlane.P!_linearACC`, `MSSMACC.proj_val`, `PureU1.VectorLikeEvenPlane.P_linearACC`, `SMνCharges.toSpecies_one`, `SMRHN.PlusU1.ElevenPlane.on_accQuad`, `SMRHN.PlusU1.eleven_dim_plane_of_no_sols_exists`, `ACCSystemGroupAction.quadInvariant`, `PureU1.ConstAbsSorted.not_hasBoundary_grav`, `ACCSystemGroupAction.cubicInvariant`, `SMRHN.SM.PlaneSeven.Bi_Bi_Bj_cubic`, `SM.SMNoGrav_quadraticACCs`, `ACCSystemLinear.linSolsAddCommMonoid_zero_val`, `SMRHN.SM.PlaneSeven.B₃_cubic`, `SMRHN.PlusU1.Y_val`, `chargesModule_smul`, `SMνACCs.cubeTriLin_decomp`, `MSSMACC.planeY₃B₃_val`, `SMRHN.SM.gravSol`, `chargesAddCommMonoid_nsmul`, `MSSMACC.α₁_proj`, `SM.accSU2_invariant`, `MSSMCharges.Hd_toSpecies_inv`, `SMRHN.SM.PlaneSeven.Bi_Bj_Bk_cubic`, `SMRHN.SM.SU3Sol`, `PureU1.VectorLikeOddPlane.span_basis`, `MSSMACC.doublePoint_Y₃_B₃`, `MSSMACC.α₂_proj`, `SM.chargesMapOfSpeciesMap_apply`, `SMRHN.PlusU1.BL.add_quad`, `PureU1.FamilyPermutations_charges_apply`, `SMRHN.PlusU1.Y.on_quadBiLin`, `SMRHN.SM.PlaneSeven.B₆_Bi_cubic`, `SM.SMNoGrav.One.linearParameters.grav`, `PureU1.VectorLikeOddPlane.P_P_P!_accCube`, `SMRHN.SM_quadraticACCs`, `SM.SMNoGrav.One.accGravSatisfied`, `SMRHN.speciesFamilyProj_apply`, `SMACCs.cubeTriLin_toFun_apply_apply`, `PureU1.Three.cube_for_linSol'`, `SMRHN.PlusU1.BL.on_quadBiLin_AFL`, `PureU1.Even.parameterizationAsLinear_val`, `SM.SMNoGrav.One.E_zero_iff_Q_zero`, `SM.accQuad_invariant`, `MSSMACC.planeY₃B₃_cubic`, `SMRHN.SM.PlaneSeven.B_in_accCube`, `MSSMACC.lineY₃B₃_doublePoint`, `SMRHN.PlusU1.Y.on_cubeTriLin`, `SMRHN.SM.PlaneSeven.B_sum_is_sol`, `SMRHN.SM.PlaneSeven.B₅_cubic`, `PureU1.VectorLikeEvenPlane.basis_accCube`, `SMνACCs.accQuad_decomp`, `SMRHN.SMNoGrav_cubicACC_apply`, `SMνACCs.quadBiLin_toFun_apply`, `MSSM.accGrav_invariant`, `MSSMACC.dot_toFun_apply`, `MSSMCharges.Hd_apply`, `SM.accCube_invariant`, `MSSMACC.AnomalyFreePerp.perpY₃`, `SMRHN.chargesMapOfSpeciesMap_toSpecies`, `SM.chargeMap_apply`, `ACCSystemQuad.QuadSols.quadSol`, `SMRHN.PlusU1.Y.on_cubeTriLin'`, `SMRHN.SMNoGrav.SU2Sol`, `PureU1.VectorLikeEvenPlane.P_P_P!_accCube`, `SM.speciesFamilyUniversial_apply`, `PureU1.VectorLikeOddPlane.swap!_as_add`, `MSSMCharges.toSMSpecies_apply`, `PureU1.accCube_explicit`, `SMRHN.PlusU1.gravSol`, `PureU1.VectorLikeEvenPlane.P!_in_span`, `MSSMACC.lineQuadAFL_quad`, `SMRHN.PlusU1_cubicACC_apply`, `MSSMACC.planeY₃B₃_quad`, `SMRHN.PlusU1.Y.add_AF_cube`, `SMRHN.PlusU1.BL_val`, `SM.accGrav_invariant`, `MSSMACC.lineQuad_cube`, `MSSMACC.cube_proj_proj_B₃`, `SMRHN.SM.PlaneSeven.B₃_Bi_cubic`, `MSSMACC.cube_proj_proj_Y₃`, `SMRHN.speciesEmbed_apply`, `MSSMACC.lineCube_quad`, `SM.SMNoGrav.SU2Sol`, `MSSM.repCharges_toSMSpecies`, `PureU1.ConstAbsSorted.boundary_accGrav''`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `MSSMACC_linearACCs`, `PureU1.VectorLikeEvenPlane.P_accCube`, `PureU1.accCube_invariant`, `SMRHN.toSpecies_sum_invariant`, `SMRHN.familyUniversal_accCube`, `SMRHN.SM.PlaneSeven.B₆_cubic`, `PureU1.VectorLikeOddPlane.P_linearACC`, `MSSMCharges.Hu_toSpecies_inv`, `SMνCharges.charges_eq_toSpecies_eq`, `SMRHN.SM.SU2Sol`, `MSSM.chargeMap_apply`, `SMRHN.PlusU1.Y.add_AFL_quad`, `MSSMACC.doublePoint_Y₃_Y₃`, `PureU1.VectorLikeEvenPlane.basis!_accCube`, `SMRHN.chargeMap_apply`, `PureU1.accGrav_invariant`, `SMRHN.PlusU1.BL.add_AFL_cube`, `SMRHN.SM.PlaneSeven.B₀_cubic`, `SMRHN.SM.PlaneSeven.B₁_Bi_cubic`, `PureU1.chargeMap_apply`, `SMRHN.accQuad_invariant`, `SM.speciesEmbed_apply`, `PureU1.VectorLikeEvenPlane.smul_basis!AsCharges_in_span`, `MSSMACC.quadSol`, `SMRHN.PlusU1.YYsol`, `chargesAddCommMonoid_add`, `SMRHN.PlusU1.ElevenPlane.basis_linear_independent`, `SMRHN.PlusU1.ElevenPlane.Bi_sum_quad`, `ACCSystemGroupAction.linearInvariant`, `SMRHN.familyUniversal_accGrav`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `PureU1.Three.cube_for_linSol`, `SMRHN.PlusU1.Y.add_AFL_cube`, `SMRHN.chargesMapOfSpeciesMap_apply`, `PureU1.VectorLikeEvenPlane.swap!_as_add`, `MSSMACC_quadraticACCs`, `MSSMACC.quad_self_proj`, `PureU1.constAbs_perm`, `SMRHN.SM.PlaneSeven.B₀_Bi_cubic`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_cube`, `SMRHN.PlusU1_quadraticACCs`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `SMRHN.SM.PlaneSeven.B₂_cubic`, `chargesAddCommMonoid_zero_num`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `SMRHN.speciesFamilyUniversial_apply`, `ACCSystemLinear.linSolsModule_smul_val`, `SMRHN.sum_familyUniversal`, `SM.SMNoGrav.One.linearParametersQENeqZero.grav`, `SM.repCharges_toSpecies`, `MSSM.toSpecies_sum_invariant`, `instFiniteRatCharges`, `SM.SMNoGrav.One.linearParameters.speciesVal`, `PureU1.VectorLikeEvenPlane.P!_accCube`, `SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero`, `SMRHN.PlusU1.ElevenPlane.quadCoeff_eq_bilinear`, `SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ`, `SMRHN.SM.PlaneSeven.B₂_Bi_cubic`, `MSSMACC.lineY₃B₃Charges_cubic`, `PureU1.VectorLikeOddPlane.P!_accCube`, `SMRHN.PlusU1.cubeSol`, `SM.accYY_invariant`, `SMRHN.SM.PlaneSeven.B₄_cubic`, `PureU1.Odd.parameterizationCharge_cube`, `SMRHN.SM_cubicACC_apply`, `SMRHN.PlusU1.SU2Sol`, `PureU1_cubicACC_apply`, `SM.speciesFamilyProj_apply`, `MSSMACC.lineY₃B₃Charges_quad`, `MSSMACCs.quadBiLin_toFun_apply`, `PureU1.Odd.lineInCubicPerm_swap`, `SMRHN.SMNoGrav.SU3Sol`, `MSSMACC.quad_B₃_proj`, `SMRHN.SM.seven_dim_plane_exists`, `SMRHN.PlusU1.exists_plane_exists_basis`, `SMνACCs.accSU2_decomp`, `ACCSystemLinear.linSolsAddCommMonoid_add_val`, `SM.accSU3_invariant`, `SMRHN.SMNoGrav.cubeSol`, `SMRHN.PlusU1.BL.add_AFL_quad`, `ACCSystemGroupAction.rep_solAction_commute`, `MSSMACC.cube_proj_proj_self`, `SMνACCs.cubeTriLin_toFun_apply_apply`, `SMRHN.PlusU1.Y.add_AFQ_cube`, `ACCSystemGroupAction.linSolRep_apply_apply_val`, `MSSMCharges.charges_eq_toSpecies_eq`, `MSSMACC.cube_proj`, `chargesAddCommMonoid_zero_den`, `MSSMACC.doublePoint_B₃_B₃`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `ACCSystemQuad.quadSolsIncl_injective`, `SMCharges.toSpecies_apply`, `SMνACCs.accGrav_decomp`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `SM.SMNoGrav.cubeSol`, `SMRHN.sum_familyUniversal_two`, `PureU1.VectorLikeEvenPlane.P_P!_P!_accCube`, `MSSM.accYY_invariant`, `SMRHN.SM.PlaneSeven.B₁_cubic`, `SMRHN.PlusU1.BL.on_quadBiLin`, `SMRHN.familyUniversal_accQuad`, `SMRHN.familyUniversal_accSU3`, `SMRHN.PlusU1.Y.on_cubeTriLin_AFL`, `PureU1.VectorLikeOddPlane.basis!_linearACC`, `PureU1.Even.P_P_P!_accCube'`, `MSSMACCs.cubeTriLin_toFun_apply_apply`, `SMRHN.familyUniversal_cubeTriLin'`, `PureU1.VectorLikeEvenPlane.span_basis`, `MSSMACCs.cubeTriLinToFun_map_add₁`, `SMνCharges.toSpecies_apply`, `PureU1.sum_of_charges`, `SMRHN.accCube_invariant`, `SMRHN.accYY_invariant`, `SMRHN.PlusU1.BL.on_cubeTriLin_AFL`, `PureU1.Even.lineInCubic_expand`, `ACCSystem.Sols.cubicSol`, `ACCSystemGroupAction.rep_quadSolAction_commute`, `SMRHN.PlusU1.SU3Sol`, `MSSM.Hd_invariant`, `SMRHN.familyUniversal_accYY`, `SMRHN.PlusU1.Y.add_quad`, `MSSMACC.quad_proj`, `SMRHN.familyUniversal_cubeTriLin`, `PureU1.ConstAbsSorted.boundary_accGrav'`, `SMCharges.toSMSpecies_toSpecies_inv`, `PureU1.VectorLikeEvenPlane.basis_linearACC`, `SM.SMNoGrav.One.linearParameters.cubic`, `SMνACCs.accYY_decomp`, `MSSM.chargeMap_toSpecies`, `SMRHN.PlusU1.quadSol`, `MSSMACC.lineCube_cube`
`chargesModule` 📖	CompOp	275 math math: `SMRHN.sum_familyUniversal_one`, `SMRHN.SM.PlaneSeven.Bi_Bj_ne_cubic`, `SMRHN.accSU3_invariant`, `MSSMACC.α₃_proj`, `SMRHN.toSpecies_familyUniversal`, `SMRHN.SMNoGrav_quadraticACCs`, `SMACCs.quadBiLin_toFun_apply`, `SM.toSpecies_sum_invariant`, `MSSMCharges.toSMSpecies_toSpecies_inv`, `PureU1.accCubeTriLinSymm_toFun_apply_apply`, `ACCSystemGroupAction.rep_linSolRep_commute`, `MSSM.accSU2_invariant`, `ACCSystemLinear.linSolsIncl_injective`, `SM.SMNoGrav_linearACCs`, `ACCSystemLinear.LinSols.linearSol`, `ACCSystem.solsIncl_injective`, `PureU1.Even.line_in_cubic_P_P_P!`, `PureU1.Odd.parameterizationAsLinear_val`, `MSSMCharges.Hu_apply`, `SMRHN.SM.PlaneSeven.basis_linear_independent`, `PureU1.Even.lineInCubicPerm_swap`, `SMRHN.sum_familyUniversal_three`, `PureU1_quadraticACCs`, `SMRHN.SM.PlaneSeven.B₄_Bi_cubic`, `MSSMACC.AnomalyFreePerp.perpB₃`, `SMRHN.familyUniversal_quadBiLin`, `SMRHN.PlusU1.BL.on_cubeTriLin`, `PureU1.sort_perm`, `SMRHN.repCharges_toSpecies`, `SM.SMNoGrav.One.accGrav_Q_neq_zero`, `MSSM.accSU3_invariant`, `SMRHN.PlusU1.ElevenPlane.Bi_Bj_quad`, `SMRHN.PlusU1.Y.on_quadBiLin_AFL`, `MSSM.accCube_invariant`, `SMRHN.SMNoGrav_linearACCs`, `MSSM.Hu_invariant`, `MSSM.accQuad_invariant`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube`, `SMRHN.SM.PlaneSeven.B₅_Bi_cubic`, `SMRHN.accSU2_invariant`, `PureU1.VectorLikeOddPlane.basis_linearACC`, `SM.SMNoGrav.SU3Sol`, `SMνACCs.accCube_decomp`, `PureU1.Even.parameterizationCharge_cube`, `SMRHN.familyUniversal_accSU2`, `PureU1.VectorLikeEvenPlane.basis!_linearACC`, `SMCharges.charges_eq_toSpecies_eq`, `SMνACCs.quadBiLin_decomp`, `SM.SMNoGrav_cubicACC_apply`, `SMRHN.SM_linearACCs`, `SMνACCs.accSU3_decomp`, `SMRHN.PlusU1_linearACCs`, `SMRHN.SM.cubeSol`, `MSSMACC_cubicACC_apply`, `ACCSystem.Hom.commute`, `MSSMACCs.cubeTriLinToFun_map_smul₁`, `SMνCharges.toSMSpecies_toSpecies_inv`, `PureU1.Odd.P_P_P!_accCube'`, `SMRHN.accGrav_invariant`, `PureU1.VectorLikeOddPlane.P_accCube`, `PureU1_linearACCs`, `PureU1.VectorLikeOddPlane.P!_linearACC`, `MSSMACC.proj_val`, `PureU1.VectorLikeEvenPlane.P_linearACC`, `SMνCharges.toSpecies_one`, `SMRHN.PlusU1.ElevenPlane.on_accQuad`, `SMRHN.PlusU1.eleven_dim_plane_of_no_sols_exists`, `ACCSystemGroupAction.quadInvariant`, `PureU1.ConstAbsSorted.not_hasBoundary_grav`, `ACCSystemGroupAction.cubicInvariant`, `SMRHN.SM.PlaneSeven.Bi_Bi_Bj_cubic`, `SM.SMNoGrav_quadraticACCs`, `SMRHN.SM.PlaneSeven.B₃_cubic`, `SMRHN.PlusU1.Y_val`, `chargesModule_smul`, `SMνACCs.cubeTriLin_decomp`, `MSSMACC.planeY₃B₃_val`, `SMRHN.SM.gravSol`, `MSSMACC.α₁_proj`, `PureU1.Even.anomalyFree_param`, `SM.accSU2_invariant`, `MSSMCharges.Hd_toSpecies_inv`, `SMRHN.SM.PlaneSeven.Bi_Bj_Bk_cubic`, `SMRHN.SM.SU3Sol`, `MSSMACC.doublePoint_Y₃_B₃`, `MSSMACC.α₂_proj`, `SM.chargesMapOfSpeciesMap_apply`, `SMRHN.PlusU1.BL.add_quad`, `PureU1.FamilyPermutations_charges_apply`, `SMRHN.PlusU1.Y.on_quadBiLin`, `SMRHN.SM.PlaneSeven.B₆_Bi_cubic`, `SM.SMNoGrav.One.linearParameters.grav`, `PureU1.VectorLikeOddPlane.P_P_P!_accCube`, `SMRHN.SM_quadraticACCs`, `PureU1.Odd.line_in_cubic_P_P_P!`, `SM.SMNoGrav.One.accGravSatisfied`, `SMRHN.speciesFamilyProj_apply`, `SMACCs.cubeTriLin_toFun_apply_apply`, `PureU1.Three.cube_for_linSol'`, `SMRHN.PlusU1.BL.on_quadBiLin_AFL`, `PureU1.Even.parameterizationAsLinear_val`, `SM.SMNoGrav.One.E_zero_iff_Q_zero`, `SM.accQuad_invariant`, `MSSMACC.planeY₃B₃_cubic`, `SMRHN.SM.PlaneSeven.B_in_accCube`, `MSSMACC.lineY₃B₃_doublePoint`, `SMRHN.PlusU1.Y.on_cubeTriLin`, `SMRHN.SM.PlaneSeven.B_sum_is_sol`, `SMRHN.SM.PlaneSeven.B₅_cubic`, `PureU1.VectorLikeEvenPlane.basis_accCube`, `SMνACCs.accQuad_decomp`, `SMRHN.SMNoGrav_cubicACC_apply`, `SMνACCs.quadBiLin_toFun_apply`, `MSSM.accGrav_invariant`, `MSSMACC.dot_toFun_apply`, `MSSMCharges.Hd_apply`, `SM.accCube_invariant`, `MSSMACC.AnomalyFreePerp.perpY₃`, `SMRHN.chargesMapOfSpeciesMap_toSpecies`, `SM.chargeMap_apply`, `ACCSystemQuad.QuadSols.quadSol`, `SMRHN.PlusU1.Y.on_cubeTriLin'`, `SMRHN.SMNoGrav.SU2Sol`, `PureU1.VectorLikeEvenPlane.P_P_P!_accCube`, `SM.speciesFamilyUniversial_apply`, `PureU1.VectorLikeOddPlane.swap!_as_add`, `MSSMCharges.toSMSpecies_apply`, `PureU1.accCube_explicit`, `SMRHN.PlusU1.gravSol`, `PureU1.VectorLikeEvenPlane.P!_in_span`, `MSSMACC.lineQuadAFL_quad`, `SMRHN.PlusU1_cubicACC_apply`, `MSSMACC.planeY₃B₃_quad`, `SMRHN.PlusU1.Y.add_AF_cube`, `SMRHN.PlusU1.BL_val`, `PureU1.Odd.anomalyFree_param`, `SM.accGrav_invariant`, `MSSMACC.lineQuad_cube`, `MSSMACC.cube_proj_proj_B₃`, `SMRHN.SM.PlaneSeven.B₃_Bi_cubic`, `PureU1.Odd.lineInCubic_expand`, `MSSMACC.cube_proj_proj_Y₃`, `SMRHN.speciesEmbed_apply`, `MSSMACC.lineCube_quad`, `SM.SMNoGrav.SU2Sol`, `MSSM.repCharges_toSMSpecies`, `PureU1.ConstAbsSorted.boundary_accGrav''`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `MSSMACC_linearACCs`, `PureU1.VectorLikeEvenPlane.P_accCube`, `PureU1.accCube_invariant`, `SMRHN.toSpecies_sum_invariant`, `SMRHN.familyUniversal_accCube`, `SMRHN.SM.PlaneSeven.B₆_cubic`, `PureU1.VectorLikeOddPlane.P_linearACC`, `MSSMCharges.Hu_toSpecies_inv`, `SMνCharges.charges_eq_toSpecies_eq`, `SMRHN.SM.SU2Sol`, `MSSM.chargeMap_apply`, `SMRHN.PlusU1.Y.add_AFL_quad`, `PureU1.VectorLikeEvenPlane.span_basis_swap!`, `MSSMACC.doublePoint_Y₃_Y₃`, `PureU1.VectorLikeEvenPlane.basis!_accCube`, `SMRHN.chargeMap_apply`, `PureU1.accGrav_invariant`, `SMRHN.PlusU1.BL.add_AFL_cube`, `SMRHN.SM.PlaneSeven.B₀_cubic`, `SMRHN.SM.PlaneSeven.B₁_Bi_cubic`, `PureU1.chargeMap_apply`, `SMRHN.accQuad_invariant`, `SM.speciesEmbed_apply`, `PureU1.VectorLikeEvenPlane.smul_basis!AsCharges_in_span`, `MSSMACC.quadSol`, `SMRHN.PlusU1.YYsol`, `SMRHN.PlusU1.ElevenPlane.basis_linear_independent`, `SMRHN.PlusU1.ElevenPlane.Bi_sum_quad`, `ACCSystemGroupAction.linearInvariant`, `SMRHN.familyUniversal_accGrav`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `PureU1.Three.cube_for_linSol`, `SMRHN.PlusU1.Y.add_AFL_cube`, `SMRHN.chargesMapOfSpeciesMap_apply`, `PureU1.VectorLikeEvenPlane.swap!_as_add`, `MSSMACC_quadraticACCs`, `MSSMACC.quad_self_proj`, `PureU1.constAbs_perm`, `SMRHN.SM.PlaneSeven.B₀_Bi_cubic`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_cube`, `SMRHN.PlusU1_quadraticACCs`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `SMRHN.SM.PlaneSeven.B₂_cubic`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `SMRHN.speciesFamilyUniversial_apply`, `ACCSystemLinear.linSolsModule_smul_val`, `SMRHN.sum_familyUniversal`, `SM.SMNoGrav.One.linearParametersQENeqZero.grav`, `SM.repCharges_toSpecies`, `MSSM.toSpecies_sum_invariant`, `instFiniteRatCharges`, `SM.SMNoGrav.One.linearParameters.speciesVal`, `PureU1.VectorLikeEvenPlane.P!_accCube`, `SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero`, `SMRHN.PlusU1.ElevenPlane.quadCoeff_eq_bilinear`, `SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ`, `SMRHN.SM.PlaneSeven.B₂_Bi_cubic`, `MSSMACC.lineY₃B₃Charges_cubic`, `PureU1.VectorLikeOddPlane.P!_accCube`, `SMRHN.PlusU1.cubeSol`, `SM.accYY_invariant`, `SMRHN.SM.PlaneSeven.B₄_cubic`, `PureU1.Odd.parameterizationCharge_cube`, `SMRHN.SM_cubicACC_apply`, `SMRHN.PlusU1.SU2Sol`, `PureU1_cubicACC_apply`, `SM.speciesFamilyProj_apply`, `MSSMACC.lineY₃B₃Charges_quad`, `MSSMACCs.quadBiLin_toFun_apply`, `PureU1.Odd.lineInCubicPerm_swap`, `SMRHN.SMNoGrav.SU3Sol`, `MSSMACC.quad_B₃_proj`, `SMRHN.SM.seven_dim_plane_exists`, `SMRHN.PlusU1.exists_plane_exists_basis`, `SMνACCs.accSU2_decomp`, `SM.accSU3_invariant`, `SMRHN.SMNoGrav.cubeSol`, `SMRHN.PlusU1.BL.add_AFL_quad`, `ACCSystemGroupAction.rep_solAction_commute`, `MSSMACC.cube_proj_proj_self`, `SMνACCs.cubeTriLin_toFun_apply_apply`, `SMRHN.PlusU1.Y.add_AFQ_cube`, `ACCSystemGroupAction.linSolRep_apply_apply_val`, `MSSMCharges.charges_eq_toSpecies_eq`, `MSSMACC.cube_proj`, `MSSMACC.doublePoint_B₃_B₃`, `PureU1.VectorLikeOddPlane.span_basis_swap!`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `ACCSystemQuad.quadSolsIncl_injective`, `SMCharges.toSpecies_apply`, `SMνACCs.accGrav_decomp`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `SM.SMNoGrav.cubeSol`, `SMRHN.sum_familyUniversal_two`, `PureU1.VectorLikeEvenPlane.P_P!_P!_accCube`, `MSSM.accYY_invariant`, `SMRHN.SM.PlaneSeven.B₁_cubic`, `SMRHN.PlusU1.BL.on_quadBiLin`, `SMRHN.familyUniversal_accQuad`, `SMRHN.familyUniversal_accSU3`, `SMRHN.PlusU1.Y.on_cubeTriLin_AFL`, `PureU1.VectorLikeOddPlane.basis!_linearACC`, `PureU1.Even.P_P_P!_accCube'`, `MSSMACCs.cubeTriLin_toFun_apply_apply`, `SMRHN.familyUniversal_cubeTriLin'`, `SMνCharges.toSpecies_apply`, `SMRHN.accCube_invariant`, `SMRHN.accYY_invariant`, `SMRHN.PlusU1.BL.on_cubeTriLin_AFL`, `PureU1.Even.lineInCubic_expand`, `ACCSystem.Sols.cubicSol`, `ACCSystemGroupAction.rep_quadSolAction_commute`, `SMRHN.PlusU1.SU3Sol`, `MSSM.Hd_invariant`, `SMRHN.familyUniversal_accYY`, `SMRHN.PlusU1.Y.add_quad`, `MSSMACC.quad_proj`, `SMRHN.familyUniversal_cubeTriLin`, `PureU1.ConstAbsSorted.boundary_accGrav'`, `SMCharges.toSMSpecies_toSpecies_inv`, `PureU1.VectorLikeEvenPlane.basis_linearACC`, `SM.SMNoGrav.One.linearParameters.cubic`, `SMνACCs.accYY_decomp`, `MSSM.chargeMap_toSpecies`, `SMRHN.PlusU1.quadSol`, `MSSMACC.lineCube_cube`
`numberCharges` 📖	CompOp	45 math math: `SMRHN.sum_familyUniversal_one`, `SMRHN.toSpecies_familyUniversal`, `SM.toSpecies_sum_invariant`, `SMRHN.sum_familyUniversal_three`, `SMSpecies_numberCharges`, `PureU1.VectorLikeEvenPlane.P_evenSnd_evenFst`, `SMRHN.familyUniversal_quadBiLin`, `PureU1.sort_apply`, `SMRHN.repCharges_toSpecies`, `SMRHN.SM_numberCharges`, `PureU1.PureU1Charges_numberCharges`, `SMνACCs.accCube_decomp`, `pureU1_cube`, `SMνACCs.quadBiLin_decomp`, `SMνACCs.accSU3_decomp`, `MSSMSpecies_numberCharges`, `SMνCharges.toSpecies_one`, `SMνACCs.cubeTriLin_decomp`, `PureU1.ConstAbsSorted.AFL_even_below`, `SMνACCs.accQuad_decomp`, `SMCharges_numberCharges`, `PureU1.ConstAbsSorted.AFL_even_above'`, `MSSM.repCharges_toSMSpecies`, `SMRHN.toSpecies_sum_invariant`, `SM.SMNoGrav_numberCharges`, `PureU1_numberCharges`, `SMνCharges_numberCharges`, `SMRHN.sum_familyUniversal`, `SMRHN.SMNoGrav_numberCharges`, `SM.repCharges_toSpecies`, `MSSM.toSpecies_sum_invariant`, `PureU1.ConstAbsSorted.AFL_even_above`, `MSSMCharges_numberCharges`, `SMνACCs.accSU2_decomp`, `MSSMACC_numberCharges`, `SMνSpecies_numberCharges`, `SMRHN.PlusU1_numberCharges`, `SMνACCs.accGrav_decomp`, `SMRHN.sum_familyUniversal_two`, `PureU1.ConstAbsSorted.AFL_even_below'`, `SMRHN.familyUniversal_cubeTriLin'`, `SMRHN.familyUniversal_cubeTriLin`, `PureU1.ConstAbsSorted.boundary_accGrav'`, `SMνACCs.accYY_decomp`, `MSSM.chargeMap_toSpecies`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chargesAddCommMonoid_add` 📖	mathematical	—	`Charges` `chargesAddCommMonoid`	—	—
`chargesAddCommMonoid_nsmul` 📖	mathematical	—	`Charges` `chargesAddCommMonoid`	—	—
`chargesAddCommMonoid_zero_den` 📖	mathematical	—	`Charges` `chargesAddCommMonoid`	—	—
`chargesAddCommMonoid_zero_num` 📖	mathematical	—	`Charges` `chargesAddCommMonoid`	—	—
`chargesModule_smul` 📖	mathematical	—	`Charges` `chargesAddCommMonoid` `chargesModule`	—	—
`instFiniteRatCharges` 📖	mathematical	—	`Charges` `chargesAddCommMonoid` `chargesModule`	—	—

ACCSystemLinear

Definitions

Name	Category	Theorems
`LinSols` 📖	CompData	49 math math: `ACCSystemGroupAction.rep_linSolRep_commute`, `linSolsIncl_injective`, `SMRHN.PlusU1.QuadSol.toQuadInv_fst`, `PureU1.VectorLikeOddPlane.basis!_linear_independent`, `MSSMACC.lineCube_smul`, `PureU1.ConstAbsSorted.AFL_odd`, `PureU1.ConstAbs.boundary_value_odd`, `PureU1.lineInPlaneCond_perm`, `PureU1.FamilyPermutations_anomalyFreeLinear_apply`, `SMRHN.PlusU1.QuadSol.toQuadInv_generic`, `ACCSystemQuad.quadSolsInclLinSols_injective`, `linSolsAddCommMonoid_zero_val`, `PureU1.BasisLinear.sum_of_vectors`, `PureU1.sum_of_anomaly_free_linear`, `PureU1.VectorLikeOddPlane.basisa_card`, `PureU1.Odd.lineInCubicPerm_permute`, `PureU1.Odd.lineInCubicPerm_zero`, `PureU1.VectorLikeEvenPlane.basis!_linear_independent`, `PureU1.VectorLikeOddPlane.Pa'_P'_P!'`, `SMRHN.PlusU1.QuadSol.toQuadInv_special`, `PureU1.BasisLinear.finrank_AnomalyFreeLinear`, `ACCSystemGroupAction.linSolRep_solAction_commute`, `MSSMACC.planeY₃B₃_smul`, `ACCSystemGroupAction.linSolRep_quadSolAction_commute`, `PureU1.VectorLikeEvenPlane.vectorLikeEven_in_span`, `PureU1.VectorLikeOddPlane.basisa_linear_independent`, `PureU1.Even.lineInCubicPerm_permute`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `PureU1.One.solEqZero`, `PureU1.Even.lineInCubicPerm_in_plane`, `PureU1.VectorLikeEvenPlane.Pa'_P'_P!'`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `SMRHN.PlusU1.QuadSol.toQuad_surjective`, `SMRHN.PlusU1.QuadSol.toQuad_rightInverse`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `linSolsModule_smul_val`, `PureU1.VectorLikeEvenPlane.basisa_card`, `SM.SMNoGrav.One.linearParametersQENeqZero.grav`, `linSolsAddCommMonoid_add_val`, `PureU1.Even.special_case`, `PureU1.VectorLikeEvenPlane.basisa_linear_independent`, `linSolsAddCommMonoid_nsmul_val`, `ACCSystemGroupAction.linSolRep_apply_apply_val`, `PureU1.BasisLinear.instFiniteRatLinSolsSucc`, `PureU1.Odd.special_case`, `SMRHN.PlusU1.QuadSol.toQuadInv_α₁_α₂`, `PureU1.VectorLikeOddPlane.basis_linear_independent`, `ACCSystem.solsInclLinSols_injective`, `PureU1.VectorLikeEvenPlane.basis_linear_independent`
`linSolsAddCommGroup` 📖	CompOp	13 math math: `MSSMACC.lineCube_smul`, `PureU1.ConstAbsSorted.AFL_odd`, `PureU1.ConstAbs.boundary_value_odd`, `ACCSystemQuad.quadSolsInclLinSols_injective`, `PureU1.Odd.lineInCubicPerm_zero`, `ACCSystemGroupAction.linSolRep_solAction_commute`, `MSSMACC.planeY₃B₃_smul`, `ACCSystemGroupAction.linSolRep_quadSolAction_commute`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `PureU1.One.solEqZero`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `PureU1.Odd.special_case`, `ACCSystem.solsInclLinSols_injective`
`linSolsAddCommMonoid` 📖	CompOp	36 math math: `ACCSystemGroupAction.rep_linSolRep_commute`, `linSolsIncl_injective`, `PureU1.VectorLikeOddPlane.basis!_linear_independent`, `MSSMACC.lineCube_smul`, `PureU1.lineInPlaneCond_perm`, `PureU1.FamilyPermutations_anomalyFreeLinear_apply`, `ACCSystemQuad.quadSolsInclLinSols_injective`, `linSolsAddCommMonoid_zero_val`, `PureU1.BasisLinear.sum_of_vectors`, `PureU1.sum_of_anomaly_free_linear`, `PureU1.VectorLikeOddPlane.basisa_card`, `PureU1.Odd.lineInCubicPerm_permute`, `PureU1.VectorLikeEvenPlane.basis!_linear_independent`, `PureU1.VectorLikeOddPlane.Pa'_P'_P!'`, `PureU1.BasisLinear.finrank_AnomalyFreeLinear`, `ACCSystemGroupAction.linSolRep_solAction_commute`, `MSSMACC.planeY₃B₃_smul`, `ACCSystemGroupAction.linSolRep_quadSolAction_commute`, `PureU1.VectorLikeEvenPlane.vectorLikeEven_in_span`, `PureU1.VectorLikeOddPlane.basisa_linear_independent`, `PureU1.Even.lineInCubicPerm_permute`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `PureU1.Even.lineInCubicPerm_in_plane`, `PureU1.VectorLikeEvenPlane.Pa'_P'_P!'`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `linSolsModule_smul_val`, `PureU1.VectorLikeEvenPlane.basisa_card`, `linSolsAddCommMonoid_add_val`, `PureU1.Even.special_case`, `PureU1.VectorLikeEvenPlane.basisa_linear_independent`, `linSolsAddCommMonoid_nsmul_val`, `ACCSystemGroupAction.linSolRep_apply_apply_val`, `PureU1.BasisLinear.instFiniteRatLinSolsSucc`, `PureU1.VectorLikeOddPlane.basis_linear_independent`, `ACCSystem.solsInclLinSols_injective`, `PureU1.VectorLikeEvenPlane.basis_linear_independent`
`linSolsIncl` 📖	CompOp	2 math math: `ACCSystemGroupAction.rep_linSolRep_commute`, `linSolsIncl_injective`
`linSolsModule` 📖	CompOp	29 math math: `ACCSystemGroupAction.rep_linSolRep_commute`, `linSolsIncl_injective`, `PureU1.VectorLikeOddPlane.basis!_linear_independent`, `MSSMACC.lineCube_smul`, `PureU1.lineInPlaneCond_perm`, `PureU1.FamilyPermutations_anomalyFreeLinear_apply`, `ACCSystemQuad.quadSolsInclLinSols_injective`, `PureU1.VectorLikeOddPlane.basisa_card`, `PureU1.Odd.lineInCubicPerm_permute`, `PureU1.VectorLikeEvenPlane.basis!_linear_independent`, `PureU1.BasisLinear.finrank_AnomalyFreeLinear`, `ACCSystemGroupAction.linSolRep_solAction_commute`, `MSSMACC.planeY₃B₃_smul`, `ACCSystemGroupAction.linSolRep_quadSolAction_commute`, `PureU1.VectorLikeEvenPlane.vectorLikeEven_in_span`, `PureU1.VectorLikeOddPlane.basisa_linear_independent`, `PureU1.Even.lineInCubicPerm_permute`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `PureU1.Even.lineInCubicPerm_in_plane`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `linSolsModule_smul_val`, `PureU1.VectorLikeEvenPlane.basisa_card`, `PureU1.Even.special_case`, `PureU1.VectorLikeEvenPlane.basisa_linear_independent`, `ACCSystemGroupAction.linSolRep_apply_apply_val`, `PureU1.BasisLinear.instFiniteRatLinSolsSucc`, `PureU1.VectorLikeOddPlane.basis_linear_independent`, `ACCSystem.solsInclLinSols_injective`, `PureU1.VectorLikeEvenPlane.basis_linear_independent`
`linearACCs` 📖	CompOp	8 math math: `SM.SMNoGrav_linearACCs`, `LinSols.linearSol`, `SMRHN.SMNoGrav_linearACCs`, `SMRHN.SM_linearACCs`, `SMRHN.PlusU1_linearACCs`, `PureU1_linearACCs`, `MSSMACC_linearACCs`, `ACCSystemGroupAction.linearInvariant`
`numberLinear` 📖	CompOp	6 math math: `SMRHN.SM_numberLinear`, `MSSMACC_numberLinear`, `PureU1_numberLinear`, `SM.SMNoGrav_numberLinear`, `SMRHN.PlusU1_numberLinear`, `SMRHN.SMNoGrav_numberLinear`
`toACCSystemCharges` 📖	CompOp	71 math math: `ACCSystemGroupAction.rep_linSolRep_commute`, `linSolsIncl_injective`, `LinSols.linearSol`, `ACCSystem.solsIncl_injective`, `PureU1.Odd.parameterizationAsLinear_val`, `SMRHN.SM.PlaneSeven.basis_linear_independent`, `PureU1.VectorLikeEvenPlane.P_evenSnd_evenFst`, `PureU1.sort_perm`, `PureU1.sort_apply`, `SMRHN.SM_numberCharges`, `pureU1_cube`, `ACCSystem.Hom.commute`, `MSSMACC.proj_val`, `SMRHN.PlusU1.ElevenPlane.on_accQuad`, `SMRHN.PlusU1.eleven_dim_plane_of_no_sols_exists`, `ACCSystemGroupAction.quadInvariant`, `ACCSystemGroupAction.cubicInvariant`, `linSolsAddCommMonoid_zero_val`, `MSSMACC.planeY₃B₃_val`, `PureU1.VectorLikeOddPlane.span_basis`, `SMRHN.PlusU1.BL.add_quad`, `PureU1.FamilyPermutations_charges_apply`, `PureU1.ConstAbsSorted.AFL_even_below`, `PureU1.Three.cube_for_linSol'`, `PureU1.Even.parameterizationAsLinear_val`, `SMRHN.SM.PlaneSeven.B_in_accCube`, `SMRHN.SM.PlaneSeven.B_sum_is_sol`, `ACCSystemQuad.QuadSols.quadSol`, `PureU1.VectorLikeOddPlane.swap!_as_add`, `PureU1.VectorLikeEvenPlane.P!_in_span`, `SMRHN.PlusU1.Y.add_AF_cube`, `PureU1.ConstAbsSorted.AFL_even_above'`, `PureU1.accCube_invariant`, `SM.SMNoGrav_numberCharges`, `PureU1_numberCharges`, `SMRHN.PlusU1.Y.add_AFL_quad`, `PureU1.accGrav_invariant`, `SMRHN.PlusU1.BL.add_AFL_cube`, `PureU1.chargeMap_apply`, `PureU1.VectorLikeEvenPlane.smul_basis!AsCharges_in_span`, `SMRHN.PlusU1.ElevenPlane.basis_linear_independent`, `SMRHN.PlusU1.ElevenPlane.Bi_sum_quad`, `ACCSystemGroupAction.linearInvariant`, `PureU1.Three.cube_for_linSol`, `SMRHN.PlusU1.Y.add_AFL_cube`, `PureU1.VectorLikeEvenPlane.swap!_as_add`, `PureU1.constAbs_perm`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `linSolsModule_smul_val`, `SMRHN.SMNoGrav_numberCharges`, `PureU1.ConstAbsSorted.AFL_even_above`, `SMRHN.SM.seven_dim_plane_exists`, `SMRHN.PlusU1.exists_plane_exists_basis`, `MSSMACC_numberCharges`, `linSolsAddCommMonoid_add_val`, `linSolsAddCommMonoid_nsmul_val`, `SMRHN.PlusU1.BL.add_AFL_quad`, `ACCSystemGroupAction.rep_solAction_commute`, `SMRHN.PlusU1.Y.add_AFQ_cube`, `ACCSystemGroupAction.linSolRep_apply_apply_val`, `SMRHN.PlusU1_numberCharges`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `ACCSystemQuad.quadSolsIncl_injective`, `PureU1.ConstAbsSorted.AFL_even_below'`, `PureU1.VectorLikeEvenPlane.span_basis`, `PureU1.sum_of_charges`, `PureU1.ConstAbsSorted.is_zero`, `ACCSystem.Sols.cubicSol`, `ACCSystemGroupAction.rep_quadSolAction_commute`, `SMRHN.PlusU1.Y.add_quad`, `PureU1.ConstAbsSorted.boundary_accGrav'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linSolsAddCommMonoid_add_val` 📖	mathematical	—	`LinSols.val` `LinSols` `linSolsAddCommMonoid` `ACCSystemCharges.Charges` `toACCSystemCharges` `ACCSystemCharges.chargesAddCommMonoid`	—	—
`linSolsAddCommMonoid_nsmul_val` 📖	mathematical	—	`LinSols.val` `LinSols` `linSolsAddCommMonoid` `ACCSystemCharges.Charges` `toACCSystemCharges` `ACCSystemCharges.ChargesAddCommGroup`	—	—
`linSolsAddCommMonoid_zero_val` 📖	mathematical	—	`LinSols.val` `LinSols` `linSolsAddCommMonoid` `ACCSystemCharges.Charges` `toACCSystemCharges` `ACCSystemCharges.chargesAddCommMonoid`	—	—
`linSolsIncl_injective` 📖 ⚠️	mathematical	—	`LinSols` `ACCSystemCharges.Charges` `toACCSystemCharges` `linSolsAddCommMonoid` `ACCSystemCharges.chargesAddCommMonoid` `linSolsModule` `ACCSystemCharges.chargesModule` `linSolsIncl`	—	—
`linSolsModule_smul_val` 📖	mathematical	—	`LinSols.val` `LinSols` `linSolsAddCommMonoid` `linSolsModule` `ACCSystemCharges.Charges` `toACCSystemCharges` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule`	—	—

ACCSystemLinear.LinSols

Definitions

Name	Category	Theorems
`val` 📖	CompOp	133 math math: `MSSMACC.α₃_proj`, `PureU1.Odd.lineInCubicPerm_constAbs`, `linearSol`, `PureU1.Odd.parameterizationAsLinear_val`, `PureU1.VectorLikeOddPlane.basis_val`, `PureU1.VectorLikeOddPlane.basis!_val`, `MSSMACC.AnomalyFreePerp.perpB₃`, `SMRHN.PlusU1.BL.on_cubeTriLin`, `SM.SMNoGrav.One.accGrav_Q_neq_zero`, `SMRHN.PlusU1.Y.on_quadBiLin_AFL`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube`, `SM.SMNoGrav.SU3Sol`, `PureU1.Even.parameterizationCharge_cube`, `pureU1_cube`, `PureU1.Three.three_sol_zero`, `PureU1.FamilyPermutations_anomalyFreeLinear_apply`, `pureU1_linear`, `SMRHN.SM.cubeSol`, `PureU1.VectorLikeEvenPlane.P'_val`, `MSSMACC.proj_val`, `ACCSystemLinear.linSolsAddCommMonoid_zero_val`, `SMRHN.PlusU1.BL₁_val`, `SMRHN.PlusU1.Y_val`, `MSSMACC.planeY₃B₃_val`, `SMRHN.SM.gravSol`, `MSSMACC.α₁_proj`, `PureU1.BasisLinear.sum_of_vectors`, `PureU1.VectorLikeEvenPlane.basis_val`, `PureU1.sum_of_anomaly_free_linear`, `SMRHN.SM.SU3Sol`, `PureU1.VectorLikeOddPlane.span_basis`, `MSSMACC.doublePoint_Y₃_B₃`, `MSSMACC.α₂_proj`, `SMRHN.PlusU1.BL.add_quad`, `PureU1.BasisLinear.asLinSols_val`, `SMRHN.PlusU1.Y.on_quadBiLin`, `SM.SMNoGrav.One.accGravSatisfied`, `PureU1.Three.cube_for_linSol'`, `MSSMACC.B₃_val`, `SMRHN.PlusU1.BL.on_quadBiLin_AFL`, `PureU1.Odd.lineInCubicPerm_last_cond`, `PureU1.Even.parameterizationAsLinear_val`, `SM.SMNoGrav.One.E_zero_iff_Q_zero`, `MSSMACC.planeY₃B₃_cubic`, `MSSMACC.lineY₃B₃_doublePoint`, `SMRHN.PlusU1.Y.on_cubeTriLin`, `MSSMACC.AnomalyFreeMk_val`, `PureU1.linesInPlane_four`, `PureU1.linesInPlane_constAbs_four`, `MSSMACC.AnomalyFreePerp.perpY₃`, `ACCSystemQuad.QuadSols.quadSol`, `SMRHN.PlusU1.Y.on_cubeTriLin'`, `PureU1.VectorLikeEvenPlane.P!'_val`, `SMRHN.SMNoGrav.SU2Sol`, `PureU1.VectorLikeOddPlane.swap!_as_add`, `MSSMACC.Y₃_val`, `SMRHN.PlusU1.gravSol`, `MSSMACC.lineQuadAFL_quad`, `MSSMACC.planeY₃B₃_quad`, `PureU1.linesInPlane_eq_sq`, `SMRHN.PlusU1.Y.add_AF_cube`, `PureU1.linesInPlane_eq_sq_four`, `SMRHN.PlusU1.BL_val`, `MSSMACC.lineQuad_cube`, `MSSMACC.cube_proj_proj_B₃`, `MSSMACC.cube_proj_proj_Y₃`, `MSSMACC.lineCube_quad`, `ACCSystemQuad.QuadSols.ext_iff`, `SM.SMNoGrav.SU2Sol`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `PureU1.Even.lineInCubicPerm_constAbs`, `SMRHN.SM.SU2Sol`, `SMRHN.PlusU1.Y.add_AFL_quad`, `MSSMACC.doublePoint_Y₃_Y₃`, `SMRHN.PlusU1.BL.add_AFL_cube`, `PureU1.Even.lineInCubicPerm_last_cond`, `PureU1.VectorLikeEvenPlane.smul_basis!AsCharges_in_span`, `MSSMACC.quadSol`, `SMRHN.PlusU1.YYsol`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `PureU1.Three.cube_for_linSol`, `SMRHN.PlusU1.Y.add_AFL_cube`, `PureU1.linesInPlane_constAbs_AF`, `PureU1.linesInPlane_constAbs`, `PureU1.VectorLikeEvenPlane.swap!_as_add`, `ext_iff`, `MSSMACC.quad_self_proj`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_cube`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `ACCSystemLinear.linSolsModule_smul_val`, `SMRHN.PlusU1.Y₁_val`, `SM.SMNoGrav.One.linearParametersQENeqZero.grav`, `PureU1.VectorLikeOddPlane.P!'_val`, `PureU1.lineInPlaneCond_eq_last`, `SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero`, `SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ`, `MSSMACC.lineY₃B₃Charges_cubic`, `PureU1.VectorLikeEvenPlane.basis!_val`, `SMRHN.PlusU1.cubeSol`, `PureU1.Odd.parameterizationCharge_cube`, `SMRHN.PlusU1.SU2Sol`, `MSSMACC.lineY₃B₃Charges_quad`, `SMRHN.SMNoGrav.SU3Sol`, `MSSMACC.quad_B₃_proj`, `SM.SMNoGrav.One.linearParameters.asLinear_val`, `ACCSystemLinear.linSolsAddCommMonoid_add_val`, `ACCSystemLinear.linSolsAddCommMonoid_nsmul_val`, `SMRHN.SMNoGrav.cubeSol`, `SMRHN.PlusU1.BL.add_AFL_quad`, `PureU1.Even.lineInCubicPerm_vectorLike`, `MSSMACC.cube_proj_proj_self`, `SMRHN.PlusU1.Y.add_AFQ_cube`, `PureU1.VectorLikeOddPlane.P'_val`, `ACCSystemGroupAction.linSolRep_apply_apply_val`, `MSSMACC.cube_proj`, `pureU1_last`, `MSSMACC.doublePoint_B₃_B₃`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `SM.SMNoGrav.cubeSol`, `SMRHN.PlusU1.BL.on_quadBiLin`, `SMRHN.PlusU1.Y.on_cubeTriLin_AFL`, `PureU1.sortAFL_val`, `PureU1.VectorLikeEvenPlane.span_basis`, `SMRHN.PlusU1.BL.on_cubeTriLin_AFL`, `ACCSystem.Sols.cubicSol`, `SMRHN.PlusU1.SU3Sol`, `SMRHN.PlusU1.Y.add_quad`, `MSSMACC.quad_proj`, `SMRHN.PlusU1.quadSol`, `MSSMACC.lineCube_cube`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`
`linearSol` 📖	mathematical	—	`ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystemLinear.linearACCs` `val`	—	—

ACCSystemQuad

Definitions

Name	Category	Theorems
`QuadSols` 📖	CompData	22 math math: `SMRHN.PlusU1.BL.addQuad_zero`, `SMRHN.PlusU1.QuadSol.toQuadInv_generic`, `quadSolsInclLinSols_injective`, `SMRHN.PlusU1.Y.addQuad_zero`, `SMRHN.PlusU1.quadSolToSolInv_α₁_α₂_neq_zero`, `SMRHN.PlusU1.QuadSol.genericToQuad_neq_zero`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_AF`, `ACCSystemGroupAction.linSolRep_quadSolAction_commute`, `MSSMACC.lineQuad_smul`, `ACCSystem.solsInclQuadSols_injective`, `ACCSystemGroupAction.quadSolAction_solAction_commute`, `SMRHN.PlusU1.quadSolToSolInv_rightInverse`, `SMRHN.PlusU1.QuadSol.genericToQuad_on_quad`, `SMRHN.PlusU1.quadSolToSolInv_generic`, `SMRHN.PlusU1.quadSolToSolInv_1`, `SMRHN.PlusU1.quadSolToSolInv_special`, `SMRHN.PlusU1.QuadSol.toQuad_surjective`, `SMRHN.PlusU1.QuadSol.toQuad_rightInverse`, `quadSolsIncl_injective`, `SMRHN.PlusU1.quadSolToSol_surjective`, `SMRHN.PlusU1.quadSolToSolInv_α₁_α₂_zero`, `ACCSystemGroupAction.rep_quadSolAction_commute`
`linSolsInclQuadSolsZero` 📖	CompOp	—
`numberQuadratic` 📖	CompOp	6 math math: `SMRHN.PlusU1_numberQuadratic`, `SM.SMNoGrav_numberQuadratic`, `SMRHN.SM_numberQuadratic`, `MSSMACC_numberQuadratic`, `SMRHN.SMNoGrav_numberQuadratic`, `PureU1_numberQuadratic`
`quadSolsIncl` 📖	CompOp	2 math math: `quadSolsIncl_injective`, `ACCSystemGroupAction.rep_quadSolAction_commute`
`quadSolsInclLinSols` 📖	CompOp	2 math math: `quadSolsInclLinSols_injective`, `ACCSystemGroupAction.linSolRep_quadSolAction_commute`
`quadSolsMulAction` 📖	CompOp	13 math math: `SMRHN.PlusU1.BL.addQuad_zero`, `SMRHN.PlusU1.QuadSol.toQuadInv_generic`, `quadSolsInclLinSols_injective`, `SMRHN.PlusU1.Y.addQuad_zero`, `SMRHN.PlusU1.QuadSol.genericToQuad_neq_zero`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_AF`, `ACCSystemGroupAction.linSolRep_quadSolAction_commute`, `MSSMACC.lineQuad_smul`, `ACCSystem.solsInclQuadSols_injective`, `ACCSystemGroupAction.quadSolAction_solAction_commute`, `SMRHN.PlusU1.QuadSol.genericToQuad_on_quad`, `quadSolsIncl_injective`, `ACCSystemGroupAction.rep_quadSolAction_commute`
`quadraticACCs` 📖	CompOp	8 math math: `SMRHN.SMNoGrav_quadraticACCs`, `PureU1_quadraticACCs`, `ACCSystemGroupAction.quadInvariant`, `SM.SMNoGrav_quadraticACCs`, `SMRHN.SM_quadraticACCs`, `QuadSols.quadSol`, `MSSMACC_quadraticACCs`, `SMRHN.PlusU1_quadraticACCs`
`toACCSystemLinear` 📖	CompOp	205 math math: `MSSMACC.α₃_proj`, `PureU1.Odd.lineInCubicPerm_constAbs`, `ACCSystemGroupAction.rep_linSolRep_commute`, `SM.SMNoGrav_linearACCs`, `ACCSystem.solsIncl_injective`, `PureU1.Odd.parameterizationAsLinear_val`, `SMRHN.SM.PlaneSeven.basis_linear_independent`, `SMRHN.PlusU1.QuadSol.toQuadInv_fst`, `PureU1.VectorLikeOddPlane.basis_val`, `PureU1.VectorLikeOddPlane.basis!_val`, `MSSMACC.AnomalyFreePerp.perpB₃`, `PureU1.VectorLikeOddPlane.basis!_linear_independent`, `PureU1.VectorLikeEvenPlane.P_evenSnd_evenFst`, `SMRHN.PlusU1.BL.on_cubeTriLin`, `MSSMACC.lineCube_smul`, `PureU1.sort_perm`, `PureU1.sort_apply`, `SM.SMNoGrav.One.accGrav_Q_neq_zero`, `SMRHN.SM_numberCharges`, `SMRHN.PlusU1.Y.on_quadBiLin_AFL`, `SMRHN.SMNoGrav_linearACCs`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube`, `SM.SMNoGrav.SU3Sol`, `PureU1.Even.parameterizationCharge_cube`, `pureU1_cube`, `PureU1.Three.three_sol_zero`, `PureU1.lineInPlaneCond_perm`, `PureU1.FamilyPermutations_anomalyFreeLinear_apply`, `pureU1_linear`, `SMRHN.SM_linearACCs`, `SMRHN.PlusU1.QuadSol.toQuadInv_generic`, `quadSolsInclLinSols_injective`, `SMRHN.PlusU1_linearACCs`, `SMRHN.SM.cubeSol`, `SMRHN.SM_numberLinear`, `ACCSystem.Hom.commute`, `PureU1.VectorLikeEvenPlane.P'_val`, `PureU1_linearACCs`, `MSSMACC.proj_val`, `SMRHN.PlusU1.ElevenPlane.on_accQuad`, `SMRHN.PlusU1.eleven_dim_plane_of_no_sols_exists`, `ACCSystemGroupAction.quadInvariant`, `ACCSystemGroupAction.cubicInvariant`, `MSSMACC_numberLinear`, `SMRHN.PlusU1.BL₁_val`, `SMRHN.PlusU1.Y_val`, `MSSMACC.planeY₃B₃_val`, `SMRHN.SM.gravSol`, `MSSMACC.α₁_proj`, `PureU1_numberLinear`, `PureU1.BasisLinear.sum_of_vectors`, `PureU1.VectorLikeEvenPlane.basis_val`, `PureU1.sum_of_anomaly_free_linear`, `SMRHN.SM.SU3Sol`, `PureU1.VectorLikeOddPlane.span_basis`, `MSSMACC.doublePoint_Y₃_B₃`, `MSSMACC.α₂_proj`, `SMRHN.PlusU1.BL.add_quad`, `PureU1.VectorLikeOddPlane.basisa_card`, `PureU1.FamilyPermutations_charges_apply`, `PureU1.BasisLinear.asLinSols_val`, `SMRHN.PlusU1.Y.on_quadBiLin`, `PureU1.Odd.lineInCubicPerm_permute`, `SM.SMNoGrav.One.accGravSatisfied`, `PureU1.Three.cube_for_linSol'`, `MSSMACC.B₃_val`, `SMRHN.PlusU1.BL.on_quadBiLin_AFL`, `PureU1.Odd.lineInCubicPerm_last_cond`, `PureU1.Odd.lineInCubicPerm_zero`, `PureU1.Even.parameterizationAsLinear_val`, `SM.SMNoGrav.One.E_zero_iff_Q_zero`, `MSSMACC.planeY₃B₃_cubic`, `SMRHN.SM.PlaneSeven.B_in_accCube`, `PureU1.VectorLikeEvenPlane.basis!_linear_independent`, `MSSMACC.lineY₃B₃_doublePoint`, `SMRHN.PlusU1.Y.on_cubeTriLin`, `MSSMACC.AnomalyFreeMk_val`, `PureU1.VectorLikeOddPlane.Pa'_P'_P!'`, `SMRHN.SM.PlaneSeven.B_sum_is_sol`, `SMRHN.PlusU1.QuadSol.toQuadInv_special`, `PureU1.BasisLinear.finrank_AnomalyFreeLinear`, `SM.SMNoGrav_numberLinear`, `PureU1.linesInPlane_four`, `PureU1.linesInPlane_constAbs_four`, `ACCSystemGroupAction.linSolRep_solAction_commute`, `MSSMACC.AnomalyFreePerp.perpY₃`, `QuadSols.quadSol`, `SMRHN.PlusU1.Y.on_cubeTriLin'`, `PureU1.VectorLikeEvenPlane.P!'_val`, `SMRHN.SMNoGrav.SU2Sol`, `MSSMACC.planeY₃B₃_smul`, `MSSMACC.Y₃_val`, `ACCSystemGroupAction.linSolRep_quadSolAction_commute`, `SMRHN.PlusU1.gravSol`, `PureU1.VectorLikeEvenPlane.P!_in_span`, `MSSMACC.lineQuadAFL_quad`, `MSSMACC.planeY₃B₃_quad`, `PureU1.linesInPlane_eq_sq`, `SMRHN.PlusU1.Y.add_AF_cube`, `PureU1.linesInPlane_eq_sq_four`, `SMRHN.PlusU1.BL_val`, `MSSMACC.lineQuad_cube`, `PureU1.VectorLikeOddPlane.basisa_linear_independent`, `MSSMACC.cube_proj_proj_B₃`, `MSSMACC.cube_proj_proj_Y₃`, `MSSMACC.lineCube_quad`, `QuadSols.ext_iff`, `SM.SMNoGrav.SU2Sol`, `PureU1.Even.lineInCubicPerm_permute`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `MSSMACC_linearACCs`, `PureU1.Even.lineInCubicPerm_constAbs`, `PureU1.accCube_invariant`, `SM.SMNoGrav_numberCharges`, `PureU1.One.solEqZero`, `PureU1_numberCharges`, `SMRHN.SM.SU2Sol`, `SMRHN.PlusU1.Y.add_AFL_quad`, `PureU1.Even.lineInCubicPerm_in_plane`, `MSSMACC.doublePoint_Y₃_Y₃`, `PureU1.accGrav_invariant`, `SMRHN.PlusU1.BL.add_AFL_cube`, `PureU1.VectorLikeEvenPlane.Pa'_P'_P!'`, `PureU1.chargeMap_apply`, `PureU1.Even.lineInCubicPerm_last_cond`, `PureU1.VectorLikeEvenPlane.smul_basis!AsCharges_in_span`, `MSSMACC.quadSol`, `SMRHN.PlusU1.YYsol`, `SMRHN.PlusU1.ElevenPlane.basis_linear_independent`, `SMRHN.PlusU1.ElevenPlane.Bi_sum_quad`, `ACCSystemGroupAction.linearInvariant`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `PureU1.Three.cube_for_linSol`, `SMRHN.PlusU1.Y.add_AFL_cube`, `PureU1.linesInPlane_constAbs_AF`, `PureU1.linesInPlane_constAbs`, `SMRHN.PlusU1.QuadSol.toQuad_surjective`, `SMRHN.PlusU1.QuadSol.toQuad_rightInverse`, `MSSMACC.quad_self_proj`, `PureU1.constAbs_perm`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_cube`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `SMRHN.SMNoGrav_numberCharges`, `SMRHN.PlusU1.Y₁_val`, `PureU1.VectorLikeEvenPlane.basisa_card`, `SM.SMNoGrav.One.linearParametersQENeqZero.grav`, `PureU1.VectorLikeOddPlane.P!'_val`, `PureU1.lineInPlaneCond_eq_last`, `SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero`, `SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ`, `MSSMACC.lineY₃B₃Charges_cubic`, `PureU1.VectorLikeEvenPlane.basis!_val`, `SMRHN.PlusU1.cubeSol`, `PureU1.Odd.parameterizationCharge_cube`, `SMRHN.PlusU1.SU2Sol`, `MSSMACC.lineY₃B₃Charges_quad`, `SMRHN.SMNoGrav.SU3Sol`, `MSSMACC.quad_B₃_proj`, `SMRHN.SM.seven_dim_plane_exists`, `SM.SMNoGrav.One.linearParameters.asLinear_val`, `SMRHN.PlusU1.exists_plane_exists_basis`, `MSSMACC_numberCharges`, `PureU1.Even.special_case`, `PureU1.VectorLikeEvenPlane.basisa_linear_independent`, `SMRHN.SMNoGrav.cubeSol`, `SMRHN.PlusU1.BL.add_AFL_quad`, `PureU1.Even.lineInCubicPerm_vectorLike`, `ACCSystemGroupAction.rep_solAction_commute`, `MSSMACC.cube_proj_proj_self`, `SMRHN.PlusU1.Y.add_AFQ_cube`, `PureU1.VectorLikeOddPlane.P'_val`, `ACCSystemGroupAction.linSolRep_apply_apply_val`, `SMRHN.PlusU1_numberCharges`, `MSSMACC.cube_proj`, `PureU1.BasisLinear.instFiniteRatLinSolsSucc`, `pureU1_last`, `SMRHN.PlusU1_numberLinear`, `MSSMACC.doublePoint_B₃_B₃`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `quadSolsIncl_injective`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `SM.SMNoGrav.cubeSol`, `PureU1.Odd.special_case`, `SMRHN.PlusU1.BL.on_quadBiLin`, `SMRHN.PlusU1.Y.on_cubeTriLin_AFL`, `PureU1.sortAFL_val`, `PureU1.VectorLikeEvenPlane.span_basis`, `PureU1.sum_of_charges`, `SMRHN.PlusU1.BL.on_cubeTriLin_AFL`, `SMRHN.SMNoGrav_numberLinear`, `PureU1.ConstAbsSorted.is_zero`, `ACCSystem.Sols.cubicSol`, `ACCSystemGroupAction.rep_quadSolAction_commute`, `SMRHN.PlusU1.SU3Sol`, `SMRHN.PlusU1.QuadSol.toQuadInv_α₁_α₂`, `PureU1.VectorLikeOddPlane.basis_linear_independent`, `SMRHN.PlusU1.Y.add_quad`, `MSSMACC.quad_proj`, `ACCSystem.solsInclLinSols_injective`, `PureU1.VectorLikeEvenPlane.basis_linear_independent`, `PureU1.ConstAbsSorted.boundary_accGrav'`, `SMRHN.PlusU1.quadSol`, `MSSMACC.lineCube_cube`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quadSolsInclLinSols_injective` 📖	mathematical	—	`QuadSols` `ACCSystemLinear.LinSols` `toACCSystemLinear` `quadSolsMulAction` `ACCSystemLinear.linSolsAddCommGroup` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule` `quadSolsInclLinSols`	—	`QuadSols.ext`
`quadSolsIncl_injective` 📖	mathematical	—	`QuadSols` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `toACCSystemLinear` `quadSolsMulAction` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `quadSolsIncl`	—	`ACCSystemLinear.linSolsIncl_injective` `quadSolsInclLinSols_injective`

ACCSystemQuad.QuadSols

Definitions

Name	Category	Theorems
`toLinSols` 📖	CompOp	85 math math: `MSSMACC.α₃_proj`, `SMRHN.PlusU1.QuadSol.toQuadInv_fst`, `MSSMACC.AnomalyFreePerp.perpB₃`, `SMRHN.PlusU1.BL.on_cubeTriLin`, `SM.SMNoGrav.One.accGrav_Q_neq_zero`, `SMRHN.PlusU1.Y.on_quadBiLin_AFL`, `MSSMACC.AnomalyFreePerp.inQuadSolProp_iff_proj_inQuadProp`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube`, `pureU1_cube`, `PureU1.Three.three_sol_zero`, `SMRHN.SM.cubeSol`, `MSSMACC.proj_val`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_eq_planeY₃B₃_on_α`, `SMRHN.PlusU1.BL₁_val`, `SMRHN.PlusU1.Y_val`, `MSSMACC.planeY₃B₃_val`, `MSSMACC.α₁_proj`, `MSSMACC.doublePoint_Y₃_B₃`, `MSSMACC.α₂_proj`, `SMRHN.PlusU1.BL.add_quad`, `SMRHN.PlusU1.Y.on_quadBiLin`, `MSSMACC.AnomalyFreePerp.linEqPropSol_iff_proj_linEqProp`, `SM.SMNoGrav.One.accGravSatisfied`, `MSSMACC.B₃_val`, `SMRHN.PlusU1.BL.on_quadBiLin_AFL`, `SM.SMNoGrav.One.E_zero_iff_Q_zero`, `MSSMACC.planeY₃B₃_cubic`, `MSSMACC.lineY₃B₃_doublePoint`, `SMRHN.PlusU1.Y.on_cubeTriLin`, `MSSMACC.AnomalyFreeMk_val`, `SMRHN.PlusU1.QuadSol.genericToQuad_neq_zero`, `MSSMACC.AnomalyFreePerp.perpY₃`, `quadSol`, `SMRHN.PlusU1.Y.on_cubeTriLin'`, `MSSMACC.Y₃_val`, `SMRHN.PlusU1.QuadSol.α₂_AFQ`, `MSSMACC.planeY₃B₃_quad`, `SMRHN.PlusU1.Y.add_AF_cube`, `SMRHN.PlusU1.BL_val`, `PureU1.Even.special_case_lineInCubic`, `MSSMACC.lineQuad_cube`, `MSSMACC.cube_proj_proj_B₃`, `MSSMACC.cube_proj_proj_Y₃`, `MSSMACC.lineCube_quad`, `ext_iff`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `SMRHN.PlusU1.QuadSol.genericToQuad_on_quad`, `SMRHN.PlusU1.Y.add_AFL_quad`, `MSSMACC.doublePoint_Y₃_Y₃`, `SMRHN.PlusU1.BL.add_AFL_cube`, `MSSMACC.quadSol`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `SMRHN.PlusU1.Y.add_AFL_cube`, `PureU1.Even.special_case_lineInCubic_perm`, `MSSMACC.quad_self_proj`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_cube`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `SMRHN.PlusU1.Y₁_val`, `SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero`, `PureU1.Odd.special_case_lineInCubic_perm`, `SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ`, `SMRHN.PlusU1.cubeSol`, `MSSMACC.AnomalyFreePerp.inCubeSolProp_iff_proj_inCubeProp`, `MSSMACC.quad_B₃_proj`, `PureU1.Even.special_case`, `SMRHN.SMNoGrav.cubeSol`, `SMRHN.PlusU1.BL.add_AFL_quad`, `MSSMACC.cube_proj_proj_self`, `SMRHN.PlusU1.Y.add_AFQ_cube`, `MSSMACC.cube_proj`, `MSSMACC.doublePoint_B₃_B₃`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `SM.SMNoGrav.cubeSol`, `PureU1.Odd.special_case`, `SMRHN.PlusU1.BL.on_quadBiLin`, `SMRHN.PlusU1.Y.on_cubeTriLin_AFL`, `SMRHN.PlusU1.BL.on_cubeTriLin_AFL`, `ACCSystem.Sols.cubicSol`, `SMRHN.PlusU1.QuadSol.toQuadInv_α₁_α₂`, `SMRHN.PlusU1.Y.add_quad`, `MSSMACC.quad_proj`, `PureU1.Odd.special_case_lineInCubic`, `SMRHN.PlusU1.quadSol`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `toLinSols`	—	—	`ACCSystemLinear.LinSols.ext`
`ext_iff` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `toLinSols`	—	`ext`
`quadSol` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `ACCSystemQuad.quadraticACCs` `ACCSystemLinear.LinSols.val` `toLinSols`	—	—

(root)

Definitions

Name	Category	Theorems
`ACCSystem` 📖	CompData	—
`ACCSystemCharges` 📖	CompData	—
`ACCSystemChargesMk` 📖	CompOp	—
`ACCSystemLinear` 📖	CompData	—
`ACCSystemQuad` 📖	CompData	—

---

← Back to Index