Inverting the density parameters for $\phi_c$ and $V_2(\phi_c)$ , Eqs. (26)–(27)

Proved

MDOUnifiedCosmology.parameter_inversion

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

cosmologymathematical-physics

Let $m_{pl}>0$ be the Planck mass with $\kappa^2=8\pi/m_{pl}^2$ , let $H_0\neq0$ , $\rho_{b,0}>0$ , $\phi_c>0$ , and use the density parameters $\rho_{\mathrm{crit},0}=3H_0^2/\kappa^2$ , $\Omega_b=\rho_{b,0}/\rho_{\mathrm{crit},0}$ , $\Omega_{DM,\phi}=\frac{\kappa^2\phi_c^2}{8}\Omega_b$ (Eq. (26)), $\Lambda_{\mathrm{eff}}=\kappa^2\left(1+\frac{\kappa^2\phi_c^2}{8}\right)V_2(\phi_c)$ (Eq. (24)) and $\Omega_{\Lambda,\phi}=\Lambda_{\mathrm{eff}}/(\kappa^2\rho_{\mathrm{crit},0})$ . Then

$\displaystyle \phi_c=m_{pl}\sqrt{\frac{\Omega_{DM,\phi}}{\pi\,\Omega_b}}$ (Sect. 6), and
$\displaystyle V_2(\phi_c)=\left(\frac{\Omega_{\Lambda,\phi}}{1+\Omega_{DM,\phi}/\Omega_b}\right)\rho_{\mathrm{crit},0}$ (Eq. (27)).

These formulas express the model parameters through observable density parameters.

Preamble

import Mathlib
import Definitions.Def_MDOUnifiedCosmology_model

open MDOUnifiedCosmology Set

Formal statement

namespace MDOUnifiedCosmology

theorem parameter_inversion (κ mpl H₀ ρb₀ φc m α : ℝ) (hmpl : 0 < mpl)
    (hκ : κ ^ 2 = 8 * Real.pi / mpl ^ 2) (hH₀ : H₀ ≠ 0) (hρb₀ : 0 < ρb₀) (hφc : 0 < φc) :
    φc = mpl * Real.sqrt (omegaDM κ φc (omegaB κ H₀ ρb₀) / (Real.pi * omegaB κ H₀ ρb₀)) ∧
    V2 m α φc = omegaLambda κ H₀ φc m α /
        (1 + omegaDM κ φc (omegaB κ H₀ ρb₀) / omegaB κ H₀ ρb₀) * critDensity κ H₀ := by
  sorry

end MDOUnifiedCosmology

Source

S. H. Pereira, M. E. S. Alves, T. M. Guimarães, "An unified cosmological evolution driven by a mass dimension one fermionic field", Eur. Phys. J. C 79 (2019) 543, https://doi.org/10.1140/epjc/s10052-019-7036-5, p. 5, Eq. (27) and the sentence before it; p. 8, Sect. 6 (

\phi_c = m_{pl}\sqrt{\Omega_{DM,\phi}/\pi\Omega_b}

);

\kappa^2 = 8\pi/m_{pl}^2

from p. 2 below Eq. (1)

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

Inverting the density parameters for ϕc\phi_cϕc​ and V2(ϕc)V_2(\phi_c)V2​(ϕc​), Eqs. (26)–(27)

Inverting the density parameters for $\phi_c$ and $V_2(\phi_c)$ , Eqs. (26)–(27)