PhysLean Documentation

PhysLean.QFT.AnomalyCancellation.SM.NoGrav.Basic

Anomaly Cancellation in the Standard Model without Gravity #

This file defines the system of anomaly equations for the SM without RHN, and without the gravitational ACC.

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

The ACC system for the standard model without RHN and without the gravitational ACC.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem SM.SMNoGrav_numberQuadratic (n : ℕ) :
    (SMNoGrav n).numberQuadratic = 0
    source
    @[simp]
    theorem SM.SMNoGrav_numberCharges (n : ℕ) :
    (SMNoGrav n).numberCharges = 5 * n
    source
    @[simp]
    theorem SM.SMNoGrav_linearACCs (n : ℕ) (i : Fin 2) :
    (SMNoGrav n).linearACCs i = match i with | 0 => { toFun := fun (S : (SMCharges n).Charges) => ∑ i : Fin n, (3 * S (finProdFinEquiv (0, i)) + S (finProdFinEquiv (3, i))), map_add' := ⋯, map_smul' := ⋯ } | 1 => { toFun := fun (S : (SMCharges 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 SM.SMNoGrav_cubicACC_apply (n : ℕ) (S : (SMCharges n).Charges) :
    (SMNoGrav 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)))
    source
    @[simp]
    theorem SM.SMNoGrav_numberLinear (n : ℕ) :
    (SMNoGrav n).numberLinear = 2
    source
    @[simp]
    theorem SM.SMNoGrav_quadraticACCs (n : ℕ) (i : Fin 0) :
    (SMNoGrav n).quadraticACCs i = i.elim0
    source
    theorem SM.SMNoGrav.SU2Sol {n : ℕ} (S : (SMNoGrav n).LinSols) :
    SMACCs.accSU2 S.val = 0

    The charges in (SMNoGrav n).LinSols satisfy the SU(2) anomaly-equation.

    source
    theorem SM.SMNoGrav.SU3Sol {n : ℕ} (S : (SMNoGrav n).LinSols) :
    SMACCs.accSU3 S.val = 0

    The charges in (SMNoGrav n).LinSols satisfy the SU(3) anomaly-equation.

    source
    theorem SM.SMNoGrav.cubeSol {n : ℕ} (S : (SMNoGrav n).Sols) :
    SMACCs.accCube S.val = 0

    The charges in (SMNoGrav n).Sols satisfy the cubic anomaly-equation.

    source
    def SM.SMNoGrav.chargeToLinear {n : ℕ} (S : (SMNoGrav n).Charges) (hSU2 : SMACCs.accSU2 S = 0) (hSU3 : SMACCs.accSU3 S = 0) :
    (SMNoGrav n).LinSols

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

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

      An element of AnomalyFreeLinear which satisfies the quadratic ACCs gives us a element of AnomalyFreeQuad.

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

        An element of AnomalyFreeQuad which satisfies the quadratic ACCs gives us a element of AnomalyFree.

        Equations
        Instances For
          source
          def SM.SMNoGrav.chargeToQuad {n : ℕ} (S : (SMNoGrav n).Charges) (hSU2 : SMACCs.accSU2 S = 0) (hSU3 : SMACCs.accSU3 S = 0) :
          (SMNoGrav n).QuadSols

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

          Equations
          Instances For
            source
            def SM.SMNoGrav.chargeToAF {n : ℕ} (S : (SMNoGrav n).Charges) (hSU2 : SMACCs.accSU2 S = 0) (hSU3 : SMACCs.accSU3 S = 0) (hc : SMACCs.accCube S = 0) :
            (SMNoGrav n).Sols

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

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

              An element of AnomalyFreeLinear which satisfies the quadratic and cubic ACCs gives us a element of AnomalyFree.

              Equations
              Instances For