From ff89c3f79dbc87371f3324752e9b4c8f7f468361 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 29 Apr 2024 08:13:52 -0400 Subject: [PATCH] refactor: Major refactor of CKMMatrix --- HepLean/FlavorPhysics/CKMMatrix/Basic.lean | 158 ++-- .../FlavorPhysics/CKMMatrix/Invariants.lean | 51 ++ HepLean/FlavorPhysics/CKMMatrix/Jarlskog.lean | 176 ---- .../FlavorPhysics/CKMMatrix/PhaseFreedom.lean | 181 +++- HepLean/FlavorPhysics/CKMMatrix/Ratios.lean | 655 --------------- .../FlavorPhysics/CKMMatrix/Relations.lean | 405 +++++++-- HepLean/FlavorPhysics/CKMMatrix/Rows.lean | 3 - .../StandardParameterization/Basic.lean | 184 ++++ .../StandardParameters.lean | 795 +++++++----------- 9 files changed, 1096 insertions(+), 1512 deletions(-) create mode 100644 HepLean/FlavorPhysics/CKMMatrix/Invariants.lean delete mode 100644 HepLean/FlavorPhysics/CKMMatrix/Jarlskog.lean delete mode 100644 HepLean/FlavorPhysics/CKMMatrix/Ratios.lean create mode 100644 HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean rename HepLean/FlavorPhysics/CKMMatrix/{ => StandardParameterization}/StandardParameters.lean (58%) diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean index 9702324..7016dcc 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean @@ -14,7 +14,7 @@ noncomputable section @[simp] def phaseShiftMatrix (a b c : ℝ) : Matrix (Fin 3) (Fin 3) ℂ := - ![![ cexp (I * a), 0, 0], ![0, cexp (I * b), 0], ![0, 0, cexp (I * c)]] + ![![cexp (I * a), 0, 0], ![0, cexp (I * b), 0], ![0, 0, cexp (I * c)]] lemma phaseShiftMatrix_one : phaseShiftMatrix 0 0 0 = 1 := by ext i j @@ -266,122 +266,58 @@ abbrev VtsAbs := VAbs 2 1 @[simp] abbrev VtbAbs := VAbs 2 2 -lemma VAbs_ge_zero (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : 0 ≤ VAbs i j V := by - obtain ⟨V, hV⟩ := Quot.exists_rep V - rw [← hV] - exact Complex.abs.nonneg _ - -lemma 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 := by - obtain ⟨V, hV⟩ := Quot.exists_rep V - subst hV - have hV := V.prop - rw [mem_unitaryGroup_iff] at hV - have ht := congrFun (congrFun hV i) i - simp [Matrix.mul_apply, Fin.sum_univ_three] at ht - rw [mul_conj, mul_conj, mul_conj] at ht - repeat rw [← Complex.sq_abs] at ht - rw [← ofReal_inj] - simpa using ht - -lemma 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 := by - obtain ⟨V, hV⟩ := Quot.exists_rep V - subst hV - have hV := V.prop - rw [mem_unitaryGroup_iff'] at hV - have ht := congrFun (congrFun hV i) i - simp [Matrix.mul_apply, Fin.sum_univ_three] at ht - rw [mul_comm, mul_conj, mul_comm, mul_conj, mul_comm, mul_conj] at ht - repeat rw [← Complex.sq_abs] at ht - rw [← ofReal_inj] - simpa using ht - - -lemma VAbs_leq_one (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : VAbs i j V ≤ 1 := by - have h := VAbs_sum_sq_row_eq_one V i - fin_cases j - change VAbs i 0 V ≤ 1 - nlinarith - change VAbs i 1 V ≤ 1 - nlinarith - change VAbs i 2 V ≤ 1 - nlinarith - - -lemma VAbs_thd_eq_one_fst_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} (hV : VAbs i 2 V = 1) : - VAbs i 0 V = 0 := by - have h := VAbs_sum_sq_row_eq_one V i - rw [hV] at h - simp at h - nlinarith - -lemma VAbs_thd_eq_one_snd_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} (hV : VAbs i 2 V = 1) : - VAbs i 1 V = 0 := by - have h := VAbs_sum_sq_row_eq_one V i - rw [hV] at h - simp at h - nlinarith - -lemma 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 := by - have h := VAbs_sum_sq_col_eq_one V i - rw [hV] at h - simp at h - nlinarith - -lemma 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 := by - have h := VAbs_sum_sq_col_eq_one V i - rw [hV] at h - simp at h - nlinarith - -lemma VAbs_thd_neq_one_fst_snd_sq_neq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} - (hV : VAbs i 2 V ≠ 1) : (VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2) ≠ 0 := by - have h1 : 1 - VAbs i 2 V ^ 2 = VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 := by - linear_combination - (VAbs_sum_sq_row_eq_one V i) - rw [← h1] - by_contra h - have h2 : VAbs i 2 V ^2 = 1 := by - nlinarith - simp only [Fin.isValue, sq_eq_one_iff] at h2 - have h3 : 0 ≤ VAbs i 2 V := VAbs_ge_zero i 2 V - have h4 : VAbs i 2 V = 1 := by - nlinarith - exact hV h4 - -lemma VAbs_thd_neq_one_sqrt_fst_snd_sq_neq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} - (hV : VAbs i 2 V ≠ 1) : √(VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2) ≠ 0 := by - rw [Real.sqrt_ne_zero (Left.add_nonneg (sq_nonneg (VAbs i 0 V)) (sq_nonneg (VAbs i 1 V)))] - exact VAbs_thd_neq_one_fst_snd_sq_neq_zero hV - -lemma VcbAbs_sq_add_VtbAbs_sq (V : Quotient CKMMatrixSetoid) : - VcbAbs V ^ 2 + VtbAbs V ^ 2 = 1 - VubAbs V ^2 := by - linear_combination (VAbs_sum_sq_col_eq_one V 2) - -lemma VudAbs_sq_add_VusAbs_sq : VudAbs V ^ 2 + VusAbs V ^2 = 1 - VubAbs V ^2 := by - linear_combination (VAbs_sum_sq_row_eq_one V 0) namespace CKMMatrix open ComplexConjugate -lemma fst_row_snd_row (V : CKMMatrix) : V.1 1 0 * conj (V.1 0 0) + V.1 1 1 * conj (V.1 0 1) - + V.1 1 2 * conj (V.1 0 2) = 0 := by - have hV := V.prop - rw [mem_unitaryGroup_iff] at hV - have ht := congrFun (congrFun hV 1) 0 - simp [Matrix.mul_apply, Fin.sum_univ_three] at ht - exact ht + +section ratios + +-- A +def Rubud (V : CKMMatrix) : ℂ := [V]ub / [V]ud + +scoped[CKMMatrix] notation (name := ub_ud_ratio) "[" V "]ub|ud" => Rubud V +-- B +def Rusud (V : CKMMatrix) : ℂ := [V]us / [V]ud + +scoped[CKMMatrix] notation (name := us_ud_ratio) "[" V "]us|ud" => Rusud V + +def Rudus (V : CKMMatrix) : ℂ := [V]ud / [V]us + +scoped[CKMMatrix] notation (name := ud_us_ratio) "[" V "]ud|us" => Rudus V + +def Rubus (V : CKMMatrix) : ℂ := [V]ub / [V]us + +scoped[CKMMatrix] notation (name := ub_us_ratio) "[" V "]ub|us" => Rubus V +-- D +def Rcdcb (V : CKMMatrix) : ℂ := [V]cd / [V]cb + +scoped[CKMMatrix] notation (name := cd_cb_ratio) "[" V "]cd|cb" => Rcdcb V + +lemma Rcdcb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cd = Rcdcb V * [V]cb := by + rw [Rcdcb] + exact (div_mul_cancel₀ (V.1 1 0) h).symm + +-- C' +def Rcscb (V : CKMMatrix) : ℂ := [V]cs / [V]cb + +scoped[CKMMatrix] notation (name := cs_cb_ratio) "[" V "]cs|cb" => Rcscb V + +lemma Rcscb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cs = Rcscb V * [V]cb := by + rw [Rcscb] + exact (div_mul_cancel₀ [V]cs h).symm -lemma fst_row_thd_row (V : CKMMatrix) : V.1 2 0 * conj (V.1 0 0) + V.1 2 1 * conj (V.1 0 1) - + V.1 2 2 * conj (V.1 0 2) = 0 := by - have hV := V.prop - rw [mem_unitaryGroup_iff] at hV - have ht := congrFun (congrFun hV 2) 0 - simp [Matrix.mul_apply, Fin.sum_univ_three] at ht - exact ht +def Rtb!cbud (V : CKMMatrix) : ℂ := conj [V]tb / ([V]cb * [V]ud) + +scoped[CKMMatrix] notation (name := tb_cb_ud_ratio) "[" V "]tb*|cb|ud" => Rtb!cbud V + +def Rtb!cbus (V : CKMMatrix) : ℂ := conj [V]tb / ([V]cb * [V]us) + +scoped[CKMMatrix] notation (name := tb_cb_us_ratio) "[" V "]tb*|cb|us" => Rtb!cbus V + + +end ratios end CKMMatrix diff --git a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean new file mode 100644 index 0000000..0c2f26d --- /dev/null +++ b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.FlavorPhysics.CKMMatrix.Basic +import HepLean.FlavorPhysics.CKMMatrix.Rows +import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom +import Mathlib.Analysis.SpecialFunctions.Complex.Arg + +open Matrix Complex +open ComplexConjugate +open CKMMatrix + + +noncomputable section +namespace Invariant + + +@[simps!] +def jarlskogℂCKM (V : CKMMatrix) : ℂ := + [V]us * [V]cb * conj [V]ub * conj [V]cs + +lemma jarlskogℂCKM_equiv (V U : CKMMatrix) (h : V ≈ U) : + jarlskogℂCKM V = jarlskogℂCKM U := by + obtain ⟨a, b, c, e, f, g, h⟩ := h + change V = phaseShiftApply U a b c e f g at h + rw [h] + simp only [jarlskogℂCKM, Fin.isValue, phaseShiftApply.ub, + phaseShiftApply.us, phaseShiftApply.cb, phaseShiftApply.cs] + simp [← exp_conj, conj_ofReal, exp_add, exp_neg] + have ha : cexp (↑a * I) ≠ 0 := exp_ne_zero _ + have hb : cexp (↑b * I) ≠ 0 := exp_ne_zero _ + have hf : cexp (↑f * I) ≠ 0 := exp_ne_zero _ + have hg : cexp (↑g * I) ≠ 0 := exp_ne_zero _ + field_simp + ring + +@[simp] +def jarlskogℂ : Quotient CKMMatrixSetoid → ℂ := + Quotient.lift jarlskogℂCKM jarlskogℂCKM_equiv + +def VusVubVcdSq (V : Quotient CKMMatrixSetoid) : ℝ := + VusAbs V ^ 2 * VubAbs V ^ 2 * VcbAbs V ^2 / (VudAbs V ^ 2 + VusAbs V ^2) + +def mulExpδ₃ (V : Quotient CKMMatrixSetoid) : ℂ := + jarlskogℂ V + VusVubVcdSq V + + +end Invariant +end diff --git a/HepLean/FlavorPhysics/CKMMatrix/Jarlskog.lean b/HepLean/FlavorPhysics/CKMMatrix/Jarlskog.lean deleted file mode 100644 index bdf9fd6..0000000 --- a/HepLean/FlavorPhysics/CKMMatrix/Jarlskog.lean +++ /dev/null @@ -1,176 +0,0 @@ -/- -Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. -Released under Apache 2.0 license. -Authors: Joseph Tooby-Smith --/ -import HepLean.FlavorPhysics.CKMMatrix.Basic -import HepLean.FlavorPhysics.CKMMatrix.Rows -import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom -import HepLean.FlavorPhysics.CKMMatrix.Ratios -import HepLean.FlavorPhysics.CKMMatrix.StandardParameters -import Mathlib.Analysis.SpecialFunctions.Complex.Arg - -open Matrix Complex -open ComplexConjugate -open CKMMatrix - - -noncomputable section - -@[simps!] -def jarlskogComplexCKM (V : CKMMatrix) : ℂ := - [V]us * [V]cb * conj [V]ub * conj [V]cs - -lemma jarlskogComplexCKM_equiv (V U : CKMMatrix) (h : V ≈ U) : - jarlskogComplexCKM V = jarlskogComplexCKM U := by - obtain ⟨a, b, c, e, f, g, h⟩ := h - change V = phaseShiftApply U a b c e f g at h - rw [h] - simp only [jarlskogComplexCKM, Fin.isValue, phaseShiftApply.ub, - phaseShiftApply.us, phaseShiftApply.cb, phaseShiftApply.cs] - simp [← exp_conj, conj_ofReal, exp_add, exp_neg] - have ha : cexp (↑a * I) ≠ 0 := exp_ne_zero _ - have hb : cexp (↑b * I) ≠ 0 := exp_ne_zero _ - have hf : cexp (↑f * I) ≠ 0 := exp_ne_zero _ - have hg : cexp (↑g * I) ≠ 0 := exp_ne_zero _ - field_simp - ring - -def inv₁ (V : Quotient CKMMatrixSetoid) : ℝ := - VusAbs V ^ 2 * VubAbs V ^ 2 * VcbAbs V ^2 /(VudAbs V ^ 2 + VusAbs V ^2) - -lemma inv₁_sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂) - (h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) : - inv₁ ⟦sP θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ = - Real.sin θ₁₂ ^ 2 * Real.cos θ₁₃ ^ 2 * Real.sin θ₁₃ ^ 2 * Real.sin θ₂₃ ^ 2 := by - simp only [inv₁, VusAbs, VAbs, VAbs', Fin.isValue, sP, standardParameterizationAsMatrix, - neg_mul, Quotient.lift_mk, cons_val', cons_val_one, head_cons, - empty_val', cons_val_fin_one, cons_val_zero, _root_.map_mul, VubAbs, cons_val_two, tail_cons, - VcbAbs, VudAbs, Complex.abs_ofReal] - by_cases hx : Real.cos θ₁₃ ≠ 0 - · - rw [Complex.abs_exp] - simp - rw [_root_.abs_of_nonneg h1, _root_.abs_of_nonneg h3, _root_.abs_of_nonneg h2, - _root_.abs_of_nonneg h4] - simp [sq] - ring_nf - nth_rewrite 2 [Real.sin_sq θ₁₂] - ring_nf - field_simp - ring - · simp at hx - rw [hx] - simp - - - -@[simp] -def jarlskogComplex : Quotient CKMMatrixSetoid → ℂ := - Quotient.lift jarlskogComplexCKM jarlskogComplexCKM_equiv - --- bad name -def expδ₁₃ (V : Quotient CKMMatrixSetoid) : ℂ := - jarlskogComplex V + inv₁ V - -lemma expδ₁₃_sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂) - (h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) : - expδ₁₃ ⟦sP θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ = - sin θ₁₂ * cos θ₁₃ ^ 2 * sin θ₂₃ * sin θ₁₃ * cos θ₁₂ * cos θ₂₃ * cexp (I * δ₁₃) := by - rw [expδ₁₃] - rw [inv₁_sP _ _ _ _ h1 h2 h3 h4 ] - simp only [expδ₁₃, jarlskogComplex, sP, standardParameterizationAsMatrix, neg_mul, - Quotient.lift_mk, jarlskogComplexCKM, Fin.isValue, cons_val', cons_val_one, head_cons, - empty_val', cons_val_fin_one, cons_val_zero, cons_val_two, tail_cons, _root_.map_mul, ← - exp_conj, map_neg, conj_I, conj_ofReal, neg_neg, map_sub] - simp - ring_nf - rw [exp_neg] - have h1 : cexp (I * δ₁₃) ≠ 0 := exp_ne_zero _ - field_simp - - -lemma expδ₁₃_sP_V (V : CKMMatrix) (δ₁₃ : ℝ) : - expδ₁₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = - sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧) - * cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) * cexp (I * δ₁₃) := by - refine expδ₁₃_sP _ _ _ _ ?_ ?_ ?_ ?_ - rw [S₁₂_eq_sin_θ₁₂] - exact S₁₂_nonneg _ - exact Real.cos_arcsin_nonneg _ - rw [S₂₃_eq_sin_θ₂₃] - exact S₂₃_nonneg _ - exact Real.cos_arcsin_nonneg _ - - -lemma expδ₁₃_eq_zero (V : CKMMatrix) (δ₁₃ : ℝ) : - expδ₁₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = 0 ↔ - VudAbs ⟦V⟧ = 0 ∨ VubAbs ⟦V⟧ = 0 ∨ VusAbs ⟦V⟧ = 0 ∨ VcbAbs ⟦V⟧ = 0 ∨ VtbAbs ⟦V⟧ = 0 := by - rw [VudAbs_eq_C₁₂_mul_C₁₃, VubAbs_eq_S₁₃, VusAbs_eq_S₁₂_mul_C₁₃, VcbAbs_eq_S₂₃_mul_C₁₃, VtbAbs_eq_C₂₃_mul_C₁₃, - ← ofReal_inj, - ← ofReal_inj, ← ofReal_inj, ← ofReal_inj, ← ofReal_inj] - simp only [ofReal_mul] - rw [← S₁₃_eq_ℂsin_θ₁₃, ← S₁₂_eq_ℂsin_θ₁₂, ← S₂₃_eq_ℂsin_θ₂₃, - ← C₁₃_eq_ℂcos_θ₁₃, ← C₂₃_eq_ℂcos_θ₂₃,← C₁₂_eq_ℂcos_θ₁₂] - simp - rw [expδ₁₃_sP_V] - simp - have h1 := exp_ne_zero (I * δ₁₃) - simp_all - aesop - -lemma inv₂_V_arg (V : CKMMatrix) (δ₁₃ : ℝ) - (h1 : expδ₁₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ ≠ 0 ) : - cexp (arg (expδ₁₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) * I) = - cexp (δ₁₃ * I) := by - have h1a := expδ₁₃_sP_V V δ₁₃ - have habs : Complex.abs (expδ₁₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) = - sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧) - * cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) := by - rw [h1a] - simp [abs_exp] - rw [complexAbs_sin_θ₁₃, complexAbs_cos_θ₁₃, complexAbs_sin_θ₁₂, complexAbs_cos_θ₁₂, - complexAbs_sin_θ₂₃, complexAbs_cos_θ₂₃] - have h2 : expδ₁₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = - Complex.abs (expδ₁₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) * exp (δ₁₃ * I) := by - rw [habs, h1a] - ring_nf - nth_rewrite 1 [← abs_mul_exp_arg_mul_I (expδ₁₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ )] at h2 - have habs_neq_zero : (Complex.abs (expδ₁₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) : ℂ) ≠ 0 := by - simp - exact h1 - rw [← mul_right_inj' habs_neq_zero] - rw [← h2] - -def δ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := arg (expδ₁₃ V) - -theorem eq_standardParameterization_δ₃ (V : CKMMatrix) : - V ≈ sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (δ₁₃ ⟦V⟧) := by - obtain ⟨δ₁₃', hδ₃⟩ := exists_standardParameterization V - have hSV := (Quotient.eq.mpr (hδ₃)) - by_cases h : expδ₁₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃'⟧ ≠ 0 - have h1 := inv₂_V_arg V δ₁₃' h - have h2 := eq_phases_sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃' - (δ₁₃ ⟦V⟧) (by rw [← h1, ← hSV, δ₁₃]) - rw [h2] at hδ₃ - exact hδ₃ - simp at h - have h1 : δ₁₃ ⟦V⟧ = 0 := by - rw [hSV, δ₁₃, h] - simp - rw [h1] - rw [expδ₁₃_eq_zero, Vs_zero_iff_cos_sin_zero] at h - cases' h with h h - exact phaseShiftEquivRelation.trans hδ₃ (sP_cos_θ₁₂_eq_zero δ₁₃' h ) - cases' h with h h - exact phaseShiftEquivRelation.trans hδ₃ (sP_cos_θ₁₃_eq_zero δ₁₃' h ) - cases' h with h h - exact phaseShiftEquivRelation.trans hδ₃ (sP_cos_θ₂₃_eq_zero δ₁₃' h ) - cases' h with h h - exact phaseShiftEquivRelation.trans hδ₃ (sP_sin_θ₁₂_eq_zero δ₁₃' h ) - cases' h with h h - exact phaseShiftEquivRelation.trans hδ₃ (sP_sin_θ₁₃_eq_zero δ₁₃' h ) - exact phaseShiftEquivRelation.trans hδ₃ (sP_sin_θ₂₃_eq_zero δ₁₃' h ) - - -end diff --git a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean index a3cf21a..0a5136b 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean @@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith -/ import HepLean.FlavorPhysics.CKMMatrix.Basic import HepLean.FlavorPhysics.CKMMatrix.Rows +import HepLean.FlavorPhysics.CKMMatrix.Relations import Mathlib.Analysis.SpecialFunctions.Complex.Arg import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic @@ -14,86 +15,88 @@ open Matrix Complex noncomputable section namespace CKMMatrix open ComplexConjugate -variable (a b c d e f : ℝ) -lemma ud_eq_abs (V : CKMMatrix) (h1 : a + d = - arg [V]ud) : - [phaseShiftApply V a b c d e f]ud = VudAbs ⟦V⟧ := by +section phaseShiftApply +variable (u c t d s b : ℝ) + +lemma ud_eq_abs (V : CKMMatrix) (h1 : u + d = - arg [V]ud) : + [phaseShiftApply V u c t d s b]ud = VudAbs ⟦V⟧ := by rw [phaseShiftApply.ud] rw [← abs_mul_exp_arg_mul_I [V]ud] rw [mul_comm, mul_assoc, ← exp_add] - have h2 : ↑(arg (V.1 0 0)) * I + (↑a * I + ↑d * I) = ↑(arg (V.1 0 0) + (a + d)) * I := by + have h2 : ↑(arg (V.1 0 0)) * I + (↑u * I + ↑d * I) = ↑(arg (V.1 0 0) + (u + d)) * I := by simp [add_assoc] ring rw [h2, h1] simp rfl -lemma us_eq_abs {V : CKMMatrix} (h1 : a + e = - arg [V]us) : - [phaseShiftApply V a b c d e f]us = VusAbs ⟦V⟧ := by +lemma us_eq_abs {V : CKMMatrix} (h1 : u + s = - arg [V]us) : + [phaseShiftApply V u c t d s b]us = VusAbs ⟦V⟧ := by rw [phaseShiftApply.us] rw [← abs_mul_exp_arg_mul_I [V]us] rw [mul_comm, mul_assoc, ← exp_add] - have h2 : ↑(arg [V]us) * I + (↑a * I + ↑e * I) = ↑(arg [V]us + (a + e)) * I := by + have h2 : ↑(arg [V]us) * I + (↑u * I + ↑s * I) = ↑(arg [V]us + (u + s)) * I := by simp [add_assoc] ring rw [h2, h1] simp rfl -lemma ub_eq_abs {V : CKMMatrix} (h1 : a + f = - arg [V]ub) : - [phaseShiftApply V a b c d e f]ub = VubAbs ⟦V⟧ := by +lemma ub_eq_abs {V : CKMMatrix} (h1 : u + b = - arg [V]ub) : + [phaseShiftApply V u c t d s b]ub = VubAbs ⟦V⟧ := by rw [phaseShiftApply.ub] rw [← abs_mul_exp_arg_mul_I [V]ub] rw [mul_comm, mul_assoc, ← exp_add] - have h2 : ↑(arg [V]ub) * I + (↑a * I + ↑f * I) = ↑(arg [V]ub + (a + f)) * I := by + have h2 : ↑(arg [V]ub) * I + (↑u * I + ↑b * I) = ↑(arg [V]ub + (u + b)) * I := by simp [add_assoc] ring rw [h2, h1] simp rfl -lemma cs_eq_abs {V : CKMMatrix} (h1 : b + e = - arg [V]cs) : - [phaseShiftApply V a b c d e f]cs = VcsAbs ⟦V⟧ := by +lemma cs_eq_abs {V : CKMMatrix} (h1 : c + s = - arg [V]cs) : + [phaseShiftApply V u c t d s b]cs = VcsAbs ⟦V⟧ := by rw [phaseShiftApply.cs] rw [← abs_mul_exp_arg_mul_I [V]cs] rw [mul_comm, mul_assoc, ← exp_add] - have h2 : ↑(arg [V]cs) * I + (↑b * I + ↑e * I) = ↑(arg [V]cs + (b + e)) * I := by + have h2 : ↑(arg [V]cs) * I + (↑c * I + ↑s * I) = ↑(arg [V]cs + (c + s)) * I := by simp [add_assoc] ring rw [h2, h1] simp rfl -lemma cb_eq_abs {V : CKMMatrix} (h1 : b + f = - arg [V]cb) : - [phaseShiftApply V a b c d e f]cb = VcbAbs ⟦V⟧ := by +lemma cb_eq_abs {V : CKMMatrix} (h1 : c + b = - arg [V]cb) : + [phaseShiftApply V u c t d s b]cb = VcbAbs ⟦V⟧ := by rw [phaseShiftApply.cb] rw [← abs_mul_exp_arg_mul_I [V]cb] rw [mul_comm, mul_assoc, ← exp_add] - have h2 : ↑(arg [V]cb) * I + (↑b * I + ↑f * I) = ↑(arg [V]cb + (b + f)) * I := by + have h2 : ↑(arg [V]cb) * I + (↑c * I + ↑b * I) = ↑(arg [V]cb + (c + b)) * I := by simp [add_assoc] ring rw [h2, h1] simp rfl -lemma tb_eq_abs {V : CKMMatrix} (h1 : c + f = - arg [V]tb) : - [phaseShiftApply V a b c d e f]tb = VtbAbs ⟦V⟧ := by +lemma tb_eq_abs {V : CKMMatrix} (h1 : t + b = - arg [V]tb) : + [phaseShiftApply V u c t d s b]tb = VtbAbs ⟦V⟧ := by rw [phaseShiftApply.tb] rw [← abs_mul_exp_arg_mul_I [V]tb] rw [mul_comm, mul_assoc, ← exp_add] - have h2 : ↑(arg [V]tb) * I + (↑c * I + ↑f * I) = ↑(arg [V]tb + (c + f)) * I := by + have h2 : ↑(arg [V]tb) * I + (↑t * I + ↑b * I) = ↑(arg [V]tb + (t + b)) * I := by simp [add_assoc] ring rw [h2, h1] simp rfl -lemma cd_eq_neg_abs {V : CKMMatrix} (h1 : b + d = Real.pi - arg [V]cd) : - [phaseShiftApply V a b c d e f]cd = - VcdAbs ⟦V⟧ := by +lemma cd_eq_neg_abs {V : CKMMatrix} (h1 : c + d = Real.pi - arg [V]cd) : + [phaseShiftApply V u c t d s b]cd = - VcdAbs ⟦V⟧ := by rw [phaseShiftApply.cd] rw [← abs_mul_exp_arg_mul_I [V]cd] rw [mul_comm, mul_assoc, ← exp_add] - have h2 : ↑(arg [V]cd) * I + (↑b * I + ↑d * I) = ↑(arg [V]cd + (b + d)) * I := by + have h2 : ↑(arg [V]cd) * I + (↑c * I + ↑d * I) = ↑(arg [V]cd + (c + d)) * I := by simp [add_assoc] ring rw [h2, h1] @@ -101,9 +104,9 @@ lemma cd_eq_neg_abs {V : CKMMatrix} (h1 : b + d = Real.pi - arg [V]cd) : rfl lemma t_eq_conj {V : CKMMatrix} {τ : ℝ} (hτ : cexp (τ * I) • (conj [V]u ×₃ conj [V]c) = [V]t) - (h1 : τ = - a - b - c - d - e - f) : - [phaseShiftApply V a b c d e f]t = - conj [phaseShiftApply V a b c d e f]u ×₃ conj [phaseShiftApply V a b c d e f]c := by + (h1 : τ = - u - c - t - d - s - b) : + [phaseShiftApply V u c t d s b]t = + conj [phaseShiftApply V u c t d s b]u ×₃ conj [phaseShiftApply V u c t d s b]c := by change _ = phaseShiftApply.ucCross _ _ _ _ _ _ _ funext i fin_cases i @@ -138,6 +141,19 @@ lemma t_eq_conj {V : CKMMatrix} {τ : ℝ} (hτ : cexp (τ * I) • (conj [V]u simp ring +end phaseShiftApply + +variable (a b c d e f : ℝ) + +-- rename +def UCond₁ (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 + +-- rename +def UCond₃ (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) + -- bad name for this lemma lemma all_cond_sol {V : CKMMatrix} (h1 : a + d = - arg [V]ud) (h2 : a + e = - arg [V]us) (h3 : b + f = - arg [V]cb) (h4 : c + f = - arg [V]tb) (h5 : τ = - a - b - c - d - e - f) : @@ -168,10 +184,28 @@ lemma all_cond_sol {V : CKMMatrix} (h1 : a + d = - arg [V]ud) (h2 : a + e = - a ring_nf simp --- rename -def UCond₁ (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 +lemma UCond₃_solv {V : CKMMatrix} (h1 : a + f = - arg [V]ub) (h2 : 0 = - a - b - c - d - e - f) + (h3 : b + d = Real.pi - arg [V]cd) (h5 : b + e = - arg [V]cs) : + c = - Real.pi + arg [V]cd + arg [V]cs + arg [V]ub + b ∧ + d = Real.pi - arg [V]cd - b ∧ + e = - arg [V]cs - b ∧ + f = - arg [V]ub - a := by + have hf : f = - arg [V]ub - a := by + linear_combination h1 + subst hf + have he : e = - arg [V]cs - b := by + linear_combination h5 + have hd : d = Real.pi - arg [V]cd - b := by + linear_combination h3 + subst he hd + simp_all + ring_nf at h2 + have hc : c = - Real.pi + arg [V]cd + arg [V]cs + arg [V]ub + b := by + linear_combination h2 + subst hc + ring +-- rename lemma all_eq_abs (V : CKMMatrix) : ∃ (U : CKMMatrix), V ≈ U ∧ UCond₁ U:= by obtain ⟨τ, hτ⟩ := V.uRow_cross_cRow_eq_tRow @@ -209,9 +243,100 @@ lemma all_eq_abs (V : CKMMatrix) : ring +lemma UCond₃_exists {V : CKMMatrix} (hb :¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) (hV : UCond₁ V) : + ∃ (U : CKMMatrix), V ≈ U ∧ UCond₃ U:= by + let U : CKMMatrix := phaseShiftApply V 0 0 (- Real.pi + arg [V]cd + arg [V]cs + arg [V]ub) + (Real.pi - arg [V]cd ) (- arg [V]cs) (- arg [V]ub ) + use U + have hUV : ⟦U⟧ = ⟦V⟧ := by + simp + symm + exact phaseShiftApply.equiv _ _ _ _ _ _ _ + apply And.intro + exact phaseShiftApply.equiv _ _ _ _ _ _ _ + apply And.intro + · simp [not_or] at hb + have h1 : VudAbs ⟦U⟧ = 0 := by + rw [hUV] + simp [VAbs, hb] + simp [VAbs] at h1 + exact h1 + apply And.intro + · simp [not_or] at hb + have h1 : VusAbs ⟦U⟧ = 0 := by + rw [hUV] + simp [VAbs, hb] + simp [VAbs] at h1 + exact h1 + apply And.intro + · simp [not_or] at hb + have h3 := cb_eq_zero_of_ud_us_zero hb + have h1 : VcbAbs ⟦U⟧ = 0 := by + rw [hUV] + simp [VAbs, h3] + simp [VAbs] at h1 + exact h1 + apply And.intro + · have hU1 : [U]ub = VubAbs ⟦V⟧ := by + apply ub_eq_abs _ _ _ _ _ _ _ + ring + rw [hU1] + have h1:= (ud_us_neq_zero_iff_ub_neq_one V).mpr.mt hb + simpa using h1 + apply And.intro + · have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by + simp + exact hV.2.2.2.2 + apply t_eq_conj _ _ _ _ _ _ hτ.symm + ring + apply And.intro + · rw [hUV] + apply cd_eq_neg_abs _ _ _ _ _ _ _ + ring + have hcs : [U]cs = VcsAbs ⟦U⟧ := by + rw [hUV] + apply cs_eq_abs _ _ _ _ _ _ _ + ring + rw [hcs, hUV, cs_of_ud_us_zero hb] +lemma cd_of_us_or_ud_neq_zero_UCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) + (hV : UCond₁ V) : [V]cd = (- VtbAbs ⟦V⟧ * VusAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) + + (- VubAbs ⟦V⟧ * VudAbs ⟦V⟧ * VcbAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2 )) * cexp (- arg [V]ub * I) + := by + have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by + simp + exact hV.2.2.2.2 + rw [cd_of_ud_us_ub_cb_tb hb hτ] + rw [hV.1, hV.2.1, hV.2.2.1, hV.2.2.2.1] + simp [sq, conj_ofReal] + have hx := Vabs_sq_add_neq_zero hb + field_simp + have h1 : conj [V]ub = VubAbs ⟦V⟧ * cexp (- arg [V]ub * I) := by + nth_rewrite 1 [← abs_mul_exp_arg_mul_I [V]ub] + rw [@RingHom.map_mul] + simp [conj_ofReal, ← exp_conj, VAbs] + rw [h1] + ring_nf +lemma cs_of_us_or_ud_neq_zero_UCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) + (hV : UCond₁ V) : [V]cs = (VtbAbs ⟦V⟧ * VudAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) + + (- VubAbs ⟦V⟧ * VusAbs ⟦V⟧ * VcbAbs ⟦V⟧/ (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) * cexp (- arg [V]ub * I) + := by + have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by + simp + exact hV.2.2.2.2 + rw [cs_of_ud_us_ub_cb_tb hb hτ] + rw [hV.1, hV.2.1, hV.2.2.1, hV.2.2.2.1] + simp [sq, conj_ofReal] + have hx := Vabs_sq_add_neq_zero hb + field_simp + have h1 : conj [V]ub = VubAbs ⟦V⟧ * cexp (- arg [V]ub * I) := by + nth_rewrite 1 [← abs_mul_exp_arg_mul_I [V]ub] + rw [@RingHom.map_mul] + simp [conj_ofReal, ← exp_conj, VAbs] + rw [h1] + ring_nf end CKMMatrix end diff --git a/HepLean/FlavorPhysics/CKMMatrix/Ratios.lean b/HepLean/FlavorPhysics/CKMMatrix/Ratios.lean deleted file mode 100644 index 0d1bba7..0000000 --- a/HepLean/FlavorPhysics/CKMMatrix/Ratios.lean +++ /dev/null @@ -1,655 +0,0 @@ -/- -Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. -Released under Apache 2.0 license. -Authors: Joseph Tooby-Smith --/ -import HepLean.FlavorPhysics.CKMMatrix.Basic -import HepLean.FlavorPhysics.CKMMatrix.Rows -import HepLean.FlavorPhysics.CKMMatrix.Relations -import Mathlib.Analysis.SpecialFunctions.Complex.Arg -import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom - -open Matrix Complex - - -noncomputable section - -namespace CKMMatrix -open ComplexConjugate - --- A -def Rubud (V : CKMMatrix) : ℂ := [V]ub / [V]ud - -scoped[CKMMatrix] notation (name := ub_ud_ratio) "[" V "]ub|ud" => Rubud V --- B -def Rusud (V : CKMMatrix) : ℂ := [V]us / [V]ud - -scoped[CKMMatrix] notation (name := us_ud_ratio) "[" V "]us|ud" => Rusud V - -def Rudus (V : CKMMatrix) : ℂ := [V]ud / [V]us - -scoped[CKMMatrix] notation (name := ud_us_ratio) "[" V "]ud|us" => Rudus V - -def Rubus (V : CKMMatrix) : ℂ := [V]ub / [V]us - -scoped[CKMMatrix] notation (name := ub_us_ratio) "[" V "]ub|us" => Rubus V --- D -def Rcdcb (V : CKMMatrix) : ℂ := [V]cd / [V]cb - -scoped[CKMMatrix] notation (name := cd_cb_ratio) "[" V "]cd|cb" => Rcdcb V - -lemma Rcdcb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cd = Rcdcb V * [V]cb := by - rw [Rcdcb] - exact (div_mul_cancel₀ (V.1 1 0) h).symm - --- C' -def Rcscb (V : CKMMatrix) : ℂ := [V]cs / [V]cb - -scoped[CKMMatrix] notation (name := cs_cb_ratio) "[" V "]cs|cb" => Rcscb V - -lemma Rcscb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cs = Rcscb V * [V]cb := by - rw [Rcscb] - exact (div_mul_cancel₀ [V]cs h).symm - - -def Rtb!cbud (V : CKMMatrix) : ℂ := conj [V]tb / ([V]cb * [V]ud) - -scoped[CKMMatrix] notation (name := tb_cb_ud_ratio) "[" V "]tb*|cb|ud" => Rtb!cbud V - -def Rtb!cbus (V : CKMMatrix) : ℂ := conj [V]tb / ([V]cb * [V]us) - -scoped[CKMMatrix] notation (name := tb_cb_us_ratio) "[" V "]tb*|cb|us" => Rtb!cbus V - -lemma orthog_fst_snd_row_ratios {V : CKMMatrix} (hb : [V]ud ≠ 0) (ha : [V]cb ≠ 0) : - [V]cd|cb + [V]cs|cb * conj ([V]us|ud) + conj ([V]ub|ud) = 0 := by - have h1 : ([V]cd * conj ([V]ud) + [V]cs * conj ([V]us) - + [V]cb * conj ([V]ub)) / ([V]cb * conj ([V]ud)) = 0 := by - rw [fst_row_snd_row V ] - simp only [Fin.isValue, zero_div] - rw [← div_add_div_same, ← div_add_div_same] at h1 - rw [mul_div_mul_comm, mul_div_mul_comm, mul_div_mul_comm] at h1 - rw [div_self, div_self] at h1 - change Rcdcb V * 1 + _ + _ = _ at h1 - have h2 : (starRingEnd ℂ) (V.1 0 2) / (starRingEnd ℂ) (V.1 0 0) = conj (Rubud V) := by - simp [Rubud] - have h3 : ((starRingEnd ℂ) (V.1 0 1) / (starRingEnd ℂ) (V.1 0 0)) = conj (Rusud V) := by - simp [Rusud] - rw [h2, h3] at h1 - simp at h1 - exact h1 - exact ha - simpa using hb - -lemma orthog_fst_snd_row_ratios_cb_us {V : CKMMatrix} (hb : [V]us ≠ 0) (ha : [V]cb ≠ 0) : - [V]cd|cb * conj ([V]ud|us) + [V]cs|cb + conj ([V]ub|us) = 0 := by - have h1 : ([V]cd * conj ([V]ud) + [V]cs * conj ([V]us) - + [V]cb * conj ([V]ub)) / ([V]cb * conj ([V]us)) = 0 := by - rw [fst_row_snd_row V ] - simp only [Fin.isValue, zero_div] - rw [← div_add_div_same, ← div_add_div_same] at h1 - rw [mul_div_mul_comm, mul_div_mul_comm, mul_div_mul_comm] at h1 - rw [div_self, div_self] at h1 - change _ + _ * 1 + _ = _ at h1 - have h2 : (starRingEnd ℂ) (V.1 0 2) / (starRingEnd ℂ) (V.1 0 1) = conj (Rubus V) := by - simp [Rubus] - have h3 : ((starRingEnd ℂ) (V.1 0 0) / (starRingEnd ℂ) (V.1 0 1)) = conj (Rudus V) := by - simp [Rudus] - rw [h2, h3] at h1 - simp at h1 - exact h1 - exact ha - simpa using hb - -def R' (V : CKMMatrix) : ℂ := [V]cs|cb * (1 + normSq [V]us|ud) + conj ([V]ub|ud) * [V]us|ud - -def R's (V : CKMMatrix) : ℂ := [V]cd|cb * (normSq [V]ud|us + 1) + conj ([V]ub|us) * [V]ud|us - -lemma R'_eq (V : CKMMatrix) : - R' V = [V]cs|cb * (1 + normSq ([V]us|ud)) + conj ([V]ub|ud) * [V]us|ud := by rfl - -lemma R's_eq (V : CKMMatrix) : - R's V = [V]cd|cb * (normSq ([V]ud|us) + 1) + conj ([V]ub|us) * [V]ud|us := by rfl - -lemma one_plus_normSq_Rusud_neq_zero_ℝ (V : CKMMatrix): - 1 + normSq ([V]us|ud) ≠ 0 := by - have h1 : 0 ≤ (normSq ([V]us|ud)) := normSq_nonneg ([V]us|ud) - have h2 : 0 < 1 + normSq ([V]us|ud) := by linarith - by_contra hn - have h3 := lt_of_lt_of_eq h2 hn - simp at h3 - -lemma normSq_Rudus_plus_one_neq_zero_ℝ (V : CKMMatrix): - normSq ([V]ud|us) + 1 ≠ 0 := by - have h1 : 0 ≤ (normSq ([V]ud|us)) := normSq_nonneg ([V]ud|us) - have h2 : 0 < normSq ([V]ud|us) + 1 := by linarith - by_contra hn - have h3 := lt_of_lt_of_eq h2 hn - simp at h3 - -lemma one_plus_normSq_Rusud_neq_zero_ℂ (V : CKMMatrix): - 1 + (normSq ([V]us|ud) : ℂ) ≠ 0 := by - by_contra hn - have h1 := one_plus_normSq_Rusud_neq_zero_ℝ V - simp at h1 - rw [← ofReal_inj] at h1 - simp_all only [ofReal_add, ofReal_one, ofReal_zero, not_true_eq_false] - -lemma normSq_Rudus_plus_one_neq_zero_ℂ (V : CKMMatrix): - (normSq ([V]ud|us) : ℂ) + 1 ≠ 0 := by - by_contra hn - have h1 := normSq_Rudus_plus_one_neq_zero_ℝ V - simp at h1 - rw [← ofReal_inj] at h1 - simp_all only [ofReal_add, ofReal_one, ofReal_zero, not_true_eq_false] - -lemma Rcscb_of_R' (V : CKMMatrix) : - [V]cs|cb = (R' V - conj [V]ub|ud * [V]us|ud) / (1 + normSq [V]us|ud) := by - have h2 : R' V - conj ([V]ub|ud) * [V]us|ud = [V]cs|cb * (1 + normSq [V]us|ud) := by - linear_combination R'_eq V - rw [h2] - rw [mul_div_cancel_right₀] - exact one_plus_normSq_Rusud_neq_zero_ℂ V - -lemma Rcdcb_of_R's (V : CKMMatrix) : - [V]cd|cb = (R's V - conj [V]ub|us * [V]ud|us) / (normSq [V]ud|us + 1) := by - have h2 : R's V - conj ([V]ub|us) * [V]ud|us = [V]cd|cb * (normSq [V]ud|us + 1) := by - linear_combination R's_eq V - rw [h2] - rw [mul_div_cancel_right₀] - exact normSq_Rudus_plus_one_neq_zero_ℂ V - -lemma Rcdcb_R'_orthog {V : CKMMatrix} (hb : [V]ud ≠ 0) (ha : [V]cb ≠ 0) : - [V]cd|cb + (conj [V]ub|ud + R' V * conj [V]us|ud ) / (1 + normSq [V]us|ud) = 0 := by - have h1 := orthog_fst_snd_row_ratios hb ha - rw [Rcscb_of_R'] at h1 - rw [div_mul_eq_mul_div] at h1 - rw [add_assoc] at h1 - rw [div_add'] at h1 - have h2 : (R' V - conj [V]ub|ud * [V]us|ud) * conj [V]us|ud + - conj [V]ub|ud * (1 + normSq [V]us|ud) = conj [V]ub|ud + R' V * conj [V]us|ud := by - rw [← mul_conj] - ring - rw [h2] at h1 - exact h1 - exact one_plus_normSq_Rusud_neq_zero_ℂ V - -lemma Rcdcb_of_R' {V : CKMMatrix} (hb : [V]ud ≠ 0) (ha : [V]cb ≠ 0) : - [V]cd|cb = - (conj [V]ub|ud + R' V * conj [V]us|ud ) / (1 + normSq [V]us|ud) := by - linear_combination (Rcdcb_R'_orthog hb ha) - -lemma Rcscb_R's_orthog {V : CKMMatrix} (hb : [V]us ≠ 0) (ha : [V]cb ≠ 0) : - [V]cs|cb + (conj [V]ub|us + R's V * conj [V]ud|us ) / (normSq [V]ud|us + 1) = 0 := by - have h1 := orthog_fst_snd_row_ratios_cb_us hb ha - rw [Rcdcb_of_R's] at h1 - rw [div_mul_eq_mul_div] at h1 - rw [add_assoc, add_comm [V]cs|cb, ← add_assoc] at h1 - rw [div_add', add_comm] at h1 - have h2 : (R's V - conj [V]ub|us * [V]ud|us) * conj [V]ud|us + - (starRingEnd ℂ) [V]ub|us * ((normSq [V]ud|us) + 1)= conj [V]ub|us + R's V * conj [V]ud|us := by - rw [← mul_conj] - ring - rw [h2] at h1 - exact h1 - exact normSq_Rudus_plus_one_neq_zero_ℂ V - -lemma Rcscb_of_R's {V : CKMMatrix} (hb : [V]us ≠ 0) (ha : [V]cb ≠ 0) : - [V]cs|cb = - (conj [V]ub|us + R's V * conj [V]ud|us ) / (normSq [V]ud|us + 1) := by - linear_combination (Rcscb_R's_orthog hb ha) - -lemma R'_of_Rcscb_Rcdcb {V : CKMMatrix} (hb : [V]ud ≠ 0) (ha : [V]cb ≠ 0) : - R' V = [V]cs|cb - [V]us|ud * [V]cd|cb := by - rw [Rcdcb_of_R' hb ha, Rcscb_of_R'] - have h1 := one_plus_normSq_Rusud_neq_zero_ℂ V - have h2 : conj [V]ud ≠ 0 := (AddEquivClass.map_ne_zero_iff starRingAut).mpr hb - field_simp - rw [Rubud, map_div₀, Rusud, map_div₀, map_div₀] - simp - rw [normSq_eq_conj_mul_self, normSq_eq_conj_mul_self] - field_simp - ring - -lemma R's_of_Rcscb_Rcdcb {V : CKMMatrix} (hb : [V]us ≠ 0) (ha : [V]cb ≠ 0) : - R's V = [V]cd|cb - [V]ud|us * [V]cs|cb := by - rw [Rcscb_of_R's hb ha, Rcdcb_of_R's] - have h1 := normSq_Rudus_plus_one_neq_zero_ℂ V - have h2 : conj [V]us ≠ 0 := (AddEquivClass.map_ne_zero_iff starRingAut).mpr hb - field_simp - rw [Rubus, map_div₀, Rudus, map_div₀, map_div₀] - simp - rw [normSq_eq_conj_mul_self, normSq_eq_conj_mul_self] - field_simp - ring - -lemma R'_of_Rtb!cbud {V : CKMMatrix} (hb : [V]ud ≠ 0) (ha : [V]cb ≠ 0) - {τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) : - R' V = cexp (τ * I) * [V]tb*|cb|ud := by - have h1 : cexp (- τ * I) = conj (cexp (τ * I)) := by - rw [← exp_conj] - simp only [neg_mul, _root_.map_mul, conj_I, mul_neg] - rw [conj_ofReal] - have h2 : [V]tb*|cb|ud = cexp (- τ * I) * R' V := by - rw [h1, R'_of_Rcscb_Rcdcb hb ha] - have h1 := congrFun hτ 2 - simp [crossProduct, tRow, uRow, cRow] at h1 - apply congrArg conj at h1 - simp at h1 - rw [Rtb!cbud, Rcscb, Rusud, Rcdcb, h1] - field_simp - ring - rw [h2, ← mul_assoc, ← exp_add] - simp - - -lemma R's_of_Rtb!cbus {V : CKMMatrix} (hb : [V]us ≠ 0) (ha : [V]cb ≠ 0) - {τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) : - R's V = - cexp (τ * I) * [V]tb*|cb|us := by - have h1 : cexp (- τ * I) = conj (cexp (τ * I)) := by - rw [← exp_conj] - simp only [neg_mul, _root_.map_mul, conj_I, mul_neg] - rw [conj_ofReal] - have h2 : [V]tb*|cb|us = - cexp (- τ * I) * R's V := by - rw [h1, R's_of_Rcscb_Rcdcb hb ha] - have h1 := congrFun hτ 2 - simp [crossProduct, tRow, uRow, cRow] at h1 - apply congrArg conj at h1 - simp at h1 - rw [Rtb!cbus, Rcscb, Rudus, Rcdcb, h1] - field_simp - ring - rw [h2] - simp - rw [← mul_assoc, ← exp_add] - simp - -lemma over_normSq_Rusud (V : CKMMatrix) (hb : [V]ud ≠ 0) (a : ℂ) : a / (1 + normSq [V]us|ud) = - (a * normSq [V]ud) / (normSq [V]ud + normSq [V]us) := by - rw [Rusud] - field_simp - rw [one_add_div] - field_simp - simp - exact hb - -lemma over_normSq_Rudus (V : CKMMatrix) (hb : [V]us ≠ 0) (a : ℂ) : a / (normSq [V]ud|us + 1) = - (a * normSq [V]us) / (normSq [V]ud + normSq [V]us) := by - rw [Rudus] - field_simp - rw [div_add_one] - field_simp - simp - exact hb - -lemma cd_of_ud_neq_zero {V : CKMMatrix} (hb : [V]ud ≠ 0) (ha : [V]cb ≠ 0) - {τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) : - [V]cd = - (conj [V]ub * [V]ud * [V]cb + cexp (τ * I) * conj [V]tb * conj [V]us) / - (normSq [V]ud + normSq [V]us) := by - obtain hτ2 := R'_of_Rtb!cbud hb ha hτ - rw [Rcdcb_mul_cb ha] - rw [Rcdcb_of_R' hb ha, hτ2] - rw [over_normSq_Rusud V hb, div_mul_eq_mul_div] - congr 1 - rw [normSq_eq_conj_mul_self, Rubud, map_div₀, Rusud, map_div₀, Rtb!cbud] - have h1 : conj [V]ud ≠ 0 := (AddEquivClass.map_ne_zero_iff starRingAut).mpr hb - field_simp - ring - -lemma cs_of_ud_neq_zero {V : CKMMatrix} (hb : [V]ud ≠ 0) (ha : [V]cb ≠ 0) - {τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) : - [V]cs = (- conj [V]ub * [V]us * [V]cb + - cexp (τ * I) * conj [V]tb * conj [V]ud ) /(normSq [V]ud + normSq [V]us) := by - have hτ2 := R'_of_Rtb!cbud hb ha hτ - rw [Rcscb_mul_cb ha] - rw [Rcscb_of_R', hτ2] - rw [over_normSq_Rusud V hb, div_mul_eq_mul_div] - congr 1 - rw [normSq_eq_conj_mul_self, Rusud, Rtb!cbud, Rubud, map_div₀] - have h1 : conj [V]ud ≠ 0 := (AddEquivClass.map_ne_zero_iff starRingAut).mpr hb - field_simp - ring - - - -lemma cd_of_us_neq_zero {V : CKMMatrix} (hb : [V]us ≠ 0) (ha : [V]cb ≠ 0) - {τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) : - [V]cd = - - (conj [V]ub * [V]ud * [V]cb + cexp (τ * I) * conj [V]tb * conj [V]us) / - (normSq [V]ud + normSq [V]us) := by - have hτ2 := R's_of_Rtb!cbus hb ha hτ - rw [Rcdcb_mul_cb ha] - rw [Rcdcb_of_R's, hτ2] - rw [over_normSq_Rudus V hb, div_mul_eq_mul_div] - congr 1 - rw [normSq_eq_conj_mul_self, Rubus, map_div₀, Rudus, Rtb!cbus] - have h1 : conj [V]us ≠ 0 := (AddEquivClass.map_ne_zero_iff starRingAut).mpr hb - field_simp - ring - -lemma cs_of_us_neq_zero {V : CKMMatrix} (hb : [V]us ≠ 0) (ha : [V]cb ≠ 0) - {τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) : - [V]cs = ( - conj [V]ub * [V]us * [V]cb + - cexp (τ * I) * conj [V]tb * conj [V]ud ) / (normSq [V]ud + normSq [V]us) := by - have hτ2 := R's_of_Rtb!cbus hb ha hτ - rw [Rcscb_mul_cb ha] - rw [Rcscb_of_R's hb ha, hτ2] - rw [over_normSq_Rudus V hb, div_mul_eq_mul_div] - congr 1 - rw [normSq_eq_conj_mul_self, Rudus, map_div₀, Rtb!cbus, Rubus, map_div₀] - have h1 : conj [V]us ≠ 0 := (AddEquivClass.map_ne_zero_iff starRingAut).mpr hb - field_simp - ring - -lemma cd_of_us_or_ud_neq_zero {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V]cb ≠ 0) - {τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) : - [V]cd = - (conj [V]ub * [V]ud * [V]cb + cexp (τ * I) * conj [V]tb * conj [V]us) / - (normSq [V]ud + normSq [V]us) := by - cases' hb with hb hb - exact cd_of_ud_neq_zero hb ha hτ - exact cd_of_us_neq_zero hb ha hτ - - -lemma cs_of_us_or_ud_neq_zero {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V]cb ≠ 0) - {τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) : - [V]cs = (- conj [V]ub * [V]us * [V]cb + - cexp (τ * I) * conj [V]tb * conj [V]ud ) / (normSq [V]ud + normSq [V]us) := by - cases' hb with hb hb - exact cs_of_ud_neq_zero hb ha hτ - exact cs_of_us_neq_zero hb ha hτ - - - -lemma cd_of_us_or_ud_neq_zero_UCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V]cb ≠ 0) - (hV : UCond₁ V) : [V]cd = (- VtbAbs ⟦V⟧ * VusAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) + - (- VubAbs ⟦V⟧ * VudAbs ⟦V⟧ * VcbAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2 )) * cexp (- arg [V]ub * I) - := by - have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by - simp - exact hV.2.2.2.2 - rw [cd_of_us_or_ud_neq_zero hb ha hτ] - rw [hV.1, hV.2.1, hV.2.2.1, hV.2.2.2.1] - simp [sq, conj_ofReal] - have hx := Vabs_sq_add_neq_zero hb - field_simp - have h1 : conj [V]ub = VubAbs ⟦V⟧ * cexp (- arg [V]ub * I) := by - nth_rewrite 1 [← abs_mul_exp_arg_mul_I [V]ub] - rw [@RingHom.map_mul] - simp [conj_ofReal, ← exp_conj, VAbs] - rw [h1] - ring_nf - -lemma cs_of_us_or_ud_neq_zero_UCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V]cb ≠ 0) - (hV : UCond₁ V) : [V]cs = (VtbAbs ⟦V⟧ * VudAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) - + (- VubAbs ⟦V⟧ * VusAbs ⟦V⟧ * VcbAbs ⟦V⟧/ (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) * cexp (- arg [V]ub * I) - := by - have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by - simp - exact hV.2.2.2.2 - rw [cs_of_us_or_ud_neq_zero hb ha hτ] - rw [hV.1, hV.2.1, hV.2.2.1, hV.2.2.2.1] - simp [sq, conj_ofReal] - have hx := Vabs_sq_add_neq_zero hb - field_simp - have h1 : conj [V]ub = VubAbs ⟦V⟧ * cexp (- arg [V]ub * I) := by - nth_rewrite 1 [← abs_mul_exp_arg_mul_I [V]ub] - rw [@RingHom.map_mul] - simp [conj_ofReal, ← exp_conj, VAbs] - rw [h1] - ring_nf - -lemma cd_of_cb_zero {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V]cb = 0) - {κ : ℝ} (hκ : [V]u = cexp (κ * I) • (conj [V]c ×₃ conj [V]t)) : - [V]cd = - cexp (κ * I) * conj [V]tb * conj [V]us / (normSq [V]ud + normSq [V]us) := by - have h2 : [V]cd = - cexp (κ * I) * conj [V]us / [V]tb := by - have h1 := congrFun hκ 1 - simp [crossProduct, tRow, uRow, cRow] at h1 - rw [ha] at h1 - apply congrArg conj at h1 - simp at h1 - rw [h1] - have hx := tb_neq_zero_of_cb_zero_ud_us_neq_zero ha hb - field_simp - have h1 : conj (cexp (↑κ * I)) = cexp (- κ * I) := by - simp [← exp_conj, conj_ofReal] - rw [h1] - rw [← mul_assoc] - rw [← exp_add] - simp - rw [div_td_of_cb_zero_ud_us_neq_zero ha hb] at h2 - rw [h2] - congr 1 - ring - -lemma cs_of_cb_zero {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V]cb = 0) - {κ : ℝ} (hκ1 : [V]u = cexp (κ * I) • (conj [V]c ×₃ conj [V]t)) : - [V]cs = cexp (κ * I) * conj [V]tb * conj [V]ud / (normSq [V]ud + normSq [V]us) := by - have h2 : [V]cs = cexp (κ * I) * conj [V]ud / [V]tb := by - have h1 := congrFun hκ1 0 - simp [crossProduct, tRow, uRow, cRow] at h1 - rw [ha] at h1 - apply congrArg conj at h1 - simp at h1 - rw [h1] - have hx := tb_neq_zero_of_cb_zero_ud_us_neq_zero ha hb - field_simp - have h1 : conj (cexp (↑κ * I)) = cexp (- κ * I) := by - rw [← exp_conj] - simp only [neg_mul, _root_.map_mul, conj_I, mul_neg] - rw [conj_ofReal] - rw [h1] - rw [← mul_assoc] - rw [← exp_add] - simp - rw [div_td_of_cb_zero_ud_us_neq_zero ha hb] at h2 - rw [h2] - congr 1 - ring - -lemma cd_of_cb_zero_UCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V]cb = 0) - (hV : UCond₁ V) {κ : ℝ} (hκ1 : [V]u = cexp (κ * I) • (conj [V]c ×₃ conj [V]t)) : - [V]cd = (- VtbAbs ⟦V⟧ * VusAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) * cexp (κ * I) := by - rw [cd_of_cb_zero hb ha hκ1] - rw [hV.1, hV.2.1, hV.2.2.2.1] - simp [sq, conj_ofReal] - have hx := Vabs_sq_add_neq_zero hb - field_simp - ring_nf - simp - -lemma cs_of_cb_zero_UCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V]cb = 0) - (hV : UCond₁ V) {κ : ℝ} (hκ1 : [V]u = cexp (κ * I) • (conj [V]c ×₃ conj [V]t)) : - [V]cs = (VtbAbs ⟦V⟧ * VudAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) * cexp (κ * I) := by - rw [cs_of_cb_zero hb ha hκ1] - rw [hV.1, hV.2.1, hV.2.2.2.1] - simp [sq, conj_ofReal] - have hx := Vabs_sq_add_neq_zero hb - field_simp - ring_nf - -def UCond₂ (U : CKMMatrix) : Prop := [U]ud = VudAbs ⟦U⟧ ∧ [U]us = VusAbs ⟦U⟧ - ∧ [U]ub = VubAbs ⟦U⟧ ∧ [U]t = conj [U]u ×₃ conj [U]c - ∧ [U]cd = (- VtbAbs ⟦U⟧ * VusAbs ⟦U⟧ / (VudAbs ⟦U⟧ ^2 + VusAbs ⟦U⟧ ^2)) ∧ - [U]cs = (VtbAbs ⟦U⟧ * VudAbs ⟦U⟧ / (VudAbs ⟦U⟧ ^2 + VusAbs ⟦U⟧ ^2)) - -lemma UCond₂_solv {V : CKMMatrix} (h1 : a + d = 0) (h2 : a + e = 0) (h3 : a + f = - arg [V]ub) - (h4 : 0 = - a - b - c - d - e - f) (h5 : b + d = - κ) (h6 : b + e = - κ) : - b = - κ + a ∧ - c = κ + arg [V]ub + a ∧ - d = - a ∧ - e = - a ∧ - f = - arg [V]ub - a := by - have hd : d = - a := by - linear_combination h1 - subst hd - have he : e = - a := by - linear_combination h2 - subst he - simp_all - have hb : b = - κ + a := by - linear_combination h6 - subst hb - simp_all - have hf : f = - arg [V]ub - a := by - linear_combination h3 - subst hf - simp_all - ring_nf at h4 - have hc : c = κ + arg [V]ub + a := by - linear_combination h4 - simp_all - - -lemma UCond₂_exists {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V]cb = 0) - (hV : UCond₁ V) : ∃ (U : CKMMatrix), V ≈ U ∧ UCond₂ U:= by - obtain ⟨κ, hκ⟩ := V.cRow_cross_tRow_eq_uRow - let U : CKMMatrix := phaseShiftApply V 0 (- κ) (κ + arg [V]ub) 0 0 (- arg [V]ub) - use U - have hUV : ⟦U⟧ = ⟦V⟧ := by - simp - symm - exact phaseShiftApply.equiv _ _ _ _ _ _ _ - apply And.intro - exact phaseShiftApply.equiv _ _ _ _ _ _ _ - apply And.intro - · rw [hUV] - apply ud_eq_abs _ _ _ _ _ _ _ - rw [hV.1, arg_ofReal_of_nonneg] - simp - exact Complex.abs.nonneg _ - apply And.intro - · rw [hUV] - apply us_eq_abs _ _ _ _ _ _ _ - rw [hV.2.1, arg_ofReal_of_nonneg] - simp - exact Complex.abs.nonneg _ - apply And.intro - · rw [hUV] - apply ub_eq_abs _ _ _ _ _ _ _ - ring - apply And.intro - · have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by - simp - exact hV.2.2.2.2 - apply t_eq_conj _ _ _ _ _ _ hτ.symm - ring - apply And.intro - · rw [phaseShiftApply.cd] - rw [cd_of_cb_zero_UCond hb ha hV hκ] - rw [mul_comm, mul_assoc, ← exp_add, hUV] - simp - · rw [phaseShiftApply.cs] - rw [cs_of_cb_zero_UCond hb ha hV hκ] - rw [mul_comm, mul_assoc, ← exp_add, hUV] - simp - - -section zero - -def UCond₃ (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) - -lemma UCond₃_solv {V : CKMMatrix} (h1 : a + f = - arg [V]ub) (h2 : 0 = - a - b - c - d - e - f) - (h3 : b + d = Real.pi - arg [V]cd) (h5 : b + e = - arg [V]cs) : - c = - Real.pi + arg [V]cd + arg [V]cs + arg [V]ub + b ∧ - d = Real.pi - arg [V]cd - b ∧ - e = - arg [V]cs - b ∧ - f = - arg [V]ub - a := by - have hf : f = - arg [V]ub - a := by - linear_combination h1 - subst hf - have he : e = - arg [V]cs - b := by - linear_combination h5 - have hd : d = Real.pi - arg [V]cd - b := by - linear_combination h3 - subst he hd - simp_all - ring_nf at h2 - have hc : c = - Real.pi + arg [V]cd + arg [V]cs + arg [V]ub + b := by - linear_combination h2 - subst hc - ring - - -lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) : - VcsAbs ⟦V⟧ = √(1 - VcdAbs ⟦V⟧ ^ 2) := by - have h1 := snd_row_normalized_abs V - symm - rw [Real.sqrt_eq_iff_sq_eq] - simp [not_or] at ha - rw [cb_eq_zero_of_ud_us_zero ha] at h1 - simp at h1 - simp [VAbs] - linear_combination h1 - simp - rw [@abs_le] - have h1 := VAbs_leq_one 1 0 ⟦V⟧ - have h0 := VAbs_ge_zero 1 0 ⟦V⟧ - simp_all - have hn : -1 ≤ (0 : ℝ) := by simp - exact hn.trans h0 - exact VAbs_ge_zero _ _ ⟦V⟧ - - -lemma UCond₃_exists {V : CKMMatrix} (hb :¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) (hV : UCond₁ V) : - ∃ (U : CKMMatrix), V ≈ U ∧ UCond₃ U:= by - let U : CKMMatrix := phaseShiftApply V 0 0 (- Real.pi + arg [V]cd + arg [V]cs + arg [V]ub) - (Real.pi - arg [V]cd ) (- arg [V]cs) (- arg [V]ub ) - use U - have hUV : ⟦U⟧ = ⟦V⟧ := by - simp - symm - exact phaseShiftApply.equiv _ _ _ _ _ _ _ - apply And.intro - exact phaseShiftApply.equiv _ _ _ _ _ _ _ - apply And.intro - · simp [not_or] at hb - have h1 : VudAbs ⟦U⟧ = 0 := by - rw [hUV] - simp [VAbs, hb] - simp [VAbs] at h1 - exact h1 - apply And.intro - · simp [not_or] at hb - have h1 : VusAbs ⟦U⟧ = 0 := by - rw [hUV] - simp [VAbs, hb] - simp [VAbs] at h1 - exact h1 - apply And.intro - · simp [not_or] at hb - have h3 := cb_eq_zero_of_ud_us_zero hb - have h1 : VcbAbs ⟦U⟧ = 0 := by - rw [hUV] - simp [VAbs, h3] - simp [VAbs] at h1 - exact h1 - apply And.intro - · have hU1 : [U]ub = VubAbs ⟦V⟧ := by - apply ub_eq_abs _ _ _ _ _ _ _ - ring - rw [hU1] - have h1:= (ud_us_neq_zero_iff_ub_neq_one V).mpr.mt hb - simpa using h1 - apply And.intro - · have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by - simp - exact hV.2.2.2.2 - apply t_eq_conj _ _ _ _ _ _ hτ.symm - ring - apply And.intro - · rw [hUV] - apply cd_eq_neg_abs _ _ _ _ _ _ _ - ring - have hcs : [U]cs = VcsAbs ⟦U⟧ := by - rw [hUV] - apply cs_eq_abs _ _ _ _ _ _ _ - ring - rw [hcs, hUV, cs_of_ud_us_zero hb] - - - - -end zero - -end CKMMatrix -end diff --git a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean index 57f02f9..6384225 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean @@ -16,29 +16,50 @@ noncomputable section namespace CKMMatrix open ComplexConjugate -lemma fst_row_normalized_abs (V : CKMMatrix) : - abs [V]ud ^ 2 + abs [V]us ^ 2 + abs [V]ub ^ 2 = 1 := by - have h1 := VAbs_sum_sq_row_eq_one ⟦V⟧ 0 - simp [VAbs] at h1 - exact h1 +section rows + +lemma 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 := by + obtain ⟨V, hV⟩ := Quot.exists_rep V + subst hV + have hV := V.prop + rw [mem_unitaryGroup_iff] at hV + have ht := congrFun (congrFun hV i) i + simp [Matrix.mul_apply, Fin.sum_univ_three] at ht + rw [mul_conj, mul_conj, mul_conj] at ht + repeat rw [← Complex.sq_abs] at ht + rw [← ofReal_inj] + simpa using ht + +lemma fst_row_normalized_abs (V : CKMMatrix) : abs [V]ud ^ 2 + abs [V]us ^ 2 + abs [V]ub ^ 2 = 1 := + VAbs_sum_sq_row_eq_one ⟦V⟧ 0 + +lemma snd_row_normalized_abs (V : CKMMatrix) : abs [V]cd ^ 2 + abs [V]cs ^ 2 + abs [V]cb ^ 2 = 1 := + VAbs_sum_sq_row_eq_one ⟦V⟧ 1 + +lemma thd_row_normalized_abs (V : CKMMatrix) : abs [V]td ^ 2 + abs [V]ts ^ 2 + abs [V]tb ^ 2 = 1 := + VAbs_sum_sq_row_eq_one ⟦V⟧ 2 lemma fst_row_normalized_normSq (V : CKMMatrix) : normSq [V]ud + normSq [V]us + normSq [V]ub = 1 := by - have h1 := V.fst_row_normalized_abs - repeat rw [Complex.sq_abs] at h1 - exact h1 - -lemma snd_row_normalized_abs (V : CKMMatrix) : - abs [V]cd ^ 2 + abs [V]cs ^ 2 + abs [V]cb ^ 2 = 1 := by - have h1 := VAbs_sum_sq_row_eq_one ⟦V⟧ 1 - simp [VAbs] at h1 - exact h1 + repeat rw [← Complex.sq_abs] + exact V.fst_row_normalized_abs lemma snd_row_normalized_normSq (V : CKMMatrix) : normSq [V]cd + normSq [V]cs + normSq [V]cb = 1 := by - have h1 := V.snd_row_normalized_abs - repeat rw [Complex.sq_abs] at h1 - exact h1 + repeat rw [← Complex.sq_abs] + exact V.snd_row_normalized_abs + +lemma thd_row_normalized_normSq (V : CKMMatrix) : + normSq [V]td + normSq [V]ts + normSq [V]tb = 1 := by + repeat rw [← Complex.sq_abs] + exact V.thd_row_normalized_abs + +-- rename +lemma normSq_Vud_plus_normSq_Vus (V : CKMMatrix) : + normSq [V]ud + normSq [V]us = 1 - normSq [V]ub := by + linear_combination (fst_row_normalized_normSq V) + lemma ud_us_neq_zero_iff_ub_neq_one (V : CKMMatrix) : [V]ud ≠ 0 ∨ [V]us ≠ 0 ↔ abs [V]ub ≠ 1 := by @@ -60,6 +81,242 @@ lemma ud_us_neq_zero_iff_ub_neq_one (V : CKMMatrix) : have h2 : ¬ 0 ≤ ( -1 : ℝ) := by simp exact h2 h1 +lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℝ {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) : + normSq [V]ud + normSq [V]us ≠ 0 := by + rw [normSq_Vud_plus_normSq_Vus V] + rw [ud_us_neq_zero_iff_ub_neq_one] at hb + by_contra hn + rw [← Complex.sq_abs] at hn + have h2 : Complex.abs (V.1 0 2) ^2 = 1 := by + linear_combination -(1 * hn) + simp at h2 + cases' h2 with h2 h2 + exact hb h2 + have h3 := Complex.abs.nonneg [V]ub + rw [h2] at h3 + have h2 : ¬ 0 ≤ ( -1 : ℝ) := by simp + exact h2 h3 + +lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℂ {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) : + (normSq [V]ud : ℂ) + normSq [V]us ≠ 0 := by + have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hb + simp at h1 + rw [← ofReal_inj] at h1 + simp_all + + + +section orthogonal + +lemma fst_row_snd_row (V : CKMMatrix) : V.1 1 0 * conj (V.1 0 0) + V.1 1 1 * conj (V.1 0 1) + + V.1 1 2 * conj (V.1 0 2) = 0 := by + have hV := V.prop + rw [mem_unitaryGroup_iff] at hV + have ht := congrFun (congrFun hV 1) 0 + simp [Matrix.mul_apply, Fin.sum_univ_three] at ht + exact ht + +lemma fst_row_thd_row (V : CKMMatrix) : V.1 2 0 * conj (V.1 0 0) + V.1 2 1 * conj (V.1 0 1) + + V.1 2 2 * conj (V.1 0 2) = 0 := by + have hV := V.prop + rw [mem_unitaryGroup_iff] at hV + have ht := congrFun (congrFun hV 2) 0 + simp [Matrix.mul_apply, Fin.sum_univ_three] at ht + exact ht + +lemma Vcd_conj_Vud (V : CKMMatrix) : + [V]cd * conj [V]ud = -[V]cs * conj [V]us - [V]cb * conj [V]ub := by + linear_combination (V.fst_row_snd_row ) + +lemma Vcs_conj_Vus (V : CKMMatrix) : + [V]cs * conj [V]us = - [V]cd * conj [V]ud - [V]cb * conj [V]ub := by + linear_combination (V.fst_row_snd_row ) + + +lemma orthog_fst_snd_row_ratios {V : CKMMatrix} (hb : [V]ud ≠ 0) (ha : [V]cb ≠ 0) : + [V]cd|cb + [V]cs|cb * conj ([V]us|ud) + conj ([V]ub|ud) = 0 := by + suffices h1 : ([V]cd * conj [V]ud + [V]cs * conj [V]us + + [V]cb * conj [V]ub) / ([V]cb * conj [V]ud) = 0 from + by + rw [← h1, Rubud, Rusud, Rcdcb, Rcscb] + have : conj [V]ud ≠ 0 := star_eq_zero.mp.mt hb + field_simp + ring + simp only [fst_row_snd_row V, Fin.isValue, zero_div] + + +lemma orthog_fst_snd_row_ratios_cb_us {V : CKMMatrix} (hb : [V]us ≠ 0) (ha : [V]cb ≠ 0) : + [V]cd|cb * conj [V]ud|us + [V]cs|cb + conj ([V]ub|us) = 0 := by + suffices h1 : ([V]cd * conj [V]ud + [V]cs * conj [V]us + + [V]cb * conj [V]ub) / ([V]cb * conj [V]us) = 0 from + by + rw [← h1, Rubus, Rudus, Rcdcb, Rcscb] + have : conj [V]us ≠ 0 := star_eq_zero.mp.mt hb + field_simp + ring + simp only [fst_row_snd_row V, Fin.isValue, zero_div] + +end orthogonal + +lemma VAbs_thd_eq_one_fst_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} (hV : VAbs i 2 V = 1) : + VAbs i 0 V = 0 := by + have h := VAbs_sum_sq_row_eq_one V i + rw [hV] at h + simp at h + nlinarith + +lemma VAbs_thd_eq_one_snd_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} (hV : VAbs i 2 V = 1) : + VAbs i 1 V = 0 := by + have h := VAbs_sum_sq_row_eq_one V i + rw [hV] at h + simp at h + nlinarith + +section crossProduct + +lemma conj_Vtb_other {V : CKMMatrix} {τ : ℝ} + (hτ : [V]t = cexp (τ * I) • (conj [V]u ×₃ conj [V]c)) : + conj [V]tb = cexp (- τ * I) * ([V]cs * [V]ud - [V]us * [V]cd) := by + have h1 := congrFun hτ 2 + simp [crossProduct, tRow, uRow, cRow] at h1 + apply congrArg conj at h1 + simp at h1 + rw [h1] + simp only [← exp_conj, _root_.map_mul, conj_ofReal, conj_I, mul_neg, Fin.isValue, neg_mul] + field_simp + ring_nf + simp + +end crossProduct + + +lemma conj_Vtb_Vud_other {V : CKMMatrix} {τ : ℝ} + (hτ : [V]t = cexp (τ * I) • (conj [V]u ×₃ conj [V]c)) : + cexp (τ * I) * conj [V]tb * conj [V]ud = + [V]cs * (normSq [V]ud + normSq [V]us) + [V]cb * conj [V]ub * [V]us := by + rw [conj_Vtb_other hτ] + simp [exp_neg] + have h1 := exp_ne_zero (τ * I) + field_simp + have h2 : cexp (τ * I) * ([V]cs * [V]ud - [V]us * [V]cd) * conj [V]ud = cexp (τ * I) * [V]cs + * [V]ud * conj [V]ud - cexp (τ * I) * [V]us * ([V]cd * conj [V]ud) := by + ring + rw [h2, V.Vcd_conj_Vud] + rw [normSq_eq_conj_mul_self, normSq_eq_conj_mul_self] + simp + ring + +-- cexp (τ * I) * conj [V]tb * conj [V]us +lemma conj_Vtb_Vus_other {V : CKMMatrix} {τ : ℝ} + (hτ : [V]t = cexp (τ * I) • (conj [V]u ×₃ conj [V]c)) : + cexp (τ * I) * conj [V]tb * conj [V]us = + - ([V]cd * (normSq [V]ud + normSq [V]us) + [V]cb * conj ([V]ub) * [V]ud) := by + rw [conj_Vtb_other hτ] + simp [exp_neg] + have h1 := exp_ne_zero (τ * I) + field_simp + have h2 : cexp (τ * I) * ([V]cs * [V]ud - [V]us * [V]cd) * conj [V]us = cexp (τ * I) * ([V]cs + * conj [V]us) * [V]ud - cexp (τ * I) * [V]us * [V]cd * conj [V]us := by + ring + rw [h2, V.Vcs_conj_Vus] + rw [normSq_eq_conj_mul_self, normSq_eq_conj_mul_self] + simp + ring + + +lemma cs_of_ud_us_ub_cb_tb {V : CKMMatrix} (h : [V]ud ≠ 0 ∨ [V]us ≠ 0) + {τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) : + [V]cs = (- conj [V]ub * [V]us * [V]cb + + cexp (τ * I) * conj [V]tb * conj [V]ud) / (normSq [V]ud + normSq [V]us) := by + have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℂ h + rw [conj_Vtb_Vud_other hτ] + field_simp + ring + +lemma cd_of_ud_us_ub_cb_tb {V : CKMMatrix} (h : [V]ud ≠ 0 ∨ [V]us ≠ 0) + {τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) : + [V]cd = - (conj [V]ub * [V]ud * [V]cb + cexp (τ * I) * conj [V]tb * conj [V]us) / + (normSq [V]ud + normSq [V]us) := by + have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℂ h + rw [conj_Vtb_Vus_other hτ] + field_simp + ring + +end rows + +section ratios + +lemma one_plus_normSq_Rusud_neq_zero_ℝ (V : CKMMatrix): + 1 + normSq ([V]us|ud) ≠ 0 := by + have h1 : 0 ≤ (normSq ([V]us|ud)) := normSq_nonneg ([V]us|ud) + have h2 : 0 < 1 + normSq ([V]us|ud) := by linarith + by_contra hn + have h3 := lt_of_lt_of_eq h2 hn + simp at h3 + +lemma normSq_Rudus_plus_one_neq_zero_ℝ (V : CKMMatrix): + normSq ([V]ud|us) + 1 ≠ 0 := by + have h1 : 0 ≤ (normSq ([V]ud|us)) := normSq_nonneg ([V]ud|us) + have h2 : 0 < normSq ([V]ud|us) + 1 := by linarith + by_contra hn + have h3 := lt_of_lt_of_eq h2 hn + simp at h3 + +lemma one_plus_normSq_Rusud_neq_zero_ℂ (V : CKMMatrix): + 1 + (normSq ([V]us|ud) : ℂ) ≠ 0 := by + by_contra hn + have h1 := one_plus_normSq_Rusud_neq_zero_ℝ V + simp at h1 + rw [← ofReal_inj] at h1 + simp_all only [ofReal_add, ofReal_one, ofReal_zero, not_true_eq_false] + +lemma normSq_Rudus_plus_one_neq_zero_ℂ (V : CKMMatrix): + (normSq ([V]ud|us) : ℂ) + 1 ≠ 0 := by + by_contra hn + have h1 := normSq_Rudus_plus_one_neq_zero_ℝ V + simp at h1 + rw [← ofReal_inj] at h1 + simp_all only [ofReal_add, ofReal_one, ofReal_zero, not_true_eq_false] + +end ratios + +section individual + +lemma VAbs_ge_zero (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : 0 ≤ VAbs i j V := by + obtain ⟨V, hV⟩ := Quot.exists_rep V + rw [← hV] + exact Complex.abs.nonneg _ + + +lemma VAbs_leq_one (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : VAbs i j V ≤ 1 := by + have h := VAbs_sum_sq_row_eq_one V i + fin_cases j + change VAbs i 0 V ≤ 1 + nlinarith + change VAbs i 1 V ≤ 1 + nlinarith + change VAbs i 2 V ≤ 1 + nlinarith + + +end individual + +section columns + + +lemma 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 := by + obtain ⟨V, hV⟩ := Quot.exists_rep V + subst hV + have hV := V.prop + rw [mem_unitaryGroup_iff'] at hV + have ht := congrFun (congrFun hV i) i + simp [Matrix.mul_apply, Fin.sum_univ_three] at ht + rw [mul_comm, mul_conj, mul_comm, mul_conj, mul_comm, mul_conj] at ht + repeat rw [← Complex.sq_abs] at ht + rw [← ofReal_inj] + simpa using ht + lemma thd_col_normalized_abs (V : CKMMatrix) : abs [V]ub ^ 2 + abs [V]cb ^ 2 + abs [V]tb ^ 2 = 1 := by have h1 := VAbs_sum_sq_col_eq_one ⟦V⟧ 2 @@ -72,6 +329,43 @@ lemma thd_col_normalized_normSq (V : CKMMatrix) : repeat rw [Complex.sq_abs] at h1 exact h1 +lemma cb_eq_zero_of_ud_us_zero {V : CKMMatrix} (h : [V]ud = 0 ∧ [V]us = 0) : + [V]cb = 0 := by + have h1 := fst_row_normalized_abs V + rw [← thd_col_normalized_abs V] at h1 + simp [h] at h1 + rw [add_assoc] at h1 + simp at h1 + rw [add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)] at h1 + simp at h1 + exact h1.1 + + +lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) : + VcsAbs ⟦V⟧ = √(1 - VcdAbs ⟦V⟧ ^ 2) := by + have h1 := snd_row_normalized_abs V + symm + rw [Real.sqrt_eq_iff_sq_eq] + simp [not_or] at ha + rw [cb_eq_zero_of_ud_us_zero ha] at h1 + simp at h1 + simp [VAbs] + linear_combination h1 + simp + rw [@abs_le] + have h1 := VAbs_leq_one 1 0 ⟦V⟧ + have h0 := VAbs_ge_zero 1 0 ⟦V⟧ + simp_all + have hn : -1 ≤ (0 : ℝ) := by simp + exact hn.trans h0 + exact VAbs_ge_zero _ _ ⟦V⟧ + +end columns + + + + + lemma cb_tb_neq_zero_iff_ub_neq_one (V : CKMMatrix) : [V]cb ≠ 0 ∨ [V]tb ≠ 0 ↔ abs [V]ub ≠ 1 := by have h2 := V.thd_col_normalized_abs @@ -100,16 +394,6 @@ lemma tb_neq_zero_of_cb_zero_ud_us_neq_zero {V : CKMMatrix} (h : [V]cb = 0) rw [← cb_tb_neq_zero_iff_ub_neq_one] at h1 simp_all -lemma cb_eq_zero_of_ud_us_zero {V : CKMMatrix} (h : [V]ud = 0 ∧ [V]us = 0) : - [V]cb = 0 := by - have h1 := fst_row_normalized_abs V - rw [← thd_col_normalized_abs V] at h1 - simp [h] at h1 - rw [add_assoc] at h1 - simp at h1 - rw [add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)] at h1 - simp at h1 - exact h1.1 @@ -135,32 +419,6 @@ lemma div_td_of_cb_zero_ud_us_neq_zero {V : CKMMatrix} (h : [V]cb = 0) simp at h1 exact h1 -lemma normSq_Vud_plus_normSq_Vus (V : CKMMatrix) : - normSq [V]ud + normSq [V]us = 1 - normSq [V]ub := by - linear_combination (fst_row_normalized_normSq V) - -lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℝ {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) : - normSq [V]ud + normSq [V]us ≠ 0 := by - rw [normSq_Vud_plus_normSq_Vus V] - rw [ud_us_neq_zero_iff_ub_neq_one] at hb - by_contra hn - rw [← Complex.sq_abs] at hn - have h2 : Complex.abs (V.1 0 2) ^2 = 1 := by - linear_combination -(1 * hn) - simp at h2 - cases' h2 with h2 h2 - exact hb h2 - have h3 := Complex.abs.nonneg [V]ub - rw [h2] at h3 - have h2 : ¬ 0 ≤ ( -1 : ℝ) := by simp - exact h2 h3 - -lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℂ {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) : - (normSq [V]ud : ℂ) + normSq [V]us ≠ 0 := by - have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hb - simp at h1 - rw [← ofReal_inj] at h1 - simp_all lemma Vabs_sq_add_neq_zero {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) : ((VAbs 0 0 ⟦V⟧ : ℂ) * ↑(VAbs 0 0 ⟦V⟧) + ↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 0 1 ⟦V⟧)) ≠ 0 := by @@ -170,5 +428,46 @@ lemma Vabs_sq_add_neq_zero {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) : exact h1 + +lemma 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 := by + have h := VAbs_sum_sq_col_eq_one V i + rw [hV] at h + simp at h + nlinarith + +lemma 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 := by + have h := VAbs_sum_sq_col_eq_one V i + rw [hV] at h + simp at h + nlinarith + +lemma VAbs_thd_neq_one_fst_snd_sq_neq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} + (hV : VAbs i 2 V ≠ 1) : (VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2) ≠ 0 := by + have h1 : 1 - VAbs i 2 V ^ 2 = VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 := by + linear_combination - (VAbs_sum_sq_row_eq_one V i) + rw [← h1] + by_contra h + have h2 : VAbs i 2 V ^2 = 1 := by + nlinarith + simp only [Fin.isValue, sq_eq_one_iff] at h2 + have h3 : 0 ≤ VAbs i 2 V := VAbs_ge_zero i 2 V + have h4 : VAbs i 2 V = 1 := by + nlinarith + exact hV h4 + +lemma VAbs_thd_neq_one_sqrt_fst_snd_sq_neq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} + (hV : VAbs i 2 V ≠ 1) : √(VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2) ≠ 0 := by + rw [Real.sqrt_ne_zero (Left.add_nonneg (sq_nonneg (VAbs i 0 V)) (sq_nonneg (VAbs i 1 V)))] + exact VAbs_thd_neq_one_fst_snd_sq_neq_zero hV + +lemma VcbAbs_sq_add_VtbAbs_sq (V : Quotient CKMMatrixSetoid) : + VcbAbs V ^ 2 + VtbAbs V ^ 2 = 1 - VubAbs V ^2 := by + linear_combination (VAbs_sum_sq_col_eq_one V 2) + +lemma VudAbs_sq_add_VusAbs_sq : VudAbs V ^ 2 + VusAbs V ^2 = 1 - VubAbs V ^2 := by + linear_combination (VAbs_sum_sq_row_eq_one V 0) + end CKMMatrix end diff --git a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean index 27edfd7..550fc19 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean @@ -283,9 +283,6 @@ lemma uRow_cross_cRow_eq_tRow (V : CKMMatrix) : rw [hx, hτ] - - - def uRow₁₂ (V : CKMMatrix) : Fin 2 → ℂ := ![[V]ud, [V]us] def cRow₁₂ (V : CKMMatrix) : Fin 2 → ℂ := ![[V]cd, [V]cs] diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean new file mode 100644 index 0000000..b02b5e2 --- /dev/null +++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean @@ -0,0 +1,184 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.FlavorPhysics.CKMMatrix.Basic +import HepLean.FlavorPhysics.CKMMatrix.Rows +import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom +import HepLean.FlavorPhysics.CKMMatrix.Invariants +import Mathlib.Analysis.SpecialFunctions.Complex.Arg + +open Matrix Complex +open ComplexConjugate +open CKMMatrix + +noncomputable section + +-- to be renamed stanParamAsMatrix ... +def standardParameterizationAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : Matrix (Fin 3) (Fin 3) ℂ := + ![![Real.cos θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₃ * exp (-I * δ₁₃)], + ![(-Real.sin θ₁₂ * Real.cos θ₂₃) - (Real.cos θ₁₂ * Real.sin θ₁₃ * Real.sin θ₂₃ * exp (I * δ₁₃)), + Real.cos θ₁₂ * Real.cos θ₂₃ - Real.sin θ₁₂ * Real.sin θ₁₃ * Real.sin θ₂₃ * exp (I * δ₁₃), + Real.sin θ₂₃ * Real.cos θ₁₃], + ![Real.sin θ₁₂ * Real.sin θ₂₃ - Real.cos θ₁₂ * Real.sin θ₁₃ * Real.cos θ₂₃ * exp (I * δ₁₃), + (-Real.cos θ₁₂ * Real.sin θ₂₃) - (Real.sin θ₁₂ * Real.sin θ₁₃ * Real.cos θ₂₃ * exp (I * δ₁₃)), + Real.cos θ₂₃ * Real.cos θ₁₃]] + +open CKMMatrix + +lemma standardParameterizationAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : + ((standardParameterizationAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standardParameterizationAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) = 1 := by + funext j i + simp only [standardParameterizationAsMatrix, neg_mul, Fin.isValue] + rw [mul_apply] + have h1 := exp_ne_zero (I * ↑δ₁₃) + fin_cases j <;> rw [Fin.sum_univ_three] + simp only [Fin.zero_eta, Fin.isValue, conjTranspose_apply, cons_val', cons_val_zero, empty_val', + cons_val_fin_one, star_mul', RCLike.star_def, conj_ofReal, cons_val_one, head_cons, star_sub, + star_neg, ← exp_conj, _root_.map_mul, conj_I, neg_mul, cons_val_two, tail_cons, head_fin_const] + simp [conj_ofReal] + rw [exp_neg ] + fin_cases i <;> simp + · ring_nf + field_simp + rw [sin_sq, sin_sq, sin_sq] + ring + · ring_nf + field_simp + rw [sin_sq, sin_sq] + ring + · ring_nf + field_simp + rw [sin_sq] + ring + simp only [Fin.mk_one, Fin.isValue, conjTranspose_apply, cons_val', cons_val_one, head_cons, + empty_val', cons_val_fin_one, cons_val_zero, star_mul', RCLike.star_def, conj_ofReal, star_sub, + ← exp_conj, _root_.map_mul, conj_I, neg_mul, cons_val_two, tail_cons, head_fin_const, star_neg] + simp [conj_ofReal] + rw [exp_neg] + fin_cases i <;> simp + · ring_nf + field_simp + rw [sin_sq, sin_sq] + ring + · ring_nf + field_simp + rw [sin_sq, sin_sq, sin_sq] + ring + · ring_nf + field_simp + rw [sin_sq] + ring + simp only [Fin.reduceFinMk, Fin.isValue, conjTranspose_apply, cons_val', cons_val_two, tail_cons, + head_cons, empty_val', cons_val_fin_one, cons_val_zero, star_mul', RCLike.star_def, conj_ofReal, + ← exp_conj, map_neg, _root_.map_mul, conj_I, neg_mul, neg_neg, cons_val_one, head_fin_const] + simp [conj_ofReal] + rw [exp_neg] + fin_cases i <;> simp + · ring_nf + rw [sin_sq] + ring + · ring_nf + rw [sin_sq] + ring + · ring_nf + field_simp + rw [sin_sq, sin_sq] + ring + +def sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix := + ⟨standardParameterizationAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by + rw [mem_unitaryGroup_iff'] + exact standardParameterizationAsMatrix_unitary θ₁₂ θ₁₃ θ₂₃ δ₁₃⟩ + +lemma sP_cross (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : + [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]t = (conj [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]u ×₃ conj [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) := by + have h1 := exp_ne_zero (I * ↑δ₁₃) + funext i + fin_cases i + · simp only [tRow, sP, standardParameterizationAsMatrix, neg_mul, exp_neg, + Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, tail_cons, + head_fin_const, cons_val_one, head_cons, Fin.zero_eta, crossProduct, uRow, cRow, + LinearMap.mk₂_apply, Pi.conj_apply, _root_.map_mul, map_inv₀, ← exp_conj, conj_I, conj_ofReal, + inv_inv, map_sub, map_neg] + field_simp + ring_nf + rw [sin_sq] + ring + · simp only [tRow, sP, standardParameterizationAsMatrix, neg_mul, exp_neg, Fin.isValue, cons_val', + cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, tail_cons, head_fin_const, + cons_val_one, head_cons, Fin.mk_one, crossProduct, uRow, cRow, LinearMap.mk₂_apply, + Pi.conj_apply, _root_.map_mul, conj_ofReal, map_inv₀, ← exp_conj, conj_I, inv_inv, map_sub, + map_neg] + field_simp + ring_nf + rw [sin_sq] + ring + · simp only [tRow, sP, standardParameterizationAsMatrix, neg_mul, exp_neg, Fin.isValue, + cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, tail_cons, head_fin_const, + cons_val_one, head_cons, Fin.reduceFinMk, crossProduct, uRow, cRow, LinearMap.mk₂_apply, + Pi.conj_apply, _root_.map_mul, conj_ofReal, map_inv₀, ← exp_conj, conj_I, inv_inv, map_sub, + map_neg] + field_simp + ring_nf + rw [sin_sq] + ring + +lemma eq_sP (U : CKMMatrix) {θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ} (hu : [U]u = [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]u) + (hc : [U]c = [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) (hU : [U]t = conj [U]u ×₃ conj [U]c) : + U = sP θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by + apply ext_Rows hu hc + rw [hU, sP_cross, hu, hc] + +lemma eq_phases_sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ δ₁₃' : ℝ) (h : cexp (δ₁₃ * I) = cexp (δ₁₃' * I)) : + sP θ₁₂ θ₁₃ θ₂₃ δ₁₃ = sP θ₁₂ θ₁₃ θ₂₃ δ₁₃' := by + simp [sP, standardParameterizationAsMatrix] + apply CKMMatrix_ext + simp + rw [show exp (I * δ₁₃) = exp (I * δ₁₃') by rw [mul_comm, h, mul_comm]] + rw [show cexp (-(I * ↑δ₁₃)) = cexp (-(I * ↑δ₁₃')) by rw [exp_neg, exp_neg, mul_comm, h, mul_comm]] + +namespace Invariant + +lemma VusVubVcdSq_sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂) + (h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) : + VusVubVcdSq ⟦sP θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ = + Real.sin θ₁₂ ^ 2 * Real.cos θ₁₃ ^ 2 * Real.sin θ₁₃ ^ 2 * Real.sin θ₂₃ ^ 2 := by + simp only [VusVubVcdSq, VusAbs, VAbs, VAbs', Fin.isValue, sP, standardParameterizationAsMatrix, + neg_mul, Quotient.lift_mk, cons_val', cons_val_one, head_cons, + empty_val', cons_val_fin_one, cons_val_zero, _root_.map_mul, VubAbs, cons_val_two, tail_cons, + VcbAbs, VudAbs, Complex.abs_ofReal] + by_cases hx : Real.cos θ₁₃ ≠ 0 + · rw [Complex.abs_exp] + simp + rw [_root_.abs_of_nonneg h1, _root_.abs_of_nonneg h3, _root_.abs_of_nonneg h2, + _root_.abs_of_nonneg h4] + simp [sq] + ring_nf + nth_rewrite 2 [Real.sin_sq θ₁₂] + ring_nf + field_simp + ring + · simp at hx + rw [hx] + simp + +lemma mulExpδ₃_sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂) + (h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) : + mulExpδ₃ ⟦sP θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ = + sin θ₁₂ * cos θ₁₃ ^ 2 * sin θ₂₃ * sin θ₁₃ * cos θ₁₂ * cos θ₂₃ * cexp (I * δ₁₃) := by + rw [mulExpδ₃, VusVubVcdSq_sP _ _ _ _ h1 h2 h3 h4 ] + simp only [jarlskogℂ, sP, standardParameterizationAsMatrix, neg_mul, + Quotient.lift_mk, jarlskogℂCKM, Fin.isValue, cons_val', cons_val_one, head_cons, + empty_val', cons_val_fin_one, cons_val_zero, cons_val_two, tail_cons, _root_.map_mul, ← + exp_conj, map_neg, conj_I, conj_ofReal, neg_neg, map_sub] + simp + ring_nf + rw [exp_neg] + have h1 : cexp (I * δ₁₃) ≠ 0 := exp_ne_zero _ + field_simp + +end Invariant + +end diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameters.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean similarity index 58% rename from HepLean/FlavorPhysics/CKMMatrix/StandardParameters.lean rename to HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean index ecdf615..d19866b 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameters.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean @@ -6,161 +6,194 @@ Authors: Joseph Tooby-Smith import HepLean.FlavorPhysics.CKMMatrix.Basic import HepLean.FlavorPhysics.CKMMatrix.Rows import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom -import HepLean.FlavorPhysics.CKMMatrix.Ratios +import HepLean.FlavorPhysics.CKMMatrix.Invariants +import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic import Mathlib.Analysis.SpecialFunctions.Complex.Arg open Matrix Complex open ComplexConjugate - +open CKMMatrix noncomputable section +def S₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := VusAbs V / (√ (VudAbs V ^ 2 + VusAbs V ^ 2)) def S₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := VubAbs V -lemma VubAbs_eq_S₁₃ (V : Quotient CKMMatrixSetoid) : VubAbs V = S₁₃ V := rfl - -def θ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₁₃ V) - -lemma S₁₃_eq_sin_θ₁₃ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₁₃ V) = S₁₃ V := by - refine Real.sin_arcsin ?_ ?_ - have h1 := VAbs_ge_zero 0 2 V - rw [← VubAbs_eq_S₁₃] - simp - linarith - rw [← VubAbs_eq_S₁₃] - exact (VAbs_leq_one 0 2 V) - -lemma S₁₃_eq_ℂsin_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.sin (θ₁₃ V) = S₁₃ V := by - rw [← S₁₃_eq_sin_θ₁₃] - simp - -lemma complexAbs_sin_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.sin (θ₁₃ V)) = - sin (θ₁₃ V):= by - rw [S₁₃_eq_ℂsin_θ₁₃, ← VubAbs_eq_S₁₃] - rw [Complex.abs_ofReal] - simp - exact VAbs_ge_zero 0 2 V - - -lemma S₁₃_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₁₃ V = 1 := by - rw [← VubAbs_eq_S₁₃, ha] - - -def C₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₁₃ V) - -lemma C₁₃_eq_ℂcos_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₁₃ V) = C₁₃ V := by - simp [C₁₃] - -lemma complexAbs_cos_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₁₃ V)) = - cos (θ₁₃ V):= by - rw [C₁₃_eq_ℂcos_θ₁₃, Complex.abs_ofReal] - simp - exact Real.cos_arcsin_nonneg _ - -lemma cos_θ₁₃_zero {V : Quotient CKMMatrixSetoid} (h1 : Real.cos (θ₁₃ V) = 0) : - VubAbs V = 1 := by - rw [θ₁₃, Real.cos_arcsin, ← VubAbs_eq_S₁₃, Real.sqrt_eq_zero] at h1 - have h2 : VubAbs V ^ 2 = 1 := by linear_combination -(1 * h1) - simp at h2 - cases' h2 with h2 h2 - exact h2 - have h3 := VAbs_ge_zero 0 2 V - rw [h2] at h3 - simp at h3 - linarith - simp - rw [_root_.abs_of_nonneg (VAbs_ge_zero 0 2 V)] - exact VAbs_leq_one 0 2 V - - -lemma S₁₃_sq_add_C₁₃_sq (V : Quotient CKMMatrixSetoid) : S₁₃ V ^ 2 + C₁₃ V ^ 2 = 1 := by - rw [← S₁₃_eq_sin_θ₁₃ V, C₁₃] - exact Real.sin_sq_add_cos_sq (θ₁₃ V) - -lemma C₁₃_of_Vub_eq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : C₁₃ V = 0 := by - rw [C₁₃, θ₁₃, Real.cos_arcsin, ← VubAbs_eq_S₁₃, ha] - simp - -lemma C₁₃_eq_add_sq (V : Quotient CKMMatrixSetoid) : C₁₃ V = √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by - rw [C₁₃, θ₁₃, Real.cos_arcsin, S₁₃] - have h1 : 1 - VubAbs V ^ 2 = VudAbs V ^ 2 + VusAbs V ^ 2 := by - linear_combination - (VAbs_sum_sq_row_eq_one V 0) - rw [h1] - -/-- If VubAbs V = 1 this will give zero.-/ -def S₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := VusAbs V / (√ (VudAbs V ^ 2 + VusAbs V ^ 2)) +def S₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := + if VubAbs V = 1 then VcdAbs V + else VcbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2) def θ₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₁₂ V) -lemma S₁₂_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₁₂ V := by - rw [S₁₂] - rw [@div_nonneg_iff] - apply Or.inl - apply And.intro - exact VAbs_ge_zero 0 1 V - exact Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2) +def θ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₁₃ V) +def θ₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₂₃ V) + +def C₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₁₂ V) + +def C₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₁₃ V) + +def C₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₂₃ V) + +def δ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := + arg (Invariant.mulExpδ₃ V) + +section sines + +lemma S₁₂_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₁₂ V := by + rw [S₁₂, div_nonneg_iff] + apply Or.inl + apply (And.intro (VAbs_ge_zero 0 1 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2))) + +lemma S₁₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₁₃ V := + VAbs_ge_zero 0 2 V + +lemma S₂₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₂₃ V := by + by_cases ha : VubAbs V = 1 + rw [S₂₃, if_pos ha] + exact VAbs_ge_zero 1 0 V + rw [S₂₃, if_neg ha, @div_nonneg_iff] + apply Or.inl + apply And.intro (VAbs_ge_zero 1 2 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2)) lemma S₁₂_leq_one (V : Quotient CKMMatrixSetoid) : S₁₂ V ≤ 1 := by - rw [S₁₂] - rw [@div_le_one_iff] + rw [S₁₂, @div_le_one_iff] by_cases h1 : √(VudAbs V ^ 2 + VusAbs V ^ 2) = 0 simp [h1] - have h2 := Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2) - rw [le_iff_eq_or_lt] at h2 + have h2 := le_iff_eq_or_lt.mp (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2)) have h3 : 0 < √(VudAbs V ^ 2 + VusAbs V ^ 2) := by cases' h2 with h2 h2 simp_all exact h2 apply Or.inl simp_all - rw [Real.le_sqrt] + rw [Real.le_sqrt (VAbs_ge_zero 0 1 V) (le_of_lt h3)] simp exact sq_nonneg (VAbs 0 0 V) - exact VAbs_ge_zero 0 1 V - exact le_of_lt h3 + +lemma S₁₃_leq_one (V : Quotient CKMMatrixSetoid) : S₁₃ V ≤ 1 := + VAbs_leq_one 0 2 V + +lemma S₂₃_leq_one (V : Quotient CKMMatrixSetoid) : S₂₃ V ≤ 1 := by + by_cases ha : VubAbs V = 1 + rw [S₂₃, if_pos ha] + exact VAbs_leq_one 1 0 V + rw [S₂₃, if_neg ha, @div_le_one_iff] + by_cases h1 : √(VudAbs V ^ 2 + VusAbs V ^ 2) = 0 + simp [h1] + have h2 := le_iff_eq_or_lt.mp (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2)) + have h3 : 0 < √(VudAbs V ^ 2 + VusAbs V ^ 2) := by + cases' h2 with h2 h2 + simp_all + exact h2 + apply Or.inl + simp_all + rw [Real.le_sqrt (VAbs_ge_zero 1 2 V) (le_of_lt h3)] + rw [VudAbs_sq_add_VusAbs_sq, ← VcbAbs_sq_add_VtbAbs_sq] + simp + exact sq_nonneg (VAbs 2 2 V) lemma S₁₂_eq_sin_θ₁₂ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₁₂ V) = S₁₂ V := Real.sin_arcsin (le_trans (by simp) (S₁₂_nonneg V)) (S₁₂_leq_one V) -lemma S₁₂_eq_ℂsin_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.sin (θ₁₂ V) = S₁₂ V := by - rw [← S₁₂_eq_sin_θ₁₂] - simp +lemma S₁₃_eq_sin_θ₁₃ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₁₃ V) = S₁₃ V := + Real.sin_arcsin (le_trans (by simp) (S₁₃_nonneg V)) (S₁₃_leq_one V) -lemma complexAbs_sin_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.sin (θ₁₂ V)) = - sin (θ₁₂ V):= by - rw [S₁₂_eq_ℂsin_θ₁₂, Complex.abs_ofReal] - simp +lemma S₂₃_eq_sin_θ₂₃ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₂₃ V) = S₂₃ V := + Real.sin_arcsin (le_trans (by simp) (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)) + +lemma complexAbs_sin_θ₁₂ (V : Quotient CKMMatrixSetoid) : + Complex.abs (Complex.sin (θ₁₂ V)) = sin (θ₁₂ V):= by + rw [S₁₂_eq_ℂsin_θ₁₂, Complex.abs_ofReal, ofReal_inj, abs_eq_self] exact S₁₂_nonneg _ +lemma complexAbs_sin_θ₁₃ (V : Quotient CKMMatrixSetoid) : + Complex.abs (Complex.sin (θ₁₃ V)) = sin (θ₁₃ V):= by + rw [S₁₃_eq_ℂsin_θ₁₃, Complex.abs_ofReal, ofReal_inj, abs_eq_self] + exact S₁₃_nonneg _ + +lemma complexAbs_sin_θ₂₃ (V : Quotient CKMMatrixSetoid) : + Complex.abs (Complex.sin (θ₂₃ V)) = sin (θ₂₃ V):= by + rw [S₂₃_eq_ℂsin_θ₂₃, Complex.abs_ofReal, ofReal_inj, abs_eq_self] + exact S₂₃_nonneg _ + lemma S₁₂_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₁₂ V = 0 := by - rw [S₁₂] have h1 : 1 - VubAbs V ^ 2 = VudAbs V ^ 2 + VusAbs V ^ 2 := by linear_combination - (VAbs_sum_sq_row_eq_one V 0) - rw [← h1] - rw [ha] - simp + simp [S₁₂, ← h1, ha] -def C₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₁₂ V) +lemma S₁₃_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₁₃ V = 1 := by + rw [S₁₃, ha] + +lemma S₂₃_of_Vub_eq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₂₃ V = VcdAbs V := by + rw [S₂₃, if_pos ha] + +lemma S₂₃_of_Vub_neq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) : + S₂₃ V = VcbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by + rw [S₂₃, if_neg ha] + +end sines + +section cosines lemma C₁₂_eq_ℂcos_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₁₂ V) = C₁₂ V := by simp [C₁₂] +lemma C₁₃_eq_ℂcos_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₁₃ V) = C₁₃ V := by + simp [C₁₃] + +lemma C₂₃_eq_ℂcos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₂₃ V) = C₂₃ V := by + simp [C₂₃] + lemma complexAbs_cos_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₁₂ V)) = cos (θ₁₂ V):= by rw [C₁₂_eq_ℂcos_θ₁₂, Complex.abs_ofReal] simp exact Real.cos_arcsin_nonneg _ -lemma C₁₂_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : C₁₂ V = 1 := by - rw [C₁₂, θ₁₂, Real.cos_arcsin, S₁₂_of_Vub_one ha] +lemma complexAbs_cos_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₁₃ V)) = + cos (θ₁₃ V):= by + rw [C₁₃_eq_ℂcos_θ₁₃, Complex.abs_ofReal] simp + exact Real.cos_arcsin_nonneg _ + +lemma complexAbs_cos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₂₃ V)) = + cos (θ₂₃ V):= by + rw [C₂₃_eq_ℂcos_θ₂₃, Complex.abs_ofReal] + simp + exact Real.cos_arcsin_nonneg _ lemma S₁₂_sq_add_C₁₂_sq (V : Quotient CKMMatrixSetoid) : S₁₂ V ^ 2 + C₁₂ V ^ 2 = 1 := by rw [← S₁₂_eq_sin_θ₁₂ V, C₁₂] exact Real.sin_sq_add_cos_sq (θ₁₂ V) +lemma S₁₃_sq_add_C₁₃_sq (V : Quotient CKMMatrixSetoid) : S₁₃ V ^ 2 + C₁₃ V ^ 2 = 1 := by + rw [← S₁₃_eq_sin_θ₁₃ V, C₁₃] + exact Real.sin_sq_add_cos_sq (θ₁₃ V) + +lemma S₂₃_sq_add_C₂₃_sq (V : Quotient CKMMatrixSetoid) : S₂₃ V ^ 2 + C₂₃ V ^ 2 = 1 := by + rw [← S₂₃_eq_sin_θ₂₃ V, C₂₃] + exact Real.sin_sq_add_cos_sq (θ₂₃ V) + +lemma C₁₂_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : C₁₂ V = 1 := by + rw [C₁₂, θ₁₂, Real.cos_arcsin, S₁₂_of_Vub_one ha] + simp + +lemma C₁₃_of_Vub_eq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : C₁₃ V = 0 := by + rw [C₁₃, θ₁₃, Real.cos_arcsin, S₁₃, ha] + simp + +--rename lemma C₁₂_eq_Vud_div_sqrt {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) : C₁₂ V = VudAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by rw [C₁₂, θ₁₂, Real.cos_arcsin, S₁₂, div_pow, Real.sq_sqrt] @@ -173,7 +206,43 @@ lemma C₁₂_eq_Vud_div_sqrt {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ exact VAbs_thd_neq_one_fst_snd_sq_neq_zero ha exact (Left.add_nonneg (sq_nonneg (VAbs 0 0 V)) (sq_nonneg (VAbs 0 1 V))) -theorem VusAbs_eq_S₁₂_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VusAbs V = S₁₂ V * C₁₃ V := by +--rename +lemma C₁₃_eq_add_sq (V : Quotient CKMMatrixSetoid) : C₁₃ V = √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by + rw [C₁₃, θ₁₃, Real.cos_arcsin, S₁₃] + have h1 : 1 - VubAbs V ^ 2 = VudAbs V ^ 2 + VusAbs V ^ 2 := by + linear_combination - (VAbs_sum_sq_row_eq_one V 0) + rw [h1] + +lemma C₂₃_of_Vub_neq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) : + C₂₃ V = VtbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by + rw [C₂₃, θ₂₃, Real.cos_arcsin, S₂₃_of_Vub_neq_one ha, div_pow, Real.sq_sqrt] + rw [VudAbs_sq_add_VusAbs_sq, ← VcbAbs_sq_add_VtbAbs_sq] + rw [one_sub_div] + simp only [VcbAbs, Fin.isValue, VtbAbs, add_sub_cancel_left] + rw [Real.sqrt_div (sq_nonneg (VAbs 2 2 V))] + rw [Real.sqrt_sq (VAbs_ge_zero 2 2 V)] + rw [VcbAbs_sq_add_VtbAbs_sq, ← VudAbs_sq_add_VusAbs_sq ] + exact VAbs_thd_neq_one_fst_snd_sq_neq_zero ha + exact (Left.add_nonneg (sq_nonneg (VAbs 0 0 V)) (sq_nonneg (VAbs 0 1 V))) + +end cosines + +section VAbs + +-- rename to VudAbs_standard_param +lemma VudAbs_eq_C₁₂_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VudAbs V = C₁₂ V * C₁₃ V := by + by_cases ha : VubAbs V = 1 + change VAbs 0 0 V = C₁₂ V * C₁₃ V + rw [VAbs_thd_eq_one_fst_eq_zero ha] + rw [C₁₃, θ₁₃, Real.cos_arcsin, S₁₃, ha] + simp + rw [C₁₂_eq_Vud_div_sqrt ha, C₁₃, θ₁₃, Real.cos_arcsin, S₁₃] + have h1 : 1 - VubAbs V ^ 2 = VudAbs V ^ 2 + VusAbs V ^ 2 := by + linear_combination - (VAbs_sum_sq_row_eq_one V 0) + rw [h1, mul_comm] + exact (mul_div_cancel₀ (VudAbs V) (VAbs_thd_neq_one_sqrt_fst_snd_sq_neq_zero ha)).symm + +lemma VusAbs_eq_S₁₂_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VusAbs V = S₁₂ V * C₁₃ V := by rw [C₁₃, θ₁₃, Real.cos_arcsin, S₁₂, S₁₃] have h1 : 1 - VubAbs V ^ 2 = VudAbs V ^ 2 + VusAbs V ^ 2 := by linear_combination - (VAbs_sum_sq_row_eq_one V 0) @@ -188,107 +257,7 @@ theorem VusAbs_eq_S₁₂_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VusAbs V have h2 := VAbs_thd_neq_one_sqrt_fst_snd_sq_neq_zero ha exact (mul_div_cancel₀ (VusAbs V) h2).symm -theorem VudAbs_eq_C₁₂_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VudAbs V = C₁₂ V * C₁₃ V := by - by_cases ha : VubAbs V = 1 - change VAbs 0 0 V = C₁₂ V * C₁₃ V - rw [VAbs_thd_eq_one_fst_eq_zero ha] - rw [C₁₃, θ₁₃, Real.cos_arcsin, ← VubAbs_eq_S₁₃, ha] - simp - rw [C₁₂_eq_Vud_div_sqrt ha, C₁₃, θ₁₃, Real.cos_arcsin, S₁₃] - have h1 : 1 - VubAbs V ^ 2 = VudAbs V ^ 2 + VusAbs V ^ 2 := by - linear_combination - (VAbs_sum_sq_row_eq_one V 0) - rw [h1, mul_comm] - exact (mul_div_cancel₀ (VudAbs V) (VAbs_thd_neq_one_sqrt_fst_snd_sq_neq_zero ha)).symm - -def S₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := - if VubAbs V = 1 then - VcdAbs V - else - VcbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2) - -lemma S₂₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₂₃ V := by - by_cases ha : VubAbs V = 1 - rw [S₂₃, if_pos ha] - exact VAbs_ge_zero 1 0 V - rw [S₂₃, if_neg ha] - rw [@div_nonneg_iff] - apply Or.inl - apply And.intro - exact VAbs_ge_zero 1 2 V - exact Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2) - -lemma S₂₃_leq_one (V : Quotient CKMMatrixSetoid) : S₂₃ V ≤ 1 := by - by_cases ha : VubAbs V = 1 - rw [S₂₃, if_pos ha] - exact VAbs_leq_one 1 0 V - rw [S₂₃, if_neg ha] - rw [@div_le_one_iff] - by_cases h1 : √(VudAbs V ^ 2 + VusAbs V ^ 2) = 0 - simp [h1] - have h2 := Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2) - rw [le_iff_eq_or_lt] at h2 - have h3 : 0 < √(VudAbs V ^ 2 + VusAbs V ^ 2) := by - cases' h2 with h2 h2 - simp_all - exact h2 - apply Or.inl - simp_all - rw [Real.le_sqrt] - rw [VudAbs_sq_add_VusAbs_sq, ← VcbAbs_sq_add_VtbAbs_sq] - simp - exact sq_nonneg (VAbs 2 2 V) - exact VAbs_ge_zero 1 2 V - exact le_of_lt h3 - -def θ₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₂₃ V) - -lemma S₂₃_eq_sin_θ₂₃ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₂₃ V) = S₂₃ V := - Real.sin_arcsin (le_trans (by simp) (S₂₃_nonneg V)) (S₂₃_leq_one V) - -lemma S₂₃_eq_ℂsin_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.sin (θ₂₃ V) = S₂₃ V := by - rw [← S₂₃_eq_sin_θ₂₃] - simp - -lemma complexAbs_sin_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.sin (θ₂₃ V)) = - sin (θ₂₃ V):= by - rw [S₂₃_eq_ℂsin_θ₂₃, Complex.abs_ofReal] - simp - exact S₂₃_nonneg _ - -lemma S₂₃_of_Vub_eq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₂₃ V = VcdAbs V := by - rw [S₂₃, if_pos ha] - -lemma S₂₃_of_Vub_neq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) : - S₂₃ V = VcbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by - rw [S₂₃, if_neg ha] - -def C₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₂₃ V) - -lemma C₂₃_eq_ℂcos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₂₃ V) = C₂₃ V := by - simp [C₂₃] - -lemma complexAbs_cos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₂₃ V)) = - cos (θ₂₃ V):= by - rw [C₂₃_eq_ℂcos_θ₂₃, Complex.abs_ofReal] - simp - exact Real.cos_arcsin_nonneg _ - -lemma S₂₃_sq_add_C₂₃_sq (V : Quotient CKMMatrixSetoid) : S₂₃ V ^ 2 + C₂₃ V ^ 2 = 1 := by - rw [← S₂₃_eq_sin_θ₂₃ V, C₂₃] - exact Real.sin_sq_add_cos_sq (θ₂₃ V) - -lemma C₂₃_of_Vub_neq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) : - C₂₃ V = VtbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by - rw [C₂₃, θ₂₃, Real.cos_arcsin, S₂₃_of_Vub_neq_one ha, div_pow, Real.sq_sqrt] - rw [VudAbs_sq_add_VusAbs_sq, ← VcbAbs_sq_add_VtbAbs_sq] - rw [one_sub_div] - simp only [VcbAbs, Fin.isValue, VtbAbs, add_sub_cancel_left] - rw [Real.sqrt_div (sq_nonneg (VAbs 2 2 V))] - rw [Real.sqrt_sq (VAbs_ge_zero 2 2 V)] - rw [VcbAbs_sq_add_VtbAbs_sq, ← VudAbs_sq_add_VusAbs_sq ] - exact VAbs_thd_neq_one_fst_snd_sq_neq_zero ha - exact (Left.add_nonneg (sq_nonneg (VAbs 0 0 V)) (sq_nonneg (VAbs 0 1 V))) - +lemma VubAbs_eq_S₁₃ (V : Quotient CKMMatrixSetoid) : VubAbs V = S₁₃ V := rfl lemma VcbAbs_eq_S₂₃_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VcbAbs V = S₂₃ V * C₁₃ V := by by_cases ha : VubAbs V = 1 @@ -308,146 +277,86 @@ lemma VtbAbs_eq_C₂₃_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VtbAbs V = rw [mul_comm] exact (mul_div_cancel₀ (VtbAbs V) (VAbs_thd_neq_one_sqrt_fst_snd_sq_neq_zero ha)).symm +end VAbs -lemma S₁₂_mul_C₂₃_of_Vud_neq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) : - S₁₂ V * C₂₃ V = VusAbs V * VtbAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2) := by - rw [S₁₂, C₂₃_of_Vub_neq_one ha] - rw [@div_mul_div_comm] - rw [Real.mul_self_sqrt] - exact (Left.add_nonneg (sq_nonneg (VAbs 0 0 V)) (sq_nonneg (VAbs 0 1 V))) -lemma C₁₂_mul_S₂₃_mul_S₁₃_of_Vud_neq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) : - C₁₂ V * S₂₃ V * S₁₃ V = VudAbs V * VcbAbs V * VubAbs V / (VudAbs V ^ 2 + VusAbs V ^ 2) := by - rw [C₁₂_eq_Vud_div_sqrt ha, S₂₃_of_Vub_neq_one ha, S₁₃] - rw [@div_mul_div_comm] - rw [Real.mul_self_sqrt (Left.add_nonneg (sq_nonneg (VAbs 0 0 V)) (sq_nonneg (VAbs 0 1 V)))] - exact (mul_div_right_comm (VudAbs V * VcbAbs V) (VubAbs V) (VudAbs V ^ 2 + VusAbs V ^ 2)).symm +namespace Invariant + +lemma mulExpδ₃_sP_inv (V : CKMMatrix) (δ₁₃ : ℝ) : + mulExpδ₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = + sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧) * cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) * cexp (I * δ₁₃) := by + refine mulExpδ₃_sP _ _ _ _ ?_ ?_ ?_ ?_ + rw [S₁₂_eq_sin_θ₁₂] + exact S₁₂_nonneg _ + exact Real.cos_arcsin_nonneg _ + rw [S₂₃_eq_sin_θ₂₃] + exact S₂₃_nonneg _ + exact Real.cos_arcsin_nonneg _ + +lemma mulExpδ₃_eq_zero (V : CKMMatrix) (δ₁₃ : ℝ) : + mulExpδ₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = 0 ↔ + VudAbs ⟦V⟧ = 0 ∨ VubAbs ⟦V⟧ = 0 ∨ VusAbs ⟦V⟧ = 0 ∨ VcbAbs ⟦V⟧ = 0 ∨ VtbAbs ⟦V⟧ = 0 := by + rw [VudAbs_eq_C₁₂_mul_C₁₃, VubAbs_eq_S₁₃, VusAbs_eq_S₁₂_mul_C₁₃, VcbAbs_eq_S₂₃_mul_C₁₃, VtbAbs_eq_C₂₃_mul_C₁₃, + ← ofReal_inj, + ← ofReal_inj, ← ofReal_inj, ← ofReal_inj, ← ofReal_inj] + simp only [ofReal_mul] + rw [← S₁₃_eq_ℂsin_θ₁₃, ← S₁₂_eq_ℂsin_θ₁₂, ← S₂₃_eq_ℂsin_θ₂₃, + ← C₁₃_eq_ℂcos_θ₁₃, ← C₂₃_eq_ℂcos_θ₂₃,← C₁₂_eq_ℂcos_θ₁₂] + rw [mulExpδ₃_sP_inv] + simp + have h1 := exp_ne_zero (I * δ₁₃) + simp_all + aesop + +lemma mulExpδ₃_abs (V : CKMMatrix) (δ₁₃ : ℝ) : + Complex.abs (mulExpδ₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) = + sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧) + * cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) := by + rw [mulExpδ₃_sP_inv] + simp [abs_exp] + rw [complexAbs_sin_θ₁₃, complexAbs_cos_θ₁₃, complexAbs_sin_θ₁₂, complexAbs_cos_θ₁₂, + complexAbs_sin_θ₂₃, complexAbs_cos_θ₂₃] + +lemma mulExpδ₃_neq_zero_arg (V : CKMMatrix) (δ₁₃ : ℝ) + (h1 : mulExpδ₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ ≠ 0 ) : + cexp (arg ( mulExpδ₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ ) * I) = + cexp (δ₁₃ * I) := by + have h1a := mulExpδ₃_sP_inv V δ₁₃ + have habs := mulExpδ₃_abs V δ₁₃ + have h2 : mulExpδ₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = + Complex.abs (mulExpδ₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) * exp (δ₁₃ * I) := by + rw [habs, h1a] + ring_nf + nth_rewrite 1 [← abs_mul_exp_arg_mul_I (mulExpδ₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ )] at h2 + have habs_neq_zero : (Complex.abs (mulExpδ₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) : ℂ) ≠ 0 := by + simp + exact h1 + rw [← mul_right_inj' habs_neq_zero] + rw [← h2] + +end Invariant + +-- to be moved. +lemma cos_θ₁₃_zero {V : Quotient CKMMatrixSetoid} (h1 : Real.cos (θ₁₃ V) = 0) : + VubAbs V = 1 := by + rw [θ₁₃, Real.cos_arcsin, ← VubAbs_eq_S₁₃, Real.sqrt_eq_zero] at h1 + have h2 : VubAbs V ^ 2 = 1 := by linear_combination -(1 * h1) + simp at h2 + cases' h2 with h2 h2 + exact h2 + have h3 := VAbs_ge_zero 0 2 V + rw [h2] at h3 + simp at h3 + linarith + simp + rw [_root_.abs_of_nonneg (VAbs_ge_zero 0 2 V)] + exact VAbs_leq_one 0 2 V -def standardParameterizationAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : Matrix (Fin 3) (Fin 3) ℂ := - ![![Real.cos θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₃ * exp (-I * δ₁₃)], - ![(-Real.sin θ₁₂ * Real.cos θ₂₃) - (Real.cos θ₁₂ * Real.sin θ₁₃ * Real.sin θ₂₃ * exp (I * δ₁₃)), - Real.cos θ₁₂ * Real.cos θ₂₃ - Real.sin θ₁₂ * Real.sin θ₁₃ * Real.sin θ₂₃ * exp (I * δ₁₃), - Real.sin θ₂₃ * Real.cos θ₁₃], - ![Real.sin θ₁₂ * Real.sin θ₂₃ - Real.cos θ₁₂ * Real.sin θ₁₃ * Real.cos θ₂₃ * exp (I * δ₁₃), - (-Real.cos θ₁₂ * Real.sin θ₂₃) - (Real.sin θ₁₂ * Real.sin θ₁₃ * Real.cos θ₂₃ * exp (I * δ₁₃)), - Real.cos θ₂₃ * Real.cos θ₁₃]] open CKMMatrix -lemma standardParameterizationAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : - ((standardParameterizationAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standardParameterizationAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) = 1 := by - funext j i - simp only [standardParameterizationAsMatrix, neg_mul, Fin.isValue] - rw [mul_apply] - have h1 := exp_ne_zero (I * ↑δ₁₃) - fin_cases j <;> rw [Fin.sum_univ_three] - simp only [Fin.zero_eta, Fin.isValue, conjTranspose_apply, cons_val', cons_val_zero, empty_val', - cons_val_fin_one, star_mul', RCLike.star_def, conj_ofReal, cons_val_one, head_cons, star_sub, - star_neg, ← exp_conj, _root_.map_mul, conj_I, neg_mul, cons_val_two, tail_cons, head_fin_const] - simp [conj_ofReal] - rw [exp_neg ] - fin_cases i <;> simp - · ring_nf - field_simp - rw [sin_sq, sin_sq, sin_sq] - ring - · ring_nf - field_simp - rw [sin_sq, sin_sq] - ring - · ring_nf - field_simp - rw [sin_sq] - ring - simp only [Fin.mk_one, Fin.isValue, conjTranspose_apply, cons_val', cons_val_one, head_cons, - empty_val', cons_val_fin_one, cons_val_zero, star_mul', RCLike.star_def, conj_ofReal, star_sub, - ← exp_conj, _root_.map_mul, conj_I, neg_mul, cons_val_two, tail_cons, head_fin_const, star_neg] - simp [conj_ofReal] - rw [exp_neg] - fin_cases i <;> simp - · ring_nf - field_simp - rw [sin_sq, sin_sq] - ring - · ring_nf - field_simp - rw [sin_sq, sin_sq, sin_sq] - ring - · ring_nf - field_simp - rw [sin_sq] - ring - simp only [Fin.reduceFinMk, Fin.isValue, conjTranspose_apply, cons_val', cons_val_two, tail_cons, - head_cons, empty_val', cons_val_fin_one, cons_val_zero, star_mul', RCLike.star_def, conj_ofReal, - ← exp_conj, map_neg, _root_.map_mul, conj_I, neg_mul, neg_neg, cons_val_one, head_fin_const] - simp [conj_ofReal] - rw [exp_neg] - fin_cases i <;> simp - · ring_nf - rw [sin_sq] - ring - · ring_nf - rw [sin_sq] - ring - · ring_nf - field_simp - rw [sin_sq, sin_sq] - ring - -def sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix := - ⟨standardParameterizationAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by - rw [mem_unitaryGroup_iff'] - exact standardParameterizationAsMatrix_unitary θ₁₂ θ₁₃ θ₂₃ δ₁₃⟩ - -lemma sP_cross (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : - [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]t = (conj [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]u ×₃ conj [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) := by - have h1 := exp_ne_zero (I * ↑δ₁₃) - funext i - fin_cases i - · simp only [tRow, sP, standardParameterizationAsMatrix, neg_mul, exp_neg, - Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, tail_cons, - head_fin_const, cons_val_one, head_cons, Fin.zero_eta, crossProduct, uRow, cRow, - LinearMap.mk₂_apply, Pi.conj_apply, _root_.map_mul, map_inv₀, ← exp_conj, conj_I, conj_ofReal, - inv_inv, map_sub, map_neg] - field_simp - ring_nf - rw [sin_sq] - ring - · simp only [tRow, sP, standardParameterizationAsMatrix, neg_mul, exp_neg, Fin.isValue, cons_val', - cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, tail_cons, head_fin_const, - cons_val_one, head_cons, Fin.mk_one, crossProduct, uRow, cRow, LinearMap.mk₂_apply, - Pi.conj_apply, _root_.map_mul, conj_ofReal, map_inv₀, ← exp_conj, conj_I, inv_inv, map_sub, - map_neg] - field_simp - ring_nf - rw [sin_sq] - ring - · simp only [tRow, sP, standardParameterizationAsMatrix, neg_mul, exp_neg, Fin.isValue, - cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, tail_cons, head_fin_const, - cons_val_one, head_cons, Fin.reduceFinMk, crossProduct, uRow, cRow, LinearMap.mk₂_apply, - Pi.conj_apply, _root_.map_mul, conj_ofReal, map_inv₀, ← exp_conj, conj_I, inv_inv, map_sub, - map_neg] - field_simp - ring_nf - rw [sin_sq] - ring - -lemma eq_sP (U : CKMMatrix) {θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ} (hu : [U]u = [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]u) - (hc : [U]c = [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) (hU : [U]t = conj [U]u ×₃ conj [U]c) : - U = sP θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by - apply ext_Rows hu hc - rw [hU, sP_cross, hu, hc] - -lemma eq_phases_sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ δ₁₃' : ℝ) (h : cexp (δ₁₃ * I) = cexp (δ₁₃' * I)) : - sP θ₁₂ θ₁₃ θ₂₃ δ₁₃ = sP θ₁₂ θ₁₃ θ₂₃ δ₁₃' := by - simp [sP, standardParameterizationAsMatrix] - apply CKMMatrix_ext - simp - rw [show exp (I * δ₁₃) = exp (I * δ₁₃') by rw [mul_comm, h, mul_comm]] - rw [show cexp (-(I * ↑δ₁₃)) = cexp (-(I * ↑δ₁₃')) by rw [exp_neg, exp_neg, mul_comm, h, mul_comm]] - section zeroEntries variable (a b c d e f : ℝ) @@ -575,15 +484,9 @@ lemma Vs_zero_iff_cos_sin_zero (V : CKMMatrix) : aesop - - - - - - end zeroEntries -lemma UCond₁_eq_sP {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V]cb ≠ 0) +lemma UCond₁_eq_sP {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (hV : UCond₁ V) : V = sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (- arg [V]ub) := by have hb' : VubAbs ⟦V⟧ ≠ 1 := by rw [ud_us_neq_zero_iff_ub_neq_one] at hb @@ -615,7 +518,7 @@ lemma UCond₁_eq_sP {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V funext i fin_cases i simp [cRow, sP, standardParameterizationAsMatrix] - rw [cd_of_us_or_ud_neq_zero_UCond hb ha hV] + rw [cd_of_us_or_ud_neq_zero_UCond hb hV] rw [S₁₂_eq_ℂsin_θ₁₂ ⟦V⟧, S₁₂, C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₁₂_eq_Vud_div_sqrt hb'] rw [S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, S₂₃_of_Vub_neq_one hb', C₂₃_eq_ℂcos_θ₂₃ ⟦V⟧, C₂₃_of_Vub_neq_one hb', S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃] @@ -628,7 +531,7 @@ lemma UCond₁_eq_sP {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V rw [C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₂₃_eq_ℂcos_θ₂₃ ⟦V⟧, S₁₂_eq_ℂsin_θ₁₂ ⟦V⟧, S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧] rw [C₁₂_eq_Vud_div_sqrt hb', C₂₃_of_Vub_neq_one hb', S₁₂, S₁₃, S₂₃_of_Vub_neq_one hb'] - rw [cs_of_us_or_ud_neq_zero_UCond hb ha hV] + rw [cs_of_us_or_ud_neq_zero_UCond hb hV] field_simp rw [h1] simp [sq] @@ -639,75 +542,6 @@ lemma UCond₁_eq_sP {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V rw [VcbAbs_eq_S₂₃_mul_C₁₃ ⟦V⟧, S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, C₁₃] simp - -lemma UCond₂_eq_sP {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (ha : [V]cb = 0) - (hV : UCond₂ V) : V = sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by - have h23 : S₂₃ ⟦V⟧ = 0 := by - have h1 := VcbAbs_eq_S₂₃_mul_C₁₃ ⟦V⟧ - simp [VAbs] at h1 - rw [ha] at h1 - simp at h1 - cases' h1 with h1 h1 - exact h1 - have h2 : abs [V]ud = 0 := by - change VudAbs ⟦V⟧ = 0 - rw [VudAbs_eq_C₁₂_mul_C₁₃, h1] - simp - have h2b : abs [V]us = 0 := by - change VusAbs ⟦V⟧ = 0 - rw [VusAbs_eq_S₁₂_mul_C₁₃, h1] - simp - simp_all - have h1 : ofReal (√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) * ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) ) - = ofReal ((VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) ) := by - rw [Real.mul_self_sqrt ] - apply add_nonneg (sq_nonneg _) (sq_nonneg _) - have hx := Vabs_sq_add_neq_zero hb - simp at h1 - have hb' : VubAbs ⟦V⟧ ≠ 1 := by - rw [ud_us_neq_zero_iff_ub_neq_one] at hb - simp [VAbs, hb] - refine eq_sP V ?_ ?_ hV.2.2.2.1 - funext i - fin_cases i - simp [uRow, sP, standardParameterizationAsMatrix] - rw [hV.1, VudAbs_eq_C₁₂_mul_C₁₃ ⟦V⟧, C₁₂, C₁₃] - simp - simp [uRow, sP, standardParameterizationAsMatrix] - rw [hV.2.1, VusAbs_eq_S₁₂_mul_C₁₃ ⟦V⟧, ← S₁₂_eq_sin_θ₁₂ ⟦V⟧, C₁₃] - simp - simp [uRow, sP, standardParameterizationAsMatrix] - rw [hV.2.2.1, VubAbs_eq_S₁₃, S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧] - funext i - fin_cases i - simp [cRow, sP, standardParameterizationAsMatrix] - rw [S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, h23] - simp - rw [C₂₃_eq_ℂcos_θ₂₃ ⟦V⟧, C₂₃_of_Vub_neq_one hb'] - rw [S₁₂_eq_ℂsin_θ₁₂ ⟦V⟧, S₁₂] - rw [hV.2.2.2.2.1] - field_simp - rw [h1] - simp [sq] - field_simp - ring_nf - simp - simp [cRow, sP, standardParameterizationAsMatrix] - rw [S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, h23] - simp - rw [C₂₃_eq_ℂcos_θ₂₃ ⟦V⟧, C₂₃_of_Vub_neq_one hb'] - rw [C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₁₂_eq_Vud_div_sqrt hb'] - rw [hV.2.2.2.2.2] - field_simp - rw [h1] - simp [sq] - field_simp - ring_nf - simp [cRow, sP, standardParameterizationAsMatrix] - rw [ha, S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, h23] - simp - - lemma UCond₃_eq_sP {V : CKMMatrix} (hV : UCond₃ V) : V = sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by have h1 : VubAbs ⟦V⟧ = 1 := by simp [VAbs] @@ -750,83 +584,72 @@ lemma UCond₃_eq_sP {V : CKMMatrix} (hV : UCond₃ V) : V = sP (θ₁₂ ⟦V rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.2.1] simp - -theorem exists_standardParameterization (V : CKMMatrix) : +theorem exists_standardParameterization_δ₁₃ (V : CKMMatrix) : ∃ (δ₃ : ℝ), V ≈ sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₃ := by obtain ⟨U, hU⟩ := all_eq_abs V have hUV : ⟦U⟧ = ⟦V⟧ := (Quotient.eq.mpr (phaseShiftEquivRelation.symm hU.1)) by_cases ha : [V]ud ≠ 0 ∨ [V]us ≠ 0 - have haU : [U]ud ≠ 0 ∨ [U]us ≠ 0 := by - by_contra hn - simp [not_or] at hn - have hna : VudAbs ⟦U⟧ = 0 ∧ VusAbs ⟦U⟧ =0 := by - simp [VAbs] - exact hn - rw [hUV] at hna - simp [VAbs] at hna - simp_all - by_cases hb : [V]cb ≠ 0 - have hbU : [U]cb ≠ 0 := by - by_contra hn - simp at hn - have hna : VcbAbs ⟦U⟧ = 0 := by - simp [VAbs] - exact hn - rw [hUV] at hna - simp [VAbs] at hna - simp_all - have hU' := UCond₁_eq_sP haU hbU hU.2 - rw [hU'] at hU - use (- arg ([U]ub)) - rw [← hUV] - exact hU.1 - simp at hb - have hbU : [U]cb = 0 := by - have hna : VcbAbs ⟦U⟧ = 0 := by - rw [hUV] - simp [VAbs] - exact hb - simpa [VAbs] using hna - obtain ⟨U2, hU2⟩ := UCond₂_exists haU hbU hU.2 - have hUVa2 : V ≈ U2 := phaseShiftEquivRelation.trans hU.1 hU2.1 - have hUV2 : ⟦U2⟧ = ⟦V⟧ := (Quotient.eq.mpr (phaseShiftEquivRelation.symm hUVa2)) - have haU2 : [U2]ud ≠ 0 ∨ [U2]us ≠ 0 := by - by_contra hn - simp [not_or] at hn - have hna : VudAbs ⟦U2⟧ = 0 ∧ VusAbs ⟦U2⟧ =0 := by - simp [VAbs] - exact hn - rw [hUV2] at hna - simp [VAbs] at hna - simp_all - have hbU2 : [U2]cb = 0 := by - have hna : VcbAbs ⟦U2⟧ = 0 := by - rw [hUV2] - simp [VAbs] - exact hb - simpa [VAbs] using hna - have hU2' := UCond₂_eq_sP haU2 hbU2 hU2.2 - use 0 - rw [← hUV2, ← hU2'] - exact hUVa2 - have haU : ¬ ([U]ud ≠ 0 ∨ [U]us ≠ 0) := by - simp [not_or] at ha - have h1 : VudAbs ⟦U⟧ = 0 ∧ VusAbs ⟦U⟧ = 0 := by - rw [hUV] - simp [VAbs] - exact ha - simpa [not_or, VAbs] using h1 - have ⟨U2, hU2⟩ := UCond₃_exists haU hU.2 - have hUVa2 : V ≈ U2 := phaseShiftEquivRelation.trans hU.1 hU2.1 - have hUV2 : ⟦U2⟧ = ⟦V⟧ := (Quotient.eq.mpr (phaseShiftEquivRelation.symm hUVa2)) - have hx := UCond₃_eq_sP hU2.2 - use 0 - rw [← hUV2, ← hx] - exact hUVa2 - - - + · have haU : [U]ud ≠ 0 ∨ [U]us ≠ 0 := by -- should be much simplier + by_contra hn + simp [not_or] at hn + have hna : VudAbs ⟦U⟧ = 0 ∧ VusAbs ⟦U⟧ =0 := by + simp [VAbs] + exact hn + rw [hUV] at hna + simp [VAbs] at hna + simp_all + have hU' := UCond₁_eq_sP haU hU.2 + rw [hU'] at hU + use (- arg ([U]ub)) + rw [← hUV] + exact hU.1 + · have haU : ¬ ([U]ud ≠ 0 ∨ [U]us ≠ 0) := by -- should be much simplier + simp [not_or] at ha + have h1 : VudAbs ⟦U⟧ = 0 ∧ VusAbs ⟦U⟧ = 0 := by + rw [hUV] + simp [VAbs] + exact ha + simpa [not_or, VAbs] using h1 + have ⟨U2, hU2⟩ := UCond₃_exists haU hU.2 + have hUVa2 : V ≈ U2 := phaseShiftEquivRelation.trans hU.1 hU2.1 + have hUV2 : ⟦U2⟧ = ⟦V⟧ := (Quotient.eq.mpr (phaseShiftEquivRelation.symm hUVa2)) + have hx := UCond₃_eq_sP hU2.2 + use 0 + rw [← hUV2, ← hx] + exact hUVa2 +open Invariant in +theorem eq_standardParameterization_δ₃ (V : CKMMatrix) : + V ≈ sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (δ₁₃ ⟦V⟧) := by + obtain ⟨δ₁₃', hδ₃⟩ := exists_standardParameterization_δ₁₃ V + have hSV := (Quotient.eq.mpr (hδ₃)) + by_cases h : Invariant.mulExpδ₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃'⟧ ≠ 0 + have h1 := Invariant.mulExpδ₃_neq_zero_arg V δ₁₃' h + have h2 := eq_phases_sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃' + (δ₁₃ ⟦V⟧) (by rw [← h1, ← hSV, δ₁₃, Invariant.mulExpδ₃]) + rw [h2] at hδ₃ + exact hδ₃ + simp at h + have h1 : δ₁₃ ⟦V⟧ = 0 := by + rw [hSV, δ₁₃, h] + simp + rw [h1] + rw [mulExpδ₃_eq_zero, Vs_zero_iff_cos_sin_zero] at h + cases' h with h h + exact phaseShiftEquivRelation.trans hδ₃ (sP_cos_θ₁₂_eq_zero δ₁₃' h ) + cases' h with h h + exact phaseShiftEquivRelation.trans hδ₃ (sP_cos_θ₁₃_eq_zero δ₁₃' h ) + cases' h with h h + exact phaseShiftEquivRelation.trans hδ₃ (sP_cos_θ₂₃_eq_zero δ₁₃' h ) + cases' h with h h + exact phaseShiftEquivRelation.trans hδ₃ (sP_sin_θ₁₂_eq_zero δ₁₃' h ) + cases' h with h h + exact phaseShiftEquivRelation.trans hδ₃ (sP_sin_θ₁₃_eq_zero δ₁₃' h ) + exact phaseShiftEquivRelation.trans hδ₃ (sP_sin_θ₂₃_eq_zero δ₁₃' h ) +lemma exists_standardParameterization (V : CKMMatrix) : + ∃ (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ), V ≈ sP θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by + use θ₁₂ ⟦V⟧, θ₁₃ ⟦V⟧, θ₂₃ ⟦V⟧, δ₁₃ ⟦V⟧ + exact eq_standardParameterization_δ₃ V end