1. Physlib
  2. Particles
  3. SuperSymmetry
  4. MSSMNu
  5. AnomalyCancellation
  6. OrthogY3B3
  7. Basic
Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.LineY3B3

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

@[expose] public section

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

structure AnomalyFreePerp extends MSSMACC.LinSols where perpY₃ : dot Y₃.val val = 0 perpB₃ : dot B₃.val val = 0

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

set_option backward.isDefEq.respectTransparency false inT:MSSMACC.LinSols⊢ ((dot B₃.val) T.val - (dot Y₃.val) T.val) * 108 + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * 108 + 108 * (dot B₃.val) T.val = 0 All goals completed! 🐙⟩
lemma 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 := 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 All goals completed! 🐙T:MSSMACC.LinSolsa:ℚb:ℚc:ℚ⊢ a • Y₃.val + b • B₃.val + (c • ((dot B₃.val) T.val - (dot Y₃.val) T.val) • Y₃.val + c • ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) • B₃.val + c • (dot Y₃.val) B₃.val • 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 All goals completed! 🐙T:MSSMACC.LinSols⊢ ((dot B₃.val) T.val - (dot Y₃.val) T.val) * 0 + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * 0 + (dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val = (dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val All goals completed! 🐙T:MSSMACC.LinSols⊢ ((dot B₃.val) T.val - (dot Y₃.val) T.val) * 0 + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * 0 + (dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val = (dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val All goals completed! 🐙T:MSSMACC.Sols⊢ ((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val + (dot Y₃.val) B₃.val * 0 = ((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val All goals completed! 🐙T:MSSMACC.Sols⊢ ((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val) + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) + (dot Y₃.val) B₃.val * (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val) = 2 * (dot Y₃.val) B₃.val * (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val) All goals completed! 🐙T:MSSMACC.LinSols⊢ 0 + (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((dot Y₃.val) B₃.val * 0) + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((dot Y₃.val) B₃.val * 0)) + ((dot Y₃.val) B₃.val * (((dot B₃.val) T.val - (dot Y₃.val) T.val) * 0) + (dot Y₃.val) B₃.val * (((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * 0) + (dot Y₃.val) B₃.val * ((dot Y₃.val) B₃.val * ((cubeTriLin T.val) T.val) Y₃.val)) = (dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val All goals completed! 🐙T:MSSMACC.LinSols⊢ 0 + (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((dot Y₃.val) B₃.val * 0) + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((dot Y₃.val) B₃.val * 0)) + ((dot Y₃.val) B₃.val * (((dot B₃.val) T.val - (dot Y₃.val) T.val) * 0) + (dot Y₃.val) B₃.val * (((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * 0) + (dot Y₃.val) B₃.val * ((dot Y₃.val) B₃.val * ((cubeTriLin T.val) T.val) B₃.val)) = (dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val All goals completed! 🐙T:MSSMACC.Sols⊢ 0 + (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((dot Y₃.val) B₃.val * ((cubeTriLin T.val) T.val) Y₃.val) + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((dot Y₃.val) B₃.val * ((cubeTriLin T.val) T.val) B₃.val)) + (dot Y₃.val) B₃.val * (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val + (dot Y₃.val) B₃.val * 0) = 2 * (dot Y₃.val) B₃.val * (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val) All goals completed! 🐙T:MSSMACC.Sols⊢ ((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val) + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val) + (dot Y₃.val) B₃.val * (2 * (dot Y₃.val) B₃.val * (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) = 3 * (dot Y₃.val) B₃.val ^ 2 * (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val + ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val) All goals completed! 🐙