Neutrino Oscillations

Stream: PhysLean

[Prabhoda CS]

Hey! I am Prabhoda, I just finished my Mast in Physics at Cambridge, and am currently working under Ben Allanach at DAMTP on a Zprime model and neutrino masses and mixings. I am new to Lean and after speaking to @Joseph Tooby-Smith , I will be trying to formalize results in neutrino oscillations starting from the PMNS matrix properties to the vacuum oscillation formula

[Joseph Tooby-Smith]

Hey @Prabhoda CS , just checking in to see if you managed to find a good place to start with this?

[Prabhoda CS]

Hey, @Joseph Tooby-Smith , sorry, I had been busy the past week preparing for the summer research festival talk where I had to present the work I did with Ben. I have forked the repo and started making a roadmap of some of the results to first prove. I will work on the basic.lean file with some properties of the pmns matrix and push them by tomorrow hopefully

[Prabhoda CS]

Hey @Joseph Tooby-Smith , I started working on the neutrino basic.lean file, and i realised i use diagonal phase matrices quite often, so i thought about writing all the results for them, and then applying it to the different cases of majorana, lepton and dirac phases. I was also thinking of having 2 kinds of proofs for the PMNS matrix, the equivalence relation of PMNS_ifdirac and PMNS_ifmajorana. Is this a good roadmap/approach?

The proofs I have come up with so far are quite lengthy and I will work on trimming it down (I'm still learning the language)

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

lemma diagPhase_zero:
  diagPhase (fun _ : Fin 3 => 0) = 1 := by
  ext i j
  fin_cases i; fin_cases j

  simp []
  simp []
  simp []

  fin_cases j
  simp []
  simp []
  simp []

  fin_cases j
  simp []
  simp []
  simp []


@[simp]
def diagPhase_unitary (θ : Fin 3 → ℝ) : unitaryGroup (Fin 3) ℂ :=
  ⟨diagPhase θ ,
  by
  rw[Matrix.mem_unitaryGroup_iff]
  change _ * (diagPhase θ)ᴴ = 1
  ext i j
  fin_cases i; fin_cases j

  simp [diagPhase, Matrix.mul_apply, Matrix.conjTranspose_apply]
  simp[← exp_conj, ← exp_add]

  simp [diagPhase, Matrix.mul_apply, Matrix.conjTranspose_apply]
  simp [diagPhase, Matrix.mul_apply, Matrix.conjTranspose_apply]
  simp [diagPhase, Matrix.mul_apply, Matrix.conjTranspose_apply]

  fin_cases j
  simp []
  simp []
  simp [← exp_conj, ← exp_add]
  simp []

  fin_cases j
  simp [diagPhase, Matrix.mul_apply, Matrix.conjTranspose_apply]
  simp [diagPhase, Matrix.mul_apply, Matrix.conjTranspose_apply]
  simp [diagPhase, Matrix.mul_apply, Matrix.conjTranspose_apply]
  simp [← exp_conj, ← exp_add]
  ⟩


/-- Given three reals `a b c` the Lepton phase shift matrix as a `3×3` complex matrix, which dictate the phase shift freedom of the charged lepton sector.

Given three reals `d e f` the neutrino phase shift matrix as a `3×3` complex matrix, which dictate the phase shift freedom of the neutrino sector (If neutrinos are Dirac particles).

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

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)

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)

[Joseph Tooby-Smith]

I think this road map sounds good to me, and I think making the matrix diagPhase is a good idea! Maybe we could also use it for the CKM matrix?

I can give you one immediate way you can shorten your proofs. For diagPhase_zero you can use the notation <;> to mean apply to all opened goals so the following should work:

lemma diagPhase_zero:
  diagPhase (fun _ : Fin 3 => 0) = 1 := by
  ext i j
  fin_cases i <;> fin_cases j <;> simp

Similar with your proof in diagPhase_unitary.

[Prabhoda CS]

Thanks for that! I will formalize all the results of diagPhase first in the Neutrino basic.lean file and push it to ensure that you feel it is adequate and correct, then upon ensuring it works well with the other definitions and proofs, I can work on pushing a similar structure to the CKM matrix file too. If that turns out to be a repeat, I was thinking of transferring all the mathematical results of the diagPhase from the neutrino folder into the mathematics folder, and then I can import that module into both the CKM and PMNS as special cases

[Prabhoda CS]

Hey @Joseph Tooby-Smith , I ran the linter checks :

C:\Users\Asus\Documents\Cambridge\Project\Lean\PhysLean>lake exe lint_all
- Style lint
This linter is not checked by GitHub but if you have time please fix these errors.
No linting issues found.

- Building
Build is successful.

- File imports
Files are not imported add the following to the `PhysLean` file:
import PhysLean.Trial

- TODO tag duplicates
Checking for duplicate tags.
Finish duplicate tag check.

- Transitive imports
Expect this linter may take a while to run, it can be skipped with
        lake exe lint_all --fast

- Lean linter
Expect this linter may take a while to run, it can be skipped with
      lake exe lint_all --fast
You can manually perform this linter by placing `#lint` at the end of the files you have modified.
Running linter on specified module: PhysLean
-- Linting passed for PhysLean.

And they all seemed to pass. I even wrote a #lint at the end of my code in VS code to check whether it matches the correct style and I seem to have no problems yet.

Hopefully the third PR is the charm!

[Joseph Tooby-Smith]

Awesome! After this PR the github workflows will run automatically on your PRs (it is only the first one that I have to keep 'approving' them to run manually).

The last step Lean linter takes by for the longest of this (this is an open project if anyone is reading this and wants to make it quicker :)), if you have run #lint at the end of every file you have edited, it is extremely likely that this one will pass, so I never really wait for it before.

I am aware that 'linting' is a bit of a burden when you first get started, and I apologize for that. Hopefully you can see the point in it - namely to have some sort of consistency enforced between the different files etc. Eventually one learns the what needs to be done when linting, which makes the whole process a lot quicker.

[Joseph Tooby-Smith]

I have made a quick commit to your PR to remove the accidentally added file, when it is done with the linters I will merge with master :).

[Prabhoda CS]

Cool, thanks! No, I understand that formatting it consistently across the files will make it easier for others and myself to refer to it later. I’m still learning the language and logic behind the code, so I might mess up some times, but I’ll try to run the lint checks locally and ensure it is within the proper framework before pushing next time onwards

[Joseph Tooby-Smith]

Merged - many thanks for this first PR :tada:

[Prabhoda CS]

The first of many, I hope! I'm finding it quite fun to formalise the physics