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.FamilyMapsHypercharge in SM with RHN.
Relevant definitions for the SM hypercharge.
@[expose] public sectionThe hypercharge for 1 family.
@[simps!]
def Y₁ : (PlusU1 1).Sols where
val := fun i =>
match i with
| (0 : Fin 6) => 1
| (1 : Fin 6) => -4
| (2 : Fin 6) => 2
| (3 : Fin 6) => -3
| (4 : Fin 6) => 6
| (5 : Fin 6) => 0
linearSol := ⊢ ∀ (i : Fin (PlusU1 1).numberLinear),
(((PlusU1 1).linearACCs i) fun i =>
match i with
| 0 => 1
| 1 => -4
| 2 => 2
| 3 => -3
| 4 => 6
| 5 => 0) =
0
i:Fin (PlusU1 1).numberLinear⊢ (((PlusU1 1).linearACCs i) fun i =>
match i with
| 0 => 1
| 1 => -4
| 2 => 2
| 3 => -3
| 4 => 6
| 5 => 0) =
0
match i with
i:Fin (PlusU1 1).numberLinearisLt✝:0 < (PlusU1 1).numberLinear⊢ (((PlusU1 1).linearACCs ⟨0, isLt✝⟩) fun i =>
match i with
| 0 => 1
| 1 => -4
| 2 => 2
| 3 => -3
| 4 => 6
| 5 => 0) =
0 with_unfolding_all All goals completed! 🐙
i:Fin (PlusU1 1).numberLinearisLt✝:1 < (PlusU1 1).numberLinear⊢ (((PlusU1 1).linearACCs ⟨1, isLt✝⟩) fun i =>
match i with
| 0 => 1
| 1 => -4
| 2 => 2
| 3 => -3
| 4 => 6
| 5 => 0) =
0 with_unfolding_all All goals completed! 🐙
i:Fin (PlusU1 1).numberLinearisLt✝:2 < (PlusU1 1).numberLinear⊢ (((PlusU1 1).linearACCs ⟨2, isLt✝⟩) fun i =>
match i with
| 0 => 1
| 1 => -4
| 2 => 2
| 3 => -3
| 4 => 6
| 5 => 0) =
0 with_unfolding_all All goals completed! 🐙
i:Fin (PlusU1 1).numberLinearisLt✝:3 < (PlusU1 1).numberLinear⊢ (((PlusU1 1).linearACCs ⟨3, isLt✝⟩) fun i =>
match i with
| 0 => 1
| 1 => -4
| 2 => 2
| 3 => -3
| 4 => 6
| 5 => 0) =
0 with_unfolding_all All goals completed! 🐙
quadSol := ⊢ ∀ (i : Fin (PlusU1 1).numberQuadratic),
(((PlusU1 1).quadraticACCs i) fun i =>
match i with
| 0 => 1
| 1 => -4
| 2 => 2
| 3 => -3
| 4 => 6
| 5 => 0) =
0
i:Fin (PlusU1 1).numberQuadratic⊢ (((PlusU1 1).quadraticACCs i) fun i =>
match i with
| 0 => 1
| 1 => -4
| 2 => 2
| 3 => -3
| 4 => 6
| 5 => 0) =
0
match i with
i:Fin (PlusU1 1).numberQuadraticisLt✝:0 < (PlusU1 1).numberQuadratic⊢ (((PlusU1 1).quadraticACCs ⟨0, isLt✝⟩) fun i =>
match i with
| 0 => 1
| 1 => -4
| 2 => 2
| 3 => -3
| 4 => 6
| 5 => 0) =
0 with_unfolding_all All goals completed! 🐙
cubicSol := ⊢ ((PlusU1 1).cubicACC fun i =>
match i with
| 0 => 1
| 1 => -4
| 2 => 2
| 3 => -3
| 4 => 6
| 5 => 0) =
0 with_unfolding_all All goals completed! 🐙
The hypercharge for n family.
@[simps!]
def Y (n : ℕ) : (PlusU1 n).Sols :=
familyUniversalAF n Y₁n:ℕS:(PlusU1 n).Charges⊢ Y₁.val 0 * ∑ i, Q S i - 2 * Y₁.val 1 * ∑ i, U S i + Y₁.val 2 * ∑ i, D S i - Y₁.val 3 * ∑ i, L S i +
Y₁.val 4 * ∑ i, E S i =
∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i
n:ℕS:(PlusU1 n).Charges⊢ 2 * 4 = 8 ∨ ∑ x, toSpeciesEquiv S 1 x = 0
n:ℕS:(PlusU1 n).Charges⊢ True ∨ ∑ x, toSpeciesEquiv S 1 x = 0
All goals completed! 🐙All goals completed! 🐙n:ℕ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 hypercharge to a QuadSol.
def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=
linearToQuad (a • S.1 + b • (Y 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 * Y₁.val 0 * Y₁.val 0 * ∑ i, Q S i + 3 * Y₁.val 1 * Y₁.val 1 * ∑ i, U S i + 3 * Y₁.val 2 * Y₁.val 2 * ∑ i, D S i +
2 * Y₁.val 3 * Y₁.val 3 * ∑ i, L S i +
Y₁.val 4 * Y₁.val 4 * ∑ i, E S i +
Y₁.val 5 * Y₁.val 5 * ∑ i, N S i =
6 * (∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i)
n:ℕS:(PlusU1 n).Charges⊢ 6 * ∑ x, toSpeciesEquiv S 0 x + 3 * 4 * 4 * ∑ x, toSpeciesEquiv S 1 x + 3 * 2 * 2 * ∑ x, toSpeciesEquiv S 2 x +
2 * 3 * 3 * ∑ x, toSpeciesEquiv S 3 x +
6 * 6 * ∑ x, toSpeciesEquiv S 4 x =
6 *
(∑ 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)
All goals completed! 🐙n:ℕS:(PlusU1 n).LinSols⊢ 6 * 0 = 0
with_unfolding_all All goals completed! 🐙n:ℕS:(PlusU1 n).Charges⊢ 6 * Y₁.val 0 * ∑ i, Q S i * Q S i + 3 * Y₁.val 1 * ∑ i, U S i * U S i + 3 * Y₁.val 2 * ∑ i, D S i * D S i +
2 * Y₁.val 3 * ∑ i, L S i * L S i +
Y₁.val 4 * ∑ i, E S i * E S i +
Y₁.val 5 * ∑ i, N S i * N S i =
6 * (∑ i, Q S i ^ 2 - 2 * ∑ i, U S i ^ 2 + ∑ i, D S i ^ 2 - ∑ i, L S i ^ 2 + ∑ i, E S i ^ 2)
n:ℕS:(PlusU1 n).Charges⊢ 6 * ∑ x, toSpeciesEquiv S 0 x * toSpeciesEquiv S 0 x + -(3 * 4 * ∑ x, toSpeciesEquiv S 1 x * toSpeciesEquiv S 1 x) +
3 * 2 * ∑ x, toSpeciesEquiv S 2 x * toSpeciesEquiv S 2 x +
-(2 * 3 * ∑ x, toSpeciesEquiv S 3 x * toSpeciesEquiv S 3 x) +
6 * ∑ x, toSpeciesEquiv S 4 x * toSpeciesEquiv S 4 x =
6 *
(∑ x, toSpeciesEquiv S 0 x ^ 2 - 2 * ∑ x, toSpeciesEquiv S 1 x ^ 2 + ∑ x, toSpeciesEquiv S 2 x ^ 2 -
∑ x, toSpeciesEquiv S 3 x ^ 2 +
∑ x, toSpeciesEquiv S 4 x ^ 2)
All goals completed! 🐙n:ℕS:(PlusU1 n).QuadSols⊢ 6 * 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) (Y n).val))) + 3 * (b * (b * (a * 0))) =
a ^ 2 * (a * accCube S.val + 3 * b * ((cubeTriLin S.val) S.val) (Y 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) Y₁.val)))) =
a ^ 2 * (a * ((cubeTriLin S.val) S.val) S.val + 3 * b * ((cubeTriLin S.val) S.val) ((familyUniversal n) Y₁.val))
All goals completed! 🐙n:ℕS:(PlusU1 n).QuadSolsa:ℚb:ℚ⊢ a ^ 2 * (a * accCube S.val + 3 * b * 0) = a ^ 3 * accCube S.val
All goals completed! 🐙n:ℕS:(PlusU1 n).Solsa:ℚb:ℚ⊢ a ^ 3 * 0 = 0
All goals completed! 🐙
The Sol obtained by adding hypercharge to a Sol.