OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialGrowthSemigroupPingPong.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial growth excludes one-sided ping-pong

Equal-length positive words suffice for the exponential word-ball count. No control of the inverse transformations is required.

  1. theorem OAI.PolycyclicRecognition.positive_word_preserves_domain line 16
  2. theorem OAI.PolycyclicRecognition.one_sided_ping_pong_equal_length line 25
  3. theorem OAI.PolycyclicRecognition.one_sided_ping_pong_exponential_word_count line 61
  4. theorem OAI.PolycyclicRecognition.polynomial_growth_excludes_one_sided_ping_pong line 89