Solution (source code)

= Solution

Let a future-directed causal tangent in the ingoing chart be
$$
X=\dot v\,\partial_v+\dot r\,\partial_r+\dot\chi\,\partial_\chi.
$$
The chosen time orientation has $\dot v\geq0$; equality occurs only for the ingoing radial null direction, which has $\dot r<0$. Causality requires
$$
g(X,X)=-f\dot v^2+2\dot v\dot r
+r^2(\dot\chi-\Omega\dot v)^2\leq0.
$$
For $r_-<r<r_+$ one has $f<0$. The first and third terms are then nonnegative, so if $\dot v>0$ the inequality forces $\dot r<0$. If $\dot v=0$, it forces $\dot\chi=0$, and future direction again gives $\dot r<0$. Thus $r$ strictly decreases along every future causal curve in this region. No such curve can cross outward through $r=r_+$ into $r>r_+$, which proves the one-way causal disconnection characteristic of an <event horizon>.