TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

The classical Stokes theorem for a $C^{2}$ patch over a finite elementary Green region

Statement

Let $(D, φ)$ be a $C^{2}$ patch over a finite elementary Green region (The induced boundary chain and circulation of a $C^{2}$ patch over a finite elementary Green region), with positive boundary chain $\partial D = (σ_{1}, \dots, σ_{m})$ and induced boundary chain $φ (\partial D)$ , and let $F$ be a $C^{1}$ vector field on an open set $U \subseteq R^{3}$ containing $φ [D]$ . Then the circulation around the induced boundary chain equals the flux of the curl in the induced orientation:

$\oint_{φ (\partial D)} F \cdot d r = \int_{D} ⟨ (curl F) \circ φ, φ_{u} \times φ_{v} ⟩ .$

The right-hand side is the flux of $curl F$ through the patch in the orientation induced by $φ$ , in the sense of Unit normal fields, orientations, and flux through a regular surface patch.

Facts & Assumptions

Given: The $C^{2}$ patch $(D, φ)$ over a finite elementary Green region with its supplied decomposition and positive boundary chain, and the $C^{1}$ field $F$ on the open $U \supseteq φ [D]$ .

[F1]

A $C^{2}$ patch over a finite elementary Green region is a regular patch whose parameter region carries a supplied elementary decomposition and whose parametrization is $C^{2}$ on an open neighbourhood of that region; the induced boundary chain is the list of arcs obtained by composing the positive boundary chain of the parameter region with the parametrization, and the circulation around it is the finite sum of the vector line integrals along those arcs; the pulled-back functions 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).

[F2]

For a finite elementary Green region the boundary integral over the positive boundary chain is the finite sum $\int_{\partial D} G \cdot d r = \sum_{k} \int_{σ_{k}} G \cdot d r$ , and likewise $\int_{\partial D} P d u + Q d v$ for the field $(P, Q)$ (Positive orientation of elementary-region boundaries, Scalar line integrals with respect to arc length and vector-field line integrals).

[F3]

A finite elementary Green region is a nonempty finite union of elementary Green regions with pairwise disjoint interiors and the stated shared-arc conditions, supplied as data (Type I, Type II, and elementary regions for Green's theorem).

[F4]

For a regular patch $(D, φ)$ and a continuous field $G$ , the flux in the orientation induced by $φ$ is $\int_{D} (G \circ φ) \cdot (φ_{u} \times φ_{v})$ , with the inner product of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ (Unit normal fields, orientations, and flux through a regular surface patch).

[F5]

A regular patch's parametrization is defined and $C^{1}$ on an open neighbourhood of its compact Jordan parameter region (Regular parametrized surface patches on compact Jordan parameter regions), and a map is $C^{k}$ when each component is ( $C^{k}$ Euclidean maps and diffeomorphisms); the curl of a $C^{1}$ field is that of Divergence and curl of a $C^{1}$ vector field.

[L1]

Let $O \subseteq R^{2}$ be open, $φ : O \to R^{3}$ be $C^{1}$ , $σ$ a piecewise- $C^{1}$ path in $O$ , and $F$ continuous on a set containing the image of its trace. Then $\int_{φ \circ σ} F \cdot d r = \int_{σ} (P^{*}, Q^{*}) \cdot d r$ (A vector line integral along an image arc is the parameter line integral of the pulled-back field).

[L2]

Let $O \subseteq R^{2}$ be open, $φ : O \to R^{3}$ be $C^{2}$ with $φ [O] \subseteq U$ and $F : U \to R^{3}$ be $C^{1}$ . Then $P^{*}, Q^{*}$ are $C^{1}$ on $O$ and $\partial_{u} Q^{*} - \partial_{v} P^{*} = ⟨ (curl F) \circ φ, φ_{u} \times φ_{v} ⟩$ (The curl flux integrand of a $C^{2}$ patch is a two-dimensional curl of the pulled-back field).

[L3]

Let $D = D_{1} \cup \dots \cup D_{N}$ be a finite elementary Green region with its supplied decomposition, oriented positively, and let $P, Q$ be $C^{1}$ on an open neighbourhood of $D$ . Then $\int_{\partial D} P d x + Q d y = \iint_{D} (\partial_{x} Q - \partial_{y} P) d A$ (Green's theorem for finite unions of elementary regions).

Proof

technique · direct

1.1

By [F1] and [F5] there is an open $O_{0} \supseteq D$ on which $φ$ is defined and $C^{2}$ . The set $φ^{- 1} [U] \cap O_{0}$ is open, since $φ$ is continuous and $U$ is open, and it contains $D$ because $φ [D] \subseteq U$ ; call it $O$ . Then $O$ is an open neighbourhood of $D$ with $φ$ of class $C^{2}$ on $O$ and $φ [O] \subseteq U$ .

givenF1F5

2.1

By [L2] applied on $O$ , the pulled-back functions $P^{*}$ and $Q^{*}$ of [F1] are $C^{1}$ on $O$ , an open neighbourhood of $D$ , and satisfy $\partial_{u} Q^{*} - \partial_{v} P^{*} = ⟨ (curl F) \circ φ, φ_{u} \times φ_{v} ⟩$ there.

step 1.1F1L2

3.1

The region $D$ is a finite elementary Green region with its supplied decomposition by [F1] and [F3], and $P^{*}, Q^{*}$ are $C^{1}$ on the open neighbourhood $O$ of $D$ by step 2.1. So [L3] applies with the parameter names $u, v$ in place of $x, y$ and gives $\int_{\partial D} P^{*} d u + Q^{*} d v = \iint_{D} (\partial_{u} Q^{*} - \partial_{v} P^{*}) d A .$

step 2.1F1F3L3

4.1

By [F2] the left-hand side of step 3.1 is $\sum_{k = 1}^{m} \int_{σ_{k}} (P^{*}, Q^{*}) \cdot d r$ . Each $σ_{k}$ is a piecewise- $C^{1}$ path with trace in $\partial D \subseteq D \subseteq O$ , and $F$ is continuous on $U \supseteq φ [O]$ , so [L1] rewrites each summand as $\int_{φ \circ σ_{k}} F \cdot d r$ ; summing and using [F1] identifies the left-hand side with $\oint_{φ (\partial D)} F \cdot d r$ .

step 1.1step 3.1F1F2L1

5.1

By step 2.1 the right-hand side of step 3.1 is $\int_{D} ⟨ (curl F) \circ φ, φ_{u} \times φ_{v} ⟩$ , which by [F4] and [F5] is the flux of the $C^{1}$ field $curl F$ through $(D, φ)$ in the orientation induced by $φ$ . With step 4.1 this is the asserted identity.

step 2.1step 3.1step 4.1F4F5∎

Remarks

The identity needs no regularity of the patch; the flux reading does. Steps 3.1 and 4.1 use only that $φ$ is $C^{2}$ near $D$ and that $D$ carries an elementary decomposition. What the regularity of the patch supplies is the right to call $\int_{D} ⟨ (curl F) \circ φ, φ_{u} \times φ_{v} ⟩$ a flux in an orientation, which is [F4]; at parameter points where the oriented area vector vanishes there is no orientation to speak of and the equality still holds.
What the surface is allowed to be. Nothing requires the patch image to be a graph over a coordinate plane, and nothing requires it to be embedded: the companion examples page checks the theorem on a lateral cylinder, which is a graph over no coordinate plane. What is required is that the parameter region be a finite elementary Green region, a hypothesis about the parameter plane and not about the image.
The two sides depend on the parametrization in the same way. Replacing $φ$ by a reparametrization that reverses orientation negates the oriented area vector and reverses the positive boundary chain's image, so both sides change sign together; nothing here asserts independence of the presentation, which is why the theorem is stated for a patch with its parametrization rather than for a surface.

Depends on

Used by

Dependency tree · two levels

50 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

J. Feldman, A. Rechnitzer and E. Yeager, CLP-4 Vector Calculus (University of British Columbia), Theorem 4.4.1 (standard reference, not scraped)
G. Strang and E. Herman, Calculus Volume 3 (OpenStax), Theorem 6.19 (standard reference, not scraped)

The classical Stokes theorem for a C2C2 patch over a finite elementary Green region