Documentation Verification Report

Basic

📁 Source: PhysLean/Particles/StandardModel/AnomalyCancellation/NoGrav/Basic.lean

Statistics

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

SM

Definitions

Name	Category	Theorems
`SMNoGrav` 📖	CompOp	15 math math: `SMNoGrav_linearACCs`, `SMNoGrav_numberQuadratic`, `SMNoGrav.One.accGrav_Q_neq_zero`, `SMNoGrav.SU3Sol`, `SMNoGrav_cubicACC_apply`, `SMNoGrav_quadraticACCs`, `SMNoGrav.One.accGravSatisfied`, `SMNoGrav.One.E_zero_iff_Q_zero`, `SMNoGrav_numberLinear`, `SMNoGrav.SU2Sol`, `SMNoGrav_numberCharges`, `SMNoGrav.One.linearParametersQENeqZero.cubic`, `SMNoGrav.One.linearParametersQENeqZero.grav`, `SMNoGrav.One.linearParameters.asLinear_val`, `SMNoGrav.cubeSol`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SMNoGrav_cubicACC_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystem.cubicACC` `SMNoGrav`	—	—
`SMNoGrav_linearACCs` 📖	mathematical	—	`ACCSystemLinear.linearACCs` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMNoGrav` `ACCSystemCharges.Charges` `SMCharges` `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` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule`	—	—

SM.SMNoGrav

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SU2Sol` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMACCs.accSU2` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SM.SMNoGrav`	—	`ACCSystemLinear.LinSols.linearSol`
`SU3Sol` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMACCs.accSU3` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SM.SMNoGrav`	—	`ACCSystemLinear.LinSols.linearSol`
`cubeSol` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `SMACCs.accCube` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SM.SMNoGrav` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols`	—	`ACCSystem.Sols.cubicSol`

---

← Back to Index