$\partial_r\Delta = 2r-2M$

Proved

KerrBL.hasDerivAt_Del_r

by He Wang · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

coordinate-geometrygeneral-relativitykerr-metrickerrbl-missionricci-flatness

For all real $M,a,r$ the function $u\mapsto\Delta(M,a,u)=a^2+u^2-2Mu$ has derivative $-2M+2r$ at $u=r$ , in the sense of HasDerivAt.

Atom lemma of Layer II: the radial derivative of $\Delta$ , consumed by hdgKerr_all and hdchrKerr_all through the chain rule.

Preamble

import Definitions.Def_KerrBL_Kerr_Metric
open KerrBL Filter Topology

Formal statement

theorem KerrBL.hasDerivAt_Del_r (M a r : ℝ) : HasDerivAt (fun u => Del M a u) (((-2))*M + 2*r) r := by sorry

Source

R. P. Kerr, Gravitational field of a spinning mass as an example of algebraically special metrics, Phys. Rev. Lett. 11 (1963) 237-238, https://doi.org/10.1103/PhysRevLett.11.237; R. H. Boyer and R. W. Lindquist, Maximal analytic extension of the Kerr metric, J. Math. Phys. 8 (1967) 265-281, https://doi.org/10.1063/1.1705193, Sec. 2 (Boyer-Lindquist form of the Kerr line element); metric components transcribed token-for-token from the project certificate EinsteinSolver/certificate/kerr/metric.json (sha256 d729883d95fd7d3cf84d9c971c6725f847155562cc4e88660535b8d0bd0be336); design record LEAN/kerr-formalization/mission/DESIGN.md, node N4 (hasDerivAt_Del_r)

Human review

Endorsed by Shuze Chen · Sep 14, 2026
Endorsed by He Wang · Sep 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

∂rΔ=2r−2M\partial_r\Delta = 2r-2M∂r​Δ=2r−2M

$\partial_r\Delta = 2r-2M$