OAI/GroupTheory/PolycyclicRecognition/Analysis/ShortSubgroupChains.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Short strict subgroup chains force superpolynomial growth

This is the counting step for the cyclic-kernel finite-generation argument: a new conjugate at every window gives a linearly short new subgroup element, and binary products then give exponentially many points in a quadratic ball.

  1. def OAI.PolycyclicRecognition.binaryProducts line 18
  2. theorem OAI.PolycyclicRecognition.binaryProducts_mem line 22
  3. theorem OAI.PolycyclicRecognition.binaryProducts_card line 38
  4. theorem OAI.PolycyclicRecognition.binaryProducts_word_bound line 56
  5. theorem OAI.PolycyclicRecognition.polynomial_growth_forbids_short_strict_chain line 69