Papers With

← All papers
First page of On the second smallest ideal right-angled hyperbolic four-polytope

On the second smallest ideal right-angled hyperbolic four-polytope

Alexander Kolpakov

math.GT Oct 28, 2026 · v1 math.MG
formalization geometry
Read PDF arXiv abstract Code
TL;DR
Selected Lean 4 modules machine-check the internal logical deductions for the volume gap, equality reduction, cut-count recursion and gluing implication.
Abstract
The regular ideal right-angled 24-cell has volume $4 π^2/3$ and is the unique minimum-volume entirely ideal right-angled hyperbolic four-polytope. We prove that the next distinct volume is $8 π^2/3$ and that its unique equality case is the reflection double of the 24-cell across one octahedral facet. We also show that an entirely ideal right-angled four-polytope whose facets are regular ideal octahedra or their doubles across triangular faces decomposes into a chain of regular 24-cells, with opposite cutting facets in each intermediate cell.
Problem

The regular ideal right-angled 24-cell is the unique minimum-volume entirely ideal right-angled hyperbolic four-polytope, with volume 4π²/3. The next distinct volume in this spectrum and the polytope attaining it were not known.

Approach

Gauss–Bonnet gives a discrete volume formula in terms of a ridge-defect quantity W(P), which links to facet defects. An opposite-cusp injection lemma, combined with cusp-shape calculations for antiprisms and doubled octahedra, gives a facet-defect inequality that rules out intermediate volumes. An octahedral cutting argument then identifies the equality case. Selected logical deductions are checked in Lean 4 modules, alongside Python code.

Results

The second distinct volume is 8π²/3, and the reflection double of the 24-cell across one octahedral facet is the unique polytope attaining it. Polytopes whose facets are all regular ideal octahedra or their doubles across triangular faces decompose into chains of regular 24-cells, with volume (k+1)·4π²/3.