Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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 solid generated by rotating y=sin⁡x on [0,π] has volume π2/2

Example

Rotate the region

{(x,y):0≤x≤π, 0≤y≤sin⁡x}

about the x-axis. The resulting solid is compact and Jordan measurable, and its volume is

V=π22.

The vanishing endpoint radii are included in the solid and require no separate measurability argument.

Facts & Assumptions

Given: The profile f(x)=sin⁡x on [0,π] and its solid of revolution about the x-axis.

[F1]

If a≤b and f:[a,b]→[0,∞) is continuous, then its solid of revolution about the x-axis is compact and Jordan measurable and has volume π∫abf(x)2 dx (The disc formula for the volume of a solid of revolution).

[L1]

sin⁡π=0, and sin⁡x>0 for every x with 0<x<π; thus π is the first positive zero of sine, in particular π>0 (Pi is the first positive zero of sine).

[L2]

The functions sin⁡ and cos⁡ are differentiable on R, with (sin⁡x)′=cos⁡x and (cos⁡x)′=−sin⁡x; also sin⁡0=0 and cos⁡0=1 (The derivatives of sine and cosine are cosine and minus sine).

[L3]

For a real-valued function on A⊆R, differentiability at a limit point c∈A implies continuity there (A function differentiable at c is continuous at c).

[L4]

For every real x, sin⁡2x=(1−cos⁡2x)/2 (Double-angle and quadratic power-reduction identities).

[L5]

Every continuous real-valued function on a nondegenerate closed interval is Riemann integrable there (A continuous function on [a,b] is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[L8]

If a<b, G:[a,b]→R is differentiable at every point of [a,b], and G′ is integrable, then ∫abG′=G(b)−G(a) (The second fundamental theorem: if G is differentiable on [a,b] with G′=f and f is integrable, then ∫abf=G(b)−G(a)).

Verification

technique · direct
1.1F1L1L2L3

Facts [L1], [L2], and [L3] show that f is continuous and nonnegative on [0,π], so [F1] makes the rotated solid compact and Jordan measurable and gives V=π∫0πsin⁡2x dx.

1.2L1L2L3L5L9L10

Since π>0 by [L1], the interval [0,π] is nondegenerate. The function G(x)=12sin⁡(2x) is differentiable with G′(x)=cos⁡(2x), and this derivative is continuous and therefore integrable on [0,π].

1.3L1L7algebra

On the same nondegenerate interval, the constant function 1 is integrable and has integral π.

2.1step 1.2step 1.3L2L4L6L8L11algebra

By power reduction and linearity, followed by the fundamental theorem applied to step 1.2, ∫0πsin⁡2x dx=12∫0π1 dx−12∫0πcos⁡(2x) dx=π/2−12(G(π)−G(0))=π/2, because periodicity and [L2] give G(π)=G(0)=0.

3.1step 1.1step 2.1algebra∎

Substituting step 2.1 into the disc formula of step 1.1 gives V=π(π/2)=π2/2.

Remarks

The profile radius vanishes at both endpoints, but [F1] permits nonnegative continuous profiles and explicitly includes zero-radius sections. No division by the profile occurs.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

71 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