LemmaStatement: Literature-sourcedProof: 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.

The piecewise-C1 line-integral sums do not depend on the admissible partition

Statement

For a piecewise- $C^{1}$ path $γ$ , the scalar and vector line-integral sums in Scalar line integrals with respect to arc length and vector-field line integrals have the same value for every admissible partition. Thus both line integrals are well-defined.

Facts & Assumptions

Given: A piecewise- $C^{1}$ path $γ : [a, b] \to R^{n}$ , continuous fields $f$ and $F$ on its trace, and two admissible partitions.

[L1]

On a nondegenerate admissible piece, the scalar summand is the integral of $f (γ (t)) ∥ γ^{'} (t) ∥_{2}$ and the vector summand is the integral of $⟨ F (γ (t)), γ^{'} (t) ⟩$ ; on a singleton parameter interval both line integrals are defined as zero (Scalar line integrals with respect to arc length and vector-field line integrals).

[L2]

An integrable function is integrable on the two sides of any inserted interior point, and its integral over the original interval is the sum of those two integrals (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

Proof

technique · direct

1.1

Inserting one point into an admissible partition only splits one smooth piece. By [L2], the original scalar summand equals the two new scalar summands, and the same holds for the vector summand. Hence either total sum is unchanged.

givenL1L2

2.1

The union of the two finite partitions is a finite common refinement. Repeatedly applying step 1.1 shows that each original sum equals the sum over this refinement.

givenstep 1.1

3.1

Therefore the two original scalar sums agree, and the two original vector sums agree.

step 2.1

4.1

A partition with no interior breakpoints already equals its own refinement. For a constant path on a nondegenerate interval every derivative extension is zero, while on a singleton interval both integrals are zero by [L1]. Thus the conclusion includes both boundary cases.

L1algebra∎

Depends on

Used by

Cited to discharge well-definedness by Scalar line integrals with respect to arc length and vector-field line integrals.

Dependency tree · next 3 levels

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

J. Lebl, Basic Analysis II, section 9.2 (standard reference, not scraped)