Non-Pseudo-Arithmetic Hyperbolic 4-Manifolds
Alexander Kolpakov
math.GT
Nov 4, 2026 · v1
math.GR
TL;DR
A Lean 4/Mathlib project verifies the radical identity, the number-field non-total-reality obstruction, the Gram matrix audits, and the conditional lattice and manifold implications.
Abstract
We give three explicit finite-volume hyperbolic Coxeter lattices in dimension four whose adjoint trace fields are not totally real. They are the reflection groups of the Ma–Zheng polytopes $P_{11,6}$, $P_{11,7}$, $P_{11,8}$. The obstruction is contained in two cyclic products of the doubled unit-normal Gram matrix $A=2G$. Those products recover elements $s=\sqrt5$ and $u$ satisfying $$ (s-1)u^2+2(s-3)u+s-7=0. $$ After the embedding $s\mapsto-\sqrt5$, this quadratic has discriminant $8(1-\sqrt5)<0$. The cyclic-product field therefore has a complex place. Vinberg's identification of that field with the adjoint trace field and the Emery–Mila total-reality obstruction imply that the three lattices are not pseudo-arithmetic. Torsion-free orientation-preserving finite-index subgroups yield orientable noncompact finite-volume hyperbolic $4$-manifolds with the same obstruction. Exact computations check the census data and provide independent field and finite-volume certificates. A pinned Lean 4 development verifies the radical identity and the number-field obstruction. It also checks the lattice and manifold implications conditional on explicit geometric and literature hypotheses.
Problem
Emery and Mila asked whether every lattice in PO(n,1), n>3, is pseudo-arithmetic, and whether every such lattice has a totally real adjoint trace field. No non-pseudo-arithmetic example was previously known in these dimensions.
Approach
Three finite-volume Coxeter 4-polytopes P_{11,6}, P_{11,7}, P_{11,8} from the Ma–Zheng census are examined. Cyclic products of the doubled Gram matrix recover s=√5 and an element u satisfying (s-1)u²+2(s-3)u+s-7=0. Under s↦-√5 this quadratic has negative discriminant, which gives a complex place. Vinberg's field identification and the Emery–Mila obstruction then rule out pseudo-arithmeticity. Exact Python computations and a Lean 4 project pinned to Mathlib check the algebra, the Gram matrices, and the conditional implications from stated external hypotheses.
Results
The three reflection groups have adjoint trace fields that are not totally real, so they are not pseudo-arithmetic. Torsion-free finite-index subgroups give orientable noncompact finite-volume hyperbolic 4-manifolds with non-pseudo-arithmetic fundamental groups. Lean proves the algebraic obstruction unconditionally and the geometric conclusions conditional on explicit literature inputs.
| polytope | cusps | volume |
|---|
| P_{11,6} | 1 | 13π²/864 |
| P_{11,7} | 1 | π²/54 |
| P_{11,8} | 2 | 19π²/864 |
The three Ma–Zheng census rows used in the proof
