Theorem · version 2
There is a seven-vertex, nine-arc directed single-source network with demands 15, 10 and 15 and a feasible fractional flow of cost 58 such that every unsplittable routing satisfying load_P(a) ≤ x(a) + 15 on every arc costs at least 60.
A finite exhaustive path-choice witness. The source contains four capacity-allowed routings, so the cost gap is not vacuous.
In Cost-preserving unsplittable flow · publication v6
The schematic shows the idea. The exact arc data, fractional routing and path enumeration are in the linked Isabelle and Lean sources; this summary is not an executed network certificate.
Fractional cost 58 versus unsplittable cost 60 →In Cost-preserving unsplittable flow · publication v9
7 vertices and 9 arcs. Each demand takes one complete path. The fractional routing costs 58; the allowed extra load on each arc is 15.
The minimum cost among allowed path combinations is 60.
Routing cost: 60. Within every arc’s load allowance.
| Arc | Fractional load | Selected load / limit | Unit cost / cost |
|---|---|---|---|
| s → t1 | 10 | 15 / 25 | 2 / 30 |
| s → t2 | 6 | 10 / 21 | 3 / 30 |
| s → u | 24 | 15 / 39 | 0 / 0 |
| u → t3 | 10 | 0 / 25 | 2 / 0 |
| u → v | 14 | 15 / 29 | 0 / 0 |
| v → t1 | 5 | 0 / 20 | 0 / 0 |
| v → w | 9 | 15 / 24 | 0 / 0 |
| w → t2 | 4 | 0 / 19 | 0 / 0 |
| w → t3 | 5 | 15 / 20 | 0 / 0 |
| Paths | Cost | Load allowance |
|---|---|---|
s → t1; s → t2; s → u → t3 | 90 | Allowed |
s → t1; s → t2; s → u → v → w → t3 | 60 | Allowed |
s → t1; s → u → v → w → t2; s → u → t3 | 60 | Allowed |
s → t1; s → u → v → w → t2; s → u → v → w → t3 | 30 | Exceeded |
s → u → v → t1; s → t2; s → u → t3 | 60 | Allowed |
s → u → v → t1; s → t2; s → u → v → w → t3 | 30 | Exceeded |
s → u → v → t1; s → u → v → w → t2; s → u → t3 | 30 | Exceeded |
s → u → v → t1; s → u → v → w → t2; s → u → v → w → t3 | 0 | Exceeded |
t1: 10 units along s → t1; 5 units along s → u → v → t1.
t2: 6 units along s → t2; 4 units along s → u → v → w → t2.
t3: 10 units along s → u → t3; 5 units along s → u → v → w → t3.
Arithmetic from the cited finite network. This explorer is not an execution of the external Isabelle or Lean proofs.
The schematic shows the idea. The exact arc data, fractional routing and path enumeration are in the linked Isabelle and Lean sources; this summary is not an executed network certificate.
Proved
Fractional cost 58; maximum demand 15; allowed unsplittable cost at least 60.
Source dated Jul 22, 2026 · Observed Oct 13, 2026
Replaces an earlier source assessment. Version history ↓
Proved
Rational and real instance; exact congestion-constrained optimum 60.
Source dated Aug 1, 2026 · Observed Oct 13, 2026
Replaces an earlier source assessment. Version history ↓
Complete formal proof reported externally
This exact lower-bound endpoint is combined with the theory’s explicit graph realization, fractional feasibility and cost-58 lemmas. It proves a cost of at least 60 under the non-strict additive allowance, rather than by itself specifying the full network. It is an Isabelle/HOL artifact, not a Lean theorem.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Dinitz_Garg_Goemans_Counterexample.bounded_unsplittable_costCommit 80985fd56a4cb63a90176bf4bfe456eaff949bfd
Complete formal proof reported externally
The formal theorem establishes non-vacuity and the exact optimum. The project’s check script reports only standard logical axioms; OpenMath has not run that script.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Submission.optimum_is_sixtyCommit ffba3523f0edd14be3460d039f22a6b98c02fd9e
In this problem · publication v6 · Selected context
Counterexample · Proved
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v9
Counterexample · Proved
Relationship not independently reviewed. This concerns its use in this problem.
A directed seven-vertex, nine-arc instance has fractional cost 58 and no congestion-allowed unsplittable routing of cost below 60.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Arthur Freitas Ramos · David Barros Hulak · Ruy Jose Guerra Barretto de Queiroz · Published · Publication date Jul 22, 2026
Public formal source; execution and statement correspondence are separate checks.
Exact proof source inspected. This digest identifies this file only, not a project build, theorem correspondence or independent reproduction.
Source revision: 80985fd56a4cb63a90176bf4bfe456eaff949bfd. Observed Oct 13, 2026.
The AFP authors credit AI assistance for proof engineering and attribute the July counterexample announcement to Dmitry Rybin.
Cost-counterexample Isabelle theory: 80985fd56a4cb63a90176bf4bfe456eaff949bfd.
The project verifies the rational and real cost conjecture refutations and exact optimum 60 for the displayed instance.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Jason Hickey · Project documentation · Publication date Aug 1, 2026
Public formal source; execution and statement correspondence are separate checks.
Exact proof source inspected. This digest identifies this file only, not a project build, theorem correspondence or independent reproduction.
Source revision: ffba3523f0edd14be3460d039f22a6b98c02fd9e. Observed Oct 13, 2026.
Jason Hickey credits Claude for the verification work and credits Dmitry Rybin’s GPT-5.6 Pro session for the original counterexample.
Cost-counterexample Lean submission: ffba3523f0edd14be3460d039f22a6b98c02fd9e.
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Rational and real instance; exact congestion-constrained optimum 60.
Source dated Aug 1, 2026 · Observed Oct 13, 2026 · Source passage →
Replaces an earlier source assessment; see the original source for its history.
Proved
Fractional cost 58; maximum demand 15; allowed unsplittable cost at least 60.
Source dated Jul 22, 2026 · Observed Oct 13, 2026 · Source passage →
Replaces an earlier source assessment; see the original source for its history.