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.
A compactly supported cutoff of an incomplete vector field is complete
Example
Choose a smooth bump function with on and . Then
agrees with the incomplete field near the origin but is complete.
Facts & Assumptions
Given: A bump function equal to on and supported in .
Smooth bump functions with prescribed compact support exist (A manifold bump for a compact set inside an open set).
A Picard–Lindelöf initial value problem has a unique maximal solution (Every Picard–Lindelöf initial value problem has one maximal solution on an open interval).
A bounded derivative on an interval gives a Lipschitz bound (If is continuous on an interval and at every interior point, then for all , so is Lipschitz with constant and uniformly continuous on ).
Continuous functions on compact metric spaces are bounded (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value), and closed bounded Euclidean sets are compact (Heine-Borel in : with the Euclidean metric a subset of 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).
A solution with a sequence of graph points in a compact interior region approaching a finite endpoint extends beyond that endpoint (A solution whose graph approaches a compact interior region at a finite endpoint extends past that endpoint).
Verification
Apply [L1] to to obtain the required smooth bump. Put . It is smooth, equals on , and vanishes off . Hence . Its derivative is continuous and zero off , so [L4] bounds globally. By [L3], is Lipschitz.
Fix any initial value and take its maximal solution from [L2]. Since , [L3] on the interval between and gives . If , set for . These times increase to , and the graph points lie in the compact rectangle , where . The ODE domain is all of , so [L5] extends the solution past , contrary to maximality. Therefore . Reflecting time applies the same argument to and gives . This uses an explicitly defined sequence and no choice assumption.
Every integral curve of is thus global, so is complete. In contrast, solves with for and diverges as , so the original field is incomplete. This verifies both the local agreement and the claimed change in completeness.
Depends on
- A manifold bump for a compact set inside an open set
- Every Picard–Lindelöf initial value problem has one maximal solution on an open interval
- If $f$ is continuous on an interval $I$ and $|f'| \le M$ at every interior point, then $|f(x) - f(y)| \le M|x-y|$ for all $x,y \in I$, so $f$ is Lipschitz with constant $M$ and uniformly continuous on $I$
- A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{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
- A solution whose graph approaches a compact interior region at a finite endpoint extends past that endpoint
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
67 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
- Will J. Merry, Differential Geometry (standard reference, not scraped)
- John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (standard reference, not scraped)