OAI/GroupTheory/PolycyclicRecognition/Finiteness/CartanVanishingHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A common subexponential bound for vanishing-height conjugations

The height error is allowed to tend to zero with the scale. The full Cartan logarithm has only a subexponential bound; the adjoint action still sends every bounded correction to one common subexponential coordinate ball.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_vanishing_height_adjoint_bound line 27