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.

Divergence theorem for a volume form

Statement

Assume ${A C}_{ω}$ . Let $M^{n}$ be oriented with boundary, $n \geq 1$ , let $μ$ be a positive smooth volume form, and let $X$ be a compactly supported smooth vector field. Then $\int_{M} ({div}_{μ} X) μ = \int_{\partial M} j^{*} (ι_{X} μ),$ with outward-normal-first orientation. For compact $M$ every smooth $X$ is allowed.

Facts & Assumptions

[F1]

Divergence as an exterior derivative: For a positive volume form $μ$ and smooth vector field $X$ on an oriented smooth $n$ -manifold, $n \geq 1$ , with boundary allowed, $d (ι_{X} μ) = ({div}_{μ} X) μ .$ No tangency assumption on $X$ at the boundary is needed.

[F2]

The general Stokes theorem: 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.

Proof

Given: The objects and hypotheses in the statement above.

1.1

The form $ι_{X} μ$ is smooth and has support contained in $supp X$ , hence compact. Its derivative is $({div}_{μ} X) μ$ by the divergence-form identity.

F1given

2.1

Apply general Stokes to that compactly supported $(n - 1)$ -form. This gives the stated formula and ensures the boundary restriction is compactly supported. On compact $M$ the support of every smooth $X$ is compact; an empty boundary yields zero, as does $X = 0$ . For $n = 1$ the right side is a signed sum of contraction values.

F2step 1.1∎

Depends on

Used by

Agreement with classical Gauss flux in Euclidean space Proposition

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 Theorem 16.32 proof p.424, using arbitrary positive mu in the form identity (standard reference, not scraped)