CartanSupportSwitch.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One switch constant for the actual Cartan alphabet

The finite family of nonzero root generators admits one logarithmic switch bound. At a supporting position, the large generator amplitude cancels the scalar part of the adjoint action exactly.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_support_switch_bound line 30
Source documentation
Uniformly short supporting switches for every letter in the constructed Cartan word model, including its generalized-root nilpotent corrections.
```
theorem exists_uniform_support_switch_bound
    (Exp : GroupLieAlgebra (𝓘(ℝ, EG)) G → G) (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput