SmallDriverRise.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed small-driver neighborhood forces a vertical rise; the radius does not depend on a choice of continuous capacity-two trace.