PhysLean Documentation

PhysLean.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters

Standard parameters for the CKM Matrix #

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

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

def S₁₂ (V : Quotient CKMMatrixSetoid) :

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

Equations

S₁₂ V = VusAbs V / √(VudAbs V ^ 2 + VusAbs V ^ 2)

Instances For

def S₁₃ (V : Quotient CKMMatrixSetoid) :

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

Equations

S₁₃ V = VubAbs V

Instances For

def S₂₃ (V : Quotient CKMMatrixSetoid) :

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

Equations

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

Instances For

def θ₁₂ (V : Quotient CKMMatrixSetoid) :

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

Equations

θ₁₂ V = Real.arcsin (S₁₂ V)

Instances For

def θ₁₃ (V : Quotient CKMMatrixSetoid) :

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

Equations

θ₁₃ V = Real.arcsin (S₁₃ V)

Instances For

def θ₂₃ (V : Quotient CKMMatrixSetoid) :

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

Equations

θ₂₃ V = Real.arcsin (S₂₃ V)

Instances For

def C₁₂ (V : Quotient CKMMatrixSetoid) :

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

Equations

C₁₂ V = Real.cos (θ₁₂ V)

Instances For

def C₁₃ (V : Quotient CKMMatrixSetoid) :

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

Equations

C₁₃ V = Real.cos (θ₁₃ V)

Instances For

def C₂₃ (V : Quotient CKMMatrixSetoid) :

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

Equations

C₂₃ V = Real.cos (θ₂₃ V)

Instances For

def δ₁₃ (V : Quotient CKMMatrixSetoid) :

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

Equations

δ₁₃ V = (Invariant.mulExpδ₁₃ V).arg

Instances For

theorem S₁₂_nonneg (V : Quotient CKMMatrixSetoid) :

0 ≤ S₁₂ V

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

theorem S₁₃_nonneg (V : Quotient CKMMatrixSetoid) :

0 ≤ S₁₃ V

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

theorem S₂₃_nonneg (V : Quotient CKMMatrixSetoid) :

0 ≤ S₂₃ V

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

theorem S₁₂_leq_one (V : Quotient CKMMatrixSetoid) :

S₁₂ V ≤ 1

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

theorem S₁₃_leq_one (V : Quotient CKMMatrixSetoid) :

S₁₃ V ≤ 1

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

theorem S₂₃_leq_one (V : Quotient CKMMatrixSetoid) :

S₂₃ V ≤ 1

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

theorem S₁₂_eq_sin_θ₁₂ (V : Quotient CKMMatrixSetoid) :

Real.sin (θ₁₂ V) = S₁₂ V

theorem S₁₃_eq_sin_θ₁₃ (V : Quotient CKMMatrixSetoid) :

Real.sin (θ₁₃ V) = S₁₃ V

theorem S₂₃_eq_sin_θ₂₃ (V : Quotient CKMMatrixSetoid) :

Real.sin (θ₂₃ V) = S₂₃ V

theorem S₁₂_eq_ℂsin_θ₁₂ (V : Quotient CKMMatrixSetoid) :

Complex.sin ↑(θ₁₂ V) = ↑(S₁₂ V)

theorem S₁₃_eq_ℂsin_θ₁₃ (V : Quotient CKMMatrixSetoid) :

Complex.sin ↑(θ₁₃ V) = ↑(S₁₃ V)

theorem S₂₃_eq_ℂsin_θ₂₃ (V : Quotient CKMMatrixSetoid) :

Complex.sin ↑(θ₂₃ V) = ↑(S₂₃ V)

theorem complexAbs_sin_θ₁₂ (V : Quotient CKMMatrixSetoid) :

↑‖Complex.sin ↑(θ₁₂ V)‖ = Complex.sin ↑(θ₁₂ V)

theorem complexAbs_sin_θ₁₃ (V : Quotient CKMMatrixSetoid) :

↑‖Complex.sin ↑(θ₁₃ V)‖ = Complex.sin ↑(θ₁₃ V)

theorem complexAbs_sin_θ₂₃ (V : Quotient CKMMatrixSetoid) :

↑‖Complex.sin ↑(θ₂₃ V)‖ = Complex.sin ↑(θ₂₃ V)

theorem S₁₂_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) :

theorem S₁₃_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) :

theorem S₂₃_of_Vub_eq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) :

S₂₃ V = VcdAbs V

theorem S₂₃_of_Vub_neq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) :

S₂₃ V = VcbAbs V / √(VudAbs V ^ 2 + VusAbs V ^ 2)

theorem C₁₂_eq_ℂcos_θ₁₂ (V : Quotient CKMMatrixSetoid) :

Complex.cos ↑(θ₁₂ V) = ↑(C₁₂ V)

theorem C₁₃_eq_ℂcos_θ₁₃ (V : Quotient CKMMatrixSetoid) :

Complex.cos ↑(θ₁₃ V) = ↑(C₁₃ V)

theorem C₂₃_eq_ℂcos_θ₂₃ (V : Quotient CKMMatrixSetoid) :

Complex.cos ↑(θ₂₃ V) = ↑(C₂₃ V)

theorem complexAbs_cos_θ₁₂ (V : Quotient CKMMatrixSetoid) :

↑‖Complex.cos ↑(θ₁₂ V)‖ = Complex.cos ↑(θ₁₂ V)

theorem complexAbs_cos_θ₁₃ (V : Quotient CKMMatrixSetoid) :

↑‖Complex.cos ↑(θ₁₃ V)‖ = Complex.cos ↑(θ₁₃ V)

theorem complexAbs_cos_θ₂₃ (V : Quotient CKMMatrixSetoid) :

↑‖Complex.cos ↑(θ₂₃ V)‖ = Complex.cos ↑(θ₂₃ V)

theorem S₁₂_sq_add_C₁₂_sq (V : Quotient CKMMatrixSetoid) :

S₁₂ V ^ 2 + C₁₂ V ^ 2 = 1

theorem S₁₃_sq_add_C₁₃_sq (V : Quotient CKMMatrixSetoid) :

S₁₃ V ^ 2 + C₁₃ V ^ 2 = 1

theorem S₂₃_sq_add_C₂₃_sq (V : Quotient CKMMatrixSetoid) :

S₂₃ V ^ 2 + C₂₃ V ^ 2 = 1

theorem C₁₂_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) :

theorem C₁₃_of_Vub_eq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) :

theorem C₁₂_eq_Vud_div_sqrt {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) :

C₁₂ V = VudAbs V / √(VudAbs V ^ 2 + VusAbs V ^ 2)

theorem C₁₃_eq_add_sq (V : Quotient CKMMatrixSetoid) :

C₁₃ V = √(VudAbs V ^ 2 + VusAbs V ^ 2)

theorem C₂₃_of_Vub_neq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) :

C₂₃ V = VtbAbs V / √(VudAbs V ^ 2 + VusAbs V ^ 2)

theorem VudAbs_eq_C₁₂_mul_C₁₃ (V : Quotient CKMMatrixSetoid) :

VudAbs V = C₁₂ V * C₁₃ V

theorem VusAbs_eq_S₁₂_mul_C₁₃ (V : Quotient CKMMatrixSetoid) :

VusAbs V = S₁₂ V * C₁₃ V

theorem VubAbs_eq_S₁₃ (V : Quotient CKMMatrixSetoid) :

VubAbs V = S₁₃ V

theorem VcbAbs_eq_S₂₃_mul_C₁₃ (V : Quotient CKMMatrixSetoid) :

VcbAbs V = S₂₃ V * C₁₃ V

theorem VtbAbs_eq_C₂₃_mul_C₁₃ (V : Quotient CKMMatrixSetoid) :

VtbAbs V = C₂₃ V * C₁₃ V

theorem VubAbs_of_cos_θ₁₃_zero {V : Quotient CKMMatrixSetoid} (h1 : Real.cos (θ₁₃ V) = 0) :

theorem 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 ∨ Real.sin (θ₁₂ ⟦V⟧) = 0 ∨ Real.sin (θ₁₃ ⟦V⟧) = 0 ∨ Real.sin (θ₂₃ ⟦V⟧) = 0

theorem standParam.mulExpδ₁₃_on_param_δ₁₃ (V : CKMMatrix) (δ₁₃ : ℝ) :

Invariant.mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = Complex.sin ↑(θ₁₂ ⟦V⟧) * Complex.cos ↑(θ₁₃ ⟦V⟧) ^ 2 * Complex.sin ↑(θ₂₃ ⟦V⟧) * Complex.sin ↑(θ₁₃ ⟦V⟧) * Complex.cos ↑(θ₁₂ ⟦V⟧) * Complex.cos ↑(θ₂₃ ⟦V⟧) * Complex.exp (Complex.I * ↑δ₁₃)

theorem standParam.mulExpδ₁₃_on_param_eq_zero_iff (V : CKMMatrix) (δ₁₃ : ℝ) :

Invariant.mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = 0 ↔ VudAbs ⟦V⟧ = 0 ∨ VubAbs ⟦V⟧ = 0 ∨ VusAbs ⟦V⟧ = 0 ∨ VcbAbs ⟦V⟧ = 0 ∨ VtbAbs ⟦V⟧ = 0

theorem standParam.mulExpδ₁₃_on_param_abs (V : CKMMatrix) (δ₁₃ : ℝ) :

↑‖Invariant.mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧‖ = Complex.sin ↑(θ₁₂ ⟦V⟧) * Complex.cos ↑(θ₁₃ ⟦V⟧) ^ 2 * Complex.sin ↑(θ₂₃ ⟦V⟧) * Complex.sin ↑(θ₁₃ ⟦V⟧) * Complex.cos ↑(θ₁₂ ⟦V⟧) * Complex.cos ↑(θ₂₃ ⟦V⟧)

theorem standParam.mulExpδ₁₃_on_param_neq_zero_arg (V : CKMMatrix) (δ₁₃ : ℝ) (h1 : Invariant.mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ ≠ 0) :

Complex.exp (↑(Invariant.mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧).arg * Complex.I) = Complex.exp (↑δ₁₃ * Complex.I)

theorem standParam.on_param_cos_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₃ ⟦V⟧) = 0) :

standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0

theorem standParam.on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₂ ⟦V⟧) = 0) :

standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0

theorem standParam.on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₂₃ ⟦V⟧) = 0) :

standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0

theorem standParam.on_param_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₃ ⟦V⟧) = 0) :

standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0

theorem standParam.on_param_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₂ ⟦V⟧) = 0) :

standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0

theorem standParam.on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₂₃ ⟦V⟧) = 0) :

standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0

theorem standParam.eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : ↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0) (hV : V.FstRowThdColRealCond) :

V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (-(↑V 0 2).arg)

theorem standParam.eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : V.ubOnePhaseCond) :

V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0

theorem standParam.exists_δ₁₃ (V : CKMMatrix) :

∃ (δ₃ : ℝ), V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₃

theorem standParam.eq_standardParameterization_δ₃ (V : CKMMatrix) :

V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (δ₁₃ ⟦V⟧)

theorem standParam.exists_for_CKMatrix (V : CKMMatrix) :

∃ (θ₁₂ : ℝ) (θ₁₃ : ℝ) (θ₂₃ : ℝ) (δ₁₃ : ℝ), V ≈ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃