← back to the atlas

d4-conf-sigecom-2009-0001 (d4-conf-sigecom-2009-0001)

Answer: —

The anchor (named result in the paper)

Corollary 3.5 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateComputing the worst case loss bound for the SCPM is a convex optimization problem. Further- more, a necessary and sufficient condition on utility func- tion u(·) in order to guarantee a bounded loss is that the difference u(⃗s) −si is bounded from above. Below, we illustrate the application of the above theorem through some examples. Detailed proofs for these examples are available in Appendix D. Example 3.6.

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

The continuous mirror question, as graded

Given \(N\) outcomes, an SCPM cost function \(C\), and \(\tau\) trader types with rational masses \(\mu_t\) summing to \(1\), each type \(t\) has a standardized claim bundle \(\mathbf{a}_t\in\{0,1\}^N\) and per-capita quantity limit \(\ell_t\). Assuming prices do not bind, compute the worst-case per-capita loss and an attaining allocation by maximizing \(q_i-C(\mathbf{q})+C(\mathbf{0})\) over outcomes \(i\) and quantities \(0\le x_t\le\mu_t\ell_t\), where \(\mathbf{q}=\sum_t x_t\mathbf{a}_t\).

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

There are \(m=N\ge1\) mutually exclusive, exhaustive outcomes; a claim on outcome \(i\) pays one unit exactly when \(i\) occurs. A society is given by its support: \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\); \(\tau\) is the support size, not the number of possible types. Each type has a bundle \(\mathbf a_t\in\{0,1\}^N\) and a finite binary-rational per-capita limit \(\ell_t\ge0\).
An SCPM cost function is a finite continuous convex function \(C:\mathbb R^N\to\mathbb R\) satisfying \(C(\mathbf q+d\mathbf e)=C(\mathbf q)+d\) for every real \(d\), where \(\mathbf e\) is the all-ones vector. Equivalently, it admits \(C(\mathbf q)=\min_{z\in\mathbb R}\{z-u(z\mathbf e-\mathbf q)\}\) for a concave continuous utility \(u\). Coordinatewise monotonicity is not required.
For an exact finite-input problem, supply the graph of \(C\) as a quantifier-free Boolean formula of rational polynomial equalities and inequalities, with polynomials listed sparsely and exponents encoded in binary; validity of the stated cost-function properties is promised. Let \(L\) be the total input bit length.
Start with zero holdings. Quantities are divisible, prices impose no additional restriction, and \(x_t\) denotes aggregate quantity purchased by type \(t\). Define \(\mathbf q=\sum_{t=1}^{\tau}x_t\mathbf a_t\) and the worst-case per-capita loss \(W=\max_{1\le i\le N,\;0\le x_t\le\mu_t\ell_t}\{q_i-C(\mathbf q)+C(\mathbf0)\}\); the associated optimization asks for this value and an attaining allocation.

Is deciding \(W\ge K\), for a binary-rational threshold \(K\), in \(\mathrm P\), with running time polynomial in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?

For finite outcomes and unrestricted nonnegative holdings, worst-case SCPM loss is a convex optimization problem, and bounded loss is equivalent to every \(u(\mathbf s)-s_i\) being bounded above. The [full version](https://web.stanford.edu/~yyye/scpm-or-final.pdf) retains this result; it does not establish exact bit complexity for the support-constrained problem stated here. No result settling that exact problem was located.

Modeling choices made when packaging the task

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

Status: a stronger partial lower bound

I do not settle the requested $\mathrm P$ versus $\mathrm{NP}$-hardness classification. I prove the following additional lower bound:

Theorem. There is a polynomial-time many-one reduction from $\mathrm{PosSLP}$ to the promised decision problem. This holds even when:

Here $\mathrm{PosSLP}$ asks whether a division-free arithmetic circuit, with constants $0,1$ and operations addition, subtraction, and multiplication, computes a positive integer.

I also give a self-contained proof that the promised decision problem belongs to $\exists\mathbb R$, and therefore to $\mathrm{PSPACE}$.

The lower bound does not establish $\mathrm{NP}$-hardness. Its significance is that exact arithmetic-circuit comparison can be encoded while preserving global convexity, compact allocation bounds, and a quadratic rational graph formula.

1. Attainment and the upper bound

Let $A$ be the matrix whose columns are the bundles, and set $b_t=\mu_t\ell_t$. The allocation box is

$$ X=\prod_{t=1}^{\tau}[0,b_t]. $$

It is nonempty and compact because every $b_t$ is finite and nonnegative. For each outcome $i$, the function

$$ F_i(\mathbf x)=(A\mathbf x)_i-C(A\mathbf x)+C(\mathbf0) $$

is continuous. Thus each $F_i$ attains its maximum on $X$, and the maximum over the finitely many outcomes is also attained.

Each $F_i$ is concave because $C\circ A$ is convex. Consequently,

$$ W=C(\mathbf0)-\min_{1\le i\le N}\min_{\mathbf x\in X} \bigl(C(A\mathbf x)-(A\mathbf x)_i\bigr). $$

This establishes the convex optimization formulation, but supplies no exact polynomial-time bound.

For $N=1$, cash invariance gives $C(q)=q+C(0)$, so $W=0$. The lower bound below concerns growing $N$.

Let $G(\mathbf q,y)$ be the supplied graph formula. On promised inputs, the decision problem is equivalent to

$$ \begin{aligned} \exists\,\mathbf x,\mathbf q,y,y_0:\quad& G(\mathbf0,y_0)\land G(\mathbf q,y)\\ &\land\bigwedge_{t=1}^{\tau}(0\le x_t\le b_t)\\ &\land\bigwedge_{j=1}^{N} \left(q_j=\sum_{t=1}^{\tau}a_{jt}x_t\right)\\ &\land\bigvee_{i=1}^{N}(q_i-y+y_0\ge K). \end{aligned} $$

The graph clauses force $y=C(\mathbf q)$ and $y_0=C(\mathbf0)$. Attainment proves the equivalence even when $W=K$.

To handle binary exponents, evaluate each sparse polynomial using arithmetic gates. Repeated squaring computes a power using a number of gates linear in the exponent’s bit length. A multiplication gate is represented by $z=uv$, and an addition gate by $z=u+v$. Existentially quantify all gate values and conjoin their equations.

These equations uniquely determine the evaluations, so this transformation preserves the entire Boolean graph formula, including negations. Its size is polynomial in the sparse input length. Clearing rational denominators also requires only polynomially many bits.

Thus the promised problem belongs to $\exists\mathbb R$. The existential theory of the reals is decidable in polynomial space, giving the claimed upper bound. [Canny, *Some Algebraic and Geometric Computations in PSPACE*](https://www2.eecs.berkeley.edu/Pubs/TechRpts/1988/6041.html).

2. Encoding arithmetic-circuit comparison by bounded convex constraints

The first part of the lower bound constructs a polynomial-size convex feasibility system. Every variable lies in $[-1,1]$, and every constraint is either affine or requires an affine symmetric matrix of order $2$ to be positive semidefinite.

2.1 Replacing signed arithmetic by nonnegative arithmetic

Represent each value $z$ in the input circuit as a difference $P-N$, where $P,N$ are computed using only addition and the operation

$$ v\longmapsto \frac{v^2}{2}. $$

Represent the constants $1$ and $0$ by the pairs $(2,1)$ and $(1,1)$, respectively. The constant $2$ is computed as $1+1$.

If two represented values are $A-B$ and $C-D$, addition and subtraction use

$$ (A-B)+(C-D)=(A+C)-(B+D), $$

$$ (A-B)-(C-D)=(A+D)-(B+C). $$

Multiplication uses

$$ \begin{aligned} P&=\frac{(A+C)^2}{2}+\frac{(B+D)^2}{2},\\ N&=\frac{(A+D)^2}{2}+\frac{(B+C)^2}{2}. \end{aligned} $$

Indeed, expansion gives

$$ P-N=AC+BD-AD-BC=(A-B)(C-D). $$

Each original gate introduces only constantly many new gates. All new values are nonnegative, and the transformed circuit has polynomial size.

Append an addition of $1$ to each of its two output values. This preserves their difference and ensures that both outputs are gate outputs.

Write the resulting circuit as

$$ v_0=1,\qquad v_1,\ldots,v_n, $$

where every gate is either

$$ v_i=v_j+v_k $$

or

$$ v_i=\frac{v_j^2}{2}, $$

with predecessor indices smaller than $i$. Let $p$ and $r$ be the two output indices. Their difference equals the integer output $z$ of the original circuit. Hence

$$ z>0\quad\Longleftrightarrow\quad v_p-v_r\ge1. $$

2.2 A convex relaxation whose minimum equals a circuit value

Introduce variables $x_0,\ldots,x_n$ and impose $x_0=1$.

For an addition gate $i$ with predecessors $j,k$, impose

$$ A_i(\mathbf x):=x_i-x_j-x_k\ge0. $$

For a squaring gate $i$ with predecessor $j$, impose

$$ M_i(\mathbf x):= \begin{pmatrix} 2x_i&x_j\\ x_j&1 \end{pmatrix} \succeq0. $$

The matrix constraint is equivalent to

$$ x_i\ge\frac{x_j^2}{2}. $$

Every feasible vector satisfies $x_i\ge v_i$. To prove this, proceed in gate order. The source coordinate equals $v_0=1$. Addition preserves the claimed lower bounds. At a squaring gate, the predecessor is nonnegative, and squaring is increasing on the nonnegative reals, so

$$ x_i\ge\frac{x_j^2}{2}\ge\frac{v_j^2}{2}=v_i. $$

The exact circuit vector $\mathbf v$ is feasible. Therefore, for every output index $o$,

$$ \min_{\mathbf x\text{ feasible}}x_o=v_o. $$

We next express attainment of this exact minimum through additional convex constraints.

2.3 Explicit dual certificates

Let $\boldsymbol\varepsilon_i$ denote the coordinate vectors in $\mathbb R^{n+1}$. For an addition gate, put

$$ \mathbf a_i=\boldsymbol\varepsilon_i-\boldsymbol\varepsilon_j-\boldsymbol\varepsilon_k. $$

For a squaring gate with predecessor $j$, and a symmetric matrix $Y$, define

$$ B_i^*(Y)=2Y_{11}\boldsymbol\varepsilon_i+2Y_{12}\boldsymbol\varepsilon_j. $$

For an output $o$, introduce:

Impose the affine equation

$$ \boldsymbol\varepsilon_o = \eta\boldsymbol\varepsilon_0 +\sum_{i\text{ addition}}\lambda_i\mathbf a_i +\sum_{i\text{ squaring}}B_i^*(Y_i). $$

Define the corresponding scalar

$$ D_o=\eta-\sum_{i\text{ squaring}}(Y_i)_{22}. $$

For any primal feasible $\mathbf x$, substitution into the affine equation gives

$$ x_o-D_o = \sum_{i\text{ addition}}\lambda_i A_i(\mathbf x) +\sum_{i\text{ squaring}} \langle Y_i,M_i(\mathbf x)\rangle, $$

where $\langle U,V\rangle=\operatorname{tr}(UV)$.

Every term on the right is nonnegative. For the matrix terms, if $U,V$ are positive semidefinite, diagonalizing $V$ gives

$$ \operatorname{tr}(UV) =\sum_k \gamma_k\,\mathbf w_k^{\mathsf T}U\mathbf w_k\ge0, $$

where $\gamma_k\ge0$ are the eigenvalues of $V$. Thus

$$ D_o\le x_o. $$

In particular, testing the feasible vector $\mathbf v$ gives $D_o\le v_o$.

There also exists a dual certificate with $D_o=v_o$. Its construction is explicit.

Initialize weights $w_o=1$ and all other weights to zero. Process gates in reverse order. At an addition gate $i$, add $w_i$ to each predecessor’s weight, counting a repeated predecessor twice. At a squaring gate $i$ with predecessor $j$, add $w_iv_j$ to $w_j$.

Set

$$ \eta=w_0,\qquad \lambda_i=w_i $$

for addition gates, and for squaring gates set

$$ Y_i=\frac{w_i}{2} \begin{pmatrix} 1&-v_j\\ -v_j&v_j^2 \end{pmatrix}. $$

All weights are nonnegative. Each $Y_i$ is positive semidefinite because it is a nonnegative multiple of an outer product.

The reverse propagation ensures the required affine equation: the contribution of a squaring gate is

$$ B_i^*(Y_i) =w_i\boldsymbol\varepsilon_i-w_iv_j\boldsymbol\varepsilon_j, $$

and the addition-gate contribution distributes $w_i$ to its two predecessors.

At $\mathbf v$, each addition constraint is tight. For a squaring gate,

$$ M_i(\mathbf v)= \begin{pmatrix} v_j^2&v_j\\ v_j&1 \end{pmatrix}, $$

which annihilates $(1,-v_j)^{\mathsf T}$. Hence

$$ \langle Y_i,M_i(\mathbf v)\rangle=0. $$

The displayed identity for $x_o-D_o$ therefore gives $D_o=v_o$.

Consequently, imposing both primal and dual feasibility and the affine equality

$$ x_o=D_o $$

forces

$$ x_o=D_o=v_o. $$

This argument uses explicit certificates and weak duality; it requires no dual-attainment theorem.

2.4 Homogenization

Use one primal vector and separate dual certificates for outputs $p$ and $r$.

Introduce a scaling variable $\alpha$, scaled primal variables $X_i$, and scaled dual variables $H^o,\Lambda_i^o,Z_i^o$, for $o\in\{p,r\}$. Impose

$$ X_0=\alpha, $$

$$ X_i-X_j-X_k\ge0 \qquad\text{for addition gates}, $$

and

$$ \begin{pmatrix} 2X_i&X_j\\ X_j&\alpha \end{pmatrix} \succeq0 \qquad\text{for squaring gates}. $$

For each output $o$, impose

$$ \Lambda_i^o\ge0,\qquad Z_i^o\succeq0, $$

$$ \alpha\boldsymbol\varepsilon_o = H^o\boldsymbol\varepsilon_0 +\sum_{i\text{ addition}}\Lambda_i^o\mathbf a_i +\sum_{i\text{ squaring}}B_i^*(Z_i^o), $$

and

$$ X_o=H^o-\sum_{i\text{ squaring}}(Z_i^o)_{22}. $$

Finally, impose

$$ X_p-X_r\ge\alpha. $$

If $\alpha>0$, dividing every scaled variable by $\alpha$ produces the primal–dual systems above. They force

$$ \frac{X_p}{\alpha}=v_p,\qquad \frac{X_r}{\alpha}=v_r. $$

Therefore this system, with $\alpha>0$, is feasible exactly when $v_p-v_r\ge1$.

2.5 Bounding every variable without allowing zero scaling

We now enforce positive scaling while restricting every scalar coordinate to $[-1,1]$.

First bound the magnitudes of the explicit unscaled witnesses. Induction on the gate index gives

$$ 0\le v_i\le R,\qquad R=2^{2^n}. $$

Indeed, addition increases the current maximum by at most a factor of $2$, while a squaring gate increases it by at most its square.

Each reverse-propagated weight is a sum over paths in the circuit. There are at most $2^n$ such paths to any fixed node: unfolding the predecessor choices gives a binary tree of depth at most $n$. Each path has at most $n$ factors, and every factor is at most $R$. Hence

$$ 0\le w_i\le2^nR^n. $$

The absolute values of the primal coordinates, the scalar dual coordinates, and all matrix entries are therefore bounded by

$$ T=2^nR^{n+2}. $$

Set $h=2n+4$. For $n\ge1$,

$$ \log_2T=n+(n+2)2^n\le2^h. $$

Thus

$$ \delta:=2^{-2^h} $$

satisfies $\delta T\le1$.

The reduction does not write $\delta$ as a rational input. Instead introduce $z_0,\ldots,z_h$, impose

$$ z_0=\frac12, $$

$$ \begin{pmatrix} z_{k+1}&z_k\\ z_k&1 \end{pmatrix} \succeq0 \qquad(0\le k<h), $$

and

$$ \alpha\ge z_h. $$

The matrix constraints imply $z_{k+1}\ge z_k^2$. Induction gives

$$ \alpha\ge z_h\ge2^{-2^h}=\delta>0. $$

Require every scalar coordinate in the entire system, including matrix entries, to lie in $[-1,1]$.

If the original circuit output is positive, take the explicit primal–dual witnesses, multiply all their coordinates by $\delta$, and choose

$$ z_k=2^{-2^k},\qquad \alpha=\delta. $$

All coordinates lie in $[-1,1]$, and every constraint holds.

Conversely, any feasible bounded system has $\alpha>0$. Division by $\alpha$ gives the original exact certificates and implies $v_p-v_r\ge1$, hence positivity of the original integer output.

We have proved:

Lemma. $\mathrm{PosSLP}$ reduces in polynomial time to feasibility of a system on a rational box $[-1,1]^d$, consisting only of affine constraints and positive-semidefiniteness constraints on affine symmetric matrices of order $2$.

The number of variables and constraints is polynomial in the circuit size. All coefficients have polynomial bit length. The doubly exponentially small quantity $\delta$ is enforced by a linear-length chain, rather than written into the input.

3. Embedding bounded matrix feasibility into SCPM loss

We now reduce every system from the preceding lemma to the stated SCPM decision problem.

3.1 Writing the constraints as convex violations

Split every affine equality into two affine inequalities. Write every affine inequality as

$$ f(\mathbf u)\le0 $$

with $f$ affine.

For an affine symmetric matrix

$$ \begin{pmatrix} a(\mathbf u)&b(\mathbf u)\\ b(\mathbf u)&c(\mathbf u) \end{pmatrix}, $$

positive semidefiniteness is equivalent to

$$ \sqrt{(a(\mathbf u)-c(\mathbf u))^2+4b(\mathbf u)^2} -a(\mathbf u)-c(\mathbf u)\le0. $$

Its eigenvalues are

$$ \frac{a+c\pm\sqrt{(a-c)^2+4b^2}}{2}, $$

so the inequality is exactly nonnegativity of the smaller eigenvalue.

Thus the bounded system is

$$ \mathbf u\in[-1,1]^d,\qquad f_1(\mathbf u)\le0,\ldots,f_s(\mathbf u)\le0, $$

where each $f_k$ is affine or has the form

$$ f_k(\mathbf u)=\sqrt{S_k(\mathbf u)}-T_k(\mathbf u). $$

Here $S_k$ is the sum of squares of two rational affine expressions, and $T_k$ is rational affine. Every $f_k$ is finite, continuous, and convex globally: the square root is a Euclidean norm of an affine map.

3.2 Society and calibration

Set

$$ \tau=d+1,\qquad N=\tau+1. $$

For $1\le j\le\tau$, use the bundle

$$ \mathbf a_j=\mathbf e-\mathbf e_j. $$

Choose dyadic masses

$$ \mu_j=2^{-j}\quad(1\le j<\tau), \qquad \mu_\tau=2^{-(\tau-1)}, $$

and limits $\ell_j=1/\mu_j$. The masses are positive and sum to $1$, and every aggregate bound is $1$.

The bundles are distinct, so the society has support size exactly $\tau$.

For arbitrary holdings define

$$ r_j=q_N-q_j. $$

On feasible allocations,

$$ q_N=\sum_{j=1}^{\tau}x_j,\qquad q_j=q_N-x_j,\qquad r_j=x_j. $$

In particular, $q_N$ is a largest holdings coordinate.

For the first $d$ coordinates put

$$ u_j=2r_j-1. $$

As the allocations range over their bounds, $\mathbf u$ ranges over $[-1,1]^d$. The final coordinate $r_\tau$ will calibrate the cost at the origin.

Let $\mathbf u^*=(-1,\ldots,-1)$. Choose a positive integer $B$ exceeding every $f_k(\mathbf u^*)$. This can be done in polynomial time without evaluating square roots. For a matrix violation, the rational upper bound

$$ |a(\mathbf u^*)-c(\mathbf u^*)| +2|b(\mathbf u^*)| +|a(\mathbf u^*)+c(\mathbf u^*)| $$

dominates its value. Affine violations are evaluated exactly. Taking $1$ plus the ceiling of the maximum of these bounds and $0$ produces a suitable $B$ of polynomial bit length.

Define

$$ g(\mathbf r)= \max\left( 0,\, B(1-r_\tau),\, f_1(\mathbf u),\ldots,f_s(\mathbf u) \right), $$

and

$$ C(\mathbf q)=q_N+g(\mathbf r). $$

3.3 Verification of the cost-function promises

Every function inside the maximum defining $g$ is finite, continuous, and convex. Hence $g$, and therefore $C$, are finite, continuous, and convex globally.

Translation by $a\mathbf e$ leaves every difference $r_j=q_N-q_j$ unchanged and increases $q_N$ by $a$. Thus

$$ C(\mathbf q+a\mathbf e)=C(\mathbf q)+a $$

for all $\mathbf q$ and all real $a$.

These are exactly the required cost-function properties. The utility representation can also be verified directly: $u(\mathbf s)=-C(-\mathbf s)$ is continuous and concave, and cash invariance gives

$$ z-u(z\mathbf e-\mathbf q) =z+C(\mathbf q-z\mathbf e) =C(\mathbf q) $$

for every real $z$.

3.4 A quantifier-free quadratic rational graph formula

It remains essential to supply the graph in the required encoding.

After substituting $u_j=2r_j-1$, write the polynomial candidates in $g$ as $p_k(\mathbf r)$. These include $0$, $B(1-r_\tau)$, and all affine violations. Write its norm candidates as

$$ \sqrt{S_j(\mathbf r)}-T_j(\mathbf r), $$

where each $S_j$ is a sum of squares of two rational affine expressions.

For graph variables $(\mathbf q,y)$, use the affine expressions

$$ r_j=q_N-q_j,\qquad H=y-q_N $$

as notation, not additional variables. Supply

$$ \begin{aligned} &\bigwedge_k(H-p_k(\mathbf r)\ge0)\\ {}\land{}& \bigwedge_j\left( H+T_j(\mathbf r)\ge0 \ \land\ (H+T_j(\mathbf r))^2-S_j(\mathbf r)\ge0 \right)\\ {}\land{}& \left( \bigvee_k(H-p_k(\mathbf r)=0) \ \lor\ \bigvee_j\bigl((H+T_j(\mathbf r))^2-S_j(\mathbf r)=0\bigr) \right). \end{aligned} $$

Because $S_j(\mathbf r)\ge0$ globally, its two inequalities are equivalent to

$$ H\ge\sqrt{S_j(\mathbf r)}-T_j(\mathbf r). $$

In the final disjunction, equality for a norm candidate selects the nonnegative root, since $H+T_j(\mathbf r)\ge0$ is already imposed. Therefore the formula says precisely that $H$ dominates every candidate and equals an active candidate. This is equivalent to $H=g(\mathbf r)$, hence to $y=C(\mathbf q)$.

Expanding the affine expressions produces polynomials of degree at most $2$. A squared affine expression has at most quadratically many monomials in the number of variables. The entire formula therefore has polynomial sparse encoding length and polynomial coefficient bit length. It contains no auxiliary quantified variables and no irrational coefficients.

3.5 Exact loss calculation

At the origin, $\mathbf r=\mathbf0$ and $\mathbf u=\mathbf u^*$. The calibration candidate equals $B$, and all other candidates are at most $B$. Hence

$$ C(\mathbf0)=B. $$

For feasible allocations, outcome $N$ has a largest holdings coordinate. Therefore

$$ \begin{aligned} W &=\max_{\mathbf x\in[0,1]^\tau} \bigl(q_N-C(\mathbf q)+B\bigr)\\ &=B-\min_{\mathbf r\in[0,1]^\tau}g(\mathbf r). \end{aligned} $$

Since $g\ge0$, we have $W\le B$. Continuity and compactness ensure that its minimum is attained.

Moreover,

$$ g(\mathbf r)=0 $$

holds exactly when

$$ r_\tau=1,\qquad f_k(2r_1-1,\ldots,2r_d-1)\le0 \quad\text{for every }k. $$

Thus, with the integer threshold $K=B$,

$$ W\ge K \quad\Longleftrightarrow\quad \text{the bounded convex system is feasible}. $$

Every stage of this construction has polynomial size. Combining it with Section 2 proves the stated $\mathrm{PosSLP}$ reduction.

4. What is proved and what remains open

The exact decision problem is $\mathrm{PosSLP}$-hard, even with unit aggregate bounds and a quadratic rational graph formula, and it belongs to $\exists\mathbb R\subseteq\mathrm{PSPACE}$.

The lower bound arises through exact convex feasibility. All constraints used in the reduction are convex, and the final cost satisfies its promises on the whole space.

The requested classification remains open in this write-up. A reduction from $\mathrm{PosSLP}$ supplies neither an exact polynomial-time algorithm nor a reduction from an established $\mathrm{NP}$-hard problem.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Assessment: correct partial progress. The stated $\mathrm{PosSLP}$ reduction and $\exists\mathbb R$ upper bound withstand verification. I found no false central step or substantive gap in those arguments. They do not resolve the requested $\mathrm P$ versus $\mathrm{NP}$-hardness classification, as the prover explicitly acknowledges.

The distinction matters: the additional theorem is supported, but the assigned problem remains unsettled.

1. Attainment and the upper bound

Allocation domain and attainment

The bounds $b_t=\mu_t\ell_t$ are finite and nonnegative under the task’s assumptions. Consequently,
$$ X=\prod_{t=1}^{\tau}[0,b_t] $$
is nonempty and compact, including when some bounds vanish.

Each function
$$ F_i(\mathbf x)=(A\mathbf x)_i-C(A\mathbf x)+C(\mathbf0) $$
is continuous. Thus its maximum exists, and taking the maximum over finitely many outcomes preserves attainment. This correctly handles the exact threshold case $W=K$.

Convex optimization formulation

Since composition with a linear map preserves convexity, $C(A\mathbf x)-(A\mathbf x)_i$ is convex. The displayed identity
$$ W=C(\mathbf0)-\min_{1\le i\le N}\min_{\mathbf x\in X} \bigl(C(A\mathbf x)-(A\mathbf x)_i\bigr) $$
has the correct signs and quantifiers.

This formulation does not itself provide an exact polynomial-time algorithm. The prover correctly avoids claiming otherwise.

For $N=1$, cash invariance indeed implies $C(q)=q+C(0)$ and hence $W=0$.

Existential encoding

On promised inputs, the graph formula uniquely determines both $y=C(\mathbf q)$ and $y_0=C(\mathbf0)$. The allocation equations and final disjunction therefore express precisely the existence of an allocation and outcome whose loss is at least $K$. Attainment establishes equivalence with $W\ge K$.

The treatment of binary exponents is valid. Repeated squaring requires polynomially many arithmetic gates in the exponent bit length. Globally conjoined gate equations uniquely determine their outputs, so introducing existential gate variables preserves Boolean combinations, including negations. Rational coefficients and the products defining $b_t$ have polynomial encoding length; clearing denominators also has polynomial bit cost.

Thus the reduction to ordinary existential real feasibility is polynomial in the supplied input length. The $\exists\mathbb R$ membership claim is valid on promised inputs.

The invoked theorem—that existential real sentences with polynomial equalities and inequalities can be decided in polynomial space—applies after this conversion. The cited [Canny report](https://www2.eecs.berkeley.edu/Pubs/TechRpts/1988/6041.html) supports this theorem. The $\mathrm{PSPACE}$ upper bound is justified.

2. Arithmetic-circuit encoding

Signed-to-nonnegative transformation

The constant pairs $(2,1)$ and $(1,1)$ represent $1$ and $0$ correctly. The addition and subtraction rules preserve the represented differences.

The multiplication identity is also correct:
$$ \frac{(A+C)^2+(B+D)^2-(A+D)^2-(B+C)^2}{2} =AC+BD-AD-BC. $$

Every transformed value is nonnegative, and each original gate introduces only constantly many gates. Appending $1$ to both outputs preserves their difference.

Although individual transformed values may be nonintegral, their output difference remains the original integer $z$. Therefore
$$ z>0\quad\Longleftrightarrow\quad v_p-v_r\ge1 $$
is valid. No integrality of the separate outputs is needed.

Primal relaxation

The matrix constraint
$$ \begin{pmatrix} 2x_i&x_j\\ x_j&1 \end{pmatrix}\succeq0 $$
is exactly equivalent to $x_i\ge x_j^2/2$.

The gate-order induction establishing $x_i\ge v_i$ is valid. At each squaring gate, the induction hypothesis gives $x_j\ge v_j\ge0$, which supplies the necessary domain restriction for monotonicity of squaring.

The exact circuit vector is feasible. Consequently, every output coordinate has attained minimum $v_o$, even though this initial feasible region is unbounded.

3. Dual certificates and homogenization

Weak-duality identity

The definition
$$ B_i^*(Y)=2Y_{11}\boldsymbol\varepsilon_i+2Y_{12}\boldsymbol\varepsilon_j $$
correctly accounts for the two off-diagonal contributions to the matrix inner product.

Substitution into the affine certificate equation gives the stated identity for $x_o-D_o$, with the correct sign for the constant matrix entry. Nonnegative affine multipliers and positive semidefinite matrix multipliers make every term nonnegative. The supplied trace argument verifies the matrix terms without assuming the matrices commute.

Thus $D_o\le x_o$, and evaluating at $\mathbf v$ gives $D_o\le v_o$.

Explicit optimal certificates

Reverse propagation uses the correct multiplier at each gate:

The matrix
$$ Y_i=\frac{w_i}{2} \begin{pmatrix} 1&-v_j\\ -v_j&v_j^2 \end{pmatrix} $$
is positive semidefinite, and its contribution to the affine equation has the stated coordinates and signs. The reverse propagation accounts for all coordinates, including the source coordinate.

At the exact circuit vector, affine residuals vanish and the stated vector lies in the kernel of each squaring matrix. Hence the matrix inner products vanish as claimed, yielding $D_o=v_o$.

Combining primal feasibility, dual feasibility, and $x_o=D_o$ therefore forces exact output evaluation. There is no unverified appeal to strong duality or dual attainment.

Homogenization

Every displayed scaled constraint divides by $\alpha>0$ into its corresponding unscaled constraint. This includes the primal matrix constraints, the affine dual equations, and the primal–dual equality.

Using one primal vector and separate certificates for the two outputs is consistent. The final inequality then expresses exactly $v_p-v_r\ge1$.

4. Bounded witnesses and strictly positive scaling

The witness bounds are sufficient:

Appending output gates ensures the construction has $n\ge1$. For this range, the stated inequality
$$ n+(n+2)2^n\le2^{2n+4} $$
holds, so $\delta T\le1$ follows.

The scaling chain is correctly indexed:
$$ z_0=\frac12,\qquad z_{k+1}\ge z_k^2 $$
forces $z_h\ge2^{-2^h}$. Hence $\alpha\ge z_h$ excludes zero scaling.

For positive circuit output, the explicit scaled witnesses and the stated choices of $z_k$ satisfy the box restrictions and every constraint. Conversely, any feasible bounded system has positive $\alpha$ and therefore decodes to exact output certificates.

The tiny number $\delta$ is used only to establish witness existence; its enormous explicit rational encoding is never part of the reduction. The bounded convex feasibility lemma is justified.

5. Embedding into the SCPM instance

Convex violations

The smaller-eigenvalue formula gives the correct positive-semidefiniteness test. Each resulting matrix violation is a Euclidean norm of an affine map minus an affine function, so it is globally finite, continuous, and convex.

Splitting affine equalities into two inequalities preserves feasibility.

Society and calibration

The dyadic masses are positive and sum to $1$. Their reciprocal limits give aggregate purchase bounds exactly equal to $1$, with polynomial encoding length.

The bundles are distinct, so $\tau$ is genuinely the support size. Their allocation identities
$$ q_N=\sum_jx_j,\qquad q_j=q_N-x_j,\qquad r_j=x_j $$
are correct. Since allocations are nonnegative, $q_N$ is a largest holdings coordinate.

The calibration bound for each matrix violation dominates its value at $\mathbf u^*$. The proposed integer $B$ is strictly positive, exceeds all those values, and has polynomial bit length.

Global cost-function promises

The function $g$ is a finite maximum of globally continuous convex functions. Composing it with the linear differences $\mathbf r$ and adding $q_N$ gives a globally finite continuous convex cost.

Cash translation leaves those differences invariant, establishing the required cash-invariance identity for every real translation. The optional utility representation also has the correct signs.

No coordinatewise monotonicity assumption is introduced.

Quantifier-free graph formula

For each norm candidate, the two inequalities impose both the nonnegative-root condition and domination. Since $S_j\ge0$ globally, they are equivalent to the stated comparison with $\sqrt{S_j}$.

The final disjunction enforces equality with at least one candidate. Its norm branches cannot select the negative root because the nonnegative-root condition is already conjoined.

Thus the formula describes exactly the graph of $C$, without auxiliary quantified variables. Substitution and expansion preserve degree at most $2$, polynomially many sparse monomials, and polynomial coefficient bit length.

Exact loss calculation

Calibration gives $C(\mathbf0)=B$. Since $q_N$ is always a largest holdings coordinate, maximizing over outcomes gives
$$ W=B-\min_{\mathbf r\in[0,1]^\tau}g(\mathbf r). $$

The minimum is attained and nonnegative. On this allocation box, $g(\mathbf r)=0$ is equivalent to the original feasibility constraints together with $r_\tau=1$.

Consequently, the threshold $K=B$ gives the claimed exact equivalence. Both positive and nonpositive circuit instances map to cost functions satisfying the promises. The complete many-one reduction is valid.

6. Issue and actionable feedback

Major issue relative to the assignment: the requested classification remains unresolved. Neither the $\mathrm{PosSLP}$ lower bound nor the $\exists\mathbb R$ upper bound establishes membership in $\mathrm P$ or $\mathrm{NP}$-hardness.

This is a missing result, not a defect in the supplied reduction, and the prover reports it honestly. Completing the assignment requires either an exact polynomial-time decision algorithm under the stated encoding or a valid $\mathrm{NP}$-hardness argument. Expositional clarification alone cannot close this issue.

No additional clarification is needed to verify the partial results as written.

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