← back to the atlas

d4-conf-wine-2020-0029 (d4-conf-wine-2020-0029)

Answer: —

The anchor (named result in the paper)

Theorem 4 — class: other

The continuous mirror question, as graded

Given rational per-capita capacities \(\bar{s}_j\) and a finite support \(\Theta\) of consumer types with rational masses \(\mu_\theta>0\), \(\sum_{\theta\in\Theta}\mu_\theta=1\), utilities \(u_\theta\), budgets \(w_\theta\), and physical constraints \(A_{\theta q}x\leq 1\), compute a market-clearing equilibrium. For each type, its allocation \(x_\theta\) must maximize \(u_\theta^\top x\) subject to \(x\geq 0\), \(p^\top x\leq w_\theta\), and its physical constraints; clearing requires \(\sum_\theta\mu_\theta x_{\theta j}=\bar{s}_j\) and each type spends its budget. The output must also include BP-SOP multipliers \(r_{\theta q}\geq 0\) and perturbations \(\lambda_\theta=\sum_q r_{\theta q}\) satisfying the paper’s fixed-point correspondence. For a guaranteed-existence version, assume an unconstrained good and that every type values every good positively.

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

A society is given by its support: the list \(\Theta\) of \(\tau\) consumer types with positive binary-rational masses \(\mu_\theta\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types.
There are \(m\geq1\) divisible goods with positive rational per-capita supplies \(\bar s_j\); each type has positive rational utilities \(u_{\theta j}\) and budget \(w_\theta\). Let \(L\) be the total input bit length.
Resource groups form a family \(T\) of pairwise disjoint nonempty subsets of goods; each consumer type specifies \(T_\theta\subseteq T\). Its physical constraints are \(A_{\theta q}x=\sum_{j\in q}x_j\leq1\) for \(q\in T_\theta\). Put \(k=\sum_\theta|T_\theta|\).
Assume a good lies outside every resource group, and promise that a nonnegative-price equilibrium exists.
An equilibrium consists of \(p\in\mathbb R_{\geq0}^m\) and \(x_\theta\in\mathbb R_{\geq0}^m\), where each \(x_\theta\) maximizes \(u_\theta^\top x\) subject to \(p^\top x\leq w_\theta\) and its physical constraints, with \(p^\top x_\theta=w_\theta\) and \(\sum_\theta\mu_\theta x_{\theta j}=\bar s_j\). Any maximizing bundle is allowed.
For fixed \(\lambda\geq0\), BP-SOP maximizes \(\sum_\theta\mu_\theta(w_\theta+\lambda_\theta)\log(u_\theta^\top x_\theta)\) over nonnegative allocations satisfying these clearing equalities and physical constraints.
The required output includes an equilibrium and \(r_{\theta q}\geq0\), \(\lambda_\theta=\sum_{q\in T_\theta}r_{\theta q}\), such that the allocation and multipliers satisfy BP-SOP's KKT conditions: \(p_j\) multiplies \(\sum_\theta\mu_\theta x_{\theta j}-\bar s_j\), and \(r_{\theta q}\) multiplies \(\mu_\theta(A_{\theta q}x_\theta-1)\). Exact coordinates use standard real-algebraic encodings.

Is this exact equilibrium-and-fixed-point search problem solvable in time polynomial in \(m,\tau,k,L\), or is it NP-hard?

For finite-agent markets, equilibrium prices correspond to BP-SOP fixed points; convergence of the proposed fixed-point iteration was demonstrated numerically. [Source](https://arxiv.org/pdf/2005.10765)
Later work proves convergence for homogeneous linear constraints, while leaving polynomial-time exact computation with nonhomogeneous constraints unresolved. [Source](https://arxiv.org/pdf/2106.10412)
No result settling this exact mass-supported formulation was located.

Modeling choices made when packaging the task

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

Status and proved extension

I do not settle the unrestricted polynomial-time versus NP-hard question. I prove the following extension of the verified results in NOTES.

Theorem. For every fixed number of goods $m$, the promised exact equilibrium-and-fixed-point search problem is solvable in time polynomial in $\tau,k,L$. The output has polynomial-length real-algebraic encodings. The polynomial’s exponent may depend on $m$.

The proof treats binary-rational masses directly and allows arbitrary indifference among maximizing bundles. Its central structural result is that a clearing allocation can be obtained by mixing at most $m$ demand profiles, using the same mixing weights for every consumer type.

1. Definitions and admissible prices

Let $\Theta$ be the support of consumer types, with $|\Theta|=\tau$, masses $\mu_\theta>0$ satisfying $\sum_\theta\mu_\theta=1$, positive budgets $w_\theta$, and positive utility coefficients $u_{\theta j}$. Supplies $\bar s_j$ are positive. All these data are rational.

The resource groups are pairwise disjoint nonempty subsets of the goods. Type $\theta$ is constrained by
$$ A_{\theta q}x=\sum_{j\in q}x_j\leq1, \qquad q\in T_\theta. $$
Fix a good $h$ outside every resource group.

Write
$$ W=\sum_{\theta\in\Theta}\mu_\theta w_\theta. $$
Let $J_0$ consist of the goods that are physically unconstrained for at least one type:
$$ J_0= \left\{ j:\text{there exists }\theta\text{ with } j\notin\bigcup_{q\in T_\theta}q \right\}. $$
In particular, $h\in J_0$.

At an equilibrium, $p_j>0$ for every $j\in J_0$. Indeed, if such a good had zero price, the corresponding type could increase its consumption without violating any constraint and strictly increase utility. It would therefore have no maximizing bundle.

Aggregating exhausted budgets and using clearing gives
$$ p^\top\bar s = \sum_\theta\mu_\theta p^\top x_\theta = W. $$
Consequently every equilibrium price belongs to
$$ \mathcal P= \left\{ p\in\mathbb R_{\geq0}^m: p_j>0\text{ for }j\in J_0,\quad p^\top\bar s=W \right\}. $$

For $p\in\mathcal P$, define the consumer’s feasible polytope and demand face by
$$ H_\theta(p)= \left\{ x\in\mathbb R_{\geq0}^m: p^\top x\leq w_\theta,\quad A_{\theta q}x\leq1\text{ for }q\in T_\theta \right\}, $$
$$ D_\theta(p)= \operatorname*{arg\,max}_{x\in H_\theta(p)} u_\theta^\top x. $$

These sets have the following properties.

Define the weighted Minkowski sum
$$ K(p)= \sum_{\theta\in\Theta}\mu_\theta D_\theta(p) = \left\{ \sum_\theta\mu_\theta x_\theta: x_\theta\in D_\theta(p) \right\}. $$
It is a nonempty compact polytope. Budget exhaustion implies
$$ K(p)\subseteq\{z\in\mathbb R^m:p^\top z=W\}. $$
Since $p_h>0$, this hyperplane has dimension $m-1$.

Thus $p\in\mathcal P$ is an equilibrium price exactly when
$$ \bar s\in K(p). $$

2. Equilibria supply precisely the required fixed-point certificates

The following result also verifies that finding an equilibrium suffices mathematically for the required BP-SOP output.

Proposition. Every equilibrium admits the specified nonnegative BP-SOP multipliers with
$$ \lambda_\theta=\sum_{q\in T_\theta}r_{\theta q}. $$
Conversely, a feasible BP-SOP KKT point satisfying this identity and $p\geq0$ is an equilibrium.

Equilibrium implies fixed-point KKT

Fix an equilibrium $(p,x)$. Each consumer linear program is feasible and has a finite attained optimum. Linear-programming strong duality supplies optimal dual variables
$$ \alpha_\theta\geq0,\qquad \gamma_{\theta q}\geq0 $$
satisfying
$$ \alpha_\theta p_j+ \sum_{\substack{q\in T_\theta\\j\in q}}\gamma_{\theta q} \geq u_{\theta j}, $$
$$ x_{\theta j} \left( \alpha_\theta p_j+ \sum_{\substack{q\in T_\theta\\j\in q}}\gamma_{\theta q} -u_{\theta j} \right)=0, $$
$$ \gamma_{\theta q}(A_{\theta q}x_\theta-1)=0. $$
Complementary slackness holds for the specified optimal allocation, including when it is one of several maximizing bundles.

The inequality for $h$ gives
$$ \alpha_\theta p_h\geq u_{\theta h}>0, $$
so $\alpha_\theta>0$. Define
$$ \beta_\theta=\frac1{\alpha_\theta}, \qquad r_{\theta q}=\frac{\gamma_{\theta q}}{\alpha_\theta}, \qquad R_{\theta j}= \sum_{\substack{q\in T_\theta\\j\in q}}r_{\theta q}. $$
Then
$$ d_{\theta j}:=p_j+R_{\theta j}-\beta_\theta u_{\theta j}\geq0, \qquad x_{\theta j}d_{\theta j}=0, $$
$$ r_{\theta q}(A_{\theta q}x_\theta-1)=0. $$

Put $U_\theta=u_\theta^\top x_\theta$. Positive expenditure and positive utility coefficients imply $U_\theta>0$. Multiplying the stationarity equalities by $x_{\theta j}$ and summing yields
$$ \beta_\theta U_\theta = p^\top x_\theta+ \sum_{q\in T_\theta}r_{\theta q}A_{\theta q}x_\theta = w_\theta+\sum_{q\in T_\theta}r_{\theta q}. $$
Therefore, with $\lambda_\theta=\sum_qr_{\theta q}$,
$$ \beta_\theta=\frac{w_\theta+\lambda_\theta}{U_\theta}. $$

For fixed $\lambda$, BP-SOP’s Lagrangian, with the conventions required in the question, is
$$ \mathcal L= \sum_\theta\mu_\theta(w_\theta+\lambda_\theta)\log U_\theta -\sum_jp_j\left(\sum_\theta\mu_\theta x_{\theta j}-\bar s_j\right) -\sum_{\theta,q}\mu_\theta r_{\theta q} (A_{\theta q}x_\theta-1). $$
Its derivative is
$$ \frac{\partial\mathcal L}{\partial x_{\theta j}} = \mu_\theta(\beta_\theta u_{\theta j}-p_j-R_{\theta j}) = -\mu_\theta d_{\theta j}. $$
Thus the nonnegativity multipliers are $\mu_\theta d_{\theta j}$, and all KKT conditions hold with exactly the requested normalization.

These conditions also certify global optimality. For any other feasible allocation $y$ with positive type utilities, logarithmic concavity gives
$$ F(y)-F(x) \leq \sum_{\theta,j}\mu_\theta\beta_\theta u_{\theta j} (y_{\theta j}-x_{\theta j}). $$
Substitute $\beta_\theta u_{\theta j}=p_j+R_{\theta j}-d_{\theta j}$. The price contribution vanishes by clearing. Each physical-constraint contribution is nonpositive by feasibility and complementary slackness. The remaining contribution equals
$$ -\sum_{\theta,j}\mu_\theta d_{\theta j}y_{\theta j}\leq0. $$
An allocation with a zero type utility has logarithmic objective value $-\infty$.

Fixed-point KKT implies equilibrium

At such a KKT point, let
$$ \beta_\theta=\frac{w_\theta+\lambda_\theta}{U_\theta}>0. $$
Stationarity and complementary slackness give the same conditions involving $d_{\theta j}$. Taking their scalar product with $x_\theta$ gives
$$ w_\theta+\lambda_\theta = \beta_\theta U_\theta = p^\top x_\theta+\sum_qr_{\theta q} = p^\top x_\theta+\lambda_\theta. $$
Hence $p^\top x_\theta=w_\theta$.

For every consumer-feasible bundle $y_\theta$,
$$ \beta_\theta u_\theta^\top y_\theta \leq p^\top y_\theta+\sum_qr_{\theta q}A_{\theta q}y_\theta \leq w_\theta+\lambda_\theta = \beta_\theta U_\theta. $$
Division by $\beta_\theta>0$ proves consumer optimality. Clearing and nonnegative prices are already hypotheses. This proves the proposition.

3. A clearing allocation needs at most $m$ common demand profiles

Call $(v_\theta)_{\theta\in\Theta}$ an exposed demand profile at $p$ if there is a direction $a\in\mathbb R^m$ such that, for every type $\theta$, $v_\theta$ uniquely maximizes $a^\top x$ over $D_\theta(p)$.

Lemma. If $p\in\mathcal P$ and $\bar s\in K(p)$, there exist at most $m$ exposed demand profiles $(v_\theta^{(i)})_\theta$ and nonnegative weights $c_i$ summing to one such that
$$ \bar s= \sum_i c_i\sum_\theta\mu_\theta v_\theta^{(i)}. $$
Consequently,
$$ x_\theta=\sum_i c_i v_\theta^{(i)} $$
is a clearing equilibrium allocation at $p$.

Proof. First consider a vertex $z$ of $K(p)$. Every vertex of a polytope is uniquely exposed by a linear functional. Here is a direct justification. If the polytope has other vertices, let $C$ be their convex hull. Since $z$ is a vertex, $z\notin C$. Let $y$ be a point of $C$ closest to $z$ and set $a=z-y$. The minimizing property gives
$$ a^\top(v-y)\leq0 \qquad(v\in C). $$
Hence
$$ a^\top(z-v)\geq\|z-y\|^2>0 \qquad(v\in C). $$
Thus $a$ uniquely exposes $z$. For a singleton polytope, any direction suffices.

For each $\theta$, choose a maximizer $v_\theta$ of $a^\top x$ over $D_\theta(p)$. Their weighted sum maximizes $a^\top z$ over $K(p)$, so it equals the uniquely exposed vertex $z$.

Each type’s maximizer must also be unique. Otherwise, replacing one type’s bundle by a different maximizer, while holding all other bundles fixed, would produce a different aggregate maximizer because $\mu_\theta>0$. This contradicts uniqueness of $z$.

Therefore every vertex of $K(p)$ comes from an exposed demand profile.

Finally, $K(p)$ has affine dimension at most $m-1$. Any point in it is a convex combination of at most $m$ vertices. To verify this bound, start with a finite vertex combination. If more than $m$ vertices have positive weights, they are affinely dependent: there are scalars $b_i$, not all zero, with
$$ \sum_i b_i=0, \qquad \sum_i b_i z_i=0. $$
Both positive and negative $b_i$ occur. Setting
$$ \varepsilon=\min_{b_i>0}\frac{c_i}{b_i} $$
and replacing $c_i$ by $c_i-\varepsilon b_i$ preserves the represented point and total weight, keeps every weight nonnegative, and removes at least one positive weight. Repetition proves the bound.

Apply this to $\bar s$. Each resulting $x_\theta$ lies in the convex demand face $D_\theta(p)$, and their weighted sum is $\bar s$. This proves the lemma. $\square$

The lemma holds without fixing $m$. Fixing $m$ makes the number of profiles usable algorithmically.

4. Polynomially many descriptions of exposed profiles for fixed $m$

Assume henceforth that $m$ is fixed.

Because the resource groups are disjoint and exclude $h$, each type has at most $m-1$ physical constraints. Thus $H_\theta(p)$ has at most $2m$ defining inequalities: $m$ nonnegativity inequalities, at most $m-1$ physical inequalities, and one budget inequality.

Every vertex is obtained by making $m$ linearly independent defining inequalities tight. Enumerate all such candidate sets $B$. There are at most
$$ \binom{2m}{m} $$
candidates per type, a constant depending only on $m$.

For a candidate $B$, Cramer’s rule gives a vector
$$ v_{\theta B}(p)=\frac{N_{\theta B}(p)}{\Delta_{\theta B}(p)} $$
when $\Delta_{\theta B}(p)\neq0$. Here $N_{\theta B}$ is a vector of rational polynomials and $\Delta_{\theta B}$ is a rational polynomial.

Both have degree at most one: only the budget row of the candidate linear system depends on $p$, and determinants are multilinear in their rows. Candidates with identically zero determinant are discarded.

At a particular price, a candidate is a genuine feasible vertex exactly when its determinant is nonzero and its coordinates satisfy all defining inequalities. Degeneracy causes no omission: the active normals at a vertex span $\mathbb R^m$, so some independent active set appears in the enumeration. Indeed, if they did not span, a nonzero direction annihilating them would permit sufficiently small perturbations in both directions while preserving every inequality, contradicting extremality.

We now construct a polynomial family in the $2m$ variables $(p,a)$. It contains:

$$ u_\theta^\top v_{\theta B}(p) - u_\theta^\top v_{\theta C}(p); $$

$$ a^\top v_{\theta B}(p) - a^\top v_{\theta C}(p). $$

For example, the numerator of the last difference is
$$ \bigl(a^\top N_{\theta B}(p)\bigr)\Delta_{\theta C}(p) - \bigl(a^\top N_{\theta C}(p)\bigr)\Delta_{\theta B}(p). $$
Including the determinant signs makes every rational comparison unambiguous.

The family contains $O_m(\tau)$ polynomials, each of degree at most three and coefficient bit length polynomial in $L$. On a region where all their signs are specified, the following information is constant for every type:

Break remaining ties by the first candidate in a fixed ordering. This selects one candidate index $B_\theta(\sigma)$ for each type, depending only on the sign vector $\sigma$.

The real-algebraic algorithmic fact used here is:

For a fixed number of variables, realizable sign conditions of rational polynomials can be enumerated, and a point satisfying a quantifier-free polynomial formula can be found exactly, in polynomial bit complexity in the number of polynomials, their degrees, and their coefficient encoding lengths. Sample points have polynomial-length algebraic representations.

This follows from standard cylindrical algebraic decomposition and its bit-complexity analysis. It includes zero signs and strict inequalities. See [Basu–Pollack–Roy, *Algorithms in Real Algebraic Geometry*](https://link.springer.com/book/10.1007/3-540-33099-2) and [Basu’s survey, Section 2.1.2](https://www.math.purdue.edu/~sbasu/raag_survey2011_final.pdf).

Its hypotheses hold: there are $2m$ variables, $m$ is fixed, the coefficients are rational, and the degree and encoding bounds above are polynomial.

We can therefore enumerate polynomially many realizable sign vectors and retain those satisfying $p\in\mathcal P$. For each retained $\sigma$, let $C_\sigma(p,a)$ be the conjunction specifying its polynomial signs, and define
$$ v_{\theta\sigma}(p)=v_{\theta,B_\theta(\sigma)}(p), \qquad V_\sigma(p)=\sum_\theta\mu_\theta v_{\theta\sigma}(p). $$

Whenever $C_\sigma(p,a)$ holds, every $v_{\theta\sigma}(p)$ belongs to $D_\theta(p)$, so $V_\sigma(p)\in K(p)$. Moreover, every vertex of $K(p)$ is represented by some such selection: choose a direction uniquely exposing that vertex and use Section 3.

The sign region need not be connected. All selection decisions depend only on the recorded signs.

5. Exact clearing in a fixed number of variables

For each retained $\sigma$, write
$$ Q_\sigma(p)= \prod_{\theta\in\Theta} \Delta_{\theta,B_\theta(\sigma)}(p), $$
$$ H_{\sigma j}(p)= \sum_{\theta\in\Theta} \mu_\theta N_{\theta,B_\theta(\sigma),j}(p) \prod_{\eta\neq\theta} \Delta_{\eta,B_\eta(\sigma)}(p). $$
Then
$$ V_{\sigma j}(p)=\frac{H_{\sigma j}(p)}{Q_\sigma(p)}. $$
Both $Q_\sigma$ and $H_{\sigma j}$ have degree at most $\tau$. Their denominator is nonzero whenever $C_\sigma(p,a)$ holds.

Enumerate ordered $m$-tuples of retained sign vectors
$$ (\sigma_1,\ldots,\sigma_m). $$
There are polynomially many tuples for fixed $m$.

For each tuple, seek variables
$$ p\in\mathbb R^m,\qquad a_1,\ldots,a_m\in\mathbb R^m,\qquad c_1,\ldots,c_m\in\mathbb R $$
satisfying
$$ p\in\mathcal P,\qquad C_{\sigma_i}(p,a_i)\quad(1\leq i\leq m), $$
$$ c_i\geq0,\qquad \sum_{i=1}^m c_i=1, $$
$$ \sum_{i=1}^m c_iV_{\sigma_i}(p)=\bar s. $$

The last equality is made polynomial by multiplying by the nonzero common denominator. For every good $j$, it becomes
$$ \sum_{i=1}^m c_iH_{\sigma_i j}(p) \prod_{\ell\neq i}Q_{\sigma_\ell}(p) - \bar s_j\prod_{\ell=1}^mQ_{\sigma_\ell}(p) =0. $$
Its degree is at most $m\tau+1$.

Each resulting system has
$$ m+m^2+m=m^2+2m $$
variables, a fixed number. It has polynomially many constraints and polynomial coefficient encoding length.

For clarity about the latter assertion, products of at most $m\tau$ affine polynomials in $m$ price variables have only polynomially many monomials when $m$ is fixed. Coefficient bit lengths grow polynomially under these products and the displayed sums. Thus the systems can be constructed explicitly in polynomial bit complexity.

Apply the fixed-dimensional real-algebraic algorithm to each system.

Soundness

From a sampled solution, define
$$ x_\theta=\sum_{i=1}^m c_i v_{\theta\sigma_i}(p). $$
Every summand belongs to $D_\theta(p)$, so convexity gives $x_\theta\in D_\theta(p)$. The clearing equations give
$$ \sum_\theta\mu_\theta x_\theta=\bar s. $$
Therefore $(p,x)$ is an equilibrium.

Completeness under the promise

Take any promised equilibrium price $p$. Section 3 represents $\bar s$ as a convex combination of at most $m$ vertices of $K(p)$, each obtained from a common exposing direction.

Section 4 represents each of those profiles by a retained sign vector. If fewer than $m$ profiles are needed, repeat one profile and give the extra copies zero weight. Consequently one enumerated system is nonempty.

The algorithm therefore finds an equilibrium.

6. Polynomial-time reconstruction of the fixed-point multipliers

It remains to construct the certificate from Section 2 with controlled encoding size.

Fix the computed price $p$ and allocation $x$. For type $\theta$, put
$$ U_\theta=u_\theta^\top x_\theta, \qquad d_\theta=1+|T_\theta|\leq m. $$
Its dual linear program has $d_\theta$ variables and is
$$ \min\left\{ \alpha w_\theta+\sum_q\gamma_q: \alpha,\gamma_q\geq0,\quad \alpha p_j+\sum_{\substack{q\in T_\theta\\j\in q}}\gamma_q \geq u_{\theta j}\text{ for every }j \right\}. $$
Strong duality applies because the primal is feasible, bounded, and attains its optimum. Thus the dual optimal face is nonempty and satisfies
$$ \alpha w_\theta+\sum_q\gamma_q=U_\theta. $$
It is bounded, since
$$ 0\leq\alpha\leq U_\theta/w_\theta, \qquad 0\leq\gamma_q\leq U_\theta. $$
Being a nonempty compact polytope, it has a vertex. Such a vertex is also a vertex of the dual feasible polyhedron: if it were a nontrivial convex combination of two dual-feasible points, optimality of the average would force both points to be optimal.

Enumerate sets of $d_\theta$ independent tight dual inequalities, solve the resulting systems, and check dual feasibility and objective value $U_\theta$. There are at most $2m$ dual inequalities, so only a constant number of candidates per type. The preceding argument guarantees an accepted candidate.

For every accepted candidate,
$$ \alpha_\theta p_h\geq u_{\theta h}>0, $$
hence $\alpha_\theta>0$. Output
$$ r_{\theta q}=\frac{\gamma_{\theta q}}{\alpha_\theta}, \qquad \lambda_\theta=\sum_qr_{\theta q}. $$
Section 2 proves that these are valid BP-SOP fixed-point multipliers.

Exact encoding and total complexity

The sampled tuple has a polynomial-length algebraic representation because the sampling system has fixed dimension. It can be represented in a common real number field of polynomial degree and polynomial coefficient bit length.

Every allocation coordinate and every dual candidate is obtained by rational arithmetic and determinants of fixed size in that field. The divisions defining $r_{\theta q}$ have nonzero denominators. These operations, sign tests, and equality tests have polynomial bit complexity, and the resulting coordinates retain polynomial-length standard real-algebraic encodings.

There are polynomially many sign vectors, polynomially many tuples for fixed $m$, polynomial-time sampling calls, and a constant number of dual candidates per type. All masses are used as rational coefficients; no replication into individual agents occurs.

This proves the theorem.

7. What remains open

The proved algorithm has running time of the form
$$ (\tau+k+L)^{C_m}, $$
where $C_m$ depends on $m$. It therefore does not establish polynomial time jointly in $m,\tau,k,L$.

No NP-hardness reduction for the unrestricted promised search problem is proved here. The unresolved step is either to obtain an algorithm whose polynomial exponent is independent of $m$, including exact encoding bounds, or to establish the requested hardness while preserving all stated restrictions.

⟨structured verdict parsed — rendered above⟩

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

The output establishes a substantive fixed-$m$ result, but does not resolve USER_TASK, which asks for polynomial time jointly in $m,\tau,k,L$ or NP-hardness. I found no false central mathematical step. The fixed-$m$ argument is sound in substance, with a minor clarification needed about exact algebraic representations.

1. Admissible prices and demand polytopes — correct.

The argument that $p_j>0$ for $j\in J_0$ is valid: for a type physically unconstrained in coordinate $j$, a zero price permits arbitrarily large increases in positive utility while preserving feasibility.

Budget exhaustion and clearing correctly imply
$$ p^\top\bar s=W. $$
Thus every equilibrium price belongs to $\mathcal P$. The proof does not incorrectly treat this necessary condition as sufficient.

For any $p\in\mathcal P$, every coordinate of $H_\theta(p)$ is bounded. A coordinate covered by a type’s physical constraints is at most one; an uncovered coordinate has positive price and is bounded by $w_\theta/p_j$. Nonemptiness, compactness, and existence of the demand face follow.

The argument for budget exhaustion throughout $D_\theta(p)$ correctly uses the globally unconstrained good $h$, its positive price, and its positive utility coefficient.

Consequently,
$$ K(p)\subseteq\{z:p^\top z=W\} $$
and its affine dimension is at most $m-1$. The equivalence between equilibrium prices and membership $\bar s\in K(p)$ follows directly from the definitions.

2. Equilibrium and fixed-point KKT equivalence — correct.

The consumer primal linear programs are feasible, bounded, and attain their optima. These are sufficient hypotheses for the stated strong-duality application and existence of optimal dual variables. Complementary slackness applies to the specified optimal allocation, even under indifference.

The inequality for $h$ correctly forces $\alpha_\theta>0$, making all subsequent divisions legitimate.

The critical identity
$$ \beta_\theta U_\theta = w_\theta+\sum_{q\in T_\theta}r_{\theta q} $$
follows from coordinate complementarity, budget exhaustion, and physical-constraint complementarity. In particular, replacing $r_{\theta q}A_{\theta q}x_\theta$ by $r_{\theta q}$ is justified.

The Lagrangian uses exactly the multiplier normalization required by USER_TASK. Its derivative and the nonnegativity multipliers $\mu_\theta d_{\theta j}$ have the correct signs and scaling. The weights $\lambda_\theta$ are held fixed when taking derivatives, as required.

The global-optimality argument is also valid: clearing eliminates the price term, active physical constraints give nonpositive contributions, and nonnegativity complementarity eliminates the corresponding terms at $x$.

Conversely, the scalar-product argument correctly recovers budget exhaustion from KKT and the fixed-point identity. The displayed inequality for every consumer-feasible bundle proves utility maximization. Positive $U_\theta$ is implicit in being a KKT point of the logarithmic objective; there is no invalid division at a zero-utility allocation.

3. At most $m$ common demand profiles — correct.

The closest-point argument correctly exposes each nonsingleton polytope vertex uniquely. The singleton case is handled separately.

For an exposing direction, independent maximization over the demand faces correctly yields a maximizing point of their weighted Minkowski sum. The uniqueness argument is valid: changing one type’s maximizing bundle changes the aggregate because $\mu_\theta>0$, contradicting unique aggregate maximization.

The affine-dependence elimination preserves the represented point, total weight, and nonnegative coefficients. It removes a positive coefficient at each iteration. The dimension bound therefore gives at most $m$ profiles.

The same mixture weights can indeed be used for every type. Convexity of each demand face ensures that the resulting individual bundles remain optimal.

4. Enumeration of profile descriptions — correct.

Pairwise disjointness and exclusion of $h$ imply
$$ |T_\theta|\leq m-1. $$
The bound of $2m$ primal inequalities and the resulting constant number of candidate bases for fixed $m$ are correct.

The active-normal argument establishes that every vertex has an enumerated independent active set, including degenerate vertices.

The degree claims check out:

Recording denominator signs correctly resolves rational comparisons. Zero determinants are excluded from feasible candidates.

The sign conditions therefore determine the candidate selection. Multiple bases describing the same geometric vertex cause no problem. Likewise, tie-breaking may select profiles that are not uniquely exposed, but soundness only requires their selected bundles to belong to demand faces. Unique exposure is used where needed for completeness.

The cited fixed-dimensional real-algebraic machinery is applicable. The CAD complexity stated in the cited survey is polynomial when the dimension is fixed; its sample-point discussion also covers realizable sign conditions. No generic-position, full-dimensionality, or connectedness assumption is required here. [Basu’s survey, Sections 2.1.2 and 2.2](https://www.math.purdue.edu/~sbasu/raag_survey2011_final.pdf).

5. Clearing systems — correct.

The expressions $Q_\sigma$ and $H_{\sigma j}$ correctly combine the type-specific rational functions, and their degrees are at most $\tau$.

Each selected determinant is nonzero wherever its sign condition holds. Thus multiplying the clearing equations by the displayed common denominator preserves equivalence and introduces no spurious solutions.

The clearing polynomial has degree at most
$$ m\tau+1, $$
and the variable count is correctly
$$ m^2+2m. $$

For fixed $m$, dense polynomial expansion has polynomially many monomials. The products and sums described have polynomial coefficient bit length. Binary-rational masses enter as coefficients, without consumer replication.

Soundness follows from convexity of demand faces and the clearing equations. Completeness follows from the common-profile lemma and sign-condition coverage. Padding with repeated profiles of zero weight is legitimate.

The case $m=1$ is also covered: the aggregate demand polytope has affine dimension zero, and only one profile is required.

6. Multiplier reconstruction and exact encodings — substantively correct; minor clarification.

The dual has $d_\theta\leq m$ variables and at most $2m$ inequalities. Strong duality gives a nonempty optimal face.

Its boundedness follows from positive objective coefficients and the fixed optimal value $U_\theta$. The argument that a vertex of the optimal face is a vertex of the feasible dual polyhedron is correct. Enumerating independent tight inequalities therefore finds an optimal dual vertex.

Any accepted dual optimum is complementary to the computed primal optimum. The inequality for $h$ again guarantees $\alpha_\theta>0$, so the reconstructed multipliers are valid.

Minor issue: Section 6 moves from “polynomial-length algebraic representation” to a common number field with polynomial degree, polynomial coefficient size, and polynomial-time arithmetic without specifying the representation or citing its precise computational guarantees. The fixed number of sampled coordinates makes this a routine representation clarification, rather than a missing mathematical argument.

Minimum clarification: Identify the exact sampling representation and cite the guarantees supporting common-field computation, exact sign/equality tests, and conversion to the standard coordinate encodings required by USER_TASK. The cited survey’s CAD statement alone should not be presented as the complete bit-complexity and representation justification.

7. Scope — major unresolved requirement.

The algorithm’s exponent depends on $m$. Thus the proved bound
$$ (\tau+k+L)^{C_m} $$
does not establish polynomial time jointly in all four input parameters.

No NP-hardness reduction is supplied. The prover explicitly acknowledges both limitations, so this is an incomplete resolution of the assignment, not a misleading claim or a refuted proof.

The genuine progress is the fixed-$m$ exact algorithm, the common-profile lemma, and the equilibrium–KKT equivalence. Completing the unrestricted assignment requires an additional result; no expositional clarification can supply it.

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