docs: CKM Relations

HepLean/FlavorPhysics/CKMMatrix/Invariants.lean

@@ -28,6 +28,7 @@ namespace Invariant
 def jarlskogℂCKM (V : CKMMatrix) : ℂ :=
   [V]us * [V]cb * conj [V]ub * conj [V]cs
 
+/-- The complex jarlskog invariant is equal for equivalent CKM matrices. -/
 lemma jarlskogℂCKM_equiv (V U : CKMMatrix) (h : V ≈ U) :
     jarlskogℂCKM V = jarlskogℂCKM U := by
   obtain ⟨a, b, c, e, f, g, h⟩ := h
@@ -50,7 +51,7 @@ def jarlskogℂ : Quotient CKMMatrixSetoid → ℂ :=
   Quotient.lift jarlskogℂCKM jarlskogℂCKM_equiv
 
 /-- An invariant for CKM mtrices corresponding to the square of the absolute values
-  of the `us`, `ub` and `cb` elements multipled together divied by `(VudAbs V ^ 2 + VusAbs V ^2)` .
+  of the `us`, `ub` and `cb` elements multipled together divided by `(VudAbs V ^ 2 + VusAbs V ^2)` .
 -/
 def VusVubVcdSq (V : Quotient CKMMatrixSetoid) : ℝ :=
     VusAbs V ^ 2 * VubAbs V ^ 2 * VcbAbs V ^2 / (VudAbs V ^ 2 + VusAbs V ^2)

HepLean/FlavorPhysics/CKMMatrix/Relations.lean

@@ -23,6 +23,7 @@ open ComplexConjugate
 
 section rows
 
+/-- The absolute value squared of any rwo of a CKM matrix is `1`, in terms of `Vabs`. -/
 lemma VAbs_sum_sq_row_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
     (VAbs i 0 V) ^ 2 + (VAbs i 1 V) ^ 2 + (VAbs i 2 V) ^ 2 = 1 := by
   obtain ⟨V, hV⟩ := Quot.exists_rep V
@@ -37,25 +38,31 @@ lemma VAbs_sum_sq_row_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
   rw [← ofReal_inj]
   simpa using ht
 
+/-- The absolute value squared of the first rwo of a CKM matrix is `1`, in terms of `abs`. -/
 lemma fst_row_normalized_abs (V : CKMMatrix) : abs [V]ud ^ 2 + abs [V]us ^ 2 + abs [V]ub ^ 2 = 1 :=
   VAbs_sum_sq_row_eq_one ⟦V⟧ 0
 
+/-- The absolute value squared of the second rwo of a CKM matrix is `1`, in terms of `abs`. -/
 lemma snd_row_normalized_abs (V : CKMMatrix) : abs [V]cd ^ 2 + abs [V]cs ^ 2 + abs [V]cb ^ 2 = 1 :=
   VAbs_sum_sq_row_eq_one ⟦V⟧ 1
 
+/-- The absolute value squared of the thid rwo of a CKM matrix is `1`, in terms of `abs`. -/
 lemma thd_row_normalized_abs (V : CKMMatrix) : abs [V]td ^ 2 + abs [V]ts ^ 2 + abs [V]tb ^ 2 = 1 :=
   VAbs_sum_sq_row_eq_one ⟦V⟧ 2
 
+/-- The absolute value squared of the first rwo of a CKM matrix is `1`, in terms of `nomSq`. -/
 lemma fst_row_normalized_normSq (V : CKMMatrix) :
     normSq [V]ud + normSq [V]us + normSq [V]ub = 1 := by
   repeat rw [← Complex.sq_abs]
   exact V.fst_row_normalized_abs
 
+/-- The absolute value squared of the second rwo of a CKM matrix is `1`, in terms of `nomSq`. -/
 lemma snd_row_normalized_normSq (V : CKMMatrix) :
     normSq [V]cd + normSq [V]cs + normSq [V]cb = 1 := by
   repeat rw [← Complex.sq_abs]
   exact V.snd_row_normalized_abs
 
+/-- The absolute value squared of the third rwo of a CKM matrix is `1`, in terms of `nomSq`. -/
 lemma thd_row_normalized_normSq (V : CKMMatrix) :
     normSq [V]td + normSq [V]ts + normSq [V]tb = 1 := by
   repeat rw [← Complex.sq_abs]
@@ -63,10 +70,10 @@ lemma thd_row_normalized_normSq (V : CKMMatrix) :
 
 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)
+  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)
+  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

HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean

@@ -36,6 +36,7 @@ def standParamAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : Matrix (Fin
 
 open CKMMatrix
 
+/-- The standard parameterization forms a unitary matrix. -/
 lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
     ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) = 1 := by
   funext j i
@@ -115,6 +116,9 @@ def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix :=
     exact standParamAsMatrix_unitary θ₁₂ θ₁₃ θ₂₃ δ₁₃⟩
 
 namespace standParam
+
+/-- The top-row of the standard parameterization is the cross product of the conjugate of the
+  up and charm rows. -/
 lemma cross_product_t (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
     [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t =
     (conj [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u ×₃ conj [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) := by
@@ -149,12 +153,16 @@ lemma cross_product_t (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
     rw [sin_sq]
     ring
 
+/-- A CKM matrix which has rows equal to that of a standard parameterisation is equal
+  to that standard parameterisation. -/
 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, cross_product_t, hu, hc]
 
+/-- Two standard parameterisations of CKM matrices are the same matrix if they have
+  the same angles and the exponential of their faces is equal. -/
 lemma eq_exp_of_phases (θ₁₂ θ₁₃ θ₂₃ δ₁₃ δ₁₃' : ℝ) (h : cexp (δ₁₃ * I) = cexp (δ₁₃' * I)) :
     standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃' := by
   simp only [standParam, standParamAsMatrix, ofReal_cos, ofReal_sin, neg_mul]

HepLean/Lorentz/ComplexTensor/Basis.lean

@@ -63,6 +63,7 @@ lemma basis_eq_FD {n : ℕ} (c : Fin n → complexLorentzTensor.C)
   subst h'
   rfl
 
+/-- The `perm` node acting on basis vectors corresponds to a basis vector. -/
 lemma perm_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     {c1 : Fin m → complexLorentzTensor.C} (σ : OverColor.mk c ⟶ OverColor.mk c1)
     (b : Π j, Fin (complexLorentzTensor.repDim (c j))) :
@@ -79,6 +80,8 @@ lemma perm_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, LinearEquiv.ofLinear_apply]
   rw [basis_eq_FD]
 
+/-- The `perm` node acting on basis vectors corresponds to a basis vector, as a tensor tree
+  structue. -/
 lemma perm_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     {c1 : Fin m → complexLorentzTensor.C} (σ : OverColor.mk c ⟶ OverColor.mk c1)
     (b : Π j, Fin (complexLorentzTensor.repDim (c j))) :
@@ -168,6 +171,7 @@ def prodBasisVecEquiv {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
   | Sum.inl _ => Equiv.refl _
   | Sum.inr _ => Equiv.refl _
 
+/-- The `prod` node acting on basis vectors corresponds to a basis vector. -/
 lemma prod_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     {c1 : Fin m → complexLorentzTensor.C}
     (b : Π k, Fin (complexLorentzTensor.repDim (c k)))
@@ -197,6 +201,7 @@ lemma prod_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
   | Sum.inl k => rfl
   | Sum.inr k => rfl
 
+/-- The prod node acting on a basis vectors is a basis vector, as a tensor tree structure. -/
 lemma prod_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     {c1 : Fin m → complexLorentzTensor.C}
     (b : Π k, Fin (complexLorentzTensor.repDim (c k)))
@@ -207,6 +212,7 @@ lemma prod_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     ((HepLean.PiTensorProduct.elimPureTensor b b1) (finSumFinEquiv.symm i))))).tensor := by
   exact prod_basisVector _ _
 
+/-- The `eval` node acting on basis vectors corresponds to a basis vector. -/
 lemma eval_basisVector {n : ℕ} {c : Fin n.succ → complexLorentzTensor.C}
     {i : Fin n.succ} (j : Fin (complexLorentzTensor.repDim (c i)))
     (b : Π k, Fin (complexLorentzTensor.repDim (c k))) :