TheoremStatement: Literature-sourcedProof: 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.

If $γ : [a, b] \to R^{n}$ is continuous, differentiable on $(a, b)$ , and $γ^{'}$ extends continuously to $[a, b]$ , then $L (γ) = \int_{a}^{b} ∥ γ^{'} (t) ∥_{2} d t$

Statement

Let $n \geq 1$ and $a < b$ . Suppose $γ : [a, b] \to R^{n}$ is continuous, differentiable on $(a, b)$ , and its derivative extends to a continuous function $v : [a, b] \to R^{n}$ . Then $γ$ is rectifiable and

$L_{[a, b]} (γ) = \int_{a}^{b} ∥ v (t) ∥_{2} d t .$

The extension values $v (a)$ and $v (b)$ are necessarily the relative one-sided derivatives of $γ$ ; thus the statement is exactly the usual $C^{1}$ hypothesis on a closed interval. The formula also holds on a singleton interval, with both sides defined as zero.

Facts & Assumptions

Given: The path $γ$ and continuous derivative extension $v$ .

[L1]

Vector differentiability and integration are componentwise (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L2]

The scalar mean value theorem identifies each endpoint difference quotient with an interior derivative value (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[L3]

If a vector-valued function is differentiable on a closed interval and its derivative is integrable, then its endpoint increment is the vector integral of its derivative (If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz).

[L4]

For $u \leq w$ , $∥ \int_{u}^{w} v ∥_{2} \leq \int_{u}^{w} ∥ v ∥_{2}$ , and the norm of an integrable vector function is integrable (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable).

[L5]

A continuous function on a compact interval is uniformly continuous (Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous, proved $R$ -natively from sequential compactness), and tagged Riemann sums of an integrable function converge uniformly over sufficiently fine tagged partitions to its integral (The Darboux and Riemann definitions agree: a bounded $f$ on $[a, b]$ is Darboux integrable with integral $I$ if and only if for every real $ε > 0$ there is a real $δ > 0$ such that $∣ S (f, P, ξ) - I ∣ < ε$ for every tagged partition of mesh below $δ$ ).

[L6]

Arc length is the supremum of polygonal lengths (Paths in $R^{n}$ , inscribed polygonal sums, arc length as their supremum, and rectifiability).

Proof

technique · two inequalities

1.1

For each coordinate and $h > 0$ , [L2] gives $(γ_{j} (a + h) - γ_{j} (a)) / h = γ_{j}^{'} (ξ_{h})$ for some $ξ_{h} \in (a, a + h)$ . Continuity of $v_{j}$ makes this tend to $v_{j} (a)$ ; the analogous argument at $b$ gives the left derivative $v_{j} (b)$ . Hence $γ$ is differentiable relative to $[a, b]$ with derivative $v$ everywhere.

givenL1L2

1.2

Fix $ε > 0$ . By uniform continuity in [L5], choose $δ > 0$ so that $∥ v (t) - v (s) ∥_{2} < ε / (2 (b - a))$ whenever $∣ t - s ∣ < δ$ . Choose a tagged partition $P$ of mesh below $δ$ whose Riemann sum for the continuous speed differs from its integral by less than $ε / 2$ .

givenL5

2.1

Applying [L3] on every subinterval $[u, w] \subseteq [a, b]$ gives $γ (w) - γ (u) = \int_{u}^{w} v$ .

step 1.1L3

3.1

For any partition $P$ , [L4] applied to each increment from step 2.1 gives $ℓ_{P} (γ) \leq \sum_{i} \int_{t_{i}}^{t_{i + 1}} ∥ v ∥_{2} = \int_{a}^{b} ∥ v ∥_{2}$ .

step 2.1L4

3.2

On a subinterval with tag $ξ_{i}$ , step 2.1 gives $γ (t_{i + 1}) - γ (t_{i}) = v (ξ_{i}) Δ t_{i} + \int_{t_{i}}^{t_{i + 1}} (v - v (ξ_{i}))$ . By [L4] and the reverse triangle inequality, its norm is at least $∥ v (ξ_{i}) ∥_{2} Δ t_{i} - ε Δ t_{i} / (2 (b - a))$ .

step 2.1step 1.2L4

4.1

Taking the supremum over $P$ gives $L (γ) \leq \int_{a}^{b} ∥ v ∥_{2}$ , so in particular $γ$ is rectifiable.

step 3.1L6

4.2

Summing step 3.2 and using the tagged-sum choice gives $ℓ_{P} (γ) > \int_{a}^{b} ∥ v ∥_{2} - ε$ . Since $L (γ) \geq ℓ_{P} (γ)$ and $ε$ is arbitrary, the reverse inequality follows.

step 1.2step 3.2L6

5.1

Combining steps 4.1 and 4.2 proves equality. On $[a, a]$ the length and oriented integral are both zero by definition.

step 4.1step 4.2∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 211 results over 28 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

A. R. Shastri, Metric Spaces, Section 5 (standard reference, not scraped)
U. Lang, Differential Geometry I, Section 1.1 (standard reference, not scraped)

If γ:[a,b]→Rnγ:[a,b]→Rn is continuous, differentiable on (a,b)(a,b), and γ′γ′ extends continuously to [a,b][a,b], then L(γ)=∫ab∥γ′(t)∥2 dtL(γ)=∫ab​∥γ′(t)∥2​dt