Documentation Verification Report

Basic

📁 Source: PhysLean/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/Basic.lean

Statistics

Metric	Count
Definitions `AnomalyFreePerp`, `toLinSols`, `proj`	3
Theorems `perpB₃`, `perpY₃`, `Y₃_plus_B₃_plus_proj`, `cube_proj`, `cube_proj_proj_B₃`, `cube_proj_proj_Y₃`, `cube_proj_proj_self`, `proj_val`, `quad_B₃_proj`, `quad_Y₃_proj`, `quad_proj`, `quad_self_proj`	12
Total	15

MSSMACC

Definitions

Name	Category	Theorems
`AnomalyFreePerp` 📖	CompData	5 math math: `AnomalyFreePerp.toSol_inQuadCube`, `AnomalyFreePerp.toSol_surjective`, `AnomalyFreePerp.toSol_inLineEq`, `AnomalyFreePerp.toSol_inQuad`, `AnomalyFreePerp.toSol_toSolNSProj`
`proj` 📖	CompOp	18 math math: `α₃_proj`, `AnomalyFreePerp.inQuadSolProp_iff_proj_inQuadProp`, `proj_val`, `α₁_proj`, `α₂_proj`, `AnomalyFreePerp.linEqPropSol_iff_proj_linEqProp`, `α₁_proj_zero`, `cube_proj_proj_B₃`, `cube_proj_proj_Y₃`, `α₂_proj_zero`, `quad_self_proj`, `Y₃_plus_B₃_plus_proj`, `AnomalyFreePerp.inCubeSolProp_iff_proj_inCubeProp`, `quad_B₃_proj`, `cube_proj_proj_self`, `cube_proj`, `quad_Y₃_proj`, `quad_proj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Y₃_plus_B₃_plus_proj` 📖	mathematical	—	`ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `Y₃` `B₃` `AnomalyFreePerp.toLinSols` `proj` `MSSMCharges` `BiLinearSymm` `BiLinearSymm.instFun` `dot`	—	`proj_val`
`cube_proj` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `MSSMACCs.cubeTriLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `AnomalyFreePerp.toLinSols` `proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `BiLinearSymm` `BiLinearSymm.instFun` `dot` `Y₃` `B₃`	—	`proj_val` `TriLinearSymm.map_add₃` `TriLinearSymm.map_smul₃` `cube_proj_proj_Y₃` `cube_proj_proj_B₃` `cube_proj_proj_self`
`cube_proj_proj_B₃` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `MSSMACCs.cubeTriLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `AnomalyFreePerp.toLinSols` `proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `B₃` `BiLinearSymm` `BiLinearSymm.instFun` `dot` `Y₃`	—	`proj_val` `TriLinearSymm.map_add₁` `TriLinearSymm.map_add₂` `lineY₃B₃_doublePoint` `TriLinearSymm.swap₂` `TriLinearSymm.map_smul₁` `TriLinearSymm.map_smul₃` `doublePoint_Y₃_B₃` `TriLinearSymm.swap₁` `doublePoint_B₃_B₃` `TriLinearSymm.map_smul₂`
`cube_proj_proj_Y₃` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `MSSMACCs.cubeTriLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `AnomalyFreePerp.toLinSols` `proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `Y₃` `BiLinearSymm` `BiLinearSymm.instFun` `dot` `B₃`	—	`proj_val` `TriLinearSymm.map_add₁` `TriLinearSymm.map_add₂` `lineY₃B₃_doublePoint` `TriLinearSymm.swap₂` `TriLinearSymm.map_smul₁` `TriLinearSymm.map_smul₃` `doublePoint_Y₃_Y₃` `TriLinearSymm.swap₁` `doublePoint_Y₃_B₃` `TriLinearSymm.map_smul₂`
`cube_proj_proj_self` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `MSSMACCs.cubeTriLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `AnomalyFreePerp.toLinSols` `proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `BiLinearSymm` `BiLinearSymm.instFun` `dot` `Y₃` `B₃`	—	`proj_val` `TriLinearSymm.map_add₁` `TriLinearSymm.map_add₂` `lineY₃B₃_doublePoint` `TriLinearSymm.map_smul₁` `TriLinearSymm.map_smul₂` `ACCSystem.Sols.cubicSol` `TriLinearSymm.swap₁` `TriLinearSymm.swap₂`
`proj_val` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `AnomalyFreePerp.toLinSols` `proj` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `MSSMCharges` `BiLinearSymm` `BiLinearSymm.instFun` `dot` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `B₃` `Y₃`	—	—
`quad_B₃_proj` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `MSSMACCs.quadBiLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `B₃` `AnomalyFreePerp.toLinSols` `proj` `dot` `Y₃`	—	`proj_val` `BiLinearSymm.map_add₂` `BiLinearSymm.map_smul₂`
`quad_Y₃_proj` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `MSSMACCs.quadBiLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `Y₃` `AnomalyFreePerp.toLinSols` `proj` `dot` `B₃`	—	`proj_val` `BiLinearSymm.map_add₂` `BiLinearSymm.map_smul₂`
`quad_proj` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `MSSMACCs.quadBiLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `AnomalyFreePerp.toLinSols` `proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `dot` `Y₃` `B₃`	—	`proj_val` `BiLinearSymm.map_add₁` `BiLinearSymm.map_smul₁` `quad_Y₃_proj` `quad_B₃_proj` `quad_self_proj`
`quad_self_proj` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `MSSMACCs.quadBiLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `AnomalyFreePerp.toLinSols` `proj` `dot` `B₃` `Y₃`	—	`proj_val` `BiLinearSymm.map_add₂` `BiLinearSymm.map_smul₂` `quadSol` `BiLinearSymm.swap`

MSSMACC.AnomalyFreePerp

Definitions

Name	Category	Theorems
`toLinSols` 📖	CompOp	18 math math: `perpB₃`, `MSSMACC.proj_val`, `MSSMACC.planeY₃B₃_val`, `MSSMACC.planeY₃B₃_cubic`, `perpY₃`, `MSSMACC.planeY₃B₃_quad`, `MSSMACC.lineQuad_cube`, `MSSMACC.cube_proj_proj_B₃`, `MSSMACC.cube_proj_proj_Y₃`, `MSSMACC.lineCube_quad`, `MSSMACC.quad_self_proj`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `MSSMACC.quad_B₃_proj`, `MSSMACC.cube_proj_proj_self`, `MSSMACC.cube_proj`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `MSSMACC.quad_proj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`perpB₃` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `MSSMACC.dot` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `MSSMACC.B₃` `toLinSols`	—	—
`perpY₃` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `MSSMACC.dot` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `MSSMACC.Y₃` `toLinSols`	—	—

---

← Back to Index