← back to the atlas

d4-journals-geb-2024-0137 (d4-journals-geb-2024-0137)

Answer: —

The anchor (named result in the paper)

Proposition A.2 — class: algorithmic

The continuous mirror question, as graded

Given a finite value set \(V\), unknown rational masses \(\mu_v\) summing to one, and a known aggregate externality term \(a\), choose thresholds \(\tau_1,\ldots,\tau_K\). In each round, observe the exact accepting mass, equivalently \(F(\tau_k)=\sum_{v<\tau_k}\mu_v\). Minimize regret against the best threshold in \(V\) for per-capita revenue \(H(\tau)=\tau-F(\tau)(\tau-a)\).

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

A society is represented 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.
Let \(V=\{v_1<\cdots<v_m\}\subseteq[0,1]\cap\mathbb Q\) be nonempty and known, with \(\tau=m\), and let the known aggregate negative externality be \(a\in\mathbb Q_{\geq0}\). The fixed masses \(\mu_v>0\), satisfying \(\sum_{v\in V}\mu_v=1\), are hidden from the learner. A known bound \(L\) limits the total binary encoding length of the public rational data and the hidden society.
Define \(F_\mu(t)=\sum_{v<t}\mu_v\) and per-capita revenue \(H_\mu(t)=t-F_\mu(t)(t-a)\). Assume the piecewise linear interpolation of \((v_j,H_\mu(v_j))\) is concave; the admissible mass class \(\mathcal M(V,a,L)\) satisfying these conditions is promised nonempty.
In each of \(K\geq1\) rounds, a possibly randomized policy selects \(t_k\in V\) using only public data and earlier observations, earns \(H_\mu(t_k)\), and observes exactly \(F_\mu(t_k)\). Types equal to the threshold accept. The same society persists throughout.
For a policy \(\pi\), define \(R_K(\pi,\mu)=\mathbb E_\pi[\sum_{k=1}^K(\max_{t\in V}H_\mu(t)-H_\mu(t_k))]\), and \(R_K^*=\inf_\pi\sup_{\mu\in\mathcal M(V,a,L)}R_K(\pi,\mu)\). The public decision input is \((V,a,L,K,B)\), with \(B\in\mathbb Q_{\geq0}\).

Is deciding whether \(R_K^*\leq B\) solvable in polynomial time in \(m,\tau,L,K\), and the bit length of \(B\), or is it NP-hard, even when \(K\) is encoded in unary?

For finite buyers with independently redrawn types, known expected externalities, and concave threshold revenue, stochastic threshold learning has regret \(O(K^{3/4})\). [Source](https://arxiv.org/html/2003.08345v6).
No result settling the exact-mass minimax decision problem specified here was identified in the search.

Modeling choices made when packaging the task

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

Status

The general polynomial-time versus $\mathrm{NP}$-hardness question remains unresolved. The following results advance the analysis:

All arguments below are self-contained. For statements concerning encoding lengths, I use explicit binary numerator–denominator encodings, or explicit dyadic encodings. Compact encodings of exponentially large denominators are not included.

1. Coordinates and some resolved instances

Write
$$ \mu_j=\mu_{v_j},\qquad s_j=\sum_{i<j}\mu_i,\qquad h_j=H_\mu(v_j). $$
The acceptance convention gives
$$ s_1=0,\qquad h_j=v_j+(a-v_j)s_j=(1-s_j)v_j+s_ja. $$
In particular, $h_1=v_1$ is known without making a query. An observation of $s_j$ determines $h_j$ exactly.

For $m\geq 2$, positivity and normalization imply
$$ 0=s_1<s_2<\cdots<s_m<1. $$
The consecutive segment slopes of the interpolated revenue function are
$$ d_j=\frac{h_{j+1}-h_j}{v_{j+1}-v_j}. $$
The concavity promise implies
$$ d_1\geq d_2\geq\cdots\geq d_{m-1}. $$
Conversely, these inequalities imply concavity: slopes of secants are weighted averages of the segment slopes, so successive secants have the inequalities required for concavity.

If $m=1$, the minimax regret is zero.

There is also a slightly larger zero-regret parameter range than the one established in the notes.

Proposition. If $m\geq2$ and $a\geq v_{m-1}$, then $v_m$ is the unique maximizer for every admissible society.

Proof. First suppose $v_{m-1}\leq a<v_m$. For $j<m$, the convex-combination formula gives $h_j\leq a$. Meanwhile,
$$ h_m-a=(1-s_m)(v_m-a)=\mu_m(v_m-a)>0. $$
Thus $h_m>h_j$ for every $j<m$.

If $a\geq v_m$, direct subtraction gives
$$ h_{j+1}-h_j =(v_{j+1}-v_j)(1-s_j)+(a-v_{j+1})\mu_j>0. $$
The first term is strictly positive and the second is nonnegative. Hence revenues strictly increase. $\square$

Consequently, every promised instance in this parameter range has $R_K^*=0$.

2. A midpoint comparison lemma

Fix a society, and put
$$ M=\max_{1\leq j\leq m}h_j,\qquad g_j=M-h_j. $$
Let $h(x)$ denote the piecewise linear interpolation of the revenues, and define
$$ g(x)=M-h(x). $$
Then $g$ is convex and nonnegative on $[v_1,v_m]$.

Suppose an index interval $[l,r]$ contains a global maximizer and $l<r$. Let
$$ x=\frac{v_l+v_r}{2}, $$
and choose the consecutive indices $c,d$ satisfying
$$ d=c+1,\qquad v_c\leq x<v_d. $$
These indices exist because $v_l<x<v_r$.

Compare $h_c$ and $h_d$:

Each retained interval contains a global maximizer. Indeed, in the first case $d_c>0$, so all earlier slopes are positive and no index at most $c$ maximizes revenue. In the second case $d_c\leq0$, so all subsequent slopes are nonpositive and every index to the right of $c$ has revenue at most $h_c$.

Define the endpoint potential
$$ P(l,r)=g_l+g_r. $$

Lemma. If $[l',r']$ is the interval retained by this comparison, then
$$ g_c+g_d \leq 3\bigl(P(l,r)-P(l',r')\bigr). $$

Proof. Suppose first that $h_c<h_d$. Choose a global maximizing index $q\in[d,r]$, so $g_q=0$.

Convexity on $[v_l,v_q]$ gives
$$ g_c\leq \frac{v_q-v_c}{v_q-v_l}g_l \leq g_l $$
and
$$ g_d\leq \frac{v_q-v_d}{v_q-v_l}g_l. $$
Since $v_d>x$ and $v_q\leq v_r$,
$$ v_d-v_l\geq\frac{v_r-v_l}{2} \geq\frac{v_q-v_l}{2}. $$
Therefore $g_d\leq g_l/2$. It follows that
$$ g_c+g_d\leq\frac32g_l. $$
The retained interval is $[d,r]$, and hence
$$ P(l,r)-P(d,r)=g_l-g_d\geq\frac12g_l. $$
Combining the two inequalities proves the claim in this case.

Now suppose $h_c\geq h_d$. Choose a global maximizing index $q\in[l,c]$. Convexity on $[v_q,v_r]$ gives
$$ g_d\leq g_r,\qquad g_c\leq \frac{v_c-v_q}{v_r-v_q}g_r. $$
Because $v_c\leq x$ and $v_q\geq v_l$,
$$ v_r-v_c\geq\frac{v_r-v_l}{2} \geq\frac{v_r-v_q}{2}. $$
Thus $g_c\leq g_r/2$, and
$$ g_c+g_d\leq\frac32g_r \leq3(g_r-g_c) =3\bigl(P(l,r)-P(l,c)\bigr). $$
This proves the lemma. $\square$

The lemma uses coordinate midpoints, rather than index midpoints. Its estimates therefore hold for arbitrarily unequal threshold spacings.

3. A constant-regret policy

Consider the following deterministic policy.

Start with $[l,r]=[1,m]$ and cache the known value $h_1=v_1$. While $l<r$, form the consecutive midpoint pair $c,d$ from Section 2. Query whichever of their revenues are not cached, then retain the prescribed interval. Once the interval is a singleton, play its threshold in every remaining round.

If the horizon ends during the search, simply stop at the end of round $K$.

Theorem. There is a deterministic policy, implementable in time polynomial in $m,L,K$, such that for every admissible society,
$$ R_K(\pi,\mu)\leq\min\{K,m-1,6\}. $$
Consequently,
$$ R_K^*\leq\min\{K,m-1,6\}. $$

Proof. If $m=1$, or if $a\geq v_m$, use the known optimal threshold and incur zero regret. It remains to consider $m\geq2$ and $a<v_m$.

First imagine allowing the midpoint search to finish, regardless of the horizon. During one iteration, its actual query regret is at most $g_c+g_d$: cached revenues require no new action. The lemma therefore bounds that iteration’s query regret by three times the decrease in endpoint potential.

Every iteration strictly reduces the number of indices in the interval. The search ends at a maximizing index $q$, where
$$ P(q,q)=2g_q=0. $$
Summing the lemma over all iterations yields
$$ \text{total search regret} \leq3P(1,m) =3\bigl(2M-v_1-h_m\bigr). $$

If the horizon interrupts the search, its query regret is a prefix of this completed search’s regret. Since every regret term is nonnegative, the same bound applies to that prefix. After a completed search, subsequent regret is zero.

Under $a<v_m$, every revenue is a convex combination of two numbers in $[0,v_m]$. Thus
$$ 0\leq h_j\leq v_m\leq1. $$
Both initial endpoint losses are at most $1$, giving total regret at most $6$.

Caching ensures that at most $m-1$ thresholds are queried, since $h_1$ is initially known. Each query costs at most $1$, giving the additional bound $m-1$. The same per-round bound gives total regret at most $K$.

For implementation, there are at most $m-1$ interval updates. Midpoint locations and revenue comparisons use exact rational arithmetic. Observations have polynomial bit length in $L$: a common denominator for a cumulative mass is the product of its constituent mass denominators, whose logarithm is bounded by the encoding budget. Hence the policy has the stated polynomial running time. $\square$

A more informative bound, valid whenever $a<v_m$, is
$$ R_K(\pi,\mu) \leq3\bigl(2M-v_1-h_m\bigr) \leq3\bigl((v_m-v_1)+(v_m-a)\bigr), $$
because $M\leq v_m$ and $h_m>a$.

This settles every promised instance with
$$ B\geq\min\{K,m-1,6\} $$
as a yes-instance. It does not establish optimality of the policy.

4. Two societies certify failure of zero regret

For an admissible society, define
$$ A_\mu=\operatorname{argmax}_{1\leq j\leq m}h_j. $$

Lemma. The set $A_\mu$ is an index interval.

Proof. If $p<q$ are maximizing indices, concavity gives, for every $p<j<q$,
$$ h_j\geq \frac{v_q-v_j}{v_q-v_p}h_p+ \frac{v_j-v_p}{v_q-v_p}h_q =M. $$
Since $M$ is the maximum, equality holds. $\square$

Write
$$ A_\mu=[p_\mu,q_\mu]\cap\mathbb Z. $$
The encoding-bounded class is finite, so these endpoints have attained extrema over the class.

Theorem. The following statements are equivalent:

$$ h_{j+1}^{-}<h_j^{-}, \qquad h_{j+1}^{+}>h_j^{+}. $$

Proof. A common maximizing threshold gives zero regret, so statement 1 implies statement 2.

If there is no common maximizer, then
$$ \max_\mu p_\mu>\min_\mu q_\mu. $$
Choose societies attaining these two extrema. Their maximizing intervals are disjoint, proving statement 3.

Order such a pair so that $q_{\mu^-}<p_{\mu^+}$, and put $j=q_{\mu^-}$. Since $j$ is the rightmost maximizer of $\mu^-$,
$$ h_j^->h_{j+1}^-. $$
For $\mu^+$, if $h_j^+\geq h_{j+1}^+$, concavity would make every later revenue at most $h_j^+$, forcing a maximizer at or before $j$. That contradicts $p_{\mu^+}>j$. Thus statement 4 holds.

Opposite strict slopes at edge $j$ force all maximizers of $\mu^-$ to lie at or before $j$, and all maximizers of $\mu^+$ to lie after $j$. Thus statement 4 also implies statement 3.

Finally, suppose two societies have disjoint maximizing sets. Define their losses by
$$ \ell_{\mu i}=M_\mu-h_{\mu i} $$
and put
$$ \delta=\frac12\min_i \bigl(\ell_{\mu^- i}+\ell_{\mu^+ i}\bigr). $$
Every summand inside this minimum is strictly positive, since the two societies have no common maximizer. Therefore $\delta>0$.

For any policy, let $p_i$ be its first-round action probabilities. These probabilities depend only on public data. Nonnegativity of later regret gives
$$ \begin{aligned} \sup_\mu R_K(\pi,\mu) &\geq\frac{R_K(\pi,\mu^-)+R_K(\pi,\mu^+)}2\\ &\geq\frac12\sum_i p_i \bigl(\ell_{\mu^- i}+\ell_{\mu^+ i}\bigr)\\ &\geq\delta. \end{aligned} $$
Taking the infimum over policies proves statement 1. $\square$

Thus a certificate for nonzero regret consists of one adjacent edge and two admissible mass lists. Its direct length is at most $2L$.

5. Polynomial certificates even when the bound is binary

The preceding certificate bound alone would not prove ordinary $\mathrm{coNP}$ membership if $L$ were exponentially large relative to its binary representation. The following small-witness argument addresses this issue.

A strictly concave reference society

For $m\geq2$, define
$$ \mu_j^0=\frac{v_{j+1}-v_j}{2}\quad(j<m), \qquad \mu_m^0=1-\frac{v_m-v_1}{2}. $$
These masses are positive and sum to one. Their cumulative masses and revenues are
$$ s_j^0=\frac{v_j-v_1}{2}, \qquad h_j^0=v_j+\frac{(a-v_j)(v_j-v_1)}2. $$
The latter values come from the quadratic
$$ h^0(x)=-\frac{x^2}{2} +\left(1+\frac{a+v_1}{2}\right)x-\frac{av_1}{2}. $$
Its consecutive secant slopes satisfy
$$ d_j^0-d_{j+1}^0=\frac{v_{j+2}-v_j}{2}>0. $$
Hence every concavity inequality is strict.

Small witnesses for a prescribed strict slope

Let $n$ be the explicit encoding length of $V,a$, including the support description. Fix an edge $j$ and a sign $\sigma\in\{-1,1\}$. Suppose a positive normalized rational society satisfies concavity and
$$ G(\mu):=\sigma(h_{j+1}-h_j)>0. $$

A sufficiently small positive mixture with $\mu^0$ preserves $G>0$ and makes every concavity inequality strict. To justify preservation explicitly, for mixture weight $\eta$,
$$ G((1-\eta)\mu+\eta\mu^0) \geq G(\mu)-\eta\bigl(G(\mu)+|G(\mu^0)|\bigr)>0 $$
whenever $\eta$ is positive and sufficiently small.

Express concavity without division through the affine forms
$$ C_i(\mu)= (h_{i+1}-h_i)(v_{i+2}-v_{i+1}) -(h_{i+2}-h_{i+1})(v_{i+1}-v_i). $$
Consider the rational polytope in variables $\mu_1,\ldots,\mu_m,\delta$ defined by
$$ \sum_i\mu_i=1,\qquad 0\leq\delta\leq1, $$
$$ \mu_i\geq\delta,\qquad G(\mu)\geq\delta,\qquad C_i(\mu)\geq\delta. $$
The mixture just constructed makes this polytope feasible with $\delta>0$. It is compact, because its masses lie in the simplex and $\delta$ lies in $[0,1]$.

Maximizing $\delta$ therefore has an optimal vertex with positive $\delta$. At a vertex, independent active constraints determine all coordinates. After clearing row denominators, their integer coefficients have bit length polynomial in $n$. Cramer’s rule and the determinant bound
$$ |\det A|\leq r!\,2^{rb} $$
for an $r$ by $r$ integer matrix with entries of absolute value at most $2^b$ show that every coordinate has polynomial bit length in $n$. The vertex thus supplies a rational society of polynomial encoding length with the prescribed strict slope.

This also supplies a polynomial-length dyadic witness when masses are required to be dyadic. Indeed, the vertex has a positive margin $\delta$ in all displayed inequalities. Approximate its first $m-1$ masses on a dyadic grid and define the last mass by normalization. If each initial approximation has error at most $\varepsilon$, every mass error is at most $m\varepsilon$.

Let $T$ bound the sums of absolute coefficients of the relevant affine forms, including positivity. Choosing
$$ mT\varepsilon<\frac{\delta}{2} $$
preserves all strict inequalities. Both $\log_2 T$ and $\log_2(1/\delta)$ are polynomially bounded in $n$, so a dyadic grid of polynomial bit length suffices.

Consequently, there is a polynomial $P$, depending only on the explicit encoding convention, such that every feasible strict edge sign has a witness whose total public-and-society encoding length is at most $P(n)$.

Consequence for the zero-budget problem

Suppose $R_K^*>0$, and take the edge and two societies from Section 4.

Thus every nonzero-regret instance has two witnessing societies of length polynomial in the actual public input length, regardless of how $L$ is encoded.

A verifier checks their lengths against $L$, positivity, normalization, concavity, and opposite strict slopes using exact rational arithmetic in polynomial time. Therefore the complement of the zero-budget problem has polynomial certificates.

Proved complexity consequence. On the promised inputs, deciding $R_K^*\leq0$ belongs to $\mathrm{coNP}$ under either conventional explicit encoding described above. This establishes neither polynomial-time solvability nor hardness of that restriction.

6. An explicit separation from zero

There is also a quantitative consequence of the two-society witness.

For a rational number $x$, let $q_x$ denote its explicitly encoded denominator. For witnessing societies $\mu^-,\mu^+$, define
$$ Q=q_a\prod_{j=1}^m q_{v_j} \prod_{i=1}^m q_{\mu_i^-} \prod_{i=1}^m q_{\mu_i^+}. $$
Every revenue and loss in these two societies is an integer multiple of $1/Q$.

At each action, their summed loss is positive, so
$$ \ell_{\mu^- i}+\ell_{\mu^+ i}\geq\frac1Q. $$
The lower bound from Section 4 therefore gives
$$ R_K^*\geq\frac1{2Q}. $$

In the explicit encodings under consideration, the logarithm of a denominator is bounded by its encoding length. Counting public data once and the two hidden societies once each gives
$$ \log_2 Q\leq2L. $$
Hence
$$ R_K^*>0 \quad\Longrightarrow\quad R_K^*\geq2^{-2L-1}. $$
In particular, for
$$ 0\leq B<2^{-2L-1}, $$
the decision $R_K^*\leq B$ is equivalent to the zero-budget decision.

7. Constant regret is unavoidable in general

The constant upper bound cannot be replaced by a guarantee tending to zero with the horizon.

Take
$$ V=\left\{\frac12,1\right\},\qquad a=0, $$
and choose $L$ large enough to admit both societies
$$ \mu^+=\left(\frac14,\frac34\right), \qquad \mu^-=\left(\frac34,\frac14\right). $$
Concavity is automatic with two vertices. Their revenues are respectively
$$ (h_1^+,h_2^+)=\left(\frac12,\frac34\right), \qquad (h_1^-,h_2^-)=\left(\frac12,\frac14\right). $$

For an arbitrary policy, let $q$ be the probability of ever querying threshold $1$. Until that first query, all observations are the known zero feedback at threshold $1/2$, so $q$ is the same in both societies.

In $\mu^+$, never querying threshold $1$ incurs regret $K/4$. In $\mu^-$, querying it at least once incurs regret at least $1/4$. Therefore
$$ \sup_{\mu\in\mathcal M}R_K(\pi,\mu) \geq \max\left\{\frac{K(1-q)}4,\frac q4\right\} \geq\frac{K}{4(K+1)}. $$
Taking the infimum gives
$$ R_K^*\geq\frac{K}{4(K+1)}. $$
Thus these promised instances retain a positive constant lower bound as $K$ grows.

8. Remaining question

The constant-regret policy does not compute the exact minimax value. The certificates and separation bound address zero regret and sufficiently small budgets, but do not yield a polynomial algorithm for general $B$.

A complete resolution still requires either an exact algorithm with the requested polynomial dependence on $m,\tau,L,K$, or a hardness reduction preserving positivity, concavity, the encoding-bounded mass class, and unary $K$.

⟨structured verdict parsed — rendered above⟩

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

The output establishes several valid auxiliary results, but it does not resolve the polynomial-time versus hardness question in USER_TASK. Its own claim of partial progress is accurate. I found no mathematical error in the auxiliary arguments under the explicitly stated encoding conventions.

1. Coordinates, concavity, and resolved parameter ranges

The acceptance convention is handled correctly:
$$ s_j=\sum_{i<j}\mu_i,\qquad h_j=v_j+(a-v_j)s_j. $$
In particular, $s_1=0$ and $h_1=v_1$ are known before any observation. Strict positivity and normalization give the stated strict inequalities between cumulative masses.

Because the thresholds are distinct and increasing, every segment-slope denominator is positive. Concavity of the interpolation is therefore equivalent to nonincreasing consecutive segment slopes, as claimed.

The case $m=1$ has zero regret because there is only one action.

The proposition for $a\geq v_{m-1}$ is correct:

$$ h_m-a=\mu_m(v_m-a)>0. $$

Thus $v_m$ is indeed the unique maximizer throughout this parameter range.

2. Midpoint comparison lemma

The midpoint pair exists and lies within the current index interval. The strict inequality $x<v_r$ ensures that the successor index exists, including when $x$ is itself a threshold.

Both interval-retention rules preserve a global maximizer:

The potential estimate is valid. In the first branch, the maximizing index satisfies $q\geq d>l$, so the convexity denominator $v_q-v_l$ is positive. The midpoint inequalities imply $g_d\leq g_l/2$, while convexity gives $g_c\leq g_l$. These establish the claimed factor $3$.

In the second branch, $q\leq c<r$, so $v_r-v_q$ is positive. The corresponding estimates $g_c\leq g_r/2$ and $g_d\leq g_r$ give the same factor.

These arguments also cover adjacent endpoints, equality in the revenue comparison, and maximizing plateaus. No spacing regularity is assumed or needed.

3. Constant-regret policy

The search policy uses only public data and observed cumulative masses. Cached revenues require no additional rounds.

Each update strictly shrinks the index interval. Its final singleton is a global maximizer by the preceding retention argument. Charging each iteration’s actual queries to $g_c+g_d$ and summing the potential decreases correctly gives
$$ \text{total search regret}\leq 3(g_1+g_m). $$

The treatment of a horizon ending during an iteration is sound: the executed queries form a prefix of the completed deterministic search for the fixed society, and all regret terms are nonnegative.

When $a<v_m$, both entries in each revenue’s convex combination lie in $[0,v_m]$. Consequently, every individual loss is at most $1$, and the stated bounds
$$ R_K(\pi,\mu)\leq \min\{K,m-1,6\} $$
follow. The count $m-1$ correctly excludes the initially known revenue $h_1$.

The running-time claim is also justified for explicit encodings. Products of mass denominators have bit length bounded by the sum of their bit lengths; cumulative observations and subsequent rational computations therefore have polynomial bit length. There are at most $m-1$ interval updates and at most $K$ executed rounds.

The more informative bound is correct because
$$ M\leq v_m,\qquad h_m>a. $$

This proves a polynomial-time implementable policy and a sufficient condition for a yes-instance. It does not compute the minimax value or establish that the policy is minimax optimal.

4. Two-society characterization of positive regret

The maximizing set is an index interval: concavity places every intermediate revenue at least at the common maximum of two maximizing endpoints, and maximality forces equality.

The equivalence theorem is correct:

The final implication to strictly positive minimax regret is especially important and is supplied correctly. For the two societies, every action has positive summed loss, so
$$ \delta=\frac12\min_i(\ell_{\mu^-i}+\ell_{\mu^+i})>0. $$
The first-round action distribution is identical across societies because no observations have yet occurred. Averaging their first-round losses gives a policy-independent lower bound $\delta$. Thus taking an infimum over policies cannot reduce the bound to zero.

The direct certificate-length bound of $2L$ is valid.

5. Small witnesses and the zero-budget complexity statement

The reference society has positive normalized masses. The cumulative masses, quadratic revenue formula, and secant-slope differences are all computed correctly. For $m=2$, the strict concavity inequalities are absent, so this part of the construction is vacuous and causes no problem.

The mixture argument correctly preserves the specified strict edge sign for sufficiently small positive mixture weight and makes every existing concavity inequality strict. This intermediate society need not satisfy the original encoding budget; the argument uses it only to establish feasibility of a separate small-witness construction.

The forms $C_i$ correctly express concavity after multiplication by positive threshold spacings.

The auxiliary polytope is compact: its masses lie in the simplex, and $\delta$ is bounded. It has a feasible point with positive $\delta$, so maximizing $\delta$ yields a positive optimum attained at a vertex. The use of independent active constraints, denominator clearing, Cramer’s rule, and the stated determinant bound gives polynomial coordinate bit length. The number of variables and constraints is polynomial in the explicit public encoding length.

The dyadic approximation argument is sound. Normalizing the final mass bounds its error by the sum of the preceding errors. The coefficient-sum bound then preserves positivity, concavity, and the prescribed strict sign using a grid of polynomial bit length.

The comparison with $L$ correctly handles both possibilities:

Checking the two witnesses requires only polynomial-time exact rational arithmetic. Therefore the claimed promised zero-budget membership in $\mathrm{coNP}$ follows under the stated conventional explicit encodings.

This is a membership result only. It establishes neither polynomial-time solvability nor hardness, even for the zero-budget restriction.

6. Separation from zero

The denominator product $Q$ is sufficient. Each product occurring in a revenue has a denominator dividing $Q$, so revenues, maxima, and losses are integer multiples of $1/Q$.

Disjoint maximizing sets make the summed loss at every action strictly positive. Hence each summed loss is at least $1/Q$, and the two-society lower bound gives
$$ R_K^*\geq\frac1{2Q}. $$

Under the stated explicit encoding conventions, the denominator bit lengths for the public data and two hidden societies give
$$ \log_2 Q\leq 2L. $$
The resulting bound
$$ R_K^*>0\implies R_K^*\geq 2^{-2L-1} $$
and the equivalence for budgets strictly below this bound are correct. The strict upper endpoint on the budget range is necessary and is stated correctly.

7. Constant lower-bound example

Both mass lists are positive and normalized, and concavity is automatic for two thresholds. The displayed revenues are correct.

The probability $q$ of ever selecting threshold $1$ is the same in both societies: every history before its first selection consists of identical actions and identical zero observations.

On the event of never selecting threshold $1$, the first society incurs regret $K/4$. Selecting it at least once incurs regret at least $1/4$ in the second society. The bound
$$ \max\left\{\frac{K(1-q)}4,\frac q4\right\} \geq \frac{K}{4(K+1)} $$
is correct. Thus the example establishes regret bounded away from zero as the horizon grows.

8. Blocking issue and minimum required continuation

The sole major issue is incompleteness relative to USER_TASK. The prover expressly leaves the requested exact decision problem unresolved.

To settle the assignment, a further write-up must supply either an exact decision algorithm with the requested polynomial dependence, together with a correctness and complexity proof, or a valid hardness reduction for the specified admissible mass class with unary $K$. The established regret bounds and zero-budget certificates do not substitute for either result.

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