TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21

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.

Peano local existence for a continuous first-order system

Statement

Let $n \in N$ with $n \geq 1$ , let $D \subseteq R \times R^{n}$ be open, let $F : D \to R^{n}$ be continuous, and let $(t_{0}, x_{0}) \in D$ . Then the IVP $x^{'} = F (t, x)$ , $x (t_{0}) = x_{0}$ , has a local solution. No uniqueness is asserted.

Facts & Assumptions

Given: The open domain, continuous field, and initial data in the Statement.

[L1]

Let $h > 0$ , let $F$ be continuous on $[t_{0}, t_{0} + h] \times \overline{B} (x_{0}, r)$ and bounded there by $M$ , and suppose $h M \leq r$ . Euler polygonal approximations with positive mesh sizes tending to zero remain in that cylinder, are uniformly bounded, and are $M$ -Lipschitz (Euler polygonal approximations for a continuous ODE are uniformly bounded and equicontinuous).

[L2]

If $n \geq 1$ , then on a nonempty compact interval a uniformly bounded equicontinuous sequence of continuous $R^{n}$ -valued curves has a uniformly convergent subsequence with continuous limit (A uniformly bounded equicontinuous sequence of $R^{n}$ -valued curves on a nonempty compact interval has a uniformly convergent subsequence).

[L3]

Uniform convergence of Riemann-integrable functions permits passage of the limit under the integral (A uniform limit of Riemann-integrable functions is Riemann integrable, and its integral is the limit of their integrals).

[L4]

A continuous map on a compact metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[L5]

Let $n \geq 1$ , let $D \subseteq R \times R^{n}$ be open, let $F : D \to R^{n}$ be continuous, and let $I$ be an order-convex interval with at least two elements. A continuous curve $x : I \to R^{n}$ whose graph lies in $D$ and contains $(t_{0}, x_{0})$ solves the IVP if and only if $x (t) = x_{0} + \int_{t_{0}}^{t} F (s, x (s)) d s$ for every $t \in I$ (A first-order initial value problem is equivalent to its Volterra integral equation).

[L6]

A closed bounded subset of $R^{m}$ , for $m \geq 1$ , is compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[L7]

The Euclidean norm is continuous, composites of continuous maps are continuous, and a continuous real function on a nonempty compact metric space is bounded and attains its maximum (The finite and reverse triangle inequalities for a norm; and for $n \geq 1$ every norm $N$ on $R^{n}$ satisfies $N (x) \leq C ∥ x ∥_{1}$ and is Lipschitz, hence continuous, for $d_{2}$ , Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, claim 1, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

Proof

technique · constructive

1.1

Since $D$ is open and contains $(t_{0}, x_{0})$ , choose $a, r > 0$ so that $C = [t_{0} - a, t_{0} + a] \times \overline{B} (x_{0}, r)$ lies in $D$ . This cylinder is closed and bounded in $R^{n + 1}$ , hence compact by [L6]. By [L7], the continuous function $(t, x) \mapsto ∥ F (t, x) ∥_{2}$ attains a maximum $M \geq 0$ on $C$ . Set $h = a$ if $M = 0$ , and $h = \min {a, r / M}$ otherwise. Then $h > 0$ and $h M \leq r$ .

givenL6L7chooseconstruct

2.1

Construct forward Euler polygons on $[t_{0}, t_{0} + h]$ with mesh tending to zero. Fact [L1] applies with the cylinder from step 1.1, and [L2] gives a subsequence converging uniformly to a continuous curve $x_{+}$ .

step 1.1L1L2construct

2.2

Apply the same construction to the reflected field $\tilde{F} (s, z) = - F (2 t_{0} - s, z)$ on $[t_{0}, t_{0} + h] \times \overline{B} (x_{0}, r)$ . It has the same bound $M$ , so [L1] and [L2] give a uniform limit $z$ ; define $x_{-} (t) = z (2 t_{0} - t)$ on $[t_{0} - h, t_{0}]$ .

step 1.1L1L2construct

3.1

Let $η_{m}$ be the forward mesh and let $τ_{m} (s)$ be the left endpoint of the mesh cell containing $s$ . The Euler construction gives $x_{m} (t) = x_{0} + \int_{t_{0}}^{t} F (τ_{m} (s), x_{m} (τ_{m} (s))) d s .$ By [L1], $∣ s - τ_{m} (s) ∣ \leq η_{m}$ and $∥ x_{m} (s) - x_{m} (τ_{m} (s)) ∥_{2} \leq M η_{m}$ . Uniform convergence to $x_{+}$ and uniform continuity of $F ∣_{C}$ from [L4] therefore make the displayed integrands converge uniformly to $F (s, x_{+} (s))$ . Applying [L3] componentwise gives the Volterra equation for $x_{+}$ . The identical reflected argument gives the oriented Volterra equation for $x_{-}$ .

step 2.1step 2.2L1L3L4algebra

4.1

Both half-intervals are nondegenerate and order-convex, both limit graphs lie in $C \subseteq D$ , and both limits contain $(t_{0}, x_{0})$ , so [L5] makes $x_{+}$ and $x_{-}$ solutions. Their piecewise union is continuous at $t_{0}$ , and the two differential equations give the same one-sided derivative $F (t_{0}, x_{0})$ there. Hence the union is differentiable at $t_{0}$ and is a solution on $[t_{0} - h, t_{0} + h]$ .

step 3.1L5discharge-construct∎

Depends on

Used by

y'=2√|y| has a continuum of delayed-start solutions through the origin Counterexample

Dependency tree · two levels

86 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

Gerald Teschl, Ordinary Differential Equations and Dynamical Systems, Ch. 2 (standard reference, not scraped)
Jiri Lebl, Basic Analysis I, Section 6.3 (standard reference, not scraped)