OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialGrowthPingPong.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial growth excludes a pair of ping-pong transformations

This is the explicit bridge from contracting linear dynamics to the word-ball counting obstruction. The free-group injection is the proved library ping-pong lemma, and the exponential count is the actual positive-word count.

  1. theorem OAI.PolycyclicRecognition.polynomial_growth_excludes_ping_pong line 19