Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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)=13∬∂BR⟨X,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, ∭Ediv⁡F=∬∂E⟨F,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]

(sin⁡t)′=cos⁡t and (cos⁡t)′=−sin⁡t (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 r≥0 has volume 4πr3/3).

[F4]

Verification

technique · direct
1.1L1F2F4L7given

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

2.1step 1.1L4L5L6F3

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∫αα+π/2∫0π/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 8⋅R3(π/2)=4πR3.

3.1step 2.1L2L3F1

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.

4.1step 3.1L8F2∎

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

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