diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean index 7016dcc..b68eb9d 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean @@ -273,11 +273,10 @@ open ComplexConjugate 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 @@ -289,7 +288,7 @@ 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 @@ -298,7 +297,6 @@ lemma Rcdcb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cd = Rcdcb V * [V]cb := 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 diff --git a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean index 0c2f26d..5ce5d0c 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean @@ -43,7 +43,7 @@ def jarlskogℂ : Quotient CKMMatrixSetoid → ℂ := 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) : ℂ := +def mulExpδ₁₃ (V : Quotient CKMMatrixSetoid) : ℂ := jarlskogℂ V + VusVubVcdSq V diff --git a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean index 0a5136b..d29ef77 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean @@ -19,7 +19,7 @@ open ComplexConjugate section phaseShiftApply variable (u c t d s b : ℝ) -lemma ud_eq_abs (V : CKMMatrix) (h1 : u + d = - arg [V]ud) : +lemma shift_ud_phase_zero (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] @@ -31,7 +31,7 @@ lemma ud_eq_abs (V : CKMMatrix) (h1 : u + d = - arg [V]ud) : simp rfl -lemma us_eq_abs {V : CKMMatrix} (h1 : u + s = - arg [V]us) : +lemma shift_us_phase_zero {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] @@ -43,7 +43,7 @@ lemma us_eq_abs {V : CKMMatrix} (h1 : u + s = - arg [V]us) : simp rfl -lemma ub_eq_abs {V : CKMMatrix} (h1 : u + b = - arg [V]ub) : +lemma shift_ub_phase_zero {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] @@ -55,7 +55,7 @@ lemma ub_eq_abs {V : CKMMatrix} (h1 : u + b = - arg [V]ub) : simp rfl -lemma cs_eq_abs {V : CKMMatrix} (h1 : c + s = - arg [V]cs) : +lemma shift_cs_phase_zero {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] @@ -67,7 +67,7 @@ lemma cs_eq_abs {V : CKMMatrix} (h1 : c + s = - arg [V]cs) : simp rfl -lemma cb_eq_abs {V : CKMMatrix} (h1 : c + b = - arg [V]cb) : +lemma shift_cb_phase_zero {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] @@ -79,7 +79,7 @@ lemma cb_eq_abs {V : CKMMatrix} (h1 : c + b = - arg [V]cb) : simp rfl -lemma tb_eq_abs {V : CKMMatrix} (h1 : t + b = - arg [V]tb) : +lemma shift_tb_phase_zero {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] @@ -91,7 +91,7 @@ lemma tb_eq_abs {V : CKMMatrix} (h1 : t + b = - arg [V]tb) : simp rfl -lemma cd_eq_neg_abs {V : CKMMatrix} (h1 : c + d = Real.pi - arg [V]cd) : +lemma shift_cd_phase_pi {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] @@ -103,8 +103,8 @@ lemma cd_eq_neg_abs {V : CKMMatrix} (h1 : c + d = Real.pi - arg [V]cd) : simp rfl -lemma t_eq_conj {V : CKMMatrix} {τ : ℝ} (hτ : cexp (τ * I) • (conj [V]u ×₃ conj [V]c) = [V]t) - (h1 : τ = - u - c - t - d - s - b) : +lemma shift_cross_product_phase_zero {V : CKMMatrix} {τ : ℝ} + (hτ : cexp (τ * I) • (conj [V]u ×₃ conj [V]c) = [V]t) (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 _ _ _ _ _ _ _ @@ -146,16 +146,17 @@ end phaseShiftApply variable (a b c d e f : ℝ) -- rename -def UCond₁ (U : CKMMatrix) : Prop := [U]ud = VudAbs ⟦U⟧ ∧ [U]us = VusAbs ⟦U⟧ +def fstRowThdColRealCond (U : CKMMatrix) : Prop := [U]ud = VudAbs ⟦U⟧ ∧ [U]us = VusAbs ⟦U⟧ ∧ [U]cb = VcbAbs ⟦U⟧ ∧ [U]tb = VtbAbs ⟦U⟧ ∧ [U]t = conj [U]u ×₃ conj [U]c -- rename -def UCond₃ (U : CKMMatrix) : Prop := +def ubOnePhaseCond (U : CKMMatrix) : Prop := [U]ud = 0 ∧ [U]us = 0 ∧ [U]cb = 0 ∧ [U]ub = 1 ∧ [U]t = conj [U]u ×₃ conj [U]c ∧ [U]cd = - VcdAbs ⟦U⟧ ∧ [U]cs = √(1 - VcdAbs ⟦U⟧ ^ 2) -- 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) +lemma fstRowThdColRealCond_shift_solution {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) : b = - τ + arg [V]ud + arg [V]us + arg [V]tb + a ∧ c = - τ + arg [V]cb + arg [V]ud + arg [V]us + a ∧ @@ -184,7 +185,8 @@ lemma all_cond_sol {V : CKMMatrix} (h1 : a + d = - arg [V]ud) (h2 : a + e = - a ring_nf simp -lemma UCond₃_solv {V : CKMMatrix} (h1 : a + f = - arg [V]ub) (h2 : 0 = - a - b - c - d - e - f) +lemma ubOnePhaseCond_shift_solution {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 ∧ @@ -206,8 +208,8 @@ lemma UCond₃_solv {V : CKMMatrix} (h1 : a + f = - arg [V]ub) (h2 : 0 = - a - b ring -- rename -lemma all_eq_abs (V : CKMMatrix) : - ∃ (U : CKMMatrix), V ≈ U ∧ UCond₁ U:= by +lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) : + ∃ (U : CKMMatrix), V ≈ U ∧ fstRowThdColRealCond U:= by obtain ⟨τ, hτ⟩ := V.uRow_cross_cRow_eq_tRow let U : CKMMatrix := phaseShiftApply V 0 @@ -225,26 +227,27 @@ lemma all_eq_abs (V : CKMMatrix) : exact phaseShiftApply.equiv _ _ _ _ _ _ _ apply And.intro rw [hUV] - apply ud_eq_abs _ _ _ _ _ _ _ + apply shift_ud_phase_zero _ _ _ _ _ _ _ ring apply And.intro rw [hUV] - apply us_eq_abs + apply shift_us_phase_zero ring apply And.intro rw [hUV] - apply cb_eq_abs + apply shift_cb_phase_zero ring apply And.intro rw [hUV] - apply tb_eq_abs + apply shift_tb_phase_zero ring - apply t_eq_conj _ _ _ _ _ _ hτ.symm + apply shift_cross_product_phase_zero _ _ _ _ _ _ hτ.symm ring -lemma UCond₃_exists {V : CKMMatrix} (hb :¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) (hV : UCond₁ V) : - ∃ (U : CKMMatrix), V ≈ U ∧ UCond₃ U:= by +lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) + (hV : fstRowThdColRealCond V) : + ∃ (U : CKMMatrix), V ≈ U ∧ ubOnePhaseCond 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 @@ -278,7 +281,7 @@ lemma UCond₃_exists {V : CKMMatrix} (hb :¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) (hV exact h1 apply And.intro · have hU1 : [U]ub = VubAbs ⟦V⟧ := by - apply ub_eq_abs _ _ _ _ _ _ _ + apply shift_ub_phase_zero _ _ _ _ _ _ _ ring rw [hU1] have h1:= (ud_us_neq_zero_iff_ub_neq_one V).mpr.mt hb @@ -287,21 +290,21 @@ lemma UCond₃_exists {V : CKMMatrix} (hb :¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) (hV · 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 + apply shift_cross_product_phase_zero _ _ _ _ _ _ hτ.symm ring apply And.intro · rw [hUV] - apply cd_eq_neg_abs _ _ _ _ _ _ _ + apply shift_cd_phase_pi _ _ _ _ _ _ _ ring have hcs : [U]cs = VcsAbs ⟦U⟧ := by rw [hUV] - apply cs_eq_abs _ _ _ _ _ _ _ + apply shift_cs_phase_zero _ _ _ _ _ _ _ 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)) + +lemma cd_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) + (hV : fstRowThdColRealCond 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 @@ -319,8 +322,8 @@ lemma cd_of_us_or_ud_neq_zero_UCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us 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)) +lemma cs_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) + (hV : fstRowThdColRealCond 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 diff --git a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean index 6384225..5fc5c75 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean @@ -60,6 +60,8 @@ 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 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) lemma ud_us_neq_zero_iff_ub_neq_one (V : CKMMatrix) : [V]ud ≠ 0 ∨ [V]us ≠ 0 ↔ abs [V]ub ≠ 1 := by @@ -105,56 +107,38 @@ lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℂ {V : CKMMatrix} (hb : [V]ud ≠ 0 simp_all +lemma Vabs_sq_add_neq_zero {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) : + ((VudAbs ⟦V⟧ : ℂ) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧)) ≠ 0 := by + have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℂ hb + rw [← Complex.sq_abs, ← Complex.sq_abs] at h1 + simp [sq] at h1 + exact h1 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 +lemma fst_row_orthog_snd_row (V : CKMMatrix) : + [V]cd * conj [V]ud + [V]cs * conj [V]us + [V]cb * conj [V]ub = 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 +lemma fst_row_orthog_thd_row (V : CKMMatrix) : + [V]td * conj [V]ud + [V]ts * conj [V]us + [V]tb * conj [V]ub = 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) : +lemma Vcd_mul_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 ) + linear_combination (V.fst_row_orthog_snd_row ) -lemma Vcs_conj_Vus (V : CKMMatrix) : +lemma Vcs_mul_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] + linear_combination (V.fst_row_orthog_snd_row ) end orthogonal @@ -174,7 +158,7 @@ lemma VAbs_thd_eq_one_snd_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} (hV section crossProduct -lemma conj_Vtb_other {V : CKMMatrix} {τ : ℝ} +lemma conj_Vtb_cross_product {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 @@ -189,36 +173,34 @@ lemma conj_Vtb_other {V : CKMMatrix} {τ : ℝ} end crossProduct - -lemma conj_Vtb_Vud_other {V : CKMMatrix} {τ : ℝ} +lemma conj_Vtb_mul_Vud {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τ] + rw [conj_Vtb_cross_product 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 [h2, V.Vcd_mul_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} {τ : ℝ} +lemma conj_Vtb_mul_Vus {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τ] + rw [conj_Vtb_cross_product 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 [h2, V.Vcs_mul_conj_Vus] rw [normSq_eq_conj_mul_self, normSq_eq_conj_mul_self] simp ring @@ -229,7 +211,7 @@ lemma cs_of_ud_us_ub_cb_tb {V : CKMMatrix} (h : [V]ud ≠ 0 ∨ [V]us ≠ 0) [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τ] + rw [conj_Vtb_mul_Vud hτ] field_simp ring @@ -238,47 +220,12 @@ lemma cd_of_ud_us_ub_cb_tb {V : CKMMatrix} (h : [V]ud ≠ 0 ∨ [V]us ≠ 0) [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τ] + rw [conj_Vtb_mul_Vus 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 @@ -287,7 +234,6 @@ lemma VAbs_ge_zero (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : 0 ≤ VAbs i 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 @@ -301,6 +247,25 @@ lemma VAbs_leq_one (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : VAbs i j V ≤ end individual +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 + section columns @@ -360,9 +325,9 @@ lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) : exact hn.trans h0 exact VAbs_ge_zero _ _ ⟦V⟧ -end columns - - +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) @@ -388,47 +353,6 @@ lemma cb_tb_neq_zero_iff_ub_neq_one (V : CKMMatrix) : have h2 : ¬ 0 ≤ ( -1 : ℝ) := by simp exact h2 h1 -lemma tb_neq_zero_of_cb_zero_ud_us_neq_zero {V : CKMMatrix} (h : [V]cb = 0) - (h1 : [V]ud ≠ 0 ∨ [V]us ≠ 0) : [V]tb ≠ 0 := by - rw [ud_us_neq_zero_iff_ub_neq_one] at h1 - rw [← cb_tb_neq_zero_iff_ub_neq_one] at h1 - simp_all - - - - -lemma normSq_tb_of_cb_zero {V : CKMMatrix} (h : [V]cb = 0) : normSq [V]tb = - normSq [V]ud + normSq [V]us := by - have h1 := fst_row_normalized_normSq V - rw [← thd_col_normalized_normSq V] at h1 - rw [h] at h1 - simp at h1 - linear_combination -(1 * h1) - - -lemma div_td_of_cb_zero_ud_us_neq_zero {V : CKMMatrix} (h : [V]cb = 0) - (h1 : [V]ud ≠ 0 ∨ [V]us ≠ 0) (a : ℂ) : a / [V]tb = - (a * conj [V]tb) / (normSq [V]ud + normSq [V]us) := by - have h2 := tb_neq_zero_of_cb_zero_ud_us_neq_zero h h1 - have h3 : conj [V]tb ≠ 0 := (AddEquivClass.map_ne_zero_iff starRingAut).mpr h2 - have h1 : a / [V]tb = a * conj [V]tb / normSq [V]tb := by - rw [normSq_eq_conj_mul_self] - field_simp - ring - rw [normSq_tb_of_cb_zero h] at h1 - simp at h1 - exact h1 - - -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 - have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℂ hb - rw [← Complex.sq_abs, ← Complex.sq_abs] at h1 - simp [sq] at h1 - 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 @@ -443,31 +367,7 @@ lemma VAbs_fst_col_eq_one_thd_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} 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 columns end CKMMatrix end diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean index b02b5e2..4bccf33 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean @@ -16,7 +16,7 @@ open CKMMatrix noncomputable section -- to be renamed stanParamAsMatrix ... -def standardParameterizationAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : Matrix (Fin 3) (Fin 3) ℂ := +def standParamAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : 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 * δ₁₃), @@ -27,10 +27,10 @@ def standardParameterizationAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) open CKMMatrix -lemma standardParameterizationAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : - ((standardParameterizationAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standardParameterizationAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) = 1 := by +lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : + ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) = 1 := by funext j i - simp only [standardParameterizationAsMatrix, neg_mul, Fin.isValue] + simp only [standParamAsMatrix, neg_mul, Fin.isValue] rw [mul_apply] have h1 := exp_ne_zero (I * ↑δ₁₃) fin_cases j <;> rw [Fin.sum_univ_three] @@ -87,17 +87,19 @@ lemma standardParameterizationAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ rw [sin_sq, sin_sq] ring -def sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix := - ⟨standardParameterizationAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by +def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix := + ⟨standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by rw [mem_unitaryGroup_iff'] - exact standardParameterizationAsMatrix_unitary θ₁₂ θ₁₃ θ₂₃ δ₁₃⟩ + exact standParamAsMatrix_unitary θ₁₂ θ₁₃ θ₂₃ δ₁₃⟩ -lemma sP_cross (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : - [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]t = (conj [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]u ×₃ conj [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) := by +namespace standParam +lemma cross_product_t (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : + [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t = + (conj [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u ×₃ conj [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) := by have h1 := exp_ne_zero (I * ↑δ₁₃) funext i fin_cases i - · simp only [tRow, sP, standardParameterizationAsMatrix, neg_mul, exp_neg, + · simp only [tRow, standParam, standParamAsMatrix, 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, @@ -106,7 +108,7 @@ lemma sP_cross (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : ring_nf rw [sin_sq] ring - · simp only [tRow, sP, standardParameterizationAsMatrix, neg_mul, exp_neg, Fin.isValue, cons_val', + · simp only [tRow, standParam, standParamAsMatrix, 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, @@ -115,7 +117,7 @@ lemma sP_cross (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : ring_nf rw [sin_sq] ring - · simp only [tRow, sP, standardParameterizationAsMatrix, neg_mul, exp_neg, Fin.isValue, + · simp only [tRow, standParam, standParamAsMatrix, 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, @@ -125,27 +127,26 @@ lemma sP_cross (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : 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 +lemma eq_rows (U : CKMMatrix) {θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ} (hu : [U]u = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u) + (hc : [U]c = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) (hU : [U]t = conj [U]u ×₃ conj [U]c) : + U = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by apply ext_Rows hu hc - rw [hU, sP_cross, hu, hc] + rw [hU, cross_product_t, hu, hc] -lemma eq_phases_sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ δ₁₃' : ℝ) (h : cexp (δ₁₃ * I) = cexp (δ₁₃' * I)) : - sP θ₁₂ θ₁₃ θ₂₃ δ₁₃ = sP θ₁₂ θ₁₃ θ₂₃ δ₁₃' := by - simp [sP, standardParameterizationAsMatrix] +lemma eq_exp_of_phases (θ₁₂ θ₁₃ θ₂₃ δ₁₃ δ₁₃' : ℝ) (h : cexp (δ₁₃ * I) = cexp (δ₁₃' * I)) : + standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃' := by + simp [standParam, standParamAsMatrix] 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 θ₁₂) +open Invariant in +lemma VusVubVcdSq_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂) (h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) : - VusVubVcdSq ⟦sP θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ = + VusVubVcdSq ⟦standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ = Real.sin θ₁₂ ^ 2 * Real.cos θ₁₃ ^ 2 * Real.sin θ₁₃ ^ 2 * Real.sin θ₂₃ ^ 2 := by - simp only [VusVubVcdSq, VusAbs, VAbs, VAbs', Fin.isValue, sP, standardParameterizationAsMatrix, + simp only [VusVubVcdSq, VusAbs, VAbs, VAbs', Fin.isValue, standParam, standParamAsMatrix, 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] @@ -164,12 +165,13 @@ lemma VusVubVcdSq_sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Rea rw [hx] simp -lemma mulExpδ₃_sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂) +open Invariant in +lemma mulExpδ₁₃_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂) (h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) : - mulExpδ₃ ⟦sP θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ = + mulExpδ₁₃ ⟦standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ = 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, + rw [mulExpδ₁₃, VusVubVcdSq_eq _ _ _ _ h1 h2 h3 h4 ] + simp only [jarlskogℂ, standParam, standParamAsMatrix, 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] @@ -179,6 +181,7 @@ lemma mulExpδ₃_sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Rea have h1 : cexp (I * δ₁₃) ≠ 0 := exp_ne_zero _ field_simp -end Invariant + +end standParam end diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean index d19866b..139d373 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean @@ -37,7 +37,7 @@ def C₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₁₃ V) def C₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₂₃ V) def δ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := - arg (Invariant.mulExpδ₃ V) + arg (Invariant.mulExpδ₁₃ V) section sines @@ -277,67 +277,7 @@ 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 - - -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) : +lemma VubAbs_of_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) @@ -352,128 +292,6 @@ lemma cos_θ₁₃_zero {V : Quotient CKMMatrixSetoid} (h1 : Real.cos (θ₁₃ rw [_root_.abs_of_nonneg (VAbs_ge_zero 0 2 V)] exact VAbs_leq_one 0 2 V - - - -open CKMMatrix - -section zeroEntries -variable (a b c d e f : ℝ) - -lemma sP_cos_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₃ ⟦V⟧) = 0) : - sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by - have hS13 := congrArg ofReal (S₁₃_of_Vub_one (cos_θ₁₃_zero h)) - simp [← S₁₃_eq_ℂsin_θ₁₃] at hS13 - have hC12 := congrArg ofReal (C₁₂_of_Vub_one (cos_θ₁₃_zero h)) - simp [← C₁₂_eq_ℂcos_θ₁₂] at hC12 - have hS12 := congrArg ofReal (S₁₂_of_Vub_one (cos_θ₁₃_zero h)) - simp [← S₁₂_eq_ℂsin_θ₁₂] at hS12 - use 0, 0, 0, δ₁₃, 0, -δ₁₃ - simp [sP, standardParameterizationAsMatrix, h, phaseShift, hS13, hC12, hS12] - funext i j - fin_cases i <;> fin_cases j <;> - simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three] - rfl - rfl - -lemma sP_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₂ ⟦V⟧) = 0) : - sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by - use 0, δ₁₃, δ₁₃, -δ₁₃, 0, - δ₁₃ - have hb := exp_ne_zero (I * δ₁₃) - simp [sP, standardParameterizationAsMatrix, h, phaseShift, exp_neg] - funext i j - fin_cases i <;> fin_cases j <;> - simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three] - apply Or.inr - rfl - change _ = _ + _ * 0 - simp - field_simp - ring - ring - field_simp - ring - change _ = _ + _ * 0 - simp - field_simp - ring - ring - field_simp - ring - -lemma sP_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₂₃ ⟦V⟧) = 0) : - sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by - use 0, δ₁₃, 0, 0, 0, - δ₁₃ - have hb := exp_ne_zero (I * δ₁₃) - simp [sP, standardParameterizationAsMatrix, h, phaseShift, exp_neg] - funext i j - fin_cases i <;> fin_cases j <;> - simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three] - apply Or.inr - rfl - ring_nf - change _ = _ + _ * 0 - simp - ring - field_simp - ring - -lemma sP_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₃ ⟦V⟧) = 0) : - sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by - use 0, 0, 0, 0, 0, 0 - simp [sP, standardParameterizationAsMatrix, h, phaseShift, exp_neg] - funext i j - fin_cases i <;> fin_cases j <;> - simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three] - apply Or.inr - rfl - apply Or.inr - rfl - -lemma sP_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₂ ⟦V⟧) = 0) : - sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by - use 0, δ₁₃, δ₁₃, 0, -δ₁₃, - δ₁₃ - have hb := exp_ne_zero (I * δ₁₃) - simp [sP, standardParameterizationAsMatrix, h, phaseShift, exp_neg] - funext i j - fin_cases i <;> fin_cases j <;> - simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three] - apply Or.inr - rfl - change _ = _ + _ * 0 - simp - ring - field_simp - ring - field_simp - ring - change _ = _ + _ * 0 - simp - ring - field_simp - ring - field_simp - ring - - -lemma sP_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₂₃ ⟦V⟧) = 0) : - sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by - use 0, 0, δ₁₃, 0, 0, - δ₁₃ - have hb := exp_ne_zero (I * δ₁₃) - simp [sP, standardParameterizationAsMatrix, h, phaseShift, exp_neg] - funext i j - fin_cases i <;> fin_cases j <;> - simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three] - apply Or.inr - rfl - change _ = _ + _ * 0 - simp - ring - ring - field_simp - ring - - lemma Vs_zero_iff_cos_sin_zero (V : CKMMatrix) : VudAbs ⟦V⟧ = 0 ∨ VubAbs ⟦V⟧ = 0 ∨ VusAbs ⟦V⟧ = 0 ∨ VcbAbs ⟦V⟧ = 0 ∨ VtbAbs ⟦V⟧ = 0 ↔ Real.cos (θ₁₂ ⟦V⟧) = 0 ∨ Real.cos (θ₁₃ ⟦V⟧) = 0 ∨ Real.cos (θ₂₃ ⟦V⟧) = 0 ∨ @@ -483,11 +301,182 @@ lemma Vs_zero_iff_cos_sin_zero (V : CKMMatrix) : rw [C₁₂, C₁₃, C₂₃, S₁₂_eq_sin_θ₁₂, S₂₃_eq_sin_θ₂₃, S₁₃_eq_sin_θ₁₃] aesop +end VAbs -end zeroEntries -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 +namespace standParam +open Invariant + +lemma mulExpδ₁₃_on_param_δ₁₃ (V : CKMMatrix) (δ₁₃ : ℝ) : + mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = + sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧) * cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) * cexp (I * δ₁₃) := by + refine mulExpδ₁₃_eq _ _ _ _ ?_ ?_ ?_ ?_ + 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δ₁₃_on_param_eq_zero_iff (V : CKMMatrix) (δ₁₃ : ℝ) : + mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦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δ₁₃_on_param_δ₁₃] + simp + have h1 := exp_ne_zero (I * δ₁₃) + simp_all + aesop + +lemma mulExpδ₁₃_on_param_abs (V : CKMMatrix) (δ₁₃ : ℝ) : + Complex.abs (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) = + sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧) + * cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) := by + rw [mulExpδ₁₃_on_param_δ₁₃] + simp [abs_exp] + rw [complexAbs_sin_θ₁₃, complexAbs_cos_θ₁₃, complexAbs_sin_θ₁₂, complexAbs_cos_θ₁₂, + complexAbs_sin_θ₂₃, complexAbs_cos_θ₂₃] + +lemma mulExpδ₁₃_on_param_neq_zero_arg (V : CKMMatrix) (δ₁₃ : ℝ) + (h1 : mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ ≠ 0 ) : + cexp (arg ( mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ ) * I) = + cexp (δ₁₃ * I) := by + have h1a := mulExpδ₁₃_on_param_δ₁₃ V δ₁₃ + have habs := mulExpδ₁₃_on_param_abs V δ₁₃ + have h2 : mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = + Complex.abs (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) * exp (δ₁₃ * I) := by + rw [habs, h1a] + ring_nf + nth_rewrite 1 [← abs_mul_exp_arg_mul_I (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ )] at h2 + have habs_neq_zero : (Complex.abs (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) : ℂ) ≠ 0 := by + simp + exact h1 + rw [← mul_right_inj' habs_neq_zero] + rw [← h2] + +lemma on_param_cos_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₃ ⟦V⟧) = 0) : + standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by + have hS13 := congrArg ofReal (S₁₃_of_Vub_one (VubAbs_of_cos_θ₁₃_zero h)) + simp [← S₁₃_eq_ℂsin_θ₁₃] at hS13 + have hC12 := congrArg ofReal (C₁₂_of_Vub_one (VubAbs_of_cos_θ₁₃_zero h)) + simp [← C₁₂_eq_ℂcos_θ₁₂] at hC12 + have hS12 := congrArg ofReal (S₁₂_of_Vub_one (VubAbs_of_cos_θ₁₃_zero h)) + simp [← S₁₂_eq_ℂsin_θ₁₂] at hS12 + use 0, 0, 0, δ₁₃, 0, -δ₁₃ + simp [standParam, standParamAsMatrix, h, phaseShift, hS13, hC12, hS12] + funext i j + fin_cases i <;> fin_cases j <;> + simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three] + rfl + rfl + + +lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₂ ⟦V⟧) = 0) : + standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by + use 0, δ₁₃, δ₁₃, -δ₁₃, 0, - δ₁₃ + have hb := exp_ne_zero (I * δ₁₃) + simp [standParam, standParamAsMatrix, h, phaseShift, exp_neg] + funext i j + fin_cases i <;> fin_cases j <;> + simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three] + apply Or.inr + rfl + change _ = _ + _ * 0 + simp + field_simp + ring + ring + field_simp + ring + change _ = _ + _ * 0 + simp + field_simp + ring + ring + field_simp + ring + +lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₂₃ ⟦V⟧) = 0) : + standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by + use 0, δ₁₃, 0, 0, 0, - δ₁₃ + have hb := exp_ne_zero (I * δ₁₃) + simp [standParam, standParamAsMatrix, h, phaseShift, exp_neg] + funext i j + fin_cases i <;> fin_cases j <;> + simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three] + apply Or.inr + rfl + ring_nf + change _ = _ + _ * 0 + simp + ring + field_simp + ring + +lemma on_param_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₃ ⟦V⟧) = 0) : + standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by + use 0, 0, 0, 0, 0, 0 + simp [standParam, standParamAsMatrix, h, phaseShift, exp_neg] + funext i j + fin_cases i <;> fin_cases j <;> + simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three] + apply Or.inr + rfl + apply Or.inr + rfl + +lemma on_param_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₂ ⟦V⟧) = 0) : + standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by + use 0, δ₁₃, δ₁₃, 0, -δ₁₃, - δ₁₃ + have hb := exp_ne_zero (I * δ₁₃) + simp [standParam, standParamAsMatrix, h, phaseShift, exp_neg] + funext i j + fin_cases i <;> fin_cases j <;> + simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three] + apply Or.inr + rfl + change _ = _ + _ * 0 + simp + ring + field_simp + ring + field_simp + ring + change _ = _ + _ * 0 + simp + ring + field_simp + ring + field_simp + ring + + +lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₂₃ ⟦V⟧) = 0) : + standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by + use 0, 0, δ₁₃, 0, 0, - δ₁₃ + have hb := exp_ne_zero (I * δ₁₃) + simp [standParam, standParamAsMatrix, h, phaseShift, exp_neg] + funext i j + fin_cases i <;> fin_cases j <;> + simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three] + apply Or.inr + rfl + change _ = _ + _ * 0 + simp + ring + ring + field_simp + ring + + + +lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) + (hV : fstRowThdColRealCond V) : V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (- arg [V]ub) := by have hb' : VubAbs ⟦V⟧ ≠ 1 := by rw [ud_us_neq_zero_iff_ub_neq_one] at hb simp [VAbs, hb] @@ -497,18 +486,18 @@ lemma UCond₁_eq_sP {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) apply add_nonneg (sq_nonneg _) (sq_nonneg _) simp at h1 have hx := Vabs_sq_add_neq_zero hb - refine eq_sP V ?_ ?_ hV.2.2.2.2 + refine eq_rows V ?_ ?_ hV.2.2.2.2 funext i fin_cases i - simp only [uRow, Fin.isValue, Fin.zero_eta, cons_val_zero, sP, standardParameterizationAsMatrix, + simp only [uRow, Fin.isValue, Fin.zero_eta, cons_val_zero, standParam, standParamAsMatrix, ofReal_cos, ofReal_sin, ofReal_neg, mul_neg, neg_mul, neg_neg, cons_val', empty_val', cons_val_fin_one, cons_val_one, head_cons, cons_val_two, tail_cons] rw [hV.1, VudAbs_eq_C₁₂_mul_C₁₃ ⟦V⟧] simp [C₁₂, C₁₃] - simp [uRow, sP, standardParameterizationAsMatrix] + simp [uRow, standParam, standParamAsMatrix] rw [hV.2.1, VusAbs_eq_S₁₂_mul_C₁₃ ⟦V⟧, ← S₁₂_eq_sin_θ₁₂ ⟦V⟧, C₁₃] simp - simp [uRow, sP, standardParameterizationAsMatrix] + simp [uRow, standParam, standParamAsMatrix] nth_rewrite 1 [← abs_mul_exp_arg_mul_I (V.1 0 2)] rw [show Complex.abs (V.1 0 2) = VubAbs ⟦V⟧ from rfl] rw [VubAbs_eq_S₁₃, ← S₁₃_eq_sin_θ₁₃ ⟦V⟧] @@ -517,8 +506,8 @@ lemma UCond₁_eq_sP {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) simp funext i fin_cases i - simp [cRow, sP, standardParameterizationAsMatrix] - rw [cd_of_us_or_ud_neq_zero_UCond hb hV] + simp [cRow, standParam, standParamAsMatrix] + rw [cd_of_fstRowThdColRealCond 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₁₃] @@ -527,50 +516,52 @@ lemma UCond₁_eq_sP {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) simp [sq] field_simp ring_nf - simp [cRow, sP, standardParameterizationAsMatrix] + simp [cRow, standParam, standParamAsMatrix] 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 hV] + rw [cs_of_fstRowThdColRealCond hb hV] field_simp rw [h1] simp [sq] field_simp ring_nf - simp [cRow, sP, standardParameterizationAsMatrix] + simp [cRow, standParam, standParamAsMatrix] rw [hV.2.2.1] rw [VcbAbs_eq_S₂₃_mul_C₁₃ ⟦V⟧, S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, C₁₃] simp -lemma UCond₃_eq_sP {V : CKMMatrix} (hV : UCond₃ V) : V = sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by + +lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) : + V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by have h1 : VubAbs ⟦V⟧ = 1 := by simp [VAbs] rw [hV.2.2.2.1] simp - refine eq_sP V ?_ ?_ hV.2.2.2.2.1 + refine eq_rows V ?_ ?_ hV.2.2.2.2.1 funext i fin_cases i - simp [uRow, sP, standardParameterizationAsMatrix] + simp [uRow, standParam, standParamAsMatrix] rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.1] simp - simp [uRow, sP, standardParameterizationAsMatrix] + simp [uRow, standParam, standParamAsMatrix] rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.1] simp - simp [uRow, sP, standardParameterizationAsMatrix] + simp [uRow, standParam, standParamAsMatrix] rw [S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃] simp [VAbs] rw [hV.2.2.2.1] simp funext i fin_cases i - simp [cRow, sP, standardParameterizationAsMatrix] + simp [cRow, standParam, standParamAsMatrix] rw [S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, S₂₃_of_Vub_eq_one h1] rw [S₁₂_eq_ℂsin_θ₁₂ ⟦V⟧, S₁₂_of_Vub_one h1] rw [C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₁₂_of_Vub_one h1] rw [S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃_of_Vub_one h1] rw [hV.2.2.2.2.2.1] simp - simp [cRow, sP, standardParameterizationAsMatrix] + simp [cRow, standParam, standParamAsMatrix] rw [S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, S₂₃_of_Vub_eq_one h1] rw [S₁₂_eq_ℂsin_θ₁₂ ⟦V⟧, S₁₂_of_Vub_one h1] rw [C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₁₂_of_Vub_one h1] @@ -580,13 +571,14 @@ lemma UCond₃_eq_sP {V : CKMMatrix} (hV : UCond₃ V) : V = sP (θ₁₂ ⟦V rw [θ₂₃, Real.cos_arcsin] simp at h3 rw [h3, S₂₃_of_Vub_eq_one h1, hV.2.2.2.2.2.2] - simp [cRow, sP, standardParameterizationAsMatrix] + simp [cRow, standParam, standParamAsMatrix] rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.2.1] simp -theorem exists_standardParameterization_δ₁₃ (V : CKMMatrix) : - ∃ (δ₃ : ℝ), V ≈ sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₃ := by - obtain ⟨U, hU⟩ := all_eq_abs V + +theorem exists_δ₁₃ (V : CKMMatrix) : + ∃ (δ₃ : ℝ), V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₃ := by + obtain ⟨U, hU⟩ := fstRowThdColRealCond_holds_up_to_equiv 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 -- should be much simplier @@ -598,7 +590,7 @@ theorem exists_standardParameterization_δ₁₃ (V : CKMMatrix) : rw [hUV] at hna simp [VAbs] at hna simp_all - have hU' := UCond₁_eq_sP haU hU.2 + have hU' := eq_standParam_of_fstRowThdColRealCond haU hU.2 rw [hU'] at hU use (- arg ([U]ub)) rw [← hUV] @@ -610,23 +602,22 @@ theorem exists_standardParameterization_δ₁₃ (V : CKMMatrix) : simp [VAbs] exact ha simpa [not_or, VAbs] using h1 - have ⟨U2, hU2⟩ := UCond₃_exists haU hU.2 + have ⟨U2, hU2⟩ := ubOnePhaseCond_hold_up_to_equiv_of_ub_one 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 + have hx := eq_standParam_of_ubOnePhaseCond 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 + V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (δ₁₃ ⟦V⟧) := by + obtain ⟨δ₁₃', hδ₃⟩ := exists_δ₁₃ 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δ₃]) + by_cases h : Invariant.mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃'⟧ ≠ 0 + have h2 := eq_exp_of_phases (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃' + (δ₁₃ ⟦V⟧) (by rw [← mulExpδ₁₃_on_param_neq_zero_arg V δ₁₃' h, ← hSV, δ₁₃, Invariant.mulExpδ₁₃]) rw [h2] at hδ₃ exact hδ₃ simp at h @@ -634,22 +625,27 @@ theorem eq_standardParameterization_δ₃ (V : CKMMatrix) : 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 ) + rw [mulExpδ₁₃_on_param_eq_zero_iff, Vs_zero_iff_cos_sin_zero] at h + refine phaseShiftEquivRelation.trans hδ₃ ?_ + rcases h with h | h | h | h | h | h + exact on_param_cos_θ₁₂_eq_zero δ₁₃' h + exact on_param_cos_θ₁₃_eq_zero δ₁₃' h + exact on_param_cos_θ₂₃_eq_zero δ₁₃' h + exact on_param_sin_θ₁₂_eq_zero δ₁₃' h + exact on_param_sin_θ₁₃_eq_zero δ₁₃' h + exact on_param_sin_θ₂₃_eq_zero δ₁₃' h -lemma exists_standardParameterization (V : CKMMatrix) : - ∃ (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ), V ≈ sP θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by + +theorem exists_for_CKMatrix (V : CKMMatrix) : + ∃ (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ), V ≈ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by use θ₁₂ ⟦V⟧, θ₁₃ ⟦V⟧, θ₂₃ ⟦V⟧, δ₁₃ ⟦V⟧ exact eq_standardParameterization_δ₃ V +end standParam + + +open CKMMatrix + + + end