Phase freedom of the CKM Matrix

The CKM matrix is only defined up to an equivalence. This leads to a freedom to shift the phases of the matrices elements of the CKM matrix.

In this file we define two sets of conditions on the CKM matrices fstRowThdColRealCond which we show can be satisfied by any CKM matrix up to equivalence and ubOnePhaseCond which we show can be satisfied by any CKM matrix up to equivalence as long as the ub element as absolute value 1.

theorem CKMMatrix.shift_ud_phase_zero (u c t d s b : ℝ) (V : CKMMatrix) (h1 : u + d = -(↑V 0 0).arg) : ↑(phaseShiftApply V u c t d s b) 0 0 = ↑(VudAbs ⟦V⟧)

theorem CKMMatrix.shift_us_phase_zero (u c t d s b : ℝ) {V : CKMMatrix} (h1 : u + s = -(↑V 0 1).arg) : ↑(phaseShiftApply V u c t d s b) 0 1 = ↑(VusAbs ⟦V⟧)

theorem CKMMatrix.shift_ub_phase_zero (u c t d s b : ℝ) {V : CKMMatrix} (h1 : u + b = -(↑V 0 2).arg) : ↑(phaseShiftApply V u c t d s b) 0 2 = ↑(VubAbs ⟦V⟧)

theorem CKMMatrix.shift_cs_phase_zero (u c t d s b : ℝ) {V : CKMMatrix} (h1 : c + s = -(↑V 1 1).arg) : ↑(phaseShiftApply V u c t d s b) 1 1 = ↑(VcsAbs ⟦V⟧)

theorem CKMMatrix.shift_cb_phase_zero (u c t d s b : ℝ) {V : CKMMatrix} (h1 : c + b = -(↑V 1 2).arg) : ↑(phaseShiftApply V u c t d s b) 1 2 = ↑(VcbAbs ⟦V⟧)

theorem CKMMatrix.shift_tb_phase_zero (u c t d s b : ℝ) {V : CKMMatrix} (h1 : t + b = -(↑V 2 2).arg) : ↑(phaseShiftApply V u c t d s b) 2 2 = ↑(VtbAbs ⟦V⟧)

theorem CKMMatrix.shift_cd_phase_pi (u c t d s b : ℝ) {V : CKMMatrix} (h1 : c + d = Real.pi - (↑V 1 0).arg) : ↑(phaseShiftApply V u c t d s b) 1 0 = -↑(VcdAbs ⟦V⟧)

theorem CKMMatrix.shift_cross_product_phase_zero (u c t d s b : ℝ) {V : CKMMatrix} {τ : ℝ} (hτ : Complex.exp (↑τ * Complex.I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow) = V.tRow) (h1 : τ = -u - c - t - d - s - b) : (phaseShiftApply V u c t d s b).tRow = (crossProduct ((starRingEnd (Fin 3 → ℂ)) (phaseShiftApply V u c t d s b).uRow)) ((starRingEnd (Fin 3 → ℂ)) (phaseShiftApply V u c t d s b).cRow)

def CKMMatrix.FstRowThdColRealCond (U : CKMMatrix) : Prop

A proposition which is satisfied by a CKM matrix if its ud, us, cb and tb elements are positive and real, and there is no phase difference between the tth-row and the cross product of the conjugates of the uth and cth rows.

Equations

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

def CKMMatrix.ubOnePhaseCond (U : CKMMatrix) : Prop

A proposition which is satisfied by a CKM matrix ub is one, ud, us and cb are zero, there is no phase difference between the tth-row and the cross product of the conjugates of the uth and cth rows, and the cdth and csth elements are real and related in a set way.

Equations

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

theorem CKMMatrix.fstRowThdColRealCond_shift_solution (a b c d e f : ℝ) {τ : ℝ} {V : CKMMatrix} (h1 : a + d = -(↑V 0 0).arg) (h2 : a + e = -(↑V 0 1).arg) (h3 : b + f = -(↑V 1 2).arg) (h4 : c + f = -(↑V 2 2).arg) (h5 : τ = -a - b - c - d - e - f) : b = -τ + (↑V 0 0).arg + (↑V 0 1).arg + (↑V 2 2).arg + a ∧ c = -τ + (↑V 1 2).arg + (↑V 0 0).arg + (↑V 0 1).arg + a ∧ d = -(↑V 0 0).arg - a ∧ e = -(↑V 0 1).arg - a ∧ f = τ - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg - a

theorem CKMMatrix.ubOnePhaseCond_shift_solution (a b c d e f : ℝ) {V : CKMMatrix} (h1 : a + f = -(↑V 0 2).arg) (h2 : 0 = -a - b - c - d - e - f) (h3 : b + d = Real.pi - (↑V 1 0).arg) (h5 : b + e = -(↑V 1 1).arg) : c = -Real.pi + (↑V 1 0).arg + (↑V 1 1).arg + (↑V 0 2).arg + b ∧ d = Real.pi - (↑V 1 0).arg - b ∧ e = -(↑V 1 1).arg - b ∧ f = -(↑V 0 2).arg - a

theorem CKMMatrix.fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) : ∃ (U : CKMMatrix), V ≈ U ∧ U.FstRowThdColRealCond

theorem CKMMatrix.ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬(↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0)) (hV : V.FstRowThdColRealCond) : ∃ (U : CKMMatrix), V ≈ U ∧ U.ubOnePhaseCond

theorem CKMMatrix.cd_of_fstRowThdColRealCond {V : CKMMatrix} (hb : ↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0) (hV : V.FstRowThdColRealCond) : ↑V 1 0 = -↑(VtbAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) / (↑(VudAbs ⟦V⟧) ^ 2 + ↑(VusAbs ⟦V⟧) ^ 2) + -↑(VubAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) * ↑(VcbAbs ⟦V⟧) / (↑(VudAbs ⟦V⟧) ^ 2 + ↑(VusAbs ⟦V⟧) ^ 2) * Complex.exp (-↑(↑V 0 2).arg * Complex.I)

theorem CKMMatrix.cs_of_fstRowThdColRealCond {V : CKMMatrix} (hb : ↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0) (hV : V.FstRowThdColRealCond) : ↑V 1 1 = ↑(VtbAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) / (↑(VudAbs ⟦V⟧) ^ 2 + ↑(VusAbs ⟦V⟧) ^ 2) + -↑(VubAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) * ↑(VcbAbs ⟦V⟧) / (↑(VudAbs ⟦V⟧) ^ 2 + ↑(VusAbs ⟦V⟧) ^ 2) * Complex.exp (-↑(↑V 0 2).arg * Complex.I)