Proof of `Arc-to-path conversion for concurrent flows`

groundedproofs/Lax455465Proofs/ArcToPath.lean · lax-455465

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.

Read the Lean proof on GitHub

Description

Extract simple positive paths by repeated bottleneck subtraction for each off-diagonal commodity. Conservation supplies a path whenever residual supply is positive, even if the residual contains cycles. Each subtraction either finishes the supply or removes a positive arc, giving finite termination. Adding the commodity path flows preserves capacities and the common value.