OAI/GroupTheory/PolycyclicRecognition/Geometry/SequenceCartanBoxAction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vanishing-height Cartan conjugation preserves a scaled template box

The input box is already exponentially scaled. The small translation of its template is absorbed into one subexponential radius in the original basis.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_sequence_small_height_box_action line 32