← back to the atlas

Fine-Grained Liquid Democracy for Cumulative Ballots (aamas24-00119)

Answer: —

The anchor (named result in the paper)

Theorem 8 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateWe can find an 𝜖-strong approximation of a solution 𝒙∈R𝑛𝑚 of an instance of FGLD for CBs with 𝑛 voters and 𝑚 candi- dates satisfying any of (EP), (EP-TI), or (WCC) in time polylog(𝒘, 𝒅, 1/𝜖)· 𝑠𝑂(𝑠) · poly(𝑛,𝑚), where 𝑠 is the number of vertices in largest SCDC.

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

The continuous mirror question, as graded

Given candidates \(C\), finite voter types \(T\), rational population masses \(\mu\in\mathbb{Q}_{\ge 0}^{T}\) with \(\sum_{t\in T}\mu_t=1\), type partitions \(\mathcal{S}_t\), bundle budgets \(b_{t,S}\), defaults \(\mathbf d_{t,S}\), weights \(w_{t,S}\), and role delegates \(\delta(t,S)\in T\), find an \(\epsilon\)-strong approximation to a resolved profile \(x=(x_t)_{t\in T}\) satisfying \(\sum_{c\in C}x_{t,c}=1\), \(\sum_{c\in S}x_{t,c}=b_{t,S}\), and \(x_{t,S}=b_{t,S}\frac{\mathbf d_{t,S}+w_{t,S}x_{\delta(t,S),S}}{\left\|\mathbf d_{t,S}+w_{t,S}x_{\delta(t,S),S}\right\|_1}\) for every \(t,S\), together with the aggregate ballot \(z_c=\sum_{t\in T}\mu_t x_{t,c}\).

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

A society is given by its support: a list \(T\) of \(\tau\ge1\) types with positive binary rational masses \(\mu_t\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types. Let \(C\) contain \(m\ge1\) candidates.
Each type \(t\) specifies a partition \(\mathcal S_t\) of \(C\) into nonempty bundles. Each bundle \(S\) has rational budget \(b_{t,S}\ge0\), default \(\mathbf d_{t,S}\in\mathbb Q_{\ge0}^{S}\) with \(\sum_{c\in S}d_{t,S,c}=b_{t,S}\), positive rational weight \(w_{t,S}\), and delegate \(\delta(t,S)\in T\); budgets sum to \(1\) for each type. Self-delegation requires \(|S|=1\), and zero-budget bundles must be self-delegated singletons.
A resolved profile \(x^*\in\mathbb R_{\ge0}^{T\times C}\) satisfies \(\sum_{c\in C}x^*_{t,c}=1\), \(\sum_{c\in S}x^*_{t,c}=b_{t,S}\), and, for every positive-budget bundle, \(x^*_{t,S}=b_{t,S}(\mathbf d_{t,S}+w_{t,S}x^*_{\delta(t,S),S})/\|\mathbf d_{t,S}+w_{t,S}x^*_{\delta(t,S),S}\|_1\), where subscripts by bundles denote restrictions. Zero-budget coordinates equal zero.
Given binary rational \(0<\epsilon<1\), the computational problem is to find a rational nonnegative profile \(\widehat x\) respecting the budgets exactly and satisfying \(\|\widehat x-x^*\|_\infty\le\epsilon\) for some resolved profile, together with \(\widehat z_c=\sum_{t\in T}\mu_t\widehat x_{t,c}\). Let \(L\) be the total binary input length.
For comparison with parameterized bounds, let \(s\) be the largest strongly connected component size in the graph on \(T\times C\), with edges \((t,c)\to(\delta(t,S),c')\) for every \(S\in\mathcal S_t\) and \(c,c'\in S\).
Can this strong-approximation problem be solved in time polynomial in \(m,\tau,L,\log(1/\epsilon)\), or is it NP-hard under polynomial-time Turing reductions?
For finite lists of voters, an algorithm with dependence \(s^{O(s)}\), polynomial dependence on the voter and candidate counts, and polylogarithmic dependence on numerical data and inverse accuracy is claimed; that work explicitly leaves computational hardness unproved. [Source](https://aamas.csc.liv.ac.uk/Proceedings/aamas2024/pdfs/p1029.pdf)
The literature search found no verified NP-hardness or W[1]-hardness result for this resolution problem, nor a general polynomial-time classification of the finitely supported mass formulation.

Modeling choices made when packaging the task

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

Partial resolution: hardness with a fixed number of candidates

I do not establish either a general polynomial-time algorithm or $\mathrm{NP}$-hardness under polynomial-time Turing reductions.

I prove a stronger version of the verified lower bound in the notes:

Theorem A. The strong-approximation problem is $\mathrm{PPAD}$-hard for the fixed accuracy $\epsilon=2^{-24}$, even under all of the following restrictions:

Thus every resolved profile in these instances is strictly positive. The masses have polynomial encoding length but need not belong to a fixed finite set.

I also prove an exact polynomial-time result:

Theorem B. Suppose every nonsingleton bundle $S$ is a union of bundles in its delegate’s partition. Then the society has a unique resolved profile, this profile is rational, and it can be computed exactly in polynomial time. In particular, this holds for every instance with at most two candidates.

Neither theorem settles the requested general classification.

1. Existence, masses, and rational answers

Let $K$ denote the set of nonnegative profiles satisfying all bundle budgets. The defaults give an element of $K$. Because the bundles partition the candidates and their budgets sum to one, the row-sum constraints follow from the bundle constraints.

The set $K$ is compact and convex. Define $F:K\to K$ by the resolution rule. For each positive-budget bundle,

$$ \left\|\mathbf d_{t,S}+w_{t,S}x_{\delta(t,S),S}\right\|_1 = b_{t,S}+w_{t,S}\sum_{c\in S}x_{\delta(t,S),c} \ge b_{t,S}>0. $$

Consequently, $F$ is continuous. Its output is nonnegative and has the prescribed total on each bundle. Brouwer’s fixed-point theorem therefore supplies a resolved profile.

The masses do not appear in $F$. Relabeling the $\tau$ support entries as $\tau$ voters leaves the resolution equations unchanged; no expansion according to mass denominators is required.

Short rational strong approximations exist. Given a resolved profile, choose an integer $r$ with $m2^{-r}\le\epsilon$. In each bundle, round all but one coordinate down to multiples of $2^{-r}$, and assign the last coordinate the exact budget remainder. The remainder is nonnegative. Its error is at most $(|S|-1)2^{-r}$, and the other errors are below $2^{-r}$. The resulting profile has polynomial encoding length and respects budgets exactly.

Finally, aggregation is exact rational arithmetic. If $\widehat x$ approximates $x^*$ as required, then

$$ \left|\widehat z_c-\sum_t\mu_t x^*_{t,c}\right| \le \sum_t\mu_t|\widehat x_{t,c}-x^*_{t,c}| \le\epsilon. $$

2. A bounded-use primitive circuit problem

Write

$$ [u]_+=\max\{0,u\}, \qquad \operatorname{clip}(u)=\min\{1,\max\{0,u\}\}. $$

Consider circuits with variables in $[0,1]$, exactly two constant nodes of values $1/4$ and $1/2$, and primitive gates

$$ N(u)=1-u, \qquad R(u,v)=[1-u-v]_+. $$

Every nonconstant node has exactly one producing gate. All nodes within a primitive gate are distinct. Constants may be used arbitrarily often.

Lemma 1. Finding an assignment satisfying every primitive gate within additive error $\delta=1/128$ is $\mathrm{PPAD}$-hard, even when each nonconstant node is an input to at most two primitive gates.

2.1 Source problem

We use the following established result: Pure-Circuit remains $\mathrm{PPAD}$-complete with gates NOR, PURIFY, and COPY, even when every node is the input of exactly one gate. Each node has exactly one producing gate, and nodes within a gate are distinct. This is the choice $(X,Y)=(\mathrm{COPY},\mathrm{NOR})$ in [Pure-Circuit, Corollary 2.3](https://arxiv.org/pdf/2209.15149).

Its labels are $\{0,1,\bot\}$. NOR must output $1$ on two zero inputs and $0$ if either input is $1$. PURIFY copies a pure input to both outputs and always has at least one pure output. COPY copies a pure input. These conditions are precisely those used below.

2.2 Doubling and ramps

The function $D(u)=\min\{1,2u\}$ has the implementation

$$ a=N(u),\qquad b=N(a),\qquad c=R(u,b),\qquad o=N(c). $$

At exact gate values, $b=u$ and $o=D(u)$.

When every primitive gate has error at most $\delta$, the errors of $a,b,c,o$ relative to their ideal values at the actual input $u$ are at most

$$ \delta,\qquad 2\delta,\qquad 3\delta,\qquad 4\delta. $$

Indeed, $N$ is one-Lipschitz, and changing either argument of $R$ changes its output by at most the change in that argument.

For either exact constant $t\in\{1/4,1/2\}$, implement

$$ T_t(u)=D\bigl(D(R(N(u),t))\bigr) =\operatorname{clip}(4(u-t)). $$

The initial $N,R$ pair has error at most $2\delta$. Since $D$ is two-Lipschitz and its implementation adds at most $4\delta$, the two doublings yield error bounds

$$ 8\delta,\qquad 20\delta. $$

Thus each ramp approximates $T_t$ within $20\delta$. The ideal ramp is four-Lipschitz.

2.3 Simulating the source gates

Decode a real variable using

$$ \ell(u)= \begin{cases} 0,&u\le1/4,\\ 1,&u\ge3/4,\\ \bot,&1/4<u<3/4. \end{cases} $$

Implement NOR by $T_{1/4}(R(u,v))$. Its ideal output is

$$ \operatorname{clip}(3-4(u+v)), $$

and its error is at most

$$ 20\delta+4\delta=24\delta=\frac3{16}<\frac14. $$

If both inputs decode to zero, $u+v\le1/2$, so the ideal output is one. If either decodes to one, $u+v\ge3/4$, so the ideal output is zero. The error bound preserves the required decoded outputs.

Implement PURIFY by

$$ T_{1/4}(u),\qquad T_{1/2}(u). $$

For $u\le1/4$, both ideal outputs are zero; for $u\ge3/4$, both are one. For every $u$, at least one ideal output is an endpoint: the second is zero when $u\le1/2$, and the first is one when $u\ge1/2$. Since

$$ 20\delta=\frac5{32}<\frac14, $$

the required decoded properties hold.

Implement COPY by $T_{1/4}(u)$. Its ideal output is zero for $u\le1/4$ and one for $u\ge3/4$, and the same error bound applies.

All internal nodes are fresh. Every ramp uses the same two designated constant nodes; no additional constant nodes are introduced. Each source output is the terminal node of its corresponding gadget.

These arguments use actual input values locally, so they remain valid in cyclic circuits.

2.4 Bounding the number of uses

Each original source node is consumed by exactly one source gate. Its primitive uses are:

Inside a doubling gadget, its input is used twice, and every other internal node is used once. Between successive gadgets, a node is used at most twice. Therefore every nonconstant primitive node is an input to at most two primitive gates.

The construction has linear size. Decoding any valid primitive assignment solves the source instance, proving Lemma 1.

3. Reusing candidates through a coloring

Construct an undirected graph on the nonconstant primitive nodes. Join two nodes when they occur together in a primitive gate.

A node has at most two neighbors from its producing gate. It occurs as an input in at most two gates, each contributing at most two further neighbors. Hence its degree is at most six.

Greedy coloring therefore gives colors $1,\ldots,7$: when a vertex is colored, at most six colors are forbidden. Assign the two constant nodes colors $8$ and $9$.

Let $\kappa(i)$ denote a node’s color. All nodes within every primitive gate have distinct colors. In particular, if $J_i$ is the input set of nonconstant node $i$, then the colors in $\{i\}\cup J_i$ are pairwise distinct.

Introduce exactly the candidates

$$ C=\{a_h,c_h:1\le h\le9\}\cup\{*\}. $$

For convenience, write

$$ a_i=a_{\kappa(i)},\qquad c_i=c_{\kappa(i)}. $$

Different circuit nodes may now refer to the same candidate pair. Within each gate, however, the relevant pairs are disjoint. This local disjointness is all the society construction needs.

4. Constructing the positive society

Fix the constants

$$ B=2^{-10},\qquad H=\frac14,\qquad W=2^{20}, \qquad \gamma=2^{-64}, \qquad k=\frac12-\frac HW. $$

Also set

$$ K=k+\frac HW=\frac12, \qquad \eta=\frac BW=2^{-30}, $$

$$ \alpha=\frac{BH}{B+K}=\frac1{2052}, \qquad \rho=\frac K{B+K}=\frac{512}{513}, \qquad \theta=\frac W{1+W}. $$

Every delegation weight is $W$.

Create a signal type $Q_i$ for every circuit node, and a feedback type $P_i$ for every nonconstant node.

4.1 Feedback types

For nonconstant node $i$, type $P_i$ has:

4.2 Signal types

For nonconstant node $i$, type $Q_i$ has:

For a constant node of value $t\in\{1/4,1/2\}$, type $Q_i$ instead has self-delegated singleton budgets

$$ \alpha t,\qquad H-\alpha t,\qquad 1-H $$

on $a_i,c_i,*$.

4.3 Positive padding

For each type, put every unused candidate in a self-delegated singleton of budget

$$ \zeta=\frac1{16\cdot19}. $$

Subtract the total padding budget from that type’s singleton budget on $*$.

The initial budget on $*$ is at least $1/4$ for every type. Padding costs at most $19\zeta=1/16$, so its final budget is positive.

Every singleton default equals its budget. Thus every bundle budget and every default coordinate is positive.

4.4 Validity and encoding

The coloring ensures that each type’s specified bundles are disjoint. Padding completes the partition. Budgets sum to one, and every nonsingleton delegates to another type. All self-delegations are singletons.

Feedback bundles have size at most three. Signal types have at most three nonsingleton bundles, each of size two. Since the candidate count is fixed, the possible padding counts are fixed. Consequently, all budgets, default entries, and weights range over fixed finite rational sets.

With $n$ circuit nodes, there are at most $2n$ types. Assign positive dyadic masses as follows. For

$$ D=2^{\lceil\log_2\tau\rceil}, $$

give the first $\tau-1$ types mass $1/D$ and the last mass $(D-\tau+1)/D$. These masses are positive, sum to one, and have polynomial encoding length.

The entire construction is polynomial-time.

5. Every resolved profile approximately evaluates the circuit

Fix any resolved profile. For a nonconstant node $i$, abbreviate

$$ p=x_{P_i,a_i},\qquad q=q_i=x_{Q_i,a_i},\qquad X=\sum_{j\in J_i}x_{Q_i,a_j}. $$

Every signal type gives total support $H$ to its own pair, including constant types.

The feedback and signal equations are

$$ p=B\frac{(1-\gamma)\eta+q}{\eta+q+X}, \qquad q=H\frac{p+\gamma H/W}{K+p}. $$

For every copied input pair,

$$ x_{Q_i,a_j} = \theta q_j+\frac{\gamma H}{1+W}. $$

Budget feasibility gives

$$ 0\le p\le B,\qquad 0\le q\le H,\qquad 0\le X\le2H. $$

5.1 A perturbed quadratic equation

Rewrite the first two equations as

$$ p=B\frac{\eta+q}{\eta+q+X}+v, \qquad q=\frac{Hp}{K+p}+u, $$

where

$$ |v|\le\gamma B\le\gamma, \qquad |u|\le\frac{\gamma H^2}{WK}\le\gamma. $$

Because $Hp/(K+p)$ is increasing in $p$,

$$ q\le\frac{HB}{K+B}+\gamma=\alpha+\gamma. $$

Set $A=\eta+q+X$. Cross-multiplication gives

$$ pA=B(\eta+q)+vA, \qquad Kq=p(H-q)+u(K+p). $$

Multiplying the second identity by $A$ and using the first yields

$$ (B+K)q^2+ \bigl((B+K)\eta+KX-BH\bigr)q-BH\eta =E, $$

where

$$ E=vA(H-q)+uA(K+p). $$

Here $A\le\eta+3H<1$, and $H+K+B<1$. Therefore

$$ |E| \le\gamma A\bigl((H-q)+(K+p)\bigr) \le\gamma. $$

Define

$$ z_i=\frac{q_i}{\alpha}, \qquad \lambda=\frac{\eta}{\alpha}=\frac{513}{2^{28}}, \qquad h=\frac{\rho X}{\alpha}. $$

Dividing the quadratic identity by $(B+K)\alpha^2$ gives

$$ \left|z_i^2+(\lambda+h-1)z_i-\lambda\right| \le\frac{\gamma}{(B+K)\alpha^2}. $$

5.2 Controlling the positive root

Let $r$ be the positive root of

$$ P(z)=z^2+(\lambda+h-1)z-\lambda. $$

Because $P(0)=-\lambda<0$ and $P(1)=h\ge0$, we have $0<r\le1$. The other root is $-\lambda/r$. Thus, for $z_i\ge0$,

$$ |z_i-r| = \frac{|P(z_i)|}{z_i+\lambda/r} \le \frac{|P(z_i)|}{\lambda}. $$

Using

$$ (B+K)\alpha^2\lambda=BH\eta=2^{-42}, $$

we obtain

$$ |z_i-r|\le2^{42}\gamma. $$

The root equation can also be written

$$ r\bigl(r-(1-h)\bigr)=\lambda(1-r). $$

If $h\le1$, this implies $r\ge1-h$. Put $e=r-(1-h)$. Then $0\le e\le r$, so

$$ e^2\le re=\lambda(1-r)\le\lambda. $$

If $h\ge1$, the same equation gives

$$ r^2\le r(r+h-1)=\lambda(1-r)\le\lambda. $$

Hence, in both cases,

$$ 0\le r-[1-h]_+\le\sqrt{\lambda}. $$

5.3 Clipped signals and gate errors

Define $\xi_i=\operatorname{clip}(z_i)$ for every node; constant nodes have $z_i=\xi_i=t$ exactly.

Clipping fixes $r\in[0,1]$ and is one-Lipschitz. Therefore

$$ |\xi_i-[1-h]_+| \le2^{42}\gamma+\sqrt{\lambda}. $$

The bound $q_i\le\alpha+\gamma$ implies

$$ 0\le z_i-\xi_i\le\frac{\gamma}{\alpha}. $$

The copy equations give

$$ h = \rho\theta\sum_{j\in J_i}z_j + \frac{\rho|J_i|\gamma H}{(1+W)\alpha}. $$

Since $|J_i|\le2$ and $0\le\xi_j\le1$,

$$ \left|h-\sum_{j\in J_i}\xi_j\right| \le 2(1-\rho\theta)+\frac{4\gamma}{\alpha}. $$

Positive part is one-Lipschitz. Combining the estimates proves that every nonconstant node satisfies

$$ \left| \xi_i-\left[1-\sum_{j\in J_i}\xi_j\right]_+ \right| \le \sigma+2^{42}\gamma+\frac{4\gamma}{\alpha}, $$

where

$$ \sigma=\sqrt{\lambda}+2(1-\rho\theta). $$

This conclusion holds for every resolved profile.

6. Decoding a strong-approximation answer

Call the strong-approximation oracle at $\epsilon=2^{-24}$. Its answer $\widehat x$ is within $\epsilon$ of some single resolved profile $x^*$.

Decode

$$ \widehat\xi_i = \operatorname{clip} \left(\frac{\widehat x_{Q_i,a_i}}{\alpha}\right). $$

For the clipped signals $\xi_i$ of $x^*$,

$$ |\widehat\xi_i-\xi_i|\le\frac{\epsilon}{\alpha}. $$

Constant nodes remain exact because their singleton budgets are respected exactly.

Each gate has at most two inputs. Consequently,

$$ \left| \widehat\xi_i- \left[1-\sum_{j\in J_i}\widehat\xi_j\right]_+ \right| \le \sigma+2^{42}\gamma+\frac{4\gamma}{\alpha} +\frac{3\epsilon}{\alpha}. $$

The constants satisfy

$$ \sqrt{\lambda}<\frac1{512}, $$

because $513/2^{28}<1/512^2$, and

$$ 2(1-\rho\theta) \le2(1-\rho)+2(1-\theta) < \frac1{256}+\frac1{2^{19}}. $$

Also,

$$ \frac{3\epsilon}{\alpha} =\frac{6156}{2^{24}}<\frac1{2048}, $$

and

$$ 2^{42}\gamma+\frac{4\gamma}{\alpha} = \frac{2^{42}+8208}{2^{64}} < 2^{-21}<\frac1{2048}. $$

Thus the total gate error is strictly below

$$ \frac1{512}+\frac1{256}+\frac1{2^{19}}+\frac1{1024} = \frac{3585}{524288} < \frac1{128}. $$

Lemma 1 now decodes a valid Pure-Circuit solution. The construction and decoding take polynomial time and use one oracle call. This proves Theorem A.

Because every default coordinate is positive, each resolved coordinate is positive as well: its resolution numerator contains a positive default term, and its denominator is positive.

The argument uses the required distance to an exact resolved profile directly. It does not identify strong approximation with a small fixed-point residual.

7. An exact polynomial-time class

Assume that for every nonsingleton bundle $S$ of type $t$, the set $S$ is a union of bundles in the partition of $u=\delta(t,S)$.

For every budget-feasible profile, the delegate’s total on $S$ is then the fixed rational number

$$ D_{t,S} = \sum_{\substack{R\in\mathcal S_u\\R\subseteq S}}b_{u,R}. $$

Hence the resolution equation becomes affine:

$$ x_{t,c} = \frac{b_{t,S}d_{t,S,c}}{b_{t,S}+w_{t,S}D_{t,S}} + \frac{b_{t,S}w_{t,S}}{b_{t,S}+w_{t,S}D_{t,S}} x_{u,c}. $$

We show that the resulting system has a unique solution.

For every coordinate in a positive-budget bundle, normalize by

$$ y_{t,c}=\frac{x_{t,c}}{b_{t,S_t(c)}}. $$

Singleton coordinates have $y_{t,c}=1$, irrespective of their delegate, because their budget fixes their only coordinate. Zero-budget coordinates are fixed at zero.

For a nonsingleton coordinate, let $R$ be the delegate’s bundle containing $c$. The union assumption implies $R\subseteq S$. If $b_{u,R}>0$, the normalized equation is

$$ y_{t,c} = \frac{d_{t,S,c}}{b_{t,S}+w_{t,S}D_{t,S}} + \beta_{t,c}y_{u,c}, $$

where

$$ \beta_{t,c} = \frac{w_{t,S}b_{u,R}} {b_{t,S}+w_{t,S}D_{t,S}} <1. $$

The strict inequality follows from $b_{u,R}\le D_{t,S}$ and $b_{t,S}>0$. If $b_{u,R}=0$, the delegate coordinate is zero and the coefficient can be omitted.

Thus the normalized equations have the form

$$ y=a+Ay, $$

where each row of $A$ has at most one nonzero entry, and every entry lies in $[0,1)$. There are finitely many rows, so

$$ q:=\|A\|_\infty<1. $$

If $y,y'$ are two solutions, then

$$ \|y-y'\|_\infty = \|A(y-y')\|_\infty \le q\|y-y'\|_\infty, $$

which forces $y=y'$. Section 1 supplies a resolved profile, so this unique linear-system solution respects all budgets and nonnegativity.

All coefficients are rational with polynomial encoding length. Exact rational linear algebra therefore computes the unique solution in polynomial time. To justify the bit bound, clear denominators row by row. If the resulting integer entries have at most $B_0$ bits and there are $n_0$ variables, determinants and minors have at most

$$ O(n_0B_0+n_0\log n_0) $$

bits, by expanding into at most $n_0!$ products. Fraction-free Gaussian elimination uses polynomially many operations on such minors. Therefore the solution and its computation have polynomial bit complexity.

This proves Theorem B.

For $m\le2$, every nonsingleton bundle is $C$, which is a union of every delegate’s bundles. Thus all such instances are exactly polynomial-time solvable. For $\tau=1$, self-delegation forces every bundle to be a singleton, so the profile is also fixed directly.

8. A general exponential upper bound

Let $N=m\tau$. On the nonnegative budget-feasible domain, resolved profiles are characterized by the quadratic equations

$$ x_{t,c} \left( b_{t,S}+w_{t,S}\sum_{c'\in S}x_{\delta(t,S),c'} \right) = b_{t,S} \left(d_{t,S,c}+w_{t,S}x_{\delta(t,S),c}\right) $$

for every positive-budget bundle and $c\in S$. Their denominators are strictly positive, so clearing them introduces no extra solutions.

Together with budgets and nonnegativity, there are $O(N)$ constraints of degree at most two. Clearing rational coefficient denominators gives polynomial total coefficient encoding length.

The strong-approximation theorem for quantifier-free real polynomial formulas, stated as [Proposition 5 in the AAMAS paper](https://aamas.csc.liv.ac.uk/Proceedings/aamas2024/pdfs/p1029.pdf), finds a rational point within $h$ of some satisfying assignment in time

$$ (PD)^{O(N)}\operatorname{poly}(L_{\mathrm{coeff}},\log(1/h)), $$

where $P$ is the number of constraints and $D$ their maximum degree. The hypotheses above give the required bounds.

Set $h=\epsilon/(m+1)$. Repair the returned rational vector $y$ separately on each positive-budget bundle of size $a$ and budget $b$. Put

$$ r_c=\max\{0,y_c\},\qquad R=\sum_{c\in S}r_c. $$

If $R>0$, output $\widehat x_c=br_c/R$. For the same exact profile $x^*$ approximated by $y$,

$$ |r_c-x_c^*|\le h,\qquad |R-b|\le ah, $$

and consequently

$$ |\widehat x_c-x_c^*| \le h+\frac{r_c}{R}|b-R| \le(a+1)h\le\epsilon. $$

If $R=0$, every exact coordinate in this bundle is at most $h$, so $b\le ah$. Output the default on that bundle. Both default and exact coordinates lie in $[0,b]$, giving error at most $ah\le\epsilon$.

Set zero-budget coordinates to zero. This repair preserves every budget exactly and remains close to the same exact resolved profile. Aggregation then completes the requested output.

The resulting general bound is

$$ (m\tau)^{O(m\tau)} \operatorname{poly}(L,\log(1/\epsilon)). $$

9. What remains open

Theorem A shows that a general polynomial-time algorithm would give polynomial-time algorithms for all $\mathrm{PPAD}$ search problems, even through instances with a fixed candidate count and strictly positive data.

It does not establish $\mathrm{NP}$-hardness under polynomial-time Turing reductions. Nor does the exponential upper bound establish the requested polynomial-time alternative. The construction does not bound the largest strongly connected component size $s$, so the lower bound creates no contradiction with the stated dependence on that parameter.

⟨structured verdict parsed — rendered above⟩

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

The output is a correct partial resolution. The proofs of Theorems A and B, and the exponential upper bound, withstand verification. However, they do not establish either alternative requested in USER_TASK: a general polynomial-time algorithm or $\mathrm{NP}$-hardness under polynomial-time Turing reductions.

The prover explicitly acknowledges this limitation. It is a limitation of coverage, rather than a false claim of having completed the assignment.

Step-by-step verification

1. Existence, masses, and rational approximations

Verified.

The budget-feasible set $K$ is nonempty because it contains the default profile. It is closed, bounded, and convex. Bundle budgets imply the row-sum constraints.

For every positive-budget bundle, nonnegativity gives

$$ \left\|\mathbf d_{t,S}+w_{t,S}x_{\delta(t,S),S}\right\|_1 = b_{t,S}+w_{t,S}\sum_{c\in S}x_{\delta(t,S),c} \ge b_{t,S}>0. $$

Thus the resolution map is continuous and maps $K$ into itself. Zero-budget coordinates are fixed at zero. The hypotheses needed for Brouwer’s theorem are satisfied, including nonemptiness.

The observation about masses is correct: masses affect aggregation but do not enter the resolution equations. Treating support entries as individually indexed voters does not require expanding rational masses into multiplicities.

The rational rounding procedure preserves every bundle budget. Rounding down the other coordinates increases the remainder coordinate by the sum of their rounding errors, so its error is at most $(|S|-1)2^{-r}$. The resulting encoding length is polynomial in the input length and $\log(1/\epsilon)$.

The aggregation error bound follows correctly from positivity and normalization of the masses.

2. Lemma 1: primitive-circuit hardness

Verified, including the external theorem.

The cited [Pure-Circuit paper, Corollary 2.3](https://arxiv.org/pdf/2209.15149) supplies the claimed $\mathrm{PPAD}$-complete source with gate set $\{\mathrm{PURIFY},\mathrm{COPY},\mathrm{NOR}\}$ and exactly one consuming gate per node. Its definitions also require one producing gate per node and distinct nodes within each gate. The prover uses the correct robust NOR, PURIFY, and COPY semantics.

The doubling implementation computes $\min\{1,2u\}$ exactly when its primitive equations are exact. Its successive error bounds $\delta$, $2\delta$, $3\delta$, and $4\delta$ correctly account for error propagation at the actual input.

The ramp identity and its error bounds are correct:

$$ T_t(u)=\operatorname{clip}(4(u-t)), \qquad 2\delta\longmapsto8\delta\longmapsto20\delta. $$

The NOR simulation has the stated ideal output and error $24\delta=3/16$. Both required decoding implications hold, including inputs at the decoding thresholds.

For PURIFY, at least one ideal output is an endpoint for every input, including $u=1/2$. The error $20\delta=5/32$ preserves that endpoint’s decoded purity. Pure inputs give the required two copies.

COPY is verified by the same ramp estimate.

The arguments are local in actual input values, so cyclic dependencies do not invalidate the estimates. Fresh internal nodes and the distinctness condition on source gates preserve primitive-gate distinctness.

The use-count calculation is correct: original nodes have at most two primitive uses, and doubling inputs also have at most two. Hence the reduction establishes Lemma 1 as stated.

3. Coloring and candidate reuse

Verified.

A nonconstant node has at most two neighbors from its producing gate and at most four from its consuming gates. Its degree is therefore at most six, allowing greedy coloring with seven colors.

Giving the two constants separate additional colors ensures that every primitive gate has pairwise distinct node colors. The construction consequently uses exactly $19$ candidates.

Candidate reuse does not create unintended overlaps inside a type’s specified bundles: the bundles depend only on the output and inputs of one primitive gate, whose colors are distinct.

4. Validity of the constructed society

Verified.

All displayed constants are consistent, including

$$ \alpha=\frac1{2052}, \qquad \rho=\frac{512}{513}, \qquad \eta=2^{-30}, \qquad K=\frac12. $$

Feedback bundles have size at most three. Signal types have at most three nonsingleton bundles. Their specified bundles are disjoint.

The initial budget on $*$ is at least $1/4$. Padding costs at most $1/16$, so its remaining budget is positive. All other budgets and all default coordinates are positive.

Every nonsingleton delegates to a different type; all self-delegations are singletons. Padding completes each partition and preserves the total budget.

Because the candidate count, gate arities, constants, and possible padding counts are fixed, the claimed fixed finite sets of numerical values follow.

The proposed dyadic masses are positive and sum to one, including when $\tau=1$. Their encoding length is polynomial. The construction has polynomial size.

5. Resolution equations and quadratic reduction

Verified.

The feedback and signal equations follow from the specified defaults, budgets, and delegate coordinates. The copied-input equation correctly uses the delegate’s fixed pair total $H$.

The perturbation terms satisfy the stated bounds. In particular, the feedback perturbation has magnitude at most $\gamma B$, while the signal perturbation is at most $\gamma H^2/(WK)$.

Cross-multiplication gives precisely the displayed quadratic identity, with

$$ E=vA(H-q)+uA(K+p). $$

The estimate $|E|\le\gamma$ is justified by the feasibility bounds and the displayed strict upper bounds on $A$ and $H+K+B$.

The normalization is correct, including the critical identity

$$ (B+K)\alpha^2\lambda=BH\eta=2^{-42}. $$

6. Root control and primitive-gate error

Verified.

Since $\lambda>0$ and $h\ge0$, the quadratic has exactly one positive root $r$, with $0<r\le1$. Its other root is $-\lambda/r$.

For $z_i\ge0$, the factorization supplies the stated bound on $|z_i-r|$. The denominator estimate is valid because $\lambda/r\ge\lambda$.

The separate cases $h\le1$ and $h\ge1$ correctly establish

$$ 0\le r-[1-h]_+\le\sqrt{\lambda}. $$

Clipping is applied correctly. The bound on $z_i-\xi_i$ also holds for constant nodes, where the difference is zero.

The copied-input formula and the fact that each gate has at most two inputs justify

$$ \left|h-\sum_{j\in J_i}\xi_j\right| \le 2(1-\rho\theta)+\frac{4\gamma}{\alpha}. $$

Thus the final primitive-gate error estimate holds for every resolved profile, rather than merely for a selected fixed point.

7. Strong-approximation decoding and numerical margin

Verified.

The oracle guarantee supplies one exact resolved profile close to the entire returned profile. The proof consistently uses that same profile.

Rescaling and clipping introduce error at most $\epsilon/\alpha$ per signal. Exact budget feasibility fixes the constant-node coordinates exactly. Accounting for the output and at most two inputs correctly adds $3\epsilon/\alpha$.

All numerical comparisons check out. The final upper bound is

$$ \frac{3585}{524288}<\frac1{128}. $$

Therefore every valid oracle answer decodes to a valid primitive-circuit assignment and then a Pure-Circuit solution. Theorem A follows with one oracle call.

The positivity conclusion also follows directly from positive defaults and positive budgets.

This proves $\mathrm{PPAD}$-hardness. It does not prove membership in $\mathrm{PPAD}$, and the output does not claim such membership.

8. Theorem B: exact polynomial-time subclass

Verified.

Under the union-of-bundles assumption, the delegate’s total on each nonsingleton bundle is fixed by its budgets. Consequently, the resolution equations become affine.

Positive-budget normalization is valid. Singleton coordinates are budget-fixed, and zero-budget coordinates are handled separately.

For every remaining dependency,

$$ 0\le\beta_{t,c}<1 $$

follows from $b_{u,R}\le D_{t,S}$ and $b_{t,S}>0$. Each row has at most one dependency, so the finite matrix satisfies $\|A\|_\infty<1$.

The uniqueness argument is correct. Existence from Section 1 ensures that the unique linear-system solution is budget-feasible and nonnegative.

The rational coefficient lengths, determinant bounds, and exact linear-algebra argument support polynomial bit complexity. The conclusions for $m\le2$ and $\tau=1$ follow under the task’s delegation restrictions.

9. General exponential upper bound

Verified, including the cited approximation result.

Clearing the positive denominators introduces no extraneous solutions on the budget-feasible nonnegative domain. There are $O(N)$ constraints of degree at most two, with polynomial total coefficient encoding length.

[Proposition 5 of the AAMAS paper](https://aamas.csc.liv.ac.uk/Proceedings/aamas2024/pdfs/p1029.pdf) states the strong-approximation result used here. Its parameter dependence supports the weaker polynomial numerical factor asserted by the prover. Equalities can be represented by paired inequalities without changing the claimed asymptotic constraint count.

The budget repair is correct in both cases:

All repairs remain close to the same exact resolved profile. The exponential bound therefore supplies valid outputs for the original strong-approximation problem.

Issue and minimum additional requirement

Major scope limitation — Sections 1 and 9 of the overall claim. The general classification requested in USER_TASK remains unresolved. A $\mathrm{PPAD}$ lower bound, a polynomial-time subclass, and an exponential upper bound do not establish either requested alternative.

No additional clarification is needed to verify the established results. Completing the assignment requires an additional mathematical result: either the requested general polynomial-time algorithm or a reduction establishing the specified $\mathrm{NP}$-hardness. The existing arguments should not be presented as implying either.

No mathematical errors or additional minor gaps were found in the submitted arguments. The reported lack of a bound on $s$ is accurate and creates no inconsistency with the parameterized comparison.

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