False statementConstruction: Literature-sourcedVerification: 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.

Pointwise local existence does not force one global uniform time interval

Statement

False claim: if an autonomous smooth ODE has a local solution through every initial point of $R^{n}$ , then there is one time $h > 0$ that works for all initial points at once.

Facts & Assumptions

Given: The ODE $x^{'} = x^{2}$ on $R$ .

[L1]

Nearby initial values share a uniform local time interval only locally in the initial data (Nearby initial values share one Picard–Lindelöf time interval and one state cylinder).

[L2]

Smooth autonomous ODEs have unique local solutions (The fundamental theorem for autonomous smooth ODEs).

Refutation

technique · direct

1.1

For each initial value $x (0) = a > 0$ , the unique solution is [L2] $x_{a} (t) = a / (1 - a t)$ , defined only for $t < 1 / a$ . Thus every initial point has a local solution by [L2].

2.1

If one positive time $h$ worked for all initial values, then taking [L1, step 1.1, assume-hyp] $a > 1 / h$ would give a solution through $a$ defined on $[- h, h]$ . But step 1.1 shows the maximal positive existence time is $1 / a < h$ , a contradiction. This does not conflict with [L1], because [L1] is a neighbourhood theorem, not a global one over all of $R$ .

L1step 1.1assume-hyp

3.1

Therefore pointwise local existence does not imply one uniform time [step 2.1] interval for all initial data.

step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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.2 (standard reference, not scraped)
Chin-Lung Wang, Banach Calculus, §4.2 (standard reference, not scraped)