PhysLean Documentation

PhysLean.Particles.FlavorPhysics.CKMMatrix.Relations

Relations for the CKM Matrix #

This file contains a collection of relations and properties between the elements of the CKM matrix.

source
theorem CKMMatrix.VAbs_sum_sq_row_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + VAbs i 2 V ^ 2 = 1

The absolute value squared of any row of a CKM matrix is 1, in terms of Vabs.

source
theorem CKMMatrix.fst_row_normalized_abs (V : CKMMatrix) :
‖↑V 0 0‖ ^ 2 + ‖↑V 0 1‖ ^ 2 + ‖↑V 0 2‖ ^ 2 = 1

The absolute value squared of the first row of a CKM matrix is 1, in terms of norm.

source
theorem CKMMatrix.snd_row_normalized_abs (V : CKMMatrix) :
‖↑V 1 0‖ ^ 2 + ‖↑V 1 1‖ ^ 2 + ‖↑V 1 2‖ ^ 2 = 1

The absolute value squared of the second row of a CKM matrix is 1, in terms of norm.

source
theorem CKMMatrix.thd_row_normalized_abs (V : CKMMatrix) :
‖↑V 2 0‖ ^ 2 + ‖↑V 2 1‖ ^ 2 + ‖↑V 2 2‖ ^ 2 = 1

The absolute value squared of the third row of a CKM matrix is 1, in terms of norm.

source
theorem CKMMatrix.fst_row_normalized_normSq (V : CKMMatrix) :
Complex.normSq (↑V 0 0) + Complex.normSq (↑V 0 1) + Complex.normSq (↑V 0 2) = 1

The absolute value squared of the first row of a CKM matrix is 1, in terms of nomSq.

source
theorem CKMMatrix.snd_row_normalized_normSq (V : CKMMatrix) :
Complex.normSq (↑V 1 0) + Complex.normSq (↑V 1 1) + Complex.normSq (↑V 1 2) = 1

The absolute value squared of the second row of a CKM matrix is 1, in terms of nomSq.

source
theorem CKMMatrix.thd_row_normalized_normSq (V : CKMMatrix) :
Complex.normSq (↑V 2 0) + Complex.normSq (↑V 2 1) + Complex.normSq (↑V 2 2) = 1

The absolute value squared of the third row of a CKM matrix is 1, in terms of nomSq.

source
theorem CKMMatrix.normSq_Vud_plus_normSq_Vus (V : CKMMatrix) :
Complex.normSq (↑V 0 0) + Complex.normSq (↑V 0 1) = 1 - Complex.normSq (↑V 0 2)
source
theorem CKMMatrix.VudAbs_sq_add_VusAbs_sq {V : Quotient CKMMatrixSetoid} :
VudAbs V ^ 2 + VusAbs V ^ 2 = 1 - VubAbs V ^ 2
source
theorem CKMMatrix.ud_us_neq_zero_iff_ub_neq_one (V : CKMMatrix) :
↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0 ↔ ‖↑V 0 2‖ ≠ 1
source
theorem CKMMatrix.normSq_Vud_plus_normSq_Vus_neq_zero_ℝ {V : CKMMatrix} (hb : ↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0) :
Complex.normSq (↑V 0 0) + Complex.normSq (↑V 0 1) ≠ 0
source
theorem CKMMatrix.VAbsub_neq_zero_Vud_Vus_neq_zero {V : Quotient CKMMatrixSetoid} (hV : VAbs 0 2 V ≠ 1) :
VudAbs V ^ 2 + VusAbs V ^ 2 ≠ 0
source
theorem CKMMatrix.VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero {V : Quotient CKMMatrixSetoid} (hV : VAbs 0 2 V ≠ 1) :
√(VudAbs V ^ 2 + VusAbs V ^ 2) ≠ 0
source
theorem CKMMatrix.normSq_Vud_plus_normSq_Vus_neq_zero_ℂ {V : CKMMatrix} (hb : ↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0) :
↑(Complex.normSq (↑V 0 0)) + ↑(Complex.normSq (↑V 0 1)) ≠ 0
source
theorem CKMMatrix.Vabs_sq_add_neq_zero {V : CKMMatrix} (hb : ↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0) :
↑(VudAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) ≠ 0
source
theorem CKMMatrix.fst_row_orthog_snd_row (V : CKMMatrix) :
↑V 1 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) = 0
source
theorem CKMMatrix.fst_row_orthog_thd_row (V : CKMMatrix) :
↑V 2 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 2 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 2 2 * (starRingEnd ℂ) (↑V 0 2) = 0
source
theorem CKMMatrix.Vcd_mul_conj_Vud (V : CKMMatrix) :
↑V 1 0 * (starRingEnd ℂ) (↑V 0 0) = -↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) - ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2)
source
theorem CKMMatrix.Vcs_mul_conj_Vus (V : CKMMatrix) :
↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) = -↑V 1 0 * (starRingEnd ℂ) (↑V 0 0) - ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2)
source
theorem CKMMatrix.VAbs_thd_eq_one_fst_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} (hV : VAbs i 2 V = 1) :
VAbs i 0 V = 0
source
theorem CKMMatrix.VAbs_thd_eq_one_snd_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} (hV : VAbs i 2 V = 1) :
VAbs i 1 V = 0
source
theorem CKMMatrix.conj_Vtb_cross_product {V : CKMMatrix} {τ : ℝ} (hτ : V.tRow = Complex.exp (↑τ * Complex.I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow)) :
(starRingEnd ℂ) (↑V 2 2) = Complex.exp (-↑τ * Complex.I) * (↑V 1 1 * ↑V 0 0 - ↑V 0 1 * ↑V 1 0)
source
theorem CKMMatrix.conj_Vtb_mul_Vud {V : CKMMatrix} {τ : ℝ} (hτ : V.tRow = Complex.exp (↑τ * Complex.I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow)) :
Complex.exp (↑τ * Complex.I) * (starRingEnd ℂ) (↑V 2 2) * (starRingEnd ℂ) (↑V 0 0) = ↑V 1 1 * (↑(Complex.normSq (↑V 0 0)) + ↑(Complex.normSq (↑V 0 1))) + ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) * ↑V 0 1
source
theorem CKMMatrix.conj_Vtb_mul_Vus {V : CKMMatrix} {τ : ℝ} (hτ : V.tRow = Complex.exp (↑τ * Complex.I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow)) :
Complex.exp (↑τ * Complex.I) * (starRingEnd ℂ) (↑V 2 2) * (starRingEnd ℂ) (↑V 0 1) = -(↑V 1 0 * (↑(Complex.normSq (↑V 0 0)) + ↑(Complex.normSq (↑V 0 1))) + ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) * ↑V 0 0)
source
theorem CKMMatrix.cs_of_ud_us_ub_cb_tb {V : CKMMatrix} (h : ↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0) {τ : ℝ} (hτ : V.tRow = Complex.exp (↑τ * Complex.I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow)) :
↑V 1 1 = (-(starRingEnd ℂ) (↑V 0 2) * ↑V 0 1 * ↑V 1 2 + Complex.exp (↑τ * Complex.I) * (starRingEnd ℂ) (↑V 2 2) * (starRingEnd ℂ) (↑V 0 0)) / (↑(Complex.normSq (↑V 0 0)) + ↑(Complex.normSq (↑V 0 1)))
source
theorem CKMMatrix.cd_of_ud_us_ub_cb_tb {V : CKMMatrix} (h : ↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0) {τ : ℝ} (hτ : V.tRow = Complex.exp (↑τ * Complex.I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow)) :
↑V 1 0 = -((starRingEnd ℂ) (↑V 0 2) * ↑V 0 0 * ↑V 1 2 + Complex.exp (↑τ * Complex.I) * (starRingEnd ℂ) (↑V 2 2) * (starRingEnd ℂ) (↑V 0 1)) / (↑(Complex.normSq (↑V 0 0)) + ↑(Complex.normSq (↑V 0 1)))
source
theorem CKMMatrix.VAbs_ge_zero (i j : Fin 3) (V : Quotient CKMMatrixSetoid) :
0 ≤ VAbs i j V
source
theorem CKMMatrix.VAbs_leq_one (i j : Fin 3) (V : Quotient CKMMatrixSetoid) :
VAbs i j V ≤ 1
source
theorem CKMMatrix.VAbs_sum_sq_col_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
VAbs 0 i V ^ 2 + VAbs 1 i V ^ 2 + VAbs 2 i V ^ 2 = 1
source
theorem CKMMatrix.thd_col_normalized_abs (V : CKMMatrix) :
‖↑V 0 2‖ ^ 2 + ‖↑V 1 2‖ ^ 2 + ‖↑V 2 2‖ ^ 2 = 1
source
theorem CKMMatrix.thd_col_normalized_normSq (V : CKMMatrix) :
Complex.normSq (↑V 0 2) + Complex.normSq (↑V 1 2) + Complex.normSq (↑V 2 2) = 1
source
theorem CKMMatrix.cb_eq_zero_of_ud_us_zero {V : CKMMatrix} (h : ↑V 0 0 = 0 ∧ ↑V 0 1 = 0) :
↑V 1 2 = 0
source
theorem CKMMatrix.cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬(↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0)) :
VcsAbs ⟦V⟧ = √(1 - VcdAbs ⟦V⟧ ^ 2)
source
theorem CKMMatrix.VcbAbs_sq_add_VtbAbs_sq (V : Quotient CKMMatrixSetoid) :
VcbAbs V ^ 2 + VtbAbs V ^ 2 = 1 - VubAbs V ^ 2
source
theorem CKMMatrix.cb_tb_neq_zero_iff_ub_neq_one (V : CKMMatrix) :
↑V 1 2 ≠ 0 ∨ ↑V 2 2 ≠ 0 ↔ ‖↑V 0 2‖ ≠ 1
source
theorem CKMMatrix.VAbs_fst_col_eq_one_snd_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} (hV : VAbs 0 i V = 1) :
VAbs 1 i V = 0
source
theorem CKMMatrix.VAbs_fst_col_eq_one_thd_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} (hV : VAbs 0 i V = 1) :
VAbs 2 i V = 0