False statementConstruction: 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.

FALSE: spherical coordinates are globally injective

Statement

False claim. The spherical-coordinate map

$S (r, ϕ, θ) = (r \sin ϕ \cos θ, r \sin ϕ \sin θ, r \cos ϕ)$

is injective on $[0, \infty) \times [0, π] \times [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 D S (r, ϕ, θ) = r^{2} \sin ϕ$

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

Facts & Assumptions

Given: The map $S : R^{3} \to R^{3}$ displayed in the Statement and its restriction to $D = [0, \infty) \times [0, π] \times [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^{2} t + \cos^{2} t = 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 $C^{1}$ map $g : R^{3} \to R^{3}$ , its Jacobian matrix consists of its coordinate partial derivatives and its Jacobian determinant is $\det D g$ (The Jacobian determinant of a square-dimensional $C^{1}$ map is the determinant of its Jacobian matrix).

[L6]

Finite componentwise products and composites of $C^{1}$ Euclidean maps are $C^{1}$ ( $C^{k}$ Euclidean maps are closed under componentwise algebra and composition).

[L7]

The number $π$ is positive (Pi as twice the smallest positive zero of cosine).

[L8]

For a real-valued function on $A \subseteq R$ , differentiability at a limit point $c \in 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 $θ \in [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 $C^{1}$ .

2.1step 1.3L1L5algebra

Direct partial differentiation gives the following.

$D S = (\begin{array}{ccc} \sin ϕ \cos θ & r \cos ϕ \cos θ & - r \sin ϕ \sin θ \\ \sin ϕ \sin θ & r \cos ϕ \sin θ & r \sin ϕ \cos θ \\ \cos ϕ & - r \sin ϕ & 0 \end{array})$

3.1step 2.1L2algebra

Expanding the determinant in step 2.1 and using the Pythagorean identity gives $\det D S = r^{2} \sin ϕ$ .

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 $r^{2} \sin ϕ = 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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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

J. Lebl, Basic Analysis II, section 11.4 Complex exponential and trigonometric functions (standard reference, not scraped)