A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture

Dinitz, Garg, and Goemans proved that a feasible fractional single-source flow can be rounded to an unsplittable flow with additive congestion bounded by the largest demand. Goemans conjectured that the rounding can simultaneously preserve cost. This entry verifies the finite counterexample announced by Dmitry Rybin in July 2026. It defines a generic finite path-flow model and realizes the displayed instance as a directed graph with seven vertices, nine arcs, and three terminal demands. Isabelle classifies every source-to-terminal path and checks a feasible fractional flow of cost \(58\) that saturates every arc. The maximum demand is \(15\). Any unsplittable routing whose load on every arc is at most the fractional load plus \(15\) must choose at least two positive-cost routes, each costing \(30\), and therefore costs at least \(60\). Consequently no cost-preserving rounding exists, even under the weaker non-strict congestion bound.