Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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 surface generated by rotating y=sinx on [0,π] has area 2π(2+arsinh1)

Example

Rotate the graph y=sinx, 0xπ, about the x-axis. The resulting surface has area

A=2π(2+arsinh1)=2π(2+log(1+2)).

The profile is positive in the parameter interior and vanishes only at its endpoints, where the generating curve meets the axis of revolution.

Facts & Assumptions

Given: The radius function r(x)=sinx on [0,π] and the surface obtained by rotating its graph about the x-axis.

[F1]

Under the hypotheses of the scalar surface-integral theorem for a surface of revolution, the rotated surface has area 2πabr(s)1+r(s)2ds (The surface of revolution has area 2πabr(s)1+r(s)2ds).

[F2]

Those hypotheses require a<b and r:[a,b][0,) to be C1 on a neighbourhood of [a,b], positive on (a,b), and allowed to vanish only at the endpoints (Scalar surface integrals on a surface of revolution).

[L1]

sinπ=0, and sinx>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 (sinx)=cosx and (cosx)=sinx; also sin0=0 and cos0=1 (The derivatives of sine and cosine are cosine and minus sine).

[L3]

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

[L4]

The function sinh:RR is odd, strictly increasing, and onto; cosh is positive; cosh2vsinh2v=1; and (sinhv)=coshv (Addition formulas, identities, parity, and derivatives of the hyperbolic functions).

[L5]

Let IR be order-convex with at least two elements, let f:IR be continuous and injective, and let g:f[I]I be its inverse. If f is differentiable at cI with f(c)0, then g is differentiable at f(c) and g(f(c))=1/f(c) (Derivative of an inverse: if f is continuous and injective on a nondegenerate interval I and differentiable at cI with f(c)0, then the inverse g is differentiable at f(c) with g(f(c))=1/f(c); and if f(c)=0 then g is not differentiable at f(c)).

[L6]

For every real u, arsinhu=log(u+u2+1) (Logarithm formulas for inverse sinh, inverse cosh, and inverse tanh on their natural domains).

[L7]

For every real α, uuα is continuous and differentiable on (0,), with derivative αuα1 (Continuity and derivatives of positive-base real powers).

[L8]

If a>0 and qQ, then the real power aq agrees with the rational power; in particular this holds for q=1/2 (The exponential definition of real powers agrees with the existing rational powers).

[L9]

Every nonnegative real a has a unique nonnegative square root a (Square roots exist: a unique a0 with (a)2=a; the positives are {x2:x0}).

[L12]

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

[L13]

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

[L14]

cos0=1 and cosπ=1 (Quarter-turn values and shifts by pi/2 and pi).

Verification

technique · direct
1.1

Facts [L1], [L2], and [L3] verify the hypotheses in [F2], so [F1] gives A=2π0πsinx1+cos2xdx.

F1F2L1L2L3
1.2

Let uR and v=arsinhu. Facts [L3], [L4], and [L5] give (arsinhu)=1/coshv=1/1+u2, where positivity of coshv and uniqueness in [L9] select the nonnegative square root. Since sinh is an odd bijection, its inverse is odd, so arsinh(u)=arsinhu.

L3L4L5L9algebra
1.3

Since π>0 by [L1], the interval [0,π] is nondegenerate. The function xsinx1+cos2x is continuous on this interval and hence integrable there.

L1L2L3L7L8L9L12algebra
2.1

Define G(x)=12(arsinh(cosx)+cosx1+cos2x). Using step 1.2, the derivative of the positive square root, and the chain and product rules gives G(x)=sinx1+cos2x.

step 1.2L2L7L8L9L10L11algebra
3.1

By the fundamental theorem, step 1.3, and step 2.1, the integral in step 1.1 is G(π)G(0)=2+arsinh1: fact [L14] gives the cosine endpoint values, and the oddness in step 1.2 changes arsinh(1) to arsinh1. Fact [L6] also gives arsinh1=log(1+2).

step 1.2step 1.3step 2.1L6L9L13L14algebra
4.1

Substituting step 3.1 into the area formula of step 1.1 gives A=2π(2+arsinh1)=2π(2+log(1+2)).

step 1.1step 3.1algebra

Remarks

The endpoint zeros satisfy the source theorem's boundary allowance. The integrand stays continuous there, since its square-root factor is at least 1, so no improper-integral convention enters the calculation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

80 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