← back to the atlas

d4-conf-atal-2014-0233 (d4-conf-atal-2014-0233)

Answer: All limits exist, and the entire vector is exactly computable in polynomial time in \(m,\tau,L\).

The anchor (named result in the paper)

Theorem 3 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe Shapley value can be computed in poly- nomial time for any reliability extension of a Max-Game.

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

The continuous mirror question, as graded

Given a finite type set \(T\), rational type shares \(\mu_t>0\) summing to \(1\), qualities \(w_t>0\), and reliabilities \(r_t\in(0,1)\), form for each scale \(M\) a random population with independent counts \(N_t\sim\operatorname{Poisson}(M\mu_t)\). Conditional on those counts, use the paper’s reliability-extension Max-Game and its ordinary finite Shapley values \(\phi_i\). For each type \(t\), compute the high-multiplicity limit \(\lim_{M\to\infty}\mathbb{E}[\sum_{i:\,\mathrm{type}(i)=t}\phi_i]\), and determine whether these limits admit an exact polynomial-time algorithm in \(|T|\) and the input bit length.

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

A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive binary rational masses \(\mu_t\), where \(\sum_{t\in T}\mu_t=1\); \(\tau\) counts listed types, not possible types. Each type has binary rational quality \(w_t>0\) and reliability \(r_t\in(0,1)\). Let \(m\) be the number of distinct qualities and \(L\) the total input bit length.
For each real scale \(M>0\), draw independent counts \(N_t\sim\operatorname{Poisson}(M\mu_t)\), creating a finite set \(N\) of distinct agents with type map \(\theta:N\to T\).
Conditional on these counts, each agent \(i\) survives independently with probability \(r_{\theta(i)}\). The coalition value is \(v^r(S)=\mathbb{E}[\max(\{w_{\theta(i)}:i\in S\text{ survives}\}\cup\{0\})]\).
Let \(\phi_i\) be the ordinary finite Shapley value of \((N,v^r)\), and define \(A_t(M)=\mathbb{E}_{(N_s)_{s\in T}}[\sum_{i:\theta(i)=t}\phi_i]\). Empty populations and absent types contribute zero; equal qualities are allowed.

Do all limits \(a_t=\lim_{M\to\infty}A_t(M)\) exist, and is computing the entire vector \((a_t)_{t\in T}\) exactly solvable in polynomial time in \(m,\tau,L\), or is this computation NP-hard?

For finite explicitly listed agents, Shapley values in reliability extensions of Max-Games are computable in polynomial time ([Bachrach, Savani and Shah, 2014](https://www.cs.toronto.edu/~nisarg/papers/MaxGames.pdf)).
No result settling this precise Poisson population limit was located in the literature search.

Modeling choices made when packaging the task

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

Result

All limits exist, and the entire vector is exactly computable in polynomial time in \(m,\tau,L\).

Write the distinct qualities as \(0=q_0<q_1<\cdots<q_m\). Define

\(\displaystyle \Delta_k=q_k-q_{k-1},\qquad T_k=\{s\in T:w_s\ge q_k\},\qquad x_t=\mu_t r_t,\qquad c_k=\sum_{s\in T_k}x_s.\)

For each type \(t\), let \(j(t)\) satisfy \(w_t=q_{j(t)}\). Every \(c_k\) is positive, because \(T_k\) is nonempty and every \(x_s\) is positive.

We will prove the exact formulas

\(\displaystyle A_t(M)=x_t\sum_{k=1}^{j(t)}\frac{\Delta_k}{c_k}\bigl(1-e^{-Mc_k}\bigr),\qquad a_t=x_t\sum_{k=1}^{j(t)}\frac{\Delta_k}{c_k}.\)

In particular, every \(a_t\) is rational.

1. Shapley values for a fixed population

Fix a finite population \(N\). Independently sample its agents’ survival indicators, and let \(B\subseteq N\) be the resulting survivor set. Define the deterministic game

\(\displaystyle g_B(S)=\max\bigl(\{w_{\theta(i)}:i\in S\cap B\}\cup\{0\}\bigr).\)

By the definition of the reliability extension, \(v^r(S)=\mathbb E_B[g_B(S)]\). The Shapley value is a finite linear combination of coalition values, so

\(\displaystyle \phi_i(v^r)=\mathbb E_B[\phi_i(g_B)].\)

For each quality threshold, put \(B_k=\{i\in B:w_{\theta(i)}\ge q_k\}\). The identity

\(\displaystyle g_B(S)=\sum_{k=1}^{m}\Delta_k\,\mathbf 1\{S\cap B_k\ne\varnothing\}\)

holds for every coalition: if its highest surviving quality is \(q_j\), precisely the first \(j\) indicators equal one, and their contributions telescope to \(q_j\). If there is no survivor, all indicators vanish.

Consider the threshold game \(h_k(S)=\mathbf 1\{S\cap B_k\ne\varnothing\}\). In a uniformly random permutation of all agents, an agent has marginal contribution one exactly when it belongs to \(B_k\) and appears before every other member of \(B_k\). Each member of a nonempty \(B_k\) has probability \(1/|B_k|\) of appearing first among its members. Therefore,

\(\displaystyle \phi_i(h_k)= \begin{cases} 1/|B_k|,&i\in B_k,\\ 0,&i\notin B_k. \end{cases}\)

When \(B_k\) is empty, the game is identically zero.

Let \(K_t\) denote the number of surviving type-\(t\) agents, and set \(K^{(k)}=\sum_{s\in T_k}K_s=|B_k|\). By Shapley linearity, the aggregate allocation to type \(t\) in \(g_B\) is

\(\displaystyle \sum_{i:\theta(i)=t}\phi_i(g_B) =\sum_{k=1}^{j(t)}\Delta_k \begin{cases} K_t/K^{(k)},&K^{(k)}>0,\\ 0,&K^{(k)}=0. \end{cases}\)

This also covers absent types and empty populations.

All these allocations are nonnegative. Their sum over types equals \(g_B(N)\), by telescoping marginal contributions along each permutation, and hence is at most \(q_m\). Thus all expectations used below are finite.

2. Averaging over the Poisson population

We now average over both population counts and survival indicators.

Conditional on \(N_t\), the count \(K_t\) is binomial with parameters \(N_t,r_t\). For \(0\le z\le1\), its probability generating function is

\(\displaystyle \mathbb E[z^{K_t}] =\mathbb E[(1-r_t+r_tz)^{N_t}] =\exp\bigl(M\mu_t r_t(z-1)\bigr). \)

The last equality follows by summing the Poisson probability series. Consequently, \(K_t\) is Poisson with mean \(Mx_t\). These surviving counts are independent across types, because the original counts and the survival experiments are independent across types.

It follows by multiplying generating functions that \(K^{(k)}\) is Poisson with mean \(Mc_k\).

Conditional on \(K^{(k)}=n\), the vector of eligible surviving counts has the multinomial distribution with probabilities \((x_s/c_k)_{s\in T_k}\). Indeed, for nonnegative integers \(h_s\) summing to \(n\), division of the joint Poisson probability by the probability of their sum gives

\(\displaystyle \Pr\bigl(K_s=h_s\text{ for all }s\in T_k\mid K^{(k)}=n\bigr) =\frac{n!}{\prod_{s\in T_k}h_s!} \prod_{s\in T_k}\left(\frac{x_s}{c_k}\right)^{h_s}. \)

Thus, for \(t\in T_k\) and \(n\ge1\),

\(\displaystyle \mathbb E\!\left[\frac{K_t}{K^{(k)}}\,\middle|\,K^{(k)}=n\right] =\frac{1}{n}\mathbb E[K_t\mid K^{(k)}=n] =\frac{x_t}{c_k}. \)

Taking the ratio to be zero when \(K^{(k)}=0\), we obtain

\(\displaystyle \mathbb E\!\left[\mathbf 1\{K^{(k)}>0\}\frac{K_t}{K^{(k)}}\right] =\frac{x_t}{c_k}\Pr(K^{(k)}>0) =\frac{x_t}{c_k}(1-e^{-Mc_k}). \)

Applying the fixed-population identity and then the law of total expectation proves

\(\displaystyle A_t(M)=x_t\sum_{k=1}^{j(t)} \frac{\Delta_k}{c_k}(1-e^{-Mc_k}). \)

3. Existence and value of every limit

There are finitely many summands, and every \(c_k\) is strictly positive. Hence each exponential tends to zero as \(M\) tends to infinity, proving

\(\displaystyle a_t=\lim_{M\to\infty}A_t(M) =x_t\sum_{k=1}^{j(t)}\frac{\Delta_k}{c_k}. \)

The formula also gives a quantitative convergence bound. Since \(c_k\ge c_m>0\),

\(\displaystyle 0\le a_t-A_t(M) =x_t\sum_{k=1}^{j(t)}\frac{\Delta_k}{c_k}e^{-Mc_k} \le a_t e^{-Mc_m}. \)

As a consistency check, the limits allocate exactly the maximum listed quality:

\(\displaystyle \sum_{t\in T}a_t =\sum_{k=1}^{m}\frac{\Delta_k}{c_k} \sum_{t\in T_k}x_t =\sum_{k=1}^{m}\Delta_k =q_m. \)

4. Exact polynomial-time computation

The formula requires sorting qualities, computing the tail sums \(c_k\), and computing the prefix sums \(\sum_{k=1}^{j}\Delta_k/c_k\). To establish polynomial bit complexity, we must also bound the sizes of these rational numbers.

Let \(D\) be the product of all denominators appearing in the input masses, reliabilities, and qualities. Since their binary encodings are included in the input, \(D\le 2^L\). Define integers

\(\displaystyle X_t=Dx_t,\qquad Q_k=Dq_k,\qquad d_k=Q_k-Q_{k-1},\qquad S_k=\sum_{t\in T_k}X_t.\)

These are integers: the denominator of \(\mu_t r_t\) divides the product of the two corresponding input denominators, which divides \(D\).

Furthermore, \(1\le S_k\le D\), because \(c_k>0\) and

\(\displaystyle c_k\le\sum_{t\in T}\mu_t r_t<\sum_{t\in T}\mu_t=1.\)

Now \(\Delta_k/c_k=d_k/S_k\). Compute integer pairs recursively by

\(\displaystyle P_0=1,\quad B_0=0,\qquad P_j=P_{j-1}S_j,\quad B_j=B_{j-1}S_j+d_jP_{j-1}. \)

Induction gives

\(\displaystyle \frac{B_j}{P_j}=\sum_{k=1}^{j}\frac{d_k}{S_k},\)

so the output for type \(t\) is the rational number

\(\displaystyle a_t=\frac{X_tB_{j(t)}}{DP_{j(t)}}.\)

These integers have polynomially bounded bit lengths. Indeed, \(P_j\le D^j\). Also, \(c_k\ge1/D\), so

\(\displaystyle \frac{B_j}{P_j} =\sum_{k=1}^{j}\frac{\Delta_k}{c_k} \le D\sum_{k=1}^{j}\Delta_k =Dq_j \le Dq_m. \)

Every input quality is at most \(2^L\). Consequently, \(B_j\le D^{j+1}2^L\). All intermediate integers and output numerators and denominators therefore have \(O((m+3)L)\) bits.

Sorting rational qualities uses polynomially many binary arithmetic operations. Grouping types by quality, forming tail sums, evaluating the recurrence, and producing all \(\tau\) fractions also use polynomially many operations on integers of the bounded sizes above. Fractions may be reduced using the polynomial-time Euclidean algorithm.

Thus the entire vector is exactly computable in polynomial time in \(m,\tau,L\), including its binary output representation.

⟨structured verdict parsed — rendered above⟩

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

The prover’s claim is correct. The argument establishes all the limits and gives an exact polynomial-time algorithm with polynomially bounded output size. No major or minor mathematical issues were found.

The ordering \(0=q_0<q_1<\cdots<q_m\) is valid because the support is nonempty and every quality is positive. Grouping equal qualities into one threshold handles ties correctly.

Every \(x_t=\mu_t r_t\) is positive. Each threshold set \(T_k\) contains at least one listed type, so \(c_k>0\). Thus all divisions by \(c_k\) used in the formulas are defined. The index \(j(t)\) exists uniquely for every listed type.

For a fixed finite population, sampling one survivor set \(B\) gives
\(v^r(S)=\mathbb E_B[g_B(S)]\) for every coalition \(S\). This coupling is valid: restricting the sampled survival indicators to \(S\) has exactly the survival distribution specified in the task.

The Shapley value is a finite linear combination of coalition values. Consequently,
\(\phi_i(v^r)=\mathbb E_B[\phi_i(g_B)]\)
follows directly, without any convergence or interchange issue.

The decomposition
\(g_B(S)=\sum_{k=1}^{m}\Delta_k\mathbf 1\{S\cap B_k\ne\varnothing\}\)
is correct. If the highest surviving quality in the coalition is \(q_j\), precisely the thresholds with \(k\le j\) contribute, and their increments sum to \(q_j\). A coalition with no survivors contributes zero.

In a nonempty threshold game, a member of \(B_k\) contributes one precisely when it is the first member of \(B_k\) in the permutation. Its probability of doing so is \(1/|B_k|\). Agents outside \(B_k\) have zero marginal contribution. Including nonsurviving agents in the permutation does not alter this reasoning.

Summing these values over type-\(t\) agents yields the stated ratio \(K_t/K^{(k)}\) for \(k\le j(t)\). When \(K^{(k)}=0\), the threshold game is zero, and the explicitly assigned zero contribution is correct. Absent types and empty populations are therefore covered.

Nonnegativity and the bound by \(q_m\) are also correct: the aggregate Shapley allocation sums to \(g_B(N)\), which lies between zero and \(q_m\). This establishes the integrability needed later.

The probability generating function computation is correct:
\(\mathbb E[z^{K_t}]=\exp(M\mu_t r_t(z-1))\).
It identifies \(K_t\) as Poisson with mean \(Mx_t\).

Independence across types follows from the independent population counts and independent survival experiments. Multiplying generating functions therefore correctly identifies \(K^{(k)}\) as Poisson with mean \(Mc_k\).

The conditional multinomial formula is correct. Dividing the joint Poisson probability by the probability of the total cancels the exponential factors and powers of \(M\), leaving precisely the displayed multinomial probability. Its parameters are positive and sum to one.

For \(n\ge1\), the conditional mean is
\(\mathbb E[K_t\mid K^{(k)}=n]=n x_t/c_k\).
Hence the conditional expected ratio is \(x_t/c_k\). Averaging over positive totals and using the specified zero convention gives
\(\frac{x_t}{c_k}(1-e^{-Mc_k})\).
The displayed indicator-times-ratio expression is well-defined under that explicit convention.

Applying the fixed-population allocation formula and the law of total expectation correctly yields
\(A_t(M)=x_t\sum_{k=1}^{j(t)}\frac{\Delta_k}{c_k}(1-e^{-Mc_k})\).

This expectation agrees with the task’s definition: survival is averaged inside the reliability game, and population counts are averaged outside it. The preceding linearity argument justifies combining those expectations.

There are finitely many summands, and every \(c_k>0\). Thus each exponential tends to zero, proving the asserted limit for every listed type.

The threshold sets are nested, so \(c_k\ge c_m>0\). All coefficients are positive, which verifies both inequalities in
\(0\le a_t-A_t(M)\le a_t e^{-Mc_m}\).

The consistency check \(\sum_{t\in T}a_t=q_m\) is correct: the finite sums can be interchanged, and the inner sum over \(T_k\) equals \(c_k\).

Taking \(D\) to be the product of all input denominator occurrences correctly makes both \(Dx_t\) and \(Dq_k\) integers. In particular, the denominator of the product \(\mu_t r_t\) divides the product of those two input denominators, which divides \(D\).

The bound \(D\le2^L\) follows from the total binary encoding length. Also,
\(0<c_k<1\), so \(S_k=Dc_k\) is a positive integer bounded by \(D\).

The recurrence for \(B_j,P_j\) correctly implements addition of \(d_j/S_j\), starting from zero. Consequently, the displayed output fraction equals the previously established limit.

The bounds \(P_j\le D^j\) and
\(B_j/P_j\le Dq_m\)
are valid. Together with \(q_m\le2^L\), they give the asserted polynomial bit bounds for the recurrence values and output fractions.

Sorting and grouping rational qualities, forming tail sums, evaluating the recurrence, and producing all type allocations require polynomially many integer operations. The established operand-size bounds make their bit complexity polynomial as well. Optional fraction reduction by the Euclidean algorithm preserves that conclusion.

The proof therefore resolves the precise support-based Poisson limit problem, including equal qualities, absent types, and empty realized populations. It does not rely on the cited finite-agent literature result or on an unstated theorem requiring additional hypotheses.

No repair or additional clarification 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.