Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Late-time MDO cosmology has exactly the ΛCDM Hubble function (Eqs. (22)–(26))

Proved
MDOUnifiedCosmology.late_time_LCDM

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

cosmologymathematical-physics

Late-time MDO cosmology reproduces the Λ\LambdaΛCDM expansion law.

Consider the model with potential V=V1+V2V=V_1+V_2V=V1​+V2​, V1(ϕ)=A4(1−ϕ2/ϕc2)2V_1(\phi)=A^4(1-\phi^2/\phi_c^2)^2V1​(ϕ)=A4(1−ϕ2/ϕc2​)2, V2(ϕ)=12m2ϕ2+α4ϕ4V_2(\phi)=\tfrac12 m^2\phi^2+\tfrac\alpha4\phi^4V2​(ϕ)=21​m2ϕ2+4α​ϕ4, where κ,A,ϕc>0\kappa, A,\phi_c>0κ,A,ϕc​>0. Suppose that on a late-time interval t>Tt>Tt>T:

  1. the scale factor aaa is positive and differentiable, and the baryon density ρb\rho_bρb​ is differentiable;
  2. the MDO field sits at the bottom of the symmetry-breaking potential, ϕ(t)=ϕc\phi(t)=\phi_cϕ(t)=ϕc​;
  3. the only other matter is pressureless baryonic matter: ρ˙b+3Hρb=0\dot\rho_b+3H\rho_b=0ρ˙​b​+3Hρb​=0 (Eq. (9) with ρm=ρb\rho_m=\rho_bρm​=ρb​, pm=0p_m=0pm​=0);
  4. the first Friedmann equation (5) holds, H2=κ23(1+κ2ϕ28)[ϕ˙22+V(ϕ)+ρb]H^2=\frac{\kappa^2}{3}\left(1+\frac{\kappa^2\phi^2}{8}\right)\left[\frac{\dot\phi^2}{2}+V(\phi)+\rho_b\right]H2=3κ2​(1+8κ2ϕ2​)[2ϕ˙​2​+V(ϕ)+ρb​].

Fix a reference time t0>Tt_0>Tt0​>T with a(t0)=1a(t_0)=1a(t0​)=1 and H0=H(t0)≠0H_0=H(t_0)\neq0H0​=H(t0​)=0. Set ρcrit,0=3H02/κ2\rho_{\mathrm{crit},0}=3H_0^2/\kappa^2ρcrit,0​=3H02​/κ2, Ωb=ρb(t0)/ρcrit,0\Omega_b=\rho_b(t_0)/\rho_{\mathrm{crit},0}Ωb​=ρb​(t0​)/ρcrit,0​, ΩDM,ϕ=κ2ϕc28Ωb\Omega_{DM,\phi}=\frac{\kappa^2\phi_c^2}{8}\Omega_bΩDM,ϕ​=8κ2ϕc2​​Ωb​, Λeff=κ2(1+κ2ϕc28)V2(ϕc)\Lambda_{\mathrm{eff}}=\kappa^2\left(1+\frac{\kappa^2\phi_c^2}{8}\right)V_2(\phi_c)Λeff​=κ2(1+8κ2ϕc2​​)V2​(ϕc​) and ΩΛ,ϕ=Λeff/(κ2ρcrit,0)\Omega_{\Lambda,\phi}=\Lambda_{\mathrm{eff}}/(\kappa^2\rho_{\mathrm{crit},0})ΩΛ,ϕ​=Λeff​/(κ2ρcrit,0​). Then for every t>Tt>Tt>T

H(t)2H02=Ωba(t)3+ΩDM,ϕa(t)3+ΩΛ,ϕ.\frac{H(t)^2}{H_0^2}=\frac{\Omega_b}{a(t)^3}+\frac{\Omega_{DM,\phi}}{a(t)^3}+\Omega_{\Lambda,\phi}.H02​H(t)2​=a(t)3Ωb​​+a(t)3ΩDM,ϕ​​+ΩΛ,ϕ​.

This is Eq. (25) of the paper: once the field is frozen at ϕc\phi_cϕc​, its gravitational (spinorial) coupling to baryons acts as a dark matter component scaling like a−3a^{-3}a−3, and the residual potential energy V2(ϕc)V_2(\phi_c)V2​(ϕc​) acts as a cosmological constant.

Formalization Note The frozen-field regime is encoded exactly (ϕ≡ϕc\phi\equiv\phi_cϕ≡ϕc​, hence ϕ˙=0\dot\phi=0ϕ˙​=0 and V1(ϕc)=0V_1(\phi_c)=0V1​(ϕc​)=0); the field equation (7) is deliberately not assumed, since the paper uses only Eqs. (12)/(15) in this regime. The hypotheses are stated on the open half-line (T,∞)(T,\infty)(T,∞) rather than on all of R\mathbb RR, because a matter-filled expanding universe cannot have a>0a>0a>0 for all times. The positivity of AAA is the paper's standing assumption.

Preamble
import Mathlib
import Definitions.Def_MDOUnifiedCosmology_model

open MDOUnifiedCosmology Set
Formal statement
namespace MDOUnifiedCosmology

theorem late_time_LCDM (κ A φc m α : ℝ) (hκ : 0 < κ) (hA : 0 < A) (hφc : 0 < φc)
    (T t₀ : ℝ) (ht₀ : T < t₀) (a φ ρb : ℝ → ℝ)
    (ha_pos : ∀ t ∈ Ioi T, 0 < a t) (ha_diff : DifferentiableOn ℝ a (Ioi T))
    (hρb_diff : DifferentiableOn ℝ ρb (Ioi T))
    (hφ : ∀ t ∈ Ioi T, φ t = φc)
    (ha₀ : a t₀ = 1) (hH₀ : hubble a t₀ ≠ 0)
    (hcons : ∀ t ∈ Ioi T, MatterConservation a ρb (fun _ => 0) t)
    (hfried : ∀ t ∈ Ioi T, FriedmannEq κ (potential A φc m α) a φ ρb t) :
    ∀ t ∈ Ioi T,
      hubble a t ^ 2 / hubble a t₀ ^ 2 =
        omegaB κ (hubble a t₀) (ρb t₀) / a t ^ 3
          + omegaDM κ φc (omegaB κ (hubble a t₀) (ρb t₀)) / a t ^ 3
          + omegaLambda κ (hubble a t₀) φc m α := 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. 4, Sect. 3, Eqs. (22)–(26) with footnote 2
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 paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me