ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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 hyperspherical-coordinate Jacobian is the standard product of a radial power and sine powers

Example

For $n = 2$ , use the polar coordinates $x_{1} = r \cos θ$ and $x_{2} = r \sin θ$ . For $n \geq 3$ , write hyperspherical coordinates as $\begin{aligned} x_{1} & = r \cos ϕ_{1}, \\ x_{k} & = r (\prod_{j = 1}^{k - 1} \sin ϕ_{j}) \cos ϕ_{k} (2 \leq k \leq n - 2), \\ x_{n - 1} & = r (\prod_{j = 1}^{n - 2} \sin ϕ_{j}) \cos θ, \\ x_{n} & = r (\prod_{j = 1}^{n - 2} \sin ϕ_{j}) \sin θ . \end{aligned}$ Its absolute Jacobian determinant is $r^{n - 1} \sin^{n - 2} ϕ_{1} \sin^{n - 3} ϕ_{2} \dots \sin ϕ_{n - 2} .$ On compact boxes with $r > 0$ , every $ϕ_{j}$ in a compact subinterval of $(0, π)$ , and $θ \in [π / 6, π / 3]$ , the factor is nonzero and the map is injective.

Facts & Assumptions

Given: The displayed coordinate convention in every dimension $n \geq 2$ .

[L1]

Sine and cosine have their standard derivatives and satisfy $\sin^{2} + \cos^{2} = 1$ (The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine).

[L2]

The determinant is the finite signed-permutation sum (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix), and for same-sized finite square matrices over a commutative ring one has $\det (A B) = \det (A) \det (B)$ (For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ ).

[L3]

Mathematical induction proves a statement from its base case and induction step (The principle of mathematical induction).

[L4]

Cosine is strictly decreasing on $[0, π]$ , and sine vanishes there only at the endpoints (Signs, monotonicity intervals, and ranges of sine and cosine, The zero sets of sine and cosine and the least positive common period 2 pi).

Verification

technique · induction

1.1

For $n = 2$ , the formula is the polar determinant $r$ , with the empty product of sine factors equal to $1$ . Direct differentiation verifies it, while the image norm and strict cosine monotonicity recover the radius and seam-free angle.

L1L4base

1.2

Assume the formula in dimension $n$ . Factor the dimension- $(n + 1)$ coordinate map as $(r, ϕ_{1}, ξ) ⟼ (s, ρ, ξ) = (r \cos ϕ_{1}, r \sin ϕ_{1}, ξ) ⟼ (s, Φ_{n} (ρ, ξ)),$ where $Φ_{n}$ is the dimension- $n$ hyperspherical map in the induction hypothesis.

ihassume-hyp

2.1

By [L1] and [L2], the first map in step 1.2 has a $2 \times 2$ Jacobian block of determinant $r (\cos^{2} ϕ_{1} + \sin^{2} ϕ_{1}) = r$ and an identity block in $ξ$ . The second has a $1 \times 1$ identity block and the Jacobian of $Φ_{n}$ at radius $ρ$ ; [L3] will discharge the induction after this step. The signed-permutation formula gives these block determinants, and multiplicativity with the induction hypothesis gives $r ρ^{n - 1} \prod_{j = 2}^{n - 1} \sin^{n - j} ϕ_{j} = r^{n} \sin^{n - 1} ϕ_{1} \prod_{j = 2}^{n - 1} \sin^{n - j} ϕ_{j} .$ On the stated boxes, the image norm recovers $r$ , then successive coordinate ratios and strict cosine monotonicity [L4] recover every $ϕ_{j}$ , and the final planar pair recovers $θ$ . The sine factors do not vanish, so the map is injective with nonzero determinant. This proves the formula and box claim in dimension $n + 1$ , and [L3] completes the induction.

L1L2L3L4step 1.2discharge-induction: base and induction step∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 130 results over 34 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

A. Leibman, Multidimensional Real Analysis, §5.5 (standard reference, not scraped)