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.
Paths in , inscribed polygonal sums, arc length as their supremum, and rectifiability
Definition
Let and . A path in is a continuous map . The map, its domain, and its parametrization are part of the path; its trace is only the set .
If and is a partition of , define the polygonal length inscribed by by
The arc length is the extended-real supremum
The path is rectifiable when these polygonal lengths are bounded above in , equivalently when . In that case the length is a nonnegative real number. When the interval is clear, write .
On a singleton interval , define and call every path with that domain rectifiable. There is one such path for each point of , namely the map sending to that point. This convention does not invoke a partition, whose published definition assumes distinct endpoints.
Depends on
- Vector-valued functions $f : A \to \mathbb{R}^m$, their limits and continuity, with the dictionary to the metric notions
- The $p$-norms $\lVert x\rVert_p$ for rational $p \ge 1$, and $\lVert x\rVert_\infty$
- Partition of $[a,b]$ as a finite strictly increasing list $a = t_0 < t_1 < \dots < t_n = b$, its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions
- Complete ordered field (least-upper-bound property)
- The extended real line $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, its order, and the arithmetic that is left undefined
- Every subset of $\overline{\mathbb{R}}$ has a least upper bound and a greatest lower bound in $\overline{\mathbb{R}}$, agreeing with the real supremum and infimum on nonempty sets bounded in $\mathbb{R}$
Used by
- Every endpoint chord is no longer than the arc: ‖γ(b)-γ(a)‖₂≤ L(γ) Corollary
- The Koch curve is a uniform limit of polygonal paths of lengths (4/3)ⁿ but is not rectifiable Counterexample
- The arc-length function s_γ(t)=L(γ|_[a,t]) of a rectifiable path Definition
- Refining a partition cannot decrease its inscribed polygonal length Lemma
- A C-Lipschitz map multiplies path length by at most C; isometries preserve length and scalar dilation multiplies it by the absolute scale Proposition
- A path in ℝⁿ is rectifiable exactly when every coordinate has bounded variation Theorem
- Arc length is additive across every subdivision point and decreases under restriction Theorem
- Arc length is invariant under every continuous surjective monotone reparametrization, including pauses and reversal Theorem
- Arc length is lower semicontinuous under uniform convergence of paths Theorem
- If γ:[a,b]→ℝⁿ is continuous, differentiable on (a,b), and γ' extends continuously to [a,b], then L(γ)=∫ₐᵇ‖γ'(t)‖₂ dt Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 137 results over 23 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, Sections 5--6 (standard reference, not scraped)
- U. Lang, Differential Geometry I, Section 1.1 (standard reference, not scraped)