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 unit box, with its six faces, is an elementary solid region
Example
Let and let with parameters . Then the six faces of the closed unit box, each parametrized on the unit square so that its oriented area vector points out of the box, form one presentation adapted in all three coordinate directions, so is an elementary solid region (Elementary solid regions: one boundary presentation adapted in all three coordinate directions) with that presentation. The six parametrizations are
all on , and their oriented area vectors are the constants , , , , and respectively.
Facts & Assumptions
Given: The box , the square , and the six parametrizations displayed above.
For and in , (The cross product in ), and has th coordinate and the others (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension , The Euclidean inner product on ).
A regular parametrized surface patch has a compact Jordan parameter region that is the closure of its nonempty connected interior, a parametrization on an open neighbourhood of it, nonvanishing parameter cross product on the interior, and no interior parameter point sharing its image with a distinct point of the region (Regular parametrized surface patches on compact Jordan parameter regions).
A compatible finite patch presentation is a finite list of regular patches whose images cover a set, such that for two distinct patches the preimage of their overlap has content zero in each parameter region, and whose induced normals agree at every point of the overlap that is the image of an interior parameter point of both (Finitely patched regular surfaces, their area, scalar integrals, and flux).
A simple description of a solid in the direction is with compact Jordan of nonempty interior and continuous on , strict on its interior, describing ; the cyclic projections are , and (Simple solid regions in a coordinate direction and their cyclic coordinate projection).
Given a compatible finite patch presentation whose images cover and lie in the boundary, it is adapted to a description in the direction when its index set splits into an upper, a lower and a lateral sublist, with the image of an upper patch in the graph of and the th coordinate of its oriented area vector positive on the parameter interior, the mirror conditions for a lower patch, that coordinate vanishing on the parameter interior for a lateral patch, the projected images of each graph sublist pairwise disjoint and filling up to content zero, and both graph sublists nonempty (Boundary presentations adapted to a simple solid region in a coordinate direction).
An elementary solid region is a compact set with a simple description in each of the three coordinate directions and one compatible finite patch presentation of its boundary adapted to a simple description in each of them (Elementary solid regions: one boundary presentation adapted in all three coordinate directions).
The oriented area vector of a patch is and the flux integrand is taken against it (Unit normal fields, orientations, and flux through a regular surface patch); integration over a bounded Jordan set is that of The Riemann integral of a bounded function over a bounded Jordan measurable set; boundaries and interiors are those of Interior, closure, boundary, limit point, isolated point and dense subset of a metric space.
A set has content zero when it admits finite cube covers of arbitrarily small total volume, and content zero passes to subsets (Measure zero and content zero in by countable and finite cube covers); 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).
For a map of two variables into , (Each coordinate of the oriented area vector is the Jacobian determinant of the matching cyclic projection).
Verification
Each of the six maps is affine, so its two parameter derivatives are the constant standard basis vectors , ; , ; , ; , ; , ; , . Computing each cross product from [F1] gives , , , , and , so the six oriented area vectors are the constants as displayed.
The three quadruples , and , with constant graph functions, are simple descriptions of in the three directions in the sense of [F4]: the base is compact, Jordan measurable and has nonempty interior; the constants satisfy the weak and the strict inequality; and in each case is exactly , because lists the two coordinates other than the th.
Each of the six pairs is a regular patch in the sense of [F2]: the square is compact and Jordan measurable, being a rectangle, and is the closure of its nonempty convex, hence connected, interior ; each is affine and therefore on all of ; each oriented area vector is a nonzero constant by step 1.1; and each is injective on , since its two direction vectors are distinct standard basis vectors and reading the two matching coordinates of the image recovers , so in particular no interior parameter point shares its image with a distinct point of .
Take , and . The image of is the face , the graph of , and by step 1.1 the coordinate of its oriented area vector is ; the image of is the graph of with coordinate ; and the four lateral vectors have coordinate , so that coordinate vanishes on the whole parameter square. The projected image is , whose complement in is of content zero by [F8], and likewise for , where ; each graph sublist is a single patch, so pairwise disjointness is vacuous, and both are nonempty. So the presentation is adapted to the description of step 1.2, in the sense of [F5].
Take , and . By step 1.1 the coordinates of the oriented area vectors are for , for and for the other four. The image of is the face and , so its projected image is ; the image of is and , again with projected image . Both complements in the base are , of content zero. So the same presentation is adapted to the description.
Take , and . By step 1.1 the coordinates of the oriented area vectors are for , for and for the other four. The image of is the face and , so its projected image is ; the image of is and , with projected image . So the same presentation is adapted to the description.
The six images are the six closed faces of , each contained in , and their union is by [F7], since a point of fails to be interior exactly when one of its coordinates is or . Two distinct faces meet in a closed edge, a vertex or the empty set; the preimage of such an intersection in either parameter square is contained in , which has content zero by [F8], so the overlap condition of [F3] holds. Interior parameter points map into the six open faces, which are pairwise disjoint, so no point of an overlap is the image of an interior parameter point of two distinct patches and the normal-agreement condition of [F3] holds with nothing to check. Hence the six patches form a compatible finite patch presentation of .
Steps 2.1 and 3.1 make the six patches a compatible finite patch presentation of , step 1.2 supplies the three simple descriptions, and steps 2.2, 2.3 and 2.4 make that one presentation adapted in all three directions. By [F6] the box , with these data, is an elementary solid region.
Remarks
-
The parameter order on each face is chosen, and the choice is what fixes the sign. Exchanging and on any one face reverses its oriented area vector and would make that face fail the adaptation condition in the direction where it is a graph face. The six orders above are the ones for which the oriented area vector is the outward standard basis vector, which is also what makes the presentation the outward one in the sense of Every patch of an elementary solid region's presentation is a graph face in some direction, and at interior base points its normal is outward.
-
Each face is lateral in two directions and a graph face in one. That is visible in step 1.1: the oriented area vector of each face is one standard basis vector, so exactly one of its three coordinates is nonzero. It is the concrete case of the general fact that no patch can be lateral in all three directions.
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 Riemann integral of a bounded function over a bounded Jordan measurable set
- Unit normal fields, orientations, and flux through a regular surface patch
- The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$; hence $\dim_F F^{n} = n$, and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- Measure zero and content zero in $\mathbb{R}^m$ by countable and finite cube covers
- A bounded set in $\mathbb{R}^m$ is Jordan measurable iff its boundary is null, equivalently of content zero
- Interior, closure, boundary, limit point, isolated point and dense subset of a metric space
Used by
Dependency tree · two levels
69 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)