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.
Assumptions
The exact rational network and costs specified in the cited formal sources.
Non-strict upper congestion allowance measured from the fractional arc load.
Scope
A finite exhaustive path-choice witness. The source contains four capacity-allowed routings, so the cost gap is not vacuous.
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 loads and costs for this routing
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
All 8 path combinations & the fractional split
All path combinations
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.
Construction details
Network size
Seven vertices and nine directed arcs
Terminal demands
15, 10, 15; largest demand 15
Fractional cost
58
Allowed routing cost
At least 60 with the non-strict additive load allowance x(a) + 15
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.
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 loads and costs for this routing
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
All 8 path combinations & the fractional split
All path combinations
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.
Construction details
Network size
Seven vertices and nine directed arcs
Terminal demands
15, 10, 15; largest demand 15
Fractional cost
58
Allowed routing cost
At least 60 with the non-strict additive load allowance x(a) + 15
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.
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
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