Documentation Verification Report

B3

📁 Source: PhysLean/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/B3.lean

Statistics

Metric	Count
Definitions `B₃`, `B₃AsCharge`	2
Theorems `B₃_val`, `doublePoint_B₃_B₃`	2
Total	4

MSSMACC

Definitions

Name	Category	Theorems
`B₃` 📖	CompOp	23 math math: `α₃_proj`, `AnomalyFreePerp.perpB₃`, `proj_val`, `planeY₃B₃_val`, `α₁_proj`, `doublePoint_Y₃_B₃`, `α₂_proj`, `B₃_val`, `planeY₃B₃_cubic`, `planeY₃B₃_quad`, `lineQuad_cube`, `cube_proj_proj_B₃`, `cube_proj_proj_Y₃`, `lineCube_quad`, `quad_self_proj`, `Y₃_plus_B₃_plus_proj`, `quad_B₃_proj`, `cube_proj_proj_self`, `cube_proj`, `doublePoint_B₃_B₃`, `lineQuad_val`, `quad_Y₃_proj`, `quad_proj`
`B₃AsCharge` 📖	CompOp	1 math math: `B₃_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`B₃_val` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `B₃` `B₃AsCharge`	—	—
`doublePoint_B₃_B₃` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `MSSMACCs.cubeTriLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `B₃`	—	`B₃_val` `B₃AsCharge.eq_1` `MSSMCharges.toSMSpecies_toSpecies_inv` `MSSMCharges.Hd_toSpecies_inv` `MSSMCharges.Hu_toSpecies_inv` `ACCSystemLinear.LinSols.linearSol`

---

← Back to Index