Answer: \(\mathrm{coNP}\)-complete under promise-preserving polynomial-time many-one reductions; hence \(\mathrm{NP}\)-hard under polynomial-time Turing reductions.
Proposition 7 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateGiven a setting pN, M, qq and a bound r P r0, 1s, a mechanism f is r-partially strategyproof if and only if it is r-DD-strategyproof.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite set \(T\) of complete assignment types, rational society masses \(\mu\in\mathbb{Q}^{T}\), per-capita capacities \(q\), and a specified anonymous continuum lift \(\mathcal F\), compute the largest \(r\in[0,1]\) such that for every positive-mass type \(t\), every alternative report \(\rho\), and every truthful-ranking prefix \(j_1\succ\cdots\succ j_K\), \(\sum_{k=1}^{K}r^k x_{\mu,t}(t)_{j_k}\ge\sum_{k=1}^{K}r^k x_{\mu,t}(\rho)_{j_k}\); equivalently, decide whether this degree is at least \(r_0\).
Let \(M\) contain \(m\ge2\) objects, and let \(\mathcal P\) be all strict complete rankings of \(M\). A society is given by its support: a nonempty list \(T\subseteq\mathcal P\) of \(\tau\) types with positive binary-rational masses \(\mu_t\), normalized by \(\sum_{t\in T}\mu_t=1\). Thus \(\tau\) is the support size, not the number of possible rankings. Per-capita capacities satisfy \(q\in\mathbb Q_{>0}^{M}\) and \(\sum_jq_j\ge1\).
The specified anonymous continuum rule at this society is represented by a supplied Boolean circuit \(C\): on a report \(\rho\in\mathcal P\), encoded as a permutation, it outputs a lottery \(C(\rho)\in\mathbb Q_{\ge0}^{M}\), with coordinates encoded as binary numerators and positive denominators. These lottery properties and truthful feasibility \(\sum_t\mu_tC(t)_j\le q_j\) are promises. A unilateral report by a zero-mass individual leaves \(\mu\) unchanged; define \(x_{\mu,t}(\rho)=C(\rho)\). Reports may be outside \(T\).
Define \(d\) as the largest \(r\in[0,1]\) for which, for every \(t\in T\) with truthful ranking \(j_1\succ\cdots\succ j_m\), every \(\rho\in\mathcal P\), and every \(K\in\{1,\ldots,m\}\), \(\sum_{k=1}^{K}r^k C(t)_{j_k}\ge\sum_{k=1}^{K}r^k C(\rho)_{j_k}\). The threshold \(r_0\in[0,1]\) is binary rational. Let \(L\) be the total bit length of the numerical inputs and \(s\) the circuit encoding length.
Is deciding whether \(d\ge r_0\) solvable in polynomial time in \(m,\tau,L,s\), or is it NP-hard under polynomial-time Turing reductions?
For finite societies, discounted-dominance inequalities characterize partial strategyproofness ([Mennle–Seuken](https://www.ifi.uzh.ch/ce/publications/PSP.pdf)); an enumeration algorithm computes the degree for rational-valued computable mechanisms, but examines exponentially many profiles and reports ([algorithmic treatment](https://arxiv.org/pdf/1401.3675)). No result settling this precisely encoded continuum decision problem was located.
The promised decision problem is \(\mathrm{coNP}\)-complete under polynomial-time many-one reductions, and therefore \(\mathrm{NP}\)-hard under polynomial-time Turing reductions.
Hardness holds with a single supported type, \(\tau=1\), the fixed threshold \(r_0=3/4\), and a circuit whose range contains at most two lotteries. The constructed degree is either \(1/2\) or \(1\).
Consequently, a polynomial-time algorithm in \(m,\tau,L,s\) exists only if \(\mathrm{P}=\mathrm{NP}\).
For a supported type \(t\), write its ranking as \(j_1\succ\cdots\succ j_m\). For a report \(\rho\), define
\(a_k=C(t)_{j_k}-C(\rho)_{j_k}\)
and, for each prefix length \(K\),
\(F_K(r)=\sum_{k=1}^{K}r^k a_k.\)
Call \(r\in[0,1]\) *feasible* if all these prefix polynomials are nonnegative, for every supported type and every report.
Lemma. If \(R>0\) is feasible, then every \(r\in[0,R]\) is feasible.
Proof. Fix a type and report, and put \(\lambda=r/R\in[0,1]\). For every \(K\),
\(F_K(r)=\lambda^K F_K(R)+\sum_{\ell=1}^{K-1}(\lambda^\ell-\lambda^{\ell+1})F_\ell(R).\)
To verify this identity, expand the right-hand side. The coefficient multiplying \(R^k a_k\) is
\(\lambda^K+\sum_{\ell=k}^{K-1}(\lambda^\ell-\lambda^{\ell+1})=\lambda^k,\)
including the case \(k=K\), where the sum is empty. Thus that contribution is \(r^k a_k\), as required.
Every coefficient in the displayed identity is nonnegative. Since feasibility of \(R\) gives \(F_\ell(R)\ge0\) for every prefix, it follows that \(F_K(r)\ge0\). This applies to every type and report, proving the lemma.
The feasible set contains \(0\). It is closed because it is the intersection of finitely many sets defined by non-strict polynomial inequalities. Being a closed subset of \([0,1]\), it has a maximum \(d\). The lemma then shows that the feasible set is exactly \([0,d]\).
In particular,
\(d\ge r_0\quad\Longleftrightarrow\quad F_K(r_0)\ge0\text{ for every }t,\rho,K.\)
This equivalence justifies checking the inequalities at the supplied threshold.
On promised inputs, a certificate for a NO answer consists of a supported type \(t\), a permutation \(\rho\), and a prefix length \(K\) such that
\(\sum_{k=1}^{K}r_0^k\bigl(C(t)_{j_k}-C(\rho)_{j_k}\bigr)<0.\)
By the preceding equivalence, such a certificate exists exactly when \(d<r_0\).
The certificate has polynomial length: a ranking requires \(O(m\log m)\) bits, while the type index and prefix length require \(O(\log\tau+\log m)\) bits. A verifier checks that the report is a permutation, evaluates the circuit on \(t\) and \(\rho\), and computes the displayed rational expression exactly.
The arithmetic also takes polynomial time. Circuit outputs have polynomially bounded bit length in \(s\). If \(r_0=u/v\), a common denominator can be obtained by multiplying \(v^m\) by the denominators of the relevant coordinates of both output lotteries. Its bit length is \(O(m(L+s))\), up to the encoding constants. Clearing denominators therefore reduces the sign test to polynomial-size integer arithmetic.
Thus the complement has a polynomial-time verifier, establishing membership in \(\mathrm{coNP}\) on the promised domain. No verification of the promises is required.
We reduce from Boolean circuit unsatisfiability. Boolean circuit satisfiability is \(\mathrm{NP}\)-complete, so its complement is \(\mathrm{coNP}\)-complete. [Circuit-SAT theorem](https://www.cs.cmu.edu/~15451-s20/lectures/lec16-np-beamer.pdf)
Let \(B\) be a Boolean circuit on \(n\ge1\) input bits. Restricting to \(n\ge1\) loses no generality: an unused input can be added.
Take
\(M=\{a,b,c\}\cup\{u_i,v_i:1\le i\le n\},\qquad m=2n+3.\)
There is one supported type,
\(t:\ a\succ b\succ c\succ u_1\succ v_1\succ\cdots\succ u_n\succ v_n,\)
with mass \(\mu_t=1\). Set \(q_j=1\) for every object and \(r_0=3/4\).
Define two lotteries \(x,y\) by
\(x_a=1/4,\quad x_b=0,\quad x_c=3/4,\)
\(y_a=0,\quad y_b=1/2,\quad y_c=1/2,\)
with all other coordinates zero.
Both lotteries have nonnegative rational coordinates summing to one.
For every permutation \(\rho\), define \(z(\rho)\in\{0,1\}^n\) by
\(z_i(\rho)=1\quad\Longleftrightarrow\quad u_i\text{ precedes }v_i\text{ in }\rho.\)
Define the supplied circuit to output \(y\) precisely when both conditions hold:
Otherwise, it outputs \(x\).
This function has a polynomial-size Boolean circuit. For example, each pair-order bit can be computed by comparing the object identifiers at each ordered pair of positions and taking an OR over the matching positions. This uses polynomially many gates in \(m\). The circuit then evaluates \(B\), tests the first object, and selects between two constant rational output vectors.
Every assignment \(z\in\{0,1\}^n\) is realized by a report starting with \(b\): begin with \(b,a,c\), and then list each pair as \(u_i,v_i\) when \(z_i=1\), or as \(v_i,u_i\) when \(z_i=0\).
The truthful report starts with \(a\), so \(C(t)=x\), independently of \(B\).
Every valid report receives either \(x\) or \(y\); hence every output is a lottery with correctly encoded nonnegative rational coordinates and positive denominators.
Truthful feasibility holds because, for every object \(j\),
\(\sum_{t'\in T}\mu_{t'}C(t')_j=x_j\le1=q_j.\)
The mass is positive and normalized, every capacity is positive, and \(\sum_jq_j=m\ge1\).
Finally, \(m\), the numerical encoding length, and the supplied circuit length are polynomial in the source instance size. The reduction therefore runs in polynomial time and always produces a promised instance.
The circuit outputs \(x\) on every report. Thus every truthful-minus-report difference is zero, and every discount in \([0,1]\) is feasible. Therefore \(d=1\).
A satisfying assignment yields a report receiving \(y\). Every report receives either \(x\) or \(y\).
Reports receiving \(x\) impose only equality constraints. For reports receiving \(y\), the differences along the truthful ranking are
\((x_a-y_a,x_b-y_b,x_c-y_c,0,\ldots,0)=(1/4,-1/2,1/4,0,\ldots,0).\)
Consequently, the prefix polynomials are
\(F_1(r)=r/4,\)
\(F_2(r)=r/4-r^2/2=(r/4)(1-2r),\)
and, for every \(K\ge3\),
\(F_K(r)=r/4-r^2/2+r^3/4=(r/4)(1-r)^2.\)
For \(r\in[0,1]\), the first and all later-prefix polynomials are nonnegative. The second-prefix polynomial is nonnegative exactly when \(r\in[0,1/2]\).
Since a report receiving \(y\) exists, the feasible set is exactly \([0,1/2]\). Therefore \(d=1/2\).
We have proved
\(B\text{ is unsatisfiable}\quad\Longleftrightarrow\quad d\ge3/4.\)
This establishes \(\mathrm{coNP}\)-hardness under promise-preserving polynomial-time many-one reductions.
Together with membership, the reduction establishes \(\mathrm{coNP}\)-completeness on the promised domain.
To solve circuit satisfiability using an oracle for the target problem, construct the instance above, ask whether \(d\ge3/4\), and negate the oracle’s answer. This is a polynomial-time Turing reduction using one oracle query. Since circuit satisfiability is \(\mathrm{NP}\)-complete, the target problem is \(\mathrm{NP}\)-hard under the requested reductions.
The endpoint \(r_0=0\) always gives YES, but the hardness construction uses a fixed interior threshold and strictly positive degrees. It applies directly to the specified zero-mass deviation model: the population masses remain fixed while the individual’s lottery changes with the report.
⟨structured verdict parsed — rendered above⟩
The prover resolves the assigned decision problem. The argument establishes \(\mathrm{coNP}\)-completeness on the promised domain under promise-preserving polynomial-time many-one reductions, and therefore \(\mathrm{NP}\)-hardness under polynomial-time Turing reductions.
I found no mathematical errors, unjustified substantive steps, or missing hypotheses. No repair is required.
The downward-closure lemma is correct. For a fixed supported type and report, feasibility of \(R\) supplies all prefix inequalities \(F_\ell(R)\ge0\), which are exactly the hypotheses used in the displayed identity.
The identity is valid: for each \(k\le K\), the coefficient of \(R^ka_k\) telescopes to \(\lambda^k\). This includes \(K=1\), when the sum is empty. All coefficients are nonnegative for \(\lambda\in[0,1]\). At \(r=0\), all exponents are positive, so the identity introduces no undefined power.
The existence of a largest feasible discount is also justified:
If the maximum is positive, the lemma establishes feasibility of every smaller discount. If the maximum is zero, the feasible set is already \(\{0\}\). Thus the feasible set is exactly \([0,d]\), including both endpoints.
Consequently, the equivalence between \(d\ge r_0\) and feasibility at \(r_0\) is proved. This is an essential step: the verifier cannot simply assume that the largest feasible discount determines feasibility of every smaller value.
The proposed certificate for a NO instance is sufficient and necessary on promised inputs. Failure of feasibility at \(r_0\) means that at least one supported type, report, and prefix has a strictly negative expression.
The certificate size is polynomial. A supported type can be specified by its index, a report by a permutation of \(m\) objects, and the prefix by an integer between \(1\) and \(m\). The verifier can check these restrictions and evaluate the supplied Boolean circuit in polynomial time.
The exact-arithmetic argument is sound under the usual explicit Boolean-circuit encoding. Output widths are bounded by the circuit encoding length, so the output numerators and denominators have polynomial bit length. The promises ensure that the denominators obtained on valid reports are positive.
For \(r_0=u/v\), multiplying \(v^m\) by the denominators of the relevant coordinates gives a positive common denominator. Its bit length is bounded by \(O(m(L+s))\) under the stated encoding. Clearing denominators therefore preserves the sign and requires only polynomial-size integer arithmetic. The polynomial number of additions and multiplications also takes polynomial time.
The endpoint \(r_0=0\) causes no problem: every expression is zero, and no negative certificate exists.
The prover correctly limits this membership claim to the promised domain. It does not claim that the verifier checks the semantic promises.
The cited theorem states that satisfiability of a finite acyclic Boolean circuit with one output is \(\mathrm{NP}\)-complete. This is the standard problem used by the reduction; its complement is therefore \(\mathrm{coNP}\)-complete. The cited source explicitly states the theorem. [Circuit-SAT theorem](https://www.cs.cmu.edu/~15451-s20/lectures/lec16-np-beamer.pdf)
Adding an unused input handles the restriction \(n\ge1\) without changing satisfiability.
The construction has \(m=2n+3\) objects, one supported ranking, and rational constants of bounded bit length. Its support description and numerical data have polynomial size.
The supplied circuit is constructible in polynomial time. The described comparisons over ordered pairs of positions compute the relative-order bits with polynomially many gates. Evaluating \(B\), testing the first object, and selecting between constant output vectors likewise require only polynomial overhead. This establishes both polynomial output size and polynomial construction time.
The assignment encoding is correct. Because every report is a permutation, exactly one member of each pair precedes the other, so every \(z_i(\rho)\) is well-defined.
The proposed report beginning with \(b,a,c\), followed by appropriately ordered pairs, realizes every assignment. It uses every object exactly once and satisfies the first-object condition. Hence a report receives \(y\) if and only if the source circuit has a satisfying assignment.
Every promise is verified:
The definition of the circuit on malformed permutation encodings is irrelevant: the task promises lottery outputs on reports in \(\mathcal P\).
The construction respects the zero-mass deviation model. Its report-dependent lottery uses the supplied circuit while the society’s mass distribution stays fixed.
When \(B\) is unsatisfiable, every report receives \(x=C(t)\). All prefix differences vanish, establishing \(d=1\).
When \(B\) is satisfiable, at least one report receives \(y\). Reports receiving \(x\) impose no additional restrictions. For a report receiving \(y\), the stated difference vector is correct:
\[
(1/4,-1/2,1/4,0,\ldots,0).
\]
The three polynomial calculations are correct:
\[
F_1(r)=r/4,\qquad
F_2(r)=(r/4)(1-2r),\qquad
F_K(r)=(r/4)(1-r)^2\quad(K\ge3).
\]
On \([0,1]\), the first and every prefix from the third onward are nonnegative. The second is nonnegative exactly on \([0,1/2]\), including both boundary values. Thus the feasible set is exactly \([0,1/2]\), establishing \(d=1/2\).
As a direct arithmetic check, at the chosen threshold \(r_0=3/4\), the violating second prefix equals \(-3/32\). The threshold therefore separates the two constructed cases strictly.
The reduction maps circuit unsatisfiability to YES instances and circuit satisfiability to NO instances, always within the promised domain. This proves the claimed promise-preserving many-one hardness.
For the requested Turing reduction, negating the target oracle’s answer decides circuit satisfiability with one query. The reduction is polynomial time and never queries an unpromised instance. Therefore the claimed \(\mathrm{NP}\)-hardness under polynomial-time Turing reductions follows.
The conditional statement about polynomial-time solvability is justified: a polynomial-time algorithm for promised target instances would yield a polynomial-time algorithm for Circuit-SAT, implying \(\mathrm P=\mathrm{NP}\).
No blocking issues or additional clarifications are needed.
⟨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.