TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-24

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 disc formula for the volume of a solid of revolution

Statement

Let $a \leq b$ and let $f : [a, b] \to [0, \infty)$ be continuous, and form $S_{x} (f)$ as in Solids of revolution about a coordinate axis. The solid of revolution is compact and Jordan measurable and has volume $π \int_{a}^{b} f (x)^{2} d x$ .

Facts & Assumptions

Given: The interval $[a, b]$ , the continuous nonnegative profile $f$ , and the solid $S_{x} (f)$ .

[F1]

A solid between continuous graphs over a compact Jordan base is compact and Jordan measurable (A solid between continuous graphs over a compact Jordan base is Jordan measurable and integrates by vertical sections).

[F2]

A closed disc of radius $r \geq 0$ has Jordan content $π r^{2}$ (A closed disc of radius $r \geq 0$ has Jordan content $π r^{2}$ ).

[F3]

If a bounded Jordan set has Jordan-measurable sections outside a content-zero parameter set, then its completed sectional-content function is integrable and its integral is the set's content (Cavalieri: Jordan content is the integral of sectional contents, and equal sections give equal content).

[F4]

Finite sums and products of continuous real-valued maps on a topological space are continuous (Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined).

[F5]

The inverse of a continuous injective real function on an interval is continuous on its image (Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f [I]$ , and the inverse $g : f [I] \to I$ is continuous and strictly monotone in the same sense as $f$ ).

[F6]

Every nonnegative real has a unique nonnegative square root (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ).

Proof

technique · direct

1.1

First apply [F1] over the compact interval $[a, b]$ to the graphs $- f$ and $f$ , obtaining the compact Jordan base $D = {(x, y) : a \leq x \leq b, ∣ y ∣ \leq f (x)}$ . By [F4], $(x, y) \mapsto f (x)^{2} - y^{2}$ is continuous and nonnegative on $D$ ; [F5] and [F6] make its nonnegative square root $ρ$ continuous. A second application of [F1] to the graphs $- ρ$ and $ρ$ identifies their solid with $S_{x} (f)$ , so $S_{x} (f)$ is compact and Jordan measurable.

givenF1F4F5F6construct

2.1

For each $x \in [a, b]$ , the section of $S_{x} (f)$ perpendicular to the $x$ -axis is the closed disc $y^{2} + z^{2} \leq f (x)^{2}$ , and [F2] gives it content $π f (x)^{2}$ , including when $f (x) = 0$ .

step 1.1F2

3.1

The sectional-content function $x \mapsto π f (x)^{2}$ is continuous, so [F3] gives $cont (S_{x} (f)) = \int_{a}^{b} π f (x)^{2} d x$ . If $a = b$ or $f$ is identically zero, the same formula gives zero.

step 2.1F3∎

Remarks

The corresponding formula about the $y$ -axis is obtained by permuting coordinates when the sections perpendicular to that axis are discs.

Depends on

Used by

Dependency tree · two levels

51 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.4 (standard reference, not scraped)