ExampleConstruction: Literature-sourcedVerification: 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.

Stokes' theorem on a flat disc and on a hemisphere with the same induced boundary circle

Example

Let $F (x, y, z) = (- y, x, 0)$ . Then $curl F = (0, 0, 2)$ . Stokes' theorem gives the same value $2 π$ on two different $C^{2}$ patches with the same induced boundary circle: the flat unit disc in the plane $z = 0$ , and the upper unit hemisphere.

Facts & Assumptions

Given: The field $F (x, y, z) = (- y, x, 0)$ , the polar disc patch $ψ (r, θ) = (r \cos θ, r \sin θ, 0)$ on $[0, 1] \times [0, 2 π]$ , and the hemisphere patch $φ (ϕ, θ) = (\sin ϕ \cos θ, \sin ϕ \sin θ, \cos ϕ)$ on $[0, π / 2] \times [0, 2 π]$ .

[L1]

Stokes' theorem identifies circulation around the induced boundary chain with the curl flux in the induced orientation (The classical Stokes theorem for a $C^{2}$ patch over a finite elementary Green region).

[F1]

The induced boundary chain is obtained by composing the positive boundary chain of the parameter region with the parametrization (The induced boundary chain and circulation of a $C^{2}$ patch over a finite elementary Green region).

[F2]

The curl is $(\partial_{y} F_{z} - \partial_{z} F_{y}, \partial_{z} F_{x} - \partial_{x} F_{z}, \partial_{x} F_{y} - \partial_{y} F_{x})$ (Divergence and curl of a $C^{1}$ vector field).

[F3]

A regular patch has no interior parameter point sharing its image with a distinct point of the parameter region (Regular parametrized surface patches on compact Jordan parameter regions).

[F4]

Flux is computed as $\int_{D} (F \circ φ) \cdot (φ_{u} \times φ_{v})$ (Unit normal fields, orientations, and flux through a regular surface patch).

[F5]

The cross product is that of The cross product in $R^{3}$ .

[L2]

$(\sin t)^{'} = \cos t$ and $(\cos t)^{'} = - \sin t$ (The derivatives of sine and cosine are cosine and minus sine).

[L3]

$\sin^{2} t + \cos^{2} t = 1$ (Parity and the Pythagorean identity for sine and cosine).

[L4]

Sine is positive on $(0, π)$ and cosine is strictly decreasing on $[0, π]$ (Signs, monotonicity intervals, and ranges of sine and cosine).

[L8]

The map $θ \mapsto (\cos θ, \sin θ)$ is injective on $[0, 2 π)$ ( $t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle).

[L5]

Jordan Fubini computes a multiple integral by iterated section integrals (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable).

[L6]

If $a < b$ , $G$ is differentiable on $[a, b]$ , and $G^{'} = f$ is integrable there, then $\int_{a}^{b} f = G (b) - G (a)$ (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[F6]

A rectangle is an elementary Green region (Type I, Type II, and elementary regions for Green's theorem).

[F7]

The positive boundary of a rectangle runs along its four sides in the usual counterclockwise order (Positive orientation of elementary-region boundaries).

[L7]

Line integrals negate under path reversal (Line integrals under reversal and concatenation).

[F8]

Vector line integrals are computed from $⟨ F (γ (t)), γ^{'} (t) ⟩$ (Scalar line integrals with respect to arc length and vector-field line integrals).

[F9]

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

Verification

technique · direct

1.1

Direct differentiation in [F2] gives $curl F = (0, 0, 2)$ .

F2given

1.2

The disc patch $ψ$ is $C^{2}$ on a neighbourhood of its parameter rectangle. On the parameter interior one has $r > 0$ , and [F5], [L2], and [L3] give $ψ_{r} \times ψ_{θ} = (0, 0, r) \neq 0$ there. Equality of two images forces equality of the positive radii by [L3] and then equality of their angles by [L8], so no interior parameter point shares its image with a distinct one. Thus [F3] makes $ψ$ a regular patch over a rectangle.

F3F5F6L2L3L8

1.3

The hemisphere patch $φ$ is $C^{2}$ on a neighbourhood of its parameter rectangle, and [F5], [L2], and [L3] give $φ_{ϕ} \times φ_{θ} = \sin ϕ φ (ϕ, θ)$ . On the parameter interior one has $0 < ϕ < π / 2$ , hence $\sin ϕ > 0$ by [L4], so this cross product is nonzero there; and the third coordinate $\cos ϕ$ fixes $ϕ$ because [L4] makes cosine injective on $[0, π]$ , while the first two then fix $θ$ by [L8]. Thus [F3] makes $φ$ a regular patch over a rectangle.

F3F5F6L2L3L4L8

2.1

By [F1], [F7], [L7], and [F8], the two radial edges of the rectangle cancel in the induced boundary chain, the edge at $r = 0$ is constant, and what remains is the unit circle $θ \mapsto (\cos θ, \sin θ, 0)$ traversed once counterclockwise.

step 1.2F1F7L7F8

3.1

The curl flux on the disc is $\int_{0}^{2 π} \int_{0}^{1} 2 r d r d θ = 2 π$ by [F4], [F9], [L5], and [L6], and the circulation around the surviving boundary circle is $\int_{0}^{2 π} 1 d θ = 2 π$ , so [L1] is verified on the disc.

step 1.1step 1.2step 2.1F4F9L5L6L1

3.2

By [F1], [F7], [L7], and [F8], the two meridian edges cancel in the induced boundary chain, the edge at $ϕ = 0$ is constant, and the remaining edge at $ϕ = π / 2$ is the same counterclockwise unit circle as in step 2.1.

step 1.3F1F7L7F8

4.1

The curl flux on the hemisphere is $\int_{0}^{2 π} \int_{0}^{π / 2} 2 \sin ϕ \cos ϕ d ϕ d θ = 2 π$ by [F4], [F9], [L5], and [L6], so [L1] gives the same circulation value there.

step 1.1step 1.3step 3.2F4F9L5L6L1

5.1

Steps 2.1 and 3.2 give the same induced boundary circle, and steps 3.1 and 4.1 give the same value $2 π$ , so the two surfaces agree exactly as Stokes' theorem predicts.

step 2.1step 3.1step 3.2step 4.1L1∎

Remarks

The shared boundary is written out, not inferred from the informal phrase "the same spanning curve". The cancellations on the parameter boundary are part of the computation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

74 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, Examples 4.4.2-4.4.4 (standard reference, not scraped)
M. Corral, Vector Calculus, Examples 4.5.3 and 4.5.4 (standard reference, not scraped)
G. Strang and E. Herman, Calculus Volume 3, Examples 6.73 and 6.74 (standard reference, not scraped)