Exact Vacuum Atlas I: seven vacuum certificates and four coordinate relations

Points of $\mathbb R^4$ are written $x=(x_0,x_1,x_2,x_3)$; a coordinate metric is a $4\times4$ matrix $g=(g_{ij})$ of real functions of $x$, and a candidate inverse $\hat g$ is another such matrix. $\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$. $\mathrm{CoordRelation}(g_1,g_2,U,V,\Phi,\Psi,J)$ (bundle Atlas_Core_Relation) asserts: $\Psi(\Phi(x))=x$ for $x\in U$; $\Phi(\Psi(y))=y$ for $y\in V$; $\Phi$ maps $U$ bijectively onto $V$; $\Phi$ is $C^\infty$ on $U$ and $\Psi$ is $C^\infty$ on $V$; for every $x\in U$ and all indices $k,i$ the slice $u\mapsto\Phi(x[x_i:=u])_k$ has derivative $J(x)_{ki}$ at $u=x_i$ (a genuine derivative, not a default value); and $J(x)^{\mathsf T}\,g_2(\Phi(x))\,J(x)=g_1(x)$ for all $x\in U$. The theorem is the conjunction of eleven statements.

Seven vacuum certificates (all parameters arbitrary reals; $\Sigma=r^2+a^2\cos^2\theta$, $\Delta=r^2-2Mr+a^2$):

1. $\mathrm{VacuumCertificate}(\eta,\eta,\mathbb R^4)$ for the Cartesian Minkowski metric $\eta=\mathrm{diag}(-1,1,1,1)$ (bundle Atlas_Minkowski_Cartesian, constant components, candidate inverse $\eta$ itself);
2. $\mathrm{VacuumCertificate}(g^{\rm sph},\hat g^{\rm sph},\{r>0,0<\theta<\pi\})$ for the spherical Minkowski metric $g^{\rm sph}$ (bundle Atlas_Minkowski_Spherical, coordinates $(t,r,\theta,\varphi)$): $g_{tt}=-1$, $g_{rr}=1$, $g_{\theta\theta}=r^2$, $g_{\varphi\varphi}=r^2\sin^2\theta$, other entries $0$, candidate inverse $\mathrm{diag}(-1,1,1/r^2,1/(r^2\sin^2\theta))$;
3. $\forall M$: $\mathrm{VacuumCertificate}(g^{\rm std}_M,\hat g^{\rm std}_M,\{r>0,r\neq2M,0<\theta<\pi\})$ for the standard Schwarzschild metric $g^{\rm std}_M$ (bundle Atlas_Schwarzschild_Defs, coordinates $(t,r,\theta,\varphi)$): $g_{tt}=-(1-2M/r)$, $g_{rr}=1/(1-2M/r)$, $g_{\theta\theta}=r^2$, $g_{\varphi\varphi}=r^2\sin^2\theta$, other entries $0$, with candidate inverse $\hat g^{tt}=-1/(1-2M/r)$, $\hat g^{rr}=1-2M/r$, $\hat g^{\theta\theta}=1/r^2$, $\hat g^{\varphi\varphi}=1/(r^2\sin^2\theta)$;
4. $\forall M$: $\mathrm{VacuumCertificate}(g^{\rm EF}_{M,1},\hat g^{\rm EF}_{M,1},\{r>0,0<\theta<\pi\})$ (ingoing, $g_{vr}=1$) for the Eddington–Finkelstein family $g^{\rm EF}_{M,\varepsilon}$ (bundle Atlas_Schwarzschild_Defs, coordinates $(w,r,\theta,\varphi)$ with $w=v$ for $\varepsilon=1$ ingoing and $w=u$ for $\varepsilon=-1$ outgoing): $g_{ww}=-(1-2M/r)$, $g_{wr}=g_{rw}=\varepsilon$, $g_{\theta\theta}=r^2$, $g_{\varphi\varphi}=r^2\sin^2\theta$, other entries $0$, with candidate inverse $\hat g^{wr}=\hat g^{rw}=\varepsilon$, $\hat g^{rr}=1-2M/r$, $\hat g^{\theta\theta}=1/r^2$, $\hat g^{\varphi\varphi}=1/(r^2\sin^2\theta)$, other entries $0$;
5. $\forall M$: $\mathrm{VacuumCertificate}(g^{\rm EF}_{M,-1},\hat g^{\rm EF}_{M,-1},\{r>0,0<\theta<\pi\})$ (outgoing, $g_{ur}=-1$);
6. $\forall M,a$: $\mathrm{VacuumCertificate}(g^{\rm BL}_{M,a},\hat g^{\rm BL}_{M,a},\{\Sigma\neq0,\Delta\neq0,\sin\theta\neq0\})$ for 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$);
7. $\forall M,a$: $\mathrm{VacuumCertificate}(g^{\rm in}_{M,a},\hat g^{\rm in}_{M,a},\{\Sigma\neq0,\sin\theta\neq0\})$ for the ingoing (Kerr's original, advanced) Kerr metric $g^{\rm in}$ of bundle Atlas_Kerr_InDefs, read off from Visser's line element $ds^2=-F\,(dv+a\sin^2\theta\,d\varphi)^2+2\,(dv+a\sin^2\theta\,d\varphi)(dr+a\sin^2\theta\,d\varphi)+\Sigma\,(d\theta^2+\sin^2\theta\,d\varphi^2)$, $F=1-2Mr/\Sigma$, with the half-Hessian convention ($g_{vr}=1$): in coordinates $(v,r,\theta,\varphi)=(x_0,x_1,x_2,x_3)$ and with $A=a\sin^2\theta$, $g_{vv}=-F$, $g_{vr}=g_{rv}=1$, $g_{v\varphi}=g_{\varphi v}=(1-F)A$, $g_{r\varphi}=g_{\varphi r}=A$, $g_{\theta\theta}=\Sigma$, $g_{\varphi\varphi}=(2-F)A^2+\Sigma\sin^2\theta$, all remaining entries $0$; its candidate inverse $\hat g^{\rm in}$ has $\hat g^{vv}=a^2\sin^2\theta/\Sigma$, $\hat g^{vr}=\hat g^{rv}=(r^2+a^2)/\Sigma$, $\hat g^{v\varphi}=\hat g^{\varphi v}=\hat g^{r\varphi}=\hat g^{\varphi r}=-a/\Sigma$, $\hat g^{rr}=\Delta/\Sigma$ with $\Delta=r^2-2Mr+a^2$, $\hat g^{\theta\theta}=1/\Sigma$, $\hat g^{\varphi\varphi}=1/(\Sigma\sin^2\theta)$, all remaining entries $0$ (both matrices are symmetric; every symmetric counterpart is listed).

Four coordinate relations, each with its explicit map, inverse, overlap/image and Jacobian:

8. R1, $\forall M$: standard Schwarzschild to ingoing EF, $\Phi(t,r,\theta,\varphi)=(t+r+2M\log\lvert r-2M\rvert,r,\theta,\varphi)$ on $U=V=\{r>0,r\neq2M,0<\theta<\pi\}$, $J_{01}=1+\frac{2M}{r-2M}$;
9. R2, $\forall M$: standard Schwarzschild to outgoing EF, $\Phi=(t-r-2M\log\lvert r-2M\rvert,r,\theta,\varphi)$, same overlap, $J_{01}=-(1+\frac{2M}{r-2M})$;
10. R3, $\forall M,a$: Boyer–Lindquist to ingoing Kerr, $\Phi=(t+r+H_1(r),r,\theta,-\varphi-H_2(r))$ with the explicit $H_1=M\log|\Delta|+2M^2K$, $H_2=aK$ ($K'=1/\Delta$ in all three branches of $M^2-a^2$), on $U=V=\{\Sigma\neq0,\Delta\neq0,\sin\theta\neq0\}$, $J$ with rows $(1,\frac{r^2+a^2}\Delta,0,0),(0,1,0,0),(0,0,1,0),(0,-\frac a\Delta,0,-1)$;
11. R4: spherical chart $\{r>0,0<\theta<\pi,0<\varphi<2\pi\}$ to Cartesian $\mathbb R^4\setminus\{y=0,x\ge0\}$, $\Phi=(t,r\sin\theta\cos\varphi,r\sin\theta\sin\varphi,r\cos\theta)$ with its explicit inverse and Jacobian.

The goal theorem of the mission: a machine-checked coordinate-level atlas of the three basic vacuum solutions in seven standard forms on explicit open domains (no domain condition excludes the Schwarzschild interior $0<r<2M$ for $M>0$, either sign of $\Delta$ or negative $r$ for Kerr, the regular-coordinate portion of $r=2M$ with $0<\theta<\pi$ for $M>0$ (Eddington–Finkelstein), or the points with $\Delta=0$ at which $\Sigma\neq0$ and $\sin\theta\neq0$ (ingoing Kerr); ExactVacuumAtlas.Release01.coverage exhibits points with $r=2M$, $\Delta<0$ and $\Delta=0$ under its sufficient parameter conditions, and it is not claimed that every parameter pair has points of each kind; the polar axis, angular identifications and global horizon geometry are not included), with the four changes of coordinates proved as explicit maps rather than existence statements. It only assembles the seven certificates and four relations proved as separate nodes. Not contained: any manifold, atlas-gluing, horizon, causal, maximal-extension or classification statement, any coordinate-covariance theorem for the coordinate Ricci tensor, or any relation to a manifold Ricci tensor of Mathlib (none exists in the pinned version).

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 $(-,+,+,+)$.