The PMNS matrix

The definition the PMNS matrix, which describes neutrino oscillations as part of U(3).

def diagPhase (θ : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℂ

diagonal phase matrix from a real-valued function on indices

Equations

• diagPhase θ i j = if i = j then Complex.exp (Complex.I * ↑(θ i)) else 0

@[simp]

theorem diagPhase_zero : (diagPhase fun (x : Fin 3) => 0) = 1

lemma stating that the diagonal phase matrix with all zeros is the identity matrix

@[simp]

theorem diagPhase_zero_eq : diagPhase 0 = diagPhase fun (x : Fin 3) => 0

lemma stating that diagPhase with θ = 0 is equal to diagPhase with all zero phases

@[simp]

theorem diagPhase_star (θ : Fin 3 → ℝ) : (diagPhase θ).conjTranspose = diagPhase (-θ)

lemma stating that the Hermitian conjugate of diagPhase diag(+iθ_i) is just diagPhase with entries diag(-iθ_i)

@[simp]

theorem diagPhase_mul (θ φ : Fin 3 → ℝ) : diagPhase θ * diagPhase φ = diagPhase (θ + φ)

lemma stating that multiplying two phase matrices is equivalent to adding the phases

def diagPhase_unitary (θ : Fin 3 → ℝ) : ↥(Matrix.unitaryGroup (Fin 3) ℂ)

diagonal phase matrix diag(iθ_i) is part of the unitary group

Equations

• diagPhase_unitary θ = ⟨diagPhase θ, ⋯⟩

@[simp]

theorem diagPhaseShift_coe_matrix (θ : Fin 3 → ℝ) : ↑(diagPhase_unitary θ) = diagPhase θ

The underlying matrix of the phase-shift element of the unitary group is the phase-shift matrix.

def leptonPhaseShift (a b c : ℝ) : Matrix (Fin 3) (Fin 3) ℂ

The Lepton phase shift matrix as a 3×3 complex matrix, given three reals a b c. This dictates the phase shift freedom of the charged lepton sector.

Equations

• leptonPhaseShift a b c = diagPhase fun (i : Fin 3) => if i = 0 then a else if i = 1 then b else c

def neutrinoPhaseShift (d e f : ℝ) : Matrix (Fin 3) (Fin 3) ℂ

The neutrino phase shift matrix as a 3×3 complex matrix, given three reals d e f. This dictates the phase shift freedom of the neutrino sector (If neutrinos are Dirac).

Equations

• neutrinoPhaseShift d e f = diagPhase fun (i : Fin 3) => if i = 0 then d else if i = 1 then e else f

def majoranaPhaseMatrix (α1 α2 : ℝ) : Matrix (Fin 3) (Fin 3) ℂ

If neutrinos are Majorana particles, then the neutrino phase shift matrix is physical, and cannot be absorbed into the definition of the neutrino fields.

Equations

• majoranaPhaseMatrix α1 α2 = diagPhase fun (i : Fin 3) => if i = 0 then 0 else if i = 1 then α1 / 2 else α2 / 2

def PMNS_dirac_equivalence (U V : ↥(Matrix.unitaryGroup (Fin 3) ℂ)) : Prop

The Dirac PMNS matrix equivalence relations

Equations

• PMNS_dirac_equivalence U V = ∃ (θ : Fin 3 → ℝ) (φ : Fin 3 → ℝ), ↑U = diagPhase θ * ↑V * diagPhase φ

theorem PMNS_dirac_equivalence_refl (U : ↥(Matrix.unitaryGroup (Fin 3) ℂ)) : PMNS_dirac_equivalence U U

The relation PMNS_dirac_equivalence is reflexive.

theorem PMNS_dirac_equivalence_symm (U V : ↥(Matrix.unitaryGroup (Fin 3) ℂ)) : PMNS_dirac_equivalence U V → PMNS_dirac_equivalence V U

The relation PMNS_dirac_equivalence is symmetric.

theorem PMNS_dirac_equivalence_trans {U V W : ↥(Matrix.unitaryGroup (Fin 3) ℂ)} : PMNS_dirac_equivalence U V → PMNS_dirac_equivalence V W → PMNS_dirac_equivalence U W

The relation PMNS_dirac_equivalence is transitive.