Proof of `Projecting split paths and preserving endpoint loads` (3rd statement)
groundedproofs/Lax263307Proofs/SplitPathProjection.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
A positive-flow path uses only positive-capacity arcs: every used arc's positive contribution is bounded by its total load, hence by its capacity. The registered flow predicate also supplies path simplicity. Apply the split-path projection theorem to paths with the retained split endpoints.
Attribution
Bonnet–Chang, flow projection in Lemma 7.