Proof of `Vertex splitting for the directed flow–cut algorithm` (4th statement)
groundedproofs/Lax263307Proofs/VertexSplitting.lean · lax-263307
What this proof establishes
no assumptions
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
No large-capacity arc crosses a cut smaller than that capacity. Reverse arcs force every inside plus port's minus port inside; graph arcs forbid an edge between the two exclusive shores. Encode each split vertex by its original vertex and port to bound shore sizes by twice the corresponding original shore sizes.
Attribution
Bonnet–Chang, cut projection in Lemma 7.