Documentation Verification Report

HyperCharge

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

Statistics

Metric	Count
Definitions `Y`, `addCube`, `addQuad`, `Y₁`	4
Theorems `addQuad_zero`, `add_AFL_cube`, `add_AFL_quad`, `add_AFQ_cube`, `add_AF_cube`, `add_quad`, `on_cubeTriLin`, `on_cubeTriLin'`, `on_cubeTriLin'_ALQ`, `on_cubeTriLin_AFL`, `on_quadBiLin`, `on_quadBiLin_AFL`, `Y_val`, `Y₁_val`	14
Total	18

SMRHN.PlusU1

Definitions

Name	Category	Theorems
`Y` 📖	CompOp	12 math math: `Y.on_quadBiLin_AFL`, `Y_val`, `Y.on_quadBiLin`, `Y.on_cubeTriLin`, `Y.on_cubeTriLin'`, `Y.add_AF_cube`, `Y.add_AFL_quad`, `Y.add_AFL_cube`, `Y.on_cubeTriLin'_ALQ`, `Y.add_AFQ_cube`, `Y.on_cubeTriLin_AFL`, `Y.add_quad`
`Y₁` 📖	CompOp	2 math math: `Y_val`, `Y₁_val`

Theorems

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

SMRHN.PlusU1.Y

Definitions

Name	Category	Theorems
`addCube` 📖	CompOp	—
`addQuad` 📖	CompOp	1 math math: `addQuad_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.Y` `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.Y`	—	`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_AFQ_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.Y`	—	`add_AFL_cube` `TriLinearSymm.swap₃` `on_cubeTriLin'_ALQ`
`add_AF_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.Y`	—	`add_AFQ_cube` `SMRHN.PlusU1.cubeSol`
`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.Y`	—	`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.Y` `SMνACCs.accYY`	—	`SMRHN.familyUniversal_cubeTriLin'` `SMνACCs.accYY_decomp`
`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.Y` `HomogeneousQuadratic` `HomogeneousQuadratic.instFun` `SMνACCs.accQuad`	—	`SMRHN.familyUniversal_cubeTriLin` `SMνACCs.accQuad_decomp`
`on_cubeTriLin'_ALQ` 📖	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.Y`	—	`on_cubeTriLin'` `SMRHN.PlusU1.quadSol`
`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.Y`	—	`on_cubeTriLin` `SMRHN.PlusU1.YYsol`
`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.Y` `SMνACCs.accYY`	—	`SMRHN.familyUniversal_quadBiLin` `SMνACCs.accYY_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.Y`	—	`on_quadBiLin` `SMRHN.PlusU1.YYsol`

---

← Back to Index