Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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 volume of a closed ball recovered from the outward flux of the position field

Example

Let X(x,y,z)=(x,y,z) be the position field on R3, and let BR be the closed ball of radius R>0 with the octant presentation of The closed ball is an elementary solid region, presented by the eight spherical octants. Then the outward flux of X through BR is 4πR3, so The volume of a glued elementary solid is a third of the outward flux of the position field gives cont(BR)=13BRX,n=43πR3.

Facts & Assumptions

Given: A radius R>0, the ball BR, the spherical octant presentation of The closed ball is an elementary solid region, presented by the eight spherical octants, one of its octant parametrizations φ(ϕ,θ)=R(sinϕcosθ,sinϕsinθ,cosϕ), and the position field X(x,y,z)=(x,y,z).

[L1]

For the spherical parametrization φ(ϕ,θ)=R(sinϕcosθ,sinϕsinθ,cosϕ), one has φϕ×φθ=Rsinϕφ(ϕ,θ) (The cross product in R3, The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine).

[L2]

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

[L3]

For an elementary solid region E and a C1 field F, EdivF=EF,n (The divergence theorem on an elementary solid region).

[F1]

The divergence of a field is the sum of its coordinate partial derivatives (Divergence and curl of a C1 vector field).

[L4]

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

[L5]

If a<b, G is differentiable on [a,b], and G=f is integrable there, then abf=G(b)G(a) (The second fundamental theorem: if G is differentiable on [a,b] with G=f and f is integrable, then abf=G(b)G(a)).

[L6]

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

[L7]
[F2]

The flux in the orientation induced by a patch φ is D(Fφ)(φu×φv) (Unit normal fields, orientations, and flux through a regular surface patch).

[F3]

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

[L8]

The closed three-dimensional ball of radius r has volume 4πr3/3 (A closed three-dimensional ball of radius r0 has volume 4πr3/3).

[F4]

Verification

technique · direct
1.1

On each spherical octant patch, [L1], [F2], [F4], and [L7] give X(φ(ϕ,θ)),φϕ×φθ=φ(ϕ,θ),Rsinϕφ(ϕ,θ)=R3sinϕ.

L1F2F4L7given
2.1

On each of the four upper octant patches, step 1.1 gives the flux integrand R3sinϕ on a parameter rectangle [0,π/2]×[α,α+π/2]; for fixed ϕ the θ-section is constant, and for fixed θ the ϕ-section is R3sinϕ, so [L4], [L5], and [L6] give the flux value R3αα+π/20π/2sinϕdϕdθ=R3(π/2). On each of the four lower octant patches the same argument gives R3αα+π/2π/2πsinϕdϕdθ=R3(π/2). Summing the eight patch fluxes by [F3] yields the total outward flux 8R3(π/2)=4πR3.

step 1.1L4L5L6F3
3.1

The field X has divergence 3 by [F1], so [L3] and [L2] both identify the content of BR with one third of the flux computed in step 2.1, namely (4/3)πR3.

step 2.1L2L3F1
4.1

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.

step 3.1L8F2

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

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