The CKM Matrix

The definition of the type of CKM matrices as unitary $3×3$-matrices.

An equivalence relation on CKM matrices is defined, where two matrices are equivalent if they are related by phase shifts.

The notation [V]ud etc can be used for the elements of a CKM matrix, and [V]ud|us etc for the ratios of elements.

def phaseShiftMatrix (a b c : ℝ) : Matrix (Fin 3) (Fin 3) ℂ

Given three real numbers a b c the complex matrix with exp (I * a) etc on the leading diagonal.

Equations

• phaseShiftMatrix a b c = ![![Complex.exp (Complex.I * ↑a), 0, 0], ![0, Complex.exp (Complex.I * ↑b), 0], ![0, 0, Complex.exp (Complex.I * ↑c)]]

theorem phaseShiftMatrix_one : phaseShiftMatrix 0 0 0 = 1

The phase shift matrix for zero-phases is the identity.

theorem phaseShiftMatrix_star (a b c : ℝ) : (phaseShiftMatrix a b c).conjTranspose = phaseShiftMatrix (-a) (-b) (-c)

The conjugate transpose of the phase shift matrix is the phase-shift matrix with negated phases.

theorem phaseShiftMatrix_mul (a b c d e f : ℝ) : phaseShiftMatrix a b c * phaseShiftMatrix d e f = phaseShiftMatrix (a + d) (b + e) (c + f)

The multiple of two phase shift matrices is equal to the phase shift matrix with added phases.

def phaseShift (a b c : ℝ) : ↥(Matrix.unitaryGroup (Fin 3) ℂ)

Given three real numbers a b c the unitary matrix with exp (I * a) etc on the leading diagonal.

Equations

• phaseShift a b c = ⟨phaseShiftMatrix a b c, ⋯⟩

@[simp]

theorem phaseShift_coe (a b c : ℝ) : ↑(phaseShift a b c) = ![![Complex.exp (Complex.I * ↑a), 0, 0], ![0, Complex.exp (Complex.I * ↑b), 0], ![0, 0, Complex.exp (Complex.I * ↑c)]]

theorem phaseShift_coe_matrix (a b c : ℝ) : ↑(phaseShift a b c) = phaseShiftMatrix a b c

The underlying matrix of the phase-shift element of the unitary group is the phase-shift matrix.

def PhaseShiftRelation (U V : ↥(Matrix.unitaryGroup (Fin 3) ℂ)) : Prop

The relation on unitary matrices (CKM matrices) satisfied if two unitary matrices are related by phase shifts of quarks.

Equations

• PhaseShiftRelation U V = ∃ (a : ℝ) (b : ℝ) (c : ℝ) (e : ℝ) (f : ℝ) (g : ℝ), U = phaseShift a b c * V * phaseShift e f g

theorem phaseShiftRelation_refl (U : ↥(Matrix.unitaryGroup (Fin 3) ℂ)) : PhaseShiftRelation U U

The relation PhaseShiftRelation is reflective.

theorem phaseShiftRelation_symm {U V : ↥(Matrix.unitaryGroup (Fin 3) ℂ)} : PhaseShiftRelation U V → PhaseShiftRelation V U

The relation PhaseShiftRelation is symmetric.

theorem phaseShiftRelation_trans {U V W : ↥(Matrix.unitaryGroup (Fin 3) ℂ)} : PhaseShiftRelation U V → PhaseShiftRelation V W → PhaseShiftRelation U W

The relation PhaseShiftRelation is transitive.

theorem phaseShiftRelation_equiv : Equivalence PhaseShiftRelation

The relation PhaseShiftRelation is an equivalence relation.

def CKMMatrix : Type

The type of CKM matrices.

Equations

• CKMMatrix = ↥(Matrix.unitaryGroup (Fin 3) ℂ)

theorem CKMMatrix_ext {U V : CKMMatrix} (h : ↑U = ↑V) : U = V

Two CKM matrices are equal if their underlying unitary matrices are equal.

def CKMMatrix.ud_element : Lean.ParserDescr

The udth element of the CKM matrix.

Equations

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

def CKMMatrix.us_element : Lean.ParserDescr

The usth element of the CKM matrix.

Equations

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

def CKMMatrix.ub_element : Lean.ParserDescr

The ubth element of the CKM matrix.

Equations

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

def CKMMatrix.cd_element : Lean.ParserDescr

The cdth element of the CKM matrix.

Equations

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

def CKMMatrix.cs_element : Lean.ParserDescr

The csth element of the CKM matrix.

Equations

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

def CKMMatrix.cb_element : Lean.ParserDescr

The cbth element of the CKM matrix.

Equations

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

def CKMMatrix.td_element : Lean.ParserDescr

The tdth element of the CKM matrix.

Equations

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

def CKMMatrix.ts_element : Lean.ParserDescr

The tsth element of the CKM matrix.

Equations

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

def CKMMatrix.tb_element : Lean.ParserDescr

The tbth element of the CKM matrix.

Equations

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

instance CKMMatrixSetoid : Setoid CKMMatrix

The setoid of CKM matrices defined by phase shifts of fermions.

Equations

• CKMMatrixSetoid = { r := PhaseShiftRelation, iseqv := phaseShiftRelation_equiv }

def phaseShiftApply (V : CKMMatrix) (a b c d e f : ℝ) : CKMMatrix

The matrix obtained from V by shifting the phases of the fermions.

Equations

• phaseShiftApply V a b c d e f = phaseShift a b c * V * phaseShift d e f

@[simp]

theorem phaseShiftApply_coe (V : CKMMatrix) (a b c d e f : ℝ) : ↑(phaseShiftApply V a b c d e f) = ![![Complex.exp (Complex.I * ↑a), 0, 0], ![0, Complex.exp (Complex.I * ↑b), 0], ![0, 0, Complex.exp (Complex.I * ↑c)]] * ↑V * ![![Complex.exp (Complex.I * ↑d), 0, 0], ![0, Complex.exp (Complex.I * ↑e), 0], ![0, 0, Complex.exp (Complex.I * ↑f)]]

theorem phaseShiftApply.equiv (V : CKMMatrix) (a b c d e f : ℝ) : V ≈ phaseShiftApply V a b c d e f

A CKM matrix is equivalent to a phase-shift of itself.

theorem phaseShiftApply.ud (V : CKMMatrix) (a b c d e f : ℝ) : ↑(phaseShiftApply V a b c d e f) 0 0 = Complex.exp (↑a * Complex.I + ↑d * Complex.I) * ↑V 0 0

The ud component of the CKM matrix obtained after applying a phase shift.

theorem phaseShiftApply.us (V : CKMMatrix) (a b c d e f : ℝ) : ↑(phaseShiftApply V a b c d e f) 0 1 = Complex.exp (↑a * Complex.I + ↑e * Complex.I) * ↑V 0 1

The us component of the CKM matrix obtained after applying a phase shift.

theorem phaseShiftApply.ub (V : CKMMatrix) (a b c d e f : ℝ) : ↑(phaseShiftApply V a b c d e f) 0 2 = Complex.exp (↑a * Complex.I + ↑f * Complex.I) * ↑V 0 2

The ub component of the CKM matrix obtained after applying a phase shift.

theorem phaseShiftApply.cd (V : CKMMatrix) (a b c d e f : ℝ) : ↑(phaseShiftApply V a b c d e f) 1 0 = Complex.exp (↑b * Complex.I + ↑d * Complex.I) * ↑V 1 0

The cd component of the CKM matrix obtained after applying a phase shift.

theorem phaseShiftApply.cs (V : CKMMatrix) (a b c d e f : ℝ) : ↑(phaseShiftApply V a b c d e f) 1 1 = Complex.exp (↑b * Complex.I + ↑e * Complex.I) * ↑V 1 1

The cs component of the CKM matrix obtained after applying a phase shift.

theorem phaseShiftApply.cb (V : CKMMatrix) (a b c d e f : ℝ) : ↑(phaseShiftApply V a b c d e f) 1 2 = Complex.exp (↑b * Complex.I + ↑f * Complex.I) * ↑V 1 2

The cb component of the CKM matrix obtained after applying a phase shift.

theorem phaseShiftApply.td (V : CKMMatrix) (a b c d e f : ℝ) : ↑(phaseShiftApply V a b c d e f) 2 0 = Complex.exp (↑c * Complex.I + ↑d * Complex.I) * ↑V 2 0

The td component of the CKM matrix obtained after applying a phase shift.

theorem phaseShiftApply.ts (V : CKMMatrix) (a b c d e f : ℝ) : ↑(phaseShiftApply V a b c d e f) 2 1 = Complex.exp (↑c * Complex.I + ↑e * Complex.I) * ↑V 2 1

The ts component of the CKM matrix obtained after applying a phase shift.

theorem phaseShiftApply.tb (V : CKMMatrix) (a b c d e f : ℝ) : ↑(phaseShiftApply V a b c d e f) 2 2 = Complex.exp (↑c * Complex.I + ↑f * Complex.I) * ↑V 2 2

The tb component of the CKM matrix obtained after applying a phase shift.

def VAbs' (V : ↥(Matrix.unitaryGroup (Fin 3) ℂ)) (i j : Fin 3) : ℝ

The absolute value of the (i,j)th element of V.

Equations

• VAbs' V i j = ‖↑V i j‖

theorem VAbs'_equiv (i j : Fin 3) (V U : CKMMatrix) (h : V ≈ U) : VAbs' V i j = VAbs' U i j

If two CKM matrices are equivalent (under phase shifts), then their absolute values are the same.

def VAbs (i j : Fin 3) : Quotient CKMMatrixSetoid → ℝ

The absolute value of the (i,j)th any representative of ⟦V⟧.

Equations

• VAbs i j = Quotient.lift (fun (V : CKMMatrix) => VAbs' V i j) ⋯

@[reducible, inline]

abbrev VudAbs : Quotient CKMMatrixSetoid → ℝ

The absolute value of the udth element of a representative of an equivalence class of CKM matrices.

Equations

• VudAbs = VAbs 0 0

@[reducible, inline]

abbrev VusAbs : Quotient CKMMatrixSetoid → ℝ

The absolute value of the usth element of a representative of an equivalence class of CKM matrices.

Equations

• VusAbs = VAbs 0 1

@[reducible, inline]

abbrev VubAbs : Quotient CKMMatrixSetoid → ℝ

The absolute value of the ubth element of a representative of an equivalence class of CKM matrices.

Equations

• VubAbs = VAbs 0 2

@[reducible, inline]

abbrev VcdAbs : Quotient CKMMatrixSetoid → ℝ

The absolute value of the cdth element of a representative of an equivalence class of CKM matrices.

Equations

• VcdAbs = VAbs 1 0

@[reducible, inline]

abbrev VcsAbs : Quotient CKMMatrixSetoid → ℝ

The absolute value of the csth element of a representative of an equivalence class of CKM matrices.

Equations

• VcsAbs = VAbs 1 1

@[reducible, inline]

abbrev VcbAbs : Quotient CKMMatrixSetoid → ℝ

The absolute value of the cbth element of a representative of an equivalence class of CKM matrices.

Equations

• VcbAbs = VAbs 1 2

@[reducible, inline]

abbrev VtdAbs : Quotient CKMMatrixSetoid → ℝ

The absolute value of the tdth element of a representative of an equivalence class of CKM matrices.

Equations

• VtdAbs = VAbs 2 0

@[reducible, inline]

abbrev VtsAbs : Quotient CKMMatrixSetoid → ℝ

The absolute value of the tsth element of a representative of an equivalence class of CKM matrices.

Equations

• VtsAbs = VAbs 2 1

@[reducible, inline]

abbrev VtbAbs : Quotient CKMMatrixSetoid → ℝ

The absolute value of the tbth element of a representative of an equivalence class of CKM matrices.

Equations

• VtbAbs = VAbs 2 2

def CKMMatrix.Rubud (V : CKMMatrix) : ℂ

The ratio of the ub and ud elements of a CKM matrix.

Equations

• V.Rubud = ↑V 0 2 / ↑V 0 0

def CKMMatrix.ub_ud_ratio : Lean.ParserDescr

The ratio of the ub and ud elements of a CKM matrix.

Equations

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

def CKMMatrix.Rusud (V : CKMMatrix) : ℂ

The ratio of the us and ud elements of a CKM matrix.

Equations

• V.Rusud = ↑V 0 1 / ↑V 0 0

def CKMMatrix.us_ud_ratio : Lean.ParserDescr

The ratio of the us and ud elements of a CKM matrix.

Equations

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

def CKMMatrix.Rudus (V : CKMMatrix) : ℂ

The ratio of the ud and us elements of a CKM matrix.

Equations

• V.Rudus = ↑V 0 0 / ↑V 0 1

def CKMMatrix.ud_us_ratio : Lean.ParserDescr

The ratio of the ud and us elements of a CKM matrix.

Equations

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

def CKMMatrix.Rubus (V : CKMMatrix) : ℂ

The ratio of the ub and us elements of a CKM matrix.

Equations

• V.Rubus = ↑V 0 2 / ↑V 0 1

def CKMMatrix.ub_us_ratio : Lean.ParserDescr

The ratio of the ub and us elements of a CKM matrix.

Equations

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

def CKMMatrix.Rcdcb (V : CKMMatrix) : ℂ

The ratio of the cd and cb elements of a CKM matrix.

Equations

• V.Rcdcb = ↑V 1 0 / ↑V 1 2

def CKMMatrix.cd_cb_ratio : Lean.ParserDescr

The ratio of the cd and cb elements of a CKM matrix.

Equations

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

theorem CKMMatrix.Rcdcb_mul_cb {V : CKMMatrix} (h : ↑V 1 2 ≠ 0) : ↑V 1 0 = V.Rcdcb * ↑V 1 2

def CKMMatrix.Rcscb (V : CKMMatrix) : ℂ

The ratio of the cs and cb elements of a CKM matrix.

Equations

• V.Rcscb = ↑V 1 1 / ↑V 1 2

def CKMMatrix.cs_cb_ratio : Lean.ParserDescr

The ratio of the cs and cb elements of a CKM matrix.

Equations

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

theorem CKMMatrix.Rcscb_mul_cb {V : CKMMatrix} (h : ↑V 1 2 ≠ 0) : ↑V 1 1 = V.Rcscb * ↑V 1 2

Multiplying the ratio of the cs by cb element of a CKM matrix by the cb element returns the cs element, as long as the cb element is non-zero.