TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-29

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.

The fundamental theorem for autonomous smooth ODEs

Statement

Let $U \subseteq R^{n}$ be open and let $V : U \to R^{n}$ be smooth. For every $x_{0} \in U$ there exist $h > 0$ and an open neighbourhood $W \subseteq U$ of $x_{0}$ such that:

for every $y \in W$ there is a unique solution $Φ (\cdot, y)$ of $x^{'} = V (x)$ on $[- h, h]$ with $Φ (0, y) = y$ ;
the map $Φ : (- h, h) \times W \to U, Φ (t, y) = Φ_{t} (y),$ is smooth in $y$ and $C^{1}$ in $t$ , with $\partial_{t} Φ (t, y) = V (Φ (t, y))$ and $Φ (0, y) = y$ .

This is the local smooth flow of the autonomous vector field $V$ .

Facts & Assumptions

Given: A smooth vector field $V : U \to R^{n}$ and a base point $x_{0} \in U$ .

[F1]

The equation $x^{'} = V (x)$ is an autonomous ODE (Autonomous ordinary differential equations).

[L1]

Picard-Lindelof gives unique local solutions (Picard-Lindelöf local existence and uniqueness for first-order systems).

[L2]

Nearby initial values share one common compact local time interval (Nearby initial values share one Picard–Lindelöf time interval and one state cylinder).

[L3]

Every initial value problem has a unique maximal solution (Every Picard–Lindelöf initial value problem has one maximal solution on an open interval).

[L4]

On a common compact local interval, solutions depend smoothly on the initial state (Smooth dependence of solutions on initial data).

Proof

technique · direct

1.1

Since a smooth vector field is continuous and locally Lipschitz, [L1] applies [L1, L2, choose] at $(0, x_{0})$ . The uniform local existence result [L2] therefore gives $h > 0$ and an open neighbourhood $W$ of $x_{0}$ such that every $y \in W$ has a unique solution on $[- h, h]$ , and all these solution graphs stay inside one compact cylinder in $R \times U$ .

L1L2choose

2.1

Define $Φ (t, y)$ to be that unique solution value at time $t$ . By [L4] the [L4, step 1.1] map is smooth in the initial state variable $y$ on $(- h, h) \times W$ . For each fixed $y$ , the curve $t \mapsto Φ (t, y)$ is a solution, so it is differentiable in $t$ and satisfies $\partial_{t} Φ (t, y) = V (Φ (t, y))$ with $Φ (0, y) = y$ .

L4step 1.1

3.1

The uniqueness in step 1.1 is exactly the local uniqueness from [L1], and [F1, L1, L3, step 2.1] the maximal-solution theorem [L3] records that these local flows are the local pieces of unique maximal trajectories rather than unrelated solution branches.

F1L1L3step 2.1∎

Depends on

Used by

A constant vector field has translation solutions Example
The harmonic oscillator as a first-order system Example
A smooth Euclidean vector field need not be complete False statement
Pointwise local existence does not force one global uniform time interval False statement
The maximal solution domain is open Proposition
The fundamental theorem for nonautonomous smooth ODEs Theorem

Dependency tree · two levels

20 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

Nigel Hitchin, Differentiable Manifolds, Appendix §10.3, Theorem 10.7 (standard reference, not scraped)
Chin-Lung Wang, Banach Calculus, §4.4 (standard reference, not scraped)