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.
Agreement of general and classical surface Stokes
Statement
Assume . Let be a compact oriented smooth embedded surface with boundary, and let be smooth on an open neighborhood of . Set and . Then On an oriented parametrization the latter integrand is ; on a boundary curve it is . On the common smooth patch scope this is the published classical Stokes theorem, using the standard Euclidean metric identification.
Facts & Assumptions
The general Stokes theorem: Assume . Let be an oriented smooth -manifold with boundary, , and let . With and the outward-normal-first orientation, An empty boundary contributes zero; in dimension one its integral is a finite signed sum of point values.
Integration on an oriented embedded submanifold: Let be an oriented embedded smooth -submanifold, with boundary allowed. For a smooth -form on such that has compact support on , define . If is an orientation-preserving diffeomorphism, this equals . Compact support is required on itself.
Computing form integrals by finite parametrizations: Let , let be oriented, and let . For let be bounded open Jordan domains and continuous and smooth up to the boundary in target coordinates: near each parameter point, a target coordinate representative extends smoothly to a Euclidean neighborhood. Suppose is an orientation-preserving diffeomorphism onto an open , the are pairwise disjoint, and . Then An empty family is allowed when the support is empty. No nonsingularity of on , and no -valued extension across a genuine target boundary, is assumed.
The classical Stokes theorem for a patch over a finite elementary Green region: Let be a patch over a finite elementary Green region (def-the-induced-boundary-chain-of-a-c2-surface-patch), with positive boundary chain and induced boundary chain , and let be a vector field on an open set containing . Then the circulation around the induced boundary chain equals the flux of the curl in the induced orientation: The right-hand side is the flux of through the patch in the orientation induced by , in the sense of def-oriented-unit-normal-and-flux-of-a-surface-patch.
Divergence and curl of a vector field: Let , let be open and let be in the componentwise Euclidean sense of def-ck-euclidean-maps-and-diffeomorphisms. Then the divergence of is , the function whose value at is . The partial derivatives are those of def-directional-and-partial-derivatives, and the sum is the finite sum used throughout def-euclidean-inner-product. Since each is continuous on , so is . Now let and let be on an open . Following def-cross-product-in-r3, write the three coordinates of a point and of a vector as rather than , so that means and are . With that naming, the curl of is , a map each of whose coordinates is continuous on . In this naming the divergence reads . Both operators are defined pointwise from the first partial derivatives of the components, so no differentiability of beyond is used and no orientation or metric structure enters beyond the standard coordinates of def-jacobian-matrix-and-gradient. For a scalar function on , the gradient is that of def-jacobian-matrix-and-gradient; in the three-coordinate naming, .
Proof
Given: The objects and hypotheses in the statement above.
Expand . Its coefficients of are respectively , exactly the three curl components. Contraction with gives the same expansion.
Pull back to the compact surface and apply general Stokes, obtaining the integral identity. Evaluating the contracted three-form on gives . The boundary pullback of is directly.
The finite-parametrization theorem turns these expressions into the scalar flux and circulation integrals. For a patch over a supplied finite elementary Green region with its induced boundary chain, the classical theorem has exactly these two integrals; smooth meet its requirements. Reversing the surface orientation changes both signs; empty surface or zero field gives zero.
Depends on
Used by
- Surface Stokes on a graph disk Example
Dependency tree · two levels
29 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
- Lee Theorem 16.34 proof, p.427 (standard reference, not scraped)