Two-right-handed-neutrino seesaw reproduces every rank- $\le 2$ symmetric light mass matrix

Proved

NewMinimalStandardModel.seesaw_accommodates_rank_two

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

linear-algebramathematical-physicsneutrino-physics

Let $v>0$ and $M_1, M_2>0$ . For every complex symmetric $3\times 3$ matrix $m$ ( $m^{\mathsf T}=m$ ) with $\operatorname{rank} m\le 2$ there is a complex $2\times3$ Yukawa matrix $h_\nu$ such that

-\,m_D^{\mathsf T}\operatorname{diag}(M_1,M_2)^{-1}m_D = m,\qquad m_D = \frac{v}{\sqrt2}h_\nu .

This makes precise the paper's remark that, with eleven real parameters in Eq. (4) and only seven light-neutrino parameters (two masses, three mixing angles, one Dirac and one Majorana phase), "we have enough parameters to accommodate the current data": every light-neutrino mass matrix with one massless state is realized by the two-right-handed-neutrino seesaw, for any choice of heavy masses.

Preamble

import Mathlib
import Definitions.Def_NewMinimalStandardModel_Defs

Formal statement

namespace NewMinimalStandardModel

theorem seesaw_accommodates_rank_two (v : ℝ) (hv : 0 < v) (M : Fin 2 → ℝ)
    (hM : ∀ α, 0 < M α) (m : Matrix (Fin 3) (Fin 3) ℂ) (hsymm : m.transpose = m)
    (hrank : m.rank ≤ 2) :
    ∃ hν : Matrix (Fin 2) (Fin 3) ℂ, seesawMassMatrix v hν M = m := 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 (parameter count 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 $v>0$ , every pair of reals $M_1>0$ , $M_2>0$ , and every complex $3\times3$ matrix $m$ satisfying $m^{\mathsf T}=m$ (plain transpose, no conjugation) and $\operatorname{rank} m\le 2$ , there exists a complex $2\times3$ matrix $h_\nu$ such that

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

exactly (entrywise equality of complex matrices). Nothing is asserted about uniqueness of $h_\nu$ , and $m=0$ is allowed.

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-neutrino seesaw reproduces every rank-≤2\le 2≤2 symmetric light mass matrix

Two-right-handed-neutrino seesaw reproduces every rank- $\le 2$ symmetric light mass matrix