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.
Scalar line integrals are parametrization-independent; vector line integrals retain orientation and change sign when it reverses
Statement
Let be piecewise-, and let be an oriented piecewise- reparametrization. For continuous fields on the trace,
If preserves orientation, then
whereas if reverses orientation, then
Facts & Assumptions
Given: The path, reparametrization, and continuous fields in the Statement.
An oriented reparametrization has nondegenerate source and target intervals and is a continuous piecewise- bijection with nonvanishing derivative of fixed sign on its smooth pieces; bijectivity excludes multiple coverings (Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations).
The scalar integrand contains the speed norm, while the vector integrand contains the oriented velocity (Scalar line integrals with respect to arc length and vector-field line integrals).
The line-integral sums are unchanged by refinement of an admissible partition (The piecewise-C1 line-integral sums do not depend on the admissible partition).
If is differentiable with integrable derivative and is continuous on an interval containing its image, then with oriented limits (Substitution: if is differentiable on with integrable and is continuous on an interval containing , then ).
The total-derivative chain rule is (The chain rule for total derivatives: ).
Proof
Refine at the breakpoints of and at their preimages of the breakpoints of . On each resulting interval, [L5] gives . The refinements do not alter either line integral by [L3].
For the scalar integrand, step 1.1 gives
For the vector integrand, step 1.1 and bilinearity give
When is increasing, and [L4] identifies the sum of these integrals with . When is decreasing, and the reversal of the oriented substitution limits supplies the second minus sign. Thus the scalar equality holds in both cases.
Applying [L4] piece by piece to step 2.2 gives the same oriented integral when , and its negative when . These are respectively the orientation-preserving and orientation-reversing cases in [L1].
Steps 3.1 and 3.2 prove all three formulas. The nondegenerate-interval, nonzero-derivative, and bijectivity hypotheses in [L1] rule out singleton reparametrizations, pauses, and multiple traversals.
Depends on
- Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations
- Scalar line integrals with respect to arc length and vector-field line integrals
- The piecewise-C1 line-integral sums do not depend on the admissible partition
- Substitution: if $\varphi$ is differentiable on $[c,d]$ with $\varphi'$ integrable and $f$ is continuous on an interval containing $\varphi([c,d])$, then $\int_{\varphi(c)}^{\varphi(d)} f = \int_c^d (f\circ\varphi)\,\varphi'$
- The chain rule for total derivatives: $D(g\circ f)(a)=Dg(f(a))\circ Df(a)$
Used by
- A vector line integral around the vortex counts repeated traversals Example
- The scalar line integral of x over the right unit semicircle equals two Example
- False: vector line integrals are invariant under reversing a path False statement
- A continuous path-independent field has a potential constructed by line integrals Theorem
- Line integrals under reversal and concatenation Theorem
- Path independence is equivalent to zero integral around every closed piecewise-C1 path Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 96 results over 18 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, Proposition 9.2.15 (standard reference, not scraped)