Documentation Verification Report

QuadSolToSol

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

Statistics

Metric	Count
Definitions `generic`, `special`, `α₁`, `α₂`, `quadSolToSol`, `quadSolToSolInv`	6
Theorems `BL_add_α₁_α₂_AF`, `BL_add_α₁_α₂_cube`, `cube_α₁_α₂_zero`, `generic_on_AF`, `generic_on_AF_α₁_ne_zero`, `special_on_AF`, `α₂_AF`, `quadSolToSolInv_1`, `quadSolToSolInv_generic`, `quadSolToSolInv_rightInverse`, `quadSolToSolInv_special`, `quadSolToSolInv_α₁_α₂_neq_zero`, `quadSolToSolInv_α₁_α₂_zero`, `quadSolToSol_surjective`	14
Total	20

SMRHN.PlusU1

Definitions

Name	Category	Theorems
`quadSolToSol` 📖	CompOp	2 math math: `quadSolToSolInv_rightInverse`, `quadSolToSol_surjective`
`quadSolToSolInv` 📖	CompOp	6 math math: `quadSolToSolInv_α₁_α₂_neq_zero`, `quadSolToSolInv_rightInverse`, `quadSolToSolInv_generic`, `quadSolToSolInv_1`, `quadSolToSolInv_special`, `quadSolToSolInv_α₁_α₂_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quadSolToSolInv_1` 📖	mathematical	—	`ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `quadSolToSolInv` `ACCSystem.Sols.toQuadSols`	—	—
`quadSolToSolInv_generic` 📖	mathematical	—	`ACCSystem.Sols` `SMRHN.PlusU1` `ACCSystem.solsMulAction` `ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `quadSolToSolInv` `QuadSolToSol.generic`	—	`quadSolToSolInv_1` `quadSolToSolInv.eq_1` `QuadSolToSol.generic_on_AF_α₁_ne_zero`
`quadSolToSolInv_rightInverse` 📖	mathematical	—	`ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystem.Sols` `quadSolToSolInv` `quadSolToSol`	—	`quadSolToSol.eq_1` `quadSolToSolInv_α₁_α₂_zero` `quadSolToSolInv_special` `quadSolToSolInv_α₁_α₂_neq_zero` `quadSolToSolInv_generic`
`quadSolToSolInv_special` 📖	mathematical	`QuadSolToSol.α₁` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1`	`QuadSolToSol.special` `ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `quadSolToSolInv` `QuadSolToSol.α₂` `quadSolToSolInv_α₁_α₂_zero`	—	`quadSolToSolInv_α₁_α₂_zero` `quadSolToSolInv_1` `QuadSolToSol.special.congr_simp` `quadSolToSolInv.eq_1` `QuadSolToSol.α₂_AF` `QuadSolToSol.special_on_AF`
`quadSolToSolInv_α₁_α₂_neq_zero` 📖	mathematical	—	`QuadSolToSol.α₁` `ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `quadSolToSolInv` `QuadSolToSol.α₂`	—	`quadSolToSolInv_1` `QuadSolToSol.α₂_AF`
`quadSolToSolInv_α₁_α₂_zero` 📖	mathematical	`QuadSolToSol.α₁` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1`	`ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `quadSolToSolInv` `QuadSolToSol.α₂`	—	`quadSolToSolInv_1` `QuadSolToSol.α₂_AF`
`quadSolToSol_surjective` 📖	mathematical	—	`ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystem.Sols` `quadSolToSol`	—	`quadSolToSolInv_rightInverse`

SMRHN.PlusU1.QuadSolToSol

Definitions

Name	Category	Theorems
`generic` 📖	CompOp	3 math math: `generic_on_AF`, `generic_on_AF_α₁_ne_zero`, `SMRHN.PlusU1.quadSolToSolInv_generic`
`special` 📖	CompOp	2 math math: `special_on_AF`, `SMRHN.PlusU1.quadSolToSolInv_special`
`α₁` 📖	CompOp	5 math math: `BL_add_α₁_α₂_cube`, `SMRHN.PlusU1.quadSolToSolInv_α₁_α₂_neq_zero`, `generic_on_AF`, `generic_on_AF_α₁_ne_zero`, `BL_add_α₁_α₂_AF`
`α₂` 📖	CompOp	6 math math: `BL_add_α₁_α₂_cube`, `SMRHN.PlusU1.quadSolToSolInv_α₁_α₂_neq_zero`, `BL_add_α₁_α₂_AF`, `SMRHN.PlusU1.quadSolToSolInv_special`, `α₂_AF`, `SMRHN.PlusU1.quadSolToSolInv_α₁_α₂_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`BL_add_α₁_α₂_AF` 📖	mathematical	—	`SMRHN.PlusU1.BL.addQuad` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1` `α₁` `α₂` `ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `ACCSystemQuad.quadSolsMulAction`	—	`α₂_AF` `SMRHN.PlusU1.BL.addQuad_zero`
`BL_add_α₁_α₂_cube` 📖	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` `SMRHN.PlusU1.BL.addQuad` `α₁` `α₂`	—	`SMRHN.PlusU1.BL.add_AFL_cube`
`cube_α₁_α₂_zero` 📖	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` `SMRHN.PlusU1.BL.addQuad`	—	`SMRHN.PlusU1.BL.add_AFL_cube`
`generic_on_AF` 📖	mathematical	—	`generic` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1` `ACCSystem.Sols` `ACCSystem.solsMulAction` `α₁`	—	`ACCSystem.Sols.ext` `BL_add_α₁_α₂_AF`
`generic_on_AF_α₁_ne_zero` 📖	mathematical	—	`ACCSystem.Sols` `SMRHN.PlusU1` `ACCSystem.solsMulAction` `α₁` `ACCSystem.Sols.toQuadSols` `generic`	—	`generic_on_AF`
`special_on_AF` 📖	mathematical	`α₁` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1`	`special` `α₂_AF`	—	`ACCSystem.Sols.ext` `α₂_AF` `SMRHN.PlusU1.BL.addQuad_zero`
`α₂_AF` 📖	mathematical	—	`α₂` `ACCSystem.Sols.toQuadSols` `SMRHN.PlusU1`	—	`ACCSystem.Sols.cubicSol`

---

← Back to Index