OAI/GroupTheory/PolycyclicRecognition/Geometry/RecognitionFromAffineHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recognition from affine height control

An invariant mean, finite-index corrected height and Poincaré-duality comparison turn an affine height bound into a recognition conclusion.

  1. theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_affine_height_coarse_virtualPolycyclic line 19