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.Basic public import Mathlib.Tactic.LinearCombination

The definition of the solution B₃ and properties thereof

We define B₃ and show that it is a double point of the cubic.

References

The main reference for the material in this file is:

[Allanach, Madigan and Tooby-Smith][Allanach:2021yjy]

@[expose] public section

B₃ is the charge which is $B-L$ in all families, but with the third family of the opposite sign.

def B₃AsCharge : MSSMACC.Charges := toSpecies.symm fun s => fun i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => - 1 | 1, 0 => - 1 | 1, 1 => - 1 | 1, 2 => 1 | 2, 0 => - 1 | 2, 1 => - 1 | 2, 2 => 1 | 3, 0 => - 3 | 3, 1 => - 3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => - 3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => - 3, fun s => match s with | 0 => -3 | 1 => 3

B₃ as a solution.

def B₃ : MSSMACC.Sols := MSSMACC.AnomalyFreeMk B₃AsCharge (accGrav B₃AsCharge = 0 with_unfolding_all All goals completed! 🐙) (accSU2 B₃AsCharge = 0 with_unfolding_all All goals completed! 🐙) (accSU3 B₃AsCharge = 0 with_unfolding_all All goals completed! 🐙) (accYY B₃AsCharge = 0 with_unfolding_all All goals completed! 🐙) (accQuad B₃AsCharge = 0 with_unfolding_all All goals completed! 🐙) (accCube B₃AsCharge = 0 with_unfolding_all All goals completed! 🐙)
lemma B₃_val : B₃.val = B₃AsCharge := B₃.val = B₃AsCharge All goals completed! 🐙R:MSSMACC.LinSolshLin: (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h0:(match 0, with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h2:(match 2, with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 06 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 R:MSSMACC.LinSolshLin: (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h0: i, (6 * Q R.val i + 3 * U R.val i + 3 * D R.val i + 2 * L R.val i + E R.val i + N R.val i) + 2 * (Hd R.val + Hu R.val) = 0h2: i, (2 * Q R.val i + U R.val i + D R.val i) = 06 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 erw [R:MSSMACC.LinSolshLin: (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h0:6 * Q R.val 0 + 3 * U R.val 0 + 3 * D R.val 0 + 2 * L R.val 0 + E R.val 0 + N R.val 0 + (6 * Q R.val 1 + 3 * U R.val 1 + 3 * D R.val 1 + 2 * L R.val 1 + E R.val 1 + N R.val 1) + (6 * Q R.val 2 + 3 * U R.val 2 + 3 * D R.val 2 + 2 * L R.val 2 + E R.val 2 + N R.val 2) + 2 * (Hd R.val + Hu R.val) = 0h2:2 * Q R.val 0 + U R.val 0 + D R.val 0 + (2 * Q R.val 1 + U R.val 1 + D R.val 1) + (2 * Q R.val 2 + U R.val 2 + D R.val 2) = 06 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0R:MSSMACC.LinSolshLin: (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h0:6 * Q R.val 0 + 3 * U R.val 0 + 3 * D R.val 0 + 2 * L R.val 0 + E R.val 0 + N R.val 0 + (6 * Q R.val 1 + 3 * U R.val 1 + 3 * D R.val 1 + 2 * L R.val 1 + E R.val 1 + N R.val 1) + (6 * Q R.val 2 + 3 * U R.val 2 + 3 * D R.val 2 + 2 * L R.val 2 + E R.val 2 + N R.val 2) + 2 * (Hd R.val + Hu R.val) = 0h2:2 * Q R.val 0 + U R.val 0 + D R.val 0 + (2 * Q R.val 1 + U R.val 1 + D R.val 1) + (2 * Q R.val 2 + U R.val 2 + D R.val 2) = 06 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 at h0 h2 R:MSSMACC.LinSolshLin: (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h0:6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))) + 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0))) + R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + R.val (Fin.castAdd 2 (finProdFinEquiv (5, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))) + 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1))) + R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1))) + R.val (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))) + 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2))) + R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2))) + R.val (Fin.castAdd 2 (finProdFinEquiv (5, 2)))) + 2 * (R.val 18 + R.val 19) = 0h2:2 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0))) + R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))) + (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1))) + R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1)))) + (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2))) + R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2)))) = 06 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2))) + 3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (5, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 linear_combination (norm := All goals completed! 🐙) 9 * (h0) - 24 * (h2)