Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck 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.

Closed Euclidean balls are Jordan measurable and their volumes satisfy the slicing recursion

Statement

For every integer n≥1 and every r≥0, put B‾n(0,r):={x∈Rn:∥x∥2≤r}, extending the positive-radius notation of Euclidean spheres and closed balls as subspaces of Rn to r=0. This closed Euclidean ball is Jordan measurable; write its content as Vn(r). One has V1(r)=2r. For n≥2 and r≥0, Vn(r)=Vn−1(1)∫−rr(r2−t2)(n−1)/2 dt.

Facts & Assumptions

Given: Positive integer dimension n, radius r≥0, and the closed Euclidean balls defined in the Statement.

[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]

If a linear map T has matrix A and E is a bounded Jordan set, then cont⁡(T(E))=∣det⁡A∣cont⁡(E) (A linear endomorphism of Rn sends bounded Jordan sets to bounded Jordan sets and scales their content by the absolute determinant).

[F3]

If a bounded Jordan set has Jordan-measurable sections outside a content-zero parameter set, then its completed sectional-content function, with empty sections assigned content 0, 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).

[F6]

Every nonnegative real has a unique nonnegative square root (Existence and uniqueness of n-th roots: a unique a1/n≥0 with (a1/n)n=a).

[F8]

The Euclidean distance is d2(u,v)=∥u−v∥2 and satisfies the metric triangle inequality (Rn as the set of functions n→R, and d1, d2, d∞ are metrics on it).

Proof

technique · induction
1.1givenF7base

For n=1, the ball is the closed bounded interval [−r,r], hence compact by [F7], and it is Jordan measurable with content 2r, including r=0.

2.1step 1.1ihF1F4F5F6F8algebra

Assume closed balls in dimension n−1 are compact and Jordan measurable. The triangle inequality in [F8], applied in both orders, gives ∣∥u∥2−∥v∥2∣≤∥u−v∥2, so the Euclidean norm is continuous. On [0,r], the estimate ∣(r2−s2)−(r2−t2)∣=∣s−t∣∣s+t∣≤2r∣s−t∣ makes s↦r2−s2 continuous; [F5] and [F6] make its nonnegative square root continuous, and [F4] makes the resulting composite continuous on the ball. Thus the n-ball is the solid between two continuous square-root graphs over B‾n−1(0,r), and [F1] makes it compact and Jordan measurable.

3.1step 2.1F2algebra

For ∣t∣≤r, the section at last coordinate t is the (n−1)-ball of radius ρ(t):=r2−t2. It is the image of the unit (n−1)-ball under scalar multiplication by ρ(t), whose determinant has absolute value ρ(t)n−1; [F2] gives section content Vn−1(1)(r2−t2)(n−1)/2. At t=±r this is zero.

4.1step 3.1F3discharge-induction∎

By [F3], integration of the section contents in step 3.1 gives the displayed recursion. Thus the induction proves Jordan measurability in every positive dimension and the recursion for every n≥2.

Depends on

Used by

Dependency tree · two levels

95 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