New Minimal Standard Model: neutrino mass matrices and slow-roll observables

Definition

NewMinimalStandardModel_Defs

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

cosmologymathematical-physicsneutrino-physics

Shared definitions for the new Minimal Standard Model (NMSM) of Davoudiasl–Kitano–Li–Murayama.

Neutrino sector (Eq. (4), p. 119). For a real Higgs vacuum expectation value parameter $v$ (with $\langle H\rangle = v/\sqrt2$ ), a complex $2\times3$ Yukawa matrix $h_\nu$ and real right-handed masses $M_1, M_2$ :

the Dirac mass matrix $m_D = \dfrac{v}{\sqrt2}\,h_\nu$ ;
the right-handed Majorana mass matrix $\operatorname{diag}(M_1, M_2)$ ;
the $5\times5$ neutral-lepton mass matrix in the basis $(\nu_1,\nu_2,\nu_3,N_1,N_2)$ ,

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

the seesaw light-neutrino mass matrix $m_\nu = -\,m_D^{\mathsf T}\operatorname{diag}(M_1,M_2)^{-1} m_D$ ;
the physical (Majorana) masses $\sigma_i(A) = \sqrt{\lambda_i(A^\dagger A)}$ of a square complex matrix $A$ , where $\lambda_i$ are the eigenvalues of the Hermitian matrix $A^\dagger A$ .

Inflaton sector (Eq. (5), p. 119; p. 122). For the quadratic potential $V(\varphi)=\tfrac12 m^2\varphi^2$ and reduced Planck mass $M_{\rm Pl}$ :

\epsilon=\frac{M_{\rm Pl}^2}{2}\Big(\frac{V'}{V}\Big)^2,\quad \eta=M_{\rm Pl}^2\frac{V''}{V},\quad N(\varphi_{\rm end},\varphi)=\frac1{M_{\rm Pl}^2}\int_{\varphi_{\rm end}}^{\varphi}\frac{V}{V'}\,d\psi,\quad n_s=1-6\epsilon+2\eta,\quad r=16\epsilon.

These definitions are used by every theorem in the mission.

Formalization Note The matrix inverse is Mathlib's Matrix.inv (the zero matrix for a singular argument); all theorems that use $m_\nu$ assume $M_1,M_2>0$ . Derivatives are Mathlib's deriv and the integral is the interval integral.

Definition code

import Mathlib

/-!
# The new Minimal Standard Model — shared definitions

Source: H. Davoudiasl, R. Kitano, T. Li, H. Murayama, *The new Minimal Standard Model*,
Phys. Lett. B 609 (2005) 117–123, doi:10.1016/j.physletb.2005.01.026.

* Neutrino sector: Eq. (4) (p. 119) with two right-handed neutrinos `N_α`, `α = 1, 2`,
  in the basis where the right-handed-neutrino mass matrix is real and diagonal.
* Inflaton sector: Eq. (5) (p. 119), quadratic chaotic inflation, with the standard
  slow-roll observables used on p. 122.
-/

namespace NewMinimalStandardModel

open Matrix

/-! ## Neutrino sector (Eq. (4)) -/

/-- Dirac mass matrix `m_D = h_ν v / √2` (a `2 × 3` complex matrix, rows indexed by the
right-handed neutrinos `α`, columns by the lepton doublets `i`), obtained from the Yukawa
coupling `h_ν^{αi} N_α L_i H̃` of Eq. (4) with Higgs vacuum expectation value `⟨H⟩ = v / √2`. -/
noncomputable def diracMass (v : ℝ) (hν : Matrix (Fin 2) (Fin 3) ℂ) :
    Matrix (Fin 2) (Fin 3) ℂ :=
  ((v : ℂ) / (Real.sqrt 2 : ℂ)) • hν

/-- Majorana mass matrix of the two right-handed neutrinos, `diag(M_1, M_2)`, in the basis
where it is real and diagonal (Eq. (4), p. 119). -/
noncomputable def rhNeutrinoMass (M : Fin 2 → ℝ) : Matrix (Fin 2) (Fin 2) ℂ :=
  Matrix.diagonal fun α => (M α : ℂ)

/-- The full `5 × 5` complex symmetric Majorana mass matrix of the neutral leptons after
electroweak symmetry breaking, in the basis `(ν_1, ν_2, ν_3, N_1, N_2)`:
`[[0, m_Dᵀ], [m_D, diag(M_1, M_2)]]`. -/
noncomputable def neutralLeptonMassMatrix (v : ℝ) (hν : Matrix (Fin 2) (Fin 3) ℂ)
    (M : Fin 2 → ℝ) : Matrix (Fin 3 ⊕ Fin 2) (Fin 3 ⊕ Fin 2) ℂ :=
  Matrix.fromBlocks 0 (diracMass v hν)ᵀ (diracMass v hν) (rhNeutrinoMass M)

/-- The seesaw light-neutrino (left-handed) Majorana mass matrix
`m_ν = - m_Dᵀ diag(M_1, M_2)⁻¹ m_D` (a `3 × 3` complex symmetric matrix). -/
noncomputable def seesawMassMatrix (v : ℝ) (hν : Matrix (Fin 2) (Fin 3) ℂ)
    (M : Fin 2 → ℝ) : Matrix (Fin 3) (Fin 3) ℂ :=
  -((diracMass v hν)ᵀ * (rhNeutrinoMass M)⁻¹ * diracMass v hν)

/-- The physical masses of the Majorana mass eigenstates described by a square complex mass
matrix `A`: its singular values, i.e. the square roots of the eigenvalues of the Hermitian
positive semidefinite matrix `Aᴴ A` (listed in the order chosen by Mathlib's spectral
theorem). -/
noncomputable def majoranaMasses {n : Type*} [Fintype n] [DecidableEq n]
    (A : Matrix n n ℂ) : n → ℝ :=
  fun i => Real.sqrt ((Matrix.isHermitian_conjTranspose_mul_self A).eigenvalues i)

/-! ## Inflaton sector (Eq. (5)) and slow-roll observables -/

/-- The quadratic inflaton potential `V(φ) = m² φ² / 2` driving chaotic inflation
(the mass term of Eq. (5); the cubic and quartic terms are neglected, p. 119). -/
noncomputable def quadraticPotential (m : ℝ) : ℝ → ℝ :=
  fun φ => m ^ 2 * φ ^ 2 / 2

/-- First slow-roll parameter `ε(φ) = (M_Pl² / 2) (V'(φ) / V(φ))²`, with `M_Pl` the reduced
Planck mass. -/
noncomputable def slowRollEpsilon (V : ℝ → ℝ) (Mpl φ : ℝ) : ℝ :=
  Mpl ^ 2 / 2 * (deriv V φ / V φ) ^ 2

/-- Second slow-roll parameter `η(φ) = M_Pl² V''(φ) / V(φ)`. -/
noncomputable def slowRollEta (V : ℝ → ℝ) (Mpl φ : ℝ) : ℝ :=
  Mpl ^ 2 * deriv (deriv V) φ / V φ

/-- Number of e-folds of slow-roll inflation between field values `φ_end` and `φ`:
`N = (1 / M_Pl²) ∫_{φ_end}^{φ} V(ψ) / V'(ψ) dψ`. -/
noncomputable def efolds (V : ℝ → ℝ) (Mpl φend φ : ℝ) : ℝ :=
  (1 / Mpl ^ 2) * ∫ ψ in φend..φ, V ψ / deriv V ψ

/-- Slow-roll scalar spectral index `n_s = 1 - 6 ε + 2 η`. -/
noncomputable def spectralIndex (V : ℝ → ℝ) (Mpl φ : ℝ) : ℝ :=
  1 - 6 * slowRollEpsilon V Mpl φ + 2 * slowRollEta V Mpl φ

/-- Slow-roll tensor-to-scalar ratio `r = 16 ε`. -/
noncomputable def tensorToScalarRatio (V : ℝ → ℝ) (Mpl φ : ℝ) : ℝ :=
  16 * slowRollEpsilon V Mpl φ

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, Eqs. (4)-(5), p. 119; p. 122

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.

The file declares, inside the namespace NewMinimalStandardModel, the following objects (no theorems).

Dirac mass. For $v\in\mathbb R$ and a complex $2\times3$ matrix $h_\nu$ (rows indexed by $\alpha\in\{1,2\}$ , columns by $i\in\{1,2,3\}$ ), $m_D(v,h_\nu)$ is the complex $2\times 3$ matrix $\frac{v}{\sqrt2}\,h_\nu$ (scalar multiple; here $\sqrt2$ is the real square root viewed as a complex number).
Right-handed mass. For $M:\{1,2\}\to\mathbb R$ , the complex $2\times2$ diagonal matrix $\operatorname{diag}(M_1,M_2)$ .
Neutral-lepton mass matrix. A complex matrix with rows and columns indexed by the disjoint union $\{1,2,3\}\sqcup\{1,2\}$ (five indices), given in block form as

\begin{pmatrix} 0 & m_D^{\mathsf T} \\ m_D & \operatorname{diag}(M_1,M_2)\end{pmatrix},

with the zero $3\times3$ block in the upper left, the plain transpose (no complex conjugation) $m_D^{\mathsf T}$ upper right, and $m_D$ lower left.

Seesaw matrix. The complex $3\times3$ matrix $-\,m_D^{\mathsf T}\,(\operatorname{diag}(M_1,M_2))^{-1}\,m_D$ , where the inverse is Mathlib's matrix inverse, which returns the zero matrix when the argument is singular (so if some $M_\alpha=0$ the whole seesaw matrix is $0$ ).
Majorana masses. For any finite index type $n$ and complex square matrix $A$ , a function $n\to\mathbb R$ sending $i$ to $\sqrt{\lambda_i}$ , where $(\lambda_i)$ is the list of real eigenvalues of the Hermitian matrix $A^\dagger A$ (conjugate transpose times $A$ ) produced by Mathlib's spectral theorem, in Mathlib's ordering; $\sqrt{\cdot}$ is the real square root (which would return $0$ on negative input, though these eigenvalues are nonnegative).
Quadratic potential. $V_m(\varphi)=m^2\varphi^2/2$ for real $m,\varphi$ .
Slow-roll $\epsilon$ . For $V:\mathbb R\to\mathbb R$ and reals $M_{\rm Pl},\varphi$ : $\epsilon = \frac{M_{\rm Pl}^2}{2}\big(V'(\varphi)/V(\varphi)\big)^2$ , where $V'$ is Mathlib's derivative (equal to $0$ where $V$ is not differentiable) and division by $0$ gives $0$ .
Slow-roll $\eta$ . $\eta = M_{\rm Pl}^2\,V''(\varphi)/V(\varphi)$ , with $V''$ the iterated Mathlib derivative and the same division convention.
E-folds. $N(V,M_{\rm Pl},\varphi_{\rm end},\varphi) = \frac{1}{M_{\rm Pl}^2}\int_{\varphi_{\rm end}}^{\varphi} \frac{V(\psi)}{V'(\psi)}\,d\psi$ (oriented interval integral; division by $0$ gives $0$ ; the integral is $0$ if the integrand is not integrable).
Spectral index. $n_s = 1 - 6\epsilon + 2\eta$ evaluated at $\varphi$ .
Tensor-to-scalar ratio. $r = 16\,\epsilon$ evaluated at $\varphi$ .

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