The type of solutions perpendicular to Y₃ and B₃

We define the type of solutions which are orthogonal to Y₃ and B₃ and prove some basic lemmas about them.

References

The main reference for the material in this file is:

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

structure MSSMACC.AnomalyFreePerpextends MSSMACC.LinSols : Type

The type of linear solutions orthogonal to $Y_3$ and $B_3$.

• val : MSSMACC.Charges
• linearSol (i : Fin MSSMACC.numberLinear) : (MSSMACC.linearACCs i) self.val = 0
• perpY₃ : (dot Y₃.val) self.val = 0
• perpB₃ : (dot B₃.val) self.val = 0

def MSSMACC.proj (T : MSSMACC.LinSols) : AnomalyFreePerp

The projection of an object in MSSMACC.AnomalyFreeLinear onto the subspace orthogonal to Y₃ andB₃.

Equations

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

theorem MSSMACC.proj_val (T : MSSMACC.LinSols) : (proj T).val = ((dot B₃.val) T.val - (dot Y₃.val) T.val) • Y₃.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) • B₃.val + (dot Y₃.val) B₃.val • T.val

theorem MSSMACC.Y₃_plus_B₃_plus_proj (T : MSSMACC.LinSols) (a b c : ℚ) : a • Y₃.val + b • B₃.val + c • (proj T).val = (a + c * ((dot B₃.val) T.val - (dot Y₃.val) T.val)) • Y₃.val + (b + c * ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)) • B₃.val + ((dot Y₃.val) B₃.val * c) • T.val

theorem MSSMACC.quad_Y₃_proj (T : MSSMACC.LinSols) : (MSSMACCs.quadBiLin Y₃.val) (proj T).val = (dot Y₃.val) B₃.val * (MSSMACCs.quadBiLin Y₃.val) T.val

theorem MSSMACC.quad_B₃_proj (T : MSSMACC.LinSols) : (MSSMACCs.quadBiLin B₃.val) (proj T).val = (dot Y₃.val) B₃.val * (MSSMACCs.quadBiLin B₃.val) T.val

theorem MSSMACC.quad_self_proj (T : MSSMACC.Sols) : (MSSMACCs.quadBiLin T.val) (proj T.toLinSols).val = ((dot B₃.val) T.val - (dot Y₃.val) T.val) * (MSSMACCs.quadBiLin Y₃.val) T.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (MSSMACCs.quadBiLin B₃.val) T.val

theorem MSSMACC.quad_proj (T : MSSMACC.Sols) : (MSSMACCs.quadBiLin (proj T.toLinSols).val) (proj T.toLinSols).val = 2 * (dot Y₃.val) B₃.val * (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (MSSMACCs.quadBiLin Y₃.val) T.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (MSSMACCs.quadBiLin B₃.val) T.val)

theorem MSSMACC.cube_proj_proj_Y₃ (T : MSSMACC.LinSols) : ((MSSMACCs.cubeTriLin (proj T).val) (proj T).val) Y₃.val = (dot Y₃.val) B₃.val ^ 2 * ((MSSMACCs.cubeTriLin T.val) T.val) Y₃.val

theorem MSSMACC.cube_proj_proj_B₃ (T : MSSMACC.LinSols) : ((MSSMACCs.cubeTriLin (proj T).val) (proj T).val) B₃.val = (dot Y₃.val) B₃.val ^ 2 * ((MSSMACCs.cubeTriLin T.val) T.val) B₃.val

theorem MSSMACC.cube_proj_proj_self (T : MSSMACC.Sols) : ((MSSMACCs.cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) T.val = 2 * (dot Y₃.val) B₃.val * (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((MSSMACCs.cubeTriLin T.val) T.val) Y₃.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((MSSMACCs.cubeTriLin T.val) T.val) B₃.val)

theorem MSSMACC.cube_proj (T : MSSMACC.Sols) : ((MSSMACCs.cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) (proj T.toLinSols).val = 3 * (dot Y₃.val) B₃.val ^ 2 * (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((MSSMACCs.cubeTriLin T.val) T.val) Y₃.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((MSSMACCs.cubeTriLin T.val) T.val) B₃.val)