1. Physlib
  2. Particles
  3. FlavorPhysics
  4. CKMMatrix
  5. PhaseFreedom
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.Relations

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.

@[expose] public sectionu:ℝc:ℝt:ℝd:ℝs:ℝb:ℝV:CKMMatrixh1:u + d = -(↑V 0 0).arg⊢ ↑‖↑V 0 0‖ = ↑(VudAbs ⟦V⟧) All goals completed! 🐙u:ℝc:ℝt:ℝd:ℝs:ℝb:ℝV:CKMMatrixh1:u + s = -(↑V 0 1).arg⊢ ↑‖↑V 0 1‖ = ↑(VusAbs ⟦V⟧) All goals completed! 🐙u:ℝc:ℝt:ℝd:ℝs:ℝb:ℝV:CKMMatrixh1:u + b = -(↑V 0 2).arg⊢ ↑‖↑V 0 2‖ = ↑(VubAbs ⟦V⟧) All goals completed! 🐙u:ℝc:ℝt:ℝd:ℝs:ℝb:ℝV:CKMMatrixh1:c + s = -(↑V 1 1).arg⊢ ↑‖↑V 1 1‖ = ↑(VcsAbs ⟦V⟧) All goals completed! 🐙u:ℝc:ℝt:ℝd:ℝs:ℝb:ℝV:CKMMatrixh1:c + b = -(↑V 1 2).arg⊢ ↑‖↑V 1 2‖ = ↑(VcbAbs ⟦V⟧) All goals completed! 🐙u:ℝc:ℝt:ℝd:ℝs:ℝb:ℝV:CKMMatrixh1:t + b = -(↑V 2 2).arg⊢ ↑‖↑V 2 2‖ = ↑(VtbAbs ⟦V⟧) All goals completed! 🐙u:ℝc:ℝt:ℝd:ℝs:ℝb:ℝV:CKMMatrixh1:c + d = Real.pi - (↑V 1 0).argh2:↑(↑V 1 0).arg * I + (↑c * I + ↑d * I) = ↑((↑V 1 0).arg + (c + d)) * I⊢ ↑‖↑V 1 0‖ * cexp (↑((↑V 1 0).arg + (Real.pi - (↑V 1 0).arg)) * I) = -↑(VcdAbs ⟦V⟧) u:ℝc:ℝt:ℝd:ℝs:ℝb:ℝV:CKMMatrixh1:c + d = Real.pi - (↑V 1 0).argh2:↑(↑V 1 0).arg * I + (↑c * I + ↑d * I) = ↑((↑V 1 0).arg + (c + d)) * I⊢ ‖↑V 1 0‖ = VAbs 1 0 ⟦V⟧ All goals completed! 🐙u:ℝc:ℝt:ℝd:ℝs:ℝb:ℝV:CKMMatrixτ:ℝhτ:cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c) = [V]th1:τ = -u - c - t - d - s - bhτ0:cexp (↑τ * I) * (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c) 2 = ↑V 2 2⊢ cexp (↑t * I + ↑b * I + ↑(-u - c - t - d - s - b) * I) * (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c) 2 = cexp (-(↑u * I) + -(↑c * I) + -(↑d * I) + -(↑s * I)) * (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c) 2 u:ℝc:ℝt:ℝd:ℝs:ℝb:ℝV:CKMMatrixτ:ℝhτ:cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c) = [V]th1:τ = -u - c - t - d - s - bhτ0:cexp (↑τ * I) * (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c) 2 = ↑V 2 2⊢ ↑t * I + ↑b * I + ↑(-u - c - t - d - s - b) * I = -(↑u * I) + -(↑c * I) + -(↑d * I) + -(↑s * I) u:ℝc:ℝt:ℝd:ℝs:ℝb:ℝV:CKMMatrixτ:ℝhτ:cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c) = [V]th1:τ = -u - c - t - d - s - bhτ0:cexp (↑τ * I) * (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c) 2 = ↑V 2 2⊢ ↑t * I + ↑b * I + (-↑u - ↑c - ↑t - ↑d - ↑s - ↑b) * I = -(↑u * I) + -(↑c * I) + -(↑d * I) + -(↑s * I) All goals completed! 🐙

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.

def FstRowThdColRealCond (U : CKMMatrix) : Prop := [U]ud = VudAbs ⟦U⟧ ∧ [U]us = VusAbs ⟦U⟧ ∧ [U]cb = VcbAbs ⟦U⟧ ∧ [U]tb = VtbAbs ⟦U⟧ ∧ [U]t = conj [U]u ⨯₃ conj [U]c

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.

def ubOnePhaseCond (U : CKMMatrix) : Prop := [U]ud = 0 ∧ [U]us = 0 ∧ [U]cb = 0 ∧ [U]ub = 1 ∧ [U]t = conj [U]u ⨯₃ conj [U]c ∧ [U]cd = - VcdAbs ⟦U⟧ ∧ [U]cs = √(1 - VcdAbs ⟦U⟧ ^ 2)
a:ℝb:ℝc:ℝf:ℝτ:ℝV:CKMMatrixhbf:b = -(↑V 1 2).arg - (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg)hcf:c = -(↑V 2 2).arg - (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg)h5:τ = a + (↑V 1 2).arg + f + (↑V 2 2).arg + (↑V 0 0).arg + (↑V 0 1).arghf:f = τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg⊢ -(↑V 1 2).arg - f = f - (-a - (-(↑V 1 2).arg - f) - (-(↑V 2 2).arg - f) - (-(↑V 0 0).arg - a) - (-(↑V 0 1).arg - a)) + (↑V 0 0).arg + (↑V 0 1).arg + (↑V 2 2).arg + a ∧ -(↑V 2 2).arg - f = f - (-a - (-(↑V 1 2).arg - f) - (-(↑V 2 2).arg - f) - (-(↑V 0 0).arg - a) - (-(↑V 0 1).arg - a)) + (↑V 1 2).arg + (↑V 0 0).arg + (↑V 0 1).arg + a ∧ f = -a - (-(↑V 1 2).arg - f) - (-(↑V 2 2).arg - f) - (-(↑V 0 0).arg - a) - (-(↑V 0 1).arg - a) - f - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg - a a:ℝb:ℝc:ℝf:ℝτ:ℝV:CKMMatrixh5:τ = a + (↑V 1 2).arg + f + (↑V 2 2).arg + (↑V 0 0).arg + (↑V 0 1).arghf:f = τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arghbf:b = -τ + a + (↑V 0 0).arg + (↑V 0 1).arg + (↑V 2 2).arghcf:c = (↑V 1 2).arg - τ + a + (↑V 0 0).arg + (↑V 0 1).arg⊢ -(↑V 1 2).arg - f = f - (-a - (-(↑V 1 2).arg - f) - (-(↑V 2 2).arg - f) - (-(↑V 0 0).arg - a) - (-(↑V 0 1).arg - a)) + (↑V 0 0).arg + (↑V 0 1).arg + (↑V 2 2).arg + a ∧ -(↑V 2 2).arg - f = f - (-a - (-(↑V 1 2).arg - f) - (-(↑V 2 2).arg - f) - (-(↑V 0 0).arg - a) - (-(↑V 0 1).arg - a)) + (↑V 1 2).arg + (↑V 0 0).arg + (↑V 0 1).arg + a ∧ f = -a - (-(↑V 1 2).arg - f) - (-(↑V 2 2).arg - f) - (-(↑V 0 0).arg - a) - (-(↑V 0 1).arg - a) - f - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg - a a:ℝτ:ℝV:CKMMatrixh5:τ = a + (↑V 1 2).arg + (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg) + (↑V 2 2).arg + (↑V 0 0).arg + (↑V 0 1).arg⊢ -(↑V 1 2).arg - (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg) = τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg - (-a - (-(↑V 1 2).arg - (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg)) - (-(↑V 2 2).arg - (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg)) - (-(↑V 0 0).arg - a) - (-(↑V 0 1).arg - a)) + (↑V 0 0).arg + (↑V 0 1).arg + (↑V 2 2).arg + a ∧ -(↑V 2 2).arg - (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg) = τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg - (-a - (-(↑V 1 2).arg - (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg)) - (-(↑V 2 2).arg - (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg)) - (-(↑V 0 0).arg - a) - (-(↑V 0 1).arg - a)) + (↑V 1 2).arg + (↑V 0 0).arg + (↑V 0 1).arg + a ∧ τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg = -a - (-(↑V 1 2).arg - (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg)) - (-(↑V 2 2).arg - (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg)) - (-(↑V 0 0).arg - a) - (-(↑V 0 1).arg - a) - (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg) - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg - a a:ℝτ:ℝV:CKMMatrixh5:τ = a + (↑V 1 2).arg + (τ - a - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg) + (↑V 2 2).arg + (↑V 0 0).arg + (↑V 0 1).arg⊢ True ∧ True ∧ True All goals completed! 🐙a:ℝb:ℝc:ℝV:CKMMatrixh2:0 = b - c - Real.pi + (↑V 1 0).arg + (↑V 1 1).arg + (↑V 0 2).arghc:c = -Real.pi + (↑V 1 0).arg + (↑V 1 1).arg + (↑V 0 2).arg + b⊢ c = -Real.pi + (↑V 1 0).arg + (↑V 1 1).arg + (↑V 0 2).arg + b a:ℝb:ℝV:CKMMatrixh2:0 = b - (-Real.pi + (↑V 1 0).arg + (↑V 1 1).arg + (↑V 0 2).arg + b) - Real.pi + (↑V 1 0).arg + (↑V 1 1).arg + (↑V 0 2).arg⊢ -Real.pi + (↑V 1 0).arg + (↑V 1 1).arg + (↑V 0 2).arg + b = -Real.pi + (↑V 1 0).arg + (↑V 1 1).arg + (↑V 0 2).arg + b All goals completed! 🐙V:CKMMatrixτ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)U:CKMMatrix := phaseShiftApply V 0 (-τ + (↑V 0 0).arg + (↑V 0 1).arg + (↑V 2 2).arg) (-τ + (↑V 1 2).arg + (↑V 0 0).arg + (↑V 0 1).arg) (-(↑V 0 0).arg) (-(↑V 0 1).arg) (τ - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg)hUV:⟦U⟧ = ⟦V⟧⊢ ↑U 2 2 = ↑(VtbAbs ⟦V⟧) V:CKMMatrixτ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)U:CKMMatrix := phaseShiftApply V 0 (-τ + (↑V 0 0).arg + (↑V 0 1).arg + (↑V 2 2).arg) (-τ + (↑V 1 2).arg + (↑V 0 0).arg + (↑V 0 1).arg) (-(↑V 0 0).arg) (-(↑V 0 1).arg) (τ - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg)hUV:⟦U⟧ = ⟦V⟧⊢ -τ + (↑V 1 2).arg + (↑V 0 0).arg + (↑V 0 1).arg + (τ - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg) = -(↑V 2 2).arg All goals completed! 🐙 V:CKMMatrixτ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)U:CKMMatrix := phaseShiftApply V 0 (-τ + (↑V 0 0).arg + (↑V 0 1).arg + (↑V 2 2).arg) (-τ + (↑V 1 2).arg + (↑V 0 0).arg + (↑V 0 1).arg) (-(↑V 0 0).arg) (-(↑V 0 1).arg) (τ - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg)hUV:⟦U⟧ = ⟦V⟧⊢ [U]t = (crossProduct ((starRingEnd (Fin 3 → ℂ)) [U]u)) ((starRingEnd (Fin 3 → ℂ)) [U]c) V:CKMMatrixτ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)U:CKMMatrix := phaseShiftApply V 0 (-τ + (↑V 0 0).arg + (↑V 0 1).arg + (↑V 2 2).arg) (-τ + (↑V 1 2).arg + (↑V 0 0).arg + (↑V 0 1).arg) (-(↑V 0 0).arg) (-(↑V 0 1).arg) (τ - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg)hUV:⟦U⟧ = ⟦V⟧⊢ τ = -0 - (-τ + (↑V 0 0).arg + (↑V 0 1).arg + (↑V 2 2).arg) - (-τ + (↑V 1 2).arg + (↑V 0 0).arg + (↑V 0 1).arg) - -(↑V 0 0).arg - -(↑V 0 1).arg - (τ - (↑V 0 0).arg - (↑V 0 1).arg - (↑V 1 2).arg - (↑V 2 2).arg) All goals completed! 🐙All goals completed! 🐙V:CKMMatrixhb:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0hV:V.FstRowThdColRealCondhτ:[V]t = cexp (↑0 * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)hx:↑(VudAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) ≠ 0h1:(starRingEnd ℂ) (↑V 0 2) = ↑(VubAbs ⟦V⟧) * cexp (-↑(↑V 0 2).arg * I)⊢ (-(↑(VAbs 2 2 ⟦V⟧) * ↑(VAbs 0 1 ⟦V⟧)) + -(↑(VubAbs ⟦V⟧) * cexp (-↑(↑V 0 2).arg * I) * ↑(VAbs 0 0 ⟦V⟧) * ↑(VAbs 1 2 ⟦V⟧))) / (↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2) = (-(↑(VAbs 2 2 ⟦V⟧) * ↑(VAbs 0 1 ⟦V⟧)) + -(↑(VAbs 0 0 ⟦V⟧) * ↑(VAbs 1 2 ⟦V⟧) * ↑(VAbs 0 2 ⟦V⟧) * cexp (-(↑(↑V 0 2).arg * I)))) / (↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2) All goals completed! 🐙V:CKMMatrixhb:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0hV:V.FstRowThdColRealCondhτ:[V]t = cexp (↑0 * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)hx:↑(VudAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) ≠ 0h1:(starRingEnd ℂ) (↑V 0 2) = ↑(VubAbs ⟦V⟧) * cexp (-↑(↑V 0 2).arg * I)⊢ (-(↑(VubAbs ⟦V⟧) * cexp (-↑(↑V 0 2).arg * I) * ↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 1 2 ⟦V⟧)) + ↑(VAbs 2 2 ⟦V⟧) * ↑(VAbs 0 0 ⟦V⟧)) / (↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2) = (↑(VAbs 2 2 ⟦V⟧) * ↑(VAbs 0 0 ⟦V⟧) + -(↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 1 2 ⟦V⟧) * ↑(VAbs 0 2 ⟦V⟧) * cexp (-(↑(↑V 0 2).arg * I)))) / (↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2) All goals completed! 🐙