Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `PlusU1`, `chargeToAF`, `chargeToLinear`, `chargeToQuad`, `linearToAF`, `linearToQuad`, `perm`, `quadToAF`	8
Theorems `SU2Sol`, `SU3Sol`, `YYsol`, `cubeSol`, `gravSol`, `quadSol`, `PlusU1_cubicACC_apply`, `PlusU1_linearACCs`, `PlusU1_numberCharges`, `PlusU1_numberLinear`, `PlusU1_numberQuadratic`, `PlusU1_quadraticACCs`	12
Total	20

SMRHN

Definitions

Name	Category	Theorems
`PlusU1` 📖	CompOp	63 math math: `PlusU1.QuadSol.toQuadInv_fst`, `PlusU1_numberQuadratic`, `PlusU1.BL.on_cubeTriLin`, `PlusU1.Y.on_quadBiLin_AFL`, `PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube`, `PlusU1.BL.addQuad_zero`, `PlusU1.QuadSol.toQuadInv_generic`, `PlusU1_linearACCs`, `PlusU1.Y.addQuad_zero`, `PlusU1.quadSolToSolInv_α₁_α₂_neq_zero`, `PlusU1.ElevenPlane.on_accQuad`, `PlusU1.eleven_dim_plane_of_no_sols_exists`, `PlusU1.BL₁_val`, `PlusU1.Y_val`, `PlusU1.QuadSolToSol.generic_on_AF`, `PlusU1.BL.add_quad`, `PlusU1.Y.on_quadBiLin`, `PlusU1.BL.on_quadBiLin_AFL`, `PlusU1.Y.on_cubeTriLin`, `PlusU1.QuadSolToSol.generic_on_AF_α₁_ne_zero`, `PlusU1.QuadSol.genericToQuad_neq_zero`, `PlusU1.Y.on_cubeTriLin'`, `PlusU1.QuadSolToSol.BL_add_α₁_α₂_AF`, `PlusU1.gravSol`, `PlusU1.QuadSol.α₂_AFQ`, `PlusU1_cubicACC_apply`, `PlusU1.Y.add_AF_cube`, `PlusU1.BL_val`, `PlusU1.quadSolToSolInv_rightInverse`, `PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `PlusU1.QuadSol.genericToQuad_on_quad`, `PlusU1.Y.add_AFL_quad`, `PlusU1.BL.add_AFL_cube`, `PlusU1.quadSolToSolInv_generic`, `PlusU1.YYsol`, `PlusU1.ElevenPlane.basis_linear_independent`, `PlusU1.ElevenPlane.Bi_sum_quad`, `PlusU1.QuadSol.accQuad_α₁_α₂`, `PlusU1.Y.add_AFL_cube`, `PlusU1.quadSolToSolInv_1`, `PlusU1.QuadSol.toQuad_surjective`, `PlusU1.QuadSol.toQuad_rightInverse`, `PlusU1_quadraticACCs`, `PlusU1.Y₁_val`, `PlusU1.QuadSolToSol.cube_α₁_α₂_zero`, `PlusU1.Y.on_cubeTriLin'_ALQ`, `PlusU1.cubeSol`, `PlusU1.SU2Sol`, `PlusU1.exists_plane_exists_basis`, `PlusU1.QuadSolToSol.α₂_AF`, `PlusU1.BL.add_AFL_quad`, `PlusU1.Y.add_AFQ_cube`, `PlusU1_numberCharges`, `PlusU1_numberLinear`, `PlusU1.QuadSol.add_AFL_quad`, `PlusU1.BL.on_quadBiLin`, `PlusU1.Y.on_cubeTriLin_AFL`, `PlusU1.quadSolToSol_surjective`, `PlusU1.BL.on_cubeTriLin_AFL`, `PlusU1.SU3Sol`, `PlusU1.QuadSol.toQuadInv_α₁_α₂`, `PlusU1.Y.add_quad`, `PlusU1.quadSol`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`PlusU1_cubicACC_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystem.cubicACC` `PlusU1`	—	—
`PlusU1_linearACCs` 📖	mathematical	—	`ACCSystemLinear.linearACCs` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PlusU1` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule`	—	—
`PlusU1_numberCharges` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PlusU1`	—	—
`PlusU1_numberLinear` 📖	mathematical	—	`ACCSystemLinear.numberLinear` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PlusU1`	—	—
`PlusU1_numberQuadratic` 📖	mathematical	—	`ACCSystemQuad.numberQuadratic` `ACCSystem.toACCSystemQuad` `PlusU1`	—	—
`PlusU1_quadraticACCs` 📖	mathematical	—	`ACCSystemQuad.quadraticACCs` `ACCSystem.toACCSystemQuad` `PlusU1` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm.toHomogeneousQuad` `SMνACCs.quadBiLin`	—	—

SMRHN.PlusU1

Definitions

Name	Category	Theorems
`chargeToAF` 📖	CompOp	—
`chargeToLinear` 📖	CompOp	—
`chargeToQuad` 📖	CompOp	—
`linearToAF` 📖	CompOp	—
`linearToQuad` 📖	CompOp	—
`perm` 📖	CompOp	—
`quadToAF` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SU2Sol` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνACCs.accSU2` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1`	—	`ACCSystemLinear.LinSols.linearSol`
`SU3Sol` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνACCs.accSU3` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1`	—	`ACCSystemLinear.LinSols.linearSol`
`YYsol` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνACCs.accYY` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1`	—	`ACCSystemLinear.LinSols.linearSol`
`cubeSol` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `SMνACCs.accCube` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols`	—	`ACCSystem.Sols.cubicSol`
`gravSol` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνACCs.accGrav` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1`	—	`ACCSystemLinear.LinSols.linearSol`
`quadSol` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `SMνACCs.accQuad` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.QuadSols.toLinSols`	—	`ACCSystemQuad.QuadSols.quadSol`

---

← Back to Index