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 radius- closed -ball is
Statement
For and , , where is an integer.
Facts & Assumptions
Given: Positive integer and radius .
One has for , and for and , (Closed Euclidean balls are Jordan measurable and their volumes satisfy the slicing recursion).
For every , (The closed form for the volume of the unit -ball).
Proof
If , the ball is a singleton of content zero, and the right side is zero because .
Suppose . For , . For , substitute in [F1]; the power and differential contribute and , so comparison with [F1] at radius gives .
Insert [F2] into step 1.2 and combine it with the zero-radius case of step 1.1. This gives the displayed formula for every allowed .
Depends on
- Closed Euclidean balls are Jordan measurable and their volumes satisfy the slicing recursion
- The closed form for the volume of the unit $n$-ball
- Substitution: if $\varphi$ is differentiable on $[c,d]$ with $\varphi'$ integrable and $f$ is continuous on an interval containing $\varphi([c,d])$, then $\int_{\varphi(c)}^{\varphi(d)} f = \int_c^d (f\circ\varphi)\,\varphi'$
- The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents
- Jordan inner and outer content and Jordan measurable bounded sets in $\mathbb{R}^m$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
50 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
- University of Toronto MAT237Y1, The Gamma Function and the Beta Function, §2.4(a,e) (standard reference, not scraped)