Vacuum certificates transport along metrics that agree on the domain

Let $n$ be a natural number, $g,\hat g$ coordinate metrics on $\mathbb R^{n+1}$, $U\subseteq\mathbb R^{n+1}$, and suppose $\mathrm{VacuumCertificate}(g,\hat g,U)$. If $g',\hat g'$ are coordinate metrics with $g'_{ij}=g_{ij}$ and $\hat g'_{ij}=\hat g_{ij}$ pointwise on $U$ for all $i,j$, then $\mathrm{VacuumCertificate}(g',\hat g',U)$. $\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_{n+1}$ 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=\eta_n=\mathrm{diag}(-1,1,\dots,1)$ with $n$ entries $+1$ (Lorentzian signature); and all $(n+1)^2$ ordered components $R_{bd}(x)$, $b,d\in\{0,\dots,n\}$, of the coordinate Ricci tensor built from $g$ and $\hat g$ vanish for $x\in U$.

Lets a certificate proved for one presentation of the data be reused for another presentation equal on the domain (Minkowski spherical = Schwarzschild at $M=0$; standard Schwarzschild = Boyer–Lindquist Kerr at $a=0$). Since the Ricci tensor is built from slice derivatives, the agreement on the open set $U$ suffices. This is equality-based transport on the same domain in total dimension $n+1$, not coordinate-covariance transport.

Formalization Note Dimension $n+1$; agreement is Set.EqOn on $U$ for every component.