The Query Complexity of Envy-Free Division: Cake, Chores, and Mixed Resources

Alireza Farhadi, Mohammadtaghi Hajiaghayi

cs.GT Nov 8, 2026 · v2

formalization mathlib economics combinatorics

Read PDF arXiv abstract Code

TL;DR

An accompanying Lean 4 artifact built on Mathlib formalizes the paper's four main query-complexity theorems on envy-free division.

Abstract

We study the query complexity of envy-free division for cake, chores, and resources with both positive and negative values. For arbitrary nonnegative nonatomic chore costs, we give a deterministic exact protocol using $2^{n\log_2 n+O(n)}$ queries and cuts. For both cake and chores, a Las Vegas protocol uses $O(n^{12}\log(2n))$ expected queries and $O(n^{11}\log(2n))$ expected cuts. Conversely, every exact protocol with fixed positive success probability requires $Ω(n^2)$ expected queries in general, even with arbitrarily many output cuts at no query cost. For mixed cake and chores, no uniform finite expected-query bound exists even when every Cut returns the leftmost root or every Cut returns the rightmost root. This holds for any fixed positive multiplicative approximation factor and success probability, already when all net totals are one. An additive impossibility holds on the same normalized domain.

Problem

The paper studies how many Robertson–Webb Eval/Cut queries are needed to compute exactly envy-free allocations of cake, of chores, and of mixed resources with signed valuations. It asks how far existing bounds can be lowered, what randomization achieves for chores, and whether bounded-query guarantees extend to signed valuations.

Approach

For chores, a deterministic protocol uses deferred compensation. Packages of partial allocations are combined through Offset SubCore calls, and a capacity-based accounting argument bounds package weights. A Las Vegas protocol handles both cake and chores, and the lower bounds use measurable randomized-protocol arguments. The four main results are formalized in Lean 4.35.0 with Mathlib and a fixed-point library.

Results

The deterministic chore protocol uses 2^{n log2 n + O(n)} queries. The Las Vegas protocol uses O(n^12 log(2n)) expected queries and O(n^11 log(2n)) expected cuts, improving on the prior Õ(n^30) for cake. Any exact protocol with fixed positive success probability needs Ω(n^2) expected queries, and for mixed resources no uniform finite expected-query bound exists.

Setting	Prior benchmark	This paper
Deterministic exact chores	Bounded function of n	Q,C ≤ 2^{n log2 n + O(n)}
Randomized exact cake	E[Q] = Õ(n^30)	E[Q] = O(n^12 log(2n)), E[C] = O(n^11 log(2n))
Randomized exact chores	Bounded expected queries	Same polynomial bounds as cake
Exact lower bounds	Ω(n^2) deterministic cake queries	E[Q] ≥ max{n(np−1)/2, n^2 p/4 − 1}

Comparison with prior bounds

Papers With

The Query Complexity of Envy-Free Division: Cake, Chores, and Mixed Resources