A Lean Certificate for the Single Source Unsplittable Flow Cost Counterexample

The cost question and the certified result

In single-source unsplittable flow, a terminal’s entire demand must be sent along one path from a common source. Dinitz, Garg, and Goemans established a rounding theorem with additive congestion bounded by the largest demand [2]. The cost-enhanced conjecture attributed to Goemans additionally asks that the rounded flow cost no more than the given fractional flow. We use the explicit formulation in Traub, Vargas Koch, and Zenklusen, Conjecture 1.3 [11]. The 1999 paper is background for the congestion theorem; it is not used here as a source for the wording of the cost conjecture.

For the positive-demand subcase sufficient here, take a finite directed graph $G=(V,A)$, source $s$, distinct terminals $t_k$ different from $s$, positive demands $d_k$, a feasible nonnegative fractional flow $x$, and nonnegative per-unit arc costs $c_a$, put $D=\max_k d_k$. The existential cost-preserving assertion is that paths $P_k$ from $s$ to $t_k$ can be selected so that, for every arc,

Conjecture 1.3 also asserts polynomial-time computation. Refuting its existential part suffices to refute that stronger claim, without formalizing a computational model. The cited formulation permits zero demands; our witness satisfies the stricter positivity condition of the Lean interface. A strict variant replaces the first inequality by $y_a<x_a+D$. We call the two bounds weak and strict only to distinguish $\le$ from $<$; the cited cost conjecture uses $\le$.

Rybin announced the counterexample on July 22, 2026, and made the discovery session public [9, 8]. The same finite certificate is formalized in Isabelle/HOL in the Archive of Formal Proofs (AFP) by Ramos, Hulak, and de Queiroz [6]. The Lean repository discussed here is a separate reimplementation [7], not a translation imported from Isabelle. Other Lean

Copyright 2026 the authors. Licensed under Creative Commons Attribution 4.0 International (CC BY 4.0). verifications by Jason Hickey and by DiscreteAlias are also publicly available [4, 3]. We make no priority claim relative to these developments and no claim to discovery.

All references to the present Lean source mean revision cc7284cf415fc2a773f00d400319ef39663c277a. The seven selected declarations are registered in Palomar as PALOMAR-2026-08-29-000003, version 1 [5]. The mathematical core is the following finite statement.

Theorem 1.1. There is a seven-vertex, nine-arc single-source instance with three demands and a feasible fractional flow $x$ of cost 58, with $D=15$, such that every unsplittable routing satisfying $y_a \le x_a+15$ on every arc has cost at least 60. Consequently neither the weak cost-preserving assertion nor its strict variant holds universally.

The selected formal theorem proves this over $\mathbb{Q}$. Its graph-path classification ensures that the finite route model covers every source-to-terminal path in the actual graph. The corresponding real-valued counterexample follows from the same integer data and finite inequalities. That interpretation is explained below; a general rational-to-real transfer theorem is not part of this snapshot.

The finite path flow interface

The generic structure PathFlowInstance has commodity, route, and arc carrier types $K,R,A$. It records an admissibility predicate $\operatorname{Adm}(k,r)$, demands $d_k \in\mathbb{Q}$, capacities $u_a \in\mathbb{Q}$, costs $c_a \in\mathbb{Q}$, and an incidence predicate $U(k,r,a)$. The generic interface is an abstract incidence model: graph endpoints and path validity are established separately for the concrete witness. With finite $K$ and $R$, fractional route amounts $f_{kr}$ induce

The latter sum requires finite $A$. The maximum demand additionally requires nonempty $K$ and is the maximum of the finite demand image.

Definition 2.1. An instance is well formed if every demand is positive, every commodity has an admissible route, and every capacity and cost is nonnegative. A fractional routing $f$ is feasible if the instance is well formed, $f_{kr}\ge0$, inadmissible routes have amount zero, $\sum_r f_{kr}=d_k$ for every $k$, and $x_a(f)\le u_a$ for every $a$.

An unsplittable routing is a function $q:K\to R$ with $\operatorname{Adm}(k,q(k))$ for every $k$. Its arc load and cost are

The definitions weakDggRounding and strictDggRounding combine admissibility, the corresponding congestion inequality relative to $x(f)$, and $C(q)\le C(f)$. Their existential versions quantify over $q$. The reference load is the specified fractional flow, not an arbitrary capacity upper bound. In this witness $x_a(f)=u_a$ on every arc, so the two numerical formulations coincide.

The finite universal negation in the registered theorem uses the specific carrier types with three commodities, two route choices, and nine arcs. It is already enough to contradict an assertion quantified over all graph instances, because the witness is realized by a genuine graph and its routes are exhaustive. The code does not establish a generic equivalence between arbitrary incidence structures and graphs.

The graph and the fractional witness

Let

The directed arcs and all numerical data are given in Table 1. Figure 1 draws the same endpoint relation. The terminal vertices have no outgoing arcs. The ordering $s,u,v,w,t_1,t_2,t_3$ places every arc forward, so the graph is acyclic. All endpoints are distinct on each arc, and no ordered endpoint pair is repeated. These observations are immediate properties of the data; separate generic graph simplicity or acyclicity theorems are not selected in this formalization.

Arc $a$	Capacity $u_a$	Fractional load $x_a$	Unit cost $c_a$
$s \to t_1$	10	10	2
$s \to t_2$	6	6	3
$s \to u$	24	24	0
$u \to v$	14	14	0
$u \to t_3$	10	10	2
$v \to t_1$	5	5	0
$v \to w$	9	9	0
$w \to t_2$	4	4	0
$w \to t_3$	5	5	0

For each terminal there is one paid route $E_k$ and one free route $Z_k$:

Here vertex lists abbreviate the consecutive directed arcs. The names paid and free refer to total route cost, not to disjointness: $E_3$ and $Z_3$ both use $s \to u$.

Lemma 3.1. Every directed source-to-$t_k$ path is exactly $E_k$ or $Z_k$.

Proof. From $w$ a nonempty path goes directly to $t_2$ or $t_3$ and then stops. From $v$ it goes to $t_1$ or to $w$; from $u$ it goes to $t_3$ or to $v$; from $s$ it goes to $t_1$, $t_2$, or $u$. Following these alternatives gives precisely the six displayed terminal paths. There are no additional continuations from any terminal. $\square$

The formal predicate edgePath is recursive on a list of arcs. It checks each tail against the current vertex, advances to the head, and accepts the empty list exactly when the current and final vertices agree. It does not assume vertex simplicity. The proof classifies all such lists from each terminal, then from $w,v,u,s$, and obtains allSourceTerminalPaths. Thus no longer walk, omitted splice, or additional source-to-terminal route escapes the two-choice model.

The fractional route amounts are

$k$	$f_{k,E_k}$	$f_{k,Z_k}$	$d_k$
1	10	5	15
2	6	4	10
3	10	5	15

They are all nonnegative and meet the three demands. Summing their incidences gives Table 1, proving feasibility and saturation. For example the backbone loads are $5 + 4 + 10 + 5 = 24$ on $s \to u$, $5 + 4 + 5 = 14$ on $u \to v$, and $4 + 5 = 9$ on $v \to w$. As an arc-flow check, the source outflow is $10 + 6 + 24 = 40$; conservation at $u,v,w$ is respectively $24 = 14 + 10$, $14 = 5 + 9$, and $9 = 4 + 5$. The terminal inflows are 15, 10, 15. Only three arcs have positive cost, so

The corresponding Lean facts are fractionalLoadEqCapacity, splitFlowFeasible, fractionalCostValue, and counterexampleMaximumDemand.

The obstruction to cost preserving rounding

Let $z_k$ be 1 if $q$ selects $Z_k$, and 0 if it selects $E_k$. Every paid route contributes 30: its cost is respectively $15 \cdot2$, $10 \cdot3$, or $15 \cdot2$. Every free route contributes zero. Hence

The crucial shared-arc loads are

The constant 15 in $y_{su}$ comes from terminal $t_3$ on either route.

Lemma 4.1. If $y_a(q) \le x_a + 15$ on every arc, then at most one free route is selected, and at least two paid routes are selected.

Proof. If $Z_1,Z_2$ are selected, then $y_{su} = 40 > 24 + 15 = 39$. If $Z_1,Z_3$ are selected, then $y_{uv} \ge30 > 14 + 15 = 29$. If $Z_2,Z_3$ are selected, then $y_{vw} = 25 > 9 + 15 = 24$. Any selection of at least two free routes contains one of these pairs, so it violates a congestion inequality. $\square$

Proof of Theorem 1.1. The preceding fractional witness is feasible and has cost 58. By Lemma 3.1, every unsplittable graph routing is represented by the three binary choices. Lemma 4.1 and (5) give $C(q) \ge60 > 58$ for any weakly bounded routing. Thus no routing can satisfy both inequalities in (1). A strict congestion bound implies the weak bound, so the strict cost-preserving assertion fails as well. $\square$

Table 2 is an exhaustive numerical cross-check. Its excess column means $\max_a(y_a-x_a)$, so weak congestion feasibility is exactly excess at most 15. All four feasible assignments actually have excess strictly below 15. This also shows that the obstruction is the cost requirement, rather than a lack of any bounded routing.

$t_{1}$	$t_{2}$	$t_{3}$	Cost	Maximum excess	Bound $\le15$
$E_{1}$	$E_{2}$	$E_{3}$	90	5	Yes
$E_{1}$	$E_{2}$	$Z_{3}$	60	10	Yes
$E_{1}$	$Z_{2}$	$E_{3}$	60	6	Yes
$E_{1}$	$Z_{2}$	$Z_{3}$	30	16	No
$Z_{1}$	$E_{2}$	$E_{3}$	60	10	Yes
$Z_{1}$	$E_{2}$	$Z_{3}$	30	16	No
$Z_{1}$	$Z_{2}$	$E_{3}$	30	16	No
$Z_{1}$	$Z_{2}$	$Z_{3}$	0	26	No

For example $(E_1,E_2,Z_3)$ has loads, in the arc order of Table 1,

Every load is strictly below $x_a+15$, and its cost is 60. Thus 60 is the exact minimum under either congestion reading. This attainment check and the full table are elementary consequences of the displayed data; the pinned selected Lean result asserts the lower bound, not a separately packaged optimum-attainment theorem. The all-free routing has cost zero and maximum excess 26, illustrating that cost alone is also satisfiable. The example makes no claim against rounding guarantees allowing larger additive error, such as $2D$.

The Lean proof and its verification boundary

The development uses Lean 4 [1] and Mathlib [10]. The graph, route lists, rational amounts, loads, and predicates are in Definitions.lean. The substantive proofs are in Proof.lean. Finite carrier instances explicitly list the three commodities, two route choices, and nine arcs. This permits finite sums to simplify to exact rational expressions.

Path completeness is proved structurally, not stipulated by making all binary choices admissible. In the concrete instance both choices are declared admissible, but routeEdgesValid proves their graph validity and allSourceTerminalPaths proves completeness for arbitrary arc lists. This separation is essential: an incidence-table counterexample would otherwise leave open whether the real graph admits an unlisted cheap routing.

The arithmetic proof first identifies the finite universes. It uses simp and norm_num for well-formedness, demand sums, capacity saturation, maximum demand, and fractional cost. The three backbone-load formulas and unsplittableCostEqPaidCount are proved by cases on the three route choices. In boundedRoutingHasTwoPaid, the hypotheses for $s \to u$, $u \to v$, $v \to w$ are extracted; each of the eight cases reduces to rational arithmetic, and linarith closes the impossible ones. Coercing the paid-count bound to $\mathbb{Q}$ yields boundedUnsplittableCost. The remaining witness and universal negations instantiate the property at the concrete instance and combine $60 \le C(q) \le58$.

The statement surface Challenge.lean repeats the definitions and states seven targets with deliberate sorry bodies. It is an interface for statement comparison, not the completed proof. Solution.lean imports DinitzGargGoemans.Proof, whose import chain goes through Definitions rather than Challenge. The inspected implementation files contain no sorry, admit, native_decide, or custom axiom declaration. A textual inspection by itself does not establish the transitive axiom footprint.

The pinned comparator configuration selects the seven theorems named in the registry and ten load, cost, feasibility, rounding, and witness definitions. It permits only propext, Quot.sound, and Classical.choice, and enables NanoDa checking. The registry records successful historical mechanical verification on August 28, 2026, under Lean v4.33.0; the Mathlib manifest resolves to db584cd6d46c92f209a44c0f1c829460d327499d. Its linked workflow is run 33131019615 [5]. These are historical verification records, not a new kernel or comparator run performed during manuscript preparation.

The boundary of the formal result is therefore explicit. It is a finite rational counterexample with exhaustive graph-path coverage and exact cost separation. Interpretation as an ordinary real-valued graph-flow counterexample uses the same integer incidence and arithmetic, and does not require choosing any irrational route amounts: the routing domain is still the same eight assignments. Source alignment, the conjecture’s historical attribution, and prose claims about other work are scholarly judgments outside the Lean kernel. The development does not formalize the general Dinitz–Garg–Goemans theorem, algorithmic complexity, parameterized counterexample families, or every published variant of the cost conjecture.

Provenance and reproducibility

This manuscript is a new exposition of the pinned Lean certificate. The counterexample is credited to Rybin and the GPT-5.6 Pro session he published; the prior AFP proof document remains a separate Isabelle artifact [8, 6]. No prior proof-document text or figure is reproduced here. The data tables and diagram were prepared from the inspected Lean definitions, with an independent exact-arithmetic enumeration used as a numerical cross-check. A matching enumeration is not a substitute for formal theorem verification.

The repository metadata records GPT-5 agent assistance for the historical Lean proof engineering. The present manuscript was generated primarily with OpenAI GPT-6.1 assistance for exposition, source comparison, bibliographic research, and typesetting. Arthur Freitas Ramos directed the submission and reports understanding some parts of the manuscript. No comprehensive personal line-by-line review by Arthur, or complete understanding by every listed author, is claimed. Model-assisted manuscript checks should not be read as independent human peer review.

The referenced Lean repository is licensed Apache 2.0, and the AFP entry has a BSD license. Those artifact licenses remain distinct from this manuscript’s CC BY 4.0 license. The source archive for this article contains only its LaTeX source and bibliography; it does not bundle the Lean project or the prior Isabelle document. The immutable source and registry references identify the formal artifact needed to inspect or independently reproduce the mathematical verification.

References