Vacuum certificate: Kerr in Boyer–Lindquist coordinates, all real $M,a$

Let $M,a$ be arbitrary real numbers, $\Sigma=r^2+a^2\cos^2\theta$, $\Delta=r^2-2Mr+a^2$. Consider $g^{\rm BL}_{M,a}$, the Boyer–Lindquist Kerr metric (platform definition KerrBL_Kerr_Metric, coordinates $(t,r,\theta,\varphi)=(x_0,x_1,x_2,x_3)$): $g_{tt}=-\big(1-\tfrac{2Mr}{\Sigma}\big)$, $g_{rr}=\tfrac{\Sigma}{\Delta}$, $g_{\theta\theta}=\Sigma$, $g_{\varphi\varphi}=\big(r^2+a^2+\tfrac{2Ma^2r\sin^2\theta}{\Sigma}\big)\sin^2\theta$, $g_{t\varphi}=g_{\varphi t}=-\tfrac{2Mar\sin^2\theta}{\Sigma}$, other entries $0$, with its closed-form candidate inverse $\hat g$ ($\hat g^{rr}=\Delta/\Sigma$, $\hat g^{\theta\theta}=1/\Sigma$ and a $(t,\varphi)$ block with denominator $\Sigma\Delta\sin^2\theta$), on the regular domain $U^{\rm BL}_{M,a}=\{x:\ \Sigma\neq0,\ \Delta\neq0,\ \sin\theta\neq0\}$. Then

$\mathrm{VacuumCertificate}(g,\hat g,U)$ (bundle Atlas_Core_Certificate) is the conjunction of eight obligations: $U$ is open and nonempty; $g_{ij}(x)=g_{ji}(x)$ for $x\in U$; $\hat g(x)\,g(x)=I_4$ for every $x\in U$; every component of $g$ and of $\hat g$ is $C^\infty$ on $U$; at every $x\in U$ there is an invertible matrix $E$ with $E^{\mathsf T}g(x)E=\mathrm{diag}(-1,1,1,1)$ (Lorentzian signature); and all sixteen components $R_{bd}(x)$, $b,d\in\{0,1,2,3\}$, of the coordinate Ricci tensor built from $g$ and $\hat g$ vanish for $x\in U$.

Row 6 of the atlas. The inverse identity and the vanishing of the sixteen Ricci components are the published, Proved platform theorems KerrBL.ginv_mul_g_Kerr and KerrBL.ricci_flat_Kerr of the 2026-09 Kerr mission; this certificate adds the open/nonempty domain, symmetry, $C^\infty$ regularity of metric and inverse, and the Lorentzian frame on the whole regular domain with no positivity condition on $\Delta$ (frameP where $\Delta>0$, frameN where $\Delta<0$). Which signs of $\Delta$ occur depends on $(M,a)$: a negative-$\Delta$ point is exhibited under $a^2<M^2$ in ExactVacuumAtlas.Release01.coverage; it is not claimed that both signs occur for every real parameter pair.

Formalization Note Everything is coordinate-level on $\mathbb R^4$ (points are functions $\{0,1,2,3\}\to\mathbb R$): no manifold, chart gluing, periodicity of $\varphi$, horizon, causal or global statement is made. Partial derivatives are Mathlib's deriv of coordinate slices; the certificates' $C^\infty$ obligations make every derivative used a genuine derivative. Units $G=c=1$, signature $(-,+,+,+)$.