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.

Smooth dependence of ODE solutions on parameters

Statement

Let $F (t, x, λ)$ be smooth in $(x, λ)$ on an open time-state-parameter domain. Near any base data $(t_{0}, x_{0}, λ_{0})$ there are a compact time interval $I$ and a neighbourhood $W$ of $(x_{0}, λ_{0})$ such that, for every $(y, λ) \in W$ , the solution of

$x^{'} (t) = F (t, x (t), λ), x (t_{0}) = y,$

is defined on $I$ , and the resulting solution map is smooth in the pair $(y, λ)$ .

Facts & Assumptions

Given: A smooth parameter-dependent vector field $F (t, x, λ)$ and base data $(t_{0}, x_{0}, λ_{0})$ .

[L1]

Solutions depend smoothly on initial data for smooth systems on a common compact interval (Smooth dependence of solutions on initial data).

Proof

technique · direct

1.1

Introduce the augmented variable $(x, λ) \in R^{n + m}$ and define the autonomous-in-parameter system below.

givenconstruct

${(\begin{array}{c} x \\ λ \end{array})}^{'} = (\begin{array}{c} F (t, x, λ) \\ 0 \end{array}) .$

Along every solution the parameter component remains constant, so solving this augmented system is equivalent to solving the original parameter-dependent ODE with fixed parameter $λ$ . [given, construct]

2.1

The augmented right-hand side is smooth in the initial data $(y, λ)$ , so [L1] applies on a common compact local time interval and makes the augmented solution map smooth in $(y, λ)$ . Projecting to the $x$ -component preserves that smoothness, which gives the claimed smooth dependence of solutions on initial state and parameter.

L1step 1.1∎

Depends on

Smooth dependence of solutions on initial data

Used by

Dependency tree · two levels

5 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.3-§4.4 (standard reference, not scraped)