PhysLean Documentation

PhysLean.Particles.FlavorPhysics.CKMMatrix.Invariants

Invariants of the CKM Matrix #

The CKM matrix is only defined up to an equivalence.

This file defines some invariants of the CKM matrix, which are well-defined with respect to this equivalence.

Of note, this file defines the complex jarlskog invariant.

source
def Invariant.jarlskogℂCKM (V : CKMMatrix) :
ℂ

The complex jarlskog invariant for a CKM matrix.

Equations
Instances For
    source
    @[simp]
    theorem Invariant.jarlskogℂCKM_im (V : CKMMatrix) :
    (jarlskogℂCKM V).im = -((((↑V 0 1).re * (↑V 1 2).re - (↑V 0 1).im * (↑V 1 2).im) * (↑V 0 2).re + ((↑V 0 1).re * (↑V 1 2).im + (↑V 0 1).im * (↑V 1 2).re) * (↑V 0 2).im) * (↑V 1 1).im) + (-(((↑V 0 1).re * (↑V 1 2).re - (↑V 0 1).im * (↑V 1 2).im) * (↑V 0 2).im) + ((↑V 0 1).re * (↑V 1 2).im + (↑V 0 1).im * (↑V 1 2).re) * (↑V 0 2).re) * (↑V 1 1).re
    source
    @[simp]
    theorem Invariant.jarlskogℂCKM_re (V : CKMMatrix) :
    (jarlskogℂCKM V).re = (((↑V 0 1).re * (↑V 1 2).re - (↑V 0 1).im * (↑V 1 2).im) * (↑V 0 2).re + ((↑V 0 1).re * (↑V 1 2).im + (↑V 0 1).im * (↑V 1 2).re) * (↑V 0 2).im) * (↑V 1 1).re + (-(((↑V 0 1).re * (↑V 1 2).re - (↑V 0 1).im * (↑V 1 2).im) * (↑V 0 2).im) + ((↑V 0 1).re * (↑V 1 2).im + (↑V 0 1).im * (↑V 1 2).re) * (↑V 0 2).re) * (↑V 1 1).im
    source
    theorem Invariant.jarlskogℂCKM_equiv (V U : CKMMatrix) (h : V ≈ U) :
    jarlskogℂCKM V = jarlskogℂCKM U

    The complex jarlskog invariant is equal for equivalent CKM matrices.

    source
    def Invariant.jarlskogℂ :
    Quotient CKMMatrixSetoid → ℂ

    The complex jarlskog invariant for an equivalence class of CKM matrices.

    Equations
    Instances For
      source
      def Invariant.VusVubVcdSq (V : Quotient CKMMatrixSetoid) :
      ℝ

      An invariant for CKM matrices corresponding to the square of the absolute values of the us, ub and cb elements multiplied together divided by (VudAbs V ^ 2 + VusAbs V ^2).

      Equations
      Instances For
        source
        def Invariant.mulExpδ₁₃ (V : Quotient CKMMatrixSetoid) :
        ℂ

        An invariant for CKM matrices. The argument of this invariant is δ₁₃ in the standard parameterization.

        Equations
        Instances For