PhysLean Documentation

PhysLean.QFT.AnomalyCancellation.SMNu.PlusU1.HyperCharge

Hypercharge in SM with RHN. #

Relavent definitions for the SM hypercharge.

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

The hypercharge for 1 family.

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

    The hypercharge for n family.

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

      The QuadSol obtained by adding hypercharge to a QuadSol.

      Equations
      Instances For
        source
        theorem SMRHN.PlusU1.Y.addQuad_zero {n : ℕ} (S : (PlusU1 n).QuadSols) (a : ℚ) :
        addQuad S a 0 = a • S
        source
        theorem SMRHN.PlusU1.Y.on_cubeTriLin {n : ℕ} (S : (PlusU1 n).Charges) :
        ((SMνACCs.cubeTriLin (Y n).val) (Y n).val) S = 6 * SMνACCs.accYY S
        source
        theorem SMRHN.PlusU1.Y.on_cubeTriLin_AFL {n : ℕ} (S : (PlusU1 n).LinSols) :
        ((SMνACCs.cubeTriLin (Y n).val) (Y n).val) S.val = 0
        source
        theorem SMRHN.PlusU1.Y.on_cubeTriLin' {n : ℕ} (S : (PlusU1 n).Charges) :
        ((SMνACCs.cubeTriLin (Y n).val) S) S = 6 * SMνACCs.accQuad S
        source
        theorem SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ {n : ℕ} (S : (PlusU1 n).QuadSols) :
        ((SMνACCs.cubeTriLin (Y n).val) S.val) S.val = 0
        source
        theorem SMRHN.PlusU1.Y.add_AFL_cube {n : ℕ} (S : (PlusU1 n).LinSols) (a b : ℚ) :
        SMνACCs.accCube (a • S.val + b • (Y n).val) = a ^ 2 * (a * SMνACCs.accCube S.val + 3 * b * ((SMνACCs.cubeTriLin S.val) S.val) (Y n).val)
        source
        theorem SMRHN.PlusU1.Y.add_AFQ_cube {n : ℕ} (S : (PlusU1 n).QuadSols) (a b : ℚ) :
        SMνACCs.accCube (a • S.val + b • (Y n).val) = a ^ 3 * SMνACCs.accCube S.val
        source
        theorem SMRHN.PlusU1.Y.add_AF_cube {n : ℕ} (S : (PlusU1 n).Sols) (a b : ℚ) :
        SMνACCs.accCube (a • S.val + b • (Y n).val) = 0
        source
        def SMRHN.PlusU1.Y.addCube {n : ℕ} (S : (PlusU1 n).Sols) (a b : ℚ) :
        (PlusU1 n).Sols

        The Sol obtained by adding hypercharge to a Sol.

        Equations
        Instances For