Prove2Me

Eq. (7.48) — local density from averaged density, ρ=(1−β/3)ρˉ\rho=(1-\beta/3)\bar\rho

Proved
Verlinde2016.local_density_of_avg_density

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

emergent-gravitymathematical-physicsverlinde-2016

Let ρ\rho be a mass density profile, continuous on (0,∞)(0,\infty) with ρ(r′) 4πr′2\rho(r')\,4\pi r'^2 integrable on every [0,r][0,r], and let M(r)=∫0rρ(r′) 4πr′2 dr′M(r) = \int_0^r\rho(r')\,4\pi r'^2\,dr' (7.39) be the enclosed mass, assumed positive for r>0r>0. With the averaged density ρˉ\bar\rho of (7.45) and its slope parameter β=− dlog⁡ρˉ/dlog⁡r\beta = -\,d\log\bar\rho/d\log r (7.46), for every r>0r>0

ρ(r)=(1−13β(r)) ρˉ(r).\rho(r) = \Big(1-\frac13\beta(r)\Big)\,\bar\rho(r).

The paper states this for the apparent dark matter (ρ=ρD\rho=\rho_D, M=MDM=M_D); the relation is kinematic and holds for any such profile, which is what is formalized.

Preamble
import Mathlib
import Definitions.Def_Verlinde2016_Defs

open Real
Formal statement
namespace Verlinde2016

theorem local_density_of_avg_density (M ρ : ℝ → ℝ) (hρ_cont : ContinuousOn ρ (Set.Ioi 0))
    (hρ_int : ∀ r : ℝ, 0 < r →
      IntervalIntegrable (fun s => ρ s * (4 * π * s ^ 2)) MeasureTheory.volume 0 r)
    (hM : ∀ r : ℝ, 0 < r → M r = ∫ s in (0 : ℝ)..r, ρ s * (4 * π * s ^ 2))
    (hM_pos : ∀ r : ℝ, 0 < r → 0 < M r) :
    ∀ r : ℝ, 0 < r → ρ r = (1 - slopeParam (avgDensity M) r / 3) * avgDensity M 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, eq. (7.48), with (7.39) p. 38 and (7.45)-(7.46) 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 M,ρ:R→RM,\rho:\mathbb R\to\mathbb R be functions such that

  • ρ\rho is continuous on (0,∞)(0,\infty);
  • for every r>0r>0 the function s↦ρ(s)⋅4πs2s\mapsto\rho(s)\cdot4\pi s^2 is integrable on the interval between 00 and rr;
  • for every r>0r>0, M(r)=∫0rρ(s) 4πs2 dsM(r) = \int_0^r \rho(s)\,4\pi s^2\,ds;
  • M(r)>0M(r)>0 for every r>0r>0.

Let ρˉ(r)=3M(r)/(4πr3)\bar\rho(r) = 3M(r)/(4\pi r^3) and β(r)=−r ρˉ′(r)/ρˉ(r)\beta(r) = -r\,\bar\rho'(r)/\bar\rho(r) with ρˉ′\bar\rho' the derivative of r↦ρˉ(r)r\mapsto\bar\rho(r). Conclusion: for every r>0r>0,

ρ(r)=(1−β(r)3) ρˉ(r).\rho(r) = \Big(1-\frac{\beta(r)}{3}\Big)\,\bar\rho(r).

No condition is placed on MM or ρ\rho for r≤0r\le0 beyond what the integrals over [0,r][0,r] use.

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