Eq. (4.44) — integral of the squared strain outside a spherical inclusion

Proved

Verlinde2016.inclusion_strain_sq_integral

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

emergent-gravitymathematical-physicsverlinde-2016

Outside a ball $B_0$ of volume $NV_0$ the normal strain is $\varepsilon = NV_0/V$ (4.41), where $V$ is the volume enclosed at radius $r$ . Writing $c = NV_0>0$ , the integral of $\varepsilon^2$ over the complement of $B_0$ , expressed in the volume variable $dV = A(r)\,dr$ , equals the volume of $B_0$ :

\int_{c}^{\infty}\left(\frac{c}{V}\right)^2 dV = c.

Preamble

import Mathlib
import Definitions.Def_Verlinde2016_Defs

open Real

Formal statement

namespace Verlinde2016

theorem inclusion_strain_sq_integral (c : ℝ) (hc : 0 < c) :
    ∫ V in Set.Ioi c, (c / V) ^ 2 = c := 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. 24, eq. (4.44)

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.

For every real number $c>0$ ,

\int_{(c,\infty)} \left(\frac{c}{V}\right)^2\,dV = c,

where the integral is the Lebesgue (Bochner) integral over the open half-line $(c,\infty)$ with respect to Lebesgue measure on $\mathbb R$ . (By Lean's convention this integral would be $0$ if the integrand were not integrable; the statement asserts the value is $c$ .) No other variables or hypotheses 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