Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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.

Geodesics continue while velocity lifts remain compact

Statement

Assume ACω, and let M be a Riemannian manifold without boundary. Let γ:I=(a,b)→M be an affinely parametrized geodesic on a nonempty open interval, where either endpoint may be infinite, and write z(t)=(γ(t),γ′(t))∈TM for its velocity lift.

  1. If b<∞ and there are t0∈I and a compact subset K⊆TM such that z(t)∈K whenever t0<t<b, then γ extends as a geodesic to an open interval with right endpoint strictly greater than b.
  2. If a>−∞ and there are t0∈I and a compact subset K⊆TM such that z(t)∈K whenever a<t<t0, then γ extends as a geodesic to an open interval with left endpoint strictly less than a.

Consequently, the velocity lift of a maximal geodesic leaves every compact subset of TM along each tail approaching a finite endpoint of its maximal interval.

Facts & Assumptions

Given: The data in the statement. The boundaryless convention is Boundaryless convention for geodesic flow and Hopf–Rinow.

[A1]
[F1]

The geodesic spray is a well-defined smooth vector field on TM uses [A1] to supply a smooth geodesic spray S on TM whose integral curves are exactly the velocity lifts of affinely parametrized geodesics.

[F2]

Applied to S, The fundamental theorem on flows supplies an open maximal-flow domain D⊆R×TM and a smooth map Φ:D→TM; the time curve s↦Φ(s,w) is the unique maximal integral curve through every w∈TM.

[F5]

Every nonempty finite set of real numbers has a positive minimum when all its members are positive (Every nonempty finite set of reals has a maximum and a minimum).

Proof

1.1A1F1F2F3

By [F1], z is an integral curve of S. By [F2], for every w∈TM one has (0,w)∈D. Since D is open, [F3] gives an open set U⊆TM containing w and an ε>0 such that (−ε,ε)×U⊆D. Thus the set A:={(ε,U):ε>0, U⊆TM open, (−ε,ε)×U⊆D} indexes an ambient-open cover (U(ε,U))(ε,U)∈A of TM, and hence of K.

2.1F4F5step 1.1

The tail hypothesis makes K nonempty. By [F4], finitely many indices (ε0,U0),…,(εn,Un)∈A cover K. By [F5], δ:=min⁡{ε0,…,εn}>0. If w∈K, then w∈Ui for some i, and ∣s∣<δ≤εi implies (s,w)∈D. Therefore (−δ,δ)×K⊆D. No pointwise family of choices was made: the index of the cover already contains both U and its admissible ε, and compactness returns a finite list of those pairs.

3.1F2F5step 2.1givenalgebra

Assume the right-endpoint hypotheses. Put c=max⁡{t0,b−δ/2}<b and t1=(c+b)/2. Then t1∈I, t1>t0, z1:=z(t1)∈K, and b−t1<δ/2. Step 2.1 makes s↦Φ(s,z1) an integral curve for ∣s∣<δ. By uniqueness in [F2], it agrees with s↦z(t1+s) wherever both are defined.

4.1F1F2step 3.1

Projecting the curve in step 3.1 to M gives a geodesic by [F1]. It agrees with γ on the overlap, so it glues smoothly to γ and defines a geodesic on I∪(t1−δ,t1+δ)=(a,t1+δ). Because t1+δ>b, this is the required extension past b. Notice that the new interval contains the formerly missing parameter value b; no value of γ at b was assumed.

5.1F1F2F5step 2.1step 3.1step 4.1

For a finite left endpoint, put c=min⁡{t0,a+δ/2}>a and t1=(a+c)/2. Then z(t1)∈K and t1−a<δ/2. The same maximal-flow curve, now using negative times, glues to z and projects to a geodesic on (t1−δ,b), whose left endpoint is strictly less than a. This proves claim 2. If γ were maximal, either extension would contradict maximality; contraposition gives the final consequence.

6.1A1F1step 1.1step 2.1step 4.1step 5.1∎

The empty manifold admits no geodesic with nonempty domain. In dimension zero the spray curves are stationary, and in dimension one the preceding argument is unchanged; no positive-dimensional coordinate was used. An empty K cannot contain the nonempty tail, while a one-member finite subcover is allowed and gives δ=ε0. Only finite endpoints are asserted, and steps 4.1 and 5.1 treat both endpoint directions. The sole choice principle is the stated ACω used through [F1]; the compact-cover argument itself is a ZF argument and makes no countable or arbitrary selection.

Remarks

  • Datar's proof of Proposition 20.2.2 gives the same endpoint-extension move for an integral curve once a subsequence converges in a compact set. Andrews, Theorem 11.5.1, printed pp.106--107, instead obtains a limiting base point from metric completeness and continues a radial geodesic there. Neither source states the finite-flow-box proof verbatim; the exact uniform compact argument above is derived from the published maximal-flow theorem [F2].
  • Compactness of the image in M alone would not suffice here: the initial condition for the spray is the full velocity lift in TM.

Depends on

Used by

Dependency tree · two levels

36 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