Alphabeta Math
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.

✓ 9 results · all verified · 9 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 9 also cleared it.

Trigonometric and Oscillatory Examples in Several Variables: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The circular curve defeats the equality form of the vector-valued mean value theorem

Statement refuted

Refuted claim: if m∈N with m≥1, if a<b are real, and if f:[a,b]→Rm is continuous on [a,b] and differentiable on (a,b), then there is some ξ∈(a,b) such that

f(b)−f(a)=(b−a)f′(ξ).

The claim is false already for m=2. The curve

f:[0,2π]⟶R2,f(t)=(cos⁡t,sin⁡t),

is continuous on its interval and differentiable in its interior, its endpoint increment is zero, and ∥f′(t)∥2=1 for every t∈(0,2π). Hence no ξ∈(0,2π) satisfies the displayed equality.

Facts & Assumptions

Given: The curve f(t)=(cos⁡t,sin⁡t) on [0,2π].

[L1]

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

[L2]

Let m∈N with m≥1, let A⊆R, and let c∈A be a limit point of A. A map g:A→Rm is differentiable at c if and only if every component is differentiable there, and its derivative then has the component derivatives as coordinates (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L3]

Let m∈N with m≥1, let A be a subspace of a metric space, and let g:A→Rm. The map g is continuous at a point of A if and only if every component is continuous there (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).

[L4]

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

[L5]

For every real t, sin⁡2t+cos⁡2t=1 (Parity and the Pythagorean identity for sine and cosine).

[L7]
[L8]

Counterexample

technique · direct
1.1L1L3L4

By [L1] and [L4], both components of f are continuous on [0,2π], so f is continuous there by [L3].

1.2L1L6algebra

Periodicity and the values at zero give f(2π)=f(0)=(1,0), so f(2π)−f(0)=(0,0).

1.3L1L2

Componentwise differentiation gives f′(t)=(−sin⁡t,cos⁡t) for every t∈(0,2π).

1.4L8algebra

Since π>0, the scalar 2π is nonzero.

2.1step 1.3L5L7algebra

For every t∈(0,2π), ∥f′(t)∥2=sin⁡2t+cos⁡2t=1.

3.1step 1.2step 2.1step 1.4algebra∎

If the refuted equality held at some ξ∈(0,2π), step 1.2 would give (0,0)=2πf′(ξ); step 1.4 would then force f′(ξ)=(0,0), contradicting step 2.1. Thus no such ξ exists.

Remarks

The obstruction is geometric: the curve returns to its initial point while its velocity never vanishes. The scalar mean value theorem is not weakened by this example; the failure is the demand that one point encode a vector increment.

False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

FALSE: the mean value equality holds for vector-valued maps

Statement

False claim. Let m∈N with m≥1, let a<b be real, and let f:[a,b]→Rm be continuous on [a,b] and differentiable on (a,b). Then some ξ∈(a,b) satisfies

f(b)−f(a)=(b−a)f′(ξ).

Facts & Assumptions

Given: The universal equality claim in the Statement.

[L1]

The curve f(t)=(cos⁡t,sin⁡t) on [0,2π] is continuous on its interval and differentiable in its interior, its endpoint increment is zero, and ∥f′(t)∥2=1 for every t∈(0,2π); hence no ξ∈(0,2π) satisfies the claimed equality (The circular curve defeats the equality form of the vector-valued mean value theorem).

[L2]

Let m∈N with m≥1, let a<b be real, and let M≥0 be real. If f:[a,b]→Rm is continuous on [a,b], differentiable on (a,b), and ∥f′(t)∥2≤M throughout (a,b), then ∥f(b)−f(a)∥2≤M(b−a) (The mean value inequality: if f:[a,b]→Rm is continuous and differentiable on (a,b) with ∥f′∥2≤M, then ∥f(b)−f(a)∥2≤M(b−a)).

Refutation

technique · direct
1.1L1

Fact [L1] supplies an instance with m=2, a=0, and b=2π that satisfies both hypotheses of the false claim but not its conclusion.

2.1step 1.1

Therefore the universal equality claim is false.

3.1L2∎

The failure does not affect the vector-valued mean value inequality: under its derivative-bound hypothesis, the estimate in [L2] remains valid.

Remarks

When m=1, the scalar mean value theorem does give the equality. The circular curve shows that the passage to a vector codomain, not a loss of regularity, is what breaks it.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

sin⁡(xy) and its mixed partial derivatives

Example

For

f:R2⟶R,f(x,y)=sin⁡(xy),

the first partial derivatives and the two mixed partial derivatives exist everywhere and satisfy

∂xf(x,y)=ycos⁡(xy),∂yf(x,y)=xcos⁡(xy),

∂y∂xf(x,y)=∂x∂yf(x,y)=cos⁡(xy)−xysin⁡(xy).

These formulas hold without excluding either coordinate axis.

Facts & Assumptions

Given: The function f(x,y)=sin⁡(xy) on R2.

[L1]

The functions sin⁡ and cos⁡ are differentiable on R, with (sin⁡t)′=cos⁡t and (cos⁡t)′=−sin⁡t (The derivatives of sine and cosine are cosine and minus sine).

[L4]

A coordinate partial derivative is the derivative at zero of the corresponding coordinate-line restriction (Directional derivatives and partial derivatives of a map U⊆Rm→Rn).

Verification

technique · direct
1.1L1L2L4

Fixing y and differentiating the map x↦sin⁡(xy) gives ∂xf(x,y)=ycos⁡(xy).

1.2L1L2L4

Fixing x and differentiating the map y↦sin⁡(xy) gives ∂yf(x,y)=xcos⁡(xy).

2.1step 1.1L1L2L3

Differentiating the formula in step 1.1 with respect to y gives ∂y∂xf(x,y)=cos⁡(xy)−xysin⁡(xy).

2.2step 1.2L1L2L3

Differentiating the formula in step 1.2 with respect to x gives ∂x∂yf(x,y)=cos⁡(xy)−xysin⁡(xy).

3.1step 1.1step 1.2step 2.1step 2.2∎

The formulas in steps 1.1 through 2.2 are defined for every (x,y)∈R2, including x=0 or y=0, and the two mixed partials agree everywhere.

Remarks

The equality is obtained by direct calculation rather than by invoking Clairaut--Schwarz theorem for continuous second partial derivatives. It is therefore an explicit instance of that theorem, not an application used to determine the common formula.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

xysin⁡(1/(x2+y2)) is differentiable at the origin with unbounded partial derivatives nearby

Example

Define f:R2→R by

f(0,0)=0,f(x,y)=xysin⁡ ⁣(1x2+y2)when (x,y)≠(0,0).

Then f is totally differentiable at the origin with Df(0,0)=0. Both partial derivatives exist at every point, but each is unbounded on every neighbourhood of the origin.

Facts & Assumptions

Given: The function f in the Example and s=x2+y2.

[L1]

For every real t, ∣sin⁡t∣≤1 and ∣cos⁡t∣≤1 (Parity and the Pythagorean identity for sine and cosine).

[L2]

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

[L5]

A map is totally differentiable at the origin with derivative zero when ∣f(h)∣/∥h∥2→0 as h→0 through nonzero vectors (The total (Fréchet) derivative Df(a) as the linear first-order approximation with o(∥h∥2) remainder).

[L6]

The coordinate partial derivatives are the derivatives of the two coordinate-line restrictions (Directional derivatives and partial derivatives of a map U⊆Rm→Rn).

[L7]

For (x,y)∈R2, ∥(x,y)∥2=x2+y2 (The p-norms ∥x∥p for rational p≥1, and ∥x∥∞).

[L9]

For every real ε>0 there is a natural n≥1 with 1/n<ε (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε).

[L10]

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

[L11]

Verification

technique · direct
1.1algebra

For all real x,y, 2∣xy∣≤x2+y2=s, since (∣x∣−∣y∣)2≥0.

1.2givenL6

Both coordinate-line restrictions through the origin are identically zero, so ∂xf(0,0)=∂yf(0,0)=0.

1.3givenL2L3L4algebra

At every point with s>0, the derivative rules give ∂xf=ysin⁡(1/s)−2x2ycos⁡(1/s)/s2 and ∂yf=xsin⁡(1/s)−2xy2cos⁡(1/s)/s2.

1.4L9L10L11algebra

For k≥1 put ak=1/4πk. Then ak>0 and ak→0: for ε>0, choose N≥1 with 1/N<4πε2 by [L9]; if k≥N, then 0<ak2=1/(4πk)<ε2, hence ak<ε.

2.1givenstep 1.1L1L7

If (x,y)≠(0,0), then ∣f(x,y)∣≤∣xy∣≤s/2=∥(x,y)∥22/2.

2.2step 1.3L2L8algebra

Since 1/(2ak2)=2πk, periodicity and the values in [L2] give sin⁡(1/(2ak2))=0 and cos⁡(1/(2ak2))=1; step 1.3 therefore gives ∂xf(ak,ak)=∂yf(ak,ak)=−1/(2ak).

3.1step 2.1L5algebra

Dividing step 2.1 by ∥(x,y)∥2>0 gives ∣f(x,y)∣/∥(x,y)∥2≤∥(x,y)∥2/2→0, so f is totally differentiable at the origin with derivative zero.

4.1step 1.4step 2.2L7choose∎

Given any neighbourhood radius δ>0 and any bound B>0, step 1.4 permits a k with ak<min⁡{δ/2,1/(2B)}; then ∥(ak,ak)∥2<δ while step 2.2 gives ∣∂xf(ak,ak)∣=∣∂yf(ak,ak)∣>B. Thus both partial derivatives are unbounded on every neighbourhood of the origin.

Remarks

Differentiability at one point controls the size of the function's increment there. It does not impose a bound on derivatives at nearby points, and the rapidly oscillating reciprocal phase makes that distinction explicit.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

r2sin⁡(1/r) is differentiable at the origin with a discontinuous gradient

Example

For (x,y)∈R2 put r=x2+y2 and define

F(0,0)=0,F(x,y)=r2sin⁡(1/r)when r>0.

Then F is totally differentiable at the origin with derivative zero. On the punctured plane,

∇F(x,y)=(2rsin⁡(1/r)−cos⁡(1/r))(xr,yr),

and this gradient is not continuous at the origin.

Facts & Assumptions

Given: The function F in the Example and r=∥(x,y)∥2.

[L1]

For (x,y)∈R2, ∥(x,y)∥2=x2+y2 (The p-norms ∥x∥p for rational p≥1, and ∥x∥∞).

[L2]

For every real t, ∣sin⁡t∣≤1 and sin⁡2t+cos⁡2t=1 (Parity and the Pythagorean identity for sine and cosine).

[L3]

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

[L6]

A map is totally differentiable at the origin with derivative zero when ∣F(h)∣/∥h∥2→0 as h→0 through nonzero vectors (The total (Fréchet) derivative Df(a) as the linear first-order approximation with o(∥h∥2) remainder).

[L7]

For a scalar function, the gradient is the vector of its coordinate partial derivatives (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[L8]

On (0,∞), (u1/2)′=12u−1/2 (Continuity and derivatives of positive-base real powers).

[L9]

If a>0 and q∈Q, 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).

[L11]

For every real t, sin⁡(t+π)=−sin⁡t and cos⁡(t+π)=−cos⁡t (Quarter-turn values and shifts by pi/2 and pi).

[L13]

For every real ε>0 there is a natural n≥1 with 1/n<ε (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε).

[L14]
[L15]

If a map is totally differentiable at a point, then each partial derivative there equals the total derivative applied to the corresponding standard basis vector (A total derivative computes every directional derivative, and its matrix is the Jacobian).

Verification

technique · direct
1.1givenL1L2algebra

For r>0, ∣F(x,y)∣/r=r∣sin⁡(1/r)∣≤r; hence this quotient tends to zero as (x,y)→(0,0).

1.2L13L14algebra

For k≥1 put ak=1/(2πk) and bk=1/((2k+1)π). Both are positive. Given ε>0, apply [L13] to 2πε>0 to obtain N≥1 with 1/N<2πε; then k≥N gives 0<bk<ak≤1/(2πN)<ε. Thus ak→0 and bk→0.

1.3givenL4L5L8L9L10algebra

On the punctured plane, applying the derivative of the positive square root to r=(x2+y2)1/2 gives ∂xr=x/r and ∂yr=y/r.

1.4L3L4L5algebra

For g(r)=r2sin⁡(1/r) on (0,∞), the derivative rules give g′(r)=2rsin⁡(1/r)−cos⁡(1/r).

2.1step 1.1L6L7L15

Therefore F is totally differentiable at the origin with derivative zero, and ∇F(0,0)=(0,0).

2.2step 1.3step 1.4L7

Since F(x,y)=g(r) for r>0, steps 1.3 and 1.4 and the definition of the gradient give ∇F(x,y)=(2rsin⁡(1/r)−cos⁡(1/r))(x/r,y/r).

3.1step 1.2step 2.2L3L11L12algebra

Along the positive x-axis, periodicity gives ∇F(ak,0)=(−1,0), while periodicity followed by the shift through π gives ∇F(bk,0)=(1,0).

4.1step 2.1step 1.2step 3.1∎

Both point sequences in step 1.2 approach the origin but their gradient values in step 3.1 are distinct constants, so ∇F has no limit at the origin and is not continuous there.

Remarks

The factor r2 is strong enough to make F(h)=o(∥h∥2) at the origin. Differentiation removes one radial power and exposes the undamped cosine oscillation, which is why the gradient behaves differently from the function.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The family sin⁡(nx)sin⁡(ny) is uniformly bounded but not equicontinuous

Example

Let K=[0,π]2 with the Euclidean metric. For every natural n≥1, define

fn:K⟶R,fn(x,y)=sin⁡(nx)sin⁡(ny).

Every fn is continuous, and the family F={fn:n≥1} is uniformly bounded by 1. It is not equicontinuous at the origin, and hence is not equicontinuous on K.

Facts & Assumptions

Given: The compact square K=[0,π]2 and the family F in the Example.

[L1]

For a nonempty compact metric space K, a family F⊆C(K,R) is equicontinuous at a when every ε>0 admits one δ>0 that works for every f∈F and every x∈K; it is uniformly bounded when one M≥0 bounds ∣f(x)∣ for all f and x (Equicontinuity, pointwise boundedness, and uniform boundedness for families in C(K,R)).

[L2]

For every real t, sin⁡(−t)=−sin⁡t and ∣sin⁡t∣≤1 (Parity and the Pythagorean identity for sine and cosine).

[L3]

For all reals u,v, ∣sin⁡u−sin⁡v∣≤∣u−v∣ (Sine and cosine are 1-Lipschitz on R).

[L4]
[L5]

For every real ε>0 there is a natural n≥1 with 1/n<ε (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε).

[L6]
[L8]

For (u,v)∈R2, ∥(u,v)∥2=u2+v2 (The p-norms ∥x∥p for rational p≥1, and ∥x∥∞).

Verification

technique · direct
1.1givenL6L7

The set K is a nonempty closed box in R2, so it is compact.

1.2givenL2L3L8algebra

For fixed n≥1 and points (x,y),(u,v)∈K, the sine bound and Lipschitz estimate give ∣fn(x,y)−fn(u,v)∣≤n∣x−u∣+n∣y−v∣≤2n∥(x−u,y−v)∥2; hence fn is continuous on K.

1.3givenL1L2algebra

For every n≥1 and (x,y)∈K, ∣fn(x,y)∣≤1, so F is uniformly bounded.

1.4givenL2L4L6algebra

For every n≥1, fn(0,0)=0, while at pn=(π/(2n),π/(2n))∈K one has fn(pn)=1.

2.1step 1.4L5L6L8choosealgebra

Let δ>0. Applying [L5] to δ/π>0 gives some natural n≥1 with π/n<δ, and then d2(pn,(0,0))=π/(2 n)<π/n<δ.

3.1step 1.1step 1.2step 1.4step 2.1L1∎

Taking ε=1/2, steps 1.4 and 2.1 show that every δ>0 admits an fn∈F and a point pn∈K within δ of the origin for which ∣fn(pn)−fn(0,0)∣=1>ε. Thus the family is not equicontinuous at the origin.

Remarks

Uniform boundedness controls the range of every function in the family. Equicontinuity asks for a common spatial scale, and the oscillation scale 1/n prevents such a scale at the origin.

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

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.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The surface generated by rotating y=sin⁡x on [0,π] has area 2π(2+arsinh⁡1)

Example

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

A=2π(2+arsinh⁡1)=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)=sin⁡x 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)2 ds (The surface of revolution has area 2π∫abr(s)1+r′(s)2 ds).

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

The function sinh⁡:R→R is odd, strictly increasing, and onto; cosh⁡ is positive; cosh⁡2v−sinh⁡2v=1; and (sinh⁡v)′=cosh⁡v (Addition formulas, identities, parity, and derivatives of the hyperbolic functions).

[L5]

Let I⊆R be order-convex with at least two elements, let f:I→R be continuous and injective, and let g:f[I]→I be its inverse. If f is differentiable at c∈I 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 c∈I 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, arsinh⁡u=log⁡(u+u2+1) (Logarithm formulas for inverse sinh, inverse cosh, and inverse tanh on their natural domains).

[L7]

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

[L8]

If a>0 and q∈Q, 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 a≥0 with (a)2=a; the positives are {x2:x≠0}).

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

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

Verification

technique · direct
1.1F1F2L1L2L3

Facts [L1], [L2], and [L3] verify the hypotheses in [F2], so [F1] gives A=2π∫0πsin⁡x1+cos⁡2x dx.

1.2L3L4L5L9algebra

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

1.3L1L2L3L7L8L9L12algebra

Since π>0 by [L1], the interval [0,π] is nondegenerate. The function x↦sin⁡x1+cos⁡2x is continuous on this interval and hence integrable there.

2.1step 1.2L2L7L8L9L10L11algebra

Define G(x)=−12(arsinh⁡(cos⁡x)+cos⁡x1+cos⁡2x). Using step 1.2, the derivative of the positive square root, and the chain and product rules gives G′(x)=sin⁡x1+cos⁡2x.

3.1step 1.2step 1.3step 2.1L6L9L13L14algebra

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

4.1step 1.1step 3.1algebra∎

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

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.

False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

FALSE: spherical coordinates are globally injective

Statement

False claim. The spherical-coordinate map

S(r,ϕ,θ)=(rsin⁡ϕcos⁡θ, rsin⁡ϕsin⁡θ, rcos⁡ϕ)

is injective on [0,∞)×[0,π]×[0,2π].

The angular seam identifies θ=0 with θ=2π. At either polar angle, every azimuth represents the same point, and at radius zero both angles are lost. The Jacobian determinant

det⁡DS(r,ϕ,θ)=r2sin⁡ϕ

vanishes on the zero-radius and polar-axis loci.

Facts & Assumptions

Given: The map S:R3→R3 displayed in the Statement and its restriction to D=[0,∞)×[0,π]×[0,2π].

[L1]

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

[L2]

For every real t, sin⁡2t+cos⁡2t=1 (Parity and the Pythagorean identity for sine and cosine).

[L3]

Sine vanishes exactly at the integer multiples of π, and both sine and cosine have period 2π (The zero sets of sine and cosine and the least positive common period 2 pi).

[L4]

sin⁡(π/2)=1, cos⁡(π/2)=0, sin⁡π=0, and cos⁡π=−1 (Quarter-turn values and shifts by pi/2 and pi).

[L5]

For a C1 map g:R3→R3, its Jacobian matrix consists of its coordinate partial derivatives and its Jacobian determinant is det⁡Dg (The Jacobian determinant of a square-dimensional C1 map is the determinant of its Jacobian matrix).

[L6]

Finite componentwise products and composites of C1 Euclidean maps are C1 (Ck Euclidean maps are closed under componentwise algebra and composition).

[L7]
[L8]

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

Refutation

technique · direct
1.1givenL1L3L4L7

The two distinct points (1,π/2,0) and (1,π/2,2π) lie in D, and periodicity gives S(1,π/2,0)=S(1,π/2,2π)=(1,0,0).

1.2givenL1L3L4algebra

At ϕ=0, every θ∈[0,2π] gives S(r,0,θ)=(0,0,r); at ϕ=π, every such θ gives S(r,π,θ)=(0,0,−r); and S(0,ϕ,θ)=(0,0,0) for every pair of angles.

1.3L1L6L8

The coordinate functions of S are finite products and composites of coordinate maps with sine and cosine; their displayed derivatives are continuous, so S is C1.

2.1step 1.3L1L5algebra

Direct partial differentiation gives the following.

DS=(sin⁡ϕcos⁡θrcos⁡ϕcos⁡θ−rsin⁡ϕsin⁡θsin⁡ϕsin⁡θrcos⁡ϕsin⁡θrsin⁡ϕcos⁡θcos⁡ϕ−rsin⁡ϕ0)

3.1step 2.1L2algebra

Expanding the determinant in step 2.1 and using the Pythagorean identity gives det⁡DS=r2sin⁡ϕ.

4.1step 1.1step 1.2step 3.1L3∎

Step 1.1 already refutes global injectivity. Steps 1.2 and 3.1 show the additional pole and zero-radius identifications and show that the derivative is singular there, since r2sin⁡ϕ=0 when r=0, ϕ=0, or ϕ=π.

Remarks

Restricting the radius away from zero, the polar angle away from its endpoints, and the azimuth to a half-open interval removes these particular identifications. The false claim fails because the full closed parameter domain retains every seam and collapsed angular coordinate.

Sources