FutureSlitHeight.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Every point of a mapped future segment lies in a strip whose squared height is at most twice the exact remaining capacity.