MDO energy density in terms of matter density, Eq. (12)

Proved

MDOUnifiedCosmology.energy_density_rewrite

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

cosmologymathematical-physics

Throughout, $\kappa^2 = 8\pi G$ (units $c=\hbar=1$ ), $a(t)>0$ is the scale factor of the flat FLRW metric, $H=\dot a/a$ is the Hubble function, $\phi(t)$ is the time-dependent part of the MDO fermionic field, $V$ is its potential, $\rho_m, p_m$ are the energy density and pressure of the other matter components, and $F(\phi) = 1+\kappa^2\phi^2/8$ .

Let the MDO energy density be defined by Eq. (10), $\rho_\phi=\frac{\dot\phi^2}{2}+V(\phi)+\frac38\frac{H^2\phi^2}{1+\kappa^2\phi^2/8}$ . If at time $t$ the first Friedmann equation (5) holds, then

\rho_\phi=\frac{\kappa^2\phi^2}{8}\rho_m+\left(1+\frac{\kappa^2\phi^2}{8}\right)\left[\frac{\dot\phi^2}{2}+V(\phi)\right].

This is Eq. (12); the first term exhibits the coupling between the MDO field and the matter density that is responsible for the dark matter behaviour.

Preamble

import Mathlib
import Definitions.Def_MDOUnifiedCosmology_model

open MDOUnifiedCosmology Set

Formal statement

namespace MDOUnifiedCosmology

theorem energy_density_rewrite (κ : ℝ) (V : ℝ → ℝ) (a φ ρm : ℝ → ℝ) (t : ℝ)
    (h5 : FriedmannEq κ V a φ ρm t) :
    rhoPhi κ V a φ t = κ ^ 2 * φ t ^ 2 / 8 * ρm t
      + couplingFactor κ (φ t) * (deriv φ t ^ 2 / 2 + V (φ t)) := 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. 3, Eqs. (5), (10), (12)

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