发表机构
University of Toronto; Tsinghua University（多伦多大学; 清华大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文构造了一个无向多播网络反例，证明网络编码可超越分数路由，并推广至无限网络族，且已在Lean中形式化验证。
AI 中文摘要
网络编码允许网络中的节点对消息进行组合，而不仅仅是转发消息。在无向网络中，一条边的两个方向共享其容量，Li和Li在2004年猜想编码相对于分数路由没有优势；该猜想已在许多特殊类别中得到证实，但从未在一般情况下得到解决。在本文中，我们通过构造一个具有单位共享边容量、最大度为三、且具有不同叶子终端的有限连通简单无向网络来反驳该猜想，在该网络上，一个二元线性分组码实现了严格高于最大分数路由速率的公共速率。该构造将一个短完成时间码转化为一个可逆电路，其寄存器全部携带独立消息，其导线上的时间度量产生了严格的路由界限。底层整数系数构造适用于每个有限域和每个非平凡有限阿贝尔群；对于确定性固定调度码，公共速率上确界为1，速率区域的闭包是单位立方体。通过保度张量构造和偶数细分放大差距，对于每个$0<\beta<1$，我们得到一个无界族的连通、简单、次三次、二分网络，其围长至少为$n^\beta$，在这些网络上编码速率接近1，而路由速率受$K_\beta/(\log n)^c$限制，其中正指数$c$与$\beta$无关。有限反例和族定理已在Lean中形式化。
英文摘要
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.
Comments17 pages
