The closed-form matrix is a left inverse of the Boyer-Lindquist Kerr metric

For all real $M,a$, every point $x$ of the regular domain ($\Sigma\neq0$, $\Delta\neq0$, $\sin\theta\neq0$) and all indices $i,j\in\{0,1,2,3\}$,

where $g$ is the Boyer-Lindquist Kerr metric and $\hat g$ the closed-form candidate inverse of KerrBL_Kerr_Metric.

This is Layer I of the mission. The generic Christoffel symbols take the inverse as data, so the Ricci-flatness statement would be vacuous for a wrong candidate (for $\hat g=0$ every $\Gamma$ vanishes). This theorem removes that loophole and is bundled into the headline vacuum_Kerr.

Formalization Note Stated componentwise with if i = j then 1 else 0. Only the left inverse $\hat g g=I$ is asserted; the two-sided statement follows mathematically but is not part of the text.