Documentation Verification Report

Y3

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

Statistics

Metric	Count
Definitions `Y₃`, `Y₃AsCharge`	2
Theorems `Y₃_val`, `doublePoint_Y₃_Y₃`	2
Total	4

MSSMACC

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Y₃_val` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `Y₃` `Y₃AsCharge`	—	—
`doublePoint_Y₃_Y₃` 📖	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` `Y₃`	—	`Y₃_val` `Y₃AsCharge.eq_1` `MSSMCharges.toSMSpecies_toSpecies_inv` `MSSMCharges.Hd_toSpecies_inv` `MSSMCharges.Hu_toSpecies_inv` `ACCSystemLinear.LinSols.linearSol`

---

← Back to Index