CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-21

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.

Nearby initial values share one Picard–Lindelöf time interval and one state cylinder

Statement

Under the hypotheses of Picard-Lindelof at $(t_{0}, x_{0})$ , there are $h, r, η > 0$ such that every initial value $(s, y)$ with $∣ s - t_{0} ∣ < η$ and $∥ y - x_{0} ∥_{2} < η$ has a unique solution on $[s - h, s + h]$ , and all these solution graphs lie in one compact time-state cylinder.

Facts & Assumptions

Given: A compact cylinder contained in the open ODE domain and a smaller cylinder with positive distance from its boundary.

[L1]

On a cylinder with bound $M$ , state-Lipschitz constant $L$ , $h M \leq r$ , and $L h < 1$ , Picard-Lindelöf gives exactly one solution on the full interval of half-length $h$ whose graph lies in that cylinder (Picard-Lindelöf local existence and uniqueness for first-order systems).

[L2]

A continuous real-valued function on a nonempty compact metric space has bounded image and attains its extrema (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

Proof

technique · direct

1.1

On the larger compact cylinder, [L2] bounds $∥ F ∥_{2}$ by a common $M$ , while local state-Lipschitz continuity and a finite compact cover give a common $L$ ; the smaller cylinder has a positive spatial and temporal boundary margin.

givenL2

2.1

Choose one radius $r > 0$ below the spatial margin and one $h > 0$ below the temporal margin so that $h M \leq r$ and $L h < 1$ ; then [L1] applies with these same data to every initial point in the smaller cylinder, giving the asserted common time and graph cylinder.

step 1.1L1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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, Ch. 2 (standard reference, not scraped)
Jiri Lebl, Basic Analysis I, Section 6.3 (standard reference, not scraped)