Alphabeta Math
TheoremStatement: 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.

Metric completeness implies geodesic completeness

Statement

Assume ACω. If a connected Riemannian manifold M without boundary is complete for its Riemannian distance dg, then M is geodesically complete: every maximal geodesic is defined on all of R.

Facts & Assumptions

Given: A connected boundaryless Riemannian manifold (M,g) whose metric space (M,dg) is complete. The boundaryless restriction is Boundaryless convention for geodesic flow and Hopf–Rinow.

[A1]
[F1]

Under [A1], Geodesically complete Riemannian manifold formulates geodesic completeness using the unique maximal geodesic through each initial vector, and Existence uniqueness and smooth dependence of geodesics supplies that uniqueness. Constant curves are geodesics by Geodesic of an affine connection, Geodesics have constant speed for a metric-compatible connection gives constant speed, and Affine reparametrization of a geodesic is a geodesic gives the affine rescalings used below.

[F2]

A finite endpoint of a maximal unit-speed geodesic produces a Cauchy curve gives the exact two-parameter Cauchy-tail estimate at a finite endpoint. Cauchy sequence in a metric space, Complete metric space: every Cauchy sequence converges in the space, and Convergence of a sequence in a metric space: xkx iff d(xk,x)0 in R say that a Cauchy sequence in (M,dg) converges to a point of M and give the corresponding epsilon condition.

[F3]

Riemannian distance is a metric supplies the triangle inequality, and The riemannian distance topology is the manifold topology identifies metric convergence with manifold convergence.

[F5]

Local comparison of a riemannian metric with the euclidean metric gives cv22gx(v,v) uniformly over a compact set in one chart, for some c>0.

[F6]

Under [A1], Geodesics continue while velocity lifts remain compact extends a geodesic whenever its velocity lift remains in a compact subset of TM along a tail approaching a finite endpoint.

Proof

1.1

Suppose, contrary to the conclusion, that M is not geodesically complete. By [F1], some initial vector has a maximal geodesic γ:I=(a,b)M, with 0I, for which at least one endpoint is finite. Reversing the parameter by [F1] if necessary, assume b<.

A1F1assume-contra
2.1

Let c=γg, constant by [F1]. If c=0, then in particular γ(0)=0. The constant curve on R at γ(0) is a geodesic with those same initial data by [F1], so initial-value uniqueness says that it is the unique maximal geodesic and contradicts the finite endpoint in step 1.1. Hence c>0. Define η:cIM by η(s)=γ(s/c). Then [F1] makes η a unit-speed geodesic with finite right endpoint β=cb. Any extension of η past β would, after the inverse rescaling, extend γ past b, so η is maximal.

F1step 1.1algebra
3.1

Put sk=ββ/(k+2) for kN. Since 0<β<, each sk(0,β)cI and skβ. The Cauchy-tail estimate [F2] makes (η(sk)) a Cauchy sequence: after the time belonging to a given ε, every sufficiently large sk lies in that tail. Completeness in [F2] therefore supplies qM with η(sk)q in dg.

F2step 2.1algebra
4.1

In fact the whole curve tends to q as sβ. Given ε>0, apply [F2] with ε/2 to obtain a tail time T. By convergence and skβ, choose one k with sk>T and dg(η(sk),q)<ε/2. Then [F2] and the triangle inequality [F3] give, for every T<s<β, dg(η(s),q)dg(η(s),η(sk))+dg(η(sk),q)<ε. Thus metric convergence of the entire tail, and hence manifold convergence by [F3], is established without selecting a sequence of witnesses.

F2F3step 3.1
5.1

Put m=dimM and first suppose m1. Choose one coordinate chart x:Ux(U) about q. Since x(U) is Euclidean-open, [F4] gives ρ>0 with Bρ(x(q))x(U); put R=ρ/2 and r=R/2. Then the closed Euclidean ball BR(x(q)) lies in x(U). Let K0=x1[BR(x(q))]. By [F4], K0 is compact. Step 4.1 implies that η(s) lies in the smaller set x1[Br(x(q))]K0 for all sufficiently late s.

F3F4step 4.1choose
6.1

Let Θ:π1(U)x(U)×Rm be the induced tangent-bundle chart. By [F5], there is c0>0 such that c0v22gy(v,v) for yK0. Since η has unit speed, its fibre coordinate satisfies η(s)2c01/2 on the late tail. The coordinate set P=BR(x(q))×Bc01/2(0)R2m is closed and bounded, hence compact by [F4]. Its inverse-chart image K:=Θ1(P) is a compact subset of TM by [F4], and the late velocity lift (η(s),η(s)) lies in K.

F4F5step 5.1
7.1

If m1, applying [F6] to the compact set K from step 6.1 extends η past β, contrary to its maximality in step 2.1. If m=0, every tangent vector is zero, so the nonzero speed c>0 from step 2.1 was already impossible. Thus the incomplete maximal geodesic chosen in step 1.1 cannot exist.

A1F1F6step 1.1step 2.1step 6.1contradiction
8.1

A connected empty manifold is allowed: it has no initial vectors and is geodesically complete vacuously. The zero-dimensional nonempty case was handled in step 7.1, and dimension one is the case m=1 of the compact product construction. Zero initial velocity was separated in step 2.1; the nonempty maximal interval contains 0, so a finite right endpoint is positive and the explicit sequence in step 3.1 is defined. Reversal in step 1.1 handles the finite left-endpoint case, and neither endpoint is assumed to belong to the maximal open interval. The only choice principle is [A1], used through [F1] and [F6] for the library's global tangent-bundle/geodesic construction. The one limit, chart, two radii, and finite-dimensional compact set are finitely many existential witnesses and need no further choice. The result is one implication, not an equivalence. The contradiction in step 7.1 discharges the assumption in step 1.1 and proves geodesic completeness by [F1].

A1F1step 1.1step 2.1step 3.1step 5.1step 6.1discharge-contradiction: step 1.1step 7.1

Source locator

Datar proves (1)(2) in Theorem 19.2.1 on pp.141--142 by taking a Cauchy sequence on a unit-speed geodesic and then using a uniform local exponential domain near its limit. Andrews proves the same implication in Theorem 11.5.1, printed pp.106--107, by identifying the limiting tail as a radial minimizing geodesic. The proof here keeps their Cauchy-limit core and uses the preceding compact velocity-lift continuation lemma for the final extension; steps 5.1--6.1 prove its compactness hypothesis rather than assuming it.

Depends on

Used by

Dependency tree · two levels

87 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