TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Complex path length equals coordinate length and piecewise speed integral

Statement

Let $a \leq b$ and let $γ : [a, b] \to C$ be continuous. Put $Γ : = Φ \circ γ = (x, y)$ , where $x (t) = Re γ (t)$ and $y (t) = Im γ (t)$ . For every partition, the complex polygonal sum of $γ$ equals the Euclidean polygonal sum of $Γ$ , and

$L_{C} (γ) = L_{R^{2}} (Γ),$

including singleton intervals. Consequently, $γ$ is rectifiable exactly when both $x$ and $y$ have bounded variation.

If $a < b$ and there is a finite partition $a = t_{0} < \dots < t_{m} = b$ such that on each piece $[t_{j}, t_{j + 1}]$ the path $Γ$ is differentiable in the interior and its derivative extends continuously to the closed piece, then

$L_{C} (γ) = \sum_{j < m} \int_{t_{j}}^{t_{j + 1}} ∥ Γ_{j}^{'} (t) ∥_{2} d t = \sum_{j < m} \int_{t_{j}}^{t_{j + 1}} \sqrt{x_{j}^{'} (t)^{2} + y_{j}^{'} (t)^{2}} d t < \infty .$

Corners and zero-speed pieces are allowed. On a singleton interval the length and coordinate variations are zero, and the piecewise-speed sum is empty.

Facts & Assumptions

Given: The continuous complex path $γ$ and, when $a < b$ , the stated finite subdivision.

[F1]

The complex coordinate isometry transports topology and affine segments: $Φ$ is a bijective isometry from $d_{C}$ to $d_{2}$ .

[F2]

Polygonal length and rectifiability of complex paths and Paths in $R^{n}$ , inscribed polygonal sums, arc length as their supremum, and rectifiability: Both lengths are suprema over the same interval partitions, with singleton length zero.

[F3]

Real and imaginary parts, complex conjugation, and modulus: $Re (a + b i) = a$ and $Im (a + b i) = b$ , so the coordinates of $Φ (γ (t))$ are $x (t), y (t)$ .

[F4]

A path in $R^{n}$ is rectifiable exactly when every coordinate has bounded variation: A continuous $R^{2}$ path is rectifiable exactly when both coordinate functions have bounded variation, including the singleton case.

[F5]

A continuous piecewise- $C^{1}$ path is rectifiable and its length is the sum of the speed integrals over its pieces: A continuous piecewise- $C^{1}$ Euclidean path has finite length equal to the sum of the speed integrals on the pieces; derivatives need not match at corners.

[F6]

The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ : For $(u, v) \in R^{2}$ , $∥ (u, v) ∥_{2} = \sqrt{u^{2} + v^{2}}$ .

Proof

1.1givenF1F2F3algebra

The path $Γ$ is continuous: for any $s, t \in [a, b]$ , [F1] gives $d_{2} (Γ (s), Γ (t)) = d_{C} (γ (s), γ (t))$ , so the continuity condition for $γ$ implies that for $Γ$ . By [F3], $Γ = (x, y)$ . For each partition point pair, [F1] identifies the chord lengths; summing termwise gives equal polygonal sums by [F2].

2.1F2step 1.1

If $a < b$ , taking the supremum of those equal sums over the identical partition set in [F2] gives $L_{C} (γ) = L_{R^{2}} (Γ)$ . If $a = b$ , both lengths are zero by [F2].

3.1F3F4step 2.1

Apply [F4] to the continuous $R^{2}$ path $Γ$ . The length equality in step 2.1 identifies its rectifiability with that of $γ$ , and [F3] identifies its coordinate functions with $x$ and $y$ . Thus the bounded-variation equivalence holds in both directions.

3.2givenF5F6step 2.1algebra

Under the piecewise- $C^{1}$ hypothesis with $a < b$ , [F5] applies to $Γ$ on the given subdivision. Substituting the length equality from step 2.1 gives the first integral formula and finiteness; [F6] gives the displayed square-root integrand. No derivative equality at adjacent endpoints is required by [F5].

4.1givenF2F4∎

If $a = b$ , [F2] gives zero for both lengths, [F4] gives zero coordinate variations, and the speed sum is empty. Hence all stated boundary conventions hold.

Depends on

Used by

Dependency tree · two levels

51 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

L. V. Ahlfors, Complex Analysis, 3rd ed., Chapter 4, Section 1.2 (standard reference, not scraped)
U. Lang, Differential Geometry I, Section 1.1 (standard reference, not scraped)