CartanSegmentPaths.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Paths to segment boxes before height factorization

Every point of the actual box determined by a Cartan segment is reached by a controlled path. Under an arbitrary linearly bounded homomorphism, that path stays over the corresponding target segment. No factorization through canonical height is required.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_segment_box_path_bound line 34
Source documentation
Actual segment-box reachability with control under the homomorphism that will be constrained by stationary volume comparison.
```
theorem exists_segment_box_path_bound
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput