Plane Y₃ B₃ and an orthogonal third point

The plane spanned by Y₃, B₃ and third orthogonal point.

References

• https://arxiv.org/pdf/2107.07926.pdf

def MSSMACC.planeY₃B₃ (R : AnomalyFreePerp) (a b c : ℚ) : MSSMACC.LinSols

The plane of linear solutions spanned by Y₃, B₃ and R, a point orthogonal to Y₃ and B₃.

Equations

• MSSMACC.planeY₃B₃ R a b c = a • MSSMACC.Y₃.toLinSols + b • MSSMACC.B₃.toLinSols + c • R.toLinSols

theorem MSSMACC.planeY₃B₃_val (R : AnomalyFreePerp) (a b c : ℚ) : (planeY₃B₃ R a b c).val = a • Y₃.val + b • B₃.val + c • R.val

theorem MSSMACC.planeY₃B₃_smul (R : AnomalyFreePerp) (a b c d : ℚ) : planeY₃B₃ R (d * a) (d * b) (d * c) = d • planeY₃B₃ R a b c

theorem MSSMACC.planeY₃B₃_eq {a' b' c' : ℚ} (R : AnomalyFreePerp) (a b c : ℚ) (h : a = a' ∧ b = b' ∧ c = c') : planeY₃B₃ R a b c = planeY₃B₃ R a' b' c'

theorem MSSMACC.planeY₃B₃_val_eq' {a' b' c' : ℚ} (R : AnomalyFreePerp) (a b c : ℚ) (hR' : R.val ≠ 0) (h : (planeY₃B₃ R a b c).val = (planeY₃B₃ R a' b' c').val) : a = a' ∧ b = b' ∧ c = c'

theorem MSSMACC.planeY₃B₃_quad (R : AnomalyFreePerp) (a b c : ℚ) : MSSMACCs.accQuad (planeY₃B₃ R a b c).val = c * (2 * a * (MSSMACCs.quadBiLin Y₃.val) R.val + 2 * b * (MSSMACCs.quadBiLin B₃.val) R.val + c * (MSSMACCs.quadBiLin R.val) R.val)

theorem MSSMACC.planeY₃B₃_cubic (R : AnomalyFreePerp) (a b c : ℚ) : MSSMACCs.accCube (planeY₃B₃ R a b c).val = c ^ 2 * (3 * a * ((MSSMACCs.cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((MSSMACCs.cubeTriLin R.val) R.val) B₃.val + c * ((MSSMACCs.cubeTriLin R.val) R.val) R.val)

def MSSMACC.lineQuadAFL (R : AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACC.LinSols

The line in the plane spanned by Y₃, B₃ and R which is in the quadratic, as LinSols.

Equations

• One or more equations did not get rendered due to their size.

theorem MSSMACC.lineQuadAFL_quad (R : AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACCs.accQuad (lineQuadAFL R c1 c2 c3).val = 0

def MSSMACC.lineQuad (R : AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACC.QuadSols

The line in the plane spanned by Y₃, B₃ and R which is in the quadratic.

Equations

• MSSMACC.lineQuad R c1 c2 c3 = MSSMACC.AnomalyFreeQuadMk' (MSSMACC.lineQuadAFL R c1 c2 c3) ⋯

theorem MSSMACC.lineQuad_val (R : AnomalyFreePerp) (c1 c2 c3 : ℚ) : (lineQuad R c1 c2 c3).val = (planeY₃B₃ R (c2 * (MSSMACCs.quadBiLin R.val) R.val - 2 * c3 * (MSSMACCs.quadBiLin B₃.val) R.val) (2 * c3 * (MSSMACCs.quadBiLin Y₃.val) R.val - c1 * (MSSMACCs.quadBiLin R.val) R.val) (2 * c1 * (MSSMACCs.quadBiLin B₃.val) R.val - 2 * c2 * (MSSMACCs.quadBiLin Y₃.val) R.val)).val

theorem MSSMACC.lineQuad_smul (R : AnomalyFreePerp) (a b c d : ℚ) : lineQuad R (d * a) (d * b) (d * c) = d • lineQuad R a b c

def MSSMACC.α₁ (T : AnomalyFreePerp) : ℚ

A helper function to simplify following expressions.

Equations

• One or more equations did not get rendered due to their size.

def MSSMACC.α₂ (T : AnomalyFreePerp) : ℚ

A helper function to simplify following expressions.

Equations

• One or more equations did not get rendered due to their size.

def MSSMACC.α₃ (T : AnomalyFreePerp) : ℚ

A helper function to simplify following expressions.

Equations

• One or more equations did not get rendered due to their size.

theorem MSSMACC.lineQuad_cube (R : AnomalyFreePerp) (c₁ c₂ c₃ : ℚ) : MSSMACCs.accCube (lineQuad R c₁ c₂ c₃).val = -4 * (c₁ * (MSSMACCs.quadBiLin B₃.val) R.val - c₂ * (MSSMACCs.quadBiLin Y₃.val) R.val) ^ 2 * (α₁ R * c₁ + α₂ R * c₂ + α₃ R * c₃)

def MSSMACC.lineCube (R : AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) : MSSMACC.LinSols

The line in the plane spanned by Y₃, B₃ and R which is in the cubic.

Equations

• One or more equations did not get rendered due to their size.

theorem MSSMACC.lineCube_smul (R : AnomalyFreePerp) (a b c d : ℚ) : lineCube R (d * a) (d * b) (d * c) = d • lineCube R a b c

theorem MSSMACC.lineCube_cube (R : AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) : MSSMACCs.accCube (lineCube R a₁ a₂ a₃).val = 0

theorem MSSMACC.lineCube_quad (R : AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) : MSSMACCs.accQuad (lineCube R a₁ a₂ a₃).val = 3 * (a₁ * ((MSSMACCs.cubeTriLin R.val) R.val) B₃.val - a₂ * ((MSSMACCs.cubeTriLin R.val) R.val) Y₃.val) * (α₁ R * a₁ + α₂ R * a₂ + α₃ R * a₃)

theorem MSSMACC.α₃_proj (T : MSSMACC.Sols) : α₃ (proj T.toLinSols) = 6 * (dot Y₃.val) B₃.val ^ 3 * (((MSSMACCs.cubeTriLin T.val) T.val) Y₃.val * (MSSMACCs.quadBiLin B₃.val) T.val - ((MSSMACCs.cubeTriLin T.val) T.val) B₃.val * (MSSMACCs.quadBiLin Y₃.val) T.val)

theorem MSSMACC.α₂_proj (T : MSSMACC.Sols) : α₂ (proj T.toLinSols) = -α₃ (proj T.toLinSols) * ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)

theorem MSSMACC.α₁_proj (T : MSSMACC.Sols) : α₁ (proj T.toLinSols) = -α₃ (proj T.toLinSols) * ((dot B₃.val) T.val - (dot Y₃.val) T.val)

theorem MSSMACC.α₁_proj_zero (T : MSSMACC.Sols) (h1 : α₃ (proj T.toLinSols) = 0) : α₁ (proj T.toLinSols) = 0

theorem MSSMACC.α₂_proj_zero (T : MSSMACC.Sols) (h1 : α₃ (proj T.toLinSols) = 0) : α₂ (proj T.toLinSols) = 0