Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `SMNoGrav`, `chargeToAF`, `chargeToLinear`, `chargeToQuad`, `linearToAF`, `linearToQuad`, `perm`, `quadToAF`	8
Theorems `SU2Sol`, `SU3Sol`, `cubeSol`, `SMNoGrav_cubicACC_apply`, `SMNoGrav_linearACCs`, `SMNoGrav_numberCharges`, `SMNoGrav_numberLinear`, `SMNoGrav_numberQuadratic`, `SMNoGrav_quadraticACCs`	9
Total	17

SMRHN

Definitions

Name	Category	Theorems
`SMNoGrav` 📖	CompOp	9 math math: `SMNoGrav_quadraticACCs`, `SMNoGrav_linearACCs`, `SMNoGrav_numberQuadratic`, `SMNoGrav_cubicACC_apply`, `SMNoGrav.SU2Sol`, `SMNoGrav_numberCharges`, `SMNoGrav.SU3Sol`, `SMNoGrav.cubeSol`, `SMNoGrav_numberLinear`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SMNoGrav_cubicACC_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystem.cubicACC` `SMNoGrav`	—	—
`SMNoGrav_linearACCs` 📖	mathematical	—	`ACCSystemLinear.linearACCs` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMNoGrav` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule`	—	—
`SMNoGrav_numberCharges` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMNoGrav`	—	—
`SMNoGrav_numberLinear` 📖	mathematical	—	`ACCSystemLinear.numberLinear` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMNoGrav`	—	—
`SMNoGrav_numberQuadratic` 📖	mathematical	—	`ACCSystemQuad.numberQuadratic` `ACCSystem.toACCSystemQuad` `SMNoGrav`	—	—
`SMNoGrav_quadraticACCs` 📖	mathematical	—	`ACCSystemQuad.quadraticACCs` `ACCSystem.toACCSystemQuad` `SMNoGrav` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule`	—	—

SMRHN.SMNoGrav

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.SMNoGrav`	—	`ACCSystemLinear.LinSols.linearSol`
`SU3Sol` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνACCs.accSU3` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.SMNoGrav`	—	`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.SMNoGrav` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols`	—	`ACCSystem.Sols.cubicSol`

---

← Back to Index