CartanRayFiberPaths.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual paths between ideal-fiber representatives at negative height

A fixed ideal element enters the expanding mixed-word box. Its support path can be based at the ray pivot even though the template does not contain zero.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_negative_height_ideal_fiber_paths line 35
Source documentation
Every fixed ray-ideal displacement can be realized at linearly negative height by an actual path with linear coarse speed and logarithmic error. The path constant is independent of the ideal displacement; the threshold is allowed to depend on it.
```
theorem exists_negative_height_ideal_fiber_paths
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput
theorem OAI.PolycyclicRecognition.CartanWordModel.exists_negative_height_ideal_fiber_words line 98
Source documentation
Unit-step representatives of the actual ideal-fiber difference. Every prefix retains a negative linear height margin, and remains in a linear ball about the ray pivot.
```
theorem exists_negative_height_ideal_fiber_words
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput
theorem OAI.PolycyclicRecognition.CartanWordModel.exists_negative_height_ideal_fiber_chains line 167
Source documentation
Actual chains for ideal-fiber independence, with an absolute linear radius and the canonical negative-height margin.
```
theorem exists_negative_height_ideal_fiber_chains
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput