LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

A maximal ODE solution cannot remain in a compact tube to a finite endpoint

Statement

Let $d \geq 1$ and $D \subseteq R \times R^{d}$ be open, and let $f : D \to R^{d}$ be continuous and locally Lipschitz in the state variable. There is no maximal solution $x : I \to R^{d}$ of $x^{'} = f (t, x)$ whose interval has a finite right endpoint $b$ and for which some $t_{0} \in I$ , $t_{0} < b$ , and compact set $C \subseteq D$ satisfy $(t, x (t)) \in C$ for every $t \in [t_{0}, b)$ . The compact tube condition supplies boundedness of $f$ along the graph and a limit point inside the open domain.

Facts & Assumptions

Given: The ODE, maximal solution, finite endpoint $b$ , and compact tube $C$ in the Statement.

[F1]

First-order systems, initial value problems, and solutions on intervals: a solution is differentiable on its interval, remains in $D$ , and satisfies $x^{'} (t) = f (t, x (t))$ .

[F2]

Extensions, maximal solutions, maximal intervals, and global solutions: maximality means that no solution on a strictly larger interval restricts to $x$ .

[F3]

A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value: a continuous real-valued function on a nonempty compact metric space is bounded.

[F4]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : a scalar function continuous on a closed interval and differentiable on its interior has a point where its derivative equals the interval's average rate of change; in particular, if the derivative is bounded in absolute value by $M$ , the function is $M$ -Lipschitz.

[F5]

The reals are complete: every Cauchy sequence of real numbers converges to a real number.

[F6]

In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones: compact subsets of Euclidean space are closed.

[F7]

Picard-Lindelöf local existence and uniqueness for first-order systems: for continuous locally state-Lipschitz $f$ on an open domain, an initial point in the domain has a local solution through it.

[F8]

Locally unique ODE solutions agree on overlaps and glue across a common endpoint: solutions through a common endpoint agree where they overlap and their adjacent pieces glue to a solution.

Proof

1.1givenF1F3F4construct

For each coordinate $f_{i}$ , compactness of $C$ and [F3] give a finite bound $M_{i}$ for $∣ f_{i} ∣$ on $C$ . Put $M : = \sum_{i = 1}^{d} M_{i}$ . For $s < t$ in $[t_{0}, b)$ , [F1] gives $∣ x_{i}^{'} (u) ∣ = ∣ f_{i} (u, x (u)) ∣ \leq M_{i}$ for every $u \in (s, t)$ ; [F4] yields $∣ x_{i} (t) - x_{i} (s) ∣ \leq M_{i} (t - s)$ . Summing coordinate differences shows $∥ x (t) - x (s) ∥_{2} \leq M (t - s)$ .

2.1F1F5F6step 1.1construct

Choose the explicit sequence $t_{n} : = b - (b - t_{0}) / (n + 1)$ . It increases to $b$ , and [F1] and step 1.1 make each coordinate of $x (t_{n})$ Cauchy. By [F5] each coordinate has a limit; call the resulting vector $x_{b}$ . The same Lipschitz estimate in step 1.1 implies $x (t) \to x_{b}$ as $t ↑ b$ . Thus $(t_{n}, x (t_{n})) \to (b, x_{b})$ in Euclidean space. Since every term lies in $C$ , [F6] gives $(b, x_{b}) \in C \subseteq D$ .

3.1F1F4F7step 2.1algebra

By [F7] there is a local solution $z$ through $(b, x_{b})$ . If $b \in I$ , continuity of the solution at its endpoint gives $x (b) = x_{b}$ ; if $b \notin I$ , define the endpoint value $x (b) : = x_{b}$ . For each coordinate and each $t < b$ sufficiently close to $b$ , the real mean value theorem [F4] applied to this continuous extension on $[t, b]$ gives a point $c \in (t, b)$ with $(x_{i} (b) - x_{i} (t)) / (b - t) = f_{i} (c, x (c))$ . Continuity of $f$ and $x (c) \to x_{b}$ makes this quotient tend to $f_{i} (b, x_{b})$ as $t ↑ b$ . Hence the left derivative at $b$ equals $f (b, x_{b})$ , which is also the right derivative of $z$ .

4.1F2F8step 3.1∎

The endpoint extension and $z$ agree at $b$ , and [F8] glues the original solution, its endpoint value, and $z$ into a solution on a strictly larger interval. This contradicts [F2], proving that no maximal solution can satisfy the stated finite-endpoint compact-tube conditions.

Depends on

Used by

A validated rational residual-tube certificate encloses an exact ODE solution Theorem

Dependency tree · two levels

66 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Gerald Teschl, Ordinary Differential Equations and Dynamical Systems, Chapter 2 (standard reference, not scraped)
Jiri Lebl, Basic Analysis I, Section 6.3 (standard reference, not scraped)