New Minimal Standard Model: one neutrino is exactly massless

Proved

NewMinimalStandardModel.exists_massless_neutrino

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

linear-algebramathematical-physicsneutrino-physics

Let $v\in\mathbb R$ (with $\langle H\rangle = v/\sqrt2$ ), let $h_\nu$ be a complex $2\times 3$ Yukawa matrix, and let $M_1,M_2>0$ be the masses of the two right-handed neutrinos of Eq. (4). Let

\mathcal M = \begin{pmatrix} 0 & m_D^{\mathsf T} \\ m_D & \operatorname{diag}(M_1,M_2)\end{pmatrix},\qquad m_D=\frac{v}{\sqrt2}h_\nu,

be the $5\times5$ Majorana mass matrix of $(\nu_1,\nu_2,\nu_3,N_1,N_2)$ . Then one of its physical masses vanishes exactly:

\exists\, i:\quad \sigma_i(\mathcal M) = \sqrt{\lambda_i(\mathcal M^\dagger\mathcal M)} = 0 .

This is the NMSM prediction that, with only two right-handed neutrinos, "one of the neutrino masses exactly vanishes (ignoring tiny Planck suppressed effects)" (p. 122), so that a neutrinoless double-beta-decay signal in near-future experiments is possible only for the inverted hierarchy.

Formalization Note The statement concerns the full tree-level neutral-lepton mass matrix, not the seesaw approximation; positivity of $M_1,M_2$ is the source's convention for the diagonal real basis.

Preamble

import Mathlib
import Definitions.Def_NewMinimalStandardModel_Defs

Formal statement

namespace NewMinimalStandardModel

theorem exists_massless_neutrino (v : ℝ) (hν : Matrix (Fin 2) (Fin 3) ℂ) (M : Fin 2 → ℝ)
    (hM : ∀ α, 0 < M α) :
    ∃ i, majoranaMasses (neutralLeptonMassMatrix 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 (Eq. (4) and the following discussion) and p. 122 ("one of the neutrino masses exactly vanishes")

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 $v$ , every complex $2\times3$ matrix $h_\nu$ , and all reals $M_1>0$ , $M_2>0$ , let $\mathcal M$ be the complex matrix indexed by $\{1,2,3\}\sqcup\{1,2\}$ with block form

\mathcal M=\begin{pmatrix} 0_{3\times3} & \big(\tfrac{v}{\sqrt2}h_\nu\big)^{\mathsf T}\\ \tfrac{v}{\sqrt2}h_\nu & \operatorname{diag}(M_1,M_2)\end{pmatrix}

(plain transpose). The theorem asserts that there exists an index $i$ (among the five) such that $\sqrt{\lambda_i}=0$ , where $(\lambda_i)$ are the eigenvalues of the Hermitian matrix $\mathcal M^\dagger\mathcal M$ as enumerated by Mathlib's spectral theorem. It does not assert how many such indices exist, and places no condition on $v$ or $h_\nu$ .

View graph