OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanRootCocycle.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sublinear logarithmic bounds on actual Cartan root coordinates

First approximate the cocycle on the nilpotent Cartan factor. A contracting one-parameter subgroup then carries every root vector into a fixed compact ball in logarithmic time. This retains the nilpotent correction in the generalized root action.

  1. theorem OAI.PolycyclicRecognition.cartan_root_cocycle_sublinear_log line 39