Kerr vacuum theorem in Boyer-Lindquist coordinates (headline)

Let $M,a\in\mathbb R$ and let $x=(t,r,\theta,\varphi)\in\mathbb R^4$ lie in the regular coordinate domain

Let $g$ be the Boyer-Lindquist Kerr metric and $\hat g$ its closed-form inverse (KerrBL_Kerr_Metric), and let $\Gamma$ and $R$ be the generic coordinate Christoffel symbols and Ricci tensor of the specification layer (KerrBL_CoordGeometry), built from $g$, $\hat g$ and Mathlib's slice derivatives. Then all of the following hold:

1. $\hat g$ is a left inverse of $g$ at $x$: $\sum_k\hat g^{ik}(x)g_{kj}(x)=\delta_{ij}$ for all $i,j$;
2. for all $l,i,j$ the slice $u\mapsto g_{ij}(x[l\mapsto u])$ is differentiable at $u=x_l$;
3. for all $l,i,j,k$ the slice $u\mapsto\Gamma^i_{jk}(x[l\mapsto u])$ is differentiable at $u=x_l$;
4. the coordinate Ricci tensor vanishes:

This is the goal theorem of the mission: a machine-checked coordinate verification that the Boyer-Lindquist Kerr family is Ricci-flat on the regular coordinate domain used by the formalization, for arbitrary real $M,a$. Clauses 1-3 make the statement self-contained: they exclude a trivialising inverse and exclude Mathlib's junk value for non-differentiable slices, so that clause 4 is a statement about the genuine coordinate Ricci tensor. The theorem does not assert a Lorentzian manifold, a global chart, the signature, positivity of $M$, the black-hole bound $|a|\le M$, anything on the axis $\sin\theta=0$ or at $\Sigma=0$, $\Delta=0$, or any coordinate-independent curvature statement.

Formalization Note The trusted base is the 45-line generic layer and the metric transcription (source-locked to the project certificate); every closed form is bridged by proof. The theorem depends only on the axioms propext, Classical.choice, Quot.sound.