PhysLean Documentation

PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.Basic

ACC system for SM with RHN (without hypercharge). #

We define the ACC system for the Standard Model (without hypercharge) with right-handed neutrinos.

source
def SMRHN.SM (n : ℕ) :
ACCSystem

The ACC system for the SM plus RHN.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem SMRHN.SM_numberLinear (n : ℕ) :
    (SM n).numberLinear = 3
    source
    @[simp]
    theorem SMRHN.SM_numberQuadratic (n : ℕ) :
    (SM n).numberQuadratic = 0
    source
    @[simp]
    theorem SMRHN.SM_quadraticACCs (n : ℕ) (i : Fin 0) :
    (SM n).quadraticACCs i = i.elim0
    source
    @[simp]
    theorem SMRHN.SM_numberCharges (n : ℕ) :
    (SM n).numberCharges = 6 * n
    source
    @[simp]
    theorem SMRHN.SM_linearACCs (n : ℕ) (i : Fin 3) :
    (SM n).linearACCs i = match i with | 0 => { toFun := fun (S : (SMνCharges n).Charges) => ∑ i : Fin n, (6 * S (finProdFinEquiv (0, i)) + 3 * S (finProdFinEquiv (1, i)) + 3 * S (finProdFinEquiv (2, i)) + 2 * S (finProdFinEquiv (3, i)) + S (finProdFinEquiv (4, i)) + S (finProdFinEquiv (5, i))), map_add' := ⋯, map_smul' := ⋯ } | 1 => { toFun := fun (S : (SMνCharges n).Charges) => ∑ i : Fin n, (3 * S (finProdFinEquiv (0, i)) + S (finProdFinEquiv (3, i))), map_add' := ⋯, map_smul' := ⋯ } | 2 => { toFun := fun (S : (SMνCharges n).Charges) => ∑ i : Fin n, (2 * S (finProdFinEquiv (0, i)) + S (finProdFinEquiv (1, i)) + S (finProdFinEquiv (2, i))), map_add' := ⋯, map_smul' := ⋯ }
    source
    @[simp]
    theorem SMRHN.SM_cubicACC_apply (n : ℕ) (S : (SMνCharges n).Charges) :
    (SM n).cubicACC S = ∑ i : Fin n, (6 * (S (finProdFinEquiv (0, i)) * S (finProdFinEquiv (0, i)) * S (finProdFinEquiv (0, i))) + 3 * (S (finProdFinEquiv (1, i)) * S (finProdFinEquiv (1, i)) * S (finProdFinEquiv (1, i))) + 3 * (S (finProdFinEquiv (2, i)) * S (finProdFinEquiv (2, i)) * S (finProdFinEquiv (2, i))) + 2 * (S (finProdFinEquiv (3, i)) * S (finProdFinEquiv (3, i)) * S (finProdFinEquiv (3, i))) + S (finProdFinEquiv (4, i)) * S (finProdFinEquiv (4, i)) * S (finProdFinEquiv (4, i)) + S (finProdFinEquiv (5, i)) * S (finProdFinEquiv (5, i)) * S (finProdFinEquiv (5, i)))
    source
    theorem SMRHN.SM.gravSol {n : ℕ} (S : (SM n).LinSols) :
    SMνACCs.accGrav S.val = 0
    source
    theorem SMRHN.SM.SU2Sol {n : ℕ} (S : (SM n).LinSols) :
    SMνACCs.accSU2 S.val = 0
    source
    theorem SMRHN.SM.SU3Sol {n : ℕ} (S : (SM n).LinSols) :
    SMνACCs.accSU3 S.val = 0
    source
    theorem SMRHN.SM.cubeSol {n : ℕ} (S : (SM n).Sols) :
    SMνACCs.accCube S.val = 0
    source
    def SMRHN.SM.chargeToLinear {n : ℕ} (S : (SM n).Charges) (hGrav : SMνACCs.accGrav S = 0) (hSU2 : SMνACCs.accSU2 S = 0) (hSU3 : SMνACCs.accSU3 S = 0) :
    (SM n).LinSols

    An element of charges which satisfies the linear ACCs gives us a element of LinSols.

    Equations
    Instances For
      source
      def SMRHN.SM.linearToQuad {n : ℕ} (S : (SM n).LinSols) :
      (SM n).QuadSols

      An element of LinSols which satisfies the quadratic ACCs gives us a element of QuadSols.

      Equations
      Instances For
        source
        def SMRHN.SM.quadToAF {n : ℕ} (S : (SM n).QuadSols) (hc : SMνACCs.accCube S.val = 0) :
        (SM n).Sols

        An element of QuadSols which satisfies the quadratic ACCs gives us a element of Sols.

        Equations
        Instances For
          source
          def SMRHN.SM.chargeToQuad {n : ℕ} (S : (SM n).Charges) (hGrav : SMνACCs.accGrav S = 0) (hSU2 : SMνACCs.accSU2 S = 0) (hSU3 : SMνACCs.accSU3 S = 0) :
          (SM n).QuadSols

          An element of charges which satisfies the linear and quadratic ACCs gives us a element of QuadSols.

          Equations
          Instances For
            source
            def SMRHN.SM.chargeToAF {n : ℕ} (S : (SM n).Charges) (hGrav : SMνACCs.accGrav S = 0) (hSU2 : SMνACCs.accSU2 S = 0) (hSU3 : SMνACCs.accSU3 S = 0) (hc : SMνACCs.accCube S = 0) :
            (SM n).Sols

            An element of charges which satisfies the linear, quadratic and cubic ACCs gives us a element of Sols.

            Equations
            Instances For
              source
              def SMRHN.SM.linearToAF {n : ℕ} (S : (SM n).LinSols) (hc : SMνACCs.accCube S.val = 0) :
              (SM n).Sols

              An element of LinSols which satisfies the quadratic and cubic ACCs gives us a element of Sols.

              Equations
              Instances For
                source
                def SMRHN.SM.perm (n : ℕ) :
                ACCSystemGroupAction (SM n)

                The permutations acting on the ACC system corresponding to the SM with RHN.

                Equations
                Instances For