TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-09

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 on a bounded C1 Euclidean domain

Statement

Assume ${A C}_{ω}$ . For $n \geq 2$ , a bounded $C^{1}$ domain Omega and $F \in C^{1} (\overline{Ω}; R^{n})$ , $\int_{Ω} div F d x = \int_{\partial Ω} F \cdot ν d S$ . Both integrals are finite, with the continuous interior derivative convention and the outward normal on every boundary component.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ , $n \geq 2$ , a bounded $C^{1}$ domain Omega, and $F \in C^{1} (\overline{Ω}; R^{n})$ with the continuous interior derivative convention.

[F1]

A compact Euclidean set admits a finite subordinate ambient partition. (Finite ambient partitions near compact sets).

[F2]

Localized graph fields satisfy the flux identity and interior fields have zero integral divergence. (The local graph flux calculation).

[F3]

Graph density and continuous outward normal are independent of charts. (Chart and partition independence of surface measure).

[F4]

Finite sums of integrable functions have the sum of their integrals. (The Lebesgue integral is linear on $L^{1} (μ)$ ).

[F5]

A rigid coordinate change preserves volume integrals, by Borel substitution with determinant modulus one, applied to positive and negative parts. (Borel change of variables from the compact-support formula and Radon uniqueness).

Proof

1.1

Compactness of the boundary gives finitely many smaller graph cylinders covering it. Together with the open set Omega these cover the compact closure of Omega. F1 gives an ambient partition chi_j subordinate to this cover. For each boundary term chi_j F, F2 and F3 identify its divergence integral with its outward surface flux, since $ν d S = (- D h, 1) d y$ . The interior term has divergence integral zero and boundary trace zero by F2. Rigid coordinate changes preserve this calculation: the transformed field is $Q^{T} F (a + Q y)$ , its derivative is $Q^{T} D F Q$ and has the same trace, its dot products are unchanged, and its volume Jacobian has modulus one.

givenF1F2F3F5

2.1

The continuous F and DF are bounded on the compact closure; Omega is bounded of finite volume and F3 gives finite boundary area. Thus all terms are integrable. The product rule gives $\sum_{j} div (χ_{j} F) = (\sum_{j} χ_{j}) div F + (\sum_{j} D χ_{j}) \cdot F = div F$ , because the partition sum is one on a neighborhood of the closure. The boundary flux sum likewise equals $F \cdot ν$ . F4 sums the local identities from step 1.1 to give the stated theorem.

step 1.1F3F4algebra∎

Source notes

Hunter §1.12 Theorem 1.46, printed pp. 17–18; Oh §3.9 Proposition 3.23, printed/PDF pp. 47–48, for the local-to-global proof.

Depends on

Used by

First Green identity Corollary
The wrong normal gives the wrong sign Counterexample
Flux and scaling on balls Example
Euclidean divergence and the Stokes comparison Remark

Dependency tree · two levels

47 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

Hunter, Notes on Partial Differential Equations (standard reference, not scraped)
Sung-Jin Oh, Lecture Notes for Math 222A (standard reference, not scraped)