OAI/GroupTheory/PolycyclicRecognition/Geometry/LinearContractingPingPong.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Free powers from a concrete contracting linear configuration

Both directions of each of two generators have a dominant eigenline. Uniform source-cone bounds and disjoint target domains then give actual free powers. Every hypothesis is an explicit linear or set-theoretic condition.

  1. def OAI.PolycyclicRecognition.signedPingPongGenerator line 20
  2. theorem OAI.PolycyclicRecognition.free_powers_of_dominant_eigenlines line 23