TheoremStatement: 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.

The general Stokes theorem

Statement

Assume ${A C}_{ω}$ . Let $M$ be an oriented smooth $n$ -manifold with boundary, $n \geq 1$ , and let $η \in Ω_{c}^{n - 1} (M)$ . With $j : \partial M ↪ M$ and the outward-normal-first orientation, $\int_{M} d η = \int_{\partial M} j^{*} η .$ An empty boundary contributes zero; in dimension one its integral is a finite signed sum of point values.

Facts & Assumptions

[F1]

Compact-support Stokes on the upper half-space: Give $H^{n} = {x_{n} \geq 0}$ the standard orientation, $n \geq 1$ , and its face the outward-normal-first orientation. If $η \in Ω_{c}^{n - 1} (H^{n})$ and $j : \partial H^{n} ↪ H^{n}$ , then $\int_{H^{n}} d η = \int_{\partial H^{n}} j^{*} η .$ With $η = \sum_{i} a_{i} d x^{1} \land \dots \land \hat{d x^{i}} \land \dots \land d x^{n}$ , both sides are $(- 1)^{n} \int_{R^{n - 1}} a_{n} (x^{'}, 0) d x^{'}$ for $n > 1$ , and $- a_{1} (0)$ for $n = 1$ .

[F2]

Localization of Stokes by a partition of unity: Assume ${A C}_{ω}$ . Let $M^{n}$ be oriented with boundary, $n \geq 1$ , $η \in Ω_{c}^{n - 1} (M)$ , and $(ρ_{i})$ a smooth chart partition. Then $η = \sum_{i} ρ_{i} η, d η = \sum_{i} d (ρ_{i} η), \sum_{i} d ρ_{i} \land η = 0,$ with only finitely many nonzero form summands. Boundary restrictions have the corresponding finite localization and compact support, so these identities can be integrated termwise.

[F3]

Change of variables on oriented manifolds: Let $F : M \to N$ be a diffeomorphism of oriented smooth $n$ -manifolds and $ω \in Ω_{c}^{n} (N)$ . If $F$ preserves orientation everywhere, $\int_{M} F^{*} ω = \int_{N} ω$ ; if it reverses orientation everywhere, $\int_{M} F^{*} ω = - \int_{N} ω$ . If the sign varies between components, apply the appropriate signed equality on each component and add.

[F4]

Integration on an oriented embedded submanifold: Let $j : S ↪ M$ 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 $\int_{S} ω : = \int_{S} j^{*} ω$ . If $F : T \to S$ is an orientation-preserving diffeomorphism, this equals $\int_{T} (j F)^{*} ω$ . Compact support is required on $S$ itself.

[F5]

The boundary of a positive-dimensional manifold is a closed embedded smooth (n-1)-manifold: If $M$ has dimension $n \geq 1$ , the restrictions of boundary charts to their faces give $\partial M$ the structure of a closed embedded smooth boundaryless $(n - 1)$ -manifold. For $n = 0$ , $\partial M = \emptyset$ .

Proof

Given: The objects and hypotheses in the statement above.

1.1

Choose a chart partition and write the finite localization $η = \sum_{i} η_{i}$ with $η_{i} = ρ_{i} η$ . Its derivative localizes by the partition cancellation lemma. The boundary is closed, so the restriction support lies in the compact set $supp η \cap \partial M$ ; both integrals are defined.

F2F4F5

1.2

For a boundary-chart term, extend the coordinate primitive by zero across artificial edges within $H^{n}$ . It remains smooth there, has compact support, and exterior differentiation commutes with its chart pullback by the local calculus used in the localization lemma. Apply half-space Stokes. Multiplication by the ambient chart sign multiplies the induced boundary sign by the same number: the transition preserves the outward side, and outward-first compares the two determinant rays. The signed change-of-variables formula therefore turns the local equality into $\int_{M} d η_{i} = \int_{\partial M} j^{*} η_{i}$ .

F1F2F3

2.1

For an interior-chart term the Euclidean calculation in the half-space lemma’s dependency gives zero integral and zero boundary restriction. Equivalently translate its compact Euclidean support into the interior of $H^{n}$ and use the half-space identity with zero face value. Sum all finitely many equalities and use the localization identities to obtain Stokes. Empty support and empty boundary are included. For $n = 1$ the local formula is the negative point value, transported with its chart sign; hence the boundary integral is exactly the specified signed sum.

F1F2F3step 1.1step 1.2∎

Depends on

Used by

A compactly supported primitive has zero total derivative integral Corollary
Agreement of general and classical surface Stokes Corollary
Closed forms have zero boundary integral Corollary
General Stokes agrees with both planar Green formulas Corollary
Stokes agrees with the fundamental theorem of calculus Corollary
An exact top form with nonzero integral on a disk Example
False: all exact forms integrate to zero everywhere False statement
Divergence theorem for a volume form Theorem

Dependency tree · two levels

20 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.11, pp.411–414; Merry Theorem 26.16 (standard reference, not scraped)