Proof of `Repeated cuts yield a balanced light separator` (1st 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
Induct on remainder cardinality. A large remainder receives an oracle cut whose nonempty right shore strictly reduces it; prepend that cut to the recursively constructed trace. A small remainder stops immediately. Apply the proved trace analysis to obtain the final separator and cost.