The generic Ricci tensor of the Kerr metric equals the explicit closed-form expression

For all real $M,a$, every point $x$ of the regular domain 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 generic derivative-based coordinate Ricci tensor of the specification layer, and RicciKerr is the explicit expression of KerrBL_Kerr_ClosedForms.

This is the bridge from the specification to the explicit expressions whose vanishing Layer III proves. The explicit Ricci expression is never assumed: this theorem derives it from the generic definitions together with the Christoffel bridge and the Christoffel-derivative certification.