Answer: For each supplied family, the exact guarantees are \(\Gamma_g=\min_{W,V\in\mathcal K}\lambda_g(W,V)\), with \(\lambda_g\) given by the rational linear programs above. Both guarantees are rational and attained, and the ratio-threshold answer is yes exactly when \(q\geq\Gamma_g\). The sharp unrestricted representation guarantee is \(k/(2k-1)\).
Theorem 2 — class: algorithmic
Given a candidate set \(C\), committee size \(k\), finite support \(\mathcal T\subseteq 2^C\), welfare choice \(g\in\{u,r\}\), and rational threshold \(q\), does there exist a rational distribution \(\mu\) supported on \(\mathcal T\) and a size-\(k\) PAV-winning committee \(W\) such that \(g_\mu(W)/\max_{|W'|=k}g_\mu(W')\le q\), where \(u_\mu(W)=\sum_{A\in\mathcal T}\mu_A|A\cap W|\) and \(r_\mu(W)=\sum_{A\in\mathcal T}\mu_A\mathbf 1[A\cap W\ne\varnothing]\), with the denominator positive?
Let \(C\) have \(m\geq1\) candidates, let \(1\leq k\leq m\), and let the explicitly listed allowable approval types \(\mathcal T\subseteq2^C\) contain at least one nonempty set. The input also specifies \(g\in\{u,r\}\) and a binary rational threshold \(q\).
A society is given by its support: its \(\tau\) types with positive mass, each mass a binary rational. Here masses are sought, rather than supplied: \(\mu_A\in\mathbb Q_{\geq0}\), \(\sum_{A\in\mathcal T}\mu_A=1\), and \(\operatorname{supp}(\mu)\subseteq\mathcal T\). Thus \(\tau\) is the actual support size, not the number of possible approval sets.
For a size-\(k\) committee \(W\), define \(u_\mu(W)=\sum_{A\in\mathcal T}\mu_A|A\cap W|\) and \(r_\mu(W)=\sum_{A\in\mathcal T}\mu_A\mathbf1[A\cap W\neq\varnothing]\).
A PAV-winning committee maximizes \(\sum_{A\in\mathcal T}\mu_A H(|A\cap W|)\) over all size-\(k\) committees, where \(H(0)=0\) and \(H(j)=\sum_{i=1}^{j}1/i\); every tied maximizer is eligible.
Write \(R_g(\mu,W)=g_\mu(W)/\max_{|V|=k}g_\mu(V)\), considering only societies with positive denominator. The ratio-threshold question asks whether some such rational society and PAV-winning \(W\) satisfy \(R_g(\mu,W)\leq q\).
The support-restricted approximation guarantee is \(\inf_{\mu}\min_{W\text{ PAV-winning}}R_g(\mu,W)\), with the infimum over these societies. State any running times in \(m,|\mathcal T|,\tau,k,L\), where \(L\) is the input bit length.
What tight utilitarian and representation approximation guarantees does PAV provide on rational mass societies restricted to the supplied \(\mathcal T\), and which boundary thresholds are attained in the ratio-threshold question?
For finite electorates, PAV's unrestricted utilitarian guarantee lies between \(1/(2+\sqrt{k})\) and \(2/\sqrt{k}\), and its representation guarantee lies between \(1/2\) and \(1/2+1/(4k-2)\). [Verified source](https://www.dbai.tuwien.ac.at/proj/sudema/papers/aij-guarantees.pdf).
No result settling the prescribed-support mass question was located in the literature search.
For every supplied family \(\mathcal T\), both guarantees are rational, exactly computable, and attained by rational masses. In particular, the ratio-threshold question has answer yes exactly when the supplied threshold is at least the corresponding guarantee, including equality.
The values depend on \(\mathcal T\). Below is an explicit linear-program formula computing them. I also prove the sharp unrestricted representation guarantee
\(\frac{k}{2k-1}\), and give a nontrivial family for which both support-restricted guarantees have explicit formulas.
Remove the empty type and write
\(\mathcal T_+=\mathcal T\setminus\{\varnothing\}\),
\(t=|\mathcal T_+|\), and
\(\mathcal K=\{X\subseteq C:|X|=k\}\).
By hypothesis, \(t\geq1\). Let \(N=|\mathcal K|=\binom{m}{k}\).
For \(A\in\mathcal T_+\) and \(X\in\mathcal K\), define
\(h_{A,X}=H(|A\cap X|)\),
\(b^u_{A,X}=|A\cap X|\), and
\(b^r_{A,X}=\mathbf1[A\cap X\neq\varnothing]\).
Fix \(g\in\{u,r\}\). For each ordered pair \(W,V\in\mathcal K\), form the following rational linear program, with variables \(x_A\), \(A\in\mathcal T_+\):
Objective: minimize
\(\sum_{A\in\mathcal T_+}b^g_{A,W}x_A\).
Constraints:
Let \(\lambda_g(W,V)\) be its optimum, assigning value \(+\infty\) to an infeasible program. Then the exact support-restricted guarantee is
\(\displaystyle \Gamma_g(C,\mathcal T,k)=\min_{W,V\in\mathcal K}\lambda_g(W,V).\)
Thus this is an exact formula for both requested guarantees, using only finitely many ordinary rational linear programs. No strict inequality or limiting optimization is needed.
First, removing the empty type preserves every relevant ratio. Indeed, positive denominator is equivalent to positive total mass
\(\alpha=\sum_{A\neq\varnothing}\mu_A\).
For such a society, set \(\widehat\mu_A=\mu_A/\alpha\) on nonempty types and set its empty-type mass to zero. Every committee’s PAV score and both objective values are divided by \(\alpha\). Consequently, the winners and ratios remain unchanged.
Now take a normalized society on \(\mathcal T_+\), a PAV winner \(W\), and a committee \(V\) maximizing \(g_\mu\). Its optimum \(d=g_\mu(V)\) is positive. Setting \(x_A=\mu_A/d\) satisfies all the displayed constraints, and the linear-program objective is exactly \(R_g(\mu,W)\).
Conversely, let \(x\) be feasible and put \(s=\sum_Ax_A\). The normalization constraint implies \(s>0\). Define \(\mu_A=x_A/s\). The committee inequalities make \(W\) PAV-winning and \(V\) optimal for \(g\), with \(g_\mu(V)=1/s>0\). Therefore
\(\displaystyle R_g(\mu,W)=\sum_A b^g_{A,W}x_A.\)
These two constructions establish the formula, provided the linear-program minima are attained. That follows from boundedness, as shown next.
For any nonempty \(A\), a uniformly random \(X\in\mathcal K\) satisfies
\(\displaystyle \mathbb E|A\cap X|=\frac{k|A|}{m}\geq\frac{k}{m}.\)
Also, fixing any \(a\in A\),
\(\displaystyle \Pr(A\cap X\neq\varnothing)\geq\Pr(a\in X)=\frac{k}{m}.\)
Hence, for either objective and any nonnegative vector \(x\),
\(\displaystyle \frac1N\sum_{X\in\mathcal K}\sum_A b^g_{A,X}x_A\geq\frac{k}{m}\sum_Ax_A.\)
In a feasible program, every committee’s \(g\)-value is at most the normalized value \(1\) of \(V\). Thus \(\sum_Ax_A\leq m/k\). Each feasible set is therefore closed and bounded.
At least one program is feasible: put all society mass on any nonempty allowed type, choose a PAV winner and a \(g\)-optimal committee, and apply the preceding construction. Every feasible objective value lies in \((0,1]\), since \(W\) has positive PAV score and \(V\) is \(g\)-optimal.
The preceding formula already proves attainment over real masses. The following argument proves rational attainment and gives a stronger bound on the support of a worst-case society.
For a committee \(W\), define its winner polytope
\(\displaystyle P_W=\left\{\mu\in\mathbb R_{\geq0}^{\mathcal T_+}:\sum_A\mu_A=1,\ \sum_A(h_{A,W}-h_{A,X})\mu_A\geq0\text{ for every }X\in\mathcal K\right\}.\)
Every nonempty \(P_W\) is a bounded rational polyhedron. We use the elementary polytope theorem: such a polyhedron is the convex hull of finitely many vertices, and every vertex is the unique solution of a full-rank subsystem of active constraints. Rational coefficients therefore give rational vertices.
For every normalized society on \(\mathcal T_+\), the averaging calculation above gives
\(\max_Xg_\mu(X)\geq k/m>0\).
If \(\mu\in P_W\), then \(W\) also has positive \(g\)-value: some committee has positive PAV score, so its PAV-winning score is positive.
Let \(Z_W\) denote the vertex set of a nonempty \(P_W\), and put
\(\gamma_W=\min_{z\in Z_W}R_g(z,W)\).
For every vertex \(z\) and every committee \(V\),
\(\displaystyle g_z(W)\geq\gamma_W\max_Xg_z(X)\geq\gamma_Wg_z(V).\)
Write any \(\mu\in P_W\) as a convex combination
\(\mu=\sum_{z\in Z_W}\theta_z z\).
Both committee values are linear in the masses, so summing the preceding inequality gives
\(g_\mu(W)\geq\gamma_Wg_\mu(V)\) for every \(V\).
Taking a maximizing \(V\) proves \(R_g(\mu,W)\geq\gamma_W\).
Consequently,
\(\displaystyle \Gamma_g(C,\mathcal T,k)=\min_{\substack{W\in\mathcal K\\P_W\neq\varnothing}}\ \min_{z\in Z_W}R_g(z,W).\)
This is a finite minimum of rational numbers, attained at a rational society.
Suppose a vertex \(z\in P_W\) has actual support size \(\tau\). Restrict its active equations to its positive coordinates. They must have rank \(\tau\); otherwise a sufficiently small nonzero perturbation in their nullspace would preserve positivity and all inactive strict inequalities, contradicting extremality.
There is one normalization equation and at most \(N-1\) nontrivial winner inequalities. Thus
\(\displaystyle \tau\leq\min\{t,N\}.\)
For an explicit bit bound, let \(D=k!\). Every \(DH(j)\), \(0\leq j\leq k\), is an integer. Clearing denominators makes the winner coefficients integers of absolute value at most \(Dk\).
The normalization row is independent of the active homogeneous winner rows: its scalar product with \(z\) is \(1\), whereas theirs is zero. Hence one can determine the positive coordinates using normalization and \(\tau-1\) independent active winner equations. Cramer’s rule and the determinant bound
\(|\det M|\leq\tau!(Dk)^\tau\)
show that each mass has numerator and denominator bit lengths
\(\displaystyle O\!\left(\tau\bigl(k\log(k+1)+\log(\tau+1)\bigr)\right).\)
The same order of bit length suffices for the resulting ratio. In particular, unrestricted rational denominators are unnecessary: a worst-case witness has polynomially bounded encoding length in \(t\) and \(k\).
Enumerating committees and their coefficients takes
\(O(mt+Nt\,k)\) elementary operations when approval types are stored as membership vectors.
Each linear program in Section 1 has \(t\) variables, at most \(2N-2\) nontrivial committee inequalities, one normalization equation, and nonnegativity constraints. Its coefficient bit lengths are \(O(k\log(k+1))\).
Applying the standard polynomial-bit-complexity theorem for rational linear programming therefore computes the exact guarantee in time
\(\displaystyle N^2\operatorname{poly}(N,m,|\mathcal T|,k,L),\qquad N=\binom{m}{k}.\)
The theorem applies because the programs have explicitly listed rational coefficients and, when feasible, bounded feasible sets. For fixed \(k\), this running time is polynomial in \(m,|\mathcal T|,L\); the displayed algorithm is exponential in general.
One can alternatively enumerate vertices of each \(P_W\). Choosing \(t-1\) active inequalities, together with normalization, gives the bound
\(\displaystyle N\binom{t+N-1}{t-1}\operatorname{poly}(N,m,t,k,L).\)
Singular systems are discarded, and each remaining solution is checked against every constraint.
For a proposed society with actual support \(\tau\) and maximum mass bit length \(B\), exhaustive verification of PAV optimality and the ratio takes
\(\displaystyle O\!\left((m\tau+N\tau k)\operatorname{poly}(L+\tau B+k\log(k+1))\right)\)
bit operations. Here \(\tau\) is the support actually supplied in the witness, not the number of allowable types.
For every allowed family,
\(\displaystyle \Gamma_r(C,\mathcal T,k)\geq\frac{k}{2k-1}.\)
This bound is attained by a rational society when the required types are allowed. Thus the unrestricted representation guarantee is exactly \(\frac{k}{2k-1}\).
Fix a society, a PAV winner \(W\), and a representation-optimal committee \(V\). Choose a bijection \(f:W\to V\) fixing every member of \(W\cap V\). Each nonidentity pair defines a valid size-\(k\) swap; identity pairs leave \(W\) unchanged. PAV optimality implies that the sum of the score changes of these \(k\) swaps is nonpositive.
For one approval type \(A\), write
\(w=|A\cap W|\),
\(v=|A\cap V|\), and
\(a=|\{c\in W:c\in A,\ f(c)\in A\}|\).
Let \(\delta_A\) be its summed contribution to the swaps.
If \(w=0\), then \(\delta_A=v\).
If \(w>0\), there are \(v-a\) pairs adding an approved candidate without removing one, and \(w-a\) pairs removing an approved candidate without adding one. Therefore
\(\displaystyle \delta_A=\frac{v-a}{w+1}-\frac{w-a}{w}.\)
Three bounds follow:
For the third bound, when \(w<k\), the displayed expression equals
\(v/(w+1)-1+a/(w(w+1))\), which is at least
\(-w/(w+1)\geq-(k-1)/k\).
When \(w=k\), every outgoing candidate is approved, so \(a=v\), and the expression is
\(-(k-v)/k\geq-(k-1)/k\).
Let \(\rho\) be the mass represented by \(W\), let \(\eta\) be the mass represented by both \(W\) and \(V\), and let \(\xi\) be the mass represented by \(V\) but not \(W\). Summing the bounds and using PAV optimality gives
\(\displaystyle 0\geq\sum_A\mu_A\delta_A\geq\xi-(\rho-\eta)-\frac{k-1}{k}\eta=\xi-\rho+\frac{\eta}{k}.\)
Hence \(\xi+\eta/k\leq\rho\). Because \(\eta\leq\rho\),
\(\displaystyle r_\mu(V)=\xi+\eta\leq\rho+\frac{k-1}{k}\eta\leq\frac{2k-1}{k}\rho.\)
Dividing by the positive optimum proves the bound.
Let \(C=X\cup Y\), with disjoint sets \(X=\{x_1,\ldots,x_k\}\) and \(Y=\{y_1,\ldots,y_k\}\). Allow \(X\) and all singleton types \(\{y_i\}\). Assign
\(\mu_X=1/2\) and \(\mu_{\{y_i\}}=1/(2k)\).
A committee containing \(j\) candidates from \(X\) has PAV score
\(F(j)=H(j)/2+(k-j)/(2k)\).
Its increments satisfy
\(F(j+1)-F(j)=1/(2(j+1))-1/(2k)\geq0\),
so \(W=X\) is a winner.
Its representation value is \(1/2\). A representation-optimal committee contains one candidate from \(X\) and \(k-1\) from \(Y\), giving optimum \((2k-1)/(2k)\). Thus the ratio is \(k/(2k-1)\). This equality construction also appears in the [cited paper](https://www.dbai.tuwien.ac.at/proj/sudema/papers/aij-guarantees.pdf).
In particular, for every fixed finite \(k\), the threshold \(1/2\) is unattainable.
A general elementary lower bound is
\(\displaystyle \Gamma_u(C,\mathcal T,k)\geq\frac{H(k)}{k}.\)
Indeed, \(H(j)/j\) is nonincreasing for positive integers \(j\): the newly added term \(1/(j+1)\) is at most the preceding average \(H(j)/j\). Consequently,
\(H(j)\geq jH(k)/k\) for \(0\leq j\leq k\), while \(H(j)\leq j\).
Writing \(p_\mu\) for PAV score, a PAV winner \(W\) and utilitarian optimum \(V\) therefore satisfy
\(\displaystyle u_\mu(W)\geq p_\mu(W)\geq p_\mu(V)\geq\frac{H(k)}{k}u_\mu(V).\)
The cited finite-electorate lower bound also transfers exactly to rational masses. Clearing their denominators produces a finite electorate whose PAV scores and objective values are all multiplied by the same integer. Thus
\(\displaystyle \Gamma_u(C,\mathcal T,k)\geq\max\left\{\frac{H(k)}{k},\frac1{2+\sqrt{k}}\right\}.\)
The second bound is [Theorem 2 of the cited paper](https://www.dbai.tuwien.ac.at/proj/sudema/papers/aij-guarantees.pdf).
For the family
\(\mathcal T=\{X,\{y_1\},\ldots,\{y_k\}\}\)
used above, both exact guarantees are
\(\displaystyle \Gamma_r=\frac{k}{2k-1},\qquad \Gamma_u=\min_{0\leq p\leq k-1}\frac{p^2+k}{k(p+1)}.\)
The representation equality is already proved. Here is a proof of the utilitarian formula.
Write \(a=\mu_X\) and \(b_i=\mu_{\{y_i\}}\). Every candidate in \(X\) has approval score \(a\); candidate \(y_i\) has approval score \(b_i\).
Suppose a PAV winner \(W\) contains \(p\) candidates from \(X\).
If \(a=0\), PAV and utilitarian scores coincide. If \(p=0\), then \(W=Y\); swapping any \(y_i\) for an \(X\)-candidate implies \(b_i\geq a\), so \(W\) is utilitarian-optimal. If \(p=k\), swapping an \(X\)-candidate for any \(y_i\) implies \(b_i\leq a/k\leq a\), again making \(W\) utilitarian-optimal.
It remains to consider \(a>0\) and \(1\leq p\leq k-1\). Let \(S\) be the selected singleton candidates. Single-swap optimality gives
\(\displaystyle b_i\geq\frac{a}{p+1}\quad(i\in S),\qquad b_j\leq\frac{a}{p}\leq a\quad(j\notin S).\)
Let \(h\) be the number of singleton candidates with \(b_i>a\). All belong to \(S\). Write their total mass as \(ha+d\), where \(d\geq0\). The utilitarian optimum is exactly \(ka+d\): select these \(h\) candidates and fill the other positions with candidates from \(X\).
Meanwhile,
\(\displaystyle u_\mu(W)\geq pa+ha+d+\frac{k-p-h}{p+1}a =\frac{p^2+k}{p+1}a+\frac{hp}{p+1}a+d \geq\frac{p^2+k}{p+1}a+d.\)
Since \((p^2+k)/(p+1)\leq k\), adding \(d\geq0\) to numerator and denominator cannot decrease the ratio below
\(\displaystyle \frac{p^2+k}{k(p+1)}.\)
This proves the required lower bound for every society on this family.
For attainment, fix \(0\leq p\leq k-1\). Give \(X\) mass \((p+1)/(k+1)\), give \(k-p\) singleton types mass \(1/(k+1)\) each, and give the remaining singleton types mass zero.
A committee containing \(p\) candidates from \(X\) and all positive-mass singleton candidates is PAV-winning. To check this, committees with fewer than \(p\) \(X\)-candidates can replace a zero-mass singleton candidate by an \(X\)-candidate and improve. Starting at \(p\) \(X\)-candidates, the score increment from increasing their number from \(j\) to \(j+1\) is
\(\displaystyle \frac{p+1}{(k+1)(j+1)}-\frac1{k+1}.\)
It is zero at \(j=p\) and negative thereafter. Thus the stated committee is a global maximizer.
The utilitarian optimum consists of \(k\) candidates from \(X\), and the resulting ratio is exactly \((p^2+k)/(k(p+1))\). Its actual support has size \(k-p+1\). Choosing a minimizing \(p\) proves attainment of the formula.
For either objective, the complete threshold characterization is
\(\displaystyle \text{a qualifying rational society exists}\quad\Longleftrightarrow\quad q\geq\Gamma_g(C,\mathcal T,k).\)
Equality is included because the exact guarantee has a rational attaining society. Thus no boundary gap arises from requiring rational masses.
Also, \(0<\Gamma_g\leq1\). Hence every \(q\leq0\) is a no-instance, and every \(q\geq1\) is a yes-instance. When \(k=1\), when \(k=m\), or when all nonempty allowable types are singletons, both guarantees equal \(1\).
The prescribed-family question is therefore settled by the exact formulas above; no closed formula for the unrestricted utilitarian worst case is asserted.
⟨structured verdict parsed — rendered above⟩
The prover resolves the prescribed-family guarantee and boundary-attainment questions. I found no mathematical errors or gaps requiring repair. The LP formulas give exact guarantees for each supplied family; they do not claim a closed formula for the unrestricted utilitarian guarantee or a general polynomial-time algorithm.
Under \(1\leq k\leq m\), positive mass on a nonempty type implies a positive optimum for both objectives: some size-\(k\) committee intersects that type. Conversely, mass concentrated on the empty type gives zero denominator.
Thus the asserted equivalence between positive denominator and \(\alpha>0\) is correct. Renormalizing nonempty masses multiplies every PAV score and objective value by the same positive factor. It preserves all maximizers, including ties, and preserves ratios. Rationality is also preserved.
For a society, a PAV winner \(W\), and a \(g\)-optimal committee \(V\), the denominator \(d=g_\mu(V)\) is positive. The substitution \(x_A=\mu_A/d\) satisfies every constraint:
The LP objective is exactly the required ratio.
Conversely, the normalization constraint implies \(s=\sum_Ax_A>0\). Normalization by \(s\) produces a society for which \(W\) is PAV-winning and \(V\) is \(g\)-optimal, with positive denominator \(1/s\). The displayed ratio identity is correct.
These constructions preserve rationality when their inputs are rational. Although the LPs can initially be considered over real vectors, Section 2 separately establishes rational attainment, so there is no unresolved real-versus-rational gap.
Both averaging calculations are correct. A fixed candidate belongs to a uniformly random size-\(k\) committee with probability \(k/m\), and a nonempty type contains at least one such candidate.
In a feasible LP, all committee objective values are at most \(1\). Consequently, the averaging inequality gives \(\sum_Ax_A\leq m/k\). Together with nonnegativity and finitely many weak linear constraints, this proves that each nonempty feasible set is compact. Its linear objective therefore attains a minimum.
At least one LP is feasible: a society concentrated on any allowed nonempty type has positive denominator, and both required maximizers exist over the finite committee set.
Every feasible objective is positive. Indeed, positive denominator implies that some committee has positive PAV score; a PAV winner consequently has positive PAV score and hence positive value for either objective. Its value is at most that of \(V\). Thus the asserted interval \((0,1]\) is correct.
Each nonempty \(P_W\) is a bounded rational polyhedron. The stated polytope theorem applies: such a polyhedron is the convex hull of its finitely many vertices, and full-rank active constraint systems give rational coordinates.
The denominator is uniformly positive on the normalized nonempty-type simplex. The PAV-winning committee also has positive numerator. Therefore every vertex ratio and \(\gamma_W\) are well-defined and positive.
The key convex-combination argument is valid. For each vertex, the inequality against every fixed committee \(V\) follows from the definition of \(\gamma_W\). Both sides are linear in the masses, so the inequality survives convex combination. Maximizing over \(V\) gives the claimed lower bound throughout \(P_W\).
Consequently, a worst ratio is attained at a rational vertex of some winner polytope. This proves rationality and rational attainment of both exact guarantees without relying on density or limiting arguments.
The rank argument on positive coordinates is correct. If the active equations had deficient rank there, a sufficiently small perturbation in both directions would preserve positivity, active equations, and all inactive inequalities. That would contradict extremality.
There are at most \(N-1\) nontrivial winner inequalities plus normalization, yielding \(\tau\leq\min\{t,N\}\). This concerns actual positive support, as the task requires.
The denominator clearing is valid because every denominator in \(H(j)\), for \(j\leq k\), divides \(k!\). The coefficient bound \(Dk\) is sufficient.
Normalization is independent of the active homogeneous winner rows for the stated reason. Cramer’s rule therefore applies to a nonsingular system on the positive coordinates. The determinant bound \(\tau!(Dk)^\tau\) is valid and gives the stated mass bit lengths. The ratio uses these same rational coordinates and integer objective coefficients, so its bit length also satisfies the stated order.
Committee coefficient construction can use membership-vector lookups and inspect the \(k\) committee members for each type. The stated elementary-operation count is sufficient.
Each pairwise LP has \(t\) variables, at most \(2N-2\) nontrivial committee inequalities, and coefficients with the stated polynomial bit lengths. The applicable rational-LP theorem provides feasibility testing and exact rational optimization in time polynomial in the explicitly written LP encoding. The prover has checked rational coefficients, finite explicit constraint lists, bounded feasible sets, and bounded objective values. Its resulting overall bound is therefore justified.
For fixed \(k\), \(N=\binom{m}{k}\) is polynomial in \(m\). For variable \(k\), the displayed enumeration algorithm can require exponentially many committees. This establishes the stated algorithmic upper bounds, without establishing general polynomial-time solvability or hardness.
The alternative vertex enumeration is also valid: a vertex admits normalization together with \(t-1\) independent active inequalities, chosen among at most \(t+N-1\) inequalities. Singular choices can be discarded and the remaining candidates checked.
Exhaustive witness verification correctly uses the actual support size \(\tau\), with rational-arithmetic costs accounted for by the polynomial factor.
A bijection fixing \(W\cap V\) pairs every remaining member of \(W\) with a member of \(V\setminus W\). Thus each nonidentity pair gives a valid swap. Each swap has nonpositive PAV score change.
The per-type formula for \(\delta_A\) correctly counts additions without removals and removals without additions. Identity pairs and pairs approving both candidates contribute zero.
All three bounds check out. In particular:
Types represented by neither committee contribute zero. The partition into masses \(\rho-\eta\), \(\eta\), and \(\xi\) therefore gives the displayed summed inequality. The subsequent inequalities use \(\eta\leq\rho\) correctly and yield the claimed representation ratio.
The equality example is valid. The increments of \(F\) are nonnegative through the final increment, which is zero, so \(X\) is eligible under the specified tie convention. The representation optimum and resulting ratio are correct, including when \(k=1\).
The same equality construction appears in Appendix A, Theorem 2 of the [cited paper](https://www.dbai.tuwien.ac.at/proj/sudema/papers/aij-guarantees.pdf). The prover’s sharper lower bound is justified by its own exchange argument.
The monotonicity argument for \(H(j)/j\) is valid, and both harmonic-score comparisons hold throughout \(0\leq j\leq k\). The chain involving PAV optimality consequently proves the elementary bound.
The finite-electorate transfer is exact: clearing rational mass denominators produces integer voter multiplicities and multiplies all relevant scores by the same positive integer. The claimed lower bound is indeed stated in Theorem 2 of the [cited paper](https://www.dbai.tuwien.ac.at/proj/sudema/papers/aij-guarantees.pdf), whose PAV formulation covers the winning committees used here.
In the party-and-singletons family, the cases \(a=0\), \(p=0\), and \(p=k\) are handled correctly. In the remaining cases, the swap inequalities have the correct marginal harmonic terms.
Every singleton with \(b_i>a\) must be selected. Its contribution to the utilitarian optimum is correctly represented by \(d\), giving optimum \(ka+d\). The lower-bound algebra is correct, and the comparison after adding \(d\) uses a coefficient at most \(k\), as required.
The attaining masses are nonnegative, rational, and sum to \(1\). The score-increment calculation establishes global optimality: below \(p\), committees contain zero-mass singleton candidates that can be replaced profitably; from \(p\) onward, the best scores have a zero first increment and negative subsequent increments. The attained ratio and actual support size are correct. The construction also covers \(p=0\) and \(k=1\).
Rational attainment proves that equality \(q=\Gamma_g\) is included. The exact-minimum characterization rules out every smaller threshold and supplies a witness for every larger one.
The conclusions for nonpositive thresholds, thresholds at least \(1\), and the special cases \(k=1\), \(k=m\), and singleton-only nonempty types are all correct. The representation threshold \(1/2\) is impossible for every finite \(k\), since the proved lower bound is strictly larger.
No additional clarification is needed to verify the mathematical conclusions. The established result is an exact prescribed-family guarantee and attainment characterization, with explicit enumeration algorithms; general complexity classification remains unclaimed.
⟨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.