Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `SM`, `chargeToAF`, `chargeToLinear`, `chargeToQuad`, `linearToAF`, `linearToQuad`, `perm`, `quadToAF`	8
Theorems `SU2Sol`, `SU3Sol`, `cubeSol`, `gravSol`, `SM_cubicACC_apply`, `SM_linearACCs`, `SM_numberCharges`, `SM_numberLinear`, `SM_numberQuadratic`, `SM_quadraticACCs`	10
Total	18

SMRHN

Definitions

Name	Category	Theorems
`SM` 📖	CompOp	14 math math: `SM.PlaneSeven.basis_linear_independent`, `SM_numberCharges`, `SM_numberQuadratic`, `SM_linearACCs`, `SM.cubeSol`, `SM_numberLinear`, `SM.gravSol`, `SM.SU3Sol`, `SM_quadraticACCs`, `SM.PlaneSeven.B_in_accCube`, `SM.PlaneSeven.B_sum_is_sol`, `SM.SU2Sol`, `SM_cubicACC_apply`, `SM.seven_dim_plane_exists`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SM_cubicACC_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystem.cubicACC` `SM`	—	—
`SM_linearACCs` 📖	mathematical	—	`ACCSystemLinear.linearACCs` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SM` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule`	—	—
`SM_numberCharges` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SM`	—	—
`SM_numberLinear` 📖	mathematical	—	`ACCSystemLinear.numberLinear` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SM`	—	—
`SM_numberQuadratic` 📖	mathematical	—	`ACCSystemQuad.numberQuadratic` `ACCSystem.toACCSystemQuad` `SM`	—	—
`SM_quadraticACCs` 📖	mathematical	—	`ACCSystemQuad.quadraticACCs` `ACCSystem.toACCSystemQuad` `SM` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule`	—	—

SMRHN.SM

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

---

← Back to Index