TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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), 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.1givenL1L2

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.

1.2givenL5

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$ .

2.1step 1.1L3

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

3.1step 2.1L4

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}$ .

3.2step 2.1step 1.2L4

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))$ .

4.1step 3.1L6

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

4.2step 1.2step 3.2L6

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.

5.1step 4.1step 4.2∎

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

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

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

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

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

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$