Standard parameterization for the CKM Matrix

This file defines the standard parameterization of CKM matrices in terms of four real numbers θ₁₂, θ₁₃, θ₂₃ and δ₁₃.

We will show that every CKM matrix can be written within this standard parameterization in the file FlavorPhysics.CKMMatrix.StandardParameters.

def standParamAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : Matrix (Fin 3) (Fin 3) ℂ

Given four reals θ₁₂ θ₁₃ θ₂₃ δ₁₃ the standard parameterization of the CKM matrix as a 3×3 complex matrix.

Equations

• One or more equations did not get rendered due to their size.

theorem standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : (standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃).conjTranspose * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃ = 1

The standard parameterization forms a unitary matrix.

def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix

A CKM Matrix from four reals θ₁₂, θ₁₃, θ₂₃, and δ₁₃. This is the standard parameterization of CKM matrices.

Equations

• standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = ⟨standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, ⋯⟩

theorem standParam.cross_product_t (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : (standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃).tRow = (crossProduct ((starRingEnd (Fin 3 → ℂ)) (standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃).uRow)) ((starRingEnd (Fin 3 → ℂ)) (standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃).cRow)

The top-row of the standard parameterization is the cross product of the conjugate of the up and charm rows.

theorem standParam.eq_rows (U : CKMMatrix) {θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ} (hu : U.uRow = (standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃).uRow) (hc : U.cRow = (standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃).cRow) (hU : U.tRow = (crossProduct ((starRingEnd (Fin 3 → ℂ)) U.uRow)) ((starRingEnd (Fin 3 → ℂ)) U.cRow)) : U = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃

A CKM matrix which has rows equal to that of a standard parameterisation is equal to that standard parameterisation.

theorem standParam.eq_exp_of_phases (θ₁₂ θ₁₃ θ₂₃ δ₁₃ δ₁₃' : ℝ) (h : Complex.exp (↑δ₁₃ * Complex.I) = Complex.exp (↑δ₁₃' * Complex.I)) : standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃'

Two standard parameterisations of CKM matrices are the same matrix if they have the same angles and the exponential of their faces is equal.

theorem standParam.VusVubVcdSq_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂) (h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) : Invariant.VusVubVcdSq ⟦standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ = Real.sin θ₁₂ ^ 2 * Real.cos θ₁₃ ^ 2 * Real.sin θ₁₃ ^ 2 * Real.sin θ₂₃ ^ 2

theorem standParam.mulExpδ₁₃_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂) (h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) : Invariant.mulExpδ₁₃ ⟦standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ = Complex.sin ↑θ₁₂ * Complex.cos ↑θ₁₃ ^ 2 * Complex.sin ↑θ₂₃ * Complex.sin ↑θ₁₃ * Complex.cos ↑θ₁₂ * Complex.cos ↑θ₂₃ * Complex.exp (Complex.I * ↑δ₁₃)