TheoremStatement: Literature-sourcedProof: 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.

Picard-Lindelöf local existence and uniqueness for first-order systems

Statement

Let $D \subseteq R \times R^{n}$ be open, let $F : D \to R^{n}$ be continuous and locally Lipschitz in the state variable, and let $(t_{0}, x_{0}) \in D$ . Then a unique local solution of the IVP exists on some interval around the initial time. More quantitatively, if $h, r > 0$ make

$[t_{0} - h, t_{0} + h] \times \overline{B} (x_{0}, r) \subseteq D,$

if $∥ F ∥_{2} \leq M$ and $F$ has state-Lipschitz constant $L$ on this cylinder, and if $h M \leq r$ and $L h < 1$ , then there is exactly one solution on $[t_{0} - h, t_{0} + h]$ through $(t_{0}, x_{0})$ whose graph lies in the cylinder. Any two solutions through the same initial data agree on every common subinterval containing $t_{0}$ .

In particular, a unique local solution exists on an interval around the initial time.

Facts & Assumptions

Given: The IVP in the Statement and a compact cylinder about $(t_{0}, x_{0})$ on which $F$ is bounded by $M$ and state-Lipschitz with constant $L$ .

[L1]

A contraction of a nonempty complete metric space has exactly one fixed point (A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point).

[L2]

A curve solves the IVP if and only if it satisfies the associated Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).

[L3]

Continuous $R^{n}$ -valued curves on a nonempty compact interval are complete in the supremum metric (Continuous $R^{n}$ -valued curves on a nonempty compact interval form a complete supremum-metric space).

[L4]

Under $h M \leq r$ , the Picard operator preserves the closed curve ball (A bounded vector field makes the Picard operator preserve a sufficiently short closed curve ball).

[L5]

Under $L h < 1$ , the Picard operator is a contraction (A state-Lipschitz vector field makes the Picard operator a contraction when $L h < 1$ ).

[L6]

Every interval in the real line is connected (The connected subspaces of $R$ with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in $R$ ").

Proof

technique · direct

1.1

Choose $r > 0$ and then $h > 0$ so the cylinder lies in $D$ , $h M \leq r$ , and $L h < 1$ ; the closed curve ball is nonempty and complete by [L3], is invariant by [L4], and its Picard operator is a contraction by [L5], so [L1] gives exactly one fixed point.

givenL1L3L4L5

2.1

By [L2] the fixed point is a solution. Any other solution cannot leave the state ball before time $h$ , by the same first-exit estimate as [L4], so it is the same fixed point there. For two solutions on a larger common interval, their agreement set is nonempty and closed, and local repetition of this argument makes it open; the common interval is connected by [L6], so they agree throughout it.

step 1.1L2L4L6∎

Depends on

Used by

Dependency tree · two levels

57 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)