CartanSegmentCoding.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous endpoint families in actual segment boxes

A common coordinate ball parametrizes true endpoints in every maximizing rescaled box. The chosen support paths have continuous time samples and uniform bounds, so coordinates can be sampled independently of normalized quasi-isometry pairs.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_continuous_segment_box_paths line 33
Source documentation
Actual segment-box endpoints have continuously sampled paths on a common positive-radius coordinate ball, with uniform coarse metric bounds.
```
theorem exists_continuous_segment_box_paths
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput