Documentation Verification Report

PlaneWithY3B3

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

Statistics

Metric	Count
Definitions `lineCube`, `lineQuad`, `lineQuadAFL`, `planeY₃B₃`, `α₁`, `α₂`, `α₃`	7
Theorems `lineCube_cube`, `lineCube_quad`, `lineCube_smul`, `lineQuadAFL_quad`, `lineQuad_cube`, `lineQuad_smul`, `lineQuad_val`, `planeY₃B₃_cubic`, `planeY₃B₃_eq`, `planeY₃B₃_quad`, `planeY₃B₃_smul`, `planeY₃B₃_val`, `planeY₃B₃_val_eq'`, `α₁_proj`, `α₁_proj_zero`, `α₂_proj`, `α₂_proj_zero`, `α₃_proj`	18
Total	25

MSSMACC

Definitions

Name	Category	Theorems
`lineCube` 📖	CompOp	3 math math: `lineCube_smul`, `lineCube_quad`, `lineCube_cube`
`lineQuad` 📖	CompOp	3 math math: `lineQuad_cube`, `lineQuad_smul`, `lineQuad_val`
`lineQuadAFL` 📖	CompOp	1 math math: `lineQuadAFL_quad`
`planeY₃B₃` 📖	CompOp	7 math math: `AnomalyFreePerp.toSolNSQuad_eq_planeY₃B₃_on_α`, `planeY₃B₃_val`, `planeY₃B₃_cubic`, `planeY₃B₃_smul`, `planeY₃B₃_quad`, `lineQuad_val`, `planeY₃B₃_eq`
`α₁` 📖	CompOp	5 math math: `AnomalyFreePerp.toSolNSQuad_eq_planeY₃B₃_on_α`, `α₁_proj`, `α₁_proj_zero`, `lineQuad_cube`, `lineCube_quad`
`α₂` 📖	CompOp	5 math math: `AnomalyFreePerp.toSolNSQuad_eq_planeY₃B₃_on_α`, `α₂_proj`, `lineQuad_cube`, `lineCube_quad`, `α₂_proj_zero`
`α₃` 📖	CompOp	6 math math: `α₃_proj`, `AnomalyFreePerp.toSolNSQuad_eq_planeY₃B₃_on_α`, `α₁_proj`, `α₂_proj`, `lineQuad_cube`, `lineCube_quad`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lineCube_cube` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `MSSMACCs.accCube` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `lineCube`	—	`lineCube.eq_1` `planeY₃B₃_cubic`
`lineCube_quad` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `MSSMACCs.accQuad` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `lineCube` `TriLinearSymm` `TriLinearSymm.instFun` `MSSMACCs.cubeTriLin` `AnomalyFreePerp.toLinSols` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `B₃` `Y₃` `α₁` `α₂` `α₃`	—	`lineCube.eq_1` `planeY₃B₃_quad` `α₁.eq_1` `α₂.eq_1` `α₃.eq_1`
`lineCube_smul` 📖	mathematical	—	`lineCube` `ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemLinear.linSolsAddCommGroup` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule`	—	`ACCSystemLinear.LinSols.ext` `planeY₃B₃_smul`
`lineQuadAFL_quad` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `MSSMACCs.accQuad` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `lineQuadAFL`	—	`lineQuadAFL.eq_1` `planeY₃B₃_quad`
`lineQuad_cube` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `MSSMACCs.accCube` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols` `lineQuad` `BiLinearSymm` `BiLinearSymm.instFun` `MSSMACCs.quadBiLin` `ACCSystem.Sols.toQuadSols` `B₃` `AnomalyFreePerp.toLinSols` `Y₃` `α₁` `α₂` `α₃`	—	`lineQuad_val` `planeY₃B₃_cubic` `α₁.eq_1` `α₂.eq_1` `α₃.eq_1`
`lineQuad_smul` 📖	mathematical	—	`lineQuad` `ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.quadSolsMulAction`	—	`ACCSystemQuad.QuadSols.ext` `planeY₃B₃_smul` `lineQuad_val`
`lineQuad_val` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols` `lineQuad` `planeY₃B₃` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `MSSMACCs.quadBiLin` `AnomalyFreePerp.toLinSols` `ACCSystem.Sols.toQuadSols` `B₃` `Y₃`	—	—
`planeY₃B₃_cubic` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `MSSMACCs.accCube` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `planeY₃B₃` `TriLinearSymm` `TriLinearSymm.instFun` `MSSMACCs.cubeTriLin` `AnomalyFreePerp.toLinSols` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `Y₃` `B₃`	—	`planeY₃B₃_val` `MSSMACCs.accCube.eq_1` `TriLinearSymm.toCubic_add` `lineY₃B₃Charges_cubic` `lineY₃B₃_doublePoint` `HomogeneousCubic.map_smul` `TriLinearSymm.map_smul₁` `TriLinearSymm.map_smul₂` `TriLinearSymm.map_add₃` `TriLinearSymm.map_smul₃`
`planeY₃B₃_eq` 📖	mathematical	—	`planeY₃B₃`	—	—
`planeY₃B₃_quad` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `MSSMACCs.accQuad` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `planeY₃B₃` `BiLinearSymm` `BiLinearSymm.instFun` `MSSMACCs.quadBiLin` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `Y₃` `AnomalyFreePerp.toLinSols` `B₃`	—	`planeY₃B₃_val` `MSSMACCs.accQuad.eq_1` `BiLinearSymm.toHomogeneousQuad_add` `lineY₃B₃Charges_quad` `HomogeneousQuadratic.map_smul` `BiLinearSymm.map_add₁` `BiLinearSymm.map_smul₁` `BiLinearSymm.map_smul₂`
`planeY₃B₃_smul` 📖	mathematical	—	`planeY₃B₃` `ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemLinear.linSolsAddCommGroup` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule`	—	`ACCSystemLinear.LinSols.ext` `planeY₃B₃_val`
`planeY₃B₃_val` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `planeY₃B₃` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `Y₃` `B₃` `AnomalyFreePerp.toLinSols`	—	—
`planeY₃B₃_val_eq'` 📖	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `planeY₃B₃`	—	—	`planeY₃B₃_val` `AnomalyFreePerp.perpY₃` `BiLinearSymm.map_smul₂` `BiLinearSymm.map_add₂` `AnomalyFreePerp.perpB₃`
`α₁_proj` 📖	mathematical	—	`α₁` `proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystem.Sols.toQuadSols` `α₃` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `dot` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `B₃` `Y₃`	—	`α₃_proj` `α₁.eq_1` `cube_proj_proj_B₃` `quad_B₃_proj` `quad_proj` `cube_proj`
`α₁_proj_zero` 📖	mathematical	`α₃` `proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystem.Sols.toQuadSols`	`α₁`	—	`α₁_proj`
`α₂_proj` 📖	mathematical	—	`α₂` `proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystem.Sols.toQuadSols` `α₃` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `dot` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `Y₃` `B₃`	—	`α₃_proj` `α₂.eq_1` `cube_proj_proj_Y₃` `quad_Y₃_proj` `quad_proj` `cube_proj`
`α₂_proj_zero` 📖	mathematical	`α₃` `proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystem.Sols.toQuadSols`	`α₂`	—	`α₂_proj`
`α₃_proj` 📖	mathematical	—	`α₃` `proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystem.Sols.toQuadSols` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `dot` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `Y₃` `B₃` `TriLinearSymm` `TriLinearSymm.instFun` `MSSMACCs.cubeTriLin` `MSSMACCs.quadBiLin`	—	`α₃.eq_1` `cube_proj_proj_Y₃` `cube_proj_proj_B₃` `quad_B₃_proj` `quad_Y₃_proj`

---

← Back to Index