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

Integration on an oriented embedded submanifold

Statement

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.

Facts & Assumptions

[F1]

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.

[F2]

Embedded smooth submanifolds with boundary: An embedded smooth submanifold with boundary of $M$ is a subset $S \subseteq M$ supplied with a manifold-with-boundary smooth structure for which $S ↪ M$ is a smooth embedding. In particular this definition does not assert $S \cap \partial M = \partial S$ .

[F3]

The pullback of a differential form: Let $F : M \to N$ be smooth, and let $ω \in Ω^{k} (N)$ . The pullback $F^{*} ω$ is the pullback of $ω$ viewed as an alternating covariant $k$ -tensor field: $(F^{*} ω)_{p} (v_{1}, \dots, v_{k}) = ω_{F (p)} (d F_{p} v_{1}, \dots, d F_{p} v_{k}) .$

Proof

Given: The objects and hypotheses in the statement above.

1.1

The specified embedding is smooth, so the pointwise formula $j^{*} ω (v_{1}, \dots, v_{k}) = ω (d j v_{1}, \dots, d j v_{k})$ defines a smooth top form on the oriented manifold $S$ . Its assumed compact support makes its intrinsic integral available. This works for empty $S$ , the zero form, and $k = 0$ .

F2F3

2.1

The pointwise pullback formula gives $(j F)^{*} ω = F^{*} (j^{*} ω)$ . Its support is compact because $F$ is a diffeomorphism. Change of variables gives $\int_{T} F^{*} (j^{*} ω) = \int_{S} j^{*} ω$ . A nonproper inclusion does not supply compact support by itself; that condition was explicitly assumed.

F1F3step 1.1∎

Depends on

Used by

A nonzero period obstructs exactness and bounding Corollary
Agreement of general and classical surface Stokes Corollary
Compact-support Stokes on the upper half-space Lemma
Computing form integrals by finite parametrizations Proposition
The general Stokes theorem Theorem

Dependency tree · two levels

9 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 submanifold paragraph p.406 (standard reference, not scraped)