False-Name Manipulations in Weighted Voting Games (d4-journals-jair-2011-0035)

Given a finite type set \(T\), rational masses \(\mu_t\) with \(\sum_t\mu_t=1\), rational weights \(w_t\), a quota rate \(q\), and a designated type \(t^\star\) with \(\mu_{t^\star}>0\), decide whether there exist rational \(0<\alpha\le\mu_{t^\star}\) and \(u,v>0\) with \(u+v=w_{t^\star}\) such that replacing mass \(\alpha\) of \(t^\star\) by mass \(\alpha\) of each of two labelled identity types of weights \(u\) and \(v\) makes their limiting total normalized Banzhaf power exceed \((\alpha/\mu_{t^\star})\) times the original limiting Banzhaf power of type \(t^\star\). The limit is taken over denominator-compatible \(N\)-player games with \(N\mu_t\) copies and quota \(Nq\), with the post-split finite measure of total mass \(1+\alpha\) normalized together with its quota.

A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational; \(\tau\) is the support size, not the number of possible types. Input comprises these masses \(\mu_t\), with \(\sum_t\mu_t=1\), binary rational weights \(w_t\ge0\), a binary rational quota rate \(0<q\le\sum_t\mu_tw_t\), and a designated supported type \(t^\star\). Let \(L\) be the total input bit length and \(m=2\) the fixed number of new identities; express running times in \(m,\tau,L\).
For any rational finite type measure \(\nu\), let \(G_N(\nu,q)\) have \(N\nu_t\) distinct players of weight \(w_t\) for each supported label \(t\), and quota \(Nq\); coalitions win when their weight meets or exceeds the quota. Take \(N\to\infty\) through all positive integers for which the counts and \(Nq\) are integral. Write \(B_A(\nu,q)=\lim_{N\to\infty}\sum_{i:\operatorname{type}(i)\in A}\beta_i(G_N(\nu,q))\), where \(\beta_i\) is the normalized Banzhaf index and \(A\) is a set of labels.
A split chooses rational \(\alpha,u,v\) with \(0<\alpha\le\mu_{t^\star}\), \(u,v>0\), and \(u+v=w_{t^\star}\). It reduces the mass of \(t^\star\) by \(\alpha\) and adds two fresh labels \(a,b\), each of mass \(\alpha\), with weights \(u,v\); all other masses and weights remain unchanged. Call the resulting measure \(\nu\), omitting zero masses. Its total mass is \(1+\alpha\); normalizing it means replacing \((\nu,q)\) by \((\nu/(1+\alpha),q/(1+\alpha))\), equivalently retaining the games just defined.
The decision problem asks whether such a split exists for which both relevant limits exist and \(B_{\{a,b\}}(\nu,q)>(\alpha/\mu_{t^\star})B_{\{t^\star\}}(\mu,q)\).

Is this continuous beneficial two-identity split problem in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?

The discrete decision problem for normalized Banzhaf power is NP-hard even when splitting is restricted to two equal positive integer weights; the hardness also survives allowing fractional splits. [Aziz, Bachrach, Elkind and Paterson](https://www.dcs.warwick.ac.uk/~msp/papers/false_name.pdf).
For growing games with finitely many positive integer weight values, Lindner and Machover establish asymptotic proportionality of Banzhaf power to weight at half-total-weight quota under a gcd condition. This concerns power limits, rather than the split-existence decision problem. [Lindner and Machover](https://research.vu.nl/ws/files/74105380/L). No result settling the decision problem defined here was located.

Result

The problem is in $\mathrm{P}$. More precisely, let
$$ W=\sum_t\mu_tw_t. $$
A beneficial split exists if and only if
$$ w_{t^\star}>0 \qquad\text{and}\qquad 2q\ne W. $$

When the answer is yes, two equal weights suffice. The freedom to choose an arbitrarily small positive rational split mass $\alpha$ is essential to the proof.

The decision algorithm uses $O((\tau+m)L^2)$ bit operations with elementary integer arithmetic, where $m=2$. It does not need to calculate any transcendental quantities.

1. The limiting Banzhaf formula

We first prove existence and identify the limits for every measure needed in the problem.

Let $\nu$ be a finite rational measure with positive supported masses, nonnegative rational weights, and
$$ W_\nu=\sum_t\nu_tw_t>0. $$
Its total mass need not equal one.

Suppose first that
$$ 0<q<W_\nu. $$
Define
$$ F_\nu(\theta) = \sum_t\nu_tw_t\frac{e^{\theta w_t}}{1+e^{\theta w_t}}. $$
This function is continuous, with limits $0$ and $W_\nu$ at negative and positive infinity, respectively. Moreover,
$$ F_\nu'(\theta) = \sum_{t:w_t>0} \nu_tw_t^2 \frac{e^{\theta w_t}}{(1+e^{\theta w_t})^2} >0. $$
Consequently, there is a unique real $\theta$ satisfying
$$ F_\nu(\theta)=q. $$
Since $F_\nu(0)=W_\nu/2$, this parameter is zero exactly at half-total-weight quota.

We will prove that, for every set of labels $A$,
$$ B_A(\nu,q) = \begin{cases} \displaystyle \frac{\sum_{t\in A}\nu_tw_t}{W_\nu}, & q=W_\nu/2,\\[10pt] \displaystyle \frac{\sum_{t\in A}\nu_t\tanh(\lambda w_t)} {\sum_t\nu_t\tanh(\lambda w_t)}, & q\ne W_\nu/2, \end{cases} $$
where
$$ \lambda=\frac{|\theta|}{2}>0 $$
in the second case. Unsupported labels contribute zero.

A lattice estimate

Because the positive weights are rational, there is a rational $h>0$ such that
$$ w_t=hk_t, \qquad k_t\in\mathbb Z_{>0}, \qquad \gcd\{k_t:w_t>0\}=1. $$

We need the following estimate. Fix probabilities $p_t\in(0,1)$ for the positive-weight labels. Let $S_N$ be the sum of independent Bernoulli variables, with $N\nu_t-d_t$ variables of weight $k_t$ for label $t$, where the nonnegative integers $d_t$ are fixed. Write
$$ a_N=\mathbb E S_N, \qquad V=\sum_{t:w_t>0}\nu_tk_t^2p_t(1-p_t)>0. $$
For integer $\ell_N$ satisfying $\ell_N-a_N=O(1)$,
$$ \Pr(S_N=\ell_N) = \frac{1+o(1)}{\sqrt{2\pi NV}}. $$
The estimate is uniform when the offsets remain in a fixed bounded interval.

Here is a proof, including the lattice condition. Let $\phi_N(x)$ be the characteristic function of $S_N-a_N$. Fourier inversion gives
$$ \Pr(S_N=\ell_N) = \frac1{2\pi} \int_{-\pi}^{\pi} e^{-ix(\ell_N-a_N)}\phi_N(x)\,dx. $$
For each label,
$$ \left|1-p_t+p_te^{ik_tx}\right|^2 = 1-4p_t(1-p_t)\sin^2(k_tx/2). $$
All these factors have modulus one simultaneously only when every $k_tx$ is an integer multiple of $2\pi$. The gcd assumption implies that, on $[-\pi,\pi]$, this occurs only at $x=0$.

It follows by compactness, and by $N\nu_t-d_t\ge N\nu_t/2$ for sufficiently large $N$, that outside any fixed neighborhood of zero,
$$ |\phi_N(x)|\le \rho^N $$
for some $\rho<1$. In a sufficiently small neighborhood of zero, the displayed modulus formula also gives
$$ |\phi_N(x)|\le e^{-cNx^2} $$
for some $c>0$. Finally, expanding the logarithms of the centered characteristic factors yields
$$ \log\phi_N(x) = -\frac12\bigl(NV+O(1)\bigr)x^2 + O(N|x|^3). $$
Thus, for each fixed $y$,
$$ \phi_N(y/\sqrt N)\longrightarrow e^{-Vy^2/2}. $$
After substituting $x=y/\sqrt N$ into Fourier inversion, the bounded-offset assumption makes the extra phase tend to one. The bound $e^{-cy^2}$ permits dominated convergence, while the part outside the small neighborhood contributes $o(N^{-1/2})$. Therefore,
$$ \sqrt N\,\Pr(S_N=\ell_N) \longrightarrow \frac1{2\pi}\int_{\mathbb R}e^{-Vy^2/2}\,dy = \frac1{\sqrt{2\pi V}}, $$
as claimed.

Applying exponential tilting

For a player of positive-weight label $t$, let $r_{N,t}$ be the probability that this player is pivotal when all other players independently join a coalition with probability $1/2$.

All players have the same factor relating pivotal probability to swing count. Hence the aggregate normalized Banzhaf index is exactly
$$ B_{A,N} = \frac{\sum_{t\in A}\nu_tr_{N,t}} {\sum_t\nu_tr_{N,t}}. $$
Zero-weight players have $r_{N,t}=0$.

Tilt the coalition distribution so that a player of label $s$ joins with probability
$$ p_s=\frac{e^{\theta w_s}}{1+e^{\theta w_s}}. $$
Set
$$ \sigma^2 = \sum_s\nu_sw_s^2p_s(1-p_s)>0, \qquad Z_N = \prod_s \left(\frac{1+e^{\theta w_s}}2\right)^{N\nu_s}. $$
For the coalition excluding one player of label $t$, let $S_{N,-t}$ denote its weight. At any attainable weight $s$,
$$ \Pr_{1/2}(S_{N,-t}=s) = Z_N\frac{2}{1+e^{\theta w_t}} e^{-\theta s} \Pr_\theta(S_{N,-t}=s). $$
This follows directly by comparing the probabilities of each coalition under the two independent-product distributions.

Under the tilted distribution,
$$ \mathbb E_\theta S_{N,-t}=Nq-w_tp_t. $$
Define
$$ C_N=\left\lceil\frac{Nq}{h}\right\rceil. $$
Because winning means meeting or exceeding the quota, the pivotal coalition weights are exactly
$$ h(C_N-j), \qquad j=1,\ldots,k_t. $$
Their distances from the tilted mean are bounded independently of $N$. Applying the lattice estimate in units of $h$ gives, uniformly over these finitely many values,
$$ \Pr_\theta(S_{N,-t}=h(C_N-j)) = \frac{h}{\sqrt{2\pi N\sigma^2}}(1+o(1)). $$
Consequently,
$$ r_{N,t} = K_N \frac{2}{1+e^{\theta w_t}} \sum_{j=1}^{k_t}e^{\theta hj} (1+o(1)), $$
where the positive factor
$$ K_N = Z_Ne^{-\theta hC_N} \frac{h}{\sqrt{2\pi N\sigma^2}} $$
is common to all labels. In particular, any dependence on the quota's position within the lattice lies in this common factor.

If $\theta=0$, the remaining factor is $k_t=w_t/h$. If $\theta\ne0$, the geometric sum gives
$$ \frac{2}{1+e^{\theta w_t}} \sum_{j=1}^{k_t}e^{\theta hj} = \frac{2e^{\theta h}}{e^{\theta h}-1} \tanh(\theta w_t/2). $$
This is a common positive multiple of $\tanh(|\theta|w_t/2)$: for negative $\theta$, both the prefactor and the hyperbolic tangent change sign.

Substitution into $B_{A,N}$ proves the asserted limiting formula. The argument holds along every admissible sequence of integers $N$, so it proves existence of the limits required in the question.

At half-total-weight quota this agrees with the proportionality result in [Lindner and Machover, Theorem 3.6](https://research.vu.nl/ws/files/74105380/L); the calculation above also supplies the off-half-quota formula needed here.

Total-weight quota

If $q=W_\nu$, a coalition wins exactly when it contains every positive-weight player. All positive-weight players therefore have equal normalized Banzhaf indices; zero-weight players have index zero.

Writing
$$ M_\nu=\sum_{t:w_t>0}\nu_t, $$
we obtain, exactly for every admissible $N$,
$$ B_{A,N} = \frac{\sum_{t\in A:w_t>0}\nu_t}{M_\nu}. $$
Thus the limit exists at this endpoint too.

2. Instances with no beneficial split

Write
$$ w=w_{t^\star}, \qquad \mu_\star=\mu_{t^\star}. $$

If $w=0$, no legal split exists, because $u,v>0$ would imply $u+v>0$.

Now suppose $w>0$ and $q=W/2$. Every legal split preserves total weight:
$$ \sum_t\nu_tw_t = W-\alpha w+\alpha u+\alpha v = W. $$
The half-quota formula therefore gives
$$ B_{\{a,b\}}(\nu,q) = \frac{\alpha(u+v)}W = \frac{\alpha w}W. $$
For the original society,
$$ \frac{\alpha}{\mu_\star} B_{\{t^\star\}}(\mu,q) = \frac{\alpha}{\mu_\star} \frac{\mu_\star w}W = \frac{\alpha w}W. $$
These quantities are equal for every legal split. Strict benefit is impossible.

3. Beneficial splits at every interior non-half quota

Assume
$$ w>0, \qquad 0<q<W, \qquad q\ne W/2. $$
Fix the rational equal-weight split
$$ u=v=w/2. $$
We show that sufficiently small positive rational $\alpha$ works.

For the continuity argument, allow real $\alpha\in[0,\mu_\star]$ and define
$$ F_\alpha(x) = F_\mu(x) + \alpha \left( w\frac{e^{xw/2}}{1+e^{xw/2}} - w\frac{e^{xw}}{1+e^{xw}} \right). $$
This is the tilted expected-weight function for the split measure. Its total weight remains $W$, so it is strictly increasing from $0$ to $W$ and has a unique root $\theta_\alpha$ of
$$ F_\alpha(\theta_\alpha)=q. $$

We have
$$ \theta_\alpha\longrightarrow\theta_0 \qquad\text{as }\alpha\downarrow0. $$
Indeed, for each $\varepsilon>0$,
$$ F_0(\theta_0-\varepsilon)<q<F_0(\theta_0+\varepsilon). $$
Continuity in $\alpha$ preserves both inequalities for sufficiently small $\alpha$, and strict monotonicity then places $\theta_\alpha$ between those two arguments.

Also, $F_\alpha(0)=W/2$ for every $\alpha$. Hence all $\theta_\alpha$ are nonzero and have the same sign. Put
$$ \lambda_\alpha=\frac{|\theta_\alpha|}{2}, \qquad H_\alpha = \sum_t\mu_t\tanh(\lambda_\alpha w_t) + \alpha \left( 2\tanh(\lambda_\alpha w/2) - \tanh(\lambda_\alpha w) \right). $$
These quantities are continuous at zero, with $\lambda_0>0$ and $H_0>0$.

For rational positive $\alpha$, the proven limit formula gives
$$ B_{\{a,b\}}(\nu_\alpha,q) = \frac{2\alpha\tanh(\lambda_\alpha w/2)}{H_\alpha}, $$
whereas
$$ \frac{\alpha}{\mu_\star} B_{\{t^\star\}}(\mu,q) = \alpha\frac{\tanh(\lambda_0w)}{H_0}. $$
After cancelling $\alpha>0$, benefit is equivalent to
$$ \frac{2\tanh(\lambda_\alpha w/2)}{H_\alpha} > \frac{\tanh(\lambda_0w)}{H_0}. $$

This inequality holds strictly at the continuous extension $\alpha=0$. To verify it, let
$$ r=\tanh(\lambda_0w/2)\in(0,1). $$
The double-angle identity gives
$$ \tanh(\lambda_0w)=\frac{2r}{1+r^2}, $$
so the difference between the two sides at zero is
$$ \frac{2r}{H_0} - \frac{2r}{(1+r^2)H_0} = \frac{2r^3}{(1+r^2)H_0} >0. $$
Continuity therefore supplies a $\delta>0$ for which the inequality holds whenever $0<\alpha<\delta$ and $\alpha\le\mu_\star$.

Choose an integer $k$ sufficiently large that
$$ \alpha=\mu_\star/k<\delta. $$
This is a legal rational split mass, and the split is beneficial.

The order of limits is respected: for each chosen rational $\alpha>0$, the population limit has already been proved. Taking $\alpha\downarrow0$ is used only to establish existence of such an $\alpha$.

4. Beneficial splits at total-weight quota

Assume $w>0$ and $q=W$. Let
$$ M=\sum_{t:w_t>0}\mu_t. $$
The original designated type has limiting power
$$ B_{\{t^\star\}}(\mu,q)=\frac{\mu_\star}{M}. $$
After any legal positive-weight split, the positive-weight mass is $M+\alpha$, and the two fresh labels have total mass $2\alpha$. Thus
$$ B_{\{a,b\}}(\nu,q)=\frac{2\alpha}{M+\alpha}. $$
Benefit is equivalent to
$$ \frac{2\alpha}{M+\alpha}>\frac{\alpha}{M}, $$
or, equivalently,
$$ \alpha<M. $$
Choose
$$ \alpha=\mu_\star/2, \qquad u=v=w/2. $$
Since $0<\mu_\star\le M$, this choice satisfies $\alpha<M$ and is beneficial.

5. Decision algorithm and complexity

The preceding cases prove the exact criterion. On a valid input, the algorithm is:

• Return no if $w_{t^\star}=0$.
• Compute $W=\sum_t\mu_tw_t$ exactly.
• Return yes if $2q\ne W$, and no otherwise.

For an explicit bit-complexity bound, take a common denominator equal to the product of the input denominators. Its bit length is $O(L)$; every denominator of a product $\mu_tw_t$ divides it. Computing the common denominator, the scaled summands, and the comparison uses $O(\tau)$ operations on $O(L)$-bit integers. Schoolbook multiplication and division therefore give
$$ O((\tau+m)L^2), \qquad m=2, $$
bit operations.

Only supported types are processed. Neither lattice scaling nor solving for $\theta$ is part of the decision algorithm.

The finite-game hardness in [Aziz, Bachrach, Elkind and Paterson, Theorem 11](https://www.dcs.warwick.ac.uk/~msp/papers/false_name.pdf) concerns a different decision problem. Here, the population limit and the ability to choose a sufficiently small positive split mass yield the polynomial-time criterion proved above.

⟨structured verdict parsed — rendered above⟩

The output resolves the assigned decision problem. The limiting formula, the beneficial-split criterion, and the claimed polynomial running time are justified. I found no major or minor issues requiring repair.

• Scope and admissible population sizes.

The input assumptions imply
$$ W=\sum_t\mu_tw_t\ge q>0. $$
Thus at least one supported type has positive weight. Rationality of the masses and quota ensures infinitely many admissible population sizes.

Every legal split preserves total weight:
$$ W_\nu=W-\alpha w_{t^\star}+\alpha(u+v)=W. $$
Consequently, the prover’s cases cover every valid input and every split relevant to the decision problem. The proof correctly allows the split measure to have total mass different from one.

• Existence and uniqueness of the tilting parameter.

For positive-weight types, the summands defining $F_\nu$ are continuous and have the stated limits. The derivative is strictly positive because at least one positive-weight type has positive mass. Hence, for $0<q<W_\nu$, there is exactly one finite parameter $\theta$ satisfying
$$ F_\nu(\theta)=q. $$

The identity $F_\nu(0)=W_\nu/2$ correctly characterizes the half-total-weight case. Zero-weight types contribute nothing to this function or its derivative.

• Lattice local estimate.

Rational positive weights admit the stated scaling $w_t=hk_t$ with integer weights of gcd one.

The Fourier argument checks the necessary lattice condition: simultaneous unit modulus of all characteristic factors requires
$$ k_tx\in2\pi\mathbb Z $$
for every positive-weight type. The gcd condition restricts this to $x=0$ on the integration interval.

Every positive-weight type has a number of Bernoulli variables growing linearly with $N$, even after fixed deletions. This justifies exponential decay away from zero. The local Gaussian bound and centered logarithmic expansion have the correct variance coefficient and error orders.

After rescaling, the bounded-offset phase converges uniformly to one, and the Gaussian bound supplies an integrable dominating function. The contribution outside the local neighborhood is negligible at the stated scale. The resulting estimate
$$ \Pr(S_N=\ell_N)=\frac{1+o(1)}{\sqrt{2\pi NV}} $$
is justified, including the bounded-offset uniformity used later.

• Normalized Banzhaf aggregation and exponential tilting.

Within a game, swing counts and pivotal probabilities differ by the same factor for every player. Summing over $N\nu_t$ players and cancelling $N$ gives the stated exact ratio
$$ B_{A,N}= \frac{\sum_{t\in A}\nu_tr_{N,t}} {\sum_t\nu_tr_{N,t}}. $$

Zero-weight players are correctly assigned zero pivotal probability.

The change-of-measure identity has the correct normalization. Removing one player of type $t$ removes precisely its factor from $Z_N$, giving
$$ \frac{2}{1+e^{\theta w_t}}. $$
The tilted mean $Nq-w_tp_t$ is also correct.

• Pivotal intervals and quota rounding.

For a player of weight $hk_t$, pivotality requires the other coalition’s weight to satisfy
$$ Nq-hk_t\le S_{N,-t}<Nq. $$
The lattice points in this interval are exactly the listed candidates
$$ h(C_N-j),\qquad j=1,\ldots,k_t. $$

This remains correct when $Nq/h$ is integral; the strict upper endpoint is handled correctly. Their distances from the tilted mean remain bounded. The local estimate therefore applies with the stated conversion between integer-unit variance and $\sigma^2$.

The quota-rounding dependence is entirely contained in the common factor $K_N$, so it cannot produce different limiting normalized powers along different admissible subsequences.

• Simplification to the limiting power formula.

At $\theta=0$, the type-dependent factor is $k_t=w_t/h$, yielding proportionality to weight.

For $\theta\ne0$, the geometric-sum identity is correct:
$$ \frac{2}{1+e^{\theta w_t}} \sum_{j=1}^{k_t}e^{\theta hj} = \frac{2e^{\theta h}}{e^{\theta h}-1} \tanh(\theta w_t/2). $$
When $\theta<0$, both factors on the right change sign, yielding the claimed common positive multiple of $\tanh(|\theta|w_t/2)$.

There are finitely many supported labels, so the typewise asymptotics can be substituted into the aggregate ratio. Its limiting denominator is positive. This establishes the claimed limits for every required label set.

• Total-weight quota.

When $q=W_\nu$, a coalition wins exactly when it contains every positive-weight player. Such players have equal pivotal probabilities, while zero-weight players have none. The exact formula
$$ B_{A,N}= \frac{\sum_{t\in A:w_t>0}\nu_t} {\sum_{t:w_t>0}\nu_t} $$
follows. The endpoint is therefore covered without using an infinite tilting parameter.

• Cases with no beneficial split.

If $w_{t^\star}=0$, positivity of both new weights makes a legal split impossible.

If $q=W/2$, total-weight preservation allows the half-quota formula to be applied before and after every legal split. Both sides of the benefit comparison equal
$$ \frac{\alpha w_{t^\star}}{W}. $$
The strict inequality is therefore impossible. This checks all legal weight allocations, rather than only equal splits.

• Interior non-half quotas.

For the equal split, $F_\alpha$ is correctly written, including the reduction in the original type’s mass. It remains strictly increasing with limits $0$ and $W$, including when that original mass becomes zero.

The bracketing argument correctly proves $\theta_\alpha\to\theta_0$. Since $F_\alpha(0)=W/2$, the parameters have a fixed nonzero sign. The subsequent quantities are continuous at zero, and $H_0>0$.

Cancelling $\alpha$ in the benefit inequality is valid only for $\alpha>0$, as stipulated. Evaluating the resulting expression at its continuous extension to zero does not assert a legal zero-mass split.

The double-angle calculation gives the correct strictly positive difference:
$$ \frac{2r^3}{(1+r^2)H_0}>0. $$
Continuity then supplies the required neighborhood of beneficial positive masses. Choosing $\alpha=\mu_\star/k$ ensures rationality and the mass constraint. The population limit is established for each fixed rational split before this existence argument is used.

• Beneficial split at the endpoint.

The positive-weight mass changes from $M$ to $M+\alpha$. The comparison
$$ \frac{2\alpha}{M+\alpha}>\frac{\alpha}{M} $$
is correctly equivalent to $\alpha<M$.

The proposed choice $\alpha=\mu_\star/2$ satisfies this strictly, including the case $\mu_\star=M$. Both equal new weights are positive.

• Decision algorithm, complexity, and references.

The preceding cases establish precisely
$$ \text{a beneficial split exists} \iff w_{t^\star}>0\ \text{and}\ 2q\ne W. $$

The algorithm requires only exact rational arithmetic. The product of the input denominators, counting their occurrences, has bit length $O(L)$ and is divisible by every denominator needed for $\mu_tw_t$. The scaled summands and their accumulated sum also have $O(L)$ bit length. The stated number of elementary integer operations therefore supports
$$ O((\tau+m)L^2),\qquad m=2. $$
Processing only supported types matches the required input representation.

No polynomial bound on the size of a witnessing $\alpha$ is needed for this decision algorithm: it decides the existence question through the proved criterion.

The external citations are contextual, not dependencies of the limiting-formula proof. The descriptions agree with [Lindner and Machover, Theorem 3.6](https://research.vu.nl/ws/files/74105380/L) and [Aziz, Bachrach, Elkind and Paterson, Theorem 11](https://www.dcs.warwick.ac.uk/~msp/papers/false_name.pdf). The finite-game hardness theorem does not establish hardness of the different population-limit problem.

No additional clarification is needed to make the argument verifiable.

⟨structured verdict parsed — rendered above⟩