CartanUniformGeneration.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform generator words for the actual Cartan boxes

This specializes the compact-law argument to the constructed nilpotent factor and its homogeneous generators. The same length and amplitude bounds work for every box shape, nonnegative scale, and maximizing word basis.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_cartan_rescaled_generator_words line 33
Source documentation
Uniform product generation for the Cartan factor by exponentially rescaled generator factors.
```
theorem exists_uniform_cartan_rescaled_generator_words
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput