TheoremStatement: Literature-sourcedProof: AI-generatedprecheck 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.1L1L2choose

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$ .

2.1L4step 1.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$ .

3.1F1L1L3step 2.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.

The fundamental theorem for autonomous smooth ODEs

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources