Proof of `Vertex splitting for the directed flow–cut algorithm` (5th statement)
groundedproofs/Lax263307Proofs/VertexSplitting.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
Instantiate the registered directed uniform algorithm on the split network. Its vertex weights are all one, and its order is twice the original order. The same total solver function and actual RAM guarantee apply to every rational split instance.
Attribution
Lax455465 directed uniform flow–cut theorem; the split construction is from Bonnet–Chang, Lemma 7.