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.
Radial geodesics minimize length in a normal neighborhood
Statement
Assume . Suppose is a diffeomorphism, where , and let . The radial geodesic , , has length and minimizes length among all piecewise smooth curves in from to .
If , equality holds precisely for the monotone radial reparametrizations where is continuous, piecewise smooth, nondecreasing, and has endpoint values and . For , equality holds precisely for the constant curve.
Facts & Assumptions
Given: The normal ball, vector, and competitor curves in the statement.
The Axiom of Countable Choice () is the assumed .
Under [A1], Gauss lemma gives unit radial speed, and Polar form of the metric in normal coordinates gives wherever . Riemannian speed and length defines length by finitely many speed integrals.
Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on takes every value between and supplies crossings of intermediate radial levels. A closed subset of the compact interval from Heine-Borel by bisection: every closed bounded interval is compact is compact by A closed subset of a compact metric space is compact, and Extreme value theorem: a continuous real function on a nonempty compact subset of attains a greatest and a least value supplies its last point.
Newton–Leibniz needs only continuity on , differentiability on , and a Riemann-integrable extension of the interior derivative, If on and both are integrable then ; and , and Integrable functions on form a set closed under sums and scalar multiples, and give on a piecewise smooth interval. A continuous on with is identically detects equality on each smooth piece, and A function continuous on an interval whose derivative vanishes at every interior point of is constant on ; consequently two such functions with the same derivative differ by a constant makes a zero-derivative angular direction constant.
Proof
Write . By radial norm preservation in [F1], , so .
Let be piecewise smooth with , , and put . Assume first and fix . By [F2], the set is nonempty; it is closed in the compact interval and hence compact, so [F2] gives its greatest element . Then for : otherwise continuity and would produce a later point of . Thus avoids on .
On every smooth piece of , [F1] gives . Summing the monotone integral inequalities and using [F3] gives Since this holds for every , . If , nonnegativity already gives . This proves minimality without differentiating at a visit to .
Conversely, for a curve of the displayed form, [F1] gives on each smooth piece. Newton--Leibniz and finite additivity in [F3] give , including any constant pauses. If , equality means ; [F3] forces the continuous speed to vanish on each smooth piece, so is constant.
The same argument proves the auxiliary estimate for any piecewise smooth : if avoids , integrate the polar inequality directly; if it meets , split there and apply step 2.1 to the reversed first part and the second part.
Suppose now and . For any , step 2.1 on the prefix and step 3.1 on the suffix give Hence , and equality forces the two lower bounds to be equal. If and avoids on , applying the prefix, middle, and suffix bounds gives Therefore and equality holds in the middle polar length estimate.
On a closed subinterval of one smooth piece on which , step 4.1 and Newton--Leibniz give zero integral for the continuous nonnegative function . By [F3] it vanishes identically. The polar identity in [F1] then gives and . Writing with , invertibility of gives ; hence [F3] makes constant on every nonzero component. A component that later returned to would have positive nondecreasing tending to zero, which is impossible. Thus is constant at until its final nonzero component, and there and is nondecreasing. This proves the stated necessary form.
Steps 2.1, 5.1, and 2.2 prove minimality and both equality directions. In dimension zero only occurs; dimension one permits the two radial directions and the proof fixes the one containing . Empty has no centre. The open-ball condition excludes , while , visits to the centre, subdivision endpoints, and constant pauses were treated explicitly. Assumption [A1] is used exactly through [F1] for the exponential and polar structures; last hitting times are unique maxima, and no further choice is made.
Depends on
- Gauss lemma
- Polar form of the metric in normal coordinates
- Riemannian speed and length
- Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$
- Heine-Borel by bisection: every closed bounded interval $[a,b]$ is compact
- A closed subset of a compact metric space is compact
- Extreme value theorem: a continuous real function on a nonempty compact subset of $\mathbb{R}$ attains a greatest and a least value
- Newton–Leibniz needs only continuity on $[a,b]$, differentiability on $(a,b)$, and a Riemann-integrable extension of the interior derivative
- If $f \le g$ on $[a,b]$ and both are integrable then $\int_a^b f \le \int_a^b g$; and $m(b-a) \le \int_a^b f \le M(b-a)$
- Integrable functions on $[a,b]$ form a set closed under sums and scalar multiples, and $\int_a^b(\lambda f+\mu g) = \lambda\int_a^b f + \mu\int_a^b g$
- A continuous $f \ge 0$ on $[a,b]$ with $\int_a^b f = 0$ is identically $0$
- A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$; consequently two such functions with the same derivative differ by a constant
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Dependency tree · two levels
88 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
- Ved Datar, Lectures on Riemannian Geometry, Corollary 18.1.3(2)--(3) and proof, pp.135--137 (standard reference, not scraped)