Network Coding Can Beat Routing in Undirected Multiple-Unicast Networks
Xindan Zhang, Baochun Li, Zongpeng Li
cs.IT
Oct 7, 2026 · v1
TL;DR
The finite counterexample and the amplified family theorem are formalized in Lean 4 with Mathlib, using only the standard axioms; the proofs are in a public repository.
Abstract
Network coding lets the nodes of a network combine messages rather than merely forward them. In undirected networks, where the two directions of an edge share its capacity, Li and Li conjectured in 2004 that coding offers no advantage over fractional routing; the conjecture has been confirmed for many special classes but never settled in general. In this paper, we disprove it by constructing a finite connected simple undirected network with unit shared edge capacities, maximum degree three, and distinct leaf terminals, on which a binary linear block code achieves a common rate strictly above the maximum fractional routing rate. The construction turns a short completion-time code into a reversible circuit whose registers all carry independent messages, and a temporal metric on its wires yields the strict routing bound. The underlying integer-coefficient construction works over every finite field and every nontrivial finite abelian group; for deterministic fixed-schedule codes the common-rate supremum is one and the closure of the rate region is the unit cube. Amplifying the gap with a degree-preserving tensor construction and an even subdivision gives, for every $0<β<1$, an unbounded family of connected, simple, subcubic, bipartite networks with girth at least $n^β$ on which coding approaches rate one while routing is bounded by $K_β/(\log n)^c$, with one positive exponent $c$ independent of $β$. The finite counterexample and the family theorem are formalized in Lean.
Problem
Li and Li conjectured in 2004 that network coding gives no advantage over fractional routing in undirected multiple-unicast networks with shared edge capacities. The conjecture had been confirmed for special classes but never settled in general.
Approach
A short completion-time auxiliary code is compiled into a reversible circuit whose registers all carry independent unicast demands. A temporal metric on the circuit's wires gives a strict fractional routing bound below one, while a one-use pipelined binary linear code approaches rate one. The gap is amplified by a degree-preserving tensor construction and made bipartite with high girth by even subdivision. Both main theorems are formalized in Lean with Mathlib.
Results
The paper disproves the conjecture with a finite connected simple subcubic network with leaf terminals on which binary linear coding beats routing. For every 0<β<1 there are unbounded families of bipartite networks with girth at least n^β where coding approaches rate one and routing is at most K_β/(log n)^c. The Lean development has 2,472 declarations and uses only the standard axioms.