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 right circular cone of radius and height has volume
Statement
A right circular cone of radius and height has volume .
Facts & Assumptions
Given: Nonnegative reals and a right circular cone.
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 or , the cone is degenerate and both sides are zero. Otherwise apply [F1] to on .
The function has derivative , so [F2] evaluates the volume as .
The positive-height computation and the zero-parameter case together prove the formula for all .
Depends on
- The disc formula for the volume of a solid of revolution
- 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
Dependency tree · two levels
31 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)