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 Y₃ and properties thereof

We define $Y_3$ and show that it is a double point of the cubic.

References

The main reference for the material in this file is:

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

@[expose] public section

$Y_3$ is the charge which is hypercharge in all families, but with the third family of the opposite sign.

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

$Y_3$ as a solution.

def Y₃ : MSSMACC.Sols := MSSMACC.AnomalyFreeMk Y₃AsCharge (accGrav Y₃AsCharge = 0 with_unfolding_all All goals completed! 🐙) (accSU2 Y₃AsCharge = 0 with_unfolding_all All goals completed! 🐙) (accSU3 Y₃AsCharge = 0 with_unfolding_all All goals completed! 🐙) (accYY Y₃AsCharge = 0 with_unfolding_all All goals completed! 🐙) (accQuad Y₃AsCharge = 0 with_unfolding_all All goals completed! 🐙) (accCube Y₃AsCharge = 0 with_unfolding_all All goals completed! 🐙)
lemma Y₃_val : Y₃.val = Y₃AsCharge := Y₃.val = Y₃AsCharge All goals completed! 🐙R:MSSMACC.LinSolshLin: (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h3:(match 3, with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 06 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 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 = 0h3: i, (Q R.val i + 8 * U R.val i + 2 * D R.val i + 3 * L R.val i + 6 * E R.val i) + 3 * (Hd R.val + Hu R.val) = 06 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 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 = 0h3:Q R.val 0 + 8 * U R.val 0 + 2 * D R.val 0 + 3 * L R.val 0 + 6 * E R.val 0 + (Q R.val 1 + 8 * U R.val 1 + 2 * D R.val 1 + 3 * L R.val 1 + 6 * E R.val 1) + (Q R.val 2 + 8 * U R.val 2 + 2 * D R.val 2 + 3 * L R.val 2 + 6 * E R.val 2) + 3 * (Hd R.val + Hu R.val) = 06 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 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 = 0h3:Q R.val 0 + 8 * U R.val 0 + 2 * D R.val 0 + 3 * L R.val 0 + 6 * E R.val 0 + (Q R.val 1 + 8 * U R.val 1 + 2 * D R.val 1 + 3 * L R.val 1 + 6 * E R.val 1) + (Q R.val 2 + 8 * U R.val 2 + 2 * D R.val 2 + 3 * L R.val 2 + 6 * E R.val 2) + 3 * (Hd R.val + Hu R.val) = 06 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 at h3 R:MSSMACC.LinSolshLin: (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h3:R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 8 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0))) + 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0))) + 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 8 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1))) + 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1))) + 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 8 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2))) + 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2))) + 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + 3 * (R.val 18 + R.val 19) = 06 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * 4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + 3 * (2 * 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2)))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 linear_combination (norm := All goals completed! 🐙) 6 * h3