TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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 divergence theorem on an elementary solid region

Statement

Let $E$ be an elementary solid region with presentation $Σ = ((D_{1}, φ_{1}), \dots, (D_{P}, φ_{P}))$ (Elementary solid regions: one boundary presentation adapted in all three coordinate directions) and let $F$ be a $C^{1}$ vector field on an open set containing $E$ . Then

$∭_{E} div F = \iint_{\partial E} ⟨ F, n ⟩,$

where the left side is the integral of $div F$ over $E$ and the right side is the flux of $F$ over the presentation $Σ$ , that is $\sum_{j = 1}^{P} \int_{D_{j}} ⟨ F (φ_{j}), φ_{j, u} \times φ_{j, v} ⟩$ . At every interior parameter point whose projection lies in the interior of the relevant base, the orientation in which that flux is taken is the outward one, by Every patch of an elementary solid region's presentation is a graph face in some direction, and at interior base points its normal is outward.

Facts & Assumptions

Given: The elementary solid region $E$ with its three simple descriptions, its presentation $Σ$ and the three partitions of ${1, \dots, P}$ into sublists, and the $C^{1}$ field $F$ on an open $O \supseteq E$ .

[F1]

For a compatible finite patch presentation the oriented flux is the sum of the patch values, each being $\int_{D_{j}} (F \circ φ_{j}) \cdot (φ_{j, u} \times φ_{j, v})$ (Finitely patched regular surfaces, their area, scalar integrals, and flux, Unit normal fields, orientations, and flux through a regular surface patch).

[F2]

The divergence of a $C^{1}$ field $F$ on an open subset of $R^{n}$ is $div F = \sum_{i < n} \partial_{i} F_{i}$ (Divergence and curl of a $C^{1}$ vector field).

[F3]

For $x, y \in R^{m}$ , $⟨ x, y ⟩ = \sum_{i < m} x_{i} y_{i}$ , and $e_{k}$ has $k$ th coordinate $1$ and the others $0$ ; so a vector $v \in R^{3}$ is $v_{x} e_{x} + v_{y} e_{y} + v_{z} e_{z}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ ).

[F4]

An elementary solid region carries one presentation adapted to a simple description of $E$ in each of the three coordinate directions (Elementary solid regions: one boundary presentation adapted in all three coordinate directions, Simple solid regions in a coordinate direction and their cyclic coordinate projection).

[F5]

Integration over a bounded Jordan measurable set is integration of the zero extension over a bounding rectangle (The Riemann integral of a bounded function over a bounded Jordan measurable set).

[L1]

Let $(k, D, γ_{1}, γ_{2})$ be a simple description of $E$ in the direction $k$ , let $Σ$ be adapted to it, and let $R$ be $C^{1}$ on an open set containing $E$ . Then the flux of $R e_{k}$ over the presentation equals the integral of the $k$ th partial derivative of $R$ over $E$ (The single-direction flux identity on a simple solid region).

[L2]

For integrable $f, g$ on a nondegenerate rectangle and scalars $α, β$ , the function $α f + β g$ is integrable with integral $α \int f + β \int g$ (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ ).

[L3]

Every continuous real function on a compact Jordan measurable set is Riemann integrable over it (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set).

Proof

technique · direct

1.1

By [F3] the field splits as $F = F_{x} e_{x} + F_{y} e_{y} + F_{z} e_{z}$ on $O$ , each $F_{k}$ being a $C^{1}$ real function there. For each patch, [F1] and [F3] make the flux integrand $⟨ F (φ_{j}), φ_{j, u} \times φ_{j, v} ⟩ = \sum_{k} F_{k} (φ_{j}) (φ_{j, u} \times φ_{j, v})_{k}$ , a sum of three continuous functions on the compact Jordan parameter region $D_{j}$ ; each is integrable by [L3], so [L2] and [F5] split that patch's flux into the three corresponding patch fluxes of the fields $F_{k} e_{k}$ . Summing over $j$ and using [F1] again, the flux of $F$ over $Σ$ is the sum over $k$ of the fluxes of $F_{k} e_{k}$ over $Σ$ .

givenF1F3F5L2L3

1.2

Fix a direction $k$ . By [F4] the same presentation $Σ$ is adapted to the $k$ th simple description of $E$ , and $F_{k}$ is $C^{1}$ on the open $O \supseteq E$ , so [L1] applies and gives that the flux of $F_{k} e_{k}$ over $Σ$ equals $\int_{E} \partial_{k} F_{k}$ . This holds for each of the three directions, with the one presentation and the three descriptions supplied with $E$ .

givenF4L1

2.1

Adding the three identities of step 1.2 and substituting into step 1.1, the flux of $F$ over $Σ$ equals $\int_{E} \partial_{x} F_{x} + \int_{E} \partial_{y} F_{y} + \int_{E} \partial_{z} F_{z}$ . Each $\partial_{k} F_{k}$ is continuous on the compact Jordan set $E$ , hence integrable over it by [L3], so [L2] and [F5] combine those three integrals into $\int_{E} (\partial_{x} F_{x} + \partial_{y} F_{y} + \partial_{z} F_{z})$ , which is $\int_{E} div F$ by [F2].

step 1.1step 1.2F2F5L2L3

3.1

Step 2.1 is the asserted identity. The requirement that one presentation be adapted in all three directions is used exactly once, in step 1.2, where the three applications of [L1] must be to the same boundary integral; and the outward reading of the normals is Every patch of an elementary solid region's presentation is a graph face in some direction, and at interior base points its normal is outward, on which no step above depends.

step 2.1∎

Remarks

The field must be $C^{1}$ on an open set containing all of $E$ , not only on $\partial E$ . Step 1.2 integrates $\partial_{k} F_{k}$ over the whole solid, so the partial derivatives must exist there. The companion examples page records the failure that quietly weakening this hypothesis produces.
Nothing is asserted for a solid presented without the data. The three descriptions, the presentation and the three sortings are hypotheses. A compact set with a piecewise smooth boundary may admit them, may admit them only after being cut into pieces — which is what The divergence theorem for finite gluings of elementary solid regions is for — or may not be shown to admit them by anything on this page.

Depends on

Used by

Dependency tree · two levels

78 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

J. Feldman, A. Rechnitzer and E. Yeager, CLP-4 Vector Calculus (University of British Columbia), Theorem 4.2.2 (standard reference, not scraped)
G. Strang and E. Herman, Calculus Volume 3 (OpenStax), Theorem 6.20 (standard reference, not scraped)