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.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.FamilyMapsB Minus L in SM with RHN.
Relevant definitions for the SM B-L.
@[expose] public section$B - L$ in the 1-family case.
@[simps!]
def BL₁ : (PlusU1 1).Sols where
val := fun i =>
match i with
| (0 : Fin 6) => 1
| (1 : Fin 6) => -1
| (2 : Fin 6) => -1
| (3 : Fin 6) => -3
| (4 : Fin 6) => 3
| (5 : Fin 6) => 3
linearSol := n:ℕ⊢ ∀ (i : Fin (PlusU1 1).numberLinear),
(((PlusU1 1).linearACCs i) fun i =>
match i with
| 0 => 1
| 1 => -1
| 2 => -1
| 3 => -3
| 4 => 3
| 5 => 3) =
0
n:ℕi:Fin (PlusU1 1).numberLinear⊢ (((PlusU1 1).linearACCs i) fun i =>
match i with
| 0 => 1
| 1 => -1
| 2 => -1
| 3 => -3
| 4 => 3
| 5 => 3) =
0
match i with
n:ℕi:Fin (PlusU1 1).numberLinearisLt✝:0 < (PlusU1 1).numberLinear⊢ (((PlusU1 1).linearACCs ⟨0, isLt✝⟩) fun i =>
match i with
| 0 => 1
| 1 => -1
| 2 => -1
| 3 => -3
| 4 => 3
| 5 => 3) =
0 with_unfolding_all All goals completed! 🐙
n:ℕi:Fin (PlusU1 1).numberLinearisLt✝:1 < (PlusU1 1).numberLinear⊢ (((PlusU1 1).linearACCs ⟨1, isLt✝⟩) fun i =>
match i with
| 0 => 1
| 1 => -1
| 2 => -1
| 3 => -3
| 4 => 3
| 5 => 3) =
0 with_unfolding_all All goals completed! 🐙
n:ℕi:Fin (PlusU1 1).numberLinearisLt✝:2 < (PlusU1 1).numberLinear⊢ (((PlusU1 1).linearACCs ⟨2, isLt✝⟩) fun i =>
match i with
| 0 => 1
| 1 => -1
| 2 => -1
| 3 => -3
| 4 => 3
| 5 => 3) =
0 with_unfolding_all All goals completed! 🐙
n:ℕi:Fin (PlusU1 1).numberLinearisLt✝:3 < (PlusU1 1).numberLinear⊢ (((PlusU1 1).linearACCs ⟨3, isLt✝⟩) fun i =>
match i with
| 0 => 1
| 1 => -1
| 2 => -1
| 3 => -3
| 4 => 3
| 5 => 3) =
0 with_unfolding_all All goals completed! 🐙
quadSol := n:ℕ⊢ ∀ (i : Fin (PlusU1 1).numberQuadratic),
(((PlusU1 1).quadraticACCs i) fun i =>
match i with
| 0 => 1
| 1 => -1
| 2 => -1
| 3 => -3
| 4 => 3
| 5 => 3) =
0
n:ℕi:Fin (PlusU1 1).numberQuadratic⊢ (((PlusU1 1).quadraticACCs i) fun i =>
match i with
| 0 => 1
| 1 => -1
| 2 => -1
| 3 => -3
| 4 => 3
| 5 => 3) =
0
match i with
n:ℕi:Fin (PlusU1 1).numberQuadraticisLt✝:0 < (PlusU1 1).numberQuadratic⊢ (((PlusU1 1).quadraticACCs ⟨0, isLt✝⟩) fun i =>
match i with
| 0 => 1
| 1 => -1
| 2 => -1
| 3 => -3
| 4 => 3
| 5 => 3) =
0 with_unfolding_all All goals completed! 🐙
cubicSol := n:ℕ⊢ ((PlusU1 1).cubicACC fun i =>
match i with
| 0 => 1
| 1 => -1
| 2 => -1
| 3 => -3
| 4 => 3
| 5 => 3) =
0 with_unfolding_all All goals completed! 🐙$B - L$ in the $n$-family case.
@[simps!]
def BL (n : ℕ) : (PlusU1 n).Sols :=
familyUniversalAF n BL₁n:ℕS:(PlusU1 n).Charges⊢ BL₁.val 0 * ∑ i, Q S i - 2 * BL₁.val 1 * ∑ i, U S i + BL₁.val 2 * ∑ i, D S i - BL₁.val 3 * ∑ i, L S i +
BL₁.val 4 * ∑ i, E S i =
1 / 2 * (∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i) +
3 / 2 * (3 * ∑ i, Q S i + ∑ i, L S i) -
2 * (2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i)
n:ℕS:(PlusU1 n).Charges⊢ ∑ x, toSpeciesEquiv S 0 x + 2 * ∑ x, toSpeciesEquiv S 1 x + -∑ x, toSpeciesEquiv S 2 x + 3 * ∑ x, toSpeciesEquiv S 3 x +
3 * ∑ x, toSpeciesEquiv S 4 x =
1 / 2 *
(∑ x, toSpeciesEquiv S 0 x + 8 * ∑ x, toSpeciesEquiv S 1 x + 2 * ∑ x, toSpeciesEquiv S 2 x +
3 * ∑ x, toSpeciesEquiv S 3 x +
6 * ∑ x, toSpeciesEquiv S 4 x) +
3 / 2 * (3 * ∑ x, toSpeciesEquiv S 0 x + ∑ x, toSpeciesEquiv S 3 x) -
2 * (2 * ∑ x, toSpeciesEquiv S 0 x + ∑ x, toSpeciesEquiv S 1 x + ∑ x, toSpeciesEquiv S 2 x)
All goals completed! 🐙n:ℕS:(PlusU1 n).LinSols⊢ 1 / 2 * 0 + 3 / 2 * 0 - 2 * 0 = 0
with_unfolding_all All goals completed! 🐙n:ℕS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ quadBiLin.toHomogeneousQuad (a • S.val) + 0 + 2 * (a * (b * 0)) = a ^ 2 * accQuad S.val
erw [n:ℕS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ a ^ 2 * accQuad S.val + 0 + 2 * (a * (b * 0)) = a ^ 2 * accQuad S.valn:ℕS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ a ^ 2 * accQuad S.val + 0 + 2 * (a * (b * 0)) = a ^ 2 * accQuad S.val
All goals completed! 🐙n:ℕS:(PlusU1 n).QuadSolsa:ℚb:ℚ⊢ a ^ 2 * 0 = 0
All goals completed! 🐙
The QuadSol obtained by adding $B-L$ to a QuadSol.
def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=
linearToQuad (a • S.1 + b • (BL n).1.1) (add_quad S a b)lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ) : addQuad S a 0 = a • S := n:ℕS:(PlusU1 n).QuadSolsa:ℚ⊢ addQuad S a 0 = a • S
n:ℕS:(PlusU1 n).QuadSolsa:ℚ⊢ { toLinSols := a • S.toLinSols, quadSol := ⋯ } = a • S
All goals completed! 🐙n:ℕS:(PlusU1 n).Charges⊢ 6 * BL₁.val 0 * BL₁.val 0 * ∑ i, Q S i + 3 * BL₁.val 1 * BL₁.val 1 * ∑ i, U S i +
3 * BL₁.val 2 * BL₁.val 2 * ∑ i, D S i +
2 * BL₁.val 3 * BL₁.val 3 * ∑ i, L S i +
BL₁.val 4 * BL₁.val 4 * ∑ i, E S i +
BL₁.val 5 * BL₁.val 5 * ∑ i, N S i =
9 * (6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i + ∑ i, N S i) -
24 * (2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i)
n:ℕS:(PlusU1 n).Charges⊢ 6 * ∑ x, toSpeciesEquiv S 0 x + 3 * ∑ x, toSpeciesEquiv S 1 x + 3 * ∑ x, toSpeciesEquiv S 2 x +
2 * 3 * 3 * ∑ x, toSpeciesEquiv S 3 x +
3 * 3 * ∑ x, toSpeciesEquiv S 4 x +
3 * 3 * ∑ x, toSpeciesEquiv S 5 x =
9 *
(6 * ∑ x, toSpeciesEquiv S 0 x + 3 * ∑ x, toSpeciesEquiv S 1 x + 3 * ∑ x, toSpeciesEquiv S 2 x +
2 * ∑ x, toSpeciesEquiv S 3 x +
∑ x, toSpeciesEquiv S 4 x +
∑ x, toSpeciesEquiv S 5 x) -
24 * (2 * ∑ x, toSpeciesEquiv S 0 x + ∑ x, toSpeciesEquiv S 1 x + ∑ x, toSpeciesEquiv S 2 x)
All goals completed! 🐙n:ℕS:(PlusU1 n).LinSols⊢ 9 * 0 - 24 * 0 = 0
with_unfolding_all All goals completed! 🐙n:ℕS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ a ^ 3 * accCube S.val + 0 + 3 * (a * (a * (b * ((cubeTriLin S.val) S.val) (BL n).val))) + 3 * (b * (b * (a * 0))) =
a ^ 2 * (a * accCube S.val + 3 * b * ((cubeTriLin S.val) S.val) (BL n).val)
n:ℕS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ a ^ 3 * ((cubeTriLin S.val) S.val) S.val +
3 * (a * (a * (b * ((cubeTriLin S.val) S.val) ((familyUniversal n) BL₁.val)))) =
a ^ 2 * (a * ((cubeTriLin S.val) S.val) S.val + 3 * b * ((cubeTriLin S.val) S.val) ((familyUniversal n) BL₁.val))
All goals completed! 🐙