$\partial_r\Sigma = 2r$

For all real $a,r,c$ the function $u\mapsto\Sigma(a,u,c)=u^2+a^2c^2$ has derivative $2r$ at $u=r$, in the sense of Mathlib's HasDerivAt.

Atom lemma of Layer II: the derivative of the abbreviation $\Sigma$ with respect to $r$, consumed by the metric-derivative theorem hdgKerr_all through the chain rule.