Every coordinate slice of every Kerr metric component is differentiable, with the closed-form derivative

For all real $M,a$, every point $x$ of the regular domain and all indices $l,i,j\in\{0,1,2,3\}$, the slice

of the Boyer-Lindquist Kerr metric component $g_{ij}$ along coordinate $l$ has, at $u=x_l$, the derivative dgKerr M a l i j evaluated at the atoms $(r,\sin\theta,\cos\theta,\Sigma,\Delta)$ of $x$, in the sense of Mathlib's HasDerivAt.

This is the metric-derivative certification of Layer II: it establishes both that the derivative exists (so the generic $\partial_l g_{ij}$ of the specification layer is a genuine derivative, not Mathlib's junk value) and that it equals the generated closed form. The companion statement in terms of pd is pdgKerr_all.