DimSevenPlane

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

Statistics

Metric	Count
Definitions `B`, `B₀`, `B₁`, `B₂`, `B₃`, `B₄`, `B₅`, `B₆`	8
Theorems `B_in_accCube`, `B_sum_is_sol`, `Bi_Bi_Bj_cubic`, `Bi_Bj_Bk_cubic`, `Bi_Bj_ne_cubic`, `B₀_Bi_cubic`, `B₀_cubic`, `B₁_Bi_cubic`, `B₁_cubic`, `B₂_Bi_cubic`, `B₂_cubic`, `B₃_Bi_cubic`, `B₃_cubic`, `B₄_Bi_cubic`, `B₄_cubic`, `B₅_Bi_cubic`, `B₅_cubic`, `B₆_Bi_cubic`, `B₆_cubic`, `basis_linear_independent`, `seven_dim_plane_exists`	21
Total	29

SMRHN.SM

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`seven_dim_plane_exists` 📖	mathematical	—	`ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.SM` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystem.IsSolution` `ACCSystemCharges.ChargesAddCommGroup`	—	`PlaneSeven.basis_linear_independent` `PlaneSeven.B_sum_is_sol`

SMRHN.SM.PlaneSeven

Definitions

Name	Category	Theorems
`B` 📖	CompOp	13 math math: `Bi_Bj_ne_cubic`, `basis_linear_independent`, `B₄_Bi_cubic`, `B₅_Bi_cubic`, `Bi_Bi_Bj_cubic`, `Bi_Bj_Bk_cubic`, `B₆_Bi_cubic`, `B_in_accCube`, `B_sum_is_sol`, `B₃_Bi_cubic`, `B₁_Bi_cubic`, `B₀_Bi_cubic`, `B₂_Bi_cubic`
`B₀` 📖	CompOp	1 math math: `B₀_cubic`
`B₁` 📖	CompOp	1 math math: `B₁_cubic`
`B₂` 📖	CompOp	1 math math: `B₂_cubic`
`B₃` 📖	CompOp	1 math math: `B₃_cubic`
`B₄` 📖	CompOp	1 math math: `B₄_cubic`
`B₅` 📖	CompOp	1 math math: `B₅_cubic`
`B₆` 📖	CompOp	1 math math: `B₆_cubic`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`B_in_accCube` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `SMνACCs.accCube` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.SM` `ACCSystemCharges.ChargesAddCommGroup` `B`	—	`TriLinearSymm.map_sum₁₂₃` `TriLinearSymm.map_smul₁` `TriLinearSymm.map_smul₂` `TriLinearSymm.map_smul₃` `Bi_Bj_Bk_cubic`
`B_sum_is_sol` 📖	mathematical	—	`ACCSystem.IsSolution` `SMRHN.SM` `ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesModule` `B`	—	`B_in_accCube`
`Bi_Bi_Bj_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B`	—	—
`Bi_Bj_Bk_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B`	—	`Bi_Bj_ne_cubic` `Bi_Bi_Bj_cubic`
`Bi_Bj_ne_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B`	—	`B₀_Bi_cubic` `B₁_Bi_cubic` `B₂_Bi_cubic` `B₃_Bi_cubic` `B₄_Bi_cubic` `B₅_Bi_cubic` `B₆_Bi_cubic`
`B₀_Bi_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B`	—	`B₀_cubic`
`B₀_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B₀`	—	—
`B₁_Bi_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B`	—	`B₁_cubic`
`B₁_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B₁`	—	—
`B₂_Bi_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B`	—	`B₂_cubic`
`B₂_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B₂`	—	—
`B₃_Bi_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B`	—	`B₃_cubic`
`B₃_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B₃`	—	—
`B₄_Bi_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B`	—	`B₄_cubic`
`B₄_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B₄`	—	—
`B₅_Bi_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B`	—	`B₅_cubic`
`B₅_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B₅`	—	—
`B₆_Bi_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B`	—	`B₆_cubic`
`B₆_cubic` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `B₆`	—	—
`basis_linear_independent` 📖	mathematical	—	`ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `SMRHN.SM` `B` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule`	—	`B₆.eq_1` `B₅.eq_1` `B₄.eq_1` `B₃.eq_1` `B₂.eq_1` `B₁.eq_1` `B₀.eq_1`

---

← Back to Index