ExampleConstruction: AI-adaptedVerification: 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.

Both sides of the divergence theorem for $F (x, y, z) = (x^{2}, y^{2}, z^{2})$ on the closed unit box

Example

Let $B = [0, 1]^{3}$ with the six-patch presentation of The closed unit box, with its six faces, is an elementary solid region and let $F (x, y, z) = (x^{2}, y^{2}, z^{2})$ on $R^{3}$ . Then both sides of the divergence theorem equal $3$ : the volume integral of $div F = 2 (x + y + z)$ over $B$ is $3$ , and the six face fluxes are $1$ for each of the faces $x = 1$ , $y = 1$ and $z = 1$ and $0$ for each of the faces $x = 0$ , $y = 0$ and $z = 0$ , so the boundary flux is $3$ as well.

Facts & Assumptions

Given: The box $B = [0, 1]^{3}$ with the six patches $φ_{z^{+}}, φ_{z^{-}}, φ_{x^{+}}, φ_{x^{-}}, φ_{y^{+}}, φ_{y^{-}}$ on $S = [0, 1]^{2}$ of The closed unit box, with its six faces, is an elementary solid region, and the field $F (x, y, z) = (x^{2}, y^{2}, z^{2})$ .

[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), and a map is $C^{k}$ when each component is ( $C^{k}$ Euclidean maps and diffeomorphisms).

[F2]

For a compatible finite patch presentation the oriented flux is the sum of the patch values, each being $\int_{S} (G \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).

[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 $⟨ x, \pm e_{k} ⟩ = \pm x_{k}$ (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$ ).

[L1]

The six faces above, with those parametrizations, make $B$ an elementary solid region, and the oriented area vectors are the constants $e_{z}, - e_{z}, e_{x}, - e_{x}, e_{y}, - e_{y}$ respectively (The closed unit box, with its six faces, is an elementary solid region).

[L2]

For an elementary solid region $E$ with presentation $Σ$ and a $C^{1}$ field $G$ on an open set containing $E$ , $∭_{E} div G = \iint_{\partial E} ⟨ G, n ⟩$ (The divergence theorem on an elementary solid region).

[L3]

For a bounded Jordan set $E \subseteq R^{p + q}$ and integrable $g$ whose sections are integrable outside a content-zero set, $\int_{E} g = \int h (x) d x$ with $h (x) = \int_{E_{x}} g_{x}$ (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable).

[L4]

If $G$ is differentiable at every point of $[a, b]$ with $a < b$ and $G^{'}$ is integrable there, then $\int_{a}^{b} G^{'} = G (b) - G (a)$ (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[L5]

For a natural $m \geq 1$ , the derivative of $t \mapsto t^{m}$ is $t \mapsto m t^{m - 1}$ ; for $m = 0$ the derivative is $0$ (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term). Sums and scalar multiples of differentiable functions differentiate termwise (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$ ).

[L6]

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

Verification

technique · direct

1.1

The three components of $F$ are $x^{2}$ , $y^{2}$ and $z^{2}$ , so by [L5] the partial derivatives $\partial_{x} F_{x} = 2 x$ , $\partial_{y} F_{y} = 2 y$ and $\partial_{z} F_{z} = 2 z$ exist and are continuous on $R^{3}$ , as are the six off-diagonal ones, which vanish. Hence $F$ is $C^{1}$ on $R^{3}$ by [F1] and $div F = 2 x + 2 y + 2 z = 2 (x + y + z)$ .

givenF1L5

1.2

By [L1] the box $B$ with those six patches is an elementary solid region, and $R^{3}$ is an open set containing it, so [L2] applies to $F$ on $B$ .

givenL1L2

2.1

The function $2 (x + y + z)$ is continuous on the compact Jordan set $B$ , hence integrable by [L6]. Applying [L3] to split off the $z$ coordinate and then again to split off $y$ , and evaluating each inner integral by [L4] and [L5]: $\int_{0}^{1} 2 (x + y + z) d z = 2 (x + y) + 1$ , then $\int_{0}^{1} (2 (x + y) + 1) d y = 2 x + 2$ , then $\int_{0}^{1} (2 x + 2) d x = 3$ . So $∭_{B} div F = 3$ by step 1.1.

step 1.1L3L4L5L6

2.2

By [F2] and [F3] the six face fluxes are the integrals over $S$ of $⟨ F (φ_{j}), φ_{j, u} \times φ_{j, v} ⟩$ , which by [L1] is $\pm$ one coordinate of $F$ along the patch. Face by face: on $φ_{z^{+}}$ it is $F_{z} (u, v, 1) = 1$ ; on $φ_{z^{-}}$ it is $- F_{z} (v, u, 0) = 0$ ; on $φ_{x^{+}}$ it is $F_{x} (1, u, v) = 1$ ; on $φ_{x^{-}}$ it is $- F_{x} (0, v, u) = 0$ ; on $φ_{y^{+}}$ it is $F_{y} (v, 1, u) = 1$ ; and on $φ_{y^{-}}$ it is $- F_{y} (u, 0, v) = 0$ . Since $S = [0, 1]^{2}$ , [L3], [L4], and [L5] give $\int_{S} 1 = \int_{0}^{1} \int_{0}^{1} 1 d u d v = 1$ , while $\int_{S} 0 = 0$ ; so the six patch fluxes are $1, 0, 1, 0, 1, 0$ and the boundary flux is their sum, $3$ .

step 1.2F2F3L1L3L4L5

3.1

Steps 2.1 and 2.2 give $3$ for the volume integral and $3$ for the boundary flux, which is what [L2] asserts of them.

step 2.1step 2.2L2∎

Remarks

The three vanishing faces vanish for a reason worth naming. On the face $x = 0$ the flux integrand is $- F_{x}$ evaluated there, and $F_{x} = x^{2}$ is zero on that face; the same happens for $y$ and $z$ . It is the choice of integrand, not any symmetry of the box, that makes half the faces contribute nothing, and each of the six was evaluated rather than inferred.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

97 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)

Both sides of the divergence theorem for F(x,y,z)=(x2,y2,z2)F(x,y,z)=(x2,y2,z2) on the closed unit box