CartanProbeBridgeLength.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Metric length of the actual source probe bridge

Conjugation by the pivot cancels the exact height dilation. The remaining residual action contributes one subexponential factor, and logarithmic distortion then retains precisely the small exponential rate.

theorem OAI.PolycyclicRecognition.source_probe_bridge_bound_in_basis line 32
Source documentation
Basis-specific form, so the actual compact section and generator may be estimated after choosing a logarithmic metric bound.
```
theorem source_probe_bridge_bound_in_basis
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput
theorem OAI.PolycyclicRecognition.exists_source_probe_bridge_bound line 77
Source documentation
One fixed basis and constant work for every probe, ideal coordinate, basepoint and sufficiently large scale. All group maps are the actual Cartan-factor maps.
```
theorem exists_source_probe_bridge_bound
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput