← back to the atlas

d4-journals-jair-2023-0006 (d4-journals-jair-2023-0006)

Answer: \(\text{Polynomial-time solvable for every fixed }d\)

The anchor (named result in the paper)

Theorem 3 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateSuppose the instance is negative and that agents have linear utility functions for bads and SPLC utility functions for goods. If the number of bads is constant, then we can compute all CE in polynomial time, i.e., for each CE we obtain one with the same utility profile.

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

The continuous mirror question, as graded

Given a finite set of complete types \(T\) with rational masses \(\mu_t>0\), \(\sum_{t\in T}\mu_t=1\), rational per-type budgets \(e_t<0\), and SPLC utilities for goods plus linear disutilities for a fixed number \(d\) of chores, compute competitive equilibria for a negative instance. Each type receives a per-person bundle \(x_t\); item \(j\) has rational supply \(q_j\) per unit of population mass, so market clearing requires \(\sum_{t\in T}\mu_t x_{tj}=q_j\). Find supporting prices and type bundles that maximize each type’s utility subject to its budget, fully spend budgets, and return one equilibrium for each distinct vector of type utilities.

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

A society is given by its support: the list \(T\) of its \(\tau\) complete types with positive binary-rational masses \(\mu_t\), where \(\sum_t\mu_t=1\); \(\tau\) is the support size, not the number of possible types. Each type specifies its utilities and a binary-rational per-person budget \(e_t<0\).
There are \(m\) divisible items with positive binary-rational supplies \(q_j\) per unit population mass. Utilities are normalized SPLC functions \(u_t(x)=\sum_j f_{tj}(x_j)\) on \(\mathbb R_{\ge0}^m\), with \(f_{tj}(0)=0\). Segment slopes and finite lengths are binary rationals; lengths are positive, the final segment is unbounded, and each function has strictly decreasing slopes that are either all positive or all negative.
An item is a good if some type has positive slopes for it; otherwise it is a chore. Exactly \(d\ge1\) items are chores, with \(d\) fixed, and every type's utility for each chore is linear with strictly negative slope. A globally classified good may be disliked by some types.
A feasible allocation assigns one per-person bundle \(x_t\ge0\) to each type and satisfies \(\sum_t\mu_t x_{tj}=q_j\) for every item. Let \(T^+\) contain the types liking at least one item. The instance is promised negative: no feasible allocation gives \(u_t(x_t)\ge0\) for every \(t\in T^+\) and \(u_t(x_t)=0\) for every \(t\notin T^+\).
An equilibrium consists of feasible bundles and prices \(p\in\mathbb R^m\), positive for goods and negative for chores, such that \(p\cdot x_t=e_t\) and \(x_t\in\arg\max\{u_t(y):y\in\mathbb R_{\ge0}^m,\ p\cdot y\le e_t\}\) for every type; any utility-maximizing bundle is allowed.
The computational problem is to return one equilibrium for each distinct type-utility vector \((u_t(x_t))_{t\in T}\). Let \(K\) be the total number of utility segments and \(L\) the total binary input length.

For every fixed \(d\), can this equilibrium-enumeration problem be solved in time polynomial in \(m,\tau,K,L\), or is it NP-hard?

For finite lists of agents, all equilibrium utility profiles can be represented in polynomial time for negative instances with a fixed number of linear chores and SPLC utilities on goods. [Garg, Hoefer, McGlaughlin and Schmalhofer (2023)](https://par.nsf.gov/servlets/purl/10491726)
No result explicitly treating this support-encoded mass formulation was located in the literature search.

Modeling choices made when packaging the task

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

Result

For every fixed \(d\), the problem is polynomial-time solvable in \(m,\tau,K,L\). A change of variables reduces it to a finite market with exactly \(\tau\) agents, preserving equilibrium utility profiles exactly.

1. The finite-market theorem

We use Theorem 3 of [Garg, Hoefer, McGlaughlin and Schmalhofer (2023)](https://par.nsf.gov/servlets/purl/10491726): for a negative finite-agent market with SPLC utilities on globally classified goods, linear utilities on globally classified chores, and a fixed number of chores, one can compute equilibrium representatives covering every equilibrium utility profile in polynomial time.

Their model permits different strictly negative budgets, and an agent may dislike an item globally classified as a good. Its equilibrium definition requires full allocation, full expenditure, and maximization over the entire nonnegative budget set. Thus these aspects agree with the task.

We now verify the remaining hypotheses through an explicit reduction.

2. Constructing the finite market

Create one agent for each \(t\in T\), and give each item unit supply. Define the agent’s budget and utility by

\(\displaystyle b_t=\mu_t e_t,\qquad v_t(z)=\sum_{j=1}^m g_{tj}(z_j),\qquad g_{tj}(a)=f_{tj}\!\left(\frac{q_j}{\mu_t}a\right).\)

For allocations and prices, use the transformations

\(\displaystyle z_{tj}=\frac{\mu_t}{q_j}x_{tj},\qquad r_j=q_jp_j.\)

Their inverses are

\(\displaystyle x_{tj}=\frac{q_j}{\mu_t}z_{tj},\qquad p_j=\frac{r_j}{q_j}.\)

All scaling factors are strictly positive.

If a segment of \(f_{tj}\) has slope \(s_{tjk}\) and finite length \(\ell_{tjk}\), the corresponding segment of \(g_{tj}\) has slope and length

\(\displaystyle \widehat s_{tjk}=\frac{q_j}{\mu_t}s_{tjk},\qquad \widehat\ell_{tjk}=\frac{\mu_t}{q_j}\ell_{tjk}.\)

The final segment remains unbounded. Positive scaling preserves normalization, concavity, strict slope ordering, slope signs, and positive finite lengths. It also preserves linearity on chores. Consequently, the transformed market has exactly the same globally classified goods and exactly \(d\) chores, and its segment count remains \(K\). Every transformed budget satisfies \(b_t<0\).

3. Feasibility and negativity are preserved

For every item \(j\),

\(\displaystyle \sum_{t\in T}z_{tj}=\frac{1}{q_j}\sum_{t\in T}\mu_t x_{tj}.\)

Thus the original allocation is feasible if and only if the transformed allocation distributes exactly one unit of each item. The transformations therefore give a bijection between feasible allocations.

Moreover, for every type,

\(\displaystyle v_t(z_t)=\sum_j f_{tj}\!\left(\frac{q_j}{\mu_t}z_{tj}\right)=u_t(x_t).\)

Hence the two markets have identical sets of feasible utility vectors, with coordinates indexed by \(T\). Their attracted types also coincide because slope signs are unchanged.

If the transformed market admitted a feasible allocation giving nonnegative utility to every attracted agent and zero utility to every repulsed agent, its inverse would violate the original negativity promise. Therefore the transformed market is negative.

4. Equilibria correspond exactly

Fix corresponding prices \(p\) and \(r\). For any nonnegative bundle \(y\) of type \(t\), put \(w_j=\mu_t y_j/q_j\). Then

\(\displaystyle r\cdot w=\sum_j(q_jp_j)\frac{\mu_t y_j}{q_j}=\mu_t(p\cdot y).\)

Since \(\mu_t>0\),

\(\displaystyle p\cdot y\le e_t\quad\Longleftrightarrow\quad r\cdot w\le b_t.\)

The bundle transformation is a bijection between the entire nonnegative budget sets, and \(v_t(w)=u_t(y)\) throughout those sets. It follows that

\(\displaystyle x_t\in\arg\max_{\substack{y\ge0\\p\cdot y\le e_t}}u_t(y)\quad\Longleftrightarrow\quad z_t\in\arg\max_{\substack{w\ge0\\r\cdot w\le b_t}}v_t(w).\)

This argument preserves all maximizing bundles, including ties.

The same cost identity gives

\(\displaystyle p\cdot x_t=e_t\quad\Longleftrightarrow\quad r\cdot z_t=b_t.\)

Finally, \(r_j=q_jp_j\) preserves each price’s sign. Together with feasibility, these facts prove a bijection between the two markets’ equilibria. Under this bijection, the utility vector is unchanged.

5. Encoding size and enumeration

The reduction creates exactly \(\tau\) agents and \(m\) items, with \(K\) segments. Each new rational is obtained using a constant number of multiplications or divisions of input rationals. Its numerator and denominator therefore have \(O(L)\) bits. The total transformed encoding length is \(O((K+m+\tau)L)\), so construction takes polynomial time.

All hypotheses of the finite-market theorem are now satisfied. For fixed \(d\), apply its algorithm to the transformed market and map every returned equilibrium back using the inverse formulas.

Every original equilibrium utility vector occurs among the transformed equilibria, so the returned representatives cover every original profile. Conversely, each inverse image is an original equilibrium. If the algorithm returns duplicate profiles, evaluate utilities exactly and retain one representative per distinct vector. Rational arithmetic, comparison, and the inverse transformations take polynomial time.

Therefore the required complete enumeration takes time polynomial in \(m,\tau,K,L\), with the polynomial allowed to depend on fixed \(d\).

⟨structured verdict parsed — rendered above⟩

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

The prover’s polynomial-time claim is correct. The reduction preserves the complete equilibrium conditions and utility vectors, and the cited theorem supplies the required enumeration guarantee. I found no major or minor mathematical issues.

Theorem 3 states polynomial-time computation of equilibrium representatives covering every equilibrium utility profile for negative instances with SPLC utilities on goods, linear utilities on chores, and a constant number of chores. The paper explicitly permits unequal negative budgets, disagreement about whether an item is desirable, and optimization over the entire nonnegative budget set. Its negativity definition matches the task. Its price-sign discussion also confirms the required strict signs under nonzero slopes. These checks support the prover’s statement of the theorem. [Garg, Hoefer, McGlaughlin and Schmalhofer (2023), Sections 2 and 4](https://par.nsf.gov/servlets/purl/10491726)

Thus the invocation does not confuse computing a single equilibrium with covering all equilibrium utility profiles.

All denominators in the transformation are nonzero because \(\mu_t>0\) and \(q_j>0\). The allocation and price formulas are mutually inverse.

The stated segment slopes and lengths are correct: composing a segment with argument scaling \(q_j/\mu_t\) multiplies its slope by \(q_j/\mu_t\) and its length by \(\mu_t/q_j\).

These positive factors preserve normalization, strict slope ordering, slope signs, positive finite lengths, and the unbounded final segment. A linear chore remains linear with strictly negative slope. Consequently, global item classifications and the number \(d\) of chores are unchanged.

The budget transformation also correctly gives \(b_t=\mu_t e_t<0\). No expansion into a population-sized list of agents occurs: there are exactly \(\tau\) transformed agents.

The identity
\[ \sum_t z_{tj}=\frac{1}{q_j}\sum_t\mu_t x_{tj} \]
establishes both directions of feasibility preservation. Nonnegativity is preserved as well. In particular, transformed feasible allocations automatically satisfy the finite market’s individual coordinate bounds \(z_{tj}\le1\).

The equality \(v_t(z_t)=u_t(x_t)\) holds coordinate by coordinate, so the sets of feasible utility vectors coincide exactly. The attracted-agent sets also coincide because all slope signs are preserved.

The contradiction argument transferring the negativity promise is therefore valid. It covers repulsed types, including the case in which every type is repulsed.

For each type, the bundle map is a bijection on the entire nonnegative orthant, and
\[ r\cdot w=\mu_t(p\cdot y). \]
Since \(\mu_t>0\), the budget inequality is preserved in both directions with the stated budget \(b_t\).

Utilities agree throughout these budget sets, rather than merely at feasible allocations. This is sufficient to preserve the argmax sets exactly, including ties. There is no implicit restriction of individual demand to available supply.

The same identity preserves full expenditure. Positive supply scaling preserves every price sign. Together with feasibility, these observations justify the claimed equilibrium bijection and the equality of equilibrium utility vectors.

Each transformed rational uses a constant number of products or quotients of input rationals. Its numerator and denominator have \(O(L)\) bits; reducing fractions cannot increase that bound.

There are \(O(K+m+\tau)\) encoded quantities, so the stated total bound \(O((K+m+\tau)L)\) is a valid upper bound. Very small masses may produce large numerical scaling factors, but their binary encoding lengths remain polynomial. No assumption that inverse masses are numerically polynomial is needed.

The cited algorithm obtains representatives through rational linear feasibility problems and recovers allocation coordinates by rational division. Thus its exact representatives admit polynomial-size rational encodings, supporting the subsequent exact utility evaluation and comparisons. [Cited paper, Section 3.2](https://par.nsf.gov/servlets/purl/10491726)

A polynomial-time enumeration produces polynomially many representatives. Applying the inverse transformations preserves polynomial encoding size. Evaluating the finitely represented SPLC utilities and comparing the resulting rational vectors takes polynomial time.

The equilibrium bijection gives completeness and soundness of the returned list. Removing duplicate utility vectors therefore produces exactly the output requested in the task.

No additional clarification is required to make the mathematical argument verifiable.

⟨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.