Vacuum certificate: Schwarzschild in ingoing Eddington–Finkelstein coordinates, all real $M$

Let $M$ be an arbitrary real number. Consider the ingoing form $g^{\rm EF}_{M,1}$ ($g_{vr}=1$) of 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$, on $U^{\rm EF}=\{x:\ r>0,\ 0<\theta<\pi\}$ ($w,\varphi$ arbitrary; for $M>0$ it includes the regular-coordinate portion of $r=2M$ with $0<\theta<\pi$, but not the polar axis, angular identifications or global horizon geometry). 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 4 of the atlas; for $M>0$ the domain includes the regular-coordinate portion of $r=2M$ with $0<\theta<\pi$ (a witness point is given in ExactVacuumAtlas.Release01.coverage).

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