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 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 =
0⊢ 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 * (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
simp only [accGrav, LinearMap.coe_mk, AddHom.coe_mk, accSU3] at h0 h2 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) = 0⊢ 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 * (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 [Fin.sum_univ_three 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) =
0⊢ 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 * (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: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) =
0⊢ 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 * (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
simp only [Fin.isValue, toSMSpecies_apply, Nat.reduceMul, Hd_apply, Fin.reduceFinMk,
Hu_apply] 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)))) =
0⊢ 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 * (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 := ring_nf All goals completed! 🐙) 9 * (h0) - 24 * (h2)