LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

A vector line integral along an image arc is the parameter line integral of the pulled-back field

Statement

Let $O \subseteq R^{2}$ be open, let $φ : O \to R^{3}$ be $C^{1}$ , let $σ = (σ_{1}, σ_{2}) : [a, b] \to O$ be a piecewise- $C^{1}$ path, and let $F$ be a continuous vector field on a set containing $φ (σ ([a, b]))$ . Put $P^{*} = ⟨ F \circ φ, φ_{u} ⟩$ and $Q^{*} = ⟨ F \circ φ, φ_{v} ⟩$ where these are defined. Then $φ \circ σ$ is a piecewise- $C^{1}$ path in $R^{3}$ and the vector line integral of the field along the image arc equals the parameter line integral of the pulled-back pair:

$\int_{φ \circ σ} F \cdot d r = \int_{σ} (P^{*}, Q^{*}) \cdot d r .$

Facts & Assumptions

Given: The open $O \subseteq R^{2}$ , the $C^{1}$ map $φ : O \to R^{3}$ , the piecewise- $C^{1}$ path $σ : [a, b] \to O$ , and the continuous field $F$ on a set containing the image of the trace of $σ$ under $φ$ .

[F1]

For a piecewise- $C^{1}$ path $γ : [a, b] \to R^{n}$ with $a < b$ , an admissible partition $a = t_{0} < \dots < t_{m} = b$ and continuous derivative extensions $v_{i}$ on the pieces, $\int_{γ} F \cdot d r = \sum_{i < m} \int_{t_{i}}^{t_{i + 1}} ⟨ F (γ (t)), v_{i} (t) ⟩ d t$ ; if $a = b$ the integral is $0$ (Scalar line integrals with respect to arc length and vector-field line integrals).

[F2]

For $x, y \in R^{m}$ , $⟨ x, y ⟩ = \sum_{i < m} x_{i} y_{i}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F3]

A piecewise- $C^{1}$ path admits a partition on whose pieces its derivative has a continuous extension, and constant paths are allowed (Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations).

[F4]

The pulled-back functions of a patch and a field are $P^{*} = ⟨ F \circ φ, φ_{u} ⟩$ and $Q^{*} = ⟨ F \circ φ, φ_{v} ⟩$ (The induced boundary chain and circulation of a $C^{2}$ patch over a finite elementary Green region).

[F5]

A map is $C^{k}$ when each component is ( $C^{k}$ Euclidean maps and diffeomorphisms), and the Jacobian matrix of $φ$ has columns $φ_{u}, φ_{v}$ (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case); a regular patch's parametrization is $C^{1}$ on an open neighbourhood of its parameter region (Regular parametrized surface patches on compact Jordan parameter regions).

[L1]

If $f$ is totally differentiable at $a$ and $g$ at $f (a)$ , then $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[L2]

If $f$ is totally differentiable at $a$ then $D_{w} f (a) = D f (a) w$ for every $w$ , and the matrix of $D f (a)$ is $J f (a)$ (A total derivative computes every directional derivative, and its matrix is the Jacobian).

[L3]

If every partial derivative of $f$ exists on a neighbourhood of $a$ and is continuous at $a$ , then $f$ is totally differentiable at $a$ with $D f (a)$ the linear map of matrix $J f (a)$ (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

[L4]

A continuous function on a closed bounded interval is Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

Proof

technique · direct

1.1

If $a = b$ then both line integrals are $0$ by [F1] and the identity holds. Assume $a < b$ , and by [F3] fix an admissible partition $a = t_{0} < \dots < t_{m} = b$ and continuous extensions $v_{i} = (v_{i, 1}, v_{i, 2})$ of $σ^{'}$ on the pieces $[t_{i}, t_{i + 1}]$ .

givenF1F3

2.1

Fix $i$ and let $t$ be interior to $[t_{i}, t_{i + 1}]$ . By [F5] and [L3] the map $φ$ is totally differentiable at $σ (t)$ , so [L1] and [L2] give that $φ \circ σ$ is differentiable at $t$ with $(φ \circ σ)^{'} (t) = D φ (σ (t)) σ^{'} (t) = φ_{u} (σ (t)) v_{i, 1} (t) + φ_{v} (σ (t)) v_{i, 2} (t),$ the second equality because by [L2] and [F5] the matrix of $D φ$ has columns $φ_{u}$ and $φ_{v}$ . The right-hand side is continuous in $t$ on the whole of $[t_{i}, t_{i + 1}]$ , since $φ_{u}, φ_{v}$ are continuous by [F5] and $v_{i}$ is continuous; so it is a continuous extension of $(φ \circ σ)^{'}$ on that piece, and $φ \circ σ$ is a piecewise- $C^{1}$ path with that admissible partition.

step 1.1F5L1L2L3

3.1

On each piece, pairing the extension of step 2.1 with $F (φ (σ (t)))$ and using [F2] gives $⟨ F (φ (σ (t))), (φ \circ σ)^{'} (t) ⟩ = ⟨ F (φ (σ (t))), φ_{u} (σ (t)) ⟩ v_{i, 1} (t) + ⟨ F (φ (σ (t))), φ_{v} (σ (t)) ⟩ v_{i, 2} (t),$ which by [F4] is $P^{*} (σ (t)) v_{i, 1} (t) + Q^{*} (σ (t)) v_{i, 2} (t) = ⟨ (P^{*}, Q^{*}) (σ (t)), v_{i} (t) ⟩$ . Both sides are continuous on the piece, hence integrable by [L4].

step 2.1F2F4L4

4.1

Summing the integrals of step 3.1 over the $m$ pieces and reading each side by [F1] — the left as the vector line integral of $F$ along $φ \circ σ$ with the partition of step 2.1, the right as the vector line integral of $(P^{*}, Q^{*})$ along $σ$ with the partition of step 1.1 — gives the asserted identity. A piece on which $σ$ is constant has $v_{i} = 0$ and contributes $0$ to both sides.

step 3.1F1∎

Remarks

No regularity of the patch is used. The parametrization need only be $C^{1}$ near the trace of $σ$ ; nothing here asks that $φ_{u} \times φ_{v}$ be nonzero, and nothing asks $σ$ to be injective or the trace to avoid the parameter boundary. That matters because the arcs of a positive boundary chain lie exactly on the parameter boundary, where a patch is allowed to be irregular.
The identity is an equality of two integrals, not a reparametrization statement. The path $φ \circ σ$ traverses a curve in $R^{3}$ and $σ$ traverses one in the parameter plane; what is being compared is the integral of $F$ along the first with the integral of a different field, $(P^{*}, Q^{*})$ , along the second.

Depends on

Used by

The classical Stokes theorem for a C² patch over a finite elementary Green region Theorem

Dependency tree · two levels

67 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

G. Strang and E. Herman, Calculus Volume 3 (OpenStax), section 6.7 (standard reference, not scraped)