TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-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.

Arc length is invariant under every continuous surjective monotone reparametrization, including pauses and reversal

Statement

Let $γ : [a, b] \to R^{n}$ be a path, and let $φ : [c, d] \to [a, b]$ be continuous, surjective, and either nondecreasing or nonincreasing. Then

$L_{[c, d]} (γ \circ φ) = L_{[a, b]} (γ) .$

The equality holds for finite or infinite length. Constant stretches of $φ$ are allowed. If $[c, d]$ is a singleton, surjectivity forces $[a, b]$ to be one as well; if instead $[a, b]$ is a singleton, $[c, d]$ need not be, since a constant map on a nondegenerate interval is continuous, surjective and monotone. In both cases each side of the displayed equality is zero.

Facts & Assumptions

Given: The path $γ$ and reparametrization $φ$ .

[L1]

A nondecreasing map preserves order and a nonincreasing map reverses it (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences).

[L2]

Arc length is the supremum of polygonal sums and repeated consecutive image points contribute zero (Paths in $R^{n}$ , inscribed polygonal sums, arc length as their supremum, and rectifiability).

Proof

technique · two inequalities

1.1

Suppose first that $φ$ is nondecreasing. The image under $φ$ of any partition of $[c, d]$ is a nondecreasing finite list from $a$ to $b$ ; deleting repetitions produces a partition of $[a, b]$ with the same polygonal sum for $γ$ .

givenL1L2

1.2

Conversely, for a partition $a = t_{0} < \dots < t_{m} = b$ , choose one $s_{i} \in φ^{- 1} (t_{i})$ for each of its finitely many values. Monotonicity forces $s_{0} < \dots < s_{m}$ , after taking $s_{0} = c$ and $s_{m} = d$ , and the resulting polygonal sum of $γ \circ φ$ equals that of $γ$ .

givenL1choose

2.1

Hence every polygonal sum of $γ \circ φ$ is at most $L (γ)$ , so $L (γ \circ φ) \leq L (γ)$ .

step 1.1L2

2.2

Taking the supremum over target partitions gives $L (γ) \leq L (γ \circ φ)$ , proving equality in the nondecreasing case.

step 1.2L2

2.3

If $φ$ is nonincreasing, reverse the order of every finite list in steps 1.1 and 1.2; Euclidean chord lengths are symmetric, so the same two inequalities hold.

step 1.1step 1.2L1L2

3.1

If $[c, d]$ is a singleton, so is its image $[a, b]$ , and the singleton convention in [L2] gives both lengths as zero. If instead $a = b$ while $c < d$ , then $γ \circ φ$ is constant, so every polygonal sum for it vanishes and $L_{[c, d]} (γ \circ φ) = 0$ , while $L_{[a, b]} (γ) = 0$ by the same convention.

givenL2∎

Depends on

Used by

Every rectifiable path factors through its arc-length function as a unit-speed path on [0,L] Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 66 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

U. Lang, Differential Geometry I, Section 1.1 (standard reference, not scraped)