← All papers
First page of Asymptotically Optimal Weighted Edge Colorings via Local Bin Packing

Asymptotically Optimal Weighted Edge Colorings via Local Bin Packing

Rishikesh Gajjala, Arindam Khan

math.CO Nov 2, 2026 · v1 cs.DM cs.DS
The five upper-bound existence statements for weighted edge coloring are formalized in Lean 4 with Mathlib, AI-assisted, in a companion repository.
We study weighted edge coloring, where each edge of a graph $G$ has a weight in $(0,1]$, and colors are assigned so that the incident weight of each color at every vertex is at most one. The objective is to minimize the number of colors, denoted by $χ'_w(G)$. This generalizes classical edge coloring (all weights are one) and bin packing ($G$ is a star). Two natural lower bounds are the maximum weighted degree $Δ_w(G)$ and the maximum local bin-packing number $\mathrm{bp}(G)$: the maximum, over vertices, of the minimum number of unit bins needed to pack the incident weights. We have $\lceilΔ_w(G)\rceil\le\mathrm{bp}(G)\leχ'_w(G)$. How closely these local lower bounds approximate the global optimum is a longstanding open problem. Our main result establishes an asymptotic weighted analogue of Vizing's theorem: every simple graph admits a coloring using at most $(1+o(1))\mathrm{bp}(G)$ colors. Thus local bin packings can be made globally consistent with asymptotically vanishing relative loss, even in nonbipartite graphs. Our local-to-global rounding framework coordinates feasible local packing distributions into a partial coloring, leaving only $o(\mathrm{bp}(G))$ uncolored weight at every vertex. For bipartite multigraphs, we prove $χ'_w(G)\le(2+o(1))Δ_w(G)$, establishing the Chung–Ross conjecture [SICOMP'91] asymptotically. For loopless multigraphs, we obtain the exact bound $χ'_w(G)\le3\lceilΔ_w(G)\rceil$. Both leading coefficients are optimal, giving weighted analogues of the classical Kőnig–Shannon bounds. Further upper and lower bounds show that the classical factor-$3/2$ separation does not persist with the local bin-packing benchmark. We also disprove the exact weighted-degree conjecture of Feige and Singh [ESA'08]. Our upper bounds have polynomial-time algorithms, and their existence statements are formalized in Lean 4.

Weighted edge coloring assigns colors to edges with weights in (0,1] so that the incident weight of each color at every vertex is at most one, and asks for the minimum number of colors. It was open how closely the local lower bounds, maximum weighted degree Δ_w and local bin-packing number bp(G), approximate this optimum.

A local-to-global rounding framework combines feasible local bin-packing distributions at each vertex into a consistent partial coloring, leaving only o(bp(G)) uncolored weight per vertex, which fresh colors then cover. Further tools are grouping of parallel edges, a skeleton-plus-insertion argument based on Shannon's theorem, and harmonic charges from bin packing. The five existence statements of the main theorem are formalized in Lean 4 and Mathlib with AI assistance; the running-time analyses are not.

Simple graphs need at most (1+o(1))bp(G) colors, bipartite multigraphs at most (2+o(1))Δ_w (the Chung–Ross conjecture, asymptotically), and loopless multigraphs at most 3⌈Δ_w⌉. Improved bin-packing bounds are 1.62 for bipartite and 1.999 for loopless multigraphs, and an explicit counterexample disproves the Feige–Singh exact total-weight conjecture.

Graph classUpper bound
Simple graphs(1+o(1)) bp(G)
Bipartite multigraphs(2+o(1)) Δ_w(G)
Loopless multigraphs3⌈Δ_w(G)⌉
Bipartite multigraphs(1.62+o(1)) bp(G)
Loopless multigraphs(1.999+o(1)) bp(G)
Upper bounds on χ'_w(G) (all formalized in Lean 4)