Answer: —
Corollary 4.5 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateA. Deciding, on input φ, whether Xφ admits an anonymous aggregator is i. in ΣP 2 ∩ΠP 2 and ii. coNP-hard. B. Given the agenda ¯φ = (φ1, . . . , φm), the question whether X ¯φ admits an anonymous aggregator is i. in ∆P 3 and ii. coNP-hard. Proof Ai.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a Boolean integrity constraint \(\varphi\) with feasible type set \(X_\varphi=\operatorname{Mod}(\varphi)\), decide whether there are maps \(g_j:\mathbb{Q}\cap[0,1]\to\{0,1\}\), one for each issue \(j\), with \(g_j(0)=0\) and \(g_j(1)=1\), such that for every finitely supported distribution \(\mu\) over \(X_\varphi\) with rational masses, the judgment vector \((g_j(\sum_{x\in X_\varphi:x_j=1}\mu_x))_{j=1}^m\) belongs to \(X_\varphi\).
Input is a Boolean formula \(\varphi\) on \(m\geq 3\) issues, with \(X_\varphi=\operatorname{Mod}(\varphi)\subseteq\{0,1\}^m\). Promise that each coordinate takes both values among elements of \(X_\varphi\).
A society is given by its support: the list of the \(\tau\) types with positive mass, each with its mass as a binary rational. Here \(\tau\) is the support size, not the number of possible types. Masses sum to \(1\); types outside the support have mass \(0\).
Seek maps \(g_j:\mathbb{Q}\cap[0,1]\to\{0,1\}\), with \(g_j(0)=0\) and \(g_j(1)=1\), such that \(\bigl(g_j(\sum_{x\in X_\varphi:x_j=1}\mu_x)\bigr)_{j=1}^m\in X_\varphi\) for every rational society \(\mu\) on \(X_\varphi\). The same maps must serve all societies; no monotonicity or regularity is imposed, and maps may differ between issues.
Only \(\varphi\) is supplied to the existence decision. Measure its running time in \(m\) and its encoding bit length \(L\); for procedures taking a represented society, use \(m,\tau,L,L_\mu\), where \(L_\mu\) is that society's encoding bit length.
Is this existence decision problem in \(\mathsf{P}\), or is it \(\mathsf{NP}\)-hard?
For finite societies, existence of a unanimity-preserving, issue-wise anonymous rule of some arity \(n\geq2\) that always returns a feasible judgment is \(\mathsf{coNP}\)-hard and belongs to \(\Sigma_2^P\cap\Pi_2^P\) when the domain is specified by an integrity constraint. [Source](https://arxiv.org/html/1711.01574v3)
No result settling the exact rational-distribution existence decision was located.
Let $\mathcal E$ denote the promised existence problem. I interpret $\mathsf{NP}$-hardness as hardness under polynomial-time many-one reductions.
I do not establish that hardness. The following results are proved below:
In particular,
$$
\mathcal E\in\mathsf P
\quad\Longleftrightarrow\quad
\mathsf P=\mathsf{NP}.
$$
This conditional statement and $\mathsf{coNP}$-hardness do not establish many-one $\mathsf{NP}$-hardness.
Write $X=X_\varphi$. The coordinate promise implies that $X$ is nonempty.
For $b\in\{0,1\}^m$, define $T_b$ by
$$
T_b(x,y)_j=
\begin{cases}
x_j,&x_j=y_j,\\
b_j,&x_j\ne y_j.
\end{cases}
$$
Thus coordinate $j$ uses AND if $b_j=0$, and OR if $b_j=1$. Call $b$ valid if
$$
T_b(x,y)\in X
\qquad\text{for every }x,y\in X.
$$
Theorem 1. The maps required in the task exist if and only if a valid $b$ exists.
Proof. Suppose the maps exist, and set
$$
b_j=g_j(1/2).
$$
For distinct $x,y\in X$, consider the society assigning mass $1/2$ to each. Its marginal on coordinate $j$ is their common value when they agree, and $1/2$ otherwise. The endpoint requirements therefore make its output $T_b(x,y)$, which must belong to $X$. For identical inputs, $T_b(x,x)=x$. Hence $b$ is valid.
Conversely, suppose $b$ is valid. For rational $p\in[0,1]$, define
$$
g_j(p)=
\begin{cases}
1,&b_j=0\text{ and }p=1,\\
1,&b_j=1\text{ and }p>0,\\
0,&\text{otherwise}.
\end{cases}
$$
Both endpoint requirements hold.
Let the positive support of a society be $x^1,\ldots,x^\tau$. Because all listed masses are positive and sum to $1$, its output on an AND coordinate is $1$ precisely when every supported type has value $1$. Its output on an OR coordinate is $1$ precisely when some supported type has value $1$.
The resulting vector is consequently the fold of $T_b$ over the support. Coordinatewise AND and OR are associative, and binary closure keeps every intermediate fold in $X$. The final output belongs to $X$. $\square$
The promise also gives a useful consequence:
$$
b\text{ valid}\quad\Longrightarrow\quad b\in X.
$$
Indeed, fold $T_b$ over all elements of $X$. Each coordinate contains both values, so its folded value is $b_j$. Closure puts this fold in $X$.
For completeness, the connection with Horn functions is explicit. Put
$$
R_b(x)=x\oplus b,
$$
where $\oplus$ is coordinatewise addition modulo $2$. Then
$$
R_b(T_b(x,y))=R_b(x)\land R_b(y).
$$
Thus $b$ is valid exactly when $R_b(X)$ is closed under AND. This is the oriented-intersection definition of a renamable Horn function used in [*Polynomial Certificates for Propositional Classes*](https://www.cs.tufts.edu/t/tech_reports/reports/2004-8/report.pdf). The proofs below establish the needed recognition properties directly.
A partial assignment $(S,a)$ consists of $S\subseteq\{1,\ldots,m\}$ and $a\in\{0,1\}^S$. It is forbidden if no $x\in X$ extends it, and minimally forbidden if deleting any assigned coordinate makes it extendible.
Every forbidden partial assignment contains a minimally forbidden restriction: repeatedly delete coordinates while forbiddenness persists. Under the coordinate promise, every minimally forbidden assignment has at least two coordinates.
Lemma 2. A vector $b$ is valid if and only if every minimally forbidden $(S,a)$ satisfies
$$
\bigl|\{j\in S:b_j=a_j\}\bigr|\leq 1.
$$
Proof of necessity. Suppose distinct $i,k\in S$ satisfy $b_i=a_i$ and $b_k=a_k$.
Minimality supplies $x^{(i)}\in X$ agreeing with $a$ on $S\setminus\{i\}$. It must disagree at $i$, since otherwise it would extend the forbidden assignment. Likewise, there is $x^{(k)}\in X$ agreeing with $a$ on $S\setminus\{k\}$ and disagreeing at $k$.
At $i$ and $k$, these inputs disagree, so their $T_b$ output equals $a$. At every other coordinate of $S$, both inputs already equal $a$. Their output therefore extends $(S,a)$ and lies outside $X$, contradicting validity.
Proof of sufficiency. Suppose instead that $x,y\in X$ and $z=T_b(x,y)\notin X$. Choose a minimally forbidden restriction $(S,z|_S)$.
The sets
$$
A=\{j\in S:x_j\ne z_j\},
\qquad
B=\{j\in S:y_j\ne z_j\}
$$
are nonempty, since neither feasible input extends that restriction. They are disjoint: if both inputs differed from $z_j$, they would both equal $1-z_j$, forcing the output to equal $1-z_j$.
Choose $i\in A$ and $k\in B$. These coordinates are distinct, the inputs disagree at each, and consequently
$$
b_i=z_i,\qquad b_k=z_k.
$$
The minimally forbidden restriction agrees with $b$ in at least two coordinates, contrary to the assumed condition. $\square$
Introduce orientation variables $B_1,\ldots,B_m$. A minimally forbidden $(S,a)$ contributes the clauses
$$
(B_i\ne a_i)\lor(B_k\ne a_k),
\qquad i,k\in S,\quad i<k.
$$
By Lemma 2, their conjunction $H_X$ has exactly the valid orientations as its satisfying assignments.
Although there may be exponentially many minimally forbidden assignments, there are at most
$$
4\binom m2
$$
distinct clauses in $H_X$.
Assume in this section that the supplied formula is already a CNF,
$$
\varphi=D_1\land\cdots\land D_r.
$$
Remove tautological clauses and duplicate literals. A remaining clause contains at most one literal of each variable.
A clause $C$ is an implicate of $\varphi$ if $\varphi\models C$. It is a prime implicate if no proper subclause is an implicate.
For a non-tautological clause
$$
C=\bigvee_{j\in S}\ell_j,
$$
let $a_j$ be the value falsifying $\ell_j$. Then $C$ is an implicate precisely when $(S,a)$ is forbidden, and is prime precisely when $(S,a)$ is minimally forbidden.
For each supplied clause $D_t$, choose any prime implicate $C_t\subseteq D_t$, and put
$$
F=C_1\land\cdots\land C_r.
$$
Theorem 3. The formulas $F$ and $\varphi$ are equivalent. Moreover, if $H_F$ contains the binary orientation clauses contributed by these selected $C_t$, then
$$
\operatorname{Mod}(H_F)
=
\{b:T_b\text{ preserves }X_\varphi\}.
$$
Proof. Every selected $C_t$ is entailed by $\varphi$, so $\varphi\models F$. Conversely, $C_t\subseteq D_t$ implies $C_t\models D_t$. Hence $F\models\varphi$.
If $b$ is valid, Lemma 2 applied to each prime $C_t$ shows that $b$ satisfies $H_F$.
For the converse, suppose $b$ satisfies $H_F$. We show that $T_b$ preserves every clause $C_t$.
Let $(S,a)$ be the falsifying partial assignment of one such clause. Satisfaction of its orientation constraints says that $b$ agrees with $a$ on at most one coordinate of $S$.
Suppose $x,y$ satisfy the clause but $z=T_b(x,y)$ falsifies it. Since $x$ satisfies it, choose $i\in S$ with $x_i\ne a_i$. Since $z_i=a_i$, the other input must have $y_i=a_i$, and $b_i=a_i$. Similarly, satisfaction by $y$ supplies $k\in S$ with $y_k\ne a_k$, $x_k=a_k$, and $b_k=a_k$. The coordinates $i,k$ are distinct because $y_i=a_i$. Thus $b$ agrees with $a$ twice, a contradiction.
Therefore $T_b$ preserves every $C_t$, hence their conjunction $F$, and therefore $X_\varphi$. $\square$
This theorem does not require enumerating all prime implicates. Choosing one prime subclause of each supplied clause suffices. Every such choice produces the same set of valid orientations.
Let $N$ be the total number of literal occurrences after normalization.
Starting with $C=D_t$, consider each literal $\ell$ currently present. Query satisfiability of
$$
\varphi\land\bigwedge_{\lambda\in C\setminus\{\ell\}}\neg\lambda.
$$
If the query is unsatisfiable, then $\varphi\models C\setminus\{\ell\}$, so delete $\ell$. Otherwise retain it.
The resulting clause remains an implicate. It is prime: when a literal was retained, the SAT answer supplied a model of $\varphi$ falsifying every other literal then present. That model still falsifies every other literal remaining at the end. Thus deleting that retained literal from the final clause destroys entailment.
There are at most $N$ queries across all supplied clauses. The promise excludes empty or singleton prime clauses: these would respectively make $\varphi$ unsatisfiable or force a coordinate.
After refinement, construct $H_F$ and solve it by the polynomial-time $2$-SAT algorithm. Theorem 3 proves the correctness of this existence decision and of the resulting orientation.
All query encodings and other work have bit length and running time polynomial in $m,L$.
Suppose every supplied clause has at most $k$ literals, where $k$ is fixed.
For each clause $D_t$ and each subclause $C\subseteq D_t$, prepare the SAT query
$$
\varphi\land\bigwedge_{\lambda\in C}\neg\lambda.
$$
All these queries are determined before any answer is received. Their answers identify every entailed subclause of each $D_t$. Select an inclusion-minimal entailed subclause; it is a prime implicate.
There are at most $r2^k$ queries. For fixed $k$, this is polynomial in the input length. Constructing $H_F$ and solving $2$-SAT then decides existence. Consequently,
$$
\mathcal E\text{ restricted to fixed-width CNF}
\in
\mathsf P_{\parallel}^{\mathsf{NP}}.
$$
Here $\mathsf P_{\parallel}^{\mathsf{NP}}$ means deterministic polynomial-time computation using polynomially many nonadaptive NP-oracle queries.
If the supplied CNF clauses are promised to be prime implicates, no SAT queries are needed: construct their orientation constraints directly and solve $2$-SAT.
For a promised $2$-CNF input, existence always holds. Choose any $b\in X_\varphi$. Each non-tautological binary clause forbids one assignment on its two coordinates. Since $b$ satisfies that clause, $b$ agrees with its falsifying assignment on at most one coordinate. The clause-preservation argument in Theorem 3 applies to every clause. Hence $b$ is valid.
The syntactic and semantic questions nevertheless differ, even under the coordinate promise. Consider
$$
\varphi=
(\neg x_1\lor x_2)
\land(x_1\lor\neg x_2)
\land(x_1\lor\neg x_2\lor x_3)
\land(x_1\lor\neg x_2\lor\neg x_3).
$$
The last two clauses are redundant, so its domain is
$$
X_\varphi=\{x:x_1=x_2\}.
$$
Every coordinate takes both values, and this domain is AND-closed.
But the displayed CNF is not syntactically renamable Horn. Under the substitution $x_j=y_j\oplus b_j$, a literal is positive precisely when $b_j$ equals its falsifying value. The first two clauses require $b_1=b_2$. Then exactly one of $x_1,\neg x_2$ becomes positive. The third clause consequently requires $b_3=1$, while the fourth requires $b_3=0$.
Prime refinement removes this syntactic obstruction by replacing both redundant clauses with $x_1\lor\neg x_2$.
The CNF refinement argument does not automatically apply to arbitrary formulas: an equivalent CNF over the same issues can have exponential size. We therefore establish the general upper bound separately.
Maintain a $2$-CNF $H$, initially empty, whose clauses are all necessary for validity.
$$
\varphi(x)\land\varphi(y)\land\neg\varphi(z)
\land[z=T_b(x,y)].
$$
If unsatisfiable, accept.
Every query has polynomial bit length in $m,L$; this statement avoids assuming unit-length variable names.
The deletion procedure preserves forbiddenness. It yields a minimally forbidden restriction because an extension witnessing that a retained coordinate could not be deleted remains an extension after other restrictions are removed.
Every added clause is necessary by Lemma 2. Furthermore, its sufficiency proof shows that the current counterexample supplies two coordinates of the final restriction agreeing with $b$. Thus $b$ violates at least one newly added clause. Because $b$ satisfied the previous $H$, that clause was not already present.
At most $4\binom m2$ distinct clauses can be added. There are therefore $O(m^2)$ unsuccessful iterations, each using $O(m)$ SAT queries and polynomial additional work.
Rejection is sound because all accumulated constraints are necessary. Acceptance is sound because it directly verifies closure. Hence
$$
\mathcal E\in\mathsf P^{\mathsf{NP}}.
$$
Let
$$
E=\{000,011,101,110\}.
$$
Lemma 4. No orientation is valid for $E$.
Proof. The coordinate promise holds for $E$, so validity would imply $b\in E$ by Theorem 1.
Coordinatewise,
$$
T_b(x,y)
=
b\oplus\bigl((x\oplus b)\land(y\oplus b)\bigr).
$$
This identity retains the common input value when the inputs agree and returns $b_j$ otherwise.
Set
$$
x=b\oplus011,\qquad y=b\oplus101.
$$
Both have even parity and belong to $E$. But
$$
T_b(x,y)
=
b\oplus(011\land101)
=
b\oplus001,
$$
which has odd parity. This contradicts closure. $\square$
Take an instance $\psi(u_1,\ldots,u_k)$ of $3$-CNF UNSAT. Introduce $v_1,v_2,v_3,s,t$, and let $\eta(v)$ be the $3$-CNF whose clauses exclude the four odd-parity assignments. Thus $\operatorname{Mod}(\eta)=E$.
Define
$$
\varphi_\psi(u,v,s,t)
=
(\neg s\lor t)\lor\bigl(\psi(u)\land\eta(v)\bigr).
$$
Its encoding length is polynomial in that of $\psi$.
The coordinate promise holds. Setting $s=0$ allows every assignment to $u,v,t$. Setting $s=t=1$ supplies feasible assignments with $s=1$.
If $\psi$ is unsatisfiable, then
$$
\varphi_\psi\equiv\neg s\lor t.
$$
This domain is AND-closed: an AND output with $s=1$ comes from two inputs with $s=1$, which must both have $t=1$. The output therefore also has $t=1$. Theorem 1 gives a YES instance.
If $\psi$ is satisfiable, fix a satisfying assignment $u=a$ and fix $s=1,t=0$. The feasible $v$-vectors on this slice are exactly $E$. Every $T_b$ preserves coordinates fixed identically in both inputs. Global closure would therefore imply closure of this slice under the restriction of $T_b$ to its three $v$-coordinates. Lemma 4 rules this out.
Consequently,
$$
\psi\text{ unsatisfiable}
\quad\Longleftrightarrow\quad
\varphi_\psi\in\mathcal E.
$$
This is a polynomial-time many-one reduction from the standard $\mathsf{coNP}$-complete problem $3$-CNF UNSAT.
It also produces width-$5$ CNF inputs. If
$$
\psi\land\eta=\bigwedge_D D,
$$
then distributivity gives
$$
\varphi_\psi\equiv\bigwedge_D(\neg s\lor t\lor D).
$$
Every $D$ has at most three literals, so every resulting clause has at most five. Thus the additional nonadaptive upper bound applies to a restriction that is already $\mathsf{coNP}$-hard.
Once a valid $b$ is available, evaluating the constructed rule on a valid represented society requires only folding AND or OR across its positive support. Marginal arithmetic is unnecessary. Reading the representation and folding its types takes
$$
O(m\tau+L_\mu)
$$
time. Here $\tau$ is exactly the listed support size.
The finite-arity existence question in the [cited aggregation paper](https://arxiv.org/html/1711.01574v3) does not imply rational-distribution existence. The relation $E$ demonstrates this directly.
Coordinatewise ternary XOR is anonymous and unanimous:
$$
a\oplus a\oplus a=a.
$$
It preserves $E$, because the parity of the output is the sum modulo $2$ of the three input parities. Nevertheless, Lemma 4 excludes the rational-distribution maps for $E$.
If $\mathcal E$ were in $\mathsf P$, the promise-preserving UNSAT reduction would put UNSAT, and therefore SAT, in $\mathsf P$. Conversely, if $\mathsf P=\mathsf{NP}$, the SAT-oracle algorithm becomes polynomial-time. This proves
$$
\mathcal E\in\mathsf P
\quad\Longleftrightarrow\quad
\mathsf P=\mathsf{NP}.
$$
The same reduction proves $\mathsf{NP}$-hardness under polynomial-time Turing reductions: query existence on $\varphi_\psi$ and negate the answer to decide SAT.
Negating an oracle answer is not a many-one reduction. I therefore leave the requested many-one $\mathsf{NP}$-hardness alternative open. The additional progress is the exact prime-refinement characterization for CNF and the nonadaptive upper bound for every fixed clause width.
⟨structured verdict parsed — rendered above⟩
Assessment: partial, with sound proved results. The submitted arguments establish the claimed characterizations, upper bounds, and $\mathsf{coNP}$-hardness. I found no mathematical error in those arguments. They do not establish polynomial-time many-one $\mathsf{NP}$-hardness, which the prover explicitly acknowledges.
The sole major issue is therefore incomplete resolution of the requested complexity alternative, rather than a false proof step.
Theorem 1 is correct in both directions.
For necessity, the society assigning mass $1/2$ to each of two distinct feasible judgments is a permitted rational society. Agreement coordinates have marginal $0$ or $1$, so the endpoint requirements return the common value. Disagreement coordinates have marginal $1/2$, so the output equals $b_j=g_j(1/2)$. Identical inputs are correctly handled separately.
For sufficiency, the displayed functions satisfy both endpoint requirements. Positive support masses ensure that an AND coordinate returns $1$ exactly when every supported judgment has value $1$, while an OR coordinate returns $1$ exactly when some supported judgment has value $1$. Since $X$ is finite and the support is nonempty, the fold is well-defined. Associativity and binary closure justify every intermediate result.
The quantifiers are correct: one fixed orientation defines one collection of maps serving every rational society.
The consequence that a valid orientation satisfies $b\in X$ is also correct. Folding over all elements of $X$ produces $b$ because every coordinate takes both values.
The identity
$$
R_b(T_b(x,y))=R_b(x)\land R_b(y)
$$
has the correct orientation convention. The cited source explicitly characterizes semantic renamable Horn functions through this oriented-intersection closure. Its hypotheses match the Boolean domain here. [*Polynomial Certificates for Propositional Classes*, Section 2.1](https://www.cs.tufts.edu/t/tech_reports/reports/2004-8/report.pdf)
Issues found: none.
Lemma 2 is correct.
In the necessity argument, minimality provides the two asserted feasible witnesses. Each must disagree at the omitted coordinate; otherwise it would extend the forbidden assignment. Their aggregate agrees with the forbidden assignment throughout $S$, so validity is contradicted.
In the sufficiency argument:
This proves the stated equivalence without an unstated assumption.
The promise excludes forbidden assignments of size zero or one: $X$ is nonempty, and neither coordinate value is globally excluded.
Each binary orientation clause prohibits exactly one simultaneous pair of agreements. There are four possible clauses for each unordered pair of distinct coordinates, so
$$
4\binom m2
$$
is a correct bound on the number of distinct constraints.
Issues found: none.
Theorem 3 is correct.
Normalization makes the correspondence between clauses and falsifying partial assignments unambiguous. Implicates correspond to forbidden assignments, and prime implicates correspond to minimally forbidden assignments.
A prime implicate contained in each supplied clause exists because that clause is an implicate and has finitely many subclauses.
Both implications establishing $F\equiv\varphi$ have the correct direction:
Necessity of the orientation constraints follows from Lemma 2. For sufficiency, the clause-preservation argument correctly produces two distinct coordinates agreeing with $b$ if two satisfying inputs aggregate to a falsifying output.
Consequently, selecting only one prime subclause per supplied clause suffices. The proof does not assume that these selected clauses exhaust the prime implicates.
The SAT query tests precisely whether the clause with the candidate literal removed remains an implicate.
The justification for a single deletion pass is sound. A satisfying witness obtained when retaining a literal still falsifies all other literals remaining at termination. Subsequent deletions cannot invalidate that witness.
Testing every remaining single-literal deletion suffices for primeness: any entailed proper subclause would entail a subclause obtained by deleting just one literal.
The number of queries is at most the original number $N$ of normalized literal occurrences. Constructing the orientation constraints and applying the polynomial-time satisfiability algorithm for $2$-CNF formulas requires polynomial additional work.
The queries correctly identify every entailed subclause of each supplied clause. An inclusion-minimal entailed subclause is prime.
The bound $r2^k$ is correct. Because $k$ is fixed, both the number and total encoding length of the queries are polynomial. The subsequent refinement selection and $2$-SAT computation use only the returned answers.
Thus the asserted membership in $\mathsf P_{\parallel}^{\mathsf{NP}}$ is established.
For supplied prime clauses, the direct orientation construction is justified.
For promised $2$-CNF inputs, a feasible $b$ exists. After normalization, the promise excludes empty and unit clauses. Satisfaction of each binary clause by $b$ excludes agreement with both coordinates of its falsifying assignment. The clause-preservation argument therefore applies.
The example separating syntactic and semantic renamable Horn recognition is correct:
Issues found in Section 3: none.
The general upper bound is established.
For a fixed orientation $b$, the counterexample query expresses exactly failure of closure. Its size is polynomial in $m$ and $L$, and ordinary SAT self-reduction can recover the assignment using $O(m)$ additional queries.
The minimization procedure correctly preserves forbiddenness. A witness showing that a coordinate cannot be deleted remains a witness after further restrictions are removed, so the final restriction is minimally forbidden.
Every accumulated constraint is necessary by Lemma 2. Applying the sufficiency argument of that lemma to the recovered counterexample and final restriction supplies a constraint violated by the current $b$.
That violated constraint must be new because $b$ satisfied every previous constraint. Therefore every unsuccessful iteration strictly increases the set of distinct clauses. The bound of $4\binom m2$ establishes polynomial termination.
Rejection and acceptance are both sound:
Hence
$$
\mathcal E\in\mathsf P^{\mathsf{NP}}
$$
follows as claimed.
Issues found: none.
Lemma 4 and the reduction are correct.
For the even-parity relation $E$, every valid orientation would lie in $E$. The selected vectors $x$ and $y$ then also have even parity. The critical computation is correct:
$$
011\land101=001.
$$
Thus the aggregate differs from $b$ in exactly one coordinate and has odd parity, contradicting closure.
The reduction has polynomial encoding length and always satisfies the coordinate promise. Setting $s=0$ permits both values of every coordinate other than $s$, and setting $s=t=1$ permits $s=1$.
If $\psi$ is unsatisfiable, the resulting domain is exactly that defined by $\neg s\lor t$, and the stated AND-closure argument is valid.
If $\psi$ is satisfiable, fixing $u=a$, $s=1$, and $t=0$ produces exactly the slice $E$ on the three remaining coordinates. Since $T_b$ preserves coordinates on which the inputs agree, global closure would imply closure of this slice. Lemma 4 excludes it.
The reduction therefore establishes the correct direction:
$$
\psi\text{ unsatisfiable}
\quad\Longleftrightarrow\quad
\varphi_\psi\in\mathcal E.
$$
Distributing the common disjunction over the clauses of $\psi\land\eta$ produces only linearly many clauses, each of width at most $5$. The restricted hardness claim is justified.
Issues found: none. This establishes many-one $\mathsf{coNP}$-hardness, not many-one $\mathsf{NP}$-hardness.
The evaluation bound
$$
O(m\tau+L_\mu)
$$
is correct for a valid represented society and an available orientation. Folding the listed types avoids marginal arithmetic. The prover correctly uses $\tau$ as the actual positive support size.
The ternary XOR example is also correct. XOR is invariant under permutations of its three inputs and satisfies ternary unanimity. The parity of the output judgment is the sum modulo $2$ of the input judgment parities, so it preserves $E$.
The cited paper’s definition of anonymity is permutation invariance in each issue, matching the property checked here. [*On the Computational Complexity of Non-dictatorial Aggregation*, Section 4.4.2](https://arxiv.org/html/1711.01574v3)
Thus the example correctly separates finite-arity anonymous existence from rational-distribution existence.
Issues found: none.
The equivalence
$$
\mathcal E\in\mathsf P
\quad\Longleftrightarrow\quad
\mathsf P=\mathsf{NP}
$$
is justified. The hardness reduction always produces promised instances, so a polynomial-time solver on the promise suffices to decide UNSAT and, by complementing its answer, SAT. Conversely, the SAT-oracle algorithm becomes polynomial-time if $\mathsf P=\mathsf{NP}$.
The Turing-hardness statement is likewise correct: deciding SAT requires one existence query and negation of its answer.
Major issue — incomplete resolution of the requested alternative. No polynomial-time many-one reduction establishing $\mathsf{NP}$-hardness is supplied. Complementing an oracle answer establishes Turing hardness but does not change the displayed reduction into a many-one reduction from SAT.
This is explicitly acknowledged, so the output does not overclaim. Nevertheless, under its stated many-one interpretation, it remains a partial answer to USER_TASK.
Minimum additional requirement: provide a polynomial-time many-one $\mathsf{NP}$-hardness reduction whose outputs satisfy the coordinate promise, or otherwise settle the requested alternative. No expositional clarification alone fills this gap. The additional requests for exact complexity classifications go beyond what is necessary to complete the task.
⟨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.