# Quasi-isometric recognition of virtually polycyclic groups

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Quasi-isometric Recognition of Virtually Polycyclic Groups](../../preprints/quasi-isometric-recognition-of-virtually-polycyclic-groups-September-24-2026/paper.pdf)

## Scope

The formalization proves quasi-isometric recognition of virtually polycyclic groups: every finitely generated group quasi-isometric to a finitely generated virtually polycyclic group is itself virtually polycyclic. It also realizes a finite-index subgroup of the recognized group as a uniform lattice in a simply connected solvable Lie group, which may differ from the original ambient group.

The linked structural estimate controls the height-coordinate behavior of self quasi-isometries of the stated unimodular solvable Lie models, up to bounded error and one of finitely many linear height symmetries.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Quasi-isometric recognition of virtually polycyclic groups and solvable lattices | [PolycyclicRecognition.lean](../ComparatorChallenges/PolycyclicRecognition.lean) |