← back to the atlas

d4-journals-jair-2026-0004 (d4-journals-jair-2026-0004)

Answer: Polynomial-time solvable.

The anchor (named result in the paper)

Theorem 3.7 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe number of queries required to decide the existence of a connected super-proportional allocation for 𝑛 hungry agents with equal entitlements, or to compute such an allocation if it exists, is in Θ(𝑛2).

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given finitely many types \(t\) with rational masses \(\mu_t\) summing to \(1\), and strictly positive normalized rational piecewise-constant densities \(f_{tj}\) on common cake cells \(I_j\) of lengths \(d_j\), decide whether there are masses \(r_{tj}\ge 0\) such that \(\sum_j r_{tj}=\mu_t\), \(\sum_t r_{tj}>0\), and \(\sum_t r_{tj}/f_{tj}<d_j\) for every cell \(j\). This asks whether a unit-mass population of repeated types can receive connected infinitesimal shares whose utility, scaled by population size, is strictly greater than the equal per-capita entitlement.

Packaged proof task (what the prover saw — nothing else)

A society is given by its support: a list of \(\tau\geq 1\) types with positive binary-rational masses \(\mu_t\), where \(\sum_{t=1}^{\tau}\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
The cake \([0,1]\) is partitioned into \(m\geq 1\) consecutive cells \(I_j\) of positive binary-rational lengths \(d_j\), with \(\sum_{j=1}^{m}d_j=1\). Type \(t\) has constant binary-rational density \(f_{tj}>0\) on cell \(I_j\), normalized by \(\sum_{j=1}^{m}d_jf_{tj}=1\). Let \(L\) be the total binary input length.
The decision problem asks whether real masses \(r_{tj}\geq 0\) exist satisfying \(\sum_{j=1}^{m}r_{tj}=\mu_t\) for every type \(t\), and both \(\sum_{t=1}^{\tau}r_{tj}>0\) and \(\sum_{t=1}^{\tau}r_{tj}/f_{tj}<d_j\) for every cell \(j\). Types may split their mass among cells.

Is this mass feasibility problem solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?

For finitely many agents with normalized valuations positive on every interval of positive length and equal entitlements, deciding whether a partition into one interval per agent gives each agent value strictly greater than \(1/n\), and computing such a partition when it exists, require \(\Theta(n^2)\) Robertson–Webb queries. This finite-agent query bound does not classify the mass feasibility problem above.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Result

The problem is polynomial-time solvable. In fact, it has the following exact characterization:

Theorem. A feasible allocation exists if and only if the supported types do not all have the same density vector.

Thus feasibility can be decided by comparing every density vector with that of the first type. The proof also gives a rational feasible allocation whenever one exists.

Identical density vectors imply infeasibility

Suppose \(f_{tj}=f_j\) for every type \(t\) and cell \(j\). If a feasible allocation existed, the strict cell inequalities would give

\( \sum_t r_{tj}<d_jf_j \)

for every \(j\), since \(f_j>0\). Summing these finitely many strict inequalities yields

\( 1=\sum_t\mu_t=\sum_j\sum_t r_{tj}<\sum_jd_jf_j=1, \)

a contradiction.

In particular, instances with \(\tau=1\) or \(m=1\) are infeasible: when \(m=1\), normalization forces every density to equal \(1\).

Different density vectors imply feasibility

Choose types \(a,b\) with different density vectors, and write

\( A_j=f_{aj},\qquad B_j=f_{bj},\qquad \rho_j=B_j/A_j. \)

The ratios \(\rho_j\) cannot all equal one constant \(c\). Otherwise \(B_j=cA_j\) for every \(j\), and normalization would imply

\( 1=\sum_jd_jB_j=c\sum_jd_jA_j=c, \)

contradicting the choice of different density vectors. Consequently, there are cells \(p,q\) with \(\rho_p<\rho_q\). Set \(\Delta=\rho_q-\rho_p>0\).

A positive allocation saturating every cell

Define the initial allocation by

\( r^0_{tj}=\mu_t d_j f_{tj}. \)

Every entry is positive. Normalization gives the required type totals:

\( \sum_jr^0_{tj}=\mu_t\sum_jd_jf_{tj}=\mu_t. \)

For every cell, its initial load is exactly its length:

\( \sum_t\frac{r^0_{tj}}{f_{tj}}=d_j\sum_t\mu_t=d_j. \)

We will perturb this allocation while preserving all type totals and reducing every cell load.

A perturbation reducing every cell load

Define \(x_p=1\), \(x_q=-1\), and \(x_j=0\) for all other cells. Define

\( y_j=-\rho_jx_j-\Delta d_jB_j. \)

Both perturbation vectors have zero sum. For \(x\) this follows directly from its definition. For \(y\), normalization of type \(b\) gives

\( \sum_jy_j=-(\rho_p-\rho_q)-\Delta\sum_jd_jB_j=\Delta-\Delta=0. \)

Moreover, in each cell,

\( \frac{x_j}{A_j}+\frac{y_j}{B_j} =\frac{x_j}{A_j}-\frac{\rho_jx_j}{B_j}-\Delta d_j =-\Delta d_j, \)

where the cancellation uses \(\rho_j=B_j/A_j\).

Thus adding a positive multiple of \(x\) to type \(a\)'s allocation and the same multiple of \(y\) to type \(b\)'s allocation preserves their total masses and strictly reduces every cell load.

Choosing the perturbation size

To retain positivity, choose the positive rational number

\( \eta=\min\left\{1,\ \min_j\frac{r^0_{aj}}{2(1+|x_j|)},\ \min_j\frac{r^0_{bj}}{2(1+|y_j|)}\right\}. \)

Set

\( r_{aj}=r^0_{aj}+\eta x_j,\qquad r_{bj}=r^0_{bj}+\eta y_j, \)

and leave every other type's allocation unchanged.

For every cell,

\( |\eta x_j| \leq\frac{r^0_{aj}|x_j|}{2(1+|x_j|)} <\frac{r^0_{aj}}2, \)

and similarly \( |\eta y_j|<r^0_{bj}/2 \). Hence every resulting entry \(r_{tj}\) remains strictly positive. In particular, every cell receives positive total mass.

The zero sums of \(x\) and \(y\) preserve all type totals. Finally, the cell loads satisfy

\( \sum_t\frac{r_{tj}}{f_{tj}} =d_j+\eta\left(\frac{x_j}{A_j}+\frac{y_j}{B_j}\right) =d_j-\eta\Delta d_j<d_j, \)

because \(\eta,\Delta,d_j\) are all positive. This verifies every feasibility requirement.

Algorithm and binary complexity

For decision, compare \(f_{tj}\) with \(f_{1j}\) for every \(t,j\). Return infeasible if all comparisons are equal, and feasible otherwise. This requires at most \(m(\tau-1)\) exact rational comparisons, each taking polynomial time in \(L\).

For construction, choose a differing pair of types and apply the formulas above. They use polynomially many rational arithmetic operations and comparisons. Each computed quantity has polynomial binary length: its formula uses a bounded number of arithmetic operations on input rationals, and taking a minimum selects an existing candidate without enlarging its representation. The resulting rational allocation therefore has polynomial output length and is computable in polynomial time in \(m,\tau,L\).

This conclusion follows directly from the mass constraints; the finite-agent Robertson–Webb query bound is not needed.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

The prover’s claim is correct. The characterization, construction, and polynomial-time complexity argument all hold under the stated hypotheses. No major or minor mathematical issues were found.

When \(f_{tj}=f_j>0\), multiplying each strict load inequality by \(f_j\) gives
\[ \sum_t r_{tj}<d_jf_j. \]
Summing over the finitely many cells preserves strictness. The row constraints and normalization then give the asserted contradiction \(1<1\). This argument correctly applies to real allocations and does not require the positive-cell-mass condition.

The stated edge cases are also correct. For \(\tau=1\), all supported density vectors are identical. For \(m=1\), the length condition gives \(d_1=1\), and normalization forces \(f_{t1}=1\) for every type.

The chosen types \(a,b\) are distinct. Every ratio \(\rho_j=B_j/A_j\) is well-defined and positive because the input densities are strictly positive.

If all ratios were a common constant \(c\), normalization of both types would force \(c=1\), making their density vectors identical. Thus the ratios are not constant, and distinct cells \(p,q\) with \(\rho_p<\rho_q\) exist. In particular, \(\Delta>0\). All hypotheses used here are explicitly supplied by the task.

Every entry \(r^0_{tj}=\mu_td_jf_{tj}\) is strictly positive. The two displayed calculations correctly establish the row totals and exact saturation of every cell:
\[ \sum_jr^0_{tj}=\mu_t, \qquad \sum_t\frac{r^0_{tj}}{f_{tj}}=d_j. \]
The first uses normalization of each type; the second uses normalization of the society’s masses.

Since \(p\ne q\), the definition of \(x\) gives \(\sum_jx_j=0\). For \(y\), the computation is correct:
\[ \sum_jy_j =-\rho_p+\rho_q-\Delta\sum_jd_jB_j =\Delta-\Delta=0. \]
This uses precisely the normalization of type \(b\).

The cellwise cancellation is also exact:
\[ \frac{x_j}{A_j}+\frac{y_j}{B_j}=-\Delta d_j. \]
It holds for every cell, including cells outside \(\{p,q\}\). Thus both modified rows retain their totals, while every cell’s load decreases strictly for any positive perturbation size.

Every candidate in the definition of \(\eta\) is a positive rational number. The minimum is over a finite, nonempty set, so \(\eta\) is positive and rational.

For each cell, the stated bound follows directly from the corresponding candidate in that minimum:
\[ |\eta x_j| \leq\frac{r^0_{aj}|x_j|}{2(1+|x_j|)} <\frac{r^0_{aj}}2. \]
The strict inequality remains valid when \(x_j=0\). The same reasoning applies to \(y_j\). Consequently, both modified rows remain strictly positive, and the unchanged rows were already strictly positive. Every cell therefore receives positive total mass.

Finally, the computed load \(d_j-\eta\Delta d_j\) is strictly below \(d_j\). Together with positivity and preserved row totals, this verifies every feasibility requirement.

Comparing every density vector against the first implements the proved characterization exactly. The number of rational comparisons is at most \(m(\tau-1)\), and exact comparison has polynomial bit complexity.

The construction uses polynomially many rational operations. The bit-length argument is valid for these particular formulas: each candidate quantity depends on a bounded number of arithmetic operations on input rationals, the minimum selects one existing candidate, and each output entry uses only bounded further arithmetic. There is no unbounded chain of arithmetic operations that could invalidate the stated size bound. The allocation therefore has polynomial binary output length and can be computed in polynomial time.

The proof invokes no external theorem requiring additional verification. It correctly keeps the finite-agent Robertson–Webb query statement separate from this mass feasibility problem.

No additional clarification or repair is needed.

⟨structured verdict parsed — rendered above⟩

Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.