Papers With

← All papers
First page of Sharp dimension bounds for right-angled hyperbolic polytopes

Sharp dimension bounds for right-angled hyperbolic polytopes

Alexander Kolpakov

math.GT Oct 28, 2026 · v1 math.MG
formalization geometry
Read PDF arXiv abstract Code
TL;DR
Lean 4 modules in the accompanying repository check the logical deductions for the projection, cubic bound and dimension bounds, with geometric facts taken as premises.
Abstract
We determine the largest dimensions in which right-angled hyperbolic polytopes of finite volume can exist. The dimension is at most eight in general, and at most four when all vertices lie at infinity. Both bounds are attained, improving the previously known upper bounds of twelve and six. Our proofs use elementary properties of hyperbolic polytopes together with bounds for configurations of points on spheres.
Problem

The question is the largest dimension in which finite-volume right-angled hyperbolic polytopes exist, both in general and when all vertices are ideal. The previous upper bounds were twelve and six.

Approach

Repeatedly projecting an interior point to a facet of maximum height produces a low-dimensional face whose outward normals form a spherical code with bounded inner products. In dimension nine, a cubic sum-of-tensor-squares argument bounds such a six-dimensional code by 26, below the known minimum of 27 facets. In the ideal case, Musin's kissing-number theorem and a minimum-facet theorem identify the facet as the ideal 24-cell, which contradicts the height bound. Exact Python checks and Lean 4 modules verify the algebraic identities and the logical deductions.

Results

Finite-volume right-angled hyperbolic polytopes have dimension at most eight, and entirely ideal ones have dimension at most four. Known examples attain both bounds, so both are sharp.