The Coxeter Group [5,3,3,3] Has No Torsion-Free Subgroup of Index 14400: A Computer-Assisted Result Related to Problem 4.124 of the K3 List

Problem 4.124 of the K3 problem list asks whether a hyperbolic integer homology 4-sphere exists, whether an arithmetic one exists, and more generally whether there is a closed hyperbolic 4-manifold with Euler characteristic 2. By a theorem of Belolipetsky, an orientable arithmetic example would be the quotient of \(\mathbb{H}^4\) by a torsion-free subgroup of index 28800 of the Coxeter group \(W=[5,3,3,3]\) that lies in the rotation subgroup of \(W\). We prove, with computer assistance, that \(W\) has no torsion-free subgroup of index 14400. This answers a question that goes back to a remark of Davis from 1985, who thought such a subgroup quite possible. Equivalently: no facet pairing of a single compact regular hyperbolic 120-cell with dihedral angle \(2\pi/3\) gives a closed hyperbolic 4-manifold; every torsion-free subgroup of finite index of \(W\) has index \(14400\,m\) with \(m\ge 2\) (Conder and Maclachlan found one with \(m=8\)); and no closed manifold that covers the orbifold \(\mathbb{H}^4/W\) has Euler characteristic 1. The proof reduces the question, with complete proofs, to the enumeration of certain involutions of the 14400 flags of the 120-cell. It then rests on two exhaustive enumerations, made by two separately written programs with different symmetry reductions and different pruning rules; both find nothing. No complete gluing was reached in either enumeration, so the result depends on every pruning rule being a necessary condition. We prove this for each of the 13 rules of the first program and each of the 14 rules of the second, and we report controls, mutation tests and partial re-enumerations with a third program. The theorem decides none of the three questions of Problem 4.124. It excludes only those subgroups of index 28800 that correspond to double covers of one-cell manifolds; the case of index 28800 itself is out of reach of our programs, and the problem stays open. This is an unrefereed note.