Documentation Verification Report

BMinusL

📁 Source: PhysLean/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/BMinusL.lean

Statistics

Metric	Count
Definitions `BL`, `addQuad`, `BL₁`	3
Theorems `addQuad_zero`, `add_AFL_cube`, `add_AFL_quad`, `add_quad`, `on_cubeTriLin`, `on_cubeTriLin_AFL`, `on_quadBiLin`, `on_quadBiLin_AFL`, `BL_val`, `BL₁_val`	10
Total	13

SMRHN.PlusU1

Definitions

Name	Category	Theorems
`BL` 📖	CompOp	8 math math: `BL.on_cubeTriLin`, `BL.add_quad`, `BL.on_quadBiLin_AFL`, `BL_val`, `BL.add_AFL_cube`, `BL.add_AFL_quad`, `BL.on_quadBiLin`, `BL.on_cubeTriLin_AFL`
`BL₁` 📖	CompOp	2 math math: `BL₁_val`, `BL_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`BL_val` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `BL` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMRHN.familyUniversal` `BL₁`	—	—
`BL₁_val` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `BL₁`	—	—

SMRHN.PlusU1.BL

Definitions

Name	Category	Theorems
`addQuad` 📖	CompOp	4 math math: `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube`, `addQuad_zero`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_AF`, `SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addQuad_zero` 📖	mathematical	—	`addQuad` `ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.quadSolsMulAction`	—	`add_quad`
`add_AFL_cube` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `SMνACCs.accCube` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1.BL` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin`	—	`TriLinearSymm.toCubic_add` `SMRHN.PlusU1.cubeSol` `HomogeneousCubic.map_smul` `TriLinearSymm.map_smul₁` `TriLinearSymm.map_smul₂` `TriLinearSymm.map_smul₃` `on_cubeTriLin_AFL`
`add_AFL_quad` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `SMνACCs.accQuad` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1.BL`	—	`BiLinearSymm.toHomogeneousQuad_add` `SMRHN.PlusU1.quadSol` `BiLinearSymm.map_smul₁` `BiLinearSymm.map_smul₂` `BiLinearSymm.swap` `on_quadBiLin_AFL` `HomogeneousQuadratic.map_smul` `SMνACCs.quadBiLin_toFun_apply`
`add_quad` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `SMνACCs.accQuad` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1.BL`	—	`add_AFL_quad` `SMRHN.PlusU1.quadSol`
`on_cubeTriLin` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1.BL` `SMνACCs.accGrav` `SMνACCs.accSU3`	—	`SMRHN.familyUniversal_cubeTriLin'` `SMνACCs.accGrav_decomp` `SMνACCs.accSU3_decomp`
`on_cubeTriLin_AFL` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1.BL`	—	`on_cubeTriLin` `SMRHN.PlusU1.gravSol` `SMRHN.PlusU1.SU3Sol`
`on_quadBiLin` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `SMνACCs.quadBiLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1.BL` `SMνACCs.accYY` `SMνACCs.accSU2` `SMνACCs.accSU3`	—	`SMRHN.familyUniversal_quadBiLin` `SMνACCs.accYY_decomp` `SMνACCs.accSU2_decomp` `SMνACCs.accSU3_decomp`
`on_quadBiLin_AFL` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `SMνACCs.quadBiLin` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1.BL`	—	`on_quadBiLin` `SMRHN.PlusU1.YYsol` `SMRHN.PlusU1.SU2Sol` `SMRHN.PlusU1.SU3Sol`

---

← Back to Index