LemmaStatement: 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.

The arc-length function is continuous and nondecreasing, with increments equal to subpath lengths; it is strictly increasing exactly when no nondegenerate subpath is constant

Statement

Let $γ : [a, b] \to R^{n}$ be rectifiable and let $s = s_{γ}$ . Then $s$ is continuous and nondecreasing. Moreover, $s$ is strictly increasing if and only if $γ$ is constant on no nondegenerate subinterval of $[a, b]$ .

On a singleton interval, continuity and nondecrease hold and the strictness equivalence is vacuous on both sides.

Facts & Assumptions

Given: The rectifiable path and its arc-length function.

[L1]

For $u \leq v$ , $s (v) - s (u)$ is the nonnegative length of the restricted path (The arc-length function $s_{γ} (t) = L (γ ∣_{[a, t]})$ of a rectifiable path, Arc length is additive across every subdivision point and decreases under restriction).

[L2]

Every coordinate $γ_{j}$ has bounded variation, the length of a restriction is at most the sum of its coordinate variations, and variation is additive on adjacent subintervals; hence ${Var}_{[u, v]} (γ_{j}) = V_{j} (v) - V_{j} (u)$ for $V_{j} (t) = {Var}_{[a, t]} (γ_{j})$ (A path in $R^{n}$ is rectifiable exactly when every coordinate has bounded variation, Total variation is additive over adjacent subintervals and decreases under restriction).

[L3]

The variation function of a bounded-variation function is continuous at every point where the function is continuous (The jumps of a variation function equal the absolute jumps of the original function).

[L4]

A path of length zero is constant (Every endpoint chord is no longer than the arc: $∥ γ (b) - γ (a) ∥_{2} \leq L (γ)$ ).

Proof

technique · comparison

1.1

From [L1], $s (v) \geq s (u)$ whenever $u \leq v$ , so $s$ is nondecreasing.

1.2

Let $V_{j} (t) = {Var}_{[a, t]} (γ_{j})$ . Each $V_{j}$ is continuous by [L2], [L3], and continuity of the path's coordinates.

givenL2L3

1.3

If $s (u) = s (v)$ for some $u < v$ , [L1] says the intervening path has length zero, and [L4] makes it constant on $[u, v]$ .

L1L4

2.1

For $u \leq v$ , [L1] and [L2] give $0 \leq s (v) - s (u) \leq \sum_{j} (V_{j} (v) - V_{j} (u))$ . The finite sum on the right tends to zero as $v \to u$ , from either permitted side, so $s$ is continuous.

step 1.2L1L2

3.1

Conversely, if $γ$ is constant on $[u, v]$ , every polygonal sum there is zero, so [L1] gives $s (u) = s (v)$ . Thus equality at distinct arguments occurs exactly on a constant subinterval, proving the strictness equivalence.

step 1.3L1algebra∎

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: 111 results over 20 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

T. M. Apostol, Mathematical Analysis, Theorem 6.19 (standard reference, not scraped)