Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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 ACω. Let SR3 be a compact oriented smooth embedded surface with boundary, and let F be smooth on an open neighborhood of S. Set α=Fxdx+Fydy+Fzdz and μ=dxdydz. Then dα=ιcurlFμ,Sα=SιcurlFμ. On an oriented parametrization r(u,v) the latter integrand is (curlF)(r)(ru×rv)dudv; on a boundary curve it is F(r)rdt. On the common smooth patch scope this is the published classical Stokes theorem, using the standard Euclidean metric identification.

Facts & Assumptions

[F1]

The general Stokes theorem: Assume ACω. Let M be an oriented smooth n-manifold with boundary, n1, and let ηΩcn1(M). With j:MM and the outward-normal-first orientation, Mdη=Mjη. An empty boundary contributes zero; in dimension one its integral is a finite signed sum of point values.

[F2]

Integration on an oriented embedded submanifold: Let j:SM be an oriented embedded smooth k-submanifold, with boundary allowed. For a smooth k-form ω on M such that jω has compact support on S, define Sω:=Sjω. If F:TS is an orientation-preserving diffeomorphism, this equals T(jF)ω. Compact support is required on S itself.

[F3]

Computing form integrals by finite parametrizations: Let n1, let Mn be oriented, and let ωΩcn(M). For 1im let DiRn be bounded open Jordan domains and Fi:DiM 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 FiDi is an orientation-preserving diffeomorphism onto an open WiM, the Wi are pairwise disjoint, and suppωiWi. Then Mω=i=1mDiFiω. An empty family is allowed when the support is empty. No nonsingularity of DFi on Di, and no M-valued extension across a genuine target boundary, is assumed.

[F4]

The classical Stokes theorem for a C2 patch over a finite elementary Green region: Let (D,φ) be a C2 patch over a finite elementary Green region (def-the-induced-boundary-chain-of-a-c2-surface-patch), with positive boundary chain D=(σ1,,σm) and induced boundary chain φ(D), and let F be a C1 vector field on an open set UR3 containing φ[D]. Then the circulation around the induced boundary chain equals the flux of the curl in the induced orientation: φ(D)Fdr=D(curlF)φ, φu×φv. The right-hand side is the flux of curlF through the patch in the orientation induced by φ, in the sense of def-oriented-unit-normal-and-flux-of-a-surface-patch.

[F5]

Divergence and curl of a C1 vector field: Let n1, let URn be open and let F=(F0,,Fn1):URn be C1 in the componentwise Euclidean sense of def-ck-euclidean-maps-and-diffeomorphisms. Then the divergence of F is divF:=i<niFi, the function UR whose value at p is i<niFi(p). 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 iFi is continuous on U, so is divF. Now let n=3 and let F:UR3 be C1 on an open UR3. Following def-cross-product-in-r3, write the three coordinates of a point and of a vector as x,y,z rather than 0,1,2, so that F=(Fx,Fy,Fz) means F=(F0,F1,F2) and x,y,z are 0,1,2. With that naming, the curl of F is curlF:=(yFzzFy, zFxxFz, xFyyFx), a map UR3 each of whose coordinates is continuous on U. In this naming the divergence reads divF=xFx+yFy+zFz. Both operators are defined pointwise from the first partial derivatives of the components, so no differentiability of F beyond C1 is used and no orientation or metric structure enters beyond the standard coordinates of def-jacobian-matrix-and-gradient. For a C1 scalar function f on U, the gradient f=(0f,,n1f) is that of def-jacobian-matrix-and-gradient; in the three-coordinate naming, f=(xf,yf,zf).

Proof

Given: The objects and hypotheses in the statement above.

1.1

Expand dα. Its coefficients of dydz,dzdx,dxdy are respectively yFzzFy,zFxxFz,xFyyFx, exactly the three curl components. Contraction with μ gives the same expansion.

F5algebra
2.1

Pull back to the compact surface and apply general Stokes, obtaining the integral identity. Evaluating the contracted three-form on (ru,rv) gives det(curlF,ru,rv)=(curlF)(ru×rv). The boundary pullback of α is F(r)rdt directly.

F1F2step 1.1
3.1

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 r,F meet its C2,C1 requirements. Reversing the surface orientation changes both signs; empty surface or zero field gives zero.

F3F4step 2.1

Depends on

Used by

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