CartanCompactProbeBridge.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The source bridge for a compact section and an actual neighbor step

The compact section, normalized generator and pivot cancellation are combined before using the metric estimate. The constants are independent of the small parameter and of every ideal probe and starting sheet.

theorem OAI.PolycyclicRecognition.exists_compact_source_probe_bridge_bound line 31
Source documentation
This is the actual neighboring-sheet source bridge. The section is any fixed linear section on a compact cube; the height identity is precisely the contact-facet pivot identity. No geometric bridge bound is assumed.
```
theorem exists_compact_source_probe_bridge_bound
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput