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.

Existence uniqueness and smooth dependence of geodesics

Statement

Assume ACω. For every (p,v)TM there is a unique maximal geodesic γp,v:Ip,vM with γp,v(0)=p and γp,v(0)=v. Each Ip,v is an open interval containing zero, the domain G={(t,p,v):tIp,v}R×TM is open, and (t,p,v)γp,v(t) is smooth on G.

Facts & Assumptions

Given: An initial tangent vector vTpM.

[F1]

The Axiom of Countable Choice (ACω) is the assumed ACω, and The geodesic spray is a well-defined smooth vector field on TM supplies a smooth spray on the resulting smooth manifold TM, with integral curves exactly the geodesic velocity lifts.

[F2]

Through each point there is a unique maximal integral curve gives a unique maximal integral curve through every point of a smooth manifold, while Local existence, uniqueness, and smooth dependence for manifold integral curves supplies its local initial-value uniqueness and smooth dependence.

[F3]

The fundamental theorem on flows makes the union of those maximal integral-curve domains open and their evaluation map smooth.

Proof

1.1

Apply [F2] to the spray at the point vTM. It gives a unique maximal integral curve Zv:IvTM on an open interval containing zero. By [F1], Zv is the velocity lift of γp,v:=πZv. Since Zv(0)=v, its base point is p, and the base component of the spray equation gives γp,v(0)=v.

F1F2given
2.1

If a geodesic with these initial data existed on a larger interval, [F1] would make its velocity lift an integral curve of the spray extending Zv, contrary to maximality. The same lift argument and integral-curve uniqueness prove uniqueness on every common interval. Thus Ip,v=Iv and the geodesic is uniquely maximal.

F1F2step 1.1
3.1

By [F3], {(t,v):tIv} is open in R×TM and (t,v)Zv(t) is smooth. This is exactly G after writing v together with its determined base point p. In induced tangent-bundle coordinates the projection π(x,w)=x is smooth, so composing gives the asserted smooth geodesic evaluation.

F1F3step 1.1step 2.1
4.1

For v=0, [F1] makes Zv stationary and the maximal geodesic is the constant curve on all of R. In dimension zero every initial vector is zero; for empty M there are no initial vectors. Each maximal domain is open, so it has no included finite endpoints. All conclusions concern one supplied initial vector at a time. The only choice principle is the declared ACω, inherited exactly from the smooth-manifold structure on TM; [F2]–[F3] then apply without another family selection.

F1F2F3step 1.1step 2.1step 3.1

Depends on

Used by

Dependency tree · two levels

18 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