Answer: Encoding-dependent: polynomial-time solvable under dense full-coordinate encoding; coNP-complete under sparse-support encoding.
Theorem 6 — class: hardness
The problem ExistsForced is coNP-complete in the combined size of the L-encodings of the axioms in the set provided.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given alternatives \(C\), a rational society \(\mu\in\Delta(L(C))\), and a nontrivial finite propositional axiom formula \(\Phi\) over atoms \(p_{\nu,c}\) for explicitly named rational societies \(\nu\), decide whether every continuous voting rule \(F:\Delta(L(C))\to\mathcal{P}^{+}(C)\) satisfying \(\Phi\) assigns the same outcome to \(\mu\).
Let \(L(C)\) be the strict linear orders on a finite candidate set \(C\), and let \(\Delta(L(C))\) be the probability simplex with its Euclidean topology; equip \(\mathcal P^+(C)\) with the discrete topology. A rational society has rational coordinates. A continuous voting rule is a continuous map \(F:\Delta(L(C))\to\mathcal P^+(C)\). For each explicitly named rational society \(\nu\), interpret \(p_{\nu,c}\) as \(c\in F(\nu)\); \(F\) satisfies \(\Phi\) under ordinary propositional semantics.
Is Continuous ExistsForced—given \(C\), \(\mu\), and satisfiable \(\Phi\), deciding whether all continuous voting rules satisfying \(\Phi\) have the same outcome at \(\mu\)—solvable in polynomial time, or is it NP-hard?
For finite electorates, the analogous ExistsForced problem with propositional \(L\)-encodings is coNP-complete in the combined encoding size. No verified result for this exact distributional formulation is stated here.
Assume that $C$ is nonempty and finite. Since $L(C)$ is finite, the probability simplex
$$ \Delta(L(C)) = \left\{x\in\mathbb R^{|L(C)|}_{\ge 0}: \sum_{\sigma\in L(C)}x_\sigma=1 \right\} $$
is convex, hence path-connected.
The codomain $\mathcal P^+(C)$ is finite and has the discrete topology. Every connected subset of a discrete space is a singleton. Therefore, for every continuous map
$$ F:\Delta(L(C))\longrightarrow\mathcal P^+(C), $$
the image $F(\Delta(L(C)))$ is a singleton. Thus there is a unique nonempty committee $S\subseteq C$ such that
$$ F(\nu)=S $$
for every society $\nu$. Conversely, every constant map with value $S\in\mathcal P^+(C)$ is continuous.
Hence continuous voting rules are in bijection with nonempty subsets of $C$.
Introduce one Boolean variable $x_c$ for each $c\in C$. From $\Phi$, form the collapsed formula $\widehat\Phi$ by replacing every atom $p_{\nu,c}$, independently of $\nu$, by $x_c$.
For a nonempty committee $S\subseteq C$, let $\alpha_S$ be the assignment
$$ \alpha_S(x_c)=1 \quad\Longleftrightarrow\quad c\in S. $$
By the preceding section, the constant rule with value $S$ satisfies $\Phi$ exactly when $\alpha_S$ satisfies $\widehat\Phi$. Therefore the permissible outcomes are precisely
$$ \mathcal A_\Phi = \left\{ S\subseteq C: S\ne\varnothing \text{ and } \alpha_S\models\widehat\Phi \right\}. $$
Under the ordinary universal interpretation of “all satisfying rules have the same outcome,” the answer is yes exactly when
$$ |\mathcal A_\Phi|\le 1. $$
This includes the vacuous case $\mathcal A_\Phi=\varnothing$. Notice that ordinary propositional satisfiability of $\Phi$ does not imply $\mathcal A_\Phi\ne\varnothing$, because continuity forces all society-indexed atoms for a fixed candidate to have the same value.
The designated society $\mu$ otherwise plays no role: every continuous rule is constant.
Suppose that a rational society is encoded by explicitly listing all $|L(C)|=|C|!$ rational coordinates, including zero coordinates.
Write $m=|C|$ and let $N$ denote the total input length. Then
$$ N=\Omega(m!). $$
Enumerate all $2^m-1$ nonempty committees $S\subseteq C$, evaluate $\widehat\Phi$ under $\alpha_S$, and stop as soon as two satisfying committees are found.
For every $m\ge 1$,
$$ 2^m\le 2m!. $$
Indeed, this holds for $m=1$, and multiplication of the left-hand side by $2$ and the right-hand side by $m+1\ge2$ preserves it inductively.
Thus the running time is
$$ O(2^m|\Phi|) = O(m!|\Phi|) = O(N^2). $$
Consequently, under dense full-coordinate encoding, Continuous ExistsForced is solvable in deterministic polynomial time.
Now suppose that a rational society is encoded by listing only its positive-mass rankings and their binary-encoded rational masses. In particular, a Dirac society can be represented using one ranking and mass $1$, in size polynomial in $m$.
A no-certificate consists of two distinct nonempty committees $S,T\subseteq C$ satisfying $\widehat\Phi$. Both assignments can be written using $O(m)$ bits, and $\widehat\Phi$ can be evaluated on them in polynomial time.
Therefore the complement is in NP, and Continuous ExistsForced is in coNP.
Reduce from UNSAT. Let $\theta(z_1,\ldots,z_n)$ be an arbitrary propositional formula. Construct
$$ C=\{a,b,c_1,\ldots,c_n\}. $$
Let $\mu$ be any Dirac society, represented sparsely. Use only atoms indexed by $\mu$, and define
$$ B = p_{\mu,b} \wedge \neg p_{\mu,a} \wedge \bigwedge_{i=1}^n\neg p_{\mu,c_i}, $$
and
$$ A = p_{\mu,a} \wedge \neg p_{\mu,b} \wedge \theta(p_{\mu,c_1},\ldots,p_{\mu,c_n}). $$
Set
$$ \Phi_\theta=B\vee A. $$
This construction has polynomial size. Moreover, $\Phi_\theta$ is always satisfiable: the committee $\{b\}$ satisfies $B$. Thus the promised propositional satisfiability condition is met, and there is always at least one satisfying continuous rule.
If $\theta$ is unsatisfiable, the $A$ branch cannot hold, while $B$ specifies exactly the committee $\{b\}$. Hence all satisfying continuous rules have the same outcome.
If $\theta$ is satisfiable, choose a satisfying assignment $\beta$ of $\theta$. In addition to $\{b\}$, the committee
$$ \{a\}\cup\{c_i:\beta(z_i)=1\} $$
satisfies $A$. These two committees are distinct. Hence the outcome is not forced.
Therefore,
$$ \theta\in\mathrm{UNSAT} \quad\Longleftrightarrow\quad (C,\mu,\Phi_\theta) \text{ is a yes-instance}. $$
This proves coNP-hardness. Together with membership, the sparse-support version is coNP-complete, even when $\Phi$ admits a satisfying continuous rule.
The stated problem has no representation-independent classification:
Thus specifying only that societies have rational coordinates is insufficient to choose between the two cases.
Strictly speaking, coNP-completeness does not unconditionally imply NP-hardness under polynomial-time many-one reductions. Since the sparse problem lies in coNP, proving it NP-hard would imply $\mathrm{NP}=\mathrm{coNP}$.
⟨structured verdict parsed — rendered above⟩
The central argument is correct. Continuity forces every voting rule to be constant, reducing the problem to counting satisfying assignments of a collapsed propositional formula. The dense-encoding polynomial-time bound and sparse-encoding coNP-completeness reduction are both valid.
Two minor clarifications are needed: treatment of the empty candidate set and precise complexity terminology for the satisfiable-$\Phi$ promise.
For finite nonempty $C$, the simplex $\Delta(L(C))$ is convex and therefore connected. The continuous image of a connected space is connected, while every connected subset of the discrete space $\mathcal P^+(C)$ is a singleton. Hence every continuous $F$ is constant.
The converse—that every constant rule is continuous—is immediate. Thus the claimed bijection between continuous rules and nonempty subsets of $C$ is correct when $C\ne\varnothing$.
The prover assumes $C$ is nonempty, but this is not explicit in USER_TASK. If $C=\varnothing$, then $\mathcal P^+(C)=\varnothing$, so there is no map from the nonempty simplex $\Delta(L(C))$ into the codomain. The asserted bijection then fails. This is a routine edge case and does not affect either complexity result, but it must be stated or handled.
Replacing every $p_{\nu,c}$ by one variable $x_c$ is justified because a continuous rule is constant across all societies. For each nonempty $S\subseteq C$, the corresponding constant rule satisfies $\Phi$ exactly when $\alpha_S$ satisfies $\widehat\Phi$.
Therefore $\mathcal A_\Phi$ is exactly the set of attainable outcomes among continuous rules satisfying $\Phi.
Under the pairwise universal—and hence vacuous when there are no satisfying rules—interpretation of “all satisfying rules have the same outcome,” the criterion $|\mathcal A_\Phi|\le 1$ is correct.
The observation that propositional satisfiability of $\Phi$ does not imply existence of a continuous satisfying rule is also correct.
If at least the input society $\mu$ is represented by explicitly listing all $m!$ coordinates, then the total input length satisfies $N=\Omega(m!)$.
There are $2^m-1$ nonempty committees. Evaluating $\widehat\Phi$ on all of them takes $O(2^m|\Phi|)$ time. The inequality
$$ 2^m\le 2m! $$
is valid for all $m\ge1$, and the stated induction is correct.
Since both $m!=O(N)$ and $|\Phi|=O(N)$, the enumeration cost is $O(N^2)$. Reading or constructing the collapsed formula adds only polynomial overhead. The dense-encoding conclusion is therefore correct.
A no-instance has two distinct nonempty committees satisfying $\widehat\Phi$. Two $m$-bit characteristic vectors form a polynomial-size certificate, and checking distinctness, nonemptiness, and satisfaction of $\widehat\Phi$ is polynomial.
Thus the unrestricted complement is in NP, so the unrestricted sparse problem is in coNP. The same verifier works on inputs satisfying the stated promise.
The reduction from UNSAT is polynomial:
$$ C=\{a,b,c_1,\ldots,c_n\}. $$
The branch
$$ B=p_{\mu,b}\wedge\neg p_{\mu,a}\wedge\bigwedge_i\neg p_{\mu,c_i} $$
is satisfied by exactly the committee $\{b\}$.
The branch
$$ A=p_{\mu,a}\wedge\neg p_{\mu,b}\wedge \theta(p_{\mu,c_1},\ldots,p_{\mu,c_n}) $$
is satisfiable exactly when $\theta$ is satisfiable. Any satisfying assignment $\beta$ yields the distinct nonempty committee
$$ \{a\}\cup\{c_i:\beta(z_i)=1\}. $$
Consequently:
Moreover, $\Phi_\theta$ is propositionally satisfiable and even admits the continuous constant rule with outcome $\{b\}$. Thus the reduction respects the promise.
The equivalence with UNSAT and the coNP-hardness claim are correct.
Strictly, because USER_TASK` presents satisfiability of $\Phi$ as a promise, “coNP-complete” should either be formulated for the natural unrestricted language, with hardness persisting under the satisfiable-input restriction, or accompanied by an explicit promise-problem convention. The proof contains everything needed for the former statement, so this is terminological rather than mathematical.
The response correctly identifies that the task lacks a specified representation of rational societies. Under dense representation, factorial input padding makes exhaustive committee enumeration polynomial in input length. Under sparse representation, the problem is coNP-complete.
The final observation is correct: coNP-completeness alone does not establish NP-hardness under polynomial-time many-one reductions unless $\mathrm{NP}=\mathrm{coNP}$.
⟨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.