ExampleConstruction: Literature-sourcedVerification: 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.

The inverse-square field is divergence free, and its flux through the sphere bounding the translated unit ball vanishes

Example

On $U = R^{3} ∖ {0}$ let $F (x, y, z) = \frac{(x, y, z)}{(x^{2} + y^{2} + z^{2})^{3 / 2}} .$ Then $div F = 0$ on $U$ . Consequently the outward flux of $F$ through the sphere bounding the translated unit ball $B = {(x, y, z) : (x^{2} + y^{2} + (z - 2)^{2}) \leq 1}$ is $0$ .

Facts & Assumptions

Given: The field $F$ on $U = R^{3} ∖ {0}$ , and the translated closed unit ball $B = {(x, y, z) : (x^{2} + y^{2} + (z - 2)^{2}) \leq 1}$ .

[L1]

For a finite gluing of elementary solid regions, a $C^{1}$ field on an open set containing the union whose divergence vanishes there has zero outward boundary flux (A field with vanishing divergence has zero outward flux through the boundary of a glued elementary solid).

[L2]

The closed ball admits the octant presentation adapted in all three coordinate directions (The closed ball is an elementary solid region, presented by the eight spherical octants).

[F1]

The divergence of a field is the sum of its coordinate partial derivatives (Divergence and curl of a $C^{1}$ vector field).

[L3]

Products differentiate by the product rule (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[L4]

Composites differentiate by the chain rule (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[L6]

For every real $α$ , the function $s \mapsto s^{α}$ is continuous and differentiable on $(0, \infty)$ , with derivative $α s^{α - 1}$ (Continuity and derivatives of positive-base real powers).

[F2]

The Jacobian matrix records the coordinate partial derivatives (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[F3]

$∥ x ∥_{2} = \sqrt{⟨ x, x ⟩}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L5]

The divergence theorem is the identity $∭_{E} div F = \iint_{\partial E} ⟨ F, n ⟩$ (The divergence theorem on an elementary solid region).

[F4]

Flux is computed against the oriented area vector of a patch (Unit normal fields, orientations, and flux through a regular surface patch).

[F5]

A subset of a metric space is open when every one of its points contains an open metric ball lying in the subset; the Euclidean metric on $R^{3}$ is induced by $∥ \cdot ∥_{2}$ (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space, $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it).

[L7]

Each coordinate projection on Euclidean space is $1$ -Lipschitz and therefore continuous; finite sums and products of continuous real-valued maps are continuous, as are their composites (Vector-valued functions $f : A \to R^{m}$ , their limits and continuity, with the dictionary to the metric notions, Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent, Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined, For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ ).

Verification

technique · direct

1.1

Put $s (x, y, z) = x^{2} + y^{2} + z^{2}$ , which is positive and continuous on $U$ by [L7]. The $i$ th component of $F$ is $F_{i} = x_{i} s^{- 3 / 2}$ . By the product and chain rules [L3, L4], the positive-base power rule [L6], and the coordinate interpretation of partial derivatives [F2], every coordinate partial derivative is $\partial_{j} F_{i} = {\begin{cases} s^{- 3 / 2} - 3 x_{i}^{2} s^{- 5 / 2}, & j = i, \\ - 3 x_{i} x_{j} s^{- 5 / 2}, & j \neq i . \end{cases}$ The coordinate projections are continuous by [L7], so $s$ is continuous; because $s > 0$ on $U$ , [L6] and [L7] make every function in the displayed formulas continuous there. Hence $F$ is $C^{1}$ on $U$ .

L3L4L6L7F2F3given

1.2

Translating the octant presentation of the unit ball by $(0, 0, 2)$ gives an elementary solid region presentation of $B$ , because translation adds a constant to each patch and changes no derivative.

L2F4given

2.1

Summing the three diagonal formulas of step 1.1 gives $div F = 3 s^{- 3 / 2} - 3 s s^{- 5 / 2} = 0$ on $U$ by [F1].

step 1.1F1

2.2

Every point of $B$ has distance at least $1$ from the origin, so $B \subseteq U$ . The set $U$ is open: if $p \in U$ , then $∥ p ∥_{2} > 0$ and the ball $B (p, ∥ p ∥_{2} / 2)$ cannot contain the deleted origin, whose distance from $p$ is $∥ p ∥_{2}$ . Step 1.1 proves that $F$ and all nine coordinate partial derivatives are continuous throughout this open set, so $F$ is $C^{1}$ on an open set containing $B$ .

step 1.1step 1.2F3F5given

3.1

Step 2.1 gives vanishing divergence and step 2.2 gives the required open neighbourhood hypothesis, so [L1] and [L5] give zero outward flux through $\partial B$ .

step 2.1step 2.2L1L5∎

Remarks

The translation in step 1.2 is not cosmetic. The origin is the singular point of the field, so moving the ball off it is exactly what makes the divergence theorem applicable.

Depends on

Used by

FALSE: a field with vanishing divergence has zero outward flux through the boundary of every solid it surrounds False statement

Dependency tree · two levels

116 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, Examples 6.78-6.80 (standard reference, not scraped)
J. Feldman, A. Rechnitzer and E. Yeager, CLP-4 Vector Calculus, Example 4.4.8 (standard reference, not scraped)