Alphabeta Math
PropositionStatement: 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 maximal solution domain is open

Statement

Let V:U→Rn be a smooth vector field on an open set U, and for each x0∈U let x( ⋅ ;x0) denote the unique maximal solution of x′=V(x) with x(0)=x0. Then the maximal solution domain

Ω:={(t,x0)∈R×U:t lies in the maximal interval of x( ⋅ ;x0)}

is open in R×U. On Ω, the evaluation map Φ(t,x0):=x(t;x0) is smooth in the state variable and continuous jointly in (t,x0).

Facts & Assumptions

Given: A smooth vector field V:U→Rn and its maximal solutions.

[L1]

Autonomous smooth ODEs have local smooth flows near every point (The fundamental theorem for autonomous smooth ODEs).

[L3]

Solutions depend continuously on nearby initial data on common compact local intervals (Continuous dependence of ODE solutions on initial data and parameters).

Proof

technique · direct
1.1L1choose

Let (t∗,x∗)∈Ω and put p:=Φ(t∗,x∗). By [L1], applied at the [L1, choose] state point p, there exist δ>0 and an open neighbourhood W⊆U of p such that every y∈W has a unique solution on [−δ,δ], and these solutions vary smoothly with y.

2.1L3step 1.1

By [L3], for initial states x sufficiently close to x∗, the solution [L3, step 1.1] Φ( ⋅ ,x) is defined at least on a compact interval around t∗ and its value at time t∗ lies in W. Therefore for every such x and every ∣s∣<δ, the solution continued from time t∗ by the local flow of step 1.1 is defined at time t∗+s. Hence all pairs (t∗+s,x) with ∣s∣<δ and x near x∗ lie in Ω.

3.1L1L2L3step 2.1∎

Step 2.1 gives an open neighbourhood of (t∗,x∗) contained in Ω, [L1, L2, L3, step 2.1] so Ω is open. On that neighbourhood, the evaluation map is the composite of the continuous time-t∗ map with the local smooth flow from step 1.1, hence is jointly continuous and smooth in the state variable. Since (t∗,x∗) was arbitrary, the same holds on all of Ω.

Depends on

Used by

Dependency tree · two levels

14 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