Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-04
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.

Local existence, uniqueness, and smooth dependence for manifold integral curves

Statement

Let X be a smooth vector field on M and let pM. Then there exist h>0, an open neighbourhood U of p, and a smooth map

Φ:(h,h)×UM

such that for every qU, the curve tΦ(t,q) is the unique integral curve of X on (h,h) with initial value Φ(0,q)=q.

Facts & Assumptions

Given: A smooth vector field X on M and a point pM.

[L1]

Chart maps are diffeomorphisms onto open subsets of Euclidean space (Chart maps are diffeomorphisms onto Euclidean open sets).

[L2]

In a chart, a smooth vector field has smooth coordinate components (Smoothness of a vector field is equivalent to smooth coordinate components).

[L3]

A smooth autonomous vector field on an open subset of Rn has a local smooth flow depending smoothly on the initial point (The fundamental theorem for autonomous smooth ODEs).

Proof

technique · direct
1.1

Choose a chart (V,x) around p. By [L1], x:Vx(V)Rn is a diffeomorphism onto an open set, and by [L2] the vector field XV corresponds to a smooth Euclidean vector field X~ on x(V).

L1L2given
2.1

Apply [L3] to X~ at the point x(p). This gives h>0, an open neighbourhood Wx(V) of x(p), and a smooth map Φ~:(h,h)×Wx(V) whose time slices are the unique integral curves of X~.

L3step 1.1choose
3.1

Set U:=x1(W) and define Φ(t,q):=x1(Φ~(t,x(q))). Because x and x1 are smooth by [L1], Φ is smooth. Each curve tΦ(t,q) is an integral curve of X and satisfies Φ(0,q)=q.

L1step 2.1construct
4.1

If another curve in M through qU solved the same initial-value problem, its coordinate expression under x would solve the Euclidean problem for X~ with the same initial value. Uniqueness in [L3] then forces the two curves to agree.

L3step 3.1
5.1

Therefore X has unique local integral curves depending smoothly on the initial point.

step 3.1step 4.1

Depends on

Used by

Dependency tree · two levels

19 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