Alphabeta Math
TheoremStatement: 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.

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,

γhfds=γfds.

If h preserves orientation, then

γhFdr=γFdr,

whereas if h reverses orientation, then

γhFdr=γFdr.

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(qu)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(gf)(a)=Dg(f(a))Df(a) (The chain rule for total derivatives: D(gf)(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))2h(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 γfds. 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 · 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