Documentation Verification Report

QuadSol

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

Statistics

Metric	Count
Definitions `genericToQuad`, `specialToQuad`, `toQuad`, `toQuadInv`, `α₁`, `α₂`	6
Theorems `accQuad_α₁_α₂`, `accQuad_α₁_α₂_zero`, `add_AFL_quad`, `genericToQuad_neq_zero`, `genericToQuad_on_quad`, `special_on_quad`, `toQuadInv_fst`, `toQuadInv_generic`, `toQuadInv_special`, `toQuadInv_α₁_α₂`, `toQuad_rightInverse`, `toQuad_surjective`, `α₂_AFQ`	13
Total	19

SMRHN.PlusU1.QuadSol

Definitions

Name	Category	Theorems
`genericToQuad` 📖	CompOp	3 math math: `toQuadInv_generic`, `genericToQuad_neq_zero`, `genericToQuad_on_quad`
`specialToQuad` 📖	CompOp	2 math math: `special_on_quad`, `toQuadInv_special`
`toQuad` 📖	CompOp	2 math math: `toQuad_surjective`, `toQuad_rightInverse`
`toQuadInv` 📖	CompOp	5 math math: `toQuadInv_fst`, `toQuadInv_generic`, `toQuadInv_special`, `toQuad_rightInverse`, `toQuadInv_α₁_α₂`
`α₁` 📖	CompOp	4 math math: `genericToQuad_neq_zero`, `genericToQuad_on_quad`, `accQuad_α₁_α₂`, `toQuadInv_α₁_α₂`
`α₂` 📖	CompOp	4 math math: `toQuadInv_special`, `α₂_AFQ`, `accQuad_α₁_α₂`, `toQuadInv_α₁_α₂`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`accQuad_α₁_α₂` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `SMνACCs.accQuad` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemLinear.LinSols` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsAddCommGroup` `ACCSystemLinear.linSolsModule` `α₁` `α₂` `ACCSystemQuad.QuadSols.toLinSols`	—	`add_AFL_quad` `α₁.eq_1` `α₂.eq_1`
`accQuad_α₁_α₂_zero` 📖	mathematical	`α₁` `α₂`	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `SMνACCs.accQuad` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemLinear.LinSols` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsAddCommGroup` `ACCSystemLinear.linSolsModule` `ACCSystemQuad.QuadSols.toLinSols`	—	`add_AFL_quad` `SMνACCs.quadBiLin_toFun_apply`
`add_AFL_quad` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `SMνACCs.accQuad` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.QuadSols.toLinSols` `BiLinearSymm` `BiLinearSymm.instFun` `SMνACCs.quadBiLin`	—	`BiLinearSymm.toHomogeneousQuad_add` `SMRHN.PlusU1.quadSol` `BiLinearSymm.map_smul₁` `BiLinearSymm.map_smul₂` `HomogeneousQuadratic.map_smul`
`genericToQuad_neq_zero` 📖	mathematical	—	`ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.quadSolsMulAction` `α₁` `ACCSystemQuad.QuadSols.toLinSols` `genericToQuad`	—	`genericToQuad_on_quad`
`genericToQuad_on_quad` 📖	mathematical	—	`genericToQuad` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.QuadSols` `ACCSystemQuad.quadSolsMulAction` `α₁`	—	`ACCSystemQuad.QuadSols.ext` `α₂_AFQ`
`special_on_quad` 📖	mathematical	`α₁` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1`	`specialToQuad` `α₂_AFQ`	—	`ACCSystemQuad.QuadSols.ext` `α₂_AFQ`
`toQuadInv_fst` 📖	mathematical	—	`ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `toQuadInv` `ACCSystemQuad.QuadSols.toLinSols`	—	`toQuadInv.eq_1`
`toQuadInv_generic` 📖	mathematical	—	`ACCSystemQuad.QuadSols` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.quadSolsMulAction` `ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `toQuadInv` `genericToQuad`	—	`toQuadInv_fst` `toQuadInv.eq_1` `genericToQuad_neq_zero`
`toQuadInv_special` 📖	mathematical	`α₁` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1`	`specialToQuad` `ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `toQuadInv` `α₂` `toQuadInv_α₁_α₂`	—	`toQuadInv_α₁_α₂` `toQuadInv_fst` `specialToQuad.congr_simp` `toQuadInv.eq_1` `α₂_AFQ` `special_on_quad`
`toQuadInv_α₁_α₂` 📖	mathematical	—	`α₁` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `toQuadInv` `α₂`	—	`toQuadInv_fst` `α₂_AFQ`
`toQuad_rightInverse` 📖	mathematical	—	`ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.QuadSols` `toQuadInv` `toQuad`	—	`toQuad.eq_1` `toQuadInv_α₁_α₂` `toQuadInv_special` `toQuadInv_generic`
`toQuad_surjective` 📖	mathematical	—	`ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemQuad.QuadSols` `toQuad`	—	`toQuad_rightInverse`
`α₂_AFQ` 📖	mathematical	—	`α₂` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1`	—	`SMRHN.PlusU1.quadSol`

---

← Back to Index