PhysLean Documentation

PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BMinusL

B Minus L in SM with RHN. #

Relavent definitions for the SM B-L.

source
def SMRHN.PlusU1.BL₁ :
(PlusU1 1).Sols

$B - L$ in the 1-family case.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem SMRHN.PlusU1.BL₁_val (i : Fin (PlusU1 1).numberCharges) :
    BL₁.val i = match i with | 0 => 1 | 1 => -1 | 2 => -1 | 3 => -3 | 4 => 3 | 5 => 3
    source
    def SMRHN.PlusU1.BL (n : ℕ) :
    (PlusU1 n).Sols

    $B - L$ in the $n$-family case.

    Equations
    Instances For
      source
      @[simp]
      theorem SMRHN.PlusU1.BL_val (n : ℕ) :
      (BL n).val = (familyUniversal n) BL₁.val
      source
      theorem SMRHN.PlusU1.BL.on_quadBiLin {n : ℕ} (S : (PlusU1 n).Charges) :
      (SMνACCs.quadBiLin (BL n).val) S = 1 / 2 * SMνACCs.accYY S + 3 / 2 * SMνACCs.accSU2 S - 2 * SMνACCs.accSU3 S
      source
      theorem SMRHN.PlusU1.BL.on_quadBiLin_AFL {n : ℕ} (S : (PlusU1 n).LinSols) :
      (SMνACCs.quadBiLin (BL n).val) S.val = 0
      source
      theorem SMRHN.PlusU1.BL.add_AFL_quad {n : ℕ} (S : (PlusU1 n).LinSols) (a b : ℚ) :
      SMνACCs.accQuad (a • S.val + b • (BL n).val) = a ^ 2 * SMνACCs.accQuad S.val
      source
      theorem SMRHN.PlusU1.BL.add_quad {n : ℕ} (S : (PlusU1 n).QuadSols) (a b : ℚ) :
      SMνACCs.accQuad (a • S.val + b • (BL n).val) = 0
      source
      def SMRHN.PlusU1.BL.addQuad {n : ℕ} (S : (PlusU1 n).QuadSols) (a b : ℚ) :
      (PlusU1 n).QuadSols

      The QuadSol obtained by adding $B-L$ to a QuadSol.

      Equations
      Instances For
        source
        theorem SMRHN.PlusU1.BL.addQuad_zero {n : ℕ} (S : (PlusU1 n).QuadSols) (a : ℚ) :
        addQuad S a 0 = a • S
        source
        theorem SMRHN.PlusU1.BL.on_cubeTriLin {n : ℕ} (S : (PlusU1 n).Charges) :
        ((SMνACCs.cubeTriLin (BL n).val) (BL n).val) S = 9 * SMνACCs.accGrav S - 24 * SMνACCs.accSU3 S
        source
        theorem SMRHN.PlusU1.BL.on_cubeTriLin_AFL {n : ℕ} (S : (PlusU1 n).LinSols) :
        ((SMνACCs.cubeTriLin (BL n).val) (BL n).val) S.val = 0
        source
        theorem SMRHN.PlusU1.BL.add_AFL_cube {n : ℕ} (S : (PlusU1 n).LinSols) (a b : ℚ) :
        SMνACCs.accCube (a • S.val + b • (BL n).val) = a ^ 2 * (a * SMνACCs.accCube S.val + 3 * b * ((SMνACCs.cubeTriLin S.val) S.val) (BL n).val)