LemmaStatement: Literature-sourcedProof: AI-generatedprecheck pending

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Escape lemma for manifold flows: a finite maximal time forces the integral curve to leave every compact set

Statement

Assume the Axioms of Countable Choice and Dependent Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain). Let $M$ be a smooth manifold without boundary, let $X$ be a smooth vector field on $M$ (A smooth vector field is a smooth section of the tangent bundle), let $p \in M$ and let $γ : (α, β) \to M$ be the unique maximal integral curve of $X$ with $γ (0) = p$ (Through each point there is a unique maximal integral curve, Integral curves of a vector field). If $β < + \infty$ then for every compact set $K \subseteq M$ (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) there is $s \in (α, β)$ such that $γ (t) \notin K$ for every $t \in (s, β)$ . Dually, if $α > - \infty$ then for every compact $K$ there is $s$ such that $γ (t) \notin K$ for every $t \in (α, s)$ .

Facts & Assumptions

Given: A smooth manifold $M$ without boundary, a smooth vector field $X$ , a point $p$ , the maximal integral curve $γ : (α, β) \to M$ with $γ (0) = p$ , a compact set $K \subseteq M$ , and the assumption $β < + \infty$ .

[L1]

Local flows with uniform time: for every $q \in M$ there exist $h > 0$ , an open neighborhood $U$ of $q$ and a smooth map $Φ : (- h, h) \times U \to M$ whose time slices are the unique integral curves of $X$ (Local existence, uniqueness, and smooth dependence for manifold integral curves).

[L2]

Maximality: the maximal integral curve $γ$ has domain $(α, β)$ equal to the union of the domains of all integral curves of $X$ through $p$ ; in particular no integral curve through $p$ is defined on an interval strictly containing $(α, β)$ (Through each point there is a unique maximal integral curve, Integral curves of a vector field).

[L3]

Every sequence in a compact subset $K$ of a Hausdorff manifold has a convergent subsequence. Indeed, the closures in $K$ of its tails are nonempty closed sets with the finite-intersection property, so compactness gives a point $q$ in their intersection. A chart at $q$ supplies the countable neighborhood basis of coordinate balls of radii tending to zero; recursively taking the least index beyond the preceding index whose term lies in that ball gives a subsequence converging to $q$ . This proves the needed sequential compactness without invoking a global metrization theorem (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Smooth manifolds and their smooth charts).

Proof

technique · contradiction

1.1assume-contragiven

(Assume a compact set is visited near the endpoint.) Suppose the assertion fails for $K$ : there are $t_{k} \in (α, β)$ with $t_{k} \to β$ and $γ (t_{k}) \in K$ ; passing to a subsequence we may assume $t_{k}$ is strictly increasing to $β$ .

2.1step 1.1L1L3choose

(A limit point and a local flow.) By sequential compactness of $K$ [L3] there is a subsequence, renamed $γ (t_{k})$ , converging to some $q \in K$ . Apply [L1] at $q$ : there are $h > 0$ , an open neighborhood $U$ of $q$ and a smooth $Φ : (- h, h) \times U \to M$ whose slices are integral curves. Since $γ (t_{k}) \to q$ , for some $k$ both $γ (t_{k}) \in U$ and $β - t_{k} < h$ hold.

3.1step 2.1L1L2discharge-contradiction∎

(Extension beyond the maximal time.) Define $\tilde{γ} : (α, t_{k} + h) \to M$ by $\tilde{γ} (t) : = γ (t)$ for $t < t_{k}$ and $\tilde{γ} (t) : = Φ (t - t_{k}, γ (t_{k}))$ for $t \in [t_{k}, t_{k} + h)$ . The two pieces agree at $t_{k}$ ; on the overlap near $t_{k}$ they are both integral curves with the same value at $t_{k}$ , so they agree by uniqueness of integral curves [L1], and $\tilde{γ}$ is an integral curve of $X$ through $p$ . Since $t_{k} + h > β$ , its domain strictly contains $(α, β)$ , contradicting maximality [L2]. Hence no such sequence exists, which is the assertion; the past-end assertion is the same argument applied to $- X$ (the maximal integral curve of $- X$ through $p$ is $t \mapsto γ (- t)$ , with endpoint $- α$ ).

Remarks

Where each hypothesis is used. Second countability enters only through metrizability of $M$ , which converts compactness of $K$ into sequential compactness; the local flow is used twice: to extend the curve beyond a finite endpoint and to identify the two pieces on their overlap.
Use. In Smooth Cauchy temporal splitting: a global temporal function with Cauchy levels and an orthogonal complete flow this escape statement turns a finite maximal time of a flow line into a contradiction with the divergence of the volume time, giving completeness of the temporal gradient field.

Escape lemma for manifold flows: a finite maximal time forces the integral curve to leave every compact set

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources