While this submission is a draft, it cannot be used by other submissions.

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.

Read the Lean proof on GitHub

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.