All sixteen coordinate Ricci components of the Kerr metric vanish on the regular domain

For all real $M,a$, every point $x=(t,r,\theta,\varphi)\in\mathbb R^4$ with

and all indices $b,d\in\{0,1,2,3\}$,

where $R_{bd}=$ ricciOf (gKerr M a) (giKerr M a) b d x is the coordinate Ricci tensor of the specification layer: the standard formula $R_{bd}=\sum_i(\partial_i\Gamma^i_{bd}-\partial_d\Gamma^i_{bi}+\sum_j(\Gamma^i_{ij}\Gamma^j_{bd}-\Gamma^i_{dj}\Gamma^j_{bi}))$ with $\Gamma^a_{bc}=\tfrac12\sum_k\hat g^{ak}(\partial_cg_{kb}+\partial_bg_{kc}-\partial_kg_{bc})$, evaluated on the Boyer-Lindquist Kerr metric $g$ and its closed-form inverse $\hat g$ with Mathlib's slice derivatives.

This is Ricci-flatness of the Boyer-Lindquist Kerr family on the regular coordinate domain of the formalization, for arbitrary real parameters $M,a$. It is not a global Lorentzian-manifold statement and it is not restricted to the black-hole regime. All sixteen components are proved separately; no symmetry of $R_{bd}$ is used or asserted.

Formalization Note Only the generic definitions appear in the statement; no closed form is mentioned. Read together with ginv_mul_g_Kerr (the inverse is genuine) and the differentiability theorems hdgKerr_all, hdchrKerr_all (no junk derivative values), as packaged in vacuum_Kerr.