ActualGeometricTubeSupport.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The required open-tube support follows from the actual capacity driver of a prescribed simple arc, finite Brownian driver tubes, and deterministic trace stability. No geometric support input is assumed.

theorem OAI.SLEExactGauge.ordinary_geometricTubeSupport line 16