CartanBoxPaths.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous controlled-height paths to the actual Cartan boxes

Uniform generation and support visits now combine without a path premise. Every endpoint of a fixed-radius box is reached, on any allowed pivot, by one continuous path with uniform coarse speed and logarithmic error.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cartan_box_path_bound line 35
Source documentation
The fixed-radius support-path conclusion for the actual box and its actual inclusion in the ambient group. All geometric bounds are derived.
```
theorem exists_cartan_box_path_bound
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput