CartanGlobalGeneratorWords.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded generator word width of the whole Cartan nilpotent factor

Uniform rescaled generation has a fixed word-length bound. Letting all positive widths grow exhausts the Lie algebra; absorbing the scale into the unrestricted real amplitudes gives the same bound globally.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_global_cartan_generator_words_lie line 30
Source documentation
Uniform Cartan box generation gives a global bound for exponential words.
```
theorem exists_global_cartan_generator_words_lie
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput
theorem OAI.PolycyclicRecognition.CartanWordModel.exists_global_cartan_generator_words line 46
Source documentation
A single finite number of homogeneous generator exponentials suffices for every element, with unrestricted real amplitudes.
```
theorem exists_global_cartan_generator_words
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput