Alphabeta MathHow 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.
A closed three-dimensional ball of radius has volume
Statement
For , put , extending the positive-radius notation of Euclidean spheres and closed balls as subspaces of to . This closed three-dimensional ball has volume .
Facts & Assumptions
Given: A radius and the closed ball defined in the Statement.
A solid of revolution with profile has volume (The disc formula for the volume of a solid of revolution).
If an integrable function is a derivative on , then its integral is (The second fundamental theorem: if is differentiable on with and is integrable, then ).
Proof
If , the ball is the singleton , which is covered by a cube of arbitrarily small volume; its content and the displayed formula are both zero.
Suppose . The ball is the solid of revolution of on , so [F1] gives .
A primitive is ; by [F2], .
Steps 1.1 and 2.1 cover respectively and , so the formula holds for every .
Remarks
The independent Cavalieri comparison is The volume of a three-ball by Cavalieri's cylinder-minus-cones proof.
Depends on
- The disc formula for the volume of a solid of revolution
- Euclidean spheres and closed balls as subspaces of $\mathbb{R}^n$
- Jordan inner and outer content and Jordan measurable bounded sets in $\mathbb{R}^m$
- For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term
- The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G' = f$ and $f$ is integrable, then $\int_a^b f = G(b)-G(a)$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
44 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
- Sigurd Angenent, Math 221 lecture notes, Chapter 8 §3 (standard reference, not scraped)