CartanStationaryPaths.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Stationary good paths to actual rescaled endpoints

Independent normalized coordinate volume and continuous endpoint coding instantiate the stationary sampling theorem. A single normalized pair is therefore good on an endpoint subset retaining half the coordinate volume.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_stationary_good_segment_paths line 37
Source documentation
For all large scales, one actual pair has controlled image paths to a subset of the actual rescaled endpoints with half the coordinate volume.
```
theorem exists_stationary_good_segment_paths
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput