Israel (1967): static vacuum black holes are Schwarzschild

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements (Aristotle, by Harmonic), with full knowledge of the source and of the intended meaning. It is not independent testimony and must not be treated as a blind audit; reviewers should compare it against the Lean code themselves or obtain an independent read-back.

$M$ is any type with a topology and a charted-space structure on $\mathbb R^4$ that is a $C^\infty$ manifold (no Hausdorff/second-countable/connected assumption). $g,F$ are arbitrary bilinear fields, $T$ a vector field, $\varphi:\mathbb R\to M\to M$ any map, $E$ an asymptotically flat end for $(g,F,\varphi)$ (data $R>0$, $\psi$, $C$ with: $\psi$ a diffeomorphism from $\Omega_R=\{|\vec y|>R\}$ onto the open set $\psi(\Omega_R)$, $\psi(y+se_0)=\varphi_s(\psi y)$, $|g_{\mu\nu}-\eta_{\mu\nu}|\le C/|\vec y|$, $|\partial_\sigma g_{\mu\nu}|\le C/|\vec y|^2$, $|F_{\mu\nu}|\le C/|\vec y|^2$ in $\psi$-coordinates). Hypothesis $h$ says: $g$ is Lorentzian (orthonormal basis of signature $(-,+,+,+)$ at each point); $g$ and $F$ have $C^\infty$ components in every chart; $F$ is antisymmetric; $T$ is continuous and $g(T,T)<0$; the coordinate Einstein–Maxwell equations ($G_{\mu\nu}=2(F_{\mu\alpha}F_\nu{}^\alpha-\frac14g_{\mu\nu}F^2)$, $\partial_\mu(\sqrt{|\det g|}F^{\mu\nu})=0$, $dF=0$) hold at every point of every chart; $\varphi$ is a jointly smooth $\mathbb R$-action preserving $g$ and $F$; the set $D=I^+(\psi(\Omega_R))\cap I^-(\psi(\Omega_R))$ (chronological sets via $C^1$ future-timelike curves, $g(\gamma',\gamma')<0$, $g(\gamma',T)<0$, on $[0,1]$) is globally hyperbolic (no closed future causal $C^1$ curve in $D$, and $J^+_D(p)\cap J^-_D(q)$ compact for $p,q\in D$); the complement of $I^-(\psi(\Omega_R))$ is nonempty; the frontier of $I^-(\psi(\Omega_R))$ is connected and nonempty.

Additional hypotheses. $F_x=0$ for every $x\in M$; and the stationary flow is static on $D$: for every atlas chart and every chart point $y$ mapping into $D$, the lowered generator components $k_\mu$ satisfy $k_\lambda(\partial_\mu k_\nu-\partial_\nu k_\mu)+k_\mu(\partial_\nu k_\lambda-\partial_\lambda k_\nu)+k_\nu(\partial_\lambda k_\mu-\partial_\mu k_\lambda)=0$.

Conclusion. There is $m>0$ such that $D$ is isometric to the Kerr–Newman DOC with parameters $(m,0,0)$ (Schwarzschild exterior $\{r>2m\}$; here $r$ is the Euclidean spatial radius).

"Isometric to the Kerr–Newman DOC with parameters $(m,a,e)$" means: there exist a real $\beta$ and a map $\Psi:\mathbb R^4\to M$ with a two-sided inverse $\chi$ between $\{y:r(y)>r_+\}$ and $D$, both $C^\infty$ on these sets, such that for all $y$ with $r(y)>r_+$ the pulled-back metric matrix $(\Psi^*g)(y)$ equals $\eta+f k k^{\mathsf T}$ (Kerr–Newman in Kerr–Schild form, with $r$, $k$, $f$ as in the coordinate definitions) and $(\Psi^*F)(y)=\cos\beta\,F^{KN}(y)+\sin\beta\,\star F^{KN}(y)$; here $r_+=m+\sqrt{m^2-a^2-e^2}$.