Alphabeta Math
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.

The closed ball is an elementary solid region, presented by the eight spherical octants

Example

Fix R>0 and let BR:={(x,y,z)R3:x2+y2+z2R2}. Let φ(ϕ,θ)=R(sinϕcosθ,sinϕsinθ,cosϕ) on [0,π]×[0,2π], and cut the parameter rectangle at ϕ=π/2 and at θ=π/2,π,3π/2. The eight restrictions of φ to the resulting closed rectangles form one outward finite patch presentation of BR adapted in all three coordinate directions, so BR is an elementary solid region.

Facts & Assumptions

Given: A real radius R>0; the spherical parametrization φ(ϕ,θ)=R(sinϕcosθ,sinϕsinθ,cosϕ); the intervals I+=[0,π/2], I=[π/2,π], and J0=[0,π/2], J1=[π/2,π], J2=[π,3π/2], J3=[3π/2,2π]; and the eight restricted patches φ±,j:=φI±×Jj.

[F1]

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

[F2]

A simple description in the direction k has the form E={pR3:πk(p)D, γ1(πk(p))pkγ2(πk(p))} (Simple solid regions in a coordinate direction and their cyclic coordinate projection).

[F3]

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

[F4]

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

[F5]

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

[F6]

The cross product in R3 is u×v=(uyvzuzvy, uzvxuxvz, uxvyuyvx) (The cross product in R3).

[L1]

For a C1 patch ψ of two variables, (ψu×ψv)k=detD(πkψ) in each coordinate direction (Each coordinate of the oriented area vector is the Jacobian determinant of the matching cyclic projection).

[L2]

(sint)=cost and (cost)=sint (The derivatives of sine and cosine are cosine and minus sine).

[L3]
[L4]

Sine is positive on (0,π) and negative on (π,2π); cosine is positive on (0,π/2)(3π/2,2π), negative on (π/2,3π/2), and strictly decreasing on [0,π]; and both functions take values in [1,1] (Signs, monotonicity intervals, and ranges of sine and cosine, Quarter-turn values and shifts by pi/2 and pi).

[L5]

sin(π/2)=1, cos(π/2)=0, sinπ=0, and cosπ=1 (Quarter-turn values and shifts by pi/2 and pi).

[F7]

Integration over a Jordan set is that of its zero extension (The Riemann integral of a bounded function over a bounded Jordan measurable set).

[L6]

A bounded set is Jordan measurable exactly when its boundary has content zero (A bounded set in Rm is Jordan measurable iff its boundary is null, equivalently of content zero).

[F8]

Choosing Nφ rather than Nφ is an orientation (Unit normal fields, orientations, and flux through a regular surface patch).

[L7]

A closed disc of radius r0 has Jordan content πr2 (A closed disc of radius r0 has Jordan content πr2).

[F9]

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 Rm by countable and finite cube covers).

[L8]

A continuous graph over a compact nondegenerate rectangle has content zero (The graph of a continuous function on a closed nondegenerate rectangle in Rm has content zero in Rm+1).

[L9]

The map θ(cosθ,sinθ) is injective on [0,2π) (t(cost,sint) is a bijection from [0,2π) onto the real unit circle).

Verification

technique · direct
1.1

The eight parameter rectangles are I±×Jj, obtained by cutting the spherical parameter rectangle at the quarter turns named in [L5].

givenL5
2.1

Differentiating gives φϕ=R(cosϕcosθ,cosϕsinθ,sinϕ) and φθ=R(sinϕsinθ,sinϕcosθ,0), and [F6], [L2], and [L3] give φϕ×φθ=Rsinϕφ(ϕ,θ).

step 1.1F6L2L3
3.1

On the interior of each rectangle one has sinϕ>0 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 cosϕ; strict monotonicity of cosine on (0,π) 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].

step 1.1step 2.1F4F5F7L4L6L9
3.2

In the z direction the base is the closed disc Dz={(x,y):x2+y2R2} and the two boundary functions are γ1z(x,y)=R2x2y2 and γ2z(x,y)=R2x2y2, so [F2] describes BR; the third coordinate of the oriented area vector is R2sinϕcosϕ, so by [L4] the four patches with ϕ(0,π/2) form the upper sublist and the four with ϕ(π/2,π) form the lower sublist, with no lateral patch because the vanishing set sinϕ=0 or cosϕ=0 lies on parameter boundaries.

step 2.1F2F3L1L4
3.3

In the x direction the base is the closed disc Dx={(y,z):y2+z2R2} and the boundary functions are γ1x(y,z)=R2y2z2 and γ2x(y,z)=R2y2z2, so [F2] again describes BR. The first coordinate of the oriented area vector is R2sin2ϕcosθ, so by [L4] the four octants with θ(0,π/2)(3π/2,2π) form the upper sublist and the other four the lower sublist; the vanishing set sinϕ=0 or cosθ=0 lies on parameter boundaries, so there is no lateral patch.

step 2.1F2F3L1L4L5
3.4

In the y direction the base is the closed disc Dy={(z,x):z2+x2R2} and the boundary functions are γ1y(z,x)=R2z2x2 and γ2y(z,x)=R2z2x2, so [F2] describes BR a third time. The second coordinate of the oriented area vector is R2sin2ϕsinθ, so the split is by θ(0,π) against θ(π,2π); again the vanishing set lies on parameter boundaries, so there is no lateral patch.

step 2.1F2F3L1L4L5
4.1

The projections of the interiors of the four upper octants onto the xy 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 Dz. 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 z direction.

step 3.2F3F9L6L7L8
5.1

In the x direction the projections onto the yz plane of the four upper octants are the four open quarter discs of Dx, pairwise disjoint: J0 gives the half with y>0 and J3 the half with y<0, and in each half the two choices ϕ(0,π/2) and ϕ(π/2,π) split by the sign of z. The four lower octants have the same projected images, now coming from J1 and J2. In each case the omitted set is the union of the two coordinate diameters and the boundary circle of Dx, which has content zero by the same argument as in step 4.1. Thus both graph sublists satisfy the coverage clause in the x direction.

step 3.3F3F9L6L7L8
5.2

In the y direction the projections onto the zx plane of the four upper octants are the four open quarter discs of Dy, pairwise disjoint: θ(0,π) gives the half with x>0 or x<0 according to whether θ(0,π/2) or (π/2,π), and the two halves are split again by the sign of z. 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 Dy, hence has content zero by the same argument as in step 4.1. So both graph sublists satisfy the coverage clause in the y direction.

step 3.4F3F9L6L7L8
6.1

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 BR with this presentation an elementary solid region.

step 3.1step 3.2step 4.1step 3.3step 5.1step 3.4step 5.2F1F8step 2.1

Remarks

  • The cuts at both ϕ=π/2 and the four azimuth quadrants are load-bearing. Without the azimuth cuts, the x and y 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

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