Proof of `The split flow-cut certificate must give a cheap separation`
groundedproofs/Lax263307Proofs/ForcedSeparation.lean · lax-263307
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
Apply the proved split certificate dichotomy. A high-value flow would produce a uniform-endpoint route distribution. Its load bound and the scale inequality give loads at most ell*x/k, contradicting the proved sparse-route obstruction. The remaining branch gives exactly the projected cut shores and separator cost bound.