Quadratic chaotic inflation: $n_s = 1-\frac{4}{2N+1}$ and $r = \frac{16}{2N+1}$

Proved

NewMinimalStandardModel.quadratic_chaotic_inflation_predictions

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

cosmologyinflationmathematical-physics

Let $m>0$ and $M_{\rm Pl}>0$ , and let $V(\varphi)=\tfrac12 m^2\varphi^2$ . Let $\varphi_{\rm end}=\sqrt2\,M_{\rm Pl}$ , let $\varphi_*>\varphi_{\rm end}$ , and let

N = \frac{1}{M_{\rm Pl}^2}\int_{\varphi_{\rm end}}^{\varphi_*}\frac{V(\psi)}{V'(\psi)}\,d\psi

be the number of e-folds between $\varphi_*$ and $\varphi_{\rm end}$ . Then

$\epsilon(\varphi_{\rm end}) = 1$ (inflation ends at $\varphi_{\rm end}$ );
$n_s(\varphi_*) = 1 - 6\epsilon(\varphi_*) + 2\eta(\varphi_*) = 1-\dfrac{4}{2N+1}$ ;
$r(\varphi_*) = 16\,\epsilon(\varphi_*) = \dfrac{16}{2N+1}$ ;
if $N = 50$ , then $|n_s - 0.96| < 0.005$ and $|r-0.16|<0.005$ .

This is the closed-form content behind the paper's predictions $n_s\simeq 0.96$ and $r\simeq0.16$ for the $\varphi^2$ chaotic inflation model.

Formalization Note The paper quotes the numerical values (citing Ellis–Raidal–Yanagida) without stating the number of e-folds; the value $N=50$ in item 4 is the conventional choice that reproduces them, and items 2–3 hold for every $N$ .

Preamble

import Mathlib
import Definitions.Def_NewMinimalStandardModel_Defs

Formal statement

namespace NewMinimalStandardModel

theorem quadratic_chaotic_inflation_predictions (m Mpl φstar N : ℝ) (hm : 0 < m)
    (hMpl : 0 < Mpl) (hφ : Real.sqrt 2 * Mpl < φstar)
    (hN : efolds (quadraticPotential m) Mpl (Real.sqrt 2 * Mpl) φstar = N) :
    slowRollEpsilon (quadraticPotential m) Mpl (Real.sqrt 2 * Mpl) = 1 ∧
    spectralIndex (quadraticPotential m) Mpl φstar = 1 - 4 / (2 * N + 1) ∧
    tensorToScalarRatio (quadraticPotential m) Mpl φstar = 16 / (2 * N + 1) ∧
    (N = 50 →
      |spectralIndex (quadraticPotential m) Mpl φstar - 0.96| < 0.005 ∧
      |tensorToScalarRatio (quadraticPotential m) Mpl φstar - 0.16| < 0.005) := 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, Eq. (5) p. 119 and p. 122 left column ("The spectrum index of the φ² chaotic inflation model is predicted to be 0.96 ... The tensor-to-scalar ratio is 0.16 [21]")

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 all reals $m, M_{\rm Pl}, \varphi_*, N$ with $m>0$ , $M_{\rm Pl}>0$ and $\sqrt2\,M_{\rm Pl}<\varphi_*$ , write $V(\varphi)=m^2\varphi^2/2$ and assume

\frac{1}{M_{\rm Pl}^2}\int_{\sqrt2 M_{\rm Pl}}^{\varphi_*}\frac{V(\psi)}{V'(\psi)}\,d\psi = N

(Mathlib derivative and interval integral; division by zero is $0$ ). Then all of the following hold: (1) $\frac{M_{\rm Pl}^2}{2}\big(V'(\sqrt2M_{\rm Pl})/V(\sqrt2M_{\rm Pl})\big)^2 = 1$ ; (2) $1 - 6\epsilon(\varphi_*) + 2\eta(\varphi_*) = 1 - \frac{4}{2N+1}$ , where $\epsilon(\varphi)=\frac{M_{\rm Pl}^2}{2}(V'(\varphi)/V(\varphi))^2$ and $\eta(\varphi)=M_{\rm Pl}^2V''(\varphi)/V(\varphi)$ ; (3) $16\,\epsilon(\varphi_*) = \frac{16}{2N+1}$ (real division; $N$ is a real number, not restricted to integers, and is determined by the hypothesis); (4) if $N=50$ then $|1-6\epsilon(\varphi_*)+2\eta(\varphi_*) - 0.96|<0.005$ and $|16\epsilon(\varphi_*)-0.16|<0.005$ .

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

Quadratic chaotic inflation: ns=1−42N+1n_s = 1-\frac{4}{2N+1}ns​=1−2N+14​ and r=162N+1r = \frac{16}{2N+1}r=2N+116​

Quadratic chaotic inflation: $n_s = 1-\frac{4}{2N+1}$ and $r = \frac{16}{2N+1}$