Answer: \(\mathrm{NP}\text{-hard}\), already for \(N=2\) and \(\tau=3\). Every valid instance has attained budget minimum \(0\) and an attained rational welfare optimum.
Theorem 6.2 — class: other
Given \(m\) queries, a finite publisher-type set \(\Theta\), masses \(N\mu_\theta\), typed document strategy sets \(D_\theta\), retrieval functions \(r_\theta\), peak parameters, and a population scale \(N\), compute the minimum \(B\) for which there exist \(\mathbf t\in[0,1]^m\) with \(\|\mathbf t\|_1\le B\) and an aggregate equilibrium measure \(\nu\) over publisher documents such that \(w_j(\nu)=\operatorname{ess\,sup}_{(\theta,d)\sim\nu}r_\theta(d,q_j)\ge t_j\) for every query; among minimum-\(B\) solutions, maximize the paper’s social-welfare objective.
A society is given by its support: \(\tau\) publisher types with positive binary-rational masses \(\mu_\theta\), summing to \(1\); \(\tau\) counts supported types, not possible types. Publishers are nonatomic, with total type mass \(N\mu_\theta\), where \(N\) is a binary-encoded integer and \(2\le N<m\).
For each type, the input specifies a nonempty rational polytope \(D_\theta\subseteq\{d\in[0,1]^m:\sum_jd_j\le1\}\), a rational peak \(1/(\lfloor m/N\rfloor+1)<p_\theta\le1\), and a continuous rational piecewise-linear function \(f_\theta:[0,1]\to[0,1]\), strictly increasing below its unique maximum at \(p_\theta\) and nonincreasing above it. Retrieval scores are \(r_\theta(d,q_j)=f_\theta(d_j)\).
An allocation is a Borel measure \(\nu\) on type-document pairs, with type marginal \(N\mu_\theta\). Write \(w_j=\operatorname{ess\,sup}_{\nu}r_\theta(d,q_j)\) and \(H_j=\nu\{(\theta,d):r_\theta(d,q_j)=w_j\}\).
Thresholds satisfy \(\mathbf t\in[0,1]^m\); feasibility requires \(w_j\ge t_j\) and \(H_j>0\) for every query. Threshold equality favors publishers; exposure is shared uniformly per unit winning mass.
Against fixed \(\nu\), a document scoring \(x\) on query \(j\) receives exposure density \(0\) if \(x<t_j\) or \(x<w_j\), \(1/H_j\) if \(x=w_j\ge t_j\), and \(+\infty\) if \(x>w_j\) and \(x\ge t_j\). Utility sums these densities; an aggregate equilibrium requires almost every publisher to maximize utility over its entire \(D_\theta\), holding \(\nu\) fixed.
Define welfare by \(SW(\nu)=-\max_j\operatorname{ess\,sup}_{\nu\restriction\{r_\theta(d,q_j)=w_j\}}|p_\theta-d_j|\), using the worst peak-distance among tied winning documents.
Minimize \(\|\mathbf t\|_1\) over feasible aggregate equilibria, then maximize \(SW\) among minimizers. Include infeasibility and nonattainment: determine the budget infimum and its attainment, and, when attained, the welfare supremum among budget minimizers and its attainment.
Is this exact lexicographic optimization problem polynomial-time solvable, or is it NP-hard? State running times in \(m\), \(\tau\), \(N\), and the total input bit length \(L\), including all polytope and function descriptions.
For the homogeneous finite-publisher version in this high-peak regime, explicit sharp threshold-budget bounds are known; the boundary is strict when the query count is not divisible by the publisher count. Nonuniform thresholds can also create welfare tradeoffs. [Verified full text](https://arxiv.org/html/2412.15878v1).
No complexity result for exactly the nonatomic formulation specified here was identified in the search.
The exact lexicographic optimization problem is \(\mathrm{NP}\text{-hard}\), already with \(N=2\) and \(\tau=3\). The hardness construction uses explicit rational linear-inequality descriptions of the polytopes.
The nonatomic formulation also has stronger existence and attainment properties than the finite-publisher model:
An exact algorithm for all requested outputs has running time
\(2^{O((m+\tau)(m+\log(\tau+1)))}L^{O(1)}\)
in bit operations. Its dependence on \(N\) is through its binary encoding, already included in \(L\).
The proofs follow.
Write \(a_\theta=N\mu_\theta>0\), and define
\(M_j=\max_{\theta}\max_{d\in D_\theta}f_\theta(d_j)\).
These maxima exist because every \(D_\theta\) is nonempty and compact, and every \(f_\theta\) is continuous.
Lemma 1. Every feasible aggregate equilibrium satisfies \(w_j=M_j\) for every query \(j\).
Proof. Every document has score at most \(M_j\), so \(w_j\le M_j\).
By the definition of essential supremum, almost every allocated document satisfies \(f_\theta(d_j)\le w_j\), simultaneously for all queries. Since feasibility requires \(H_j>0\), its utility is finite and bounded above by \(\sum_j1/H_j\).
Suppose \(w_j<M_j\). Some supported type \(\theta\) has a document \(d\in D_\theta\) with \(f_\theta(d_j)>w_j\). Feasibility gives \(t_j\le w_j\), so this deviation also satisfies \(f_\theta(d_j)\ge t_j\). Its utility is therefore \(+\infty\).
Almost every publisher of this type currently has finite utility and hence fails to maximize utility. Because \(a_\theta>0\), this contradicts aggregate equilibrium. Thus \(w_j=M_j\). \(\square\)
Consequently, once equilibrium is feasible, thresholds have no effect on incentives. For every \(\mathbf t\) satisfying \(0\le t_j\le M_j\), utility is exactly
\(U_\theta(d;H)=\sum_{j:\,f_\theta(d_j)=M_j}1/H_j\).
There are no attainable strict overtakes.
For each type and document, define its winning set
\(S_\theta(d)=\{j:f_\theta(d_j)=M_j\}\),
and let \(\mathcal A_\theta=\{S_\theta(d):d\in D_\theta\}\). This is a finite, nonempty family of subsets of \(\{1,\ldots,m\}\). Write \(\chi_S\) for the incidence vector of \(S\).
The possible vectors of winning masses form the compact convex set
\(C=\left\{\sum_\theta a_\theta z_\theta:z_\theta\in\operatorname{conv}\{\chi_S:S\in\mathcal A_\theta\}\right\}\subseteq[0,N]^m\).
Every point of \(C\) can be realized by assigning each type’s mass to finitely many representative documents.
Moreover, \(C\) contains a vector with every coordinate positive. For each query, a document attains \(M_j\), and its type has positive mass. Distributing each type’s mass positively over representatives of all its available winning sets therefore covers every query with positive mass.
Consider
\(\Phi(H)=\sum_{j=1}^m\log H_j\)
on the positive part of \(C\). It has a maximizer \(H^*\) with all coordinates positive. Indeed, \(C\) is compact, a positive point exists, and approaching a boundary point with a zero coordinate sends \(\Phi\) to \(-\infty\), while every other coordinate is bounded above by \(N\).
Choose a finite allocation realizing \(H^*\). Suppose it assigns positive mass to a winning set \(S\) of type \(\theta\). Replacing a sufficiently small amount of that mass by any \(T\in\mathcal A_\theta\) changes the potential with derivative
\(\nabla\Phi(H^*)\cdot(\chi_T-\chi_S)=\sum_{j\in T}1/H_j^*-\sum_{j\in S}1/H_j^*\).
This derivative cannot be positive, because \(H^*\) maximizes \(\Phi\). Thus every positively used winning set maximizes that type’s utility.
All allocated scores are at most \(M_j\), and the positive winning masses ensure \(w_j=M_j\). The allocation is consequently a feasible aggregate equilibrium at \(\mathbf t=\mathbf0\).
Atoms in this document distribution represent positive masses of publishers choosing identical documents; they do not require atomic publishers.
Corollary. Every valid instance is feasible. Its minimum threshold budget is \(0\), attained at \(\mathbf t=\mathbf0\). Since thresholds are nonnegative, this is the only budget-minimizing threshold vector.
Call \(S\in\mathcal A_\theta\) inclusion-maximal if no strictly larger set belongs to \(\mathcal A_\theta\).
At equilibrium, only inclusion-maximal winning sets can have positive mass: a strict superset would add at least one strictly positive term \(1/H_j\) to utility.
For each inclusion-maximal set, define
\(K_{\theta,S}=\{d\in D_\theta:f_\theta(d_j)=M_j\text{ for every }j\in S\}\).
This set is nonempty and compact. Every document in it has winning set exactly \(S\): an additional winner would contradict maximality.
Define its minimum possible worst winning distance by
\(c_{\theta,S}=\min_{d\in K_{\theta,S}}\max_{j\in S}|p_\theta-d_j|\),
with \(c_{\theta,\varnothing}=0\). The minimum is attained, since the objective is continuous on a compact set.
Now take any equilibrium. Group its allocation by type and winning set, and replace each positive group by a document attaining \(c_{\theta,S}\). This preserves:
It weakly improves welfare. The resulting welfare is exactly
\(-\max\{c_{\theta,S}:\text{the group }(\theta,S)\text{ has positive mass}\}\).
There are finitely many possible group supports, and at least one supports an equilibrium by Section 2. For each feasible support, the preceding replacement attains its best possible welfare. Taking the best of these finitely many supports proves attainment of the global welfare optimum.
Finally, each \(c_{\theta,S}\) is rational. A level set \(f_\theta(x)=M_j\) is a finite union of rational closed intervals and points. Thus \(K_{\theta,S}\) is a finite union of rational polytopes. On each component, minimizing the worst distance is a rational linear program, using a variable \(z\) and constraints \(-z\le p_\theta-d_j\le z\) for \(j\in S\). Its attained optimum is rational.
Therefore the welfare optimum is rational and attained.
We reduce from Independent Set: given a graph \(G=(V,E)\), with \(n=|V|\ge2\), and \(2\le k\le n\), decide whether its independence number satisfies \(\alpha(G)\ge k\). This is the standard \(\mathrm{NP}\)-complete problem, equivalently Clique on the complement graph. [Karp, *Reducibility among Combinatorial Problems*](https://link.springer.com/chapter/10.1007/978-1-4684-2001-2_9).
Set \(N=2\), \(m=2n+1\), and \(\tau=3\). Partition the queries into one anchor \(a\), vertex queries \(v\in V\), and padding queries \(z_1,\ldots,z_n\). Let \(b=1/n\).
Choose a power of two \(Q>2k+1\), with \(Q\le2(2k+1)\), and set
\(\mu_A=2/Q,\qquad \mu_B=(2k-1)/Q,\qquad \mu_C=(Q-2k-1)/Q\).
These are positive dyadic rational masses summing to \(1\). Denote their total publisher masses by \(A=N\mu_A\), \(B=N\mu_B\), and \(C=N\mu_C\). Their relevant ratio is
\(B/A=k-\tfrac12\).
Type \(A\) has peak \(p_A=1\) and function \(f_A(x)=x\).
Types \(B\) and \(C\) have peak \(p_B=p_C=b\). Their common function equals \(x\) on \([0,b]\) and \((1-x)/(n-1)\) on \([b,1]\). It is continuous, rational piecewise linear, strictly increasing before its unique maximum at \(b\), and strictly decreasing afterward.
The high-peak requirement holds for all three types, since
\(\frac1{\lfloor m/N\rfloor+1}=\frac1{n+1}<\frac1n=b\le p_\theta\).
Also \(2=N<m\).
Type \(B\) has a singleton document polytope: its document assigns \(b\) to every vertex query and zero elsewhere.
Type \(C\) likewise has a singleton polytope: its document assigns \(b\) to every padding query and zero elsewhere.
Both documents have total coordinate sum \(nb=1\).
For type \(A\), write the anchor coordinate as \(s\), the vertex coordinates as \(x_v\), and the padding coordinates as \(y_i\). Its polytope is given by
\(0\le s\le1,\qquad 0\le x_v\le b(1-s),\qquad y_i=0\),
and, for every edge \(\{u,v\}\in E\),
\(x_u+x_v\le b(1-s)\).
This is a nonempty rational polytope. Every document satisfies
\(s+\sum_vx_v+\sum_i y_i\le s+nb(1-s)=1\),
so it lies in the required document simplex.
The global maximum scores are
\(M_a=1,\qquad M_v=b\text{ for }v\in V,\qquad M_{z_i}=b\).
A type \(A\) document wins the anchor exactly when \(s=1\). The coordinate bounds then force every \(x_v=0\), so its winning set is exactly \(\{a\}\).
A type \(A\) document wins a vertex query exactly when \(x_v=b\). The bound \(x_v\le b(1-s)\) forces \(s=0\). If two adjacent vertices both had coordinate \(b\), their edge constraint would require \(2b\le b\), which is impossible. Its winning vertices therefore form an independent set.
Conversely, every independent set \(S\subseteq V\) is realized by setting \(s=0\), \(x_v=b\) for \(v\in S\), and all other coordinates to zero.
Type \(A\) cannot win a padding query. Hence its complete family of winning sets consists of the anchor singleton and the independent vertex sets, including the empty set.
At equilibrium, its empty winning set cannot receive positive mass: it has utility zero, whereas the anchor document has positive utility.
Every winning coordinate of types \(B\) and \(C\) equals their peak \(b\), so their winning distances are zero.
A type \(A\) anchor winner also has distance zero. Every type \(A\) vertex winner, however, has distance \(1-b\). Consequently every equilibrium has welfare either \(0\) or \(-(1-b)\).
An equilibrium has welfare zero exactly when all type \(A\) mass chooses the anchor document. For this allocation, winning masses are \(A\) at the anchor, \(B\) at every vertex query, and \(C\) at every padding query.
Type \(A\)’s anchor utility is \(1/A\). Its utility from an independent vertex set \(S\) is \(|S|/B\). Thus the allocation is an equilibrium exactly when
\(1/A\ge\alpha(G)/B\),
equivalently,
\(\alpha(G)\le B/A=k-\tfrac12\).
Because \(\alpha(G)\) is an integer, this is equivalent to \(\alpha(G)\le k-1\). Types \(B\) and \(C\) have only one document each and automatically maximize utility.
It follows that:
Therefore a single exact optimal-value call decides Independent Set: its answer is yes exactly when optimal welfare is negative. More specifically, deciding whether optimal welfare is strictly negative is \(\mathrm{NP}\text{-hard}\) under polynomial-time many-one reductions.
The construction has three supported types, constant \(N=2\), and constant-size piecewise-linear function descriptions. Even with dense inequality encoding, it has \(L=O(n^3\log n)\) and is constructible in polynomial time. This proves hardness of the exact optimization problem.
Here polytopes are explicitly described by rational linear constraints.
For each type and query, two rational linear programs compute the coordinate projection of \(D_\theta\), a closed interval. Maximizing \(f_\theta\) over this interval means evaluating it at the peak if the peak belongs to the interval, and otherwise at the endpoint nearest the peak. Taking the maximum over types computes every \(M_j\) in polynomial time.
For any level \(M_j\), the set \(f_\theta(x)=M_j\) has at most two connected components: at most one point below the peak and at most one interval or point above it. Their endpoints are rational and computable from the function description.
For every \(\theta\) and \(S\subseteq\{1,\ldots,m\}\), test joint attainability of its winning equalities by enumerating at most \(2^{|S|}\) component choices and solving rational linear programs. Retain only inclusion-maximal jointly attainable sets. These are precisely the maximal winning sets used in Section 3.
For each retained set, compute \(c_{\theta,S}\) by the distance linear program from Section 3 over all its components. A sufficient preprocessing bound is
\(\tau4^m\operatorname{poly}(m,L)\).
Let \(K\le\tau2^m\) be the number of retained type-set pairs. Optimal worst winning distance belongs to the finite list of their costs.
Consider an equilibrium using masses \(\lambda_{\theta,S}\) on retained pairs. Its type masses and winning masses satisfy
\((a,H)=\sum_{\theta,S}\lambda_{\theta,S}(e_\theta,\chi_S)\in\mathbb R^{\tau+m}\),
where \(e_\theta\) is the type’s unit vector.
If more than \(m+\tau\) coefficients are positive, their vectors are linearly dependent. Any dependence has coefficients summing to zero, by summing its first \(\tau\) coordinates, and therefore has both positive and negative coefficients. Moving the allocation coefficients along this dependence until one becomes zero preserves \((a,H)\) and nonnegativity.
Repeating reduces the support to at most \(m+\tau\) pairs. The remaining pairs retain their best-response status because \(H\) is unchanged. Deleting pairs cannot worsen welfare.
For a candidate distance \(\delta\), enumerate supports of at most \(m+\tau\) pairs satisfying \(c_{\theta,S}\le\delta\).
For each support, use variables \(\lambda_{\theta,S}>0\), \(q_j>0\), and \(u_\theta\). Impose the type-mass equations
\(\sum_{S:\,(\theta,S)\text{ selected}}\lambda_{\theta,S}=a_\theta\),
the reciprocal-winning-mass equations
\(q_j\sum_{\text{selected }(\theta,S):\,j\in S}\lambda_{\theta,S}=1\),
and the best-response conditions
\(u_\theta\ge\sum_{j\in T}q_j\quad\text{for every retained }T\text{ of type }\theta\),
\(u_\theta=\sum_{j\in S}q_j\quad\text{for every selected pair }(\theta,S)\).
The reciprocal equations enforce positive winning masses and \(q_j=1/H_j\). The inequalities cover every possible deviation, because every available winning set is contained in a maximal one and all \(q_j\) are positive. The equalities make every allocated document a best response.
Thus this system is feasible exactly when the selected support yields an equilibrium of welfare at least \(-\delta\), using its minimum-distance representative documents.
The system has \(O(m+\tau)\) variables, \(O(K+m+\tau)\) polynomial constraints, degree at most two, and rational coefficients of polynomial bit length. Standard algorithms for existential real-algebraic feasibility give running time \(K^{O(m+\tau)}L^{O(1)}\) for these systems. The required single-block bounds, including coefficient-bit bounds, are stated in [Basu, *Algorithms in Real Algebraic Geometry: A Survey*, Theorem 2.27](https://arxiv.org/pdf/1409.1534).
Enumerating supports and candidate costs preserves the total bound
\((\tau2^m)^{O(m+\tau)}L^{O(1)}=2^{O((m+\tau)(m+\log(\tau+1)))}L^{O(1)}\).
The smallest feasible candidate is the attained optimal worst distance; its negative is optimal welfare. Exact algebraic sampling can also provide allocation masses if an optimizing allocation is requested.
The budget value and its attainment can be reported in \(O(L)\) time, because Section 2 proves that every promised valid instance has minimum budget zero.
The cited paper studies finite publishers whose deviations alter the winning configuration and tie shares. [Nachimovsky and Tennenholtz, *On the Power of Strategic Corpus Enrichment in Content Creation Games*, Sections 2 and 6](https://arxiv.org/html/2412.15878v1).
Here a deviation holds the aggregate allocation fixed, and any qualifying strict overtake receives infinite utility. That rule forces global maximum scores and eliminates positive threshold budgets. The remaining welfare optimization retains computational hardness through the permitted document polytopes.
⟨structured verdict parsed — rendered above⟩
The substantive argument is correct: it establishes hardness of the exact welfare optimization, universal feasibility, an attained zero budget minimum, and an attained rational welfare optimum. I found two minor issues in the algorithmic presentation. Neither affects the reduction or the final running-time bound.
Section 1 is correct.
The maxima defining \(M_j\) exist: each document polytope is nonempty and compact, the functions are continuous, and there are finitely many supported types.
For each query, allocated scores are at most their essential supremum almost everywhere. Since there are finitely many queries, this holds simultaneously outside one null set. Feasibility gives \(H_j>0\), so almost every allocated document has finite utility, bounded by \(\sum_j1/H_j\).
If \(w_j<M_j\), the document attaining a higher score belongs to a supported type with positive mass. Since \(t_j\le w_j\), its strict overtake qualifies for infinite utility. Almost every currently allocated publisher of that type therefore fails to maximize utility. This contradicts the equilibrium condition exactly as specified in the task.
Thus \(w_j=M_j\) follows. Once this holds, every threshold vector satisfying \(0\le t_j\le M_j\) leaves the utility formula unchanged. This conclusion uses the task’s fixed-allocation deviation rule correctly.
Section 2 is correct.
The family of winning sets for each type is finite and nonempty. The displayed set \(C\) is precisely the set of realizable winning-mass vectors: finite convex combinations can be implemented by positive masses choosing representative documents.
Every query has a global maximizer in a supported type. Distributing positive mass over all available winning sets therefore produces a point of \(C\) with every coordinate positive.
The logarithmic potential attains a maximum in the positive part of \(C\). Compactness alone would not suffice on this relatively open domain, but the prover supplies the necessary boundary argument: any coordinate approaching zero forces the potential to negative infinity, while the other coordinates remain bounded above by \(N\).
The mass-transfer derivative is correct. A positively used winning set can be replaced by another available set in a sufficiently small positive amount while preserving type masses. A positive derivative would contradict maximality of the potential. Consequently, every positively used set is a best response.
Positive winning masses also ensure that the realized essential suprema equal \(M_j\). The constructed allocation is therefore feasible at \(\mathbf t=\mathbf0\).
The budget conclusion follows: nonnegative thresholds cannot have budget below zero, and zero budget uniquely determines the zero threshold vector. This settles infeasibility and budget nonattainment for every promised valid instance.
Section 3 is correct.
A nonmaximal winning set cannot receive positive equilibrium mass: an attainable strict superset increases utility by at least one positive reciprocal winning mass.
For a maximal set \(S\), the set \(K_{\theta,S}\) is nonempty and compact. Its documents have exactly winning set \(S\), since any additional winning coordinate would produce an attainable strict superset.
The representative-document replacement preserves type masses, winning masses, and best-response status. It also respects the task’s essential-supremum welfare definition: each positive group contributes its worst winning distance, and replacing that group by a minimum-distance representative cannot worsen that contribution. Null groups do not affect welfare.
There are finitely many possible positive group supports. For any support admitting an equilibrium, replacement attains the best welfare available on that support. Taking the best among the finitely many feasible supports proves global attainment without requiring compactness of the equilibrium allocation space.
Rationality is also justified. The score maxima are rational, and rational piecewise-linear level sets have rational endpoints. Each relevant document set is a finite union of rational polytopes, and the distance objective has the stated linear-programming formulation.
The empty-set convention causes no problem: a type whose maximal winning set is empty contributes no winning documents to welfare.
Section 4 is correct.
All promise conditions are satisfied:
The claimed global maximum scores are correct. Type \(A\) supplies anchor score one; types \(B\) and \(C\) supply vertex and padding scores \(b\), respectively. No permitted document exceeds these scores.
The characterization of type \(A\)’s winning sets is exact. An anchor winner forces \(s=1\) and all vertex coordinates zero. A vertex winner forces \(s=0\); the edge inequalities prohibit adjacent winning vertices. Conversely, every independent set is realized by the displayed document.
The welfare dichotomy is correct. Type \(A\)’s anchor winners and all winners of types \(B\) and \(C\) have zero peak-distance. Any positive mass of type \(A\) vertex winners gives distance \(1-b\). Empty winning sets cannot receive positive equilibrium mass because the anchor deviation has positive utility.
Accordingly, zero welfare requires all type \(A\) mass to choose the anchor. For that allocation, the exact best-response condition is
\(1/A\ge\alpha(G)/B\), equivalently \(\alpha(G)\le k-1\).
The half-integer ratio removes equality ambiguity.
Thus the reduction has the correct direction: an Independent Set yes-instance corresponds to strictly negative optimal welfare. Universal existence from Section 2 ensures that the other welfare value is attained when zero welfare is impossible.
The construction is polynomial in the graph input size. It establishes hardness already with \(N=2\), three supported types, and explicit rational inequality descriptions.
The algorithm is sound, with two minor presentation issues.
The coordinate projections are closed intervals, and the stated maximization of the retrieval function over each interval is valid. The monotonicity assumptions ensure that each level set has at most two connected components.
Testing joint winning equalities and retaining maximal jointly attainable subsets produces exactly the maximal winning sets required earlier. Computing their costs by componentwise linear programs is valid.
The support-reduction argument is correct. Linear dependence among more than \(m+\tau\) selected vectors permits elimination of a positive coefficient while preserving all type and winning masses. Its dependence coefficients have both signs because their sum is zero. Preserving winning masses preserves best-response status; removing groups cannot worsen welfare.
The candidate-support feasibility system is also correct:
The cited theorem supports existential feasibility for polynomial equalities and strict or weak inequalities, including unbounded domains. Its one-block specialization and integer coefficient-size bounds support the final bit-complexity estimate. [Basu, Theorem 2.27](https://arxiv.org/pdf/1409.1534).
Minor issue 1 — input representation. The upper-bound algorithm assumes explicit rational linear constraints for the polytopes. The task does not fix a representation, and the opening algorithm claim is broader than the qualification in Section 5.
Minimum clarification: State the representation assumption alongside the opening running-time claim, including an explicit rational piecewise-linear function encoding. The reduction already establishes hardness for the explicitly specified inequality representation.
Minor issue 2 — intermediate constraint-count bound. The system has \(O(K+m+\tau)\) constraints, so the cited theorem does not directly yield the displayed bound \(K^{O(m+\tau)}L^{O(1)}\) uniformly when \(K\) is small. For example, a single type with \(D_\theta=\{\mathbf0\}\) and \(f_\theta(x)=x\) has \(K=1\), regardless of the query count.
Minimum clarification: Retain the additive \(m+\tau\) contribution when applying the theorem, and explain its absorption into the final displayed exponential bound. This is a routine bound clarification; the final bound remains supported.
The dependence on \(N\) through its binary encoding is correctly accounted for. The budget-reporting claim applies to promised valid inputs and does not assert that validating those promises takes linear time.
Section 6 is consistent with the cited model.
The cited paper defines finite-player deviations against the other players’ documents, with uniform publisher tie-breaking. The present task instead fixes the aggregate allocation during deviations and assigns infinite utility to qualifying strict overtakes. That distinction supports the prover’s explanation of why the finite-publisher budget bounds do not transfer. [Nachimovsky and Tennenholtz, Section 2](https://arxiv.org/html/2412.15878v1).
No major issue or counterexample was found. The two requested clarifications concern presentation and complexity accounting, rather than new mathematics.
⟨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.