Refactor: Names

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

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
 
 

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)
+lemma shift_cross_product_phase_zero {V : CKMMatrix} {τ : ℝ}
-  (h1 : τ = - u - c - t - d - s - b) :
+  (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) :
+lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) :
-    ∃ (U : CKMMatrix), V ≈ U ∧ UCond₁ U:= by
+    ∃ (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)  :
+lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0))
-    ∃ (U : CKMMatrix), V ≈ U ∧ UCond₃ U:= by
+    (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)
+lemma cd_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0)
-    (hV : UCond₁ V) : [V]cd = (- VtbAbs ⟦V⟧ * VusAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) +
+    (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)
+lemma cs_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0)
-    (hV : UCond₁ V) : [V]cs = (VtbAbs ⟦V⟧ * VudAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2))
+    (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

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)
+lemma fst_row_orthog_snd_row (V : CKMMatrix) :
-    + V.1 1 2 * conj (V.1 0 2) = 0 := by
+    [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)
+lemma fst_row_orthog_thd_row (V : CKMMatrix) :
-    + V.1 2 2 * conj (V.1 0 2) = 0 := by
+    [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 )
+  linear_combination (V.fst_row_orthog_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
 
@@ -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_mul_Vud {V : CKMMatrix} {τ : ℝ}
-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τ]
+  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_mul_Vus {V : CKMMatrix} {τ : ℝ}
-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τ]
+  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}
+end columns
-    (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

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  (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
+lemma standParamAsMatrix_unitary  (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
-    ((standardParameterizationAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ *  standardParameterizationAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)  = 1 := by
+    ((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 :=
+def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix :=
-  ⟨standardParameterizationAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by
+  ⟨standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by
    rw [mem_unitaryGroup_iff']
-   exact standardParameterizationAsMatrix_unitary θ₁₂ θ₁₃ θ₂₃ δ₁₃⟩
+   exact standParamAsMatrix_unitary θ₁₂ θ₁₃ θ₂₃ δ₁₃⟩
 
-lemma sP_cross (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
+namespace standParam
-    [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]t = (conj [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]u ×₃ conj [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) := by
+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)
+lemma eq_rows (U : CKMMatrix) {θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ} (hu : [U]u = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u)
-    (hc : [U]c = [sP θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) (hU :  [U]t = conj [U]u ×₃ conj [U]c) :
+    (hc : [U]c = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) (hU :  [U]t = conj [U]u ×₃ conj [U]c) :
-    U = sP θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by
+    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)) :
+lemma eq_exp_of_phases (θ₁₂ θ₁₃ θ₂₃ δ₁₃ δ₁₃' : ℝ) (h : cexp (δ₁₃ * I) = cexp (δ₁₃' * I)) :
-    sP θ₁₂ θ₁₃ θ₂₃ δ₁₃ = sP θ₁₂ θ₁₃ θ₂₃ δ₁₃' := by
+    standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃' := by
-  simp [sP, standardParameterizationAsMatrix]
+  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
+open Invariant in
-
+lemma VusVubVcdSq_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂)
-lemma VusVubVcdSq_sP (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (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 ]
+  rw [mulExpδ₁₃, VusVubVcdSq_eq _ _ _ _ h1 h2 h3 h4 ]
-  simp only [jarlskogℂ, sP, standardParameterizationAsMatrix, neg_mul,
+  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

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
+lemma VubAbs_of_cos_θ₁₃_zero {V : Quotient CKMMatrixSetoid} (h1 : Real.cos (θ₁₃ V) = 0) :
-
-
-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)
@@ -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)
+namespace standParam
-    (hV : UCond₁ V) : V = sP (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (- arg [V]ub) := by
+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]
+  simp [cRow, standParam, standParamAsMatrix]
-  rw [cd_of_us_or_ud_neq_zero_UCond hb hV]
+  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
+theorem exists_δ₁₃ (V : CKMMatrix) :
-  obtain ⟨U, hU⟩ := all_eq_abs V
+    ∃ (δ₃ : ℝ), 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
+    V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (δ₁₃ ⟦V⟧) := by
-  obtain ⟨δ₁₃', hδ₃⟩ := exists_standardParameterization_δ₁₃ V
+  obtain ⟨δ₁₃', hδ₃⟩ := exists_δ₁₃ V
   have hSV := (Quotient.eq.mpr (hδ₃))
-  by_cases h : Invariant.mulExpδ₃ ⟦sP (θ₁₂ ⟦V⟧) (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃'⟧ ≠ 0
+  by_cases h : Invariant.mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃'⟧ ≠ 0
-  have h1 := Invariant.mulExpδ₃_neq_zero_arg V δ₁₃' h
+  have h2 := eq_exp_of_phases (θ₁₂ ⟦V⟧)  (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃'
-  have h2 := eq_phases_sP (θ₁₂ ⟦V⟧)  (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃'
+    (δ₁₃ ⟦V⟧) (by rw [← mulExpδ₁₃_on_param_neq_zero_arg V δ₁₃' h, ← hSV, δ₁₃, Invariant.mulExpδ₁₃])
-    (δ₁₃ ⟦V⟧) (by rw [← h1, ← 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
+  rw [mulExpδ₁₃_on_param_eq_zero_iff, Vs_zero_iff_cos_sin_zero] at h
-  cases' h with h h
+  refine phaseShiftEquivRelation.trans hδ₃ ?_
-  exact phaseShiftEquivRelation.trans hδ₃ (sP_cos_θ₁₂_eq_zero δ₁₃' h )
+  rcases h with h | h | h | h | h | h
-  cases' h with h h
+  exact on_param_cos_θ₁₂_eq_zero δ₁₃' h
-  exact phaseShiftEquivRelation.trans hδ₃ (sP_cos_θ₁₃_eq_zero δ₁₃' h )
+  exact on_param_cos_θ₁₃_eq_zero δ₁₃' h
-  cases' h with h h
+  exact on_param_cos_θ₂₃_eq_zero δ₁₃' h
-  exact phaseShiftEquivRelation.trans hδ₃ (sP_cos_θ₂₃_eq_zero δ₁₃' h )
+  exact on_param_sin_θ₁₂_eq_zero δ₁₃' h
-  cases' h with h h
+  exact on_param_sin_θ₁₃_eq_zero δ₁₃' h
-  exact phaseShiftEquivRelation.trans hδ₃ (sP_sin_θ₁₂_eq_zero δ₁₃' h )
+  exact on_param_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
+theorem exists_for_CKMatrix (V : CKMMatrix) :
+    ∃ (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ), V ≈ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by
   use θ₁₂ ⟦V⟧, θ₁₃ ⟦V⟧, θ₂₃ ⟦V⟧, δ₁₃ ⟦V⟧
   exact eq_standardParameterization_δ₃ V
 
+end standParam
+
+
+open CKMMatrix
+
+
+
 end