RecenteredGuideCompactness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual stopped charts recentered at their physical tips. The tip may escape to infinity as the ribbon front varies; subtracting it before the normal-family argument removes any artificial bound on its location.

theorem OAI.SLEExactGauge.recentered_actual_guide_compactness line 16