Alphabeta Math
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 is invariant under monotone surjective reparametrization

Statement

Let a≤b and c≤d. Suppose γ:[a,b]→C is continuous and φ:[c,d]→[a,b] is continuous, surjective, and either nondecreasing or nonincreasing in the sense of Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of R, with the dictionary to monotone sequences. Then

LC(γ∘φ)=LC(γ).

The equality includes finite and infinite lengths, constant pauses, reversal, and singleton intervals. A nondecreasing map preserves parameter order; a nonincreasing map reverses it. When a=b, φ is constant and there is no nontrivial orientation to distinguish.

Facts & Assumptions

Given: The intervals, continuous path, and continuous surjective monotone map in the statement.

[F1]

Polygonal length and rectifiability of complex paths: A complex path must be continuous from the usual real metric to dC, and its length is the extended-real supremum of its partition sums, with singleton length zero.

[F2]

The complex coordinate isometry transports topology and affine segments and Complex path length equals coordinate length and piecewise speed integral: Φ is an isometry and the length of every continuous complex path equals that of its coordinate path, including singleton intervals.

[F3]

Arc length is invariant under every continuous surjective monotone reparametrization, including pauses and reversal: A continuous surjective nondecreasing or nonincreasing reparametrization preserves Euclidean polygonal length, including pauses, reversal, and singleton intervals.

Proof

1.1givenF1F5choose

The composite γ∘φ is continuous. Indeed, fix s0∈[c,d] and ε>0. By continuity of γ at φ(s0) choose δ>0 such that u∈[a,b] and ∣u−φ(s0)∣<δ imply dC(γ(u),γ(φ(s0)))<ε. By continuity of φ at s0 choose η>0 such that s∈[c,d] and ∣s−s0∣<η imply ∣φ(s)−φ(s0)∣<δ. The implication in [F5] then proves continuity of the composite at s0.

1.2givenF1

If c=d, surjectivity forces a=b, so both lengths are zero by [F1]. If a=b while c<d, then γ and γ∘φ are constant paths and both lengths are zero by [F1]. Thus the equality covers all singleton cases.

2.1givenF2F3step 1.1

Put Γ=Φ∘γ. By the isometry in [F2], Γ is continuous and Φ∘(γ∘φ)=Γ∘φ. The Euclidean reparametrization theorem [F3] gives LR2(Γ∘φ)=LR2(Γ).

3.1F2step 1.1step 2.1

Apply the complex-to-coordinate length equality [F2] to γ and, using step 1.1, to γ∘φ. Together with step 2.1 this yields LC(γ∘φ)=LC(γ).

4.1givenF4algebra∎

By [F4], the nondecreasing case preserves order and the nonincreasing case reverses it. If a<b, a nondecreasing surjection must attain a at c and b at d; a nonincreasing surjection must attain b at c and a at d. If a=b, the map is constant and there is no nontrivial orientation.

Depends on

Used by

Dependency tree · two levels

50 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