Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16
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 line integrals change sign under reversal and add under concatenation

Statement

For a rectifiable contour γ, γfdz=γfdz,γfdz=γfdz. For composable rectifiable contours α,β, αβfdz=αfdz+βfdz, and the analogous additive identity holds for the absolute integral.

Facts & Assumptions

Given: Continuous integrands and rectifiable contours with matching endpoints when concatenated.

[L1]

A contour reversal is γ(t)=γ(a+bt); unit-interval contours with matching endpoints concatenate by the two standard affine pieces, and length is unchanged by monotone reparametrization (Rectifiable complex contours, reversal, concatenation, closedness, and orientation).

[L2]

Real Riemann–Stieltjes integrals are additive across a join and linear in the integrator (Linearity and interval additivity of the Riemann–Stieltjes integral).

[L3]

For piecewise-C1 paths, published vector line integrals change sign under reversal and both scalar and vector line integrals add under concatenation (Line integrals under reversal and concatenation).

[L4]

The complex integral is the combination of four component Riemann–Stieltjes integrals, and the absolute integral is the Riemann–Stieltjes integral against arc length (The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral, The absolute line integral over a rectifiable path using its arc-length function).

[L5]

Let c<d and a<b, and let ϕ:[c,d][a,b] be a strictly increasing continuous bijection. For f,α:[a,b]R, one of the two Riemann–Stieltjes integrals below exists if and only if the other does, and then abfdα=cd(fϕ)d(αϕ) (Change of variable for the Riemann–Stieltjes integral).

Proof

technique · direct
1.1

By [L1] the reversal is γ(t)=γ(a+bt). The map ta+bt sends a partition a=t0<<tn=b to the partition with points a+btn<<a+bt0 and sends tags to tags, so it is a mesh-preserving bijection between tagged partitions of [a,b] and tagged partitions of [a,b]. Under it each coordinate increment for γ is the negative of the matching increment for γ, since the two subinterval endpoints are exchanged; each arc-length increment is instead unchanged, because by [L1] length is unaffected by monotone reparametrization. Hence every Riemann–Stieltjes sum in the coordinate integrators of [L4] for γ is the negative of the corresponding sum for γ, and every sum in the arc-length integrator is equal to it. Passing to the limit over refinements yields the two reversal identities.

L1L4algebra
1.2

By [L1] the concatenation αβ is given on [0,12] and [12,1] by the two standard affine pieces, each a strictly increasing continuous bijection onto its factor's parameter interval. Apply [L5] to each component Stieltjes integral in [L4] to transport it to the factor's own interval. The integrators are coordinates and arc length of a rectifiable path, hence of bounded variation, and the integrand is continuous, so the join 12 satisfies the additivity hypotheses of [L2]; splitting there and recombining gives both additive identities.

L1L2L4L5
2.1

On piecewise-C1 contours these conclusions agree exactly with [L3], whose hypotheses and orientation distinction are preserved. Constant pieces contribute 0.

step 1.1step 1.2L3

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 95 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