ExampleConstruction: Literature-sourcedVerification: 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.

A line segment has length equal to the distance between its endpoints, and a finitely piecewise-linear path has length equal to the sum of its edge lengths

Example

For $p, q \in R^{n}$ , the line segment $γ (t) = (1 - t) p + t q$ on $[0, 1]$ has

$L (γ) = ∥ q - p ∥_{2} .$

More generally, a polygonal path with successive vertices $p_{0}, \dots, p_{m}$ , traversing each segment once and in that order on adjacent parameter subintervals, has

$L = \sum_{i < m} ∥ p_{i + 1} - p_{i} ∥_{2} .$

For $m = 0$ the path is constant and the empty sum is zero.

Facts & Assumptions

Given: The segment or polygonal path in the statement.

[L1]

A piecewise $C^{1}$ path has length equal to the sum of the integrals of the speeds on its pieces (A continuous piecewise- $C^{1}$ path is rectifiable and its length is the sum of the speed integrals over its pieces).

[L2]

Length is additive over adjacent parameter subintervals (Arc length is additive across every subdivision point and decreases under restriction).

Verification

technique · direct

1.1

The segment derivative is the constant vector $q - p$ , so [L1] gives $L (γ) = \int_{0}^{1} ∥ q - p ∥_{2} d t = ∥ q - p ∥_{2}$ .

givenL1algebra

2.1

On a polygonal path, the $i$ -th affine piece has length $∥ p_{i + 1} - p_{i} ∥_{2}$ by step 1.1, independently of its positive traversal time.

step 1.1algebra

3.1

Add the piece lengths using [L1] or [L2] to obtain the displayed sum. If $m = 0$ , the path is constant and both sides are zero.

step 2.1L1L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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