Physlib.Particles.FlavorPhysics.CKMMatrix.Invariants

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Particles.FlavorPhysics.CKMMatrix.Basic
public import Mathlib.Analysis.Complex.Basic

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.

@[expose] public section

The complex jarlskog invariant for a CKM matrix.

def jarlskogℂCKM (V : CKMMatrix) : ℂ :=
  [V]us * [V]cb * conj [V]ub * conj [V]cs

The complex jarlskog invariant is equal for equivalent CKM matrices.


lemma jarlskogℂCKM_equiv (V U : CKMMatrix) (h : V ≈ U) :
    jarlskogℂCKM V = jarlskogℂCKM U := byV:CKMMatrixU:CKMMatrixh:V ≈ U⊢ jarlskogℂCKM V = jarlskogℂCKM U
  obtain ⟨a, b, c, e, f, g, h⟩ := hV:CKMMatrixU:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝh:V = phaseShift a b c * U * phaseShift e f g⊢ jarlskogℂCKM V = jarlskogℂCKM U
  change V = phaseShiftApply U a b c e f g at hV:CKMMatrixU:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝh:V = phaseShiftApply U a b c e f g⊢ jarlskogℂCKM V = jarlskogℂCKM U
  rw [hV:CKMMatrixU:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝh:V = phaseShiftApply U a b c e f g⊢ jarlskogℂCKM (phaseShiftApply U a b c e f g) = jarlskogℂCKM UV:CKMMatrixU:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝh:V = phaseShiftApply U a b c e f g⊢ jarlskogℂCKM (phaseShiftApply U a b c e f g) = jarlskogℂCKM U]V:CKMMatrixU:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝh:V = phaseShiftApply U a b c e f g⊢ jarlskogℂCKM (phaseShiftApply U a b c e f g) = jarlskogℂCKM U
  simp only [jarlskogℂCKM, phaseShiftApply.ub, phaseShiftApply.us, phaseShiftApply.cb,
    phaseShiftApply.cs, exp_add, _root_.map_mul, ← exp_conj, conj_ofReal, conj_I, mul_neg, exp_neg]V:CKMMatrixU:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝh:V = phaseShiftApply U a b c e f g⊢ cexp (↑a * I) * cexp (↑f * I) * ↑U 0 1 * (cexp (↑b * I) * cexp (↑g * I) * ↑U 1 2) *
      ((cexp (↑a * I))⁻¹ * (cexp (↑g * I))⁻¹ * (starRingEnd ℂ) (↑U 0 2)) *
    ((cexp (↑b * I))⁻¹ * (cexp (↑f * I))⁻¹ * (starRingEnd ℂ) (↑U 1 1)) =
  ↑U 0 1 * ↑U 1 2 * (starRingEnd ℂ) (↑U 0 2) * (starRingEnd ℂ) (↑U 1 1)
  field_simp [Complex.exp_ne_zero]All goals completed! 🐙

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

@[simp]
def jarlskogℂ : Quotient CKMMatrixSetoid → ℂ :=
  Quotient.lift jarlskogℂCKM jarlskogℂCKM_equiv

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).

def VusVubVcdSq (V : Quotient CKMMatrixSetoid) : ℝ :=
    VusAbs V ^ 2 * VubAbs V ^ 2 * VcbAbs V ^2 / (VudAbs V ^ 2 + VusAbs V ^2)

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

def mulExpδ₁₃ (V : Quotient CKMMatrixSetoid) : ℂ :=
  jarlskogℂ V + VusVubVcdSq V