Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Scalar line integrals are parametrization-independent; vector line integrals retain orientation and change sign when it reverses

Statement

Let γ:[a,b]→Rn be piecewise-C1, and let h:[c,d]→[a,b] be an oriented piecewise-C1 reparametrization. For continuous fields on the trace,

∫γ∘hf ds=∫γf ds.

If h preserves orientation, then

∫γ∘hF⋅dr=∫γF⋅dr,

whereas if h reverses orientation, then

∫γ∘hF⋅dr=−∫γF⋅dr.

Facts & Assumptions

Given: The path, reparametrization, and continuous fields in the Statement.

[L1]

An oriented reparametrization has nondegenerate source and target intervals and is a continuous piecewise-C1 bijection with nonvanishing derivative of fixed sign on its smooth pieces; bijectivity excludes multiple coverings (Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations).

[L2]

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).

[L3]

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).

[L4]

If u is differentiable with integrable derivative and q is continuous on an interval containing its image, then ∫u(c)u(d)q=∫cd(q∘u)u′, with oriented limits (Substitution: if φ is differentiable on [c,d] with φ′ integrable and f is continuous on an interval containing φ([c,d]), then ∫φ(c)φ(d)f=∫cd(f∘φ) φ′).

[L5]

The total-derivative chain rule is D(g∘f)(a)=Dg(f(a))∘Df(a) (The chain rule for total derivatives: D(g∘f)(a)=Dg(f(a))∘Df(a)).

Proof

technique · direct
1.1

Refine at the breakpoints of h and at their preimages of the breakpoints of γ. On each resulting interval, [L5] gives (γ∘h)′=(γ′∘h)h′. The refinements do not alter either line integral by [L3].

givenL1L3L5
2.1

For the scalar integrand, step 1.1 gives f(γ(h(t)))∥(γ∘h)′(t)∥2=f(γ(h(t)))∥γ′(h(t))∥2∣h′(t)∣.

step 1.1L2algebra
2.2

For the vector integrand, step 1.1 and bilinearity give ⟨F(γ(h(t))),(γ∘h)′(t)⟩=⟨F(γ(h(t))),γ′(h(t))⟩h′(t).

step 1.1L2algebra
3.1

When h is increasing, ∣h′∣=h′ and [L4] identifies the sum of these integrals with ∫γf ds. When h is decreasing, ∣h′∣=−h′ and the reversal of the oriented substitution limits supplies the second minus sign. Thus the scalar equality holds in both cases.

L1L4step 2.1algebra
3.2

Applying [L4] piece by piece to step 2.2 gives the same oriented integral when h(c)=a,h(d)=b, and its negative when h(c)=b,h(d)=a. These are respectively the orientation-preserving and orientation-reversing cases in [L1].

L1L4step 2.2
4.1

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.

step 3.1step 3.2L1∎

Depends on

Used by

Dependency tree · two levels

28 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