Late-time MDO cosmology has exactly the ΛCDM Hubble function (Eqs. (22)–(26))
ProvedMDOUnifiedCosmology.late_time_LCDMLate-time MDO cosmology reproduces the CDM expansion law.
Consider the model with potential , , , where . Suppose that on a late-time interval :
- the scale factor is positive and differentiable, and the baryon density is differentiable;
- the MDO field sits at the bottom of the symmetry-breaking potential, ;
- the only other matter is pressureless baryonic matter: (Eq. (9) with , );
- the first Friedmann equation (5) holds, .
Fix a reference time with and . Set , , , and . Then for every
This is Eq. (25) of the paper: once the field is frozen at , its gravitational (spinorial) coupling to baryons acts as a dark matter component scaling like , and the residual potential energy acts as a cosmological constant.
Formalization Note The frozen-field regime is encoded exactly (, hence and ); 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 rather than on all of , because a matter-filled expanding universe cannot have for all times. The positivity of is the paper's standing assumption.
import Mathlib import Definitions.Def_MDOUnifiedCosmology_model open MDOUnifiedCosmology Set
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 MDOUnifiedCosmologyConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.