LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-10-22 (gpt-6.1-sol)

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.

Volume of an ideal orthoscheme region

Statement

For $0 < ζ < π / 2$ , let $O_{ζ} = {(x + i y, t) \in H^{3} : 0 \leq x \leq \cos ζ, 0 \leq y \leq x \tan ζ, t \geq \sqrt{1 - x^{2} - y^{2}}} .$ Its hyperbolic volume in the upper half-space metric is $\frac{1}{2} Λ (ζ)$ .

Statement references

Jessica S. Purcell, Hyperbolic Knot Theory, Lemma 9.8

Diagram

The shaded triangle is the vertical projection of $O_{ζ}$ . The dashed arc is the unit circle; the vertex $(\cos ζ, \sin ζ)$ lies on it. The region in $H^{3}$ lies above the corresponding unit hemisphere and is unbounded toward the ideal point at infinity. This is a projection only; the proof uses the stated coordinate inequalities and integral.

\begin{center} \begin{tikzpicture}[scale=2.2] \def\a{38} \coordinate (O) at (0,0); \coordinate (A) at ({cos(\a)},0); \coordinate (B) at ({cos(\a)},{sin(\a)}); \fill[blue!12] (O)--(A)--(B)--cycle; \draw[thick,blue!70!black] (O)--(A)--(B)--cycle; \draw[dashed] (1,0) arc[start angle=0,end angle=\a,radius=1]; \draw[->] (-0.08,0)--(1.13,0) node[right] { $x$ }; \draw[->] (0,-0.08)--(0,0.92) node[above] { $y$ }; \draw (0.16,0) arc[start angle=0,end angle=\a,radius=0.16]; \node[below left] at (O) { $O$ }; \node[below] at (A) { $A = (\cos ζ, 0)$ }; \node[above right] at (B) { $B = (\cos ζ, \sin ζ)$ }; \node at (0.28,0.09) { $ζ$ }; \node[below right] at (0.92,0.12) { $x^{2} + y^{2} = 1$ }; \end{tikzpicture} \end{center}

Facts & Assumptions

Given: The region $O_{ζ}$ and $0 < ζ < π / 2$ .

[F1]

Ideal tetrahedron shape and cusp holonomy gives the upper half-space metric with volume density $d x d y d t / t^{3}$ .

[F2]

Lobachevsky function defines $Λ (θ) = - \int_{0}^{θ} \log ∣ 2 \sin u ∣ d u$ .

[F3]

Lobachevsky Fourier expansion and a certified π/3 value proves that $Λ$ is odd and $π$ -periodic, $Λ (π / 2) = 0$ , and $Λ (2 θ) = 2 Λ (θ) + 2 Λ (θ + π / 2)$ .

Proof

1.1givenF1algebra

Integrating the volume density in $t$ gives $Vol (O_{ζ}) = \int_{0}^{\cos ζ} \int_{0}^{x \tan ζ} \frac{d y d x}{2 (1 - x^{2} - y^{2})}$ . For fixed $x$ , put $A = \sqrt{1 - x^{2}}$ ; since $x \tan ζ < A$ for $0 \leq x < \cos ζ$ , the inner integral is $\frac{1}{4 A} \log \frac{A + x \tan ζ}{A - x \tan ζ}$ .

2.1F2step 1.1algebra

Set $x = \cos θ$ , so $ζ \leq θ \leq π / 2$ . Sine addition identities change the logarithm ratio to $\sin (θ + ζ) / \sin (θ - ζ)$ , and therefore $Vol (O_{ζ}) = \frac{1}{4} \int_{ζ}^{π / 2} \log \frac{\sin (θ + ζ)}{\sin (θ - ζ)} d θ = \frac{1}{4} (Λ (2 ζ) - Λ (π / 2 + ζ) + Λ (π / 2 - ζ))$ . The logarithmic singularity at $θ = ζ$ is integrable, so the substitution and improper endpoint evaluation are valid.

3.1F3step 2.1algebra∎

By oddness and period $π$ from [F3], $Λ (π / 2 - ζ) = - Λ (π / 2 + ζ)$ . Also [F3] gives $Λ (2 ζ) = 2 Λ (ζ) + 2 Λ (ζ + π / 2)$ . Substitution in step 2.1 cancels the two $Λ (ζ + π / 2)$ terms and leaves $Vol (O_{ζ}) = \frac{1}{2} Λ (ζ)$ .

Sources

Jessica S. Purcell, Hyperbolic Knot Theory, Lemma 9.8

Depends on

Used by

Volume of the regular ideal tetrahedron Theorem

Dependency tree · one level

3 results within one dependency step 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

Jessica S. Purcell, Hyperbolic Knot Theory (standard reference, not scraped)
William P. Thurston, The Geometry and Topology of Three-Manifolds (standard reference, not scraped)