1. Physlib
  2. Particles
  3. NeutrinoPhysics
  4. Basic
Imports
/- Copyright (c) 2025 Prabhoda Chandra Sarjapur. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Prabhoda Chandra Sarjapur -/ module public import Mathlib.LinearAlgebra.UnitaryGroup public import Mathlib.Analysis.Complex.Exponential

The PMNS matrix

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

@[expose] public section

diagonal phase matrix from a real-valued function on indices

@[simp] def diagPhase (θ : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℂ := λ i j => if i = j then cexp (I * θ i) else 0

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

@[simp] lemma diagPhase_zero: diagPhase (fun _ : Fin 3 => 0) = 1 := ⊢ (diagPhase fun x => 0) = 1 i:Fin 3j:Fin 3⊢ diagPhase (fun x => 0) i j = 1 i j All goals completed! 🐙

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

@[simp] lemma diagPhase_zero_eq : diagPhase 0 = diagPhase (fun _ : Fin 3 => 0) := ⊢ diagPhase 0 = diagPhase fun x => 0 i:Fin 3j:Fin 3⊢ diagPhase 0 i j = diagPhase (fun x => 0) i j All goals completed! 🐙

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

@[simp] lemma diagPhase_star (θ : Fin 3 → ℝ) : (diagPhase θ)ᴴ = diagPhase (- θ) := θ:Fin 3 → ℝ⊢ (diagPhase θ)ᴴ = diagPhase (-θ) θ:Fin 3 → ℝ⊢ (diagonal fun i => cexp (I * ↑(θ i)))ᴴ = diagonal fun i => cexp (I * ↑((-θ) i)) All goals completed! 🐙

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

@[simp] lemma diagPhase_mul (θ φ : Fin 3 → ℝ) : diagPhase θ * diagPhase φ = diagPhase (θ + φ) := θ:Fin 3 → ℝφ:Fin 3 → ℝ⊢ diagPhase θ * diagPhase φ = diagPhase (θ + φ) θ:Fin 3 → ℝφ:Fin 3 → ℝ⊢ ((diagonal fun i => cexp (I * ↑(θ i))) * diagonal fun i => cexp (I * ↑(φ i))) = diagonal fun i => cexp (I * ↑((θ + φ) i)) All goals completed! 🐙

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

θ:Fin 3 → ℝ⊢ diagPhase θ * star (diagPhase θ) = 1 θ:Fin 3 → ℝ⊢ diagPhase θ * (diagPhase θ)ᴴ = 1 θ:Fin 3 → ℝi:Fin 3j:Fin 3⊢ (diagPhase θ * (diagPhase θ)ᴴ) i j = 1 i j θ:Fin 3 → ℝj:Fin 3⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨0, ⋯⟩) j = 1 ((fun i => i) ⟨0, ⋯⟩) jθ:Fin 3 → ℝj:Fin 3⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨1, ⋯⟩) j = 1 ((fun i => i) ⟨1, ⋯⟩) jθ:Fin 3 → ℝj:Fin 3⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨2, ⋯⟩) j = 1 ((fun i => i) ⟨2, ⋯⟩) j θ:Fin 3 → ℝj:Fin 3⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨0, ⋯⟩) j = 1 ((fun i => i) ⟨0, ⋯⟩) jθ:Fin 3 → ℝj:Fin 3⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨1, ⋯⟩) j = 1 ((fun i => i) ⟨1, ⋯⟩) jθ:Fin 3 → ℝj:Fin 3⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨2, ⋯⟩) j = 1 ((fun i => i) ⟨2, ⋯⟩) j θ:Fin 3 → ℝ⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = 1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)θ:Fin 3 → ℝ⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = 1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)θ:Fin 3 → ℝ⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = 1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) θ:Fin 3 → ℝ⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = 1 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)θ:Fin 3 → ℝ⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = 1 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)θ:Fin 3 → ℝ⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = 1 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)θ:Fin 3 → ℝ⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = 1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)θ:Fin 3 → ℝ⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = 1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)θ:Fin 3 → ℝ⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = 1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)θ:Fin 3 → ℝ⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = 1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)θ:Fin 3 → ℝ⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = 1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)θ:Fin 3 → ℝ⊢ (diagPhase θ * (diagPhase θ)ᴴ) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = 1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙⟩

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

@[simp] lemma diagPhaseShift_coe_matrix (θ : Fin 3 → ℝ) : ↑(diagPhaseUnitary θ) = diagPhase θ := rfl

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.

def leptonPhaseShift (a b c : ℝ) : Matrix (Fin 3) (Fin 3) ℂ := diagPhase (fun i => if i = 0 then a else if i = 1 then b else c)

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).

def neutrinoPhaseShift (d e f : ℝ) : Matrix (Fin 3) (Fin 3) ℂ := diagPhase (fun i => if i = 0 then d else if i = 1 then e else f)

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

def majoranaPhaseMatrix (α1 α2 : ℝ) : Matrix (Fin 3) (Fin 3) ℂ := diagPhase (fun i => if i = 0 then 0 else if i = 1 then α1/2 else α2/2)

The Dirac PMNS matrix equivalence relations

def PMNSDiracEquivalence (U V : unitaryGroup (Fin 3) ℂ) : Prop := ∃ (θ φ : Fin 3 → ℝ), U = diagPhase θ * V * diagPhase φ

The relation PMNSDiracEquivalence is reflexive.

lemma PMNSDiracEquivalence_refl : ∀ U : unitaryGroup (Fin 3) ℂ, PMNSDiracEquivalence U U := ⊢ ∀ (U : ↥(unitaryGroup (Fin 3) ℂ)), PMNSDiracEquivalence U U U:↥(unitaryGroup (Fin 3) ℂ)⊢ PMNSDiracEquivalence U U exact ⟨0, 0, U:↥(unitaryGroup (Fin 3) ℂ)⊢ ↑U = diagPhase 0 * ↑U * diagPhase 0 All goals completed! 🐙⟩

The relation PMNSDiracEquivalence is symmetric.

lemma PMNSDiracEquivalence_symm : ∀ U V : unitaryGroup (Fin 3) ℂ, PMNSDiracEquivalence U V → PMNSDiracEquivalence V U := ⊢ ∀ (U V : ↥(unitaryGroup (Fin 3) ℂ)), PMNSDiracEquivalence U V → PMNSDiracEquivalence V U U:↥(unitaryGroup (Fin 3) ℂ)V:↥(unitaryGroup (Fin 3) ℂ)θ:Fin 3 → ℝφ:Fin 3 → ℝh':↑U = diagPhase θ * ↑V * diagPhase φ⊢ PMNSDiracEquivalence V U U:↥(unitaryGroup (Fin 3) ℂ)V:↥(unitaryGroup (Fin 3) ℂ)θ:Fin 3 → ℝφ:Fin 3 → ℝh':↑U = diagPhase θ * ↑V * diagPhase φ⊢ ↑V = diagPhase (-θ) * ↑U * diagPhase (-φ) U:↥(unitaryGroup (Fin 3) ℂ)V:↥(unitaryGroup (Fin 3) ℂ)θ:Fin 3 → ℝφ:Fin 3 → ℝh':↑U = diagPhase θ * ↑V * diagPhase φ⊢ ↑V = diagPhase (-θ + θ) * ↑V * diagPhase φ * diagPhase (-φ) All goals completed! 🐙

The relation PMNSDiracEquivalence is transitive.

lemma PMNSDiracEquivalence_trans {U V W : unitaryGroup (Fin 3) ℂ} : PMNSDiracEquivalence U V → PMNSDiracEquivalence V W → PMNSDiracEquivalence U W := U:↥(unitaryGroup (Fin 3) ℂ)V:↥(unitaryGroup (Fin 3) ℂ)W:↥(unitaryGroup (Fin 3) ℂ)⊢ PMNSDiracEquivalence U V → PMNSDiracEquivalence V W → PMNSDiracEquivalence U W U:↥(unitaryGroup (Fin 3) ℂ)V:↥(unitaryGroup (Fin 3) ℂ)W:↥(unitaryGroup (Fin 3) ℂ)θ1:Fin 3 → ℝφ1:Fin 3 → ℝhUV:↑U = diagPhase θ1 * ↑V * diagPhase φ1θ2:Fin 3 → ℝφ2:Fin 3 → ℝhVW:↑V = diagPhase θ2 * ↑W * diagPhase φ2⊢ PMNSDiracEquivalence U W U:↥(unitaryGroup (Fin 3) ℂ)V:↥(unitaryGroup (Fin 3) ℂ)W:↥(unitaryGroup (Fin 3) ℂ)θ1:Fin 3 → ℝφ1:Fin 3 → ℝhUV:↑U = diagPhase θ1 * ↑V * diagPhase φ1θ2:Fin 3 → ℝφ2:Fin 3 → ℝhVW:↑V = diagPhase θ2 * ↑W * diagPhase φ2⊢ ↑U = diagPhase (θ1 + θ2) * ↑W * diagPhase (φ1 + φ2) U:↥(unitaryGroup (Fin 3) ℂ)V:↥(unitaryGroup (Fin 3) ℂ)W:↥(unitaryGroup (Fin 3) ℂ)θ1:Fin 3 → ℝφ1:Fin 3 → ℝhUV:↑U = diagPhase θ1 * ↑V * diagPhase φ1θ2:Fin 3 → ℝφ2:Fin 3 → ℝhVW:↑V = diagPhase θ2 * ↑W * diagPhase φ2⊢ diagPhase (θ1 + θ2) * ↑W * diagPhase φ2 * diagPhase φ1 = diagPhase (θ1 + θ2) * ↑W * diagPhase (φ1 + φ2) All goals completed! 🐙