Proof of `Repeated cuts yield a balanced light separator` (2nd statement)
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The remainder equals the initial set minus previously discarded shores. Hence discarded shores are disjoint and their nonemptiness bounds the number of cuts. The exclusive pieces and final remainder partition all undeleted vertices without cross edges. Their size bounds certify balance; the cumulative cut-cost theorem gives the separator budget.