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.

Complex path length equals coordinate length and piecewise speed integral

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources