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 closed ball is an elementary solid region, presented by the eight spherical octants
Example
Fix and let Let on , and cut the parameter rectangle at and at . The eight restrictions of to the resulting closed rectangles form one outward finite patch presentation of adapted in all three coordinate directions, so is an elementary solid region.
Facts & Assumptions
Given: A real radius ; the spherical parametrization ; the intervals , , and , , , ; and the eight restricted patches .
An elementary solid region is a compact solid equipped with one compatible finite patch presentation of its boundary that is adapted to a simple description in each coordinate direction (Elementary solid regions: one boundary presentation adapted in all three coordinate directions).
A simple description in the direction has the form (Simple solid regions in a coordinate direction and their cyclic coordinate projection).
In an adapted outward boundary presentation, the projected images of the upper sublist are pairwise disjoint and fill the base up to content zero (Boundary presentations adapted to a simple solid region in a coordinate direction).
A regular patch has no interior parameter point with the same image as a distinct point of the parameter region (Regular parametrized surface patches on compact Jordan parameter regions).
In a compatible finite patch presentation, distinct patches meet only with content-zero overlap in each parameter region (Finitely patched regular surfaces, their area, scalar integrals, and flux).
The cross product in is (The cross product in ).
For a patch of two variables, in each coordinate direction (Each coordinate of the oriented area vector is the Jacobian determinant of the matching cyclic projection).
Sine is positive on and negative on ; cosine is positive on , negative on , and strictly decreasing on ; and both functions take values in (Signs, monotonicity intervals, and ranges of sine and cosine, Quarter-turn values and shifts by pi/2 and pi).
, , , and (Quarter-turn values and shifts by pi/2 and pi).
Integration over a Jordan set is that of its zero extension (The Riemann integral of a bounded function over a bounded Jordan measurable set).
A bounded set is Jordan measurable exactly when its boundary has content zero (A bounded set in is Jordan measurable iff its boundary is null, equivalently of content zero).
Choosing rather than is an orientation (Unit normal fields, orientations, and flux through a regular surface patch).
A closed disc of radius has Jordan content (A closed disc of radius has Jordan content ).
A set has content zero when it can be covered by finitely many cubes of arbitrarily small total volume, and content zero passes to subsets (Measure zero and content zero in by countable and finite cube covers).
A continuous graph over a compact nondegenerate rectangle has content zero (The graph of a continuous function on a closed nondegenerate rectangle in has content zero in ).
The map is injective on ( is a bijection from onto the real unit circle).
Verification
The eight parameter rectangles are , obtained by cutting the spherical parameter rectangle at the quarter turns named in [L5].
Differentiating gives and , and [F6], [L2], and [L3] give .
On the interior of each rectangle one has by [L4], so step 2.1 gives a nonzero oriented area vector. If two interior parameter points have the same image, their third coordinates give the same ; strict monotonicity of cosine on gives the same , and the first two coordinates then give the same point of the unit circle, so [L9] gives the same . Thus each restriction is injective on its interior. Two distinct octants meet only along boundary arcs whose preimages have content zero and contain no point that is interior for both patches. Hence the eight restrictions are regular and compatible in the senses of [F4] and [F5].
In the direction the base is the closed disc and the two boundary functions are and , so [F2] describes ; the third coordinate of the oriented area vector is , so by [L4] the four patches with form the upper sublist and the four with form the lower sublist, with no lateral patch because the vanishing set or lies on parameter boundaries.
In the direction the base is the closed disc and the boundary functions are and , so [F2] again describes . The first coordinate of the oriented area vector is , so by [L4] the four octants with form the upper sublist and the other four the lower sublist; the vanishing set or lies on parameter boundaries, so there is no lateral patch.
In the direction the base is the closed disc and the boundary functions are and , so [F2] describes a third time. The second coordinate of the oriented area vector is , so the split is by against ; again the vanishing set lies on parameter boundaries, so there is no lateral patch.
The projections of the interiors of the four upper octants onto the plane are the four open quarter discs, pairwise disjoint, and the same is true for the four lower octants; each union misses only the two coordinate diameters and the boundary circle of . The circle has content zero because the closed disc is Jordan measurable by [L6] and [L7], so its boundary has content zero; each diameter is a continuous graph over a compact interval and has content zero by [L8]; and the finite union of those three sets has content zero by [F9]. Thus both graph sublists satisfy the coverage clause in the direction.
In the direction the projections onto the plane of the four upper octants are the four open quarter discs of , pairwise disjoint: gives the half with and the half with , and in each half the two choices and split by the sign of . The four lower octants have the same projected images, now coming from and . In each case the omitted set is the union of the two coordinate diameters and the boundary circle of , which has content zero by the same argument as in step 4.1. Thus both graph sublists satisfy the coverage clause in the direction.
In the direction the projections onto the plane of the four upper octants are the four open quarter discs of , pairwise disjoint: gives the half with or according to whether or , and the two halves are split again by the sign of . The four lower octants have the same projected images. The omitted set is the union of the two coordinate diameters and the boundary circle of , hence has content zero by the same argument as in step 4.1. So both graph sublists satisfy the coverage clause in the direction.
Steps 3.1, 3.2, 4.1, 3.3, 5.1, 3.4, and 5.2 show that the same eight patches are compatible and adapted in all three coordinate directions, and step 2.1 gives them the outward orientation. Therefore [F1] makes with this presentation an elementary solid region.
Remarks
-
The cuts at both and the four azimuth quadrants are load-bearing. Without the azimuth cuts, the and coordinates of the oriented area vector would change sign inside one parameter interior.
-
The poles are harmless: step 3.1 uses that they lie on parameter boundaries, so their vanishing oriented area vector does not violate regularity.
Depends on
- Elementary solid regions: one boundary presentation adapted in all three coordinate directions
- Simple solid regions in a coordinate direction and their cyclic coordinate projection
- Boundary presentations adapted to a simple solid region in a coordinate direction
- Regular parametrized surface patches on compact Jordan parameter regions
- Finitely patched regular surfaces, their area, scalar integrals, and flux
- The cross product in $\mathbb R^3$
- Each coordinate of the oriented area vector is the Jacobian determinant of the matching cyclic projection
- The derivatives of sine and cosine are cosine and minus sine
- Parity and the Pythagorean identity for sine and cosine
- Signs, monotonicity intervals, and ranges of sine and cosine
- $t\mapsto(\cos t,\sin t)$ is a bijection from $[0,2\pi)$ onto the real unit circle
- Quarter-turn values and shifts by pi/2 and pi
- The Riemann integral of a bounded function over a bounded Jordan measurable set
- A bounded set in $\mathbb{R}^m$ is Jordan measurable iff its boundary is null, equivalently of content zero
- Unit normal fields, orientations, and flux through a regular surface patch
- A closed disc of radius $r\ge0$ has Jordan content $\pi r^2$
- Measure zero and content zero in $\mathbb{R}^m$ by countable and finite cube covers
- The graph of a continuous function on a closed nondegenerate rectangle in $\mathbb{R}^m$ has content zero in $\mathbb{R}^{m+1}$
Used by
Dependency tree · two levels
70 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, section 6.8 (standard reference, not scraped)
- J. Feldman, A. Rechnitzer and E. Yeager, CLP-4 Vector Calculus, chapter 4 (standard reference, not scraped)