Strong causality bounds the auxiliary length of causal curves contained in a compact set

(A finite precompact causally convex cover.) For each point of $K$, choose an adapted chart and a closed coordinate ball compactly contained in it. Use its open half-radius ball as the neighborhood in strong causality [L1], obtaining a causally convex open $V$ around the point contained in that smaller ball. The collection of all such admissible $V$, charts and radii covers $K$; compactness selects finitely many members, with no choice of a family indexed by all points of $K$. Write them $V_j\subset U_j$ for $1\le j\le m$, with $U_j$ their open coordinate balls and $\overline{U_j}$ compactly contained in their respective larger charts. Define $M_j={\sup }_{U_j}{x}_j^0-{\inf }_{U_j}{x}_j^0<\mathrm{\infty }$, $H_j={\max }_{\overline{U_j}}\mathrm{\parallel }h{\mathrm{\parallel }}_{\mathrm{e},\mathrm{o}\mathrm{p}}<\mathrm{\infty }$, and $c_j=\max \{1,\sqrt{H_j}{K}_j\}$. Then [L2] gives $\sqrt{h({\gamma }^{\mathrm{\prime }},{\gamma }^{\mathrm{\prime }})}\le c_j(x_j^0\circ \gamma {)}^{\mathrm{\prime }}$ almost everywhere on every subarc in $U_j$. If $K$ is empty the conclusion is immediate with $L(K)=0$; henceforth use the finite cover for nonempty $K$.

(The visit of a causal curve to one causally convex set is one interval.) Let $\gamma :[a,b]\to K$ be future causal and fix $j$. If $s<t$ with $\gamma (s),\gamma (t)\in V_j$, then $\gamma ([s,t])\subseteq V_j$ by the defining property of $V_j$; hence the parameter set ${\gamma }^{-1}(V_j)$ is an interval in $[a,b]$: whenever it contains $s<t$ it contains $[s,t]$. In particular ${\gamma }^{-1}(V_j)$ has at most one connected component and is an interval $I_j$, possibly empty.

(Length over a compact part of one visit.) For every compact nondegenerate $[s,t]\subset I_j$, the curve image lies in $V_j\subset U_j$, so the fundamental theorem in [L4] and step 1.1 give ${\int }_s^t\sqrt{h({\gamma }^{\mathrm{\prime }},{\gamma }^{\mathrm{\prime }})}\le c_j{\int }_s^t(x_j^0\circ \gamma {)}^{\mathrm{\prime }}=c_j(x_j^0(\gamma (t))-x_j^0(\gamma (s)))\le c_j{M}_j$. The restricted speed is integrable, since the coordinate derivatives are integrable and dominate it. The relatively open visit $I_j={\gamma }^{-1}(V_j)$ need not contain its endpoints; only compact subintervals contained in $I_j$ are used in this argument.

(Finite compact-interval cover and length sum.) The relatively open intervals $I_j$ form a finite cover of the compact parameter interval $[a,b]$. A sufficiently fine finite partition has each of its closed subintervals contained in some $I_j$, by a Lebesgue number of this cover. Assign each partition piece to the least such $j$; this requires only finitely many choices. For every index used, let $J_j$ be the closed interval from the least left endpoint to the greatest right endpoint of its assigned pieces. As $I_j$ is an interval, $J_j\subset I_j$; these finitely many compact intervals cover $[a,b]$. Step 3.1 applies on each $J_j$. The nonnegative integral over their union is at most the sum of their integrals, so the global speed is integrable and ${\mathrm{\ell }}_h(\gamma )\le {\sum }_j{\int }_{J_j}\sqrt{h({\gamma }^{\mathrm{\prime }},{\gamma }^{\mathrm{\prime }})}\le {\sum }_{j=1}^m{c}_j{M}_j=:L(K)<\mathrm{\infty }$, with unused indices contributing no interval. If $a=b$ the length is zero. For an arclength-parametrized curve ${\mathrm{\ell }}_h(\gamma )=b-a$, giving the second assertion. No possibly missing visit endpoint is evaluated.

(Imprisonment form.) There is no sequence of future causal curves with images in a fixed compact $K$ and auxiliary lengths tending to infinity: each length is bounded by the same $L(K)$ from step 4.1. Equivalently, there is no family of $h$-arclength-parametrized future causal curves with images in $K$ and parameter-domain lengths tending to infinity.

(Conclusion.) The finite causally convex cover, the interval visit estimate and the nonnegative integral bound establish both assertions, with exactly the declared calculus premises.