CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

A field with vanishing divergence has zero outward flux through the boundary of a glued elementary solid

Statement

Let a finite gluing of elementary solid regions be given, with union $E$ and outer boundary presentation $Σ^{o u t}$ , and let $F$ be a $C^{1}$ vector field on an open set $O$ containing $E$ . If the divergence vanishes on an open set containing the solid then the outward boundary flux is zero: if $div F = 0$ at every point of $O$ , then

$\iint_{\partial E} ⟨ F, n ⟩ = 0.$

The hypothesis is that $F$ is $C^{1}$ with vanishing divergence on an open set containing the whole of $E$ , not merely on $\partial E$ and not merely wherever $F$ happens to be defined.

Facts & Assumptions

Given: The finite gluing with union $E$ and outer presentation $Σ^{o u t}$ , the open set $O \supseteq E$ , and the $C^{1}$ field $F$ on $O$ with $div F = 0$ throughout $O$ .

[F1]

The divergence of a $C^{1}$ field is $div G = \sum_{i < n} \partial_{i} G_{i}$ (Divergence and curl of a $C^{1}$ vector field).

[F2]

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]

For a finite gluing with union $E$ and outer presentation $Σ^{o u t}$ and a $C^{1}$ field $G$ on an open set containing $E$ , $∭_{E} div G = \iint_{\partial E} ⟨ G, n ⟩$ (The divergence theorem for finite gluings of elementary solid regions).

[L2]

For a finite gluing, $E$ is compact and Jordan measurable (Internal faces cancel and volume integrals add when elementary solid regions are glued).

[L3]

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}$ ).

Proof

technique · direct

1.1

By [L2] the set $E$ is compact and Jordan measurable, and by hypothesis and [F1] the function $div F$ is identically zero on $E$ . Its zero extension to a bounding rectangle is the zero function, which by [L3] with $α = β = 0$ is integrable with integral $0$ ; so $\int_{E} div F = 0$ by [F2].

givenF1F2L2L3

2.1

The field $F$ is $C^{1}$ on the open $O \supseteq E$ , so [L1] applies and gives $\iint_{\partial E} ⟨ F, n ⟩ = ∭_{E} div F$ , which is $0$ by step 1.1.

step 1.1L1∎

Remarks

The hypothesis is about an open set containing $E$ , and that is exactly what fails in the standard counterexample. The inverse-square field has vanishing divergence at every point where it is defined, yet its outward flux through the unit sphere is $4 π$ ; the field is not defined at the origin, so no open set containing the closed unit ball carries it. The companion examples page states the false weakening and carries the computation.

Depends on

Used by

Dependency tree · two levels

40 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

G. Strang and E. Herman, Calculus Volume 3 (OpenStax), section 6.8 (standard reference, not scraped)