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 of geodesically convex neighborhoods

Statement

Assume ACω. Let (M,g) be a boundaryless Riemannian manifold. An open set W⊆M is called strongly geodesically convex here when, for every ordered pair (x,y)∈W×W, there is a unique affinely parametrized geodesic γx,y:[0,1]→M that globally minimizes length from x to y, its image lies in W, and (x,y,t)↦γx,y(t) is smooth.

Every point of M has a strongly geodesically convex neighbourhood. More precisely, the neighbourhood may be chosen inside any prescribed open neighbourhood of the point, and it may be chosen so that every piecewise smooth curve attaining the global minimum between two of its points is a monotone reparametrization of the displayed connector. Every nonempty intersection of a positive finite family of strongly geodesically convex open sets is again strongly geodesically convex.

Facts & Assumptions

Given: A point p of the boundaryless Riemannian manifold and, for the relative form, an open neighbourhood O of p.

[A1]
[F1]

Under [A1], Existence of normal neighborhoods, Normal neighborhood and normal coordinate chart, and Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans give an orthonormal normal coordinate chart z=(z1,…,zn) centred at p, which may be restricted into O. Properties of normal coordinates at the center gives z(p)=0 and Γijk(p)=0.

[F2]

Under [A1], The exponential domain is open and the exponential map is smooth makes the total exponential map smooth on an open neighbourhood of the zero section, and The differential of exp at zero is the identity gives its vertical differential at 0p. The coordinate Choice-free smooth inverse function theorem in Euclidean space turns an invertible coordinate derivative into a local diffeomorphism; Existence uniqueness and smooth dependence of geodesics supplies the same unique geodesic evaluation used by the exponential map.

[F4]

Coordinate geodesic equation is the coordinate geodesic equation. Geodesics have constant speed for a metric-compatible connection gives constant Riemannian speed. Extreme value theorem: a continuous real function on a nonempty compact subset of R attains a greatest and a least value gives an attained maximum of a continuous real function on [0,1].

[F5]

Under [A1], Sufficiently short geodesic segments are uniquely minimizing says that every radial segment inside a normal exponential ball is globally minimizing and characterizes every equal-length piecewise smooth competitor as a monotone radial reparametrization. The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space supplies product neighbourhoods inside an open subset of M×M.

Proof

technique · direct
1.1F1algebra

If n=dim⁡M≥1, take from [F1] an orthonormal normal chart z:V→z(V) centred at p and restricted so that V⊆O. Define Bjk(q)=δjk−∑izi(q)Γijk(q). At p this smooth symmetric matrix is the identity by [F1]. By continuity, after shrinking V, one has ∣Bjk(q)−δjk∣<1/(2n) for every q∈V and every j,k. Thus, for a≠0, ∑j,kBjk(q)ajak≥∣a∣22−12n(∑j∣aj∣)2≥12∣a∣22>0, where the last inequality is the finite Cauchy--Schwarz calculation (∑j∣aj∣)2≤n∑j(aj)2. Hence B is positive definite throughout V.

1.2F2given

Let E be the total exponential domain and set Φ:E→M×M by Φ(q,v)=(q,exp⁡qv). In tangent-bundle and product coordinates at (p,0p), [F2] and the identity exp⁡q(0q)=q give DΦ(p,0p)(X,Y)=(X,X+Y), whose inverse is (A,D)↦(A,D−A). Applying the Euclidean inverse theorem in those charts gives an open neighbourhood D of (p,0p) on which Φ is a diffeomorphism onto an open neighbourhood of (p,p). Intersecting D with the inverse images of V under the base and exponential projections preserves these properties and ensures that (q,v)∈D implies q,exp⁡qv∈V.

1.3given

Let W1,…,Wm be a positive finite family of strongly geodesically convex open sets with nonempty intersection I. It is open. For x,y∈I, every Wi supplies a normalized globally minimizing geodesic from x to y. The uniqueness clause for W1 makes all these geodesics equal, so their common image lies in every Wi and hence in I. The connector on I×I×[0,1] is the restriction of the smooth connector for W1, and its global uniqueness is unchanged. Hence I is strongly geodesically convex.

2.1F2F3step 1.2

In the tangent-bundle coordinates used in step 1.2, choose an open coordinate ball G about p, with compact closure K⊆V, and R>0 such that PR={(q,v):q∈G, ∣v∣2<R}⊆D. The compactness assertions in [F3] apply to K. Take their constants 0<c≤C. Choose 0<ρ<cR, then choose 0<r<R with Cr<ρ, and put Pr={(q,v):q∈G, ∣v∣2<r}. For q∈G, the Riemannian ball Bρ(0q) lies in the fibre of PR, whereas the fibre of Pr lies in Bρ(0q). Restricting the diffeomorphism Φ∣D therefore shows that exp⁡q:Bρ(0q)→Uq:=exp⁡q(Bρ(0q)) is a normal-ball diffeomorphism.

3.1F2F3F5step 1.2step 2.1

Since Pr is open, Φ(Pr) is an open neighbourhood of (p,p). By [F5], choose a positive coordinate radius s so small that W:={q∈G:∣z(q)∣2<s} satisfies W×W⊆Φ(Pr). For (x,y)∈W×W, write Φ−1(x,y)=(x,v(x,y)) and put γx,y(t)=exp⁡x(tv(x,y)). The inverse and exponential maps are smooth, so this curve depends smoothly on (x,y,t). Step 2.1 gives ∣v(x,y)∣gx<ρ and W⊆Ux. Moreover (x,tv(x,y))∈Pr⊆D for 0≤t≤1, so the entire connector lies in V even before the sharper conclusion below.

4.1F4step 1.1step 3.1

Fix x,y∈W. If x=y, injectivity of Φ∣D gives v(x,x)=0x and the connector is constant. Suppose x≠y, and set h(t)=∑i(zi(γx,y(t)))2. With aj(t)=d(zj∘γx,y)/dt, differentiating twice and using the coordinate geodesic equation [F4] gives h′′(t)=2∑j,k(δjk−∑izi(γx,y(t))Γijk(γx,y(t)))aj(t)ak(t)=2Bγx,y(t)(a(t),a(t)). The geodesic has nonzero constant speed by [F4], so a(t)≠0 and step 1.1 gives h′′(t)>0 for 0<t<1.

5.1F4step 3.1step 4.1assume-contradischarge-contradiction

If the connector left W, [F4] would give a point t0∈(0,1) where h attains its maximum, because h(0),h(1)<s2 while some value is at least s2. At an interior maximum, for small u>0, [h(t0+u)−2h(t0)+h(t0−u)]/u2≤0, and passage to the limit gives h′′(t0)≤0, contradicting step 4.1. Thus γx,y([0,1])⊆W, including the possibility that it merely touches the coordinate sphere.

6.1F4F5step 2.1step 3.1step 5.1

For fixed x∈W, step 2.1 supplies the normal exponential ball Bρ(0x) and step 3.1 puts the endpoint vector v(x,y) inside it. By [F5], γx,y globally minimizes length from x to y. Any other globally minimizing affinely parametrized geodesic on [0,1] is an equal-length piecewise smooth competitor, so [F5] makes it a monotone radial reparametrization of γx,y. Constant speed from [F4] and the endpoint values force that radial parameter to be t∣v(x,y)∣gx when x≠y; when x=y, zero length forces zero speed and the constant curve. Thus the normalized minimizing geodesic is unique. Together with steps 3.1 and 5.1, W is strongly geodesically convex and lies in the prescribed O.

7.1A1F1F2F3F4F5step 1.1step 2.1step 3.1step 4.1step 5.1step 6.1step 1.3∎

If M is empty there is no point p and the existence assertion is vacuous. In dimension zero, every point is an open singleton, and that singleton is strongly convex with its constant connector; a nonempty finite intersection of such sets is again a singleton. Dimension one is included in steps 1.1--6.1. Coincident endpoints and zero tangent vector were treated in steps 4.1 and 6.1; the closed parameter endpoints are included, whereas every tangent ball and coordinate ball used in the construction is open. The intersection assertion excludes the empty family, whose intersection would be all of M, and assumes the resulting intersection is nonempty. Assumption [A1] is used exactly through [F1], [F2], and [F5] for the existing global geodesic/exponential constructions; the one fixed chart, finite coefficient shrink, uniquely defined inverse, finite intersection, and compact extrema add no choice.

Source locator

Datar, Theorem 18.0.1 and proof, printed pp.133--137, supplies the endpoint-map and normal-ball minimality argument but only remarks that a refinement keeps the connector inside the chosen neighbourhood. Steinbauer, Theorem 2.2.7 and equations (2.2.8)--(2.2.11), printed pp.49--50 (PDF pp.52--53), supplies that refinement: the squared normal-coordinate radius has positive second derivative along every nonconstant local connector, contradicting an interior maximum. The global-minimizer formulation then makes the finite-intersection clause immediate.

Depends on

Dependency tree · 2 levels

Sources