Eq. (3.6) and Sec. 3.1: initial Hubble rate, , slow-roll parameters, mass and coupling for the benchmark parameters
ProvedPereiraGuimaraesElko.chaotic_inflation_estimates_sec_3_1cosmologymathematical-physicsordinary-differential-equations
Work in Planck units , so . Take the benchmark parameters of Section 3.1:
the potential of (3.1), and the slow-roll value of the initial Hubble rate (3.6),
Then each of the following quantities agrees with the value printed in the paper to within relative error:
- ;
- s, using ;
- ;
- (slow-roll parameter (1.6));
- (slow-roll parameter (3.5));
- ;
- GeV, using GeV;
and the self-coupling is exactly .
These are the analytic estimates that fix the benchmark model before the numerical integration.
Formalization Note The paper writes "" with two or three significant digits (and truncates to ); a uniform relative tolerance is used to encode "". The e-fold number 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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.