Answer: Literally, every instance fails, so verification is in \(\mathrm{P}\). With nonempty coalitions, verification is \(\mathrm{coNP}\)-complete, and violation detection is \(\mathrm{NP}\)-complete.
Theorem 4.2 — class: hardness
Given candidates \(C\), committee size \(k\), committee \(W\subseteq C\) with \(|W|=k\), distinct approval types \(A_1,\ldots,A_\tau\subseteq C\), and rational masses \(\mu_i\ge0\) summing to \(1\), decide whether for every integer \(\ell\ge1\), witness set \(Q\subseteq C\), and type subset \(I\subseteq\{1,\ldots,\tau\}\) satisfying \(\sum_{i\in I}\mu_i\ge|Q|/k\) and \(|A_i\cap Q|\ge\ell\) for all \(i\in I\), we have \(|W\cap\bigcup_{i\in I}A_i|\ge\ell\).
Let \(C\) be a candidate set with \(m=|C|\), let \(1\le k\le m\) be an integer, and let \(W\subseteq C\) satisfy \(|W|=k\).
A society is given by its support: distinct approval types \(A_1,\ldots,A_\tau\subseteq C\) with positive binary rational masses \(\mu_i\), where \(\sum_{i=1}^{\tau}\mu_i=1\). Approval sets may be empty. Here \(\tau\) is the support size, not the number of possible approval sets; let \(L\) be the total input bit length.
The verification problem asks whether, for every integer \(\ell\ge1\), every witness set \(Q\subseteq C\), and every type subset \(I\subseteq\{1,\ldots,\tau\}\), the conditions \(\sum_{i\in I}\mu_i\ge |Q|/k\) and \(|A_i\cap Q|\ge\ell\) for all \(i\in I\) imply \(|W\cap\bigcup_{i\in I}A_i|\ge\ell\). Coalitions in this formulation select whole types.
State running times in \(m,\tau,L\), and \(k\).
Is this verification problem in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?
For a finite list of voters, verifying Full Proportional Justified Representation with the same mass threshold replaced by the coalition's fraction of voters is \(\mathrm{coNP}\)-complete. No continuous-side complexity result is assumed here.
Literally, every instance fails: take \(I=Q=\varnothing\) and \(\ell=1\). Both premises hold, while the conclusion is false. Thus the literal problem is decidable in constant time.
For the intended, nondegenerate question, I require \(I\ne\varnothing\). Under this interpretation, verification is \(\mathrm{coNP}\)-complete, and detecting a violation is \(\mathrm{NP}\)-complete.
The proof below uses only the supplied finite-voter hardness result; it derives the complexity of the support representation.
A violation consists of a nonempty type subset \(I\), a candidate subset \(Q\), and an integer \(\ell\) satisfying
\[ \sum_{i\in I}\mu_i\ge \frac{|Q|}{k}, \qquad |A_i\cap Q|\ge\ell\ \text{for every }i\in I, \qquad \left|W\cap\bigcup_{i\in I}A_i\right|<\ell. \]
Because \(I\ne\varnothing\), the approval condition implies \(\ell\le |Q|\). Because the total mass is \(1\), the threshold implies \(|Q|\le k\). Hence every violation satisfies \(1\le\ell\le |Q|\le k\), and has a certificate of length \(O(m+\tau+\log(k+1))\).
All conditions can be checked exactly in polynomial time. To justify the arithmetic bound, write \(\mu_i=a_i/b_i\), and set
\[ D=\prod_{i=1}^{\tau}b_i, \qquad w_i=a_i(D/b_i). \]
The integers \(D\) and \(w_i\) have \(O(L)\) bits. The mass inequality is equivalent to the integer comparison
\[ k\sum_{i\in I}w_i\ge |Q|D. \]
Using ordinary integer arithmetic and direct scans of approval sets, a conservative certificate-checking bound, including this preprocessing, is \(O(\tau(m+L)^2)\) bit operations. Therefore verification belongs to \(\mathrm{coNP}\).
Consider a finite electorate \(V\), with \(n=|V|\ge1\). Partition its voters into nonempty classes \(V_1,\ldots,V_\tau\), where all voters in \(V_i\) have approval set \(A_i\), and the sets \(A_i\) are distinct. Construct the support instance with masses
\[ \mu_i=\frac{|V_i|}{n}. \]
Keep \(C,k,W\) unchanged.
Claim. The finite electorate has a violation if and only if this support instance has a violation.
From a voter violation to a type violation. Suppose a nonempty voter coalition \(S\subseteq V\), together with \(Q,\ell\), witnesses a violation. Define
\[ I=\{i:S\cap V_i\ne\varnothing\}, \qquad S^\ast=\bigcup_{i\in I}V_i. \]
Then \(S\subseteq S^\ast\), so
\[ \sum_{i\in I}\mu_i=\frac{|S^\ast|}{n} \ge\frac{|S|}{n} \ge\frac{|Q|}{k}. \]
For each \(i\in I\), some voter in \(S\) has approval set \(A_i\). Consequently \(|A_i\cap Q|\ge\ell\). Moreover, adding the remaining voters of these types introduces no new approval sets:
\[ \bigcup_{v\in S}A_v=\bigcup_{i\in I}A_i. \]
Thus the number of approved committee members remains below \(\ell\), and \(I,Q,\ell\) witnesses a support-instance violation.
From a type violation to a voter violation. Conversely, given a support violation \(I,Q,\ell\), select the voter coalition \(S=\bigcup_{i\in I}V_i\). Its voter fraction is exactly \(\sum_{i\in I}\mu_i\); its approval union is exactly \(\bigcup_{i\in I}A_i\); and every member satisfies the same approval condition. Hence it witnesses a finite-voter violation.
This proves the claim.
The construction is polynomial: grouping explicitly listed ballots requires polynomial time, and each mass has numerator and denominator of \(O(\log(n+1))\) bits. Using incidence-vector encoding, the resulting input length is \(O(m+\tau m+\tau\log(n+1))\), with \(\tau\le n\).
The supplied theorem states that finite-voter FPJR verification is \(\mathrm{coNP}\)-complete; this result also appears in [Kalayci, Liu, and Kempe, *Full Proportional Justified Representation*](https://www.ifaamas.org/Proceedings/aamas2025/pdfs/p1070.pdf). The equivalence just proved gives a polynomial many-one reduction to support-instance verification. Thus the latter is \(\mathrm{coNP}\)-hard. Together with Section 2, it is \(\mathrm{coNP}\)-complete.
There is also a direct algorithm whose dependence on the parameters can be stated explicitly.
Enumerate every \(Q\subseteq C\) with \(1\le |Q|\le k\), and every \(S\subseteq W\) with \(|S|<|Q|\). Define
\[ E(Q,S)= \{i:A_i\cap W\subseteq S \text{ and }|A_i\cap Q|\ge |S|+1\}. \]
Report a violation precisely when some enumerated pair satisfies
\[ \sum_{i\in E(Q,S)}\mu_i\ge\frac{|Q|}{k}. \]
Soundness. The positive threshold makes \(E(Q,S)\) nonempty. Set \(I=E(Q,S)\) and \(\ell=|S|+1\). Every selected type approves at least \(\ell\) candidates in \(Q\), while their committee approval union is contained in \(S\), so its size is below \(\ell\).
Completeness. Given any violation \(I,Q,\ell\), put \(S=W\cap\bigcup_{i\in I}A_i\). Then \(|S|<\ell\le |Q|\le k\), so \((Q,S)\) is enumerated. Every \(i\in I\) belongs to \(E(Q,S)\), because \(|A_i\cap Q|\ge\ell\ge |S|+1\). Positivity of the masses therefore implies that \(E(Q,S)\) also meets the threshold.
Let \(B(m,k)=\sum_{q=1}^{k}\binom{m}{q}\). With the exact arithmetic described above, the algorithm runs in
\[ O\!\left(2^k B(m,k)\,\tau(m+L)^2\right) \]
bit operations. This is polynomial for each fixed \(k\), and is at most \(O(4^m\tau(m+L)^2)\).
For nonempty coalitions, the exact classification is \(\mathrm{coNP}\)-completeness. Consequently:
Thus the intended problem has a complete hardness classification, with the usual distinction between verification and finding a violation.
⟨structured verdict parsed — rendered above⟩
The output resolves the intended problem correctly: with nonempty coalitions, verification is \(\mathrm{coNP}\)-complete, and violation detection is \(\mathrm{NP}\)-complete. The reduction, certificate bounds, and enumeration algorithm are valid. No major or minor proof defects were found.
The empty-coalition observation is correct. With \(I=Q=\varnothing\) and \(\ell=1\), the mass inequality holds, the approval condition is vacuous, and the conclusion fails.
The prover then explicitly requires \(I\ne\varnothing\), which is the natural interpretation consistent with the supplied finite-voter hardness statement. Under the verifier’s stipulated standard, this clarification is acceptable. Crucially, the prover also resolves that intended question; it does not rely solely on the degenerate literal reading.
Every claimed certificate bound is valid:
The exact arithmetic is also correct. Since the denominator bit lengths sum to at most \(L\), the product \(D\) has \(O(L)\) bits. Each integer \(w_i=a_i(D/b_i)\) likewise has \(O(L)\) bits. Clearing denominators gives exactly
\(k\sum_{i\in I}w_i\ge |Q|D\).
Ordinary multiplication, exact division, addition, and approval scans fit within the stated conservative bound \(O(\tau(m+L)^2)\) bit operations. Thus violation detection belongs to \(\mathrm{NP}\), establishing verification membership in \(\mathrm{coNP}\).
Both directions of the equivalence are sound.
For a finite-voter violation, replacing the coalition by all voters of every represented type:
The last point is decisive: the enlarged coalition introduces copies of existing approval sets, so its committee representation remains below \(\ell\).
Conversely, selecting all voters of the types in a support violation reproduces its mass, approval union, and individual approval conditions exactly.
The constructed support satisfies every input requirement: its types are distinct, its masses are positive rationals summing to \(1\), and \(C,k,W\) remain valid. Empty approval types cause no difficulty; they cannot participate in a violation with positive \(\ell\).
Grouping an explicitly listed electorate is polynomial time. The masses require \(O(\log(n+1))\) bits each, and the stated incidence-vector output-length bound is valid. No expansion of arbitrary binary rational masses into an electorate is required: the reduction runs only from the explicit finite electorate to the support representation.
The finite-voter hardness theorem is explicitly supplied by USER_TASK, and its hypotheses match this construction. The supplementary citation also supports the claim: Theorem 4.2 states the finite-profile verification result. [Kalayci, Liu, and Kempe, *Full Proportional Justified Representation*](https://www.ifaamas.org/Proceedings/aamas2025/pdfs/p1070.pdf).
Therefore the polynomial many-one reduction establishes \(\mathrm{coNP}\)-hardness, and the membership argument establishes completeness.
The soundness argument is correct. Because enumerated \(Q\) is nonempty, its threshold is positive. If the test succeeds, \(E(Q,S)\) is therefore nonempty. Taking \(\ell=|S|+1\) gives the required approval condition, while the committee approval union is contained in \(S\) and hence has size below \(\ell\).
The completeness argument is also correct. For an existing violation, its actual committee approval union \(S\) satisfies
\(|S|<\ell\le |Q|\le k\).
Thus the pair is enumerated. Every violating type belongs to \(E(Q,S)\), and the nonnegative masses ensure that enlarging the selected type set preserves the threshold.
There are at most \(2^k B(m,k)\) enumerated pairs, so the stated running time
\(O(2^k B(m,k)\tau(m+L)^2)\)
is valid. For fixed \(k\), \(B(m,k)\) is polynomial in \(m\). Since \(k\le m\) and \(B(m,k)\le 2^m\), the bound \(O(4^m\tau(m+L)^2)\) is also valid.
All distinctions in Section 5 are correct:
The intended complexity question is settled. No missing lemma, false assertion, unverified theorem application, or repair requiring additional mathematics was identified. No additional clarification is necessary.
⟨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.