Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Eq. (3.6) and Sec. 3.1: initial Hubble rate, V(Φi)V(\Phi_i)V(Φi​), slow-roll parameters, mass and coupling for the benchmark parameters

Proved
PereiraGuimaraesElko.chaotic_inflation_estimates_sec_3_1

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

cosmologymathematical-physicsordinary-differential-equations

Work in Planck units mpl=1m_{\rm pl}=1mpl​=1, so κ2=8π\kappa^2=8\piκ2=8π. Take the benchmark parameters of Section 3.1:

v0=0,Φi=2.1,σ=1,Λ=5×10−6,v_0=0,\qquad \Phi_i=2.1,\qquad \sigma=1,\qquad \Lambda=5\times10^{-6},v0​=0,Φi​=2.1,σ=1,Λ=5×10−6,

the potential V(Φ)=v0+Λ4(1−Φ2/σ2)2V(\Phi)=v_0+\Lambda^4(1-\Phi^2/\sigma^2)^2V(Φ)=v0​+Λ4(1−Φ2/σ2)2 of (3.1), and the slow-roll value of the initial Hubble rate (3.6),

H2(ti)=κ23(1+κ2Φi28)V(Φi).H^2(t_i)=\frac{\kappa^2}{3}\left(1+\frac{\kappa^2\Phi_i^2}{8}\right)V(\Phi_i).H2(ti​)=3κ2​(1+8κ2Φi2​​)V(Φi​).

Then each of the following quantities agrees with the value printed in the paper to within 5%5\%5% relative error:

  1. H2(ti)≃9.04×10−19H^2(t_i)\simeq9.04\times10^{-19}H2(ti​)≃9.04×10−19;
  2. ti=H(ti)−1≃5.7×10−35 t_i=H(t_i)^{-1}\simeq5.7\times10^{-35}\,ti​=H(ti​)−1≃5.7×10−35s, using mpl=1.86×1043 s−1m_{\rm pl}=1.86\times10^{43}\,{\rm s}^{-1}mpl​=1.86×1043s−1;
  3. V(Φi)≃7.2×10−21V(\Phi_i)\simeq7.2\times10^{-21}V(Φi​)≃7.2×10−21;
  4. ϵ=1κ2(V′(Φi)V(Φi))2≃0.24\epsilon=\dfrac1{\kappa^2}\left(\dfrac{V'(\Phi_i)}{V(\Phi_i)}\right)^2\simeq0.24ϵ=κ21​(V(Φi​)V′(Φi​)​)2≃0.24 (slow-roll parameter (1.6));
  5. ∣η∣=∣1κ2V′′(Φi)(1+κ2Φi2/8)V(Φi)∣≃0.011|\eta|=\left|\dfrac1{\kappa^2}\dfrac{V''(\Phi_i)}{(1+\kappa^2\Phi_i^2/8)V(\Phi_i)}\right|\simeq0.011∣η∣=​κ21​(1+κ2Φi2​/8)V(Φi​)V′′(Φi​)​​≃0.011 (slow-roll parameter (3.5));
  6. m=2 μ=2⋅2Λ2/σ≃7.1×10−11m=\sqrt2\,\mu=\sqrt2\cdot2\Lambda^2/\sigma\simeq7.1\times10^{-11}m=2​μ=2​⋅2Λ2/σ≃7.1×10−11;
  7. m≃8.6×108 m\simeq8.6\times10^{8}\,m≃8.6×108GeV, using mpl=1.22×1019 m_{\rm pl}=1.22\times10^{19}\,mpl​=1.22×1019GeV;

and the self-coupling is exactly α=4Λ4/σ4=2.5×10−21\alpha=4\Lambda^4/\sigma^4=2.5\times10^{-21}α=4Λ4/σ4=2.5×10−21.

These are the analytic estimates that fix the benchmark model before the numerical integration.

Formalization Note The paper writes "≃\simeq≃" with two or three significant digits (and truncates V(Φi)=7.27…×10−21V(\Phi_i)=7.27\ldots\times10^{-21}V(Φi​)=7.27…×10−21 to 7.27.27.2); a uniform 5%5\%5% relative tolerance is used to encode "≃\simeq≃". The e-fold number N=93N=93N=93 and the other outputs of the numerical integration are not part of this item.

Preamble
import Mathlib
Formal statement
namespace PereiraGuimaraesElko

theorem chaotic_inflation_estimates_sec_3_1 (κ Λ σ v₀ Φi Hi2 : ℝ) (V : ℝ → ℝ)
    (hκ : κ ^ 2 = 8 * Real.pi)
    (hΛ : Λ = 5e-6) (hσ : σ = 1) (hv₀ : v₀ = 0) (hΦi : Φi = 2.1)
    (hV : ∀ Φ, V Φ = v₀ + Λ ^ 4 * (1 - Φ ^ 2 / σ ^ 2) ^ 2)
    (hHi2 : Hi2 = κ ^ 2 / 3 * (1 + κ ^ 2 * Φi ^ 2 / 8) * V Φi) :
    |Hi2 - 9.04e-19| ≤ 0.05 * 9.04e-19 ∧
    |1 / (Real.sqrt Hi2 * 1.86e43) - 5.7e-35| ≤ 0.05 * 5.7e-35 ∧
    |V Φi - 7.2e-21| ≤ 0.05 * 7.2e-21 ∧
    |1 / κ ^ 2 * (deriv V Φi / V Φi) ^ 2 - 0.24| ≤ 0.05 * 0.24 ∧
    |abs (1 / κ ^ 2 * deriv (deriv V) Φi / ((1 + κ ^ 2 * Φi ^ 2 / 8) * V Φi)) - 0.011|
      ≤ 0.05 * 0.011 ∧
    |Real.sqrt 2 * (2 * Λ ^ 2 / σ) - 7.1e-11| ≤ 0.05 * 7.1e-11 ∧
    |Real.sqrt 2 * (2 * Λ ^ 2 / σ) * 1.22e19 - 8.6e8| ≤ 0.05 * 8.6e8 ∧
    4 * Λ ^ 4 / σ ^ 4 = 2.5e-21 := by
  sorry

end PereiraGuimaraesElko
Source
S. H. Pereira and T. M. Guimarães, "From inflation to recent cosmic acceleration: the fermionic Elko field driving the evolution of the universe", JCAP 09 (2017) 038, https://doi.org/10.1088/1475-7516/2017/09/038 (arXiv:1702.07385), pp. 7–8, Sec. 3.1, Eq. (3.6), slow-roll parameters (1.6) and (3.5), and the following values; unit conversions m_pl = 1.22e19 GeV = 1.86e43 s^-1 from Appendix B, p. 15
Human review
  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me