ToSols

📁 Source: PhysLean/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/ToSols.lean

Statistics

Metric	Count
Definitions `InCubeProp`, `InCubeSolProp`, `InLineEq`, `InLineEqSol`, `InQuad`, `InQuadCube`, `InQuadCubeSol`, `InQuadProp`, `InQuadSol`, `InQuadSolProp`, `LineEqProp`, `LineEqPropSol`, `NotInLineEqSol`, `cubicCoeff`, `inLineEqProj`, `inLineEqToSol`, `inQuadCubeProj`, `inQuadCubeToSol`, `inQuadProj`, `inQuadToSol`, `instDecidableInCubeProp`, `instDecidableInQuadProp`, `instDecidableLineEqProp`, `lineEqCoeff`, `quadCoeff`, `toSol`, `toSolNS`, `toSolNSProj`, `toSolNSQuad`	29
Theorems `inCubeSolProp_iff_cubicCoeff_zero`, `inCubeSolProp_iff_proj_inCubeProp`, `inLineEqToSol_proj`, `inLineEqTo_smul`, `inQuadCubeToSol_proj`, `inQuadCubeToSol_smul`, `inQuadSolProp_iff_proj_inQuadProp`, `inQuadSolProp_iff_quadCoeff_zero`, `inQuadToSol_proj`, `inQuadToSol_smul`, `linEqPropSol_iff_proj_linEqProp`, `lineEqPropSol_iff_lineEqCoeff_zero`, `toSolNSQuad_cube`, `toSolNSQuad_eq_planeY₃B₃_on_α`, `toSolNS_proj`, `toSol_inLineEq`, `toSol_inQuad`, `toSol_inQuadCube`, `toSol_surjective`, `toSol_toSolNSProj`	20
Total	49

MSSMACC.AnomalyFreePerp

Definitions

Name	Category	Theorems
`InCubeProp` 📖	MathDef	1 math math: `inCubeSolProp_iff_proj_inCubeProp`
`InCubeSolProp` 📖	MathDef	6 math math: `toSol_inQuadCube`, `inQuadCubeToSol_proj`, `inQuadToSol_proj`, `inCubeSolProp_iff_cubicCoeff_zero`, `toSol_inQuad`, `inCubeSolProp_iff_proj_inCubeProp`
`InLineEq` 📖	CompOp	1 math math: `inLineEqTo_smul`
`InLineEqSol` 📖	CompOp	—
`InQuad` 📖	CompOp	1 math math: `inQuadToSol_smul`
`InQuadCube` 📖	CompOp	1 math math: `inQuadCubeToSol_smul`
`InQuadCubeSol` 📖	CompOp	—
`InQuadProp` 📖	MathDef	1 math math: `inQuadSolProp_iff_proj_inQuadProp`
`InQuadSol` 📖	CompOp	—
`InQuadSolProp` 📖	MathDef	8 math math: `toSol_inQuadCube`, `inQuadCubeToSol_proj`, `inQuadSolProp_iff_proj_inQuadProp`, `inQuadToSol_proj`, `toSol_inLineEq`, `inLineEqToSol_proj`, `toSol_inQuad`, `inQuadSolProp_iff_quadCoeff_zero`
`LineEqProp` 📖	MathDef	1 math math: `linEqPropSol_iff_proj_linEqProp`
`LineEqPropSol` 📖	MathDef	10 math math: `toSol_inQuadCube`, `inQuadCubeToSol_proj`, `toSolNS_proj`, `inQuadToSol_proj`, `linEqPropSol_iff_proj_linEqProp`, `toSol_inLineEq`, `lineEqPropSol_iff_lineEqCoeff_zero`, `inLineEqToSol_proj`, `toSol_inQuad`, `toSol_toSolNSProj`
`NotInLineEqSol` 📖	CompOp	—
`cubicCoeff` 📖	CompOp	1 math math: `inCubeSolProp_iff_cubicCoeff_zero`
`inLineEqProj` 📖	CompOp	1 math math: `inLineEqToSol_proj`
`inLineEqToSol` 📖	CompOp	2 math math: `inLineEqTo_smul`, `inLineEqToSol_proj`
`inQuadCubeProj` 📖	CompOp	1 math math: `inQuadCubeToSol_proj`
`inQuadCubeToSol` 📖	CompOp	2 math math: `inQuadCubeToSol_proj`, `inQuadCubeToSol_smul`
`inQuadProj` 📖	CompOp	1 math math: `inQuadToSol_proj`
`inQuadToSol` 📖	CompOp	2 math math: `inQuadToSol_proj`, `inQuadToSol_smul`
`instDecidableInCubeProp` 📖	CompOp	—
`instDecidableInQuadProp` 📖	CompOp	—
`instDecidableLineEqProp` 📖	CompOp	—
`lineEqCoeff` 📖	CompOp	1 math math: `lineEqPropSol_iff_lineEqCoeff_zero`
`quadCoeff` 📖	CompOp	1 math math: `inQuadSolProp_iff_quadCoeff_zero`
`toSol` 📖	CompOp	5 math math: `toSol_inQuadCube`, `toSol_surjective`, `toSol_inLineEq`, `toSol_inQuad`, `toSol_toSolNSProj`
`toSolNS` 📖	CompOp	1 math math: `toSolNS_proj`
`toSolNSProj` 📖	CompOp	1 math math: `toSolNS_proj`
`toSolNSQuad` 📖	CompOp	2 math math: `toSolNSQuad_eq_planeY₃B₃_on_α`, `toSolNSQuad_cube`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inCubeSolProp_iff_cubicCoeff_zero` 📖	mathematical	—	`InCubeSolProp` `cubicCoeff`	—	`cubicCoeff.eq_1`
`inCubeSolProp_iff_proj_inCubeProp` 📖	mathematical	—	`InCubeSolProp` `InCubeProp` `MSSMACC.proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystem.Sols.toQuadSols`	—	`InCubeSolProp.eq_1` `InCubeProp.eq_1` `MSSMACC.cube_proj` `MSSMACC.cube_proj_proj_Y₃` `MSSMACC.cube_proj_proj_B₃`
`inLineEqToSol_proj` 📖	mathematical	—	`inLineEqToSol` `inLineEqProj` `ACCSystem.Sols` `MSSMACC` `LineEqPropSol` `InQuadSolProp`	—	`inLineEqProj.eq_1` `inLineEqTo_smul` `ACCSystem.Sols.ext` `MSSMACC.lineQuad_val` `MSSMACC.planeY₃B₃_val` `MSSMACC.Y₃_plus_B₃_plus_proj` `MSSMACC.quad_proj` `MSSMACC.quad_Y₃_proj` `MSSMACC.quad_B₃_proj` `quadCoeff.eq_1` `inQuadSolProp_iff_quadCoeff_zero`
`inLineEqTo_smul` 📖	mathematical	—	`inLineEqToSol` `InLineEq` `ACCSystem.Sols` `MSSMACC` `ACCSystem.solsMulAction`	—	`ACCSystem.Sols.ext` `MSSMACC.lineQuad_smul`
`inQuadCubeToSol_proj` 📖	mathematical	—	`inQuadCubeToSol` `inQuadCubeProj` `ACCSystem.Sols` `MSSMACC` `LineEqPropSol` `InQuadSolProp` `InCubeSolProp`	—	`inQuadCubeProj.eq_1` `inQuadCubeToSol_smul` `ACCSystem.Sols.ext` `MSSMACC.planeY₃B₃_val` `MSSMACC.Y₃_plus_B₃_plus_proj`
`inQuadCubeToSol_smul` 📖	mathematical	—	`inQuadCubeToSol` `InQuadCube` `ACCSystem.Sols` `MSSMACC` `ACCSystem.solsMulAction`	—	`ACCSystem.Sols.ext` `MSSMACC.planeY₃B₃_smul`
`inQuadSolProp_iff_proj_inQuadProp` 📖	mathematical	—	`InQuadSolProp` `InQuadProp` `MSSMACC.proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystem.Sols.toQuadSols`	—	`InQuadSolProp.eq_1` `InQuadProp.eq_1` `MSSMACC.quad_proj` `MSSMACC.quad_Y₃_proj` `MSSMACC.quad_B₃_proj`
`inQuadSolProp_iff_quadCoeff_zero` 📖	mathematical	—	`InQuadSolProp` `quadCoeff`	—	`quadCoeff.eq_1`
`inQuadToSol_proj` 📖	mathematical	—	`inQuadToSol` `inQuadProj` `ACCSystem.Sols` `MSSMACC` `LineEqPropSol` `InQuadSolProp` `InCubeSolProp`	—	`inQuadProj.eq_1` `inQuadToSol_smul` `ACCSystem.Sols.ext` `MSSMACC.planeY₃B₃_val` `MSSMACC.Y₃_plus_B₃_plus_proj` `MSSMACC.cube_proj` `MSSMACC.cube_proj_proj_B₃` `MSSMACC.cube_proj_proj_Y₃` `cubicCoeff.eq_1` `inCubeSolProp_iff_cubicCoeff_zero`
`inQuadToSol_smul` 📖	mathematical	—	`inQuadToSol` `InQuad` `ACCSystem.Sols` `MSSMACC` `ACCSystem.solsMulAction`	—	`ACCSystem.Sols.ext` `MSSMACC.lineCube_smul`
`linEqPropSol_iff_proj_linEqProp` 📖	mathematical	—	`LineEqPropSol` `LineEqProp` `MSSMACC.proj` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystem.Sols.toQuadSols`	—	`lineEqPropSol_iff_lineEqCoeff_zero` `lineEqCoeff.eq_1` `LineEqProp.eq_1` `MSSMACC.α₁_proj` `MSSMACC.α₂_proj`
`lineEqPropSol_iff_lineEqCoeff_zero` 📖	mathematical	—	`LineEqPropSol` `lineEqCoeff`	—	`LineEqPropSol.eq_1` `lineEqCoeff.eq_1` `MSSMACC.α₃.eq_1` `MSSMACC.cube_proj_proj_B₃` `MSSMACC.cube_proj_proj_Y₃` `MSSMACC.quad_B₃_proj` `MSSMACC.quad_Y₃_proj` `MSSMACCs.quadBiLin_toFun_apply`
`toSolNSQuad_cube` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `MSSMACCs.accCube` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols` `toSolNSQuad`	—	`toSolNSQuad.eq_1` `MSSMACC.lineQuad_val` `MSSMACC.planeY₃B₃_cubic`
`toSolNSQuad_eq_planeY₃B₃_on_α` 📖	mathematical	—	`ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.toACCSystemQuad` `MSSMACC` `toSolNSQuad` `MSSMACC.planeY₃B₃` `MSSMACC.α₁` `MSSMACC.α₂` `MSSMACC.α₃`	—	`MSSMACC.planeY₃B₃_eq` `MSSMACC.α₁.eq_1` `MSSMACC.α₂.eq_1` `MSSMACC.α₃.eq_1`
`toSolNS_proj` 📖	mathematical	—	`toSolNS` `toSolNSProj` `ACCSystem.Sols` `MSSMACC` `LineEqPropSol`	—	`ACCSystem.Sols.ext` `toSolNSQuad_cube` `toSolNS.eq_1` `toSolNSProj.eq_1` `toSolNSQuad_eq_planeY₃B₃_on_α` `MSSMACC.planeY₃B₃_val` `MSSMACC.Y₃_plus_B₃_plus_proj` `MSSMACC.α₁_proj` `MSSMACC.α₂_proj` `lineEqCoeff.eq_1` `lineEqPropSol_iff_lineEqCoeff_zero`
`toSol_inLineEq` 📖	mathematical	—	`toSol` `ACCSystem.Sols` `MSSMACC` `LineEqPropSol` `InQuadSolProp`	—	`inQuadSolProp_iff_proj_inQuadProp` `linEqPropSol_iff_proj_linEqProp` `inLineEqToSol_proj`
`toSol_inQuad` 📖	mathematical	—	`toSol` `ACCSystem.Sols` `MSSMACC` `LineEqPropSol` `InQuadSolProp` `InCubeSolProp`	—	`inCubeSolProp_iff_proj_inCubeProp` `inQuadSolProp_iff_proj_inQuadProp` `linEqPropSol_iff_proj_linEqProp` `inQuadToSol_proj`
`toSol_inQuadCube` 📖	mathematical	—	`toSol` `ACCSystem.Sols` `MSSMACC` `LineEqPropSol` `InQuadSolProp` `InCubeSolProp`	—	`inCubeSolProp_iff_proj_inCubeProp` `inQuadSolProp_iff_proj_inQuadProp` `linEqPropSol_iff_proj_linEqProp` `inQuadCubeToSol_proj`
`toSol_surjective` 📖	mathematical	—	`MSSMACC.AnomalyFreePerp` `ACCSystem.Sols` `MSSMACC` `toSol`	—	`toSol_toSolNSProj` `toSol_inLineEq` `toSol_inQuad` `toSol_inQuadCube`
`toSol_toSolNSProj` 📖	mathematical	—	`toSol` `ACCSystem.Sols` `MSSMACC` `LineEqPropSol`	—	`linEqPropSol_iff_proj_linEqProp` `toSolNS_proj`

---

← Back to Index