TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

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.

Riemannian distance is a metric

Statement

$d_{g}$ is a finite metric on a connected Riemannian manifold.

Facts & Assumptions

Given: A connected Riemannian manifold, with its infimum distance.

[F1]

Riemannian distance on a connected manifold: On a connected Riemannian manifold define $d_{g} (p, q) = \inf {L_{g} (γ) : γ is piecewise C^{1} from p to q}$ . Lengths are those of def-riemannian-speed-and-length. For each pair $p, q$ , lem-any-two-points-in-a-connected-smooth-manifold-can-be-joined-by-a-piecewise-c-one-curve supplies a curve, so the set of lengths is nonempty, contains a finite real number and is bounded below by zero. Applying the least-upper-bound property cor-cauchy-reals-lub-complete to the negatives gives a finite nonnegative infimum. On the empty connected manifold this defines the empty distance function; there are no pairs to evaluate. No minimizing curve is part of this definition.

[F2]

Length is additive under concatenation and invariant under reversal: Length adds under finite concatenation and is unchanged by reversal.

[F3]

Local comparison of a riemannian metric with the euclidean metric: For a compact set $K$ contained in one coordinate chart of an $n$ -dimensional Riemannian manifold, there are $0 < c \leq C < \infty$ such that $c ∣ v ∣^{2} \leq g_{x} (v, v) \leq C ∣ v ∣^{2}$ for $x \in K$ . The dimension-zero assertion is vacuous.

[F4]

Line-integral estimates by arc length and the supremum of the field: Let $γ$ be a piecewise- $C^{1}$ path of length $L (γ)$ , let $f$ be a continuous scalar field and $F$ a continuous vector field on its trace, and let $M \geq 0$ . 1. If $∣ f (x) ∣ \leq M$ on the trace of $γ$ , then $∣ \int_{γ} f d s ∣ \leq M L (γ) .$ 2. If $∥ F (x) ∥_{2} \leq M$ on the trace of $γ$ , then $∣ \int_{γ} F \cdot d r ∣ \leq M L (γ) .$

[F5]

Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative: Let $a < b$ . Suppose $G : [a, b] \to R$ is continuous on $[a, b]$ and differentiable on $(a, b)$ . If $f : [a, b] \to R$ is Riemann integrable and $f (x) = G^{'} (x) (a < x < b),$ then $\int_{a}^{b} f = G (b) - G (a) .$ No derivative of $G$ at either endpoint is assumed, and the two endpoint values assigned to the integrable extension $f$ do not enter the conclusion.

Proof

technique · direct

1.1

Nonnegativity and finiteness follow from the definition. A constant curve gives $d_{g} (p, p) = 0$ , and reversal of curves gives symmetry. For any $ε > 0$ choose paths from $p$ to $q$ and from $q$ to $r$ with lengths less than their respective infima plus $ε$ . Concatenation gives $d_{g} (p, r) < d_{g} (p, q) + d_{g} (q, r) + 2 ε$ ; letting $ε$ decrease to zero gives the triangle inequality.

F1F2given

1.2

For distinct $p, q$ , choose a chart about $p$ and a ball $B$ centred at its coordinate image, of radius $r_{0} > 0$ , whose closed ball stays inside the chart and excludes $q$ . On its compact closure the comparison lemma gives $g (v, v) \geq c ∣ v ∣^{2}$ , $c > 0$ . Any curve $γ : [a, b] \to M$ from $p$ to $q$ has a first exit time $t_{0}$ from $B$ : the nonempty closed preimage of $M ∖ B$ is compact and has a minimum. Continuity puts $γ (t_{0})$ on the sphere, and the initial curve remains in the closed ball.

F3given

2.1

For that initial coordinate curve $x (t)$ , let $e = (x (t_{0}) - x (a)) / r_{0}$ . The vector line integral of the constant unit field $e$ is $e \cdot (x (t_{0}) - x (a)) = r_{0}$ , by Newton–Leibniz applied to each coordinate on every closed smooth piece and telescoping the endpoints. The line-integral estimate bounds this by $\int_{a}^{t_{0}} ∣ \dot{x} ∣ d t$ . Therefore $L_{g} (γ) \geq \sqrt{c} \int_{a}^{t_{0}} ∣ \dot{x} ∣ d t \geq \sqrt{c} r_{0}$ . Taking infima proves $d_{g} (p, q) > 0$ . At boundary points replace the ball by its intersection with the half-space; the same first-exit sphere estimate holds. A connected zero-manifold is a point, and the empty manifold has the empty metric.

F1F4F5step 1.2∎

Source locator

Lee, Chapter 13, pp.337–340, Proposition 13.25, Lemma 13.28 and Theorem 13.29; finite piecewise $C^{1}$ refinements and pauses are treated explicitly here.

Depends on

Used by

Extended riemannian distance on a disconnected manifold Definition
Distance to a nonempty subset is one lipschitz Proposition
The riemannian distance topology is the manifold topology Theorem

Dependency tree · two levels

24 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

John M. Lee, Introduction to Smooth Manifolds, second edition (standard reference, not scraped)