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.LinearCombinationThe 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 =
0⊢ 6 * 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
simp only [accYY, LinearMap.coe_mk, AddHom.coe_mk] at h3 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) = 0⊢ 6 * 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 [Fin.sum_univ_three 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) =
0⊢ 6 * 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: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) =
0⊢ 6 * 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
simp only [Fin.isValue, toSMSpecies_apply, Nat.reduceMul, Hd_apply, Fin.reduceFinMk,
Hu_apply] 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) =
0⊢ 6 * 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 := ring_nf All goals completed! 🐙) 6 * h3