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 volume of a closed ball recovered from the outward flux of the position field
Example
Let be the position field on , and let be the closed ball of radius with the octant presentation of The closed ball is an elementary solid region, presented by the eight spherical octants. Then the outward flux of through is , so The volume of a glued elementary solid is a third of the outward flux of the position field gives
Facts & Assumptions
Given: A radius , the ball , the spherical octant presentation of The closed ball is an elementary solid region, presented by the eight spherical octants, one of its octant parametrizations , and the position field .
For the spherical parametrization , one has (The cross product in , The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine).
The content of a glued elementary solid is one third of the outward flux of the position field through its boundary (The volume of a glued elementary solid is a third of the outward flux of the position field).
For an elementary solid region and a field , (The divergence theorem on an elementary solid region).
The divergence of a field is the sum of its coordinate partial derivatives (Divergence and curl of a vector field).
For a bounded Jordan set and an integrable function whose sections are integrable outside a content-zero exceptional set, Jordan Fubini computes the multiple integral by the corresponding iterated section integrals (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable).
If , is differentiable on , and is integrable there, then (The second fundamental theorem: if is differentiable on with and is integrable, then ).
The flux in the orientation induced by a patch is (Unit normal fields, orientations, and flux through a regular surface patch).
For a finite patch presentation, the total flux is the sum of the patch fluxes (Finitely patched regular surfaces, their area, scalar integrals, and flux).
The closed three-dimensional ball of radius has volume (A closed three-dimensional ball of radius has volume ).
Verification
On each spherical octant patch, [L1], [F2], [F4], and [L7] give .
On each of the four upper octant patches, step 1.1 gives the flux integrand on a parameter rectangle ; for fixed the -section is constant, and for fixed the -section is , so [L4], [L5], and [L6] give the flux value . On each of the four lower octant patches the same argument gives . Summing the eight patch fluxes by [F3] yields the total outward flux .
The field has divergence by [F1], so [L3] and [L2] both identify the content of with one third of the flux computed in step 2.1, namely .
This agrees with the published volume formula [L8]. An inward presentation would reverse the sign of the flux, so the agreement is a check on the orientation convention as well as a computation of the volume.
Remarks
- The flux is independent of how the sphere is cut into octants. The octant presentation matters here because it is the one proved on the A page to be adapted in all three directions.
Depends on
- The closed ball is an elementary solid region, presented by the eight spherical octants
- The volume of a glued elementary solid is a third of the outward flux of the position field
- The divergence theorem on an elementary solid region
- Divergence and curl of a $C^1$ vector field
- Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable
- 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)$
- The derivatives of sine and cosine are cosine and minus sine
- Parity and the Pythagorean identity for sine and cosine
- Unit normal fields, orientations, and flux through a regular surface patch
- Finitely patched regular surfaces, their area, scalar integrals, and flux
- A closed three-dimensional ball of radius $r\ge0$ has volume $4\pi r^3/3$
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- The cross product in $\mathbb R^3$
Used by
Nothing in the library uses this result yet.
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
- M. Corral, Vector Calculus, Example 4.2 (standard reference, not scraped)
- G. Strang and E. Herman, Calculus Volume 3, section 6.8 (standard reference, not scraped)