d4-conf-sagt-2018-0017 (d4-conf-sagt-2018-0017)

Given four types \(T\), rational masses \(\mu_t>0\) summing to \(1\), and one normalized, additive, divisible valuation oracle \(v_t\) per type over \([0,1]\), can a Robertson–Webb protocol output bundles \(X_t\) that are finite unions of intervals, satisfy \(v_t(X_t)\ge v_t(X_s)\) for all \(t,s\), and meet \(\sum_t \mu_t \mathbf{1}_{X_t}(x)\le 1\) almost everywhere, using at most \(61\) cut queries and \(110\) evaluation queries? Theorem 1’s protocol answers this: its four output bundles partition the cake.

A society is given by its support: a list of \(\tau=4\) types with positive binary rational masses \(\mu_t\) summing to \(1\); \(\tau\) counts supported types, not possible types. Let \(L\) be the total bit length of the masses. Each type has a nonnegative, normalized, additive, divisible valuation on finite unions of intervals in \([0,1]\), accessed through the Robertson–Webb model.
Output bundles \(X_t\), each a finite union of intervals, with \(\bigcup_t X_t=[0,1]\), satisfying \(v_t(X_t)\ge v_t(X_s)\) for every \(t,s\) and \(\sum_t\mu_t\mathbf{1}_{X_t}(x)\le1\) almost everywhere. Overlaps are permitted subject to this capacity constraint. Preferences are weak; equality satisfies envy-freeness. Measure oracle complexity by cut and evaluation queries, and any additional computational complexity in \(\tau,L\); there is no candidate parameter \(m\).

Can a Robertson–Webb protocol always produce such bundles using at most \(61\) cut queries and \(110\) evaluation queries, or must some instances exceed one of these budgets?

For four individual agents, a verified algorithm produces a complete envy-free partition within these query budgets ([Amanatidis et al.](https://arxiv.org/pdf/1807.00317)). Its guarantee also settles the stated mass problem, since its output satisfies the specified coverage and capacity conditions; consequently this target is already closed.

Conclusion

Yes. A Robertson–Webb protocol always suffices within \(61\) cut queries and \(110\) evaluation queries. No instance forces either budget to be exceeded.

Literally, the stated conditions even permit the zero-query allocation \(X_t=[0,1]\) for every type: all compared values equal \(1\), and the capacity sum equals \(\sum_t\mu_t=1\). The stronger, intended conclusion also holds: these budgets suffice for a complete envy-free partition.

Published theorem and hypothesis checks

Theorem 1 of [Amanatidis et al., *An Improved Envy-Free Cake Cutting Protocol for Four Agents*](https://arxiv.org/pdf/1807.00317) guarantees an envy-free allocation using at most \(61\) cut queries and \(110\) evaluation queries. The protocol allocates the entire cake, and each bundle is a finite union of intervals. Its valuation assumptions are normalization, additivity, divisibility, and nonnegativity, exactly as in the task. Its query accounting includes the cost of implementing queries on disconnected residues using interval queries.

Apply this theorem to four agents indexed by the four supported types, with agent \(t\) having valuation \(v_t\). This uses one agent per supported type; the masses do not determine the number of agents. The theorem does not require distinct valuations, and its tie-breaking convention accommodates weak preferences.

Verification of the mass allocation

Let \(P_t\) be the bundle returned for agent \(t\), and output \(X_t=P_t\).

First, each \(X_t\) is a finite union of intervals, and completeness gives \(\bigcup_{t=1}^{4}X_t=[0,1]\).

Second, envy-freeness of the returned allocation gives \(v_t(X_t)\geq v_t(X_s)\) for every pair \(t,s\). These are precisely the required comparisons: the task does not impose a mass-weighted envy condition.

Third, for every point \(x\), nonnegativity of the masses and \(\mathbf{1}_{X_t}(x)\leq1\) imply
\(\sum_{t=1}^{4}\mu_t\mathbf{1}_{X_t}(x)\leq\sum_{t=1}^{4}\mu_t=1\).
Thus capacity holds pointwise, including at interval endpoints.

The reduction adds no cut or evaluation queries. It requires no mass arithmetic; reading the mass encodings takes \(O(L)\) time. With \(\tau=4\) fixed, the protocol has bounded control and exact arithmetic operations in the usual Robertson–Webb model. This is an oracle-model operation count, not a bit-complexity assertion about arbitrary real oracle answers. No candidate parameter \(m\) is needed.

⟨structured verdict parsed — rendered above⟩

The prover resolves the assigned target. The cited theorem applies to the four supported types, and the conversion to a mass allocation preserves every required condition. No major or minor mathematical issue was found.

• The theorem is correctly identified and applicable. Theorem 1 gives the stated bounds for four agents. Section 2 assumes normalized, additive, divisible, nonnegative valuations on finite unions of intervals, matching the task. The protocol produces a complete allocation; the paper also explicitly addresses ties and simulating queries on disconnected residues. [Amanatidis et al., Sections 2–4](https://arxiv.org/pdf/1807.00317)

The prover invokes this published result rather than reproducing its proof. That is sufficient here, especially because USER_TASK explicitly supplies its verified guarantee.

• The four-agent identification is valid. There are exactly \(\tau=4\) supported types. Assigning valuation \(v_t\) to agent \(t\) therefore satisfies the theorem’s agent-count hypothesis. No requirement says that agent multiplicities must encode the masses, or that valuations must be distinct. Weak preferences are compatible with the cited guarantee.

• The output has the required form and coverage. Setting \(X_t=P_t\) transfers the theorem’s finite-union and completeness guarantees directly:

\(\bigcup_{t=1}^{4}X_t=[0,1]\).
The prover does not substitute a partial allocation for the complete output.

• The envy comparisons are exactly those requested. The theorem gives \(v_t(P_t)\geq v_t(P_s)\) for every ordered pair \(t,s\), hence \(v_t(X_t)\geq v_t(X_s)\). The task contains no mass weighting in these comparisons.

• The capacity calculation is correct. For every point \(x\), each indicator lies between \(0\) and \(1\), and each mass is positive. Consequently,

\(\sum_{t=1}^{4}\mu_t\mathbf{1}_{X_t}(x)\leq\sum_{t=1}^{4}\mu_t=1\).
This establishes the required almost-everywhere condition, with the stronger pointwise bound. Shared endpoints cannot invalidate this calculation. Disjointness is unnecessary for this particular inequality.

• The query bounds are preserved and correctly accounted for. Relabeling the four returned bundles adds no oracle queries. The paper’s accounting includes interval-query simulation for disconnected residues. Its final totals check arithmetically:

\(5\cdot9+3\cdot5+1=61\) cut queries and
\(5\cdot15+3\cdot12+1-2=110\) evaluation queries. [Amanatidis et al., Section 4, “Counting Queries”](https://arxiv.org/pdf/1807.00317)

• The additional complexity statement is appropriately qualified. Reading the mass encodings takes \(O(L)\) time. With four agents fixed, the cited finite protocol uses a bounded number of control and exact arithmetic operations in the stated oracle model. The prover explicitly avoids asserting a bit-complexity bound for arbitrary real oracle answers. No candidate parameter is introduced.

• The zero-query observation is correct but supplementary. The proposed \(X_t=[0,1]\) gives coverage, values \(v_t(X_s)=1\) for every pair, and capacity exactly \(1\). Under the task’s intended-reading rule, this observation alone would not substantiate the stronger partition conclusion. The prover separately establishes that conclusion through the applicable theorem, so its answer does not depend on the permissive overlap formulation.

No additional clarification is needed to verify the conclusion. The answer establishes polynomial complexity in the specified oracle-operation model for the fixed support size; it makes no claim about general support sizes or arbitrary-real bit complexity.

⟨structured verdict parsed — rendered above⟩