Eq. (7.43) — Milgrom relation $g_D=\sqrt{a_M g_B}$ , $a_M=a_0/6$ , for a central point mass

Proved

Verlinde2016.milgrom_relation_point_mass

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

emergent-gravitymathematical-physicsverlinde-2016

Let $G>0$ , $a_0>0$ and a constant baryonic mass $M_B>0$ concentrated at the origin. Let $M_D:(0,\infty)\to[0,\infty)$ be a continuous apparent dark matter mass profile satisfying Verlinde's main formula (7.40),

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

Then for all $r>0$ ,

g_D(r) = \sqrt{a_M\,g_B(r)},\qquad g_B(r) = \frac{GM_B}{r^2},\quad g_D(r)=\frac{GM_D(r)}{r^2},\quad a_M = \frac{a_0}{6}.

Continuity and non-negativity of $M_D$ on $(0,\infty)$ are the physical conventions of the paper (a mass enclosed in a radius), made explicit.

Preamble

import Mathlib
import Definitions.Def_Verlinde2016_Defs

open Real

Formal statement

namespace Verlinde2016

theorem milgrom_relation_point_mass (G a₀ M_B : ℝ) (hG : 0 < G) (ha₀ : 0 < a₀) (hM_B : 0 < M_B)
    (M_D : ℝ → ℝ) (hM_D_cont : ContinuousOn M_D (Set.Ioi 0))
    (hM_D_nonneg : ∀ r : ℝ, 0 < r → 0 ≤ M_D r)
    (hmain : ∀ r : ℝ, 0 < r → ∫ s in (0 : ℝ)..r, G * M_D s ^ 2 / s ^ 2 = M_B * a₀ * r / 6) :
    ∀ r : ℝ, 0 < r → G * M_D r / r ^ 2 = Real.sqrt (a₀ / 6 * (G * M_B / r ^ 2)) := 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. 38, eqs. (7.40), (7.42), (7.43)

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$ , $a_0$ , $M_B$ be real numbers with $G>0$ , $a_0>0$ , $M_B>0$ . Let $M_D:\mathbb R\to\mathbb R$ be any function such that

$M_D$ is continuous on the open half-line $(0,\infty)$ (no condition at $r\le 0$ );
$M_D(r)\ge 0$ for every $r>0$ ;
for every $r>0$ ,

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

Here the integral is the oriented interval integral over $[0,r]$ ; by convention it equals $0$ when the integrand is not integrable on $[0,r]$ , and the integrand at $s=0$ is $0$ because division by zero returns $0$ (a single point, irrelevant for the integral). Since the right-hand side is strictly positive for $r>0$ , the hypothesis can only hold if $s\mapsto G M_D(s)^2/s^2$ is integrable on every $[0,r]$ .

Conclusion: for every $r>0$ ,

\frac{G\,M_D(r)}{r^2} = \sqrt{\frac{a_0}{6}\cdot\frac{G\,M_B}{r^2}},

where $\sqrt{\cdot}$ is the real square root (which returns $0$ on negative inputs; here the argument is positive). $M_B$ is a single constant, not a function of $r$ . Nothing is asserted for $r\le 0$ .

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.43) — Milgrom relation gD=aMgBg_D=\sqrt{a_M g_B}gD​=aM​gB​​, aM=a0/6a_M=a_0/6aM​=a0​/6, for a central point mass

Eq. (7.43) — Milgrom relation $g_D=\sqrt{a_M g_B}$ , $a_M=a_0/6$ , for a central point mass