Two right-handed neutrinos: the seesaw mass matrix has rank $\le 2$ and a massless state

Proved

NewMinimalStandardModel.seesawMassMatrix_rank_le_two

by Lucas · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebramathematical-physicsneutrino-physics

Let $v\in\mathbb R$ , let $h_\nu$ be a complex $2\times3$ Yukawa matrix and let $M_1,M_2>0$ be the right-handed-neutrino masses. Let $m_D = h_\nu v/\sqrt2$ and let

m_\nu = -\,m_D^{\mathsf T}\operatorname{diag}(M_1,M_2)^{-1}m_D

be the seesaw light-neutrino mass matrix. Then

$\operatorname{rank} m_\nu \le 2$ , and
some physical mass of $m_\nu$ vanishes: $\sigma_i(m_\nu)=0$ for some $i$ , where $\sigma_i(m_\nu)=\sqrt{\lambda_i(m_\nu^\dagger m_\nu)}$ .

This is the statement "Because the left-handed neutrino Majorana mass matrix has rank two, there is one massless state" (p. 119).

Preamble

import Mathlib
import Definitions.Def_NewMinimalStandardModel_Defs

Formal statement

namespace NewMinimalStandardModel

theorem seesawMassMatrix_rank_le_two (v : ℝ) (hν : Matrix (Fin 2) (Fin 3) ℂ) (M : Fin 2 → ℝ)
    (hM : ∀ α, 0 < M α) :
    (seesawMassMatrix v hν M).rank ≤ 2 ∧
      ∃ i, majoranaMasses (seesawMassMatrix v hν M) i = 0 := by sorry

end NewMinimalStandardModel

Source

H. Davoudiasl, R. Kitano, T. Li, H. Murayama, The new Minimal Standard Model, Phys. Lett. B 609 (2005) 117-123, https://doi.org/10.1016/j.physletb.2005.01.026, p. 119, right column (discussion after Eq. (4))

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent that drafted the statements; NON-BLIND, not an independent auditor

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor and must not be treated as independent evidence of faithfulness. Reviewers should compare the Lean code against the source themselves.

For every real number $v$ , every complex $2\times3$ matrix $h_\nu$ , and every pair of real numbers $M_1, M_2$ with $M_1>0$ and $M_2>0$ , consider the complex $3\times3$ matrix

m_\nu = -\Big(\tfrac{v}{\sqrt2}h_\nu\Big)^{\mathsf T}\operatorname{diag}(M_1,M_2)^{-1}\Big(\tfrac{v}{\sqrt2}h_\nu\Big)

(plain transpose; Mathlib matrix inverse, which here is the genuine inverse since $M_1,M_2\neq0$ ). The theorem asserts two things: (1) the rank of $m_\nu$ (as a matrix over $\mathbb C$ ) is at most $2$ ; and (2) there exists an index $i\in\{1,2,3\}$ such that $\sqrt{\lambda_i}=0$ , where $\lambda_1,\lambda_2,\lambda_3$ are the eigenvalues of the Hermitian matrix $m_\nu^\dagger m_\nu$ as enumerated by Mathlib's spectral theorem. No hypothesis is placed on $v$ (it may be $0$ , in which case $m_\nu=0$ ) or on $h_\nu$ .

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Two right-handed neutrinos: the seesaw mass matrix has rank ≤2\le 2≤2 and a massless state

Two right-handed neutrinos: the seesaw mass matrix has rank $\le 2$ and a massless state