Eq. (7.51) — $\Omega_D^2=\frac43\Omega_B$ from (7.47) at the Hubble radius

Proved

Verlinde2016.density_parameter_relation

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

emergent-gravitymathematical-physicsverlinde-2016

Apply (7.47) to the whole universe with constant baryonic density ( $\beta_B=0$ ) at the Hubble radius $r=L=c/H_0$ , with $a_0=cH_0$ :

\bar\rho_D^2 = 4\,\frac{a_0\,\bar\rho_B}{8\pi G\,L}.

With the critical density $\rho_{\rm crit} = \dfrac{3H_0^2}{8\pi G} = \dfrac{3a_0}{8\pi G}\dfrac1L$ (7.50) and $\Omega_B=\bar\rho_B/\rho_{\rm crit}$ , $\Omega_D=\bar\rho_D/\rho_{\rm crit}$ , this gives

\Omega_D^2 = \frac43\,\Omega_B .

The specialized form of (7.47) is taken as the hypothesis.

Preamble

import Mathlib
import Definitions.Def_Verlinde2016_Defs

open Real

Formal statement

namespace Verlinde2016

theorem density_parameter_relation (G c H₀ ρ_B ρ_D : ℝ) (hG : 0 < G) (hc : 0 < c) (hH₀ : 0 < H₀)
    (h747 : ρ_D ^ 2 = (4 - 0) * (c * H₀) * ρ_B / (8 * π * G * (c / H₀))) :
    (ρ_D / (3 * H₀ ^ 2 / (8 * π * G))) ^ 2 = 4 / 3 * (ρ_B / (3 * H₀ ^ 2 / (8 * π * G))) := by sorry

end Verlinde2016

Source

E. Verlinde, Emergent Gravity and the Dark Universe, SciPost Phys. 2, 016 (2017), arXiv:1611.02269v2, https://arxiv.org/abs/1611.02269, p. 41, eqs. (7.50)-(7.51), using (7.47) p. 40

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent as drafter, non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, at the explicit instruction of the account owner. It was not produced blind by an independent auditor, and the author had seen the source paper and the intended meaning while writing it. Reviewers should not treat it as independent evidence of faithfulness and should check the Lean code directly.

Let $G, c, H_0$ be real numbers with $G>0$ , $c>0$ , $H_0>0$ , and let $\rho_B,\rho_D$ be arbitrary real numbers satisfying

\rho_D^2 = \frac{(4-0)\,(cH_0)\,\rho_B}{8\pi G\,(c/H_0)}.

(The factor $(4-0)$ is written literally; the hypothesis forces $\rho_B\ge0$ .) Put $\rho_{\rm crit} = 3H_0^2/(8\pi G)$ (written out inline in the code, not as a named quantity). Conclusion:

\Big(\frac{\rho_D}{\rho_{\rm crit}}\Big)^2 = \frac43\cdot\frac{\rho_B}{\rho_{\rm crit}}.

The statement is a purely algebraic implication between real numbers; no functions, derivatives or integrals appear.

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Eq. (7.51) — ΩD2=43ΩB\Omega_D^2=\frac43\Omega_BΩD2​=34​ΩB​ from (7.47) at the Hubble radius

Eq. (7.51) — $\Omega_D^2=\frac43\Omega_B$ from (7.47) at the Hubble radius