TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 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 volume of a three-ball by Cavalieri's cylinder-minus-cones proof

Statement

For $r \geq 0$ , put ${\overline{B}}_{3} (0, r) : = {x \in R^{3} : ∥ x ∥_{2} \leq r}$ , extending the positive-radius notation of Euclidean spheres and closed balls as subspaces of $R^{n}$ to $r = 0$ . This closed three-dimensional ball has volume $4 π r^{3} / 3$ .

Facts & Assumptions

Given: A radius $r \geq 0$ , the ball $B : = {\overline{B}}_{3} (0, r)$ of the Statement, a radius- $r$ cylinder of height $2 r$ , and inside it the two radius- $r$ , height- $r$ cones with common vertex at the centre and bases at the top and bottom faces.

[F1]

If two bounded Jordan sets have Jordan sections outside content-zero exceptional parameter sets and their ordinary sectional contents agree away from those sets, then the two sets have equal content (Cavalieri: Jordan content is the integral of sectional contents, and equal sections give equal content).

[F2]

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

[F3]

A right circular cylinder of radius $R \geq 0$ and height $h \geq 0$ has volume $π R^{2} h$ (A right circular cylinder of radius $R$ and height $h$ has volume $π R^{2} h$ ).

[F4]

A right circular cone of radius $R \geq 0$ and height $h \geq 0$ has volume $π R^{2} h / 3$ (A right circular cone of radius $R$ and height $h$ has volume $π R^{2} h / 3$ ).

[F5]

Jordan content is additive on disjoint finite families, and more generally across content-zero overlaps (Jordan content is finitely additive when the overlap has content zero).

[F6]

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).

[F7]

A Euclidean set is compact if and only if it is closed and bounded (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[F8]

A composite of continuous maps is continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).

[F9]

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$ ).

[F10]

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$ ).

[F11]

The Euclidean distance is $d_{2} (u, v) = ∥ u - v ∥_{2}$ and satisfies the metric triangle inequality ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it).

[F12]

A bounded set is Jordan measurable if and only if its boundary has content zero (A bounded set in $R^{m}$ is Jordan measurable iff its boundary is null, equivalently of content zero).

Proof

technique · direct

1.1

Let $D \subseteq R^{2}$ be the closed disc of radius $r$ . It is Jordan measurable by [F2], and it is closed and bounded, hence compact by [F7]. The triangle inequality in [F11], applied in both orders, gives $∣ ∥ u ∥_{2} - ∥ v ∥_{2} ∣ \leq ∥ u - v ∥_{2}$ , so the norm is continuous. On $[0, r]$ , the estimate $∣ (r^{2} - s^{2}) - (r^{2} - t^{2}) ∣ = ∣ s - t ∣ ∣ s + t ∣ \leq 2 r ∣ s - t ∣$ makes $s \mapsto r^{2} - s^{2}$ continuous; [F9] and [F10] make the nonnegative square root continuous, and [F8] then makes $ρ (u) : = \sqrt{r^{2} - ∥ u ∥_{2}^{2}}$ continuous on $D$ . Thus [F6] identifies $B$ with the compact Jordan solid between $- ρ$ and $ρ$ . Fact [F6] likewise makes the cylinder between the constant graphs $- r, r$ , the upper and lower cones between $∥ u ∥_{2}, r$ and $- r, - ∥ u ∥_{2}$ , and the comparison solid $C$ between $- ∥ u ∥_{2}, ∥ u ∥_{2}$ compact Jordan sets.

givenF2F6F7F8F9F10F11constructalgebra

2.1

At height $z \in [- r, r]$ , [F2] gives the ball section area $π (r^{2} - z^{2})$ . The comparison section is the radius- $r$ disc with the open radius- $∣ z ∣$ disc removed. It is bounded and its boundary lies in the two disc boundary circles, so [F12] makes it Jordan measurable; its overlap with the closed inner disc is the inner boundary circle and has content zero. Facts [F2] and [F5] therefore give the same area $π (r^{2} - z^{2})$ . At $z = \pm r$ both areas are zero.

step 1.1F2F5F12algebra

2.2

The cylinder is the union of $C$ and the two cones from step 1.1. Their pairwise overlaps lie in boundaries, which have content zero by [F12], so [F5], [F3], and [F4] give $cont (C) = 2 π r^{3} - 2 (π r^{3} / 3) = 4 π r^{3} / 3$ .

step 1.1F3F4F5F12algebra

3.1

The bounded Jordan sets $B$ and $C$ have the equal Jordan sections of step 2.1, so [F1] gives $cont (B) = cont (C) = 4 π r^{3} / 3$ . The construction and calculation include $r = 0$ .

step 1.1step 2.1step 2.2F1∎

Remarks

This proof compares sections with a cylinder minus cones. The disc-integration proof A closed three-dimensional ball of radius $r \geq 0$ has volume $4 π r^{3} / 3$ follows a different route and is not a dependency of this theorem.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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