OAI/GroupTheory/PolycyclicRecognition/Algebra/RecognitionFromPolycyclicComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The geometric height estimate feeds the original polycyclic comparison

This composition removes the separate Poincaré-duality comparison premise. The corrected height estimate remains a geometric obligation; this theorem is not the manuscript's completed recognition theorem.

  1. theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_corrected_height_coarse_virtualPolycyclic line 29