Documentation Verification Report

LineY3B3

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

Statistics

Metric	Count
Definitions `lineY₃B₃`, `lineY₃B₃Charges`	2
Theorems `doublePoint_Y₃_B₃`, `lineY₃B₃Charges_cubic`, `lineY₃B₃Charges_quad`, `lineY₃B₃_doublePoint`	4
Total	6

MSSMACC

Definitions

Name	Category	Theorems
`lineY₃B₃` 📖	CompOp	1 math math: `lineY₃B₃_doublePoint`
`lineY₃B₃Charges` 📖	CompOp	2 math math: `lineY₃B₃Charges_cubic`, `lineY₃B₃Charges_quad`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`doublePoint_Y₃_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` `Y₃` `B₃`	—	`B₃_val` `Y₃_val` `B₃AsCharge.eq_1` `Y₃AsCharge.eq_1` `MSSMCharges.toSMSpecies_toSpecies_inv` `MSSMCharges.Hd_toSpecies_inv` `MSSMCharges.Hu_toSpecies_inv` `ACCSystemLinear.LinSols.linearSol`
`lineY₃B₃Charges_cubic` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `MSSMACCs.accCube` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `lineY₃B₃Charges`	—	`MSSMACCs.accCube.eq_1` `TriLinearSymm.toCubic_add` `HomogeneousCubic.map_smul` `TriLinearSymm.map_smul₁` `TriLinearSymm.map_smul₂` `TriLinearSymm.map_smul₃` `ACCSystem.Sols.cubicSol`
`lineY₃B₃Charges_quad` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `MSSMACCs.accQuad` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `lineY₃B₃Charges`	—	`MSSMACCs.accQuad.eq_1` `BiLinearSymm.toHomogeneousQuad_add` `HomogeneousQuadratic.map_smul` `BiLinearSymm.map_smul₁` `BiLinearSymm.map_smul₂` `quadSol`
`lineY₃B₃_doublePoint` 📖	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` `lineY₃B₃`	—	`TriLinearSymm.map_add₂` `TriLinearSymm.map_add₁` `TriLinearSymm.map_smul₂` `TriLinearSymm.map_smul₁` `doublePoint_B₃_B₃` `doublePoint_Y₃_Y₃` `doublePoint_Y₃_B₃` `TriLinearSymm.swap₁`

---

← Back to Index