CartanInverseSections.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous inverse schemes in actual Cartan boxes

The same published exponential and Dynkin inputs now supply a uniformly bounded continuous endpoint coding on a fixed ball in every actual rescaled Cartan root-ideal chart.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_cartan_inverse_sections line 32
Source documentation
Common continuous endpoint coding for all actual Cartan rescalings.
```
theorem exists_uniform_cartan_inverse_sections
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput