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.PhaseFreedom public import Physlib.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.Basic

Standard parameters for the CKM Matrix

Given a CKM matrix V we can extract four real numbers θ₁₂, θ₁₃, θ₂₃ and δ₁₃. These, when used in the standard parameterization return V up to equivalence.

This leads to the theorem standParam.exists_for_CKMatrix which says that up to equivalence every CKM matrix can be written using the standard parameterization.

@[expose] public section

Given a CKM matrix V the real number corresponding to sin θ₁₂ in the standard parameterization. -

def S₁₂ (V : Quotient CKMMatrixSetoid) : := VusAbs V / ( (VudAbs V ^ 2 + VusAbs V ^ 2))

Given a CKM matrix V the real number corresponding to sin θ₁₃ in the standard parameterization. -

def S₁₃ (V : Quotient CKMMatrixSetoid) : := VubAbs V

Given a CKM matrix V the real number corresponding to sin θ₂₃ in the standard parameterization. -

def S₂₃ (V : Quotient CKMMatrixSetoid) : := if VubAbs V = 1 then VcdAbs V else VcbAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2)

Given a CKM matrix V the real number corresponding to θ₁₂ in the standard parameterization. -

def θ₁₂ (V : Quotient CKMMatrixSetoid) : := Real.arcsin (S₁₂ V)

Given a CKM matrix V the real number corresponding to θ₁₃ in the standard parameterization. -

def θ₁₃ (V : Quotient CKMMatrixSetoid) : := Real.arcsin (S₁₃ V)

Given a CKM matrix V the real number corresponding to θ₂₃ in the standard parameterization. -

def θ₂₃ (V : Quotient CKMMatrixSetoid) : := Real.arcsin (S₂₃ V)

Given a CKM matrix V the real number corresponding to cos θ₁₂ in the standard parameterization. -

def C₁₂ (V : Quotient CKMMatrixSetoid) : := Real.cos (θ₁₂ V)

Given a CKM matrix V the real number corresponding to cos θ₁₃ in the standard parameterization. -

def C₁₃ (V : Quotient CKMMatrixSetoid) : := Real.cos (θ₁₃ V)

Given a CKM matrix V the real number corresponding to sin θ₂₃ in the standard parameterization. -

def C₂₃ (V : Quotient CKMMatrixSetoid) : := Real.cos (θ₂₃ V)

Given a CKM matrix V the real number corresponding to the phase δ₁₃ in the standard parameterization. -

def δ₁₃ (V : Quotient CKMMatrixSetoid) : := arg (Invariant.mulExpδ₁₃ V)

For a CKM matrix sin θ₁₂ is non-negative.

lemma S₁₂_nonneg (V : Quotient CKMMatrixSetoid) : 0 S₁₂ V := div_nonneg (VAbs_ge_zero 0 1 V) (Real.sqrt_nonneg _)

For a CKM matrix sin θ₁₃ is non-negative.

lemma S₁₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 S₁₃ V := VAbs_ge_zero 0 2 V

For a CKM matrix sin θ₂₃ is non-negative.

V:Quotient CKMMatrixSetoid0 if VubAbs V = 1 then VcdAbs V else VcbAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2) V:Quotient CKMMatrixSetoidh✝:VubAbs V = 10 VcdAbs VV:Quotient CKMMatrixSetoidh✝:¬VubAbs V = 10 VcbAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2) V:Quotient CKMMatrixSetoidh✝:VubAbs V = 10 VcdAbs V All goals completed! 🐙 V:Quotient CKMMatrixSetoidh✝:¬VubAbs V = 10 VcbAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2) All goals completed! 🐙

For a CKM matrix sin θ₁₂ is less than or equal to 1.

V:Quotient CKMMatrixSetoidVusAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2) 1 All goals completed! 🐙

For a CKM matrix sin θ₁₃ is less than or equal to 1.

lemma S₁₃_leq_one (V : Quotient CKMMatrixSetoid) : S₁₃ V 1 := VAbs_leq_one 0 2 V

For a CKM matrix sin θ₂₃ is less than or equal to 1.

V:Quotient CKMMatrixSetoidh✝:¬VubAbs V = 1VcbAbs V (VcbAbs V ^ 2 + VtbAbs V ^ 2) All goals completed! 🐙
lemma S₁₂_eq_sin_θ₁₂ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₁₂ V) = S₁₂ V := Real.sin_arcsin (le_trans (V:Quotient CKMMatrixSetoid-1 0 All goals completed! 🐙) (S₁₂_nonneg V)) (S₁₂_leq_one V)lemma S₁₃_eq_sin_θ₁₃ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₁₃ V) = S₁₃ V := Real.sin_arcsin (le_trans (V:Quotient CKMMatrixSetoid-1 0 All goals completed! 🐙) (S₁₃_nonneg V)) (S₁₃_leq_one V)lemma S₂₃_eq_sin_θ₂₃ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₂₃ V) = S₂₃ V := Real.sin_arcsin (le_trans (V:Quotient CKMMatrixSetoid-1 0 All goals completed! 🐙) (S₂₃_nonneg V)) (S₂₃_leq_one V)lemma S₁₂_eq_ℂsin_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.sin (θ₁₂ V) = S₁₂ V := (ofReal_sin _).symm.trans (congrArg ofReal (S₁₂_eq_sin_θ₁₂ V))lemma S₁₃_eq_ℂsin_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.sin (θ₁₃ V) = S₁₃ V := (ofReal_sin _).symm.trans (congrArg ofReal (S₁₃_eq_sin_θ₁₃ V))lemma S₂₃_eq_ℂsin_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.sin (θ₂₃ V) = S₂₃ V := (ofReal_sin _).symm.trans (congrArg ofReal (S₂₃_eq_sin_θ₂₃ V))V:Quotient CKMMatrixSetoidS₁₂ V = S₁₂ V All goals completed! 🐙V:Quotient CKMMatrixSetoidS₁₃ V = S₁₃ V All goals completed! 🐙V:Quotient CKMMatrixSetoidS₂₃ V = S₂₃ V All goals completed! 🐙lemma S₁₂_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₁₂ V = 0 := V:Quotient CKMMatrixSetoidha:VubAbs V = 1S₁₂ V = 0 All goals completed! 🐙lemma S₁₃_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₁₃ V = 1 := haAll goals completed! 🐙All goals completed! 🐙lemma C₁₂_eq_ℂcos_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₁₂ V) = C₁₂ V := V:Quotient CKMMatrixSetoidcos (θ₁₂ V) = (C₁₂ V) All goals completed! 🐙lemma C₁₃_eq_ℂcos_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₁₃ V) = C₁₃ V := V:Quotient CKMMatrixSetoidcos (θ₁₃ V) = (C₁₃ V) All goals completed! 🐙lemma C₂₃_eq_ℂcos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₂₃ V) = C₂₃ V := V:Quotient CKMMatrixSetoidcos (θ₂₃ V) = (C₂₃ V) All goals completed! 🐙V:Quotient CKMMatrixSetoidC₁₂ V = (C₁₂ V) All goals completed! 🐙V:Quotient CKMMatrixSetoidC₁₃ V = (C₁₃ V) All goals completed! 🐙V:Quotient CKMMatrixSetoidC₂₃ V = (C₂₃ V) All goals completed! 🐙lemma S₁₂_sq_add_C₁₂_sq (V : Quotient CKMMatrixSetoid) : S₁₂ V ^ 2 + C₁₂ V ^ 2 = 1 := V:Quotient CKMMatrixSetoidS₁₂ V ^ 2 + C₁₂ V ^ 2 = 1 All goals completed! 🐙lemma S₁₃_sq_add_C₁₃_sq (V : Quotient CKMMatrixSetoid) : S₁₃ V ^ 2 + C₁₃ V ^ 2 = 1 := V:Quotient CKMMatrixSetoidS₁₃ V ^ 2 + C₁₃ V ^ 2 = 1 All goals completed! 🐙lemma S₂₃_sq_add_C₂₃_sq (V : Quotient CKMMatrixSetoid) : S₂₃ V ^ 2 + C₂₃ V ^ 2 = 1 := V:Quotient CKMMatrixSetoidS₂₃ V ^ 2 + C₂₃ V ^ 2 = 1 All goals completed! 🐙lemma C₁₂_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : C₁₂ V = 1 := V:Quotient CKMMatrixSetoidha:VubAbs V = 1C₁₂ V = 1 All goals completed! 🐙lemma C₁₃_of_Vub_eq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : C₁₃ V = 0 := V:Quotient CKMMatrixSetoidha:VubAbs V = 1C₁₃ V = 0 All goals completed! 🐙All goals completed! 🐙 All goals completed! 🐙 All goals completed! 🐙All goals completed! 🐙V:Quotient CKMMatrixSetoidha:VubAbs V 1VudAbs V ^ 2 + VusAbs V ^ 2 0 All goals completed! 🐙 All goals completed! 🐙V:Quotient CKMMatrixSetoidha:¬VubAbs V = 1VudAbs V = (VudAbs V ^ 2 + VusAbs V ^ 2) * (VudAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2)) All goals completed! 🐙V:Quotient CKMMatrixSetoidha:¬VubAbs V = 1VusAbs V = (VudAbs V ^ 2 + VusAbs V ^ 2) * (VusAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2)) All goals completed! 🐙lemma VubAbs_eq_S₁₃ (V : Quotient CKMMatrixSetoid) : VubAbs V = S₁₃ V := rflV:Quotient CKMMatrixSetoidha:¬VubAbs V = 1VcbAbs V = (VudAbs V ^ 2 + VusAbs V ^ 2) * (VcbAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2)) All goals completed! 🐙V:Quotient CKMMatrixSetoidha:¬VubAbs V = 1VtbAbs V = (VudAbs V ^ 2 + VusAbs V ^ 2) * (VtbAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2)) All goals completed! 🐙V:Quotient CKMMatrixSetoidh1:1 - S₁₃ V ^ 2 0S₁₃ V = 1 V:Quotient CKMMatrixSetoidh1:1 - S₁₃ V ^ 2 01 S₁₃ V All goals completed! 🐙V:CKMMatrixReal.cos (θ₁₂ V) * Real.cos (θ₁₃ V) = 0 S₁₃ V = 0 S₁₂ V * Real.cos (θ₁₃ V) = 0 S₂₃ V * Real.cos (θ₁₃ V) = 0 Real.cos (θ₂₃ V) * Real.cos (θ₁₃ V) = 0 Real.cos (θ₁₂ V) = 0 Real.cos (θ₁₃ V) = 0 Real.cos (θ₂₃ V) = 0 S₁₂ V = 0 S₁₃ V = 0 S₂₃ V = 0 All goals completed! 🐙lemma mulExpδ₁₃_on_param_δ₁₃ (V : CKMMatrix) (δ₁₃ : ) : mulExpδ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ = sin (θ₁₂ V) * cos (θ₁₃ V) ^ 2 * sin (θ₂₃ V) * sin (θ₁₃ V) * cos (θ₁₂ V) * cos (θ₂₃ V) * cexp (I * δ₁₃) := V:CKMMatrixδ₁₃:mulExpδ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ = sin (θ₁₂ V) * cos (θ₁₃ V) ^ 2 * sin (θ₂₃ V) * sin (θ₁₃ V) * cos (θ₁₂ V) * cos (θ₂₃ V) * cexp (I * δ₁₃) V:CKMMatrixδ₁₃:0 Real.sin (θ₁₂ V)V:CKMMatrixδ₁₃:0 Real.sin (θ₂₃ V) V:CKMMatrixδ₁₃:0 Real.sin (θ₁₂ V) All goals completed! 🐙 V:CKMMatrixδ₁₃:0 Real.sin (θ₂₃ V) All goals completed! 🐙V:CKMMatrixδ₁₃:sin (θ₁₂ V) * cos (θ₁₃ V) ^ 2 * sin (θ₂₃ V) * sin (θ₁₃ V) * cos (θ₁₂ V) * cos (θ₂₃ V) * cexp (I * δ₁₃) = 0 cos (θ₁₂ V) * cos (θ₁₃ V) = 0 sin (θ₁₃ V) = 0 sin (θ₁₂ V) * cos (θ₁₃ V) = 0 sin (θ₂₃ V) * cos (θ₁₃ V) = 0 cos (θ₂₃ V) * cos (θ₁₃ V) = 0 V:CKMMatrixδ₁₃:((((sin (θ₁₂ V) = 0 cos (θ₁₃ V) = 0) sin (θ₂₃ V) = 0) sin (θ₁₃ V) = 0) cos (θ₁₂ V) = 0) cos (θ₂₃ V) = 0 (cos (θ₁₂ V) = 0 cos (θ₁₃ V) = 0) sin (θ₁₃ V) = 0 (sin (θ₁₂ V) = 0 cos (θ₁₃ V) = 0) (sin (θ₂₃ V) = 0 cos (θ₁₃ V) = 0) cos (θ₂₃ V) = 0 cos (θ₁₃ V) = 0 All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙lemma on_param_cos_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ) (h : Real.cos (θ₁₃ V) = 0) : standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 := V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ = phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃) V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1i:Fin 3j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) i j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) i j V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 0, ) jV:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 1, ) jV:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 2, ) j V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 0, ) jV:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 1, ) jV:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 2, ) j V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 0, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 1, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 2, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 2, ) V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 0, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 1, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 2, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 2, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 0, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 1, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 2, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 2, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 0, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 1, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₃ V) = 0hub:VubAbs V = 1(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 2, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 2, ) All goals completed! 🐙lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ) (h : Real.cos (θ₁₂ V) = 0) : standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 := V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ = phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃) V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0i:Fin 3j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) i j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) i j V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 0, ) jV:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 1, ) jV:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 2, ) j V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 0, ) jV:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 1, ) jV:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 2, ) j V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 0, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 1, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 2, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 2, ) V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 0, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 1, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 2, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 2, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 0, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 1, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 2, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 2, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 0, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 1, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 2, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 2, ) V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0cos (θ₂₃ V) * cos (θ₁₃ V) = cexp (I * δ₁₃) * (cos (θ₂₃ V) * cos (θ₁₃ V)) * (cexp (I * δ₁₃))⁻¹ V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0sin (θ₁₂ V) * cos (θ₂₃ V) = cexp (I * δ₁₃) * (sin (θ₁₂ V) * cos (θ₂₃ V)) * (cexp (I * δ₁₃))⁻¹V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0sin (θ₁₂ V) * sin (θ₁₃ V) * sin (θ₂₃ V) * cexp (I * δ₁₃) = cexp (I * δ₁₃) * (sin (θ₁₂ V) * sin (θ₁₃ V) * sin (θ₂₃ V))V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0sin (θ₂₃ V) * cos (θ₁₃ V) = cexp (I * δ₁₃) * (sin (θ₂₃ V) * cos (θ₁₃ V)) * (cexp (I * δ₁₃))⁻¹V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0sin (θ₁₂ V) * sin (θ₂₃ V) = cexp (I * δ₁₃) * (sin (θ₁₂ V) * sin (θ₂₃ V)) * (cexp (I * δ₁₃))⁻¹V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0sin (θ₁₂ V) * sin (θ₁₃ V) * cos (θ₂₃ V) * cexp (I * δ₁₃) = cexp (I * δ₁₃) * (sin (θ₁₂ V) * sin (θ₁₃ V) * cos (θ₂₃ V))V:CKMMatrixδ₁₃:h:Real.cos (θ₁₂ V) = 0cos (θ₂₃ V) * cos (θ₁₃ V) = cexp (I * δ₁₃) * (cos (θ₂₃ V) * cos (θ₁₃ V)) * (cexp (I * δ₁₃))⁻¹ All goals completed! 🐙lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ) (h : Real.cos (θ₂₃ V) = 0) : standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 := V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ = phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃) V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0i:Fin 3j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) i j = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) i j V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) j = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 0, ) jV:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) j = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 1, ) jV:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) j = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) j V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) j = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 0, ) jV:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) j = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 1, ) jV:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) j = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) j V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 0, ) = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 1, ) = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 2, ) = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 2, ) V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 0, ) = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 1, ) = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 2, ) = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 2, )V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 0, ) = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 1, ) = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 2, ) = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 2, )V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 0, ) = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 1, ) = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 2, ) = (phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 2, ) All goals completed! 🐙 V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0cos (θ₁₂ V) * sin (θ₁₃ V) * sin (θ₂₃ V) * cexp (I * δ₁₃) = cexp (I * δ₁₃) * (cos (θ₁₂ V) * sin (θ₁₃ V) * sin (θ₂₃ V))V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0sin (θ₁₂ V) * sin (θ₁₃ V) * sin (θ₂₃ V) * cexp (I * δ₁₃) = cexp (I * δ₁₃) * (sin (θ₁₂ V) * sin (θ₁₃ V) * sin (θ₂₃ V))V:CKMMatrixδ₁₃:h:Real.cos (θ₂₃ V) = 0sin (θ₂₃ V) * cos (θ₁₃ V) = cexp (I * δ₁₃) * (sin (θ₂₃ V) * cos (θ₁₃ V)) * (cexp (I * δ₁₃))⁻¹ All goals completed! 🐙lemma on_param_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ) (h : Real.sin (θ₁₃ V) = 0) : standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 := V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ = phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0 V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0i:Fin 3j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) i j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) i j V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 0, ) jV:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 1, ) jV:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 2, ) j V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 0, ) jV:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 1, ) jV:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) j = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 2, ) j V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 0, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 2, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 1, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 2, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 2, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 2, ) ((fun i => i) 2, ) V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 0, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 0, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 1, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 0, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 2, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 0, ) ((fun i => i) 2, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 0, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 1, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 1, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 1, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 2, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 1, ) ((fun i => i) 2, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 0, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 2, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 1, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 2, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 2, ) = (phaseShift 0 0 0 * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 0) ((fun i => i) 2, ) ((fun i => i) 2, ) All goals completed! 🐙lemma on_param_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ) (h : Real.sin (θ₁₂ V) = 0) : standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 := V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ = phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃) V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0i:Fin 3j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) i j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) i j V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 0, ) jV:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 1, ) jV:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 2, ) j V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 0, ) jV:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 1, ) jV:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) j = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 2, ) j V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 0, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 1, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 2, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 2, ) V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 0, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 1, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 2, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 2, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 0, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 1, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 2, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 2, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 0, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 1, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 2, ) = (phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 2, ) V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0cos (θ₂₃ V) * cos (θ₁₃ V) = cexp (I * δ₁₃) * (cos (θ₂₃ V) * cos (θ₁₃ V)) * (cexp (I * δ₁₃))⁻¹ V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0cos (θ₁₂ V) * sin (θ₁₃ V) * sin (θ₂₃ V) * cexp (I * δ₁₃) = cexp (I * δ₁₃) * (cos (θ₁₂ V) * sin (θ₁₃ V) * sin (θ₂₃ V))V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0cos (θ₁₂ V) * cos (θ₂₃ V) = cexp (I * δ₁₃) * (cos (θ₁₂ V) * cos (θ₂₃ V)) * (cexp (I * δ₁₃))⁻¹V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0sin (θ₂₃ V) * cos (θ₁₃ V) = cexp (I * δ₁₃) * (sin (θ₂₃ V) * cos (θ₁₃ V)) * (cexp (I * δ₁₃))⁻¹V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0cos (θ₁₂ V) * sin (θ₁₃ V) * cos (θ₂₃ V) * cexp (I * δ₁₃) = cexp (I * δ₁₃) * (cos (θ₁₂ V) * sin (θ₁₃ V) * cos (θ₂₃ V))V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0cos (θ₁₂ V) * sin (θ₂₃ V) = cexp (I * δ₁₃) * (cos (θ₁₂ V) * sin (θ₂₃ V)) * (cexp (I * δ₁₃))⁻¹V:CKMMatrixδ₁₃:h:Real.sin (θ₁₂ V) = 0cos (θ₂₃ V) * cos (θ₁₃ V) = cexp (I * δ₁₃) * (cos (θ₂₃ V) * cos (θ₁₃ V)) * (cexp (I * δ₁₃))⁻¹ All goals completed! 🐙lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ) (h : Real.sin (θ₂₃ V) = 0) : standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 := V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃ = phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃) V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0i:Fin 3j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) i j = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) i j V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) j = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 0, ) jV:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) j = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 1, ) jV:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) j = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) j V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) j = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 0, ) jV:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) j = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 1, ) jV:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0j:Fin 3(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) j = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) j V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 0, ) = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 1, ) = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 2, ) = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 2, ) V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 0, ) = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 1, ) = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 0, ) ((fun i => i) 2, ) = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 0, ) ((fun i => i) 2, )V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 0, ) = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 1, ) = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 1, ) ((fun i => i) 2, ) = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 1, ) ((fun i => i) 2, )V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 0, ) = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 0, )V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 1, ) = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 1, )V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0(standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) δ₁₃) ((fun i => i) 2, ) ((fun i => i) 2, ) = (phaseShift 0 0 δ₁₃ * standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) 2, ) ((fun i => i) 2, ) V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0cos (θ₂₃ V) * cos (θ₁₃ V) = cexp (I * δ₁₃) * (cos (θ₂₃ V) * cos (θ₁₃ V)) * (cexp (I * δ₁₃))⁻¹ V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0cos (θ₁₂ V) * sin (θ₁₃ V) * cos (θ₂₃ V) * cexp (I * δ₁₃) = cexp (I * δ₁₃) * (cos (θ₁₂ V) * sin (θ₁₃ V) * cos (θ₂₃ V))V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0sin (θ₁₂ V) * sin (θ₁₃ V) * cos (θ₂₃ V) * cexp (I * δ₁₃) = cexp (I * δ₁₃) * (sin (θ₁₂ V) * sin (θ₁₃ V) * cos (θ₂₃ V))V:CKMMatrixδ₁₃:h:Real.sin (θ₂₃ V) = 0cos (θ₂₃ V) * cos (θ₁₃ V) = cexp (I * δ₁₃) * (cos (θ₂₃ V) * cos (θ₁₃ V)) * (cexp (I * δ₁₃))⁻¹ All goals completed! 🐙V:CKMMatrixhb:V 0 0 0 V 0 1 0hV:V.FstRowThdColRealCondhb':VubAbs V 1h1:(VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) * (VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) = (VAbs 0 0 V) ^ 2 + (VAbs 0 1 V) ^ 2hx:(VudAbs V) * (VudAbs V) + (VusAbs V) * (VusAbs V) 0(VtbAbs V) * (VudAbs V) / ((VudAbs V) ^ 2 + (VusAbs V) ^ 2) + -(VubAbs V) * (VusAbs V) * (VcbAbs V) / ((VudAbs V) ^ 2 + (VusAbs V) ^ 2) * cexp (-(V 0 2).arg * I) = (VudAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2)) * (VtbAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2)) - (VusAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2)) * (VubAbs V) * (VcbAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2)) * cexp (-(I * (V 0 2).arg)) V:CKMMatrixhb:V 0 0 0 V 0 1 0hV:V.FstRowThdColRealCondhb':VubAbs V 1h1:(VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) * (VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) = (VAbs 0 0 V) ^ 2 + (VAbs 0 1 V) ^ 2hx:(VudAbs V) * (VudAbs V) + (VusAbs V) * (VusAbs V) 0(VAbs 2 2 V) * (VAbs 0 0 V) / ((VAbs 0 0 V) ^ 2 + (VAbs 0 1 V) ^ 2) + -((VAbs 0 2 V) * (VAbs 0 1 V) * (VAbs 1 2 V)) / ((VAbs 0 0 V) ^ 2 + (VAbs 0 1 V) ^ 2) * cexp (-((V 0 2).arg * I)) = (VAbs 0 0 V) / (VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) * ((VAbs 2 2 V) / (VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2)) - (VAbs 0 1 V) / (VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) * (VAbs 0 2 V) * ((VAbs 1 2 V) / (VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2)) * cexp (-(I * (V 0 2).arg)) V:CKMMatrixhb:V 0 0 0 V 0 1 0hV:V.FstRowThdColRealCondhb':VubAbs V 1h1:(VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) * (VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) = (VAbs 0 0 V) ^ 2 + (VAbs 0 1 V) ^ 2hx:(VudAbs V) * (VudAbs V) + (VusAbs V) * (VusAbs V) 0((VAbs 2 2 V) * (VAbs 0 0 V) + -((VAbs 0 1 V) * (VAbs 0 2 V) * (VAbs 1 2 V) * cexp (-((V 0 2).arg * I)))) / ((VAbs 0 0 V) ^ 2 + (VAbs 0 1 V) ^ 2) = ((VAbs 2 2 V) * (VAbs 0 0 V) - (VAbs 0 1 V) * (VAbs 0 2 V) * (VAbs 1 2 V) * cexp (-((V 0 2).arg * I))) / (VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) ^ 2 conv_rhs => V:CKMMatrixhb:V 0 0 0 V 0 1 0hV:V.FstRowThdColRealCondhb':VubAbs V 1h1:(VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) * (VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) = (VAbs 0 0 V) ^ 2 + (VAbs 0 1 V) ^ 2hx:(VudAbs V) * (VudAbs V) + (VusAbs V) * (VusAbs V) 0| ((VAbs 2 2 V) * (VAbs 0 0 V) - (VAbs 0 1 V) * (VAbs 0 2 V) * (VAbs 1 2 V) * cexp (-((V 0 2).arg * I))) / ((VAbs 0 0 V) ^ 2 + (VAbs 0 1 V) ^ 2) V:CKMMatrixhb:V 0 0 0 V 0 1 0hV:V.FstRowThdColRealCondhb':VubAbs V 1h1:(VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) * (VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) = (VAbs 0 0 V) ^ 2 + (VAbs 0 1 V) ^ 2hx:(VudAbs V) * (VudAbs V) + (VusAbs V) * (VusAbs V) 0((VAbs 2 2 V) * (VAbs 0 0 V) + -((VAbs 0 1 V) * (VAbs 0 2 V) * (VAbs 1 2 V) * cexp (-((V 0 2).arg * I)))) / ((VAbs 0 0 V) * (VAbs 0 0 V) + (VAbs 0 1 V) * (VAbs 0 1 V)) = ((VAbs 2 2 V) * (VAbs 0 0 V) - (VAbs 0 1 V) * (VAbs 0 2 V) * (VAbs 1 2 V) * cexp (-((V 0 2).arg * I))) / ((VAbs 0 0 V) * (VAbs 0 0 V) + (VAbs 0 1 V) * (VAbs 0 1 V)) V:CKMMatrixhb:V 0 0 0 V 0 1 0hV:V.FstRowThdColRealCondhb':VubAbs V 1h1:(VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) * (VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) = (VAbs 0 0 V) ^ 2 + (VAbs 0 1 V) ^ 2hx:(VudAbs V) * (VudAbs V) + (VusAbs V) * (VusAbs V) 0((VAbs 2 2 V) * (VAbs 0 0 V) + -((VAbs 0 1 V) * (VAbs 0 2 V) * (VAbs 1 2 V) * cexp (-((V 0 2).arg * I)))) / ((VAbs 0 0 V) ^ 2 + (VAbs 0 1 V) ^ 2) = ((VAbs 2 2 V) * (VAbs 0 0 V) - (VAbs 0 1 V) * (VAbs 0 2 V) * (VAbs 1 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.FstRowThdColRealCondhb':VubAbs V 1h1:(VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) * (VAbs 0 0 V ^ 2 + VAbs 0 1 V ^ 2) = (VAbs 0 0 V) ^ 2 + (VAbs 0 1 V) ^ 2hx:(VudAbs V) * (VudAbs V) + (VusAbs V) * (VusAbs V) 0[V]c ((fun i => i) 2, ) = [standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) (-(V 0 2).arg)]c ((fun i => i) 2, ) All goals completed! 🐙V:CKMMatrixhV:V.ubOnePhaseCondh1:VubAbs V = 10 = sin (θ₂₃ V) * 0 All goals completed! 🐙V:CKMMatrixU:CKMMatrixhU:V U U.FstRowThdColRealCondhUV:U = Vha:¬(V 0 0 0 V 0 1 0)haU:¬(U 0 0 0 U 0 1 0)U2:CKMMatrixhU2:U U2 U2.ubOnePhaseCondhUVa2:V U2hUV2:U2 = Vhx:U2 = standParam (θ₁₂ U2) (θ₁₃ U2) (θ₂₃ U2) 0V U2 All goals completed! 🐙theorem exists_for_CKMatrix (V : CKMMatrix) : (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ), V standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := V:CKMMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, V standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ V:CKMMatrixV standParam (θ₁₂ V) (θ₁₃ V) (θ₂₃ V) (δ₁₃ V) All goals completed! 🐙