← back to the atlas

d4-conf-atal-2010-0264 (d4-conf-atal-2010-0264)

Answer: Polynomial-time solvable: weighted isotonic regression computes an exact optimal rational design with quota \(q=\tfrac12\).

The anchor (named result in the paper)

Corollary 12 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateExactEnum is an exact, anytime algorithm that runs in exponential time for (f, g, Gcwvg, Lweights)-PVGD, for any choice of power index function f that is computable within exponential time. 6.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given rational type masses \mu_t>0 summing to \(1\), rational target densities \pi_t\ge 0 with \sum_t\mu_t\pi_t=1, and rational \varepsilon>0, find rational non-increasing type weights w_1\ge\cdots\ge w_\tau\ge0 normalized by \sum_t\mu_tw_t=1 and a quota q\in(0,1] whose objective is within \varepsilon of its infimum. For each admissible replication size N, form a finite game with N\mu_t members of type t, each of weight w_t/N, and quota q; if \beta_{t,N}(w,q) is one such member’s normalized Banzhaf index, minimize \limsup_{N\to\infty,\;N\mu_t\in\mathbb Z\;\forall t}\sum_t\mu_t(N\beta_{t,N}(w,q)-\pi_t)^2.

Packaged proof task (what the prover saw — nothing else)

A society is given by its support: an ordered list of \(\tau\ge1\) types with positive binary-rational masses \(\mu_t\) summing to \(1\). Here \(\tau\) is the support size, not the number of possible types; the type order is fixed input.
The remaining input consists of binary-rational target densities \(\pi_t\ge0\) satisfying \(\sum_t\mu_t\pi_t=1\), and binary-rational \(\varepsilon>0\). Let \(L\) be the total input bit length; voting has two alternatives, so \(m=2\) is fixed.
A feasible design consists of rational weights \(w_1\ge\cdots\ge w_\tau\ge0\) with \(\sum_t\mu_tw_t=1\), and a rational quota \(q\in(0,1]\).
For every positive integer \(N\) satisfying \(N\mu_t\in\mathbb Z\) for all types, the replicated game has \(N\mu_t\) members of type \(t\), each of weight \(w_t/N\). A coalition wins exactly when its total weight is at least \(q\), including equality.
Let \(\beta_{t,N}(w,q)\) be the normalized Banzhaf index of any one member of type \(t\). Define \(F(w,q)=\limsup_{N\to\infty,\;N\mu_t\in\mathbb Z\;\forall t}\sum_{t=1}^{\tau}\mu_t\bigl(N\beta_{t,N}(w,q)-\pi_t\bigr)^2\); the design is held fixed throughout this limit.
The computational problem is to find a feasible rational design with \(F(w,q)\le\inf_{(u,r)\text{ feasible}}F(u,r)+\varepsilon\).

Is this problem solvable in time polynomial in \(\tau\) and \(L\), with \(m=2\) fixed and \(\varepsilon\) encoded in binary, or is it NP-hard?

Discrete canonical weighted voting game design with squared error has an exact anytime algorithm running in exponential time in the number of agents, for every exponential-time computable power index, including normalized Banzhaf ([source](https://www.pakvla.nl/bart/votingaamas.pdf)).
For growing electorates with finitely many positive integer weights, half quota, and gcd \(1\) among weights occurring infinitely often, Banzhaf power ratios converge to weight ratios ([source](https://www.lse.ac.uk/cpnss/assets/documents/voting-power-and-procedures/publications/2004/lindner.pdf)). No result settling the specified replication-limit optimization was located.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Exact polynomial-time solvability

The problem is polynomial-time solvable. An exact optimal rational design is obtained by weighted isotonic regression of the target densities in the given type order, with quota \(q=\tfrac12\). Thus the running time has no dependence on \(1/\varepsilon\).

1. A lower bound valid for every feasible design

Define
\[ \mathcal C=\left\{x\in\mathbb R^\tau:x_1\ge\cdots\ge x_\tau\ge0,\ \sum_{t=1}^{\tau}\mu_tx_t=1\right\}, \qquad G(x)=\sum_{t=1}^{\tau}\mu_t(x_t-\pi_t)^2. \]

First, consider any finite replicated game. Let \(f(S)\) denote the indicator that coalition \(S\) wins, and let \(\alpha_i\) denote voter \(i\)'s absolute Banzhaf index: the probability that \(i\) is pivotal when all other voters join independently with probability \(\tfrac12\).

For distinct voters \(i,j\), let \(R\) be a uniformly random coalition excluding both. Conditioning on whether the other voter joins gives
\[ \alpha_i=\frac12\mathbb E\!\left[f(R\cup\{i\})-f(R)+f(R\cup\{i,j\})-f(R\cup\{j\})\right]. \]
Subtracting the corresponding expression for \(\alpha_j\) yields
\[ \alpha_i-\alpha_j=\mathbb E\!\left[f(R\cup\{i\})-f(R\cup\{j\})\right]. \]
If \(i\)'s weight is at least \(j\)'s, then \(f(R\cup\{i\})\ge f(R\cup\{j\})\) for every \(R\). Consequently, absolute and normalized Banzhaf indices respect the weight order.

The normalization denominator is positive: the empty coalition loses and the grand coalition wins, so a chain adding voters one at a time contains a pivotal addition.

Members of the same type have equal indices by symmetry. Therefore, for every admissible replication size \(N\), the vector
\[ x_{t,N}=N\beta_{t,N}(w,q) \]
satisfies
\[ x_{1,N}\ge\cdots\ge x_{\tau,N}\ge0, \qquad \sum_t\mu_tx_{t,N}=\sum_tN\mu_t\beta_{t,N}(w,q)=1. \]
Thus \(x_N\in\mathcal C\), and hence
\[ F(w,q)=\limsup_NG(x_N)\ge\min_{x\in\mathcal C}G(x). \tag{1} \]

This argument does not require convergence of Banzhaf indices at arbitrary quotas.

2. Every rational vector in the constraint set is attained at half quota

We use the following known theorem: for nested growing electorates with fixed positive integer voter weights taking finitely many values, if the gcd of the weight values occurring infinitely often is \(1\), then at half quota the normalized Banzhaf ratio of any two fixed voters converges to their weight ratio. The convention is that equality with the quota wins. This is [Lindner–Machover, Theorem 3.6](https://www.lse.ac.uk/cpnss/assets/documents/voting-power-and-procedures/publications/2004/lindner.pdf).

Let \(w\in\mathcal C\) be rational. We check its applicability:

Since \(w_1>0\), the theorem therefore gives, for positive-weight types,
\[ \frac{\beta_{t,N}(w,\tfrac12)}{\beta_{1,N}(w,\tfrac12)} \longrightarrow\frac{w_t}{w_1}. \]
For zero-weight types both the index and the corresponding weight ratio are zero. The denominator is positive for every \(N\), because a maximum-weight voter has positive power whenever any voter does.

Set \(r_{t,N}=\beta_{t,N}/\beta_{1,N}\). Normalization gives
\[ N\beta_{1,N}=\frac{1}{\sum_t\mu_tr_{t,N}} \longrightarrow \frac{1}{\sum_t\mu_tw_t/w_1}=w_1. \]
Consequently,
\[ N\beta_{t,N}(w,\tfrac12)\longrightarrow w_t \qquad\text{for every type }t. \]
Since the sum defining the objective has finitely many terms, this proves
\[ F(w,\tfrac12)=G(w) \qquad\text{for every rational }w\in\mathcal C. \tag{2} \]

3. Computing the optimal vector exactly

Here is an explicit weighted pool-adjacent-violators algorithm.

Start with consecutive singleton blocks. For each block \(B\), maintain its mass and target sum,
\[ A_B=\sum_{t\in B}\mu_t, \qquad T_B=\sum_{t\in B}\mu_t\pi_t, \]
and its mean \(a_B=T_B/A_B\).

Process types from left to right using a stack of blocks. Whenever the last two blocks \(I,J\) violate decreasing order, meaning \(a_I<a_J\), merge them and add their masses and target sums. Repeat until the violation disappears. At termination, set \(w_t=a_B\) for every \(t\in B\).

All means are rational and nonnegative. The final block means are nonincreasing, and
\[ \sum_t\mu_tw_t=\sum_BA_Ba_B=\sum_B T_B=\sum_t\mu_t\pi_t=1. \]
Thus the output belongs to \(\mathcal C\).

For completeness, we prove optimality of this algorithm.

The block invariant

Every block produced by the algorithm has the following property: the weighted target mean of every nonempty prefix of that block is at most the mean of the entire block.

It holds for singletons. Suppose blocks \(I,J\) satisfying it are merged, with means \(a<b\), masses \(A,B\), and merged mean
\[ c=\frac{Aa+Bb}{A+B}. \]
A prefix contained in \(I\) has mean at most \(a<c\). A prefix extending into \(J\), whose portion inside \(J\) has mass \(h\) and mean \(d\), satisfies \(d\le b\) and \(h\le B\). Its mean is therefore at most \((Aa+hb)/(A+h)\). Moreover,
\[ c-\frac{Aa+hb}{A+h} =\frac{A(B-h)(b-a)}{(A+B)(A+h)}\ge0. \]
The invariant is preserved.

Optimality certificate

Define residuals and prefix sums by
\[ \rho_t=\mu_t(w_t-\pi_t), \qquad R_k=\sum_{t=1}^{k}\rho_t. \]
Every final block has residual sum zero, because its fitted value is its weighted target mean. The block invariant implies that residual sums of prefixes within a block are nonnegative. Hence
\[ R_k\ge0\quad\text{for all }k, \qquad R_\tau=0. \]

Because \(w\) is constant on each block,
\[ \sum_t\rho_tw_t=0. \]
For any \(x\in\mathcal C\), summation by parts gives
\[ \sum_t\rho_tx_t =\sum_{k=1}^{\tau-1}R_k(x_k-x_{k+1})+R_\tau x_\tau \ge0. \]
Expanding the squares now yields
\[ G(x)-G(w) =\sum_t\mu_t(x_t-w_t)^2 +2\sum_t\rho_t(x_t-w_t) \ge0. \]
Thus \(w\) minimizes \(G\) over \(\mathcal C\). Since all masses are positive, the squared term also proves uniqueness.

4. Bit complexity and the optimal design

There are \(\tau\) block insertions and at most \(\tau-1\) merges, so the stack algorithm uses \(O(\tau)\) exact rational operations and comparisons.

All block quantities are sums of input masses or products \(\mu_t\pi_t\). A common denominator for each such sum can be chosen as a product of input denominators, whose binary length is \(O(L)\). Numerators also have polynomial length; indeed, the nonnegative block masses and target sums are at most \(1\). Block means and comparison cross-products therefore have polynomial bit length. Exact integer arithmetic implements the algorithm in time polynomial in \(\tau\) and \(L\), and the output has polynomial encoding length.

Return this rational vector \(w\) and \(q=\tfrac12\). Combining (1), optimality of \(w\), and (2), we obtain
\[ \inf_{(u,r)\text{ feasible}}F(u,r) \ge\min_{x\in\mathcal C}G(x) =G(w) =F(w,\tfrac12). \]
Since the returned design is feasible, equality holds throughout. It attains the infimum exactly and therefore satisfies the requested guarantee for every input \(\varepsilon>0\).

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

The prover’s claim is proved. The argument establishes an exact optimal rational design and a polynomial-time algorithm for computing it. I found no major or minor mathematical issues requiring repair.

1. Finite-game lower bound

The conditioning formula for the absolute Banzhaf index is correct. Subtracting the corresponding formula for voter \(j\) cancels the terms involving neither voter and both voters, leaving exactly
\( \alpha_i-\alpha_j=\mathbb E[f(R\cup\{i\})-f(R\cup\{j\})]. \)
There is no missing factor.

If voter \(i\) has at least voter \(j\)’s weight, the coalition containing \(i\) has at least the weight of the corresponding coalition containing \(j\). The stated winning convention therefore gives the pointwise inequality used in the proof, including when coalition weight equals the quota.

The normalization denominator is positive for every feasible design and every admissible replication size: the empty coalition loses because \(q>0\), and the grand coalition wins because its total weight is \(1\) and \(q\le1\). A losing-to-winning transition along a chain of coalitions supplies a swing with positive probability. Dividing absolute indices by their common positive sum preserves their order.

Symmetry within types and normalization then correctly give
\( x_{1,N}\ge\cdots\ge x_{\tau,N}\ge0 \)
and
\( \sum_t\mu_t x_{t,N}=1. \)
Thus every finite-replication vector belongs to \(\mathcal C\). Taking the limsup of the pointwise objective lower bound is valid and requires no convergence assumption at arbitrary quotas.

The minimum used in this bound is explicitly attained by the vector constructed and certified in Section 3.

Assessment: Correct.

2. Attainment at half quota

The cited theorem has been verified against the source. Theorem 3.6 applies to a nested half-quota chain with fixed voter weights taking finitely many positive integer values, provided the gcd of the values occurring infinitely often is \(1\). Its conclusion includes convergence of normalized Banzhaf ratios to weight ratios. The source’s definition of a weighted voting game uses the same equality-winning convention as the task. [Lindner–Machover, Definition 1.1 and Theorem 3.6](https://www.lse.ac.uk/cpnss/assets/documents/voting-power-and-procedures/publications/2004/lindner.pdf)

The applicability checks in the output are sufficient:

The use of fixed voters in the theorem is compatible with type-index notation: the nested chain can retain a representative of each positive-weight type, and symmetry identifies its index with the common index of that type.

The reference denominator \(\beta_{1,N}\) is positive. Section 1 establishes that some voter has positive power and that a maximum-weight voter has at least that power. Also, \(w_1>0\) follows from feasibility.

The normalization calculation is correct:
\( N\beta_{1,N}=1/\sum_t\mu_t r_{t,N}. \)
The denominator converges to
\( \sum_t\mu_t w_t/w_1=1/w_1>0, \)
so taking its reciprocal is justified. Multiplying by the convergent ratios gives
\( N\beta_{t,N}\to w_t \)
for every type, including zero-weight types.

Consequently, the finite sum of squared errors converges to \(G(w)\), proving equation (2). This is convergence for each fixed rational design, exactly as required; no uniform convergence or effective convergence rate is needed.

Assessment: Correct, with all cited-theorem hypotheses satisfied.

3. Isotonic algorithm and optimality certificate

The stack algorithm merges precisely the violations of decreasing order. Its final means are rational, nonnegative, and nonincreasing. Its mass-preservation identity correctly proves membership in \(\mathcal C\).

The prefix invariant is proved for every possible merge. A prefix either lies within the first block or contains that block and a nonempty prefix of the second. These cases exhaust the possibilities. The displayed difference
\( A(B-h)(b-a)/((A+B)(A+h)) \)
is algebraically correct and nonnegative under the stated ranges.

For a final block, the invariant gives nonnegative prefix residual sums, while its full residual sum is zero. Thus the global prefix sums satisfy \(R_k\ge0\) and \(R_\tau=0\).

The identity \(\sum_t\rho_tw_t=0\) follows from constancy of the fitted value on each block and the block’s zero residual sum. The summation-by-parts formula has the correct sign for decreasing \(x\). Therefore the linear term in the objective expansion is nonnegative.

The squared-error expansion is correct. Since all masses are positive, its squared term is strictly positive whenever \(x\ne w\), establishing uniqueness as claimed.

Equal adjacent means cause no problem: leaving them unmerged preserves both feasibility and the certificate. For \(\tau=1\), the summation-by-parts sum is empty and the same argument applies.

Assessment: Correct.

4. Bit complexity

There are linearly many insertions, merges, and comparisons. The arithmetic operands have polynomial encoding length:

Exact rational arithmetic therefore implements the algorithm in polynomial time. The output consists of polynomial-length rational weights and the constant rational quota \(q=\tfrac12\).

The potentially large replication denominator and integer-weight scaling are used only to justify the limit theorem. The algorithm does not enumerate replicated games or wait for convergence.

Assessment: Correct.

5. Resolution of the assigned task

The universal lower bound, certified minimizer, and half-quota attainment establish equality between the feasible-design infimum and the returned design’s objective. The design attains the infimum exactly, so it satisfies every permitted positive binary-encoded \(\varepsilon\).

The output resolves the specified replication-limit optimization in polynomial time. No additional clarification or mathematical repair is 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.