Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-04
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.

Compactly supported time-dependent vector fields have global evolution on a compact time interval

Statement

Let JR be a compact interval, and let Xt be a smooth time-dependent vector field on M such that

tJsupp(Xt)

is contained in a compact subset KM. Then there is a global evolution operator Ψt,s:MM for all s,tJ.

Facts & Assumptions

Given: A compact interval J, a smooth time-dependent vector field Xt on M, and a compact set K containing all supports supp(Xt) for tJ.

[L1]

Smooth time-dependent vector fields have unique local smooth evolution operators (Time-dependent vector fields have local smooth evolution operators).

[L2]

Local evolution operators satisfy the two-time cocycle law (Time-dependent evolution satisfies the two-time cocycle law).

[L3]

Outside the support of Xt, the vector field Xt vanishes (Smooth sections, local sections, and support).

Proof

technique · direct
1.1

Let γ:(a,b)M be a maximal solution of γ˙(t)=Xt(γ(t)) with initial time sJ. If γ(t0)K for some t0(a,b), then Xt(γ(t0))=0 for every tJ by [L3], so the constant curve through γ(t0) also solves the equation. Uniqueness therefore forces γ to be constant on the connected component of {t(a,b):γ(t)K} containing t0. Thus every nonconstant part of the trajectory stays inside K.

L3given
2.1

Suppose b<supJ. Choose times tnb. If infinitely many γ(tn) lie in K, compactness of K gives a subsequence converging to some qK. Otherwise γ(tn)K for all large n, and step 1.1 makes those tail values constant on a neighbourhood of b; hence γ(tn)q for some qMK. Applying [L1] at (b,q) gives ε>0, an open neighbourhood U of q, and a local evolution operator Ψt,s for s,t(bε,b+ε). Choose n large enough that tn(bε,b) and γ(tn)U. Then tΨt,tn(γ(tn)) is a solution on (bε,b+ε). On the common interval (bε,b) it agrees with γ by uniqueness, because both solve the same equation and have the same value at time tn. This extends γ past b, contradicting maximality.

L1step 1.1choose
3.1

The same argument excludes a left endpoint larger than infJ. Therefore every maximal solution with initial time in J exists on all of J.

step 2.1
4.1

Define Ψt,s(p) to be the value at time t of the unique solution starting from p at time s. Step 3.1 makes this global on J, and [L2] supplies the cocycle law. Hence Ψt,s:MM is the desired global evolution operator.

L2step 3.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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