Eq. (7.47) — averaged apparent dark matter density $\bar\rho_D^2=(4-\beta_B)\,a_0\bar\rho_B/(8\pi G r)$

Proved

Verlinde2016.avg_apparent_dm_density

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

emergent-gravitymathematical-physicsverlinde-2016

Let $G>0$ , $a_0>0$ . Let $M_B$ be a baryonic mass profile, positive and differentiable on $(0,\infty)$ , and $M_D$ an apparent dark matter mass profile, continuous on $(0,\infty)$ , satisfying the main formula (7.40)

\int_0^r\frac{G\,M_D(r')^2}{r'^2}\,dr' = \frac{M_B(r)\,a_0\,r}{6}\qquad (r>0).

With the averaged densities $\bar\rho_B,\bar\rho_D$ of (7.45) and the slope parameter $\beta_B = -\,d\log\bar\rho_B/d\log r$ of (7.46), for every $r>0$

\bar\rho_D(r)^2 = \big(4-\beta_B(r)\big)\,\frac{a_0\,\bar\rho_B(r)}{8\pi G\,r}.

(The paper says this follows "by differentiating (7.36)"; the computation is the differentiation of its spherically symmetric form (7.40).)

Preamble

import Mathlib
import Definitions.Def_Verlinde2016_Defs

open Real

Formal statement

namespace Verlinde2016

theorem avg_apparent_dm_density (G a₀ : ℝ) (hG : 0 < G) (ha₀ : 0 < a₀)
    (M_B M_D : ℝ → ℝ) (hM_B_diff : DifferentiableOn ℝ M_B (Set.Ioi 0))
    (hM_B_pos : ∀ r : ℝ, 0 < r → 0 < M_B r) (hM_D_cont : ContinuousOn M_D (Set.Ioi 0))
    (hmain : ∀ r : ℝ, 0 < r → ∫ s in (0 : ℝ)..r, G * M_D s ^ 2 / s ^ 2 = M_B r * a₀ * r / 6) :
    ∀ r : ℝ, 0 < r → avgDensity M_D r ^ 2
      = (4 - slopeParam (avgDensity M_B) r) * a₀ * avgDensity M_B r / (8 * π * G * r) := 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. 40, eqs. (7.45)-(7.47), using (7.40) on p. 38

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>0$ and $a_0>0$ be real numbers and let $M_B, M_D:\mathbb R\to\mathbb R$ be functions such that

$M_B$ is differentiable at every point of $(0,\infty)$ ;
$M_B(r)>0$ for every $r>0$ ;
$M_D$ is continuous on $(0,\infty)$ (no sign condition on $M_D$ );
for every $r>0$ ,

\int_0^r \frac{G\,M_D(s)^2}{s^2}\,ds = \frac{M_B(r)\,a_0\,r}{6},

the oriented interval integral over $[0,r]$ (which would be $0$ for a non-integrable integrand; the positive right-hand side rules this out).

Define $\bar\rho_B(r) = 3M_B(r)/(4\pi r^3)$ and $\bar\rho_D(r)=3M_D(r)/(4\pi r^3)$ , and $\beta_B(r) = -r\,\bar\rho_B'(r)/\bar\rho_B(r)$ , where $\bar\rho_B'$ is the derivative of the function $r\mapsto\bar\rho_B(r)$ . Conclusion: for every $r>0$ ,

\bar\rho_D(r)^2 = \frac{\big(4-\beta_B(r)\big)\,a_0\,\bar\rho_B(r)}{8\pi G\,r}.

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.47) — averaged apparent dark matter density ρˉD2=(4−βB) a0ρˉB/(8πGr)\bar\rho_D^2=(4-\beta_B)\,a_0\bar\rho_B/(8\pi G r)ρˉ​D2​=(4−βB​)a0​ρˉ​B​/(8πGr)

Eq. (7.47) — averaged apparent dark matter density $\bar\rho_D^2=(4-\beta_B)\,a_0\bar\rho_B/(8\pi G r)$