← back to the atlas

d4-conf-wine-2017-0027 (d4-conf-wine-2017-0027)

Answer: —

The anchor (named result in the paper)

Theorem 3.3 — class: other

The continuous mirror question, as graded

Given rational \(B,p,\varepsilon>0\) and a finite-support rational distribution \(\mu\) over types \(t=(\alpha_t,\delta_t)\), with rational \(0<\alpha_t,\delta_t<1\) and common share success probability \(p\), compute a finite-support rational payout sequence \(x_i\ge0\), \(\sum_i x_i\le B\), whose welfare \(p\sum_t\mu_t\sum_{i\ge0}\delta_t^i x_i^{\alpha_t}\) is within \(\varepsilon\) of the supremum over feasible payout sequences.

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

A society is given by its support: the list of the \(\tau\ge1\) types with positive mass, each with its mass as a binary rational. Here \(\tau\) is the support size, not the number of possible types. Types are \(t=(\alpha_t,\delta_t)\), with rational \(0<\alpha_t,\delta_t<1\), and masses satisfy \(\sum_t\mu_t=1\).
Inputs also include binary rationals \(B,\varepsilon>0\) and a common share success probability \(0<p\le1\). Let \(L\) be the total input bit length; there is no candidate-count parameter \(m\).
A fixed payout rule assigns the same amount \(x_i\) to a share whenever a successful share occurs \(i\) submissions later, including its own success at \(i=0\). Successes are independent with probability \(p\); payouts are amounts, and the rule cannot depend on type or history.
Feasible rules are real sequences \(x=(x_i)_{i\ge0}\) with \(x_i\ge0\) and \(\sum_{i\ge0}x_i\le B\). Define \(W(x)=p\sum_t\mu_t\sum_{i\ge0}\delta_t^i x_i^{\alpha_t}\), with \(0^{\alpha_t}=0\), and \(W^*=\sup_{x\text{ feasible}}W(x)\).
The computational problem is to output a feasible finite-support rational rule satisfying \(W(x)\ge W^*-\varepsilon\), encoded as a list of nonzero entries with binary indices and binary rational amounts; all omitted entries are zero.

Is this additive approximation problem solvable in time polynomial in \(\tau\) and \(L\), or is it NP-hard?

For the original homogeneous model, an optimal geometric fixed payout rule is steady-state optimal among pure pools; this is an optimality characterization, not a bit-complexity bound. [Source](https://arxiv.org/pdf/1703.03846)
No result settling the stated heterogeneous, explicitly encoded approximation problem was located.

Modeling choices made when packaging the task

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

1. Status and additional progress

The stated problem is not solvable in polynomial time, because some inputs require exponentially many explicitly listed payouts. This does not, by itself, establish NP-hardness.

In addition to reproving that obstruction, I establish the following upper bound:

Proven upper bound. Let
$$ > d=\min_t(1-\delta_t). > $$
There is a feasible finite-support rational approximation computable in
$$ > N\,\operatorname{poly}(\tau,L+\log N) > $$
bit operations, where
$$ > N=O\!\left(\frac{L}{d}\right). > $$
Each output amount has $O(L+\log N)$ bits. Consequently, the problem has a worst-case $2^{O(L)}$-time algorithm. On any subclass satisfying $d\ge 1/q(L)$ for a fixed polynomial $q$, it is polynomial-time solvable.

Thus the worst-case exponential lower and upper bounds are established. NP-hardness remains unresolved.

For the algorithmic upper bound, I use the intended finite-input convention that the supplied probability $p$ is also a binary rational. The lower bound uses $p=1$.

2. Exponential output is necessary

Consider one type with mass $1$, exponent $\alpha=\tfrac12$, discount $\delta=q\in(0,1)$, and $p=1$. Then
$$ W(x)=\sum_{i\ge0}q^i\sqrt{x_i}. $$

Cauchy–Schwarz applied to finite partial sums, followed by passage to the limit, gives
$$ W(x)\le \left(\sum_{i\ge0}q^{2i}\right)^{1/2} \left(\sum_{i\ge0}x_i\right)^{1/2} \le \sqrt{\frac{B}{1-q^2}}. $$
The feasible rule
$$ x_i=B(1-q^2)q^{2i} $$
attains this bound. Therefore
$$ W^*=\sqrt{\frac{B}{1-q^2}}. $$

Suppose a rule has at most $k$ nonzero entries. Order its nonzero indices as
$$ i_0<i_1<\cdots<i_{r-1}, \qquad r\le k. $$
Since $i_j\ge j$,
$$ \sum_{j=0}^{r-1}q^{2i_j} \le \sum_{j=0}^{k-1}q^{2j}. $$
Another application of Cauchy–Schwarz yields
$$ W(x)\le \sqrt{\frac{B(1-q^{2k})}{1-q^2}}. $$
This bound is attained by the rational rule
$$ x_i= \frac{Bq^{2i}}{\sum_{j=0}^{k-1}q^{2j}} \quad(0\le i<k), $$
with all remaining entries zero. In particular, large binary indices cannot improve the support-constrained optimum.

Now choose, for each integer $n\ge1$,
$$ q_n=1-2^{-n}, \qquad B_n=1-q_n^2, \qquad \varepsilon=\frac14. $$
All these inputs are dyadic rationals, and their total encoding length satisfies $L_n=\Theta(n)$. The optimum is $W^*=1$, while every rule with at most $k$ nonzero entries satisfies
$$ W(x)\le\sqrt{1-q_n^{2k}}. $$
An acceptable output must therefore satisfy
$$ q_n^{2k}\le\frac7{16}, $$
and hence
$$ k\ge \frac{\log(16/7)}{2[-\log q_n]}. $$

For $0<s\le\tfrac12$,
$$ -\log(1-s) = \int_0^s\frac{du}{1-u} \le 2s. $$
Substituting $s=2^{-n}$ gives
$$ k\ge \frac{\log(16/7)}4\,2^n. $$

Thus every acceptable output on this family contains $2^{\Omega(L_n)}$ explicitly listed entries. Writing those entries already requires exponential time. This proves the unconditional failure of polynomial-time solvability for the prescribed encoding.

3. A uniformly controlled finite horizon

Define
$$ C=\max\{1,B\}, \qquad d=\min_t(1-\delta_t), \qquad U=\frac{C}{d}. $$
Feasibility implies $x_i\le B$. Since $0<\alpha_t<1$,
$$ B^{\alpha_t}\le C. $$
Using $p\le1$ and $\sum_t\mu_t=1$, we obtain
$$ W(x) \le p\sum_t\mu_t\frac{B^{\alpha_t}}{1-\delta_t} \le U. $$
In particular, $W^*$ is finite. If $\varepsilon\ge U$, the zero rule is acceptable. Henceforth assume $\varepsilon<U$.

Let $H$ be the least positive integer satisfying
$$ U2^{-H}\le\frac{\varepsilon}{8}, $$
and set
$$ R=\left\lceil\frac1d\right\rceil, \qquad N=HR. $$
These quantities are computable by rational arithmetic and comparisons with powers of two.

To bound the tail, observe that
$$ (1-d)^{-R} = \left(1+\frac{d}{1-d}\right)^R \ge 1+Rd \ge2, $$
where the first inequality follows from the binomial expansion. Consequently,
$$ (1-d)^N\le2^{-H}. $$

For every feasible rule,
$$ \begin{aligned} W(x)-p\sum_t\mu_t\sum_{i=0}^{N-1}\delta_t^i x_i^{\alpha_t} &\le p\sum_t\mu_t B^{\alpha_t} \frac{\delta_t^N}{1-\delta_t}\\ &\le U(1-d)^N\\ &\le\frac{\varepsilon}{8}. \end{aligned} $$

Define
$$ f_i(u)=p\sum_t\mu_t\delta_t^i u^{\alpha_t}, \qquad F(x)=\sum_{i=0}^{N-1}f_i(x_i). $$
Let $V_N$ denote the maximum of $F$ over nonnegative vectors with total payout at most $B$. This maximum exists because the feasible set is compact and $F$ is continuous.

Every $f_i$ is strictly increasing. Thus a maximizing vector uses the full budget:
$$ \sum_{i=0}^{N-1}x_i=B. $$
The uniform tail bound proves
$$ V_N\le W^*\le V_N+\frac{\varepsilon}{8}. $$

Under binary rational encoding,
$$ d\ge2^{-O(L)}, \qquad U\le2^{O(L)}, \qquad \varepsilon\ge2^{-O(L)}. $$
Therefore
$$ H=O(L), \qquad N=O\!\left(\frac{L}{d}\right), \qquad \log N=O(L). $$

It remains to solve this finite problem with precision depending polynomially on the input bit length.

4. A positive floor and stable marginal equations

4.1. Enforcing a small positive floor

Set
$$ \gamma=\frac{\varepsilon}{8U}, \qquad a=\frac{\gamma B}{N}. $$
Then $0<\gamma<\tfrac18$ and $Na=\gamma B<B$.

Let $V_a$ be the maximum of $F$ on
$$ \mathcal K_a= \left\{ x\in[a,B]^N: \sum_{i=0}^{N-1}x_i=B \right\}. $$
This set is nonempty and compact.

Take a vector $v$ attaining $V_N$, and define
$$ y_i=(1-\gamma)v_i+a. $$
Then $y\in\mathcal K_a$. For every type and coordinate,
$$ y_i^{\alpha_t} \ge (1-\gamma)^{\alpha_t}v_i^{\alpha_t} \ge (1-\gamma)v_i^{\alpha_t}. $$
The last inequality holds because $0<1-\gamma<1$ and $\alpha_t<1$. Hence
$$ V_a\ge(1-\gamma)V_N \ge V_N-\frac{\varepsilon}{8}, $$
using $V_N\le U$.

4.2. Adding a small quadratic penalty

Set
$$ \kappa=\frac{\varepsilon}{8B^2}, \qquad G(x)=F(x)-\frac{\kappa}{2}\sum_{i=0}^{N-1}x_i^2. $$
Let $z^*$ maximize $G$ on $\mathcal K_a$.

If $v^*$ maximizes $F$ on $\mathcal K_a$, then
$$ G(z^*)\ge G(v^*). $$
Every vector in $\mathcal K_a$ satisfies
$$ \sum_i x_i^2\le\left(\sum_i x_i\right)^2=B^2. $$
It follows that
$$ F(z^*)\ge V_a-\frac{\kappa B^2}{2} = V_a-\frac{\varepsilon}{16}. $$

The penalty makes the marginal equations uniformly stable. Define
$$ D_i(u)=f_i'(u)-\kappa u. $$
For $u>0$,
$$ f_i'(u) = p\sum_t\mu_t\alpha_t\delta_t^i u^{\alpha_t-1}, $$
and
$$ f_i''(u) = p\sum_t\mu_t\alpha_t(\alpha_t-1)\delta_t^i u^{\alpha_t-2}<0. $$
Therefore
$$ D_i'(u)\le-\kappa. $$

Also, for $u\in[a,B]$,
$$ 0<f_i'(u)\le\max\{1,a^{-1}\}<M, \qquad M=1+a^{-1}. $$
Indeed, $u^{\alpha_t-1}\le1$ when $a\ge1$, and $u^{\alpha_t-1}\le a^{-1}$ when $a<1$.

4.3. Reduction to one scalar multiplier

For a real number $\lambda$, let $z_i(\lambda)$ be the unique maximizer on $[a,B]$ of
$$ f_i(u)-\frac{\kappa}{2}u^2-\lambda u. $$
Equivalently,
$$ z_i(\lambda)= \begin{cases} a,&D_i(a)\le\lambda,\\ B,&D_i(B)\ge\lambda,\\ \text{the unique }u\in(a,B)\text{ with }D_i(u)=\lambda, & D_i(B)<\lambda<D_i(a). \end{cases} $$

These functions are nonincreasing and satisfy
$$ |z_i(\lambda)-z_i(\lambda')| \le\frac{|\lambda-\lambda'|}{\kappa}. $$
Here is a proof including the endpoint cases. Suppose $\lambda<\lambda'$ and write $z=z_i(\lambda)$, $z'=z_i(\lambda')$. Adding the two maximizing inequalities gives
$$ (\lambda'-\lambda)(z-z')\ge0, $$
so $z\ge z'$. If $z>z'$, the first-order inequalities at the two constrained maximizers give
$$ D_i(z)\ge\lambda, \qquad D_i(z')\le\lambda'. $$
Consequently,
$$ \kappa(z-z') \le D_i(z')-D_i(z) \le\lambda'-\lambda. $$

Put
$$ S(\lambda)=\sum_{i=0}^{N-1}z_i(\lambda). $$
The preceding bound implies that $S$ is continuous. At
$$ \lambda_-=-\kappa B, \qquad \lambda_+=M, $$
we have
$$ S(\lambda_-)=NB, \qquad S(\lambda_+)=Na<B. $$
The first equality follows from $D_i(B)>-\kappa B$; the second follows from $D_i(a)<M$.

Since $N>1$, the intermediate value theorem supplies $\lambda^*\in[\lambda_-,\lambda_+]$ with
$$ S(\lambda^*)=B. $$
The vector $z(\lambda^*)$ maximizes $G$ on $\mathcal K_a$. To verify this directly, coordinate optimality gives, for every $v_i\in[a,B]$,
$$ \bigl(D_i(z_i(\lambda^*))-\lambda^*\bigr) \bigl(v_i-z_i(\lambda^*)\bigr)\le0. $$
Concavity supplies the supporting-line inequality. Summing it over coordinates, the multiplier contribution vanishes because both vectors have total payout $B$. Thus
$$ G(v)\le G(z(\lambda^*)). $$
We may therefore take $z^*=z(\lambda^*)$.

5. Certified rational bisection

Define the coordinate accuracy
$$ s=\frac{\varepsilon}{64NM}. $$

5.1. Computing a coordinate within error $s$

For rational $\lambda$, one can compute a rational $y_i\in[a,B]$ satisfying
$$ |y_i-z_i(\lambda)|\le s $$
by bisection on $[a,B]$.

At each midpoint $u$, evaluate $D_i(u)$ with absolute error at most
$$ \eta=\frac{\kappa s}{4}. $$
Such evaluations are justified in Section 6.

If the computed value exceeds $\lambda+\eta$, then the true value exceeds $\lambda$, so the maximizer lies to the right. If the computed value is below $\lambda-\eta$, the maximizer lies to the left.

Otherwise,
$$ |D_i(u)-\lambda|\le2\eta=\frac{\kappa s}{2}. $$
The bound $D_i'\le-\kappa$ then implies
$$ |u-z_i(\lambda)|\le\frac{s}{2}, $$
including when the maximizer is an endpoint. For example, if $z_i(\lambda)=a$, then
$$ \lambda-D_i(u) \ge D_i(a)-D_i(u) \ge\kappa(u-a). $$
The case $z_i(\lambda)=B$ is analogous.

If this residual stopping condition never occurs, stop once the enclosing interval has width at most $2s$ and return its midpoint. The number of iterations is
$$ O\!\left(1+\log\max\{1,B/s\}\right). $$

5.2. Computing the multiplier

Maintain a bracket $[\ell,r]$ containing $\lambda^*$, initially $[\lambda_-,\lambda_+]$.

At its midpoint $\lambda$, compute the rational coordinates $y_i$ above and their exact sum
$$ S_y=\sum_i y_i. $$
Since
$$ |S_y-S(\lambda)|\le Ns, $$
the following updates are certified:

If the bracket reaches width at most $\kappa s$, compute $y$ at its midpoint and accept it. Thus the number of outer iterations is at most
$$ O\!\left( 1+\log\max\left\{1,\frac{M+\kappa B}{\kappa s}\right\} \right). $$

5.3. Exact budget correction

Correct the accepted rational vector $y$ to a rational vector $x\in\mathcal K_a$.

If its sum exceeds $B$, decrease coordinates, preserving their lower bound $a$, until the excess is removed. There is enough removable mass because $Na<B$. If its sum is below $B$, increase coordinates, preserving the upper bound $B$, until the deficit is removed. The total available capacity is $NB-S_y\ge B-S_y$.

This can be done sequentially, using exact rational arithmetic, and satisfies
$$ \|x-y\|_1=|S_y-B|. $$

If acceptance occurred because $|S_y-B|\le Ns$, then
$$ |S(\lambda)-B|\le2Ns. $$
All coordinates of $z(\lambda)-z(\lambda^*)$ have the same sign, by monotonicity. Therefore
$$ \|z(\lambda)-z^*\|_1 = |S(\lambda)-B| \le2Ns. $$
Together with $\|y-z(\lambda)\|_1\le Ns$ and the budget correction, this gives
$$ \|x-z^*\|_1\le4Ns. $$

If acceptance occurred because the bracket width is at most $\kappa s$, then
$$ |\lambda-\lambda^*|\le\frac{\kappa s}{2}, $$
so
$$ \|y-z^*\|_1\le\frac32Ns. $$
The budget correction adds at most another $\tfrac32Ns$. Thus the same bound $\|x-z^*\|_1\le4Ns$ holds in both cases.

Since $f_i'$ is bounded by $M$ on $[a,B]$, integration of the derivative gives
$$ |F(x)-F(z^*)| \le M\|x-z^*\|_1 \le4NMs =\frac{\varepsilon}{16}. $$

Combining all losses,
$$ \begin{aligned} F(x) &\ge V_a-\frac{\varepsilon}{16}-\frac{\varepsilon}{16}\\ &\ge V_N-\frac{\varepsilon}{4}\\ &\ge W^*-\frac{3\varepsilon}{8}. \end{aligned} $$
Extending $x$ by zeros at indices $i\ge N$ therefore gives an acceptable rule. It is rational, has finite support, and uses exactly the budget $B$.

6. Bit complexity

The bisection procedure uses certified approximations to rational powers. The following details ensure that it does not assume a real-arithmetic oracle.

6.1. Evaluating rational powers

Let $r>0$ have binary encoding length at most $K$, let $\beta\in[-1,0]$ be rational with encoding length at most $K$, and let $Q\ge1$. A rational approximation to $r^\beta$ with absolute error at most $2^{-Q}$ can be computed in time polynomial in $K+Q$.

To justify this, write
$$ r=2^e v, \qquad 1\le v<2, \qquad |e|=O(K). $$
For
$$ w=\frac{v-1}{v+1}, $$
we have $0\le w<\tfrac13$ and
$$ \log v = 2\sum_{j=0}^{\infty}\frac{w^{2j+1}}{2j+1}. $$
After $m$ terms, the error is at most
$$ 2\sum_{j=m}^{\infty}|w|^{2j+1} \le\frac34\,9^{-m}. $$
The same series with $w=\tfrac13$ evaluates $\log2$. Hence $\log r=e\log2+\log v$ can be approximated to any prescribed binary precision with polynomially many rational operations and polynomial intermediate bit length.

Next use
$$ r^\beta=\exp(\beta\log r). $$
The exponent has magnitude $O(K)$. Its approximation needs only $Q+O(K+\log K)$ bits of absolute precision, because the derivative of the exponential on this range is bounded by $2^{O(K)}$.

To evaluate the exponential, divide its argument by a power of two until its magnitude is at most $1$. Approximate the resulting exponential by its Taylor series, then repeatedly square. The number of squarings is $O(\log(K+1))$, and the Taylor remainder decreases at least geometrically with the number of terms. Using $Q+O(K+\log K)$ bits of initial accuracy controls the final error: for positive $A,B$,
$$ |A^m-B^m| \le m\max\{A,B\}^{m-1}|A-B|. $$
Here $m=O(K+1)$ and the initial values are bounded by a constant. Exact rational evaluation of the finite series and subsequent squarings has polynomial bit complexity.

This argument applies even when the denominator of $\beta$ is exponentially large in its bit length.

6.2. Evaluating discounted coefficients

For $0<\delta<1$ and a binary integer $i$, the value $\delta^i$ can be approximated to absolute error $2^{-Q}$ in time polynomial in
$$ L+\log(i+1)+Q. $$
Use repeated squaring and binary exponentiation, rounding intermediate values to a sufficiently fine dyadic grid.

All factors remain in $[0,1]$. Squaring propagates an error $e$ to at most $2e$ plus the rounding error, while multiplication propagates at most the sum of its two input errors plus the rounding error. Consequently, choosing
$$ Q+O(\log(i+1)) $$
fractional bits controls the final absolute error. Only $O(\log(i+1))$ multiplications are needed.

6.3. Evaluating the marginals

At every coordinate-bisection point $u\in[a,B]$,
$$ u^{\alpha_t-1}\le M. $$
Approximate each $\delta_t^i$ and each $u^{\alpha_t-1}$ to absolute error at most
$$ \zeta= \min\left\{1,\frac{\eta}{4\tau(M+2)}\right\}. $$
The resulting error in each product is at most $(M+2)\zeta$. Since $p\mu_t\alpha_t\le1$, summing over types gives an error at most $\eta/4$, and hence at most $\eta$. The term $-\kappa u$ is rational and can be handled exactly.

Thus every derivative evaluation required by Section 5 has polynomial bit complexity in the input lengths and requested precision.

6.4. Sizes and total running time

The rational quantities
$$ a,\ \kappa,\ M,\ s,\ \lambda_-,\ \lambda_+ $$
have $O(L+\log N)$ bits. The logarithmic iteration bounds in Section 5 are also $O(L+\log N)$.

Coordinate outputs are midpoints obtained by at most $O(L+\log N)$ bisections of $[a,B]$. Their denominators therefore divide one common denominator whose bit length is $O(L+\log N)$. The exact budget correction preserves that denominator. Since every final amount lies in $[a,B]$, each amount has $O(L+\log N)$ bits.

Each outer iteration performs $N$ coordinate computations, each involving polynomially many arithmetic operations and power evaluations. The total running time is consequently
$$ N\,\operatorname{poly}(\tau,L+\log N), $$
and the explicit output length is
$$ O\bigl(N(L+\log N)\bigr). $$

Because $\log N=O(L)$ and $N\le2^{O(L)}$, this proves the claimed $2^{O(L)}$ worst-case upper bound.

If $d\ge1/q(L)$ for a fixed polynomial $q$, then
$$ N=O(Lq(L)), $$
and the same algorithm runs in polynomial time.

7. Remaining classification question

The following conclusions are proved:

These results provide no reduction establishing NP-hardness. Some instances have no polynomial-length valid output, so a hardness claim must specify how a polynomial-time reduction accesses potentially exponentially long oracle answers. Establishing or refuting NP-hardness under such a specified reduction remains open here.

⟨structured verdict parsed — rendered above⟩

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

Overall assessment

The mathematical arguments establish the claimed exponential output-size obstruction and the algorithmic upper bound. I found no false central step or substantive gap in either argument.

The answer is nevertheless partial relative to the requested complexity classification: it proves that polynomial-time solvability is impossible for the prescribed explicit output format, but it does not establish NP-hardness. The prover explicitly acknowledges this limitation. An output-length lower bound is not an NP-hardness reduction.

Step-by-step verification

1. Input convention

The upper bound assumes that $p$ is a binary rational included in the input length $L$. The task specifies a common probability $p$ without explicitly specifying its encoding.

This is the natural finite-input interpretation, and the prover states it explicitly. Under the requested verification standard, this is an acceptable clarification. The lower bound uses $p=1$ and does not depend on the ambiguity.

2. Homogeneous optimum and support-constrained bound

For $\alpha=\tfrac12$, $\delta=q$, and $p=1$, the Cauchy–Schwarz bound
$$ W(x)\le \sqrt{\frac{B}{1-q^2}} $$
is valid. Passing from finite partial sums to the infinite sum is justified because the summands are nonnegative and the bounds are uniform.

The proposed geometric rule is feasible: its entries are nonnegative and sum to $B$. Substitution attains the displayed bound, so the formula for $W^*$ is correct.

For a rule with at most $k$ nonzero entries, the ordered indices satisfy $i_j\ge j$. Consequently, the stated comparison of geometric sums and the second Cauchy–Schwarz application are valid:
$$ W(x)\le \sqrt{\frac{B(1-q^{2k})}{1-q^2}}. $$
For positive integer $k$, the displayed rational allocation on the first $k$ indices attains this bound. Thus the assertion that large binary indices cannot improve this support-constrained optimum is justified.

3. Exponential output-size obstruction

For the specified family,
$$ q_n=1-2^{-n}, \qquad B_n=1-q_n^2, $$
all parameters satisfy the task’s restrictions, and their total binary encoding length is $\Theta(n)$.

The optimum equals $1$. Requiring welfare at least $\tfrac34$ implies
$$ q_n^{2k}\le\frac7{16}. $$
Taking logarithms gives the stated lower bound on $k$, with the inequality direction correct.

The integral estimate
$$ -\log(1-s)\le2s \qquad \left(0<s\le\tfrac12\right) $$
is correct, including the endpoint relevant to $n=1$. Therefore
$$ k\ge\frac{\log(16/7)}4\,2^n. $$
Every acceptable output must contain exponentially many explicitly listed entries. This establishes an unconditional obstruction to polynomial-time output generation under the required encoding.

It does not establish NP-hardness, and the prover does not claim otherwise.

4. Uniform finite horizon

The bound $x_i\le B$ follows from feasibility, and
$$ B^{\alpha_t}\le\max\{1,B\} $$
holds for every permitted exponent. The resulting bound $W(x)\le U$ is valid.

The zero-rule case $\varepsilon\ge U$ is correctly handled.

For the remaining case, $d\in(0,1)$ and $R$ is a positive integer, so the binomial estimate used to establish
$$ (1-d)^N\le2^{-H} $$
has its hypotheses satisfied.

The tail estimate is uniform over all feasible rules and has the claimed constant $\varepsilon/8$. Compactness and continuity justify existence of the finite-dimensional maximum. Strict monotonicity justifies full budget use.

The comparison
$$ V_N\le W^*\le V_N+\frac{\varepsilon}{8} $$
follows from zero extension and the uniform truncation bound.

The binary rational size estimates imply $H=O(L)$, $N=O(L/d)$, and $\log N=O(L)$ as claimed.

5. Positive floor and quadratic penalty

The floor construction satisfies $Na=\gamma B<B$. The transformed maximizing vector has total budget $B$ and coordinates in $[a,B]$.

The exponent inequality used in the floor-loss estimate is valid for every $0<\alpha_t<1$. Thus the loss of at most $\varepsilon/8$ is justified.

The penalty comparison uses the valid inequality
$$ \sum_i x_i^2\le B^2. $$
Its resulting loss is exactly $\varepsilon/16$.

The derivative formulas are correct, and positivity of the weights and the restrictions on the exponents imply strict concavity. In particular,
$$ D_i'(u)\le-\kappa. $$
The upper bound on $f_i'$ over $[a,B]$ also holds in both cases $a<1$ and $a\ge1$.

6. Scalar multiplier characterization

Each coordinate objective is strictly concave on a compact interval, so its unique maximizer exists. The three-case characterization is correct.

The monotonicity argument follows from the maximizing inequalities. In the Lipschitz argument, when $z>z'$, the first maximizer cannot be the lower endpoint and the second cannot be the upper endpoint. The stated first-order inequalities therefore hold, including the remaining endpoint cases. The bound
$$ |z_i(\lambda)-z_i(\lambda')| \le\frac{|\lambda-\lambda'|}{\kappa} $$
is justified.

The endpoint values of $S$ are correct. The assertion $N>1$ follows from $\varepsilon<U$, which forces $H\ge4$. Continuity and the intermediate value theorem therefore provide the required multiplier.

The coordinate optimality inequalities and the concave supporting-line inequality establish global optimality on $\mathcal K_a$. The multiplier terms cancel because both vectors have total budget $B$.

7. Certified bisection and budget correction

The coordinate-bisection comparisons correctly account for evaluation error. The residual stopping condition and the slope bound give the stated coordinate accuracy, including clipped endpoint maximizers.

The outer comparisons correctly account for the aggregate coordinate error $Ns$, so they preserve a bracket containing the selected multiplier.

Exact budget correction is feasible in both directions. Its total change in the $\ell_1$ norm equals the budget discrepancy.

Both acceptance cases yield
$$ \|x-z^*\|_1\le4Ns. $$
For the residual acceptance case, monotonicity ensures that all coordinate differences between the two multiplier vectors have the same sign, justifying the equality between their $\ell_1$ distance and their total-mass discrepancy.

The derivative bound then gives a welfare loss of at most $\varepsilon/16$. Combining the three finite-dimensional losses and the tail loss gives
$$ F(x)\ge W^*-\frac{3\varepsilon}{8}, $$
which is stronger than the requested guarantee. Zero extension produces a feasible finite-support rational rule.

8. Bit complexity

The rational-power evaluation argument supplies an algorithm rather than assuming an exact real-arithmetic oracle.

The logarithm-series remainder constant is correct. Range reduction bounds the exponential argument by $O(K)$, and the stated additional precision controls error amplification. Exact rational evaluation of the finite series and subsequent squarings has polynomial intermediate bit length.

For discounted coefficients, repeated squaring with the stated additional precision controls error propagation in polynomial time in the binary index length.

The marginal product-error estimate is valid:
$$ \text{product error}\le(M+2)\zeta. $$
The chosen $\zeta$ makes the aggregate error no greater than the required tolerance.

The bisection endpoints share a common rational denominator, and the bounded number of midpoint operations enlarges its bit length by only $O(L+\log N)$. Budget correction preserves a suitable common denominator containing that of $B$. Consequently, the claimed bit bound per output amount is justified.

The total running time
$$ N\,\operatorname{poly}(\tau,L+\log N) $$
follows. Since $\tau$ is bounded by the explicit input length and $N\le2^{O(L)}$, the worst-case upper bound is valid. The polynomial-time result under a fixed inverse-polynomial lower bound on $d$ is also valid.

Issue and minimum required follow-up

Major task-completion issue — Sections 1 and 7: The NP-hardness classification remains unanswered. This is an acknowledged limitation, not a mathematical error in the established bounds.

To complete that part of the task, the prover must specify the reduction notion and how it handles potentially exponential oracle outputs, then supply the corresponding hardness argument or another resolution of the hardness question. No repair to the output-size lower bound or the upper-bound algorithm is required.

⟨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.