PlaneNonSols

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

Statistics

Metric	Count
Definitions `B`, `B₀`, `B₁`, `B₁₀`, `B₂`, `B₃`, `B₄`, `B₅`, `B₆`, `B₇`, `B₈`, `B₉`, `quadCoeff`	13
Theorems `Bi_Bj_quad`, `Bi_sum_quad`, `basis_linear_independent`, `isSolution_f0`, `isSolution_f1`, `isSolution_f10`, `isSolution_f2`, `isSolution_f3`, `isSolution_f4`, `isSolution_f5`, `isSolution_f6`, `isSolution_f7`, `isSolution_f8`, `isSolution_f9`, `isSolution_f_zero`, `isSolution_grav`, `isSolution_only_if_zero`, `isSolution_quadCoeff_f_sq_zero`, `isSolution_sum_part`, `isSolution_sum_part'`, `on_accQuad`, `quadCoeff_eq_bilinear`, `eleven_dim_plane_of_no_sols_exists`	23
Total	36

SMRHN.PlusU1

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eleven_dim_plane_of_no_sols_exists` 📖	mathematical	—	`ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystemCharges.ChargesAddCommGroup`	—	`ElevenPlane.basis_linear_independent` `ElevenPlane.isSolution_only_if_zero`

SMRHN.PlusU1.ElevenPlane

Definitions

Name	Category	Theorems
`B` 📖	CompOp	5 math math: `Bi_Bj_quad`, `on_accQuad`, `basis_linear_independent`, `Bi_sum_quad`, `quadCoeff_eq_bilinear`
`B₀` 📖	CompOp	—
`B₁` 📖	CompOp	—
`B₁₀` 📖	CompOp	2 math math: `isSolution_sum_part'`, `isSolution_sum_part`
`B₂` 📖	CompOp	—
`B₃` 📖	CompOp	—
`B₄` 📖	CompOp	—
`B₅` 📖	CompOp	—
`B₆` 📖	CompOp	—
`B₇` 📖	CompOp	—
`B₈` 📖	CompOp	—
`B₉` 📖	CompOp	2 math math: `isSolution_sum_part'`, `isSolution_sum_part`
`quadCoeff` 📖	CompOp	3 math math: `on_accQuad`, `isSolution_quadCoeff_f_sq_zero`, `quadCoeff_eq_bilinear`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Bi_Bj_quad` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `SMνACCs.quadBiLin` `B`	—	—
`Bi_sum_quad` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `SMνACCs.quadBiLin` `B` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `ACCSystemCharges.ChargesAddCommGroup`	—	`BiLinearSymm.map_sum₂` `BiLinearSymm.map_smul₂` `Bi_Bj_quad`
`basis_linear_independent` 📖	mathematical	—	`ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.PlusU1` `B` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule`	—	`isSolution_f_zero`
`isSolution_f0` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_quadCoeff_f_sq_zero`
`isSolution_f1` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_quadCoeff_f_sq_zero`
`isSolution_f10` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_grav` `isSolution_f9`
`isSolution_f2` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_quadCoeff_f_sq_zero`
`isSolution_f3` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_quadCoeff_f_sq_zero`
`isSolution_f4` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_quadCoeff_f_sq_zero`
`isSolution_f5` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_quadCoeff_f_sq_zero`
`isSolution_f6` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_quadCoeff_f_sq_zero`
`isSolution_f7` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_quadCoeff_f_sq_zero`
`isSolution_f8` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_quadCoeff_f_sq_zero`
`isSolution_f9` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_sum_part'` `SMRHN.PlusU1.cubeSol` `TriLinearSymm.map_smul₃` `TriLinearSymm.map_smul₂` `TriLinearSymm.map_smul₁` `HomogeneousCubic.map_smul` `TriLinearSymm.toCubic_add`
`isSolution_f_zero` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_f0` `isSolution_f1` `isSolution_f2` `isSolution_f3` `isSolution_f4` `isSolution_f5` `isSolution_f6` `isSolution_f7` `isSolution_f8` `isSolution_f9` `isSolution_f10`
`isSolution_grav` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_sum_part` `SMRHN.PlusU1.gravSol`
`isSolution_only_if_zero` 📖	—	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	—	`isSolution_sum_part` `isSolution_grav` `isSolution_f9`
`isSolution_quadCoeff_f_sq_zero` 📖	mathematical	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	`quadCoeff`	—	`SMRHN.PlusU1.quadSol` `on_accQuad`
`isSolution_sum_part` 📖	mathematical	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	`B₉` `B₁₀`	—	`isSolution_f0` `isSolution_f1` `isSolution_f2` `isSolution_f3` `isSolution_f4` `isSolution_f5` `isSolution_f6` `isSolution_f7` `isSolution_f8`
`isSolution_sum_part'` 📖	mathematical	`ACCSystem.IsSolution` `SMRHN.PlusU1` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	`B₉` `B₁₀`	—	`isSolution_sum_part` `isSolution_grav`
`on_accQuad` 📖	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` `B` `quadCoeff`	—	`BiLinearSymm.map_sum₁` `BiLinearSymm.map_smul₁` `Bi_sum_quad` `quadCoeff_eq_bilinear`
`quadCoeff_eq_bilinear` 📖	mathematical	—	`quadCoeff` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `SMνACCs.quadBiLin` `B`	—	—

---

← Back to Index