Documentation

PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.HyperCharge

Hypercharge in SM with RHN. #

Relevant definitions for the SM hypercharge.

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

The hypercharge for 1 family.

Equations
    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