Answer: —
Theorem 4.3 — class: algorithmic
Given finitely many ex ante types \(\Theta\) with rational masses \(\mu_\theta\), finitely represented valuation and initial-state laws \(\nu_{\theta,1}\), participation probabilities, capacities \(\kappa_m\), and horizon \(T\), evolve the atomless karma market under \(K\): bids are \(b=\min\{\Delta v/P_{[\underline{\lambda},\overline{\lambda}]}(\lambda),k\}\), prices are aggregate bid quantiles, and redistribution updates \(\nu_{\theta,t}\). Decide or approximate whether \(K\) is an \(\varepsilon\)-approximate Nash equilibrium, namely whether \(\sup_{\theta\in\Theta}\bigl(\bar C_\theta(K)-\inf_{\beta}\bar C_\theta(\beta;K)\bigr)\le\varepsilon\) for a tagged type-\(\theta\) agent.
An atomless society has total mass \(1\) and is given by its support: \(\Theta\), the list of \(\tau\) ex ante types with positive binary-rational masses \(\mu_\theta\) summing to \(1\); \(\tau\) is the support size, not the number of possible types. There are \(m\ge1\) parallel auctions and a finite horizon \(T\ge1\). All numerical inputs are rational; \(L\) is their total encoding length, including the laws described below.
For each type, valuations are independent across agents and time, with a density represented by rational polynomial pieces, continuously differentiable and bounded above and strictly away from zero on \([\underline v_\theta,1]\), where \(0<\underline v_\theta<1\). The initial-state law \(\nu_{\theta,1}\) is an explicit finite list of rational atoms \((k,\lambda)\) with rational probabilities, \(k>0\), and \(\lambda\in[\underline\lambda,\overline\lambda]\). Independently of valuations and states, each agent draws exactly one auction each period with probabilities \(\pi_{\theta,j}\), summing to \(1\); capacities satisfy \(0<\kappa_j<\sum_\theta\mu_\theta\pi_{\theta,j}\).
Fix \(0<\Delta\le1\), \(0<\underline\lambda<\overline\lambda\), a common step size \(\eta>0\), and \(0\le\varepsilon\le\Delta\). Strategy \(K\) bids \(b=\min\{\Delta v/P_{[\underline\lambda,\overline\lambda]}(\lambda),k\}\), where \(P\) denotes projection.
Let \(B_{j,t}\) be the aggregate bid measure in auction \(j\), induced by the current state laws, valuations, and participation probabilities. Its price is \(p_{j,t}=\inf\{p\ge0:B_{j,t}((p,\infty))\le\kappa_j\}\). Bids above the price win, bids below lose, and bids equal to it receive a uniform lottery allocating the remaining capacity; this convention also applies at price zero.
A winner in auction \(j\) pays \(z=xp_{j,t}\), where \(x\in\{0,1\}\) indicates winning. Every agent receives \(g_t=\sum_{j=1}^m\kappa_jp_{j,t}\). Its cost is \(v(1-\Delta x)\), and its next state under \(K\) is \((k-z+g_t,\lambda+\eta(z-g_t))\); these transitions define \(\nu_{\theta,t+1}\).
Retain the following regularity promises. Represent individuals by a unit-mass label space \(A\); for a fixed multiplier profile \(q\), let \(\ell(q)(a)=\mathbb E[z(a)-g]\) under uncapped bids \(\Delta v(a)/q(a)\). On \(H=\{q:\int_Aq=\int_A\lambda_1\}\) with \(\underline\lambda<q<\overline\lambda\), an interior profile \(q^\star\) satisfies \(\ell(q^\star)=0\), and \(\int_A(q-q')(\ell(q)-\ell(q'))\le-\alpha\int_A(q-q')^2\) for an input \(\alpha>0\); require \(\eta\le1/(2\alpha)\).
A tagged type-\(\theta\) agent has zero mass, starts from \(\nu_{\theta,1}\), and cannot change aggregate prices or redistribution. A deviation \(\beta\) is any measurable randomized history-dependent strategy bidding in \([0,k]\), observing its type, initial state, horizon, current valuation, auction and balance, and its past bids, payments, costs and gains. It retains the same valuation, participation, payment and balance rules. Define \(\bar C_\theta(\beta;K)=T^{-1}\mathbb E[\sum_{t=1}^T v_t(1-\Delta x_t)]\), and \(\bar C_\theta(K)=\bar C_\theta(K;K)\).
Is deciding whether \(\max_{\theta\in\Theta}\{\bar C_\theta(K)-\inf_\beta\bar C_\theta(\beta;K)\}\le\varepsilon\) solvable in time polynomial in \(m,\tau,L,T\), or is it NP-hard?
For finite populations, adaptive karma pacing has a conditional finite-horizon bound on unilateral gains and becomes an approximate Nash equilibrium under suitable joint scaling of horizon, population, parallel auctions, budgets and step size; this is not an equilibrium-verification complexity result ([Berriaud et al.](https://arxiv.org/html/2403.04057v2)).
For a different population model with integer karma and pairwise contests, stationary Nash equilibrium existence is established ([Elokda et al.](https://link.springer.com/article/10.1007/s13235-023-00503-0)); this does not settle the finite-horizon verification question above.
I do not resolve the polynomial-time versus NP-hardness classification. I prove a new obstruction to a polynomial-time algorithm:
Theorem. The square-root-sum decision problem polynomial-time many-one reduces to the verification problem in USER_TASK, even when $T=1$, $\tau=1$, the initial-state law has one atom, and the valuation density is a single polynomial of degree one. Every constructed instance satisfies the functional regularity promises.
Thus exact arithmetic already presents a substantive difficulty in a one-period subclass. The reduction preserves the direction and equality case of the requested weak inequality. It does not establish NP-hardness.
Define the square-root-sum decision problem as follows. Its input consists of positive integers $n_1,\ldots,n_m$ and an integer $K$, encoded in binary; its question is whether
$$ \sum_{j=1}^m\sqrt{n_j}\le K. $$
Related square-root-sum comparison problems are studied in [Kayal and Saha, *On the Sum of Square Roots of Polynomials and Related Problems*](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/Sum20of20Square20Roots20ToCT.pdf). The reduction below is self-contained and assumes no complexity classification for this source problem.
First consider the nontrivial range
$$ m\le K<\sum_{j=1}^m n_j. $$
The remaining inputs will be handled in Section 5.
Write
$$ N=\max_j n_j,\qquad D=2N,\qquad a=\frac{1}{2D},\qquad S=\sum_{j=1}^m\frac{1}{n_j}. $$
Construct a society with one type of mass $1$, one period, and $m$ auctions. Set
$$ \Delta=1,\qquad \underline\lambda=1,\qquad \overline\lambda=\frac{11}{10},\qquad M=\frac{21}{20},\qquad \eta=1,\qquad \alpha=\frac{1}{D^3}. $$
The initial-state law is the single atom
$$ (k_1,\lambda_1)=(2,M). $$
The valuation support is $[a,1]$, with density
$$ f(v)=\frac{2v}{1-a^2}. $$
Participation probabilities and capacities are
$$ \pi_j=\frac{1}{n_jS}, \qquad \kappa_j= \pi_j\frac{1-n_j/D^2}{1-a^2}. $$
Finally, choose the verification threshold
$$ \varepsilon= \frac{2}{3(1-a^2)} \left( \frac{K}{SD^3}-a^3 \right). $$
All these input quantities are rational. For the analysis, introduce
$$ h_j=\frac{\sqrt{n_j}}{D}. $$
The numbers $h_j$ are not part of the encoded output. They satisfy
$$ \frac{1}{D}\le h_j\le\frac12, \qquad h_j^2=\frac{n_j}{D^2}, \qquad \kappa_j=\pi_j\frac{1-h_j^2}{1-a^2}. $$
There is one supported type, with positive binary-rational mass $1$. Its initial balance is positive and its initial multiplier is strictly inside the prescribed interval.
The valuation density is a rational polynomial and is continuously differentiable on $[a,1]$. Moreover,
$$ \int_a^1 f(v)\,dv = \frac{1-a^2}{1-a^2} =1, $$
and throughout its support,
$$ 0< \frac{2a}{1-a^2} \le f(v)\le \frac{2}{1-a^2}. $$
Thus it is bounded above and strictly away from zero.
The participation probabilities are positive and satisfy
$$ \sum_{j=1}^m\pi_j = \frac{1}{S}\sum_{j=1}^m\frac{1}{n_j} =1. $$
Because $a^2=1/(4D^2)$ and $n_j\ge1$,
$$ a^2<h_j^2<1. $$
Consequently,
$$ 0< \frac{1-h_j^2}{1-a^2} <1, $$
so every auction satisfies
$$ 0<\kappa_j<\pi_j. $$
This is precisely the capacity promise for a single type of mass $1$.
The threshold is also admissible. Since $S\le m$ and $K\ge m$,
$$ \frac{K}{SD^3}\ge\frac{1}{D^3}> \frac{1}{8D^3}=a^3, $$
which gives $\varepsilon>0$. For the upper bound, use
$$ S\ge\frac{m}{N}, \qquad K<\sum_j n_j\le mN, \qquad D=2N. $$
These inequalities imply
$$ \frac{K}{SD^3}\le\frac{1}{8N}\le\frac18. $$
Since $a\le1/4$,
$$ \varepsilon \le \frac{2}{3(1-a^2)}\frac18 \le \frac{32}{45}\frac18 = \frac{4}{45}<1=\Delta. $$
It remains to establish the functional regularity promises. Those promises require a statement about all admissible multiplier profiles, rather than merely the constant initial profile.
Take the label space to be $A=[0,1]$ with Lebesgue measure. The hyperplane in the task is
$$ H= \left\{ q:\int_Aq(a)\,da=M \right\}. $$
Throughout this section, consider measurable profiles satisfying
$$ q\in H, \qquad 1<q(a)<\frac{11}{10} $$
almost everywhere. Write
$$ R(q)=\int_Aq(a)^2\,da. $$
In particular,
$$ 1\le R(q)\le\frac{121}{100}. $$
The valuation tail, for $a<y<1$, is
$$ \Pr(v>y)=\frac{1-y^2}{1-a^2}. $$
I claim that the uncapped clearing price in auction $j$ is
$$ p_j(q)=\frac{h_j}{\sqrt{R(q)}}. $$
First, every valuation threshold at this proposed price lies strictly inside the valuation support. Indeed,
$$ p_j(q)q(a) \ge h_j\frac{10}{11} \ge \frac{10}{11D} > \frac{1}{2D}=a, $$
while
$$ p_j(q)q(a) \le h_j\frac{11}{10} \le \frac{11}{20}<1. $$
Thus the aggregate uncapped bid tail at the proposed price is
$$ \begin{aligned} B_j((p_j(q),\infty)) &= \pi_j\int_A \frac{1-p_j(q)^2q(a)^2}{1-a^2}\,da\\ &= \pi_j\frac{1-p_j(q)^2R(q)}{1-a^2}\\ &= \pi_j\frac{1-h_j^2}{1-a^2}\\ &=\kappa_j. \end{aligned} $$
The bounds on the thresholds have a uniform positive margin. Hence, in a neighborhood of this positive price, the tail is
$$ B_j((p,\infty)) = \pi_j\frac{1-p^2R(q)}{1-a^2}, $$
which is strictly decreasing in $p$. Every sufficiently close smaller price therefore has tail strictly greater than capacity. Monotonicity of the tail gives the same conclusion for every smaller nonnegative price. This proves the claimed price under the infimum definition in the task.
There are no bid atoms at these prices: conditional on any label’s multiplier, the uncapped bid has a density. Integrating these zero point masses over labels still gives zero.
Define the positive constant
$$ C_0= \frac{1}{1-a^2}\sum_{j=1}^m\pi_jh_j^3. $$
For a fixed profile $q$, a label with multiplier $q(a)$ has expected payment in auction $j$, including its participation probability,
$$ \pi_jp_j(q) \frac{1-p_j(q)^2q(a)^2}{1-a^2}. $$
Redistribution equals $\sum_j\kappa_jp_j(q)$. Substituting the price and capacity formulas and subtracting redistribution gives
$$ \begin{aligned} \ell(q)(a) &= \sum_j \frac{\pi_jp_j(q)}{1-a^2} \left[ 1-p_j(q)^2q(a)^2-(1-h_j^2) \right]\\ &= \sum_j \frac{\pi_jh_j^3}{(1-a^2)\sqrt{R(q)}} \left[ 1-\frac{q(a)^2}{R(q)} \right]\\ &= C_0\frac{R(q)-q(a)^2}{R(q)^{3/2}}. \end{aligned} $$
The constant profile
$$ q^\star(a)=M $$
is interior and belongs to $H$. Since $R(q^\star)=M^2$, the displayed formula yields
$$ \ell(q^\star)(a)=0 $$
for every label.
Let $q,q'\in H$ be admissible, and put
$$ h=q-q', \qquad q_s=q'+sh,\qquad 0\le s\le1. $$
Then every $q_s$ remains admissible and
$$ \int_Ah\,da=0. $$
For an intermediate profile $r=q_s$, abbreviate $R=R(r)$. Differentiating the drift formula along the segment gives
$$ D\ell(r)[h](a) = C_0\left[ -\frac{2r(a)h(a)}{R^{3/2}} + \left( -\frac{1}{R^{3/2}} +\frac{3r(a)^2}{R^{5/2}} \right) \int_A rh\,da \right]. $$
Pairing this derivative with $h$, and using $\int_Ah=0$, gives
$$ \int_AhD\ell(r)[h]\,da = C_0\left[ -\frac{2\int_A rh^2\,da}{R^{3/2}} + \frac{ 3\left(\int_A rh\,da\right) \left(\int_A r^2h\,da\right) }{R^{5/2}} \right]. $$
Here are explicit bounds for both terms. Write
$$ u=\frac{11}{10}, \qquad \delta=\frac{1}{20}, \qquad \|h\|_2^2=\int_Ah^2\,da. $$
Because $r\ge1$ and $R\le u^2$,
$$ \frac{2\int_A rh^2\,da}{R^{3/2}} \ge \frac{2}{u^3}\|h\|_2^2. $$
Also, $|r-M|\le\delta$. The zero integral of $h$ and the Cauchy–Schwarz inequality imply
$$ \left|\int_A rh\,da\right| = \left|\int_A(r-M)h\,da\right| \le\delta\|h\|_2. $$
Similarly, since $|r^2-M^2|\le\delta(2M+\delta)$,
$$ \left|\int_A r^2h\,da\right| = \left|\int_A(r^2-M^2)h\,da\right| \le \delta(2M+\delta)\|h\|_2. $$
Using $R\ge1$, we therefore obtain
$$ \int_AhD\ell(r)[h]\,da \le -C_0 \left[ \frac{2}{u^3} - 3\delta^2(2M+\delta) \right] \|h\|_2^2. $$
The bracket is strictly greater than $1$, because
$$ \frac{2}{u^3} - 3\delta^2(2M+\delta) = \frac{2000}{1331}-\frac{129}{8000} = \frac{15828301}{10648000}>1. $$
Furthermore, $h_j\ge1/D$ and $\sum_j\pi_j=1$, so
$$ C_0 = \frac{\sum_j\pi_jh_j^3}{1-a^2} \ge \frac{1}{D^3} =\alpha. $$
It follows that
$$ \int_AhD\ell(r)[h]\,da \le -\alpha\|h\|_2^2. $$
All profiles and directions used here are bounded, and $R$ stays bounded away from zero. Thus differentiation under the label integral and integration of the derivative along the segment are justified by bounded domination. Integrating over $s$ proves
$$ \begin{aligned} \int_A(q-q')(\ell(q)-\ell(q'))\,da &= \int_0^1\int_AhD\ell(q_s)[h]\,da\,ds\\ &\le -\alpha\int_A(q-q')^2\,da. \end{aligned} $$
This is the required strong-monotonicity inequality on the entire promised domain.
Finally, $D\ge2$, and hence
$$ \eta=1\le\frac{D^3}{2}=\frac{1}{2\alpha}. $$
Every functional regularity promise is satisfied.
Initially all multipliers equal $M$. The strategy-$K$ bid is uncapped, since
$$ \frac{v}{M}\le\frac{1}{M}<1<k_1=2. $$
Therefore the actual initial bid measures coincide with the uncapped bid measures analyzed above. Since $R(M)=M^2$, auction $j$ has price
$$ p_{j,1}=\frac{h_j}{M}. $$
There is no bid atom at the price. Under strategy $K$, the tagged agent wins precisely when
$$ \frac{v}{M}>\frac{h_j}{M}, $$
equivalently when $v>h_j$, apart from an event of probability zero.
A deviation can bid its entire balance $2$ in every auction. Since
$$ p_{j,1}=\frac{h_j}{M}<1<2, $$
this deviation wins surely. With $\Delta=1$, its cost is zero. Every feasible strategy has nonnegative cost, so
$$ \inf_\beta\bar C_\theta(\beta;K)=0. $$
Under $K$, losing in auction $j$ incurs cost $v$. Its expected cost conditional on participating in that auction is
$$ \int_a^{h_j}vf(v)\,dv = \frac{2}{1-a^2}\int_a^{h_j}v^2\,dv = \frac{2(h_j^3-a^3)}{3(1-a^2)}. $$
There is one type and one period. Consequently the unilateral gain in the target decision is exactly
$$ \begin{aligned} G &= \bar C_\theta(K)-\inf_\beta\bar C_\theta(\beta;K)\\ &= \frac{2}{3(1-a^2)} \left[ \sum_{j=1}^m\pi_jh_j^3-a^3 \right]. \end{aligned} $$
By the definitions of $\pi_j$ and $h_j$,
$$ \pi_jh_j^3 = \frac{1}{n_jS}\frac{n_j^{3/2}}{D^3} = \frac{\sqrt{n_j}}{SD^3}. $$
Thus
$$ G= \frac{2}{3(1-a^2)} \left[ \frac{\sum_j\sqrt{n_j}}{SD^3}-a^3 \right]. $$
Comparing this expression with the constructed rational threshold gives the exact equivalence
$$ G\le\varepsilon \quad\Longleftrightarrow\quad \sum_{j=1}^m\sqrt{n_j}\le K. $$
The multiplier of the compared expressions is strictly positive. In particular, equality is preserved.
The construction above handles $m\le K<\sum_jn_j$.
If $K<m$, then
$$ \sum_j\sqrt{n_j}\ge m>K, $$
so the source instance is a no-instance. If $K\ge\sum_jn_j$, then
$$ \sum_j\sqrt{n_j}\le\sum_jn_j\le K, $$
so it is a yes-instance.
For these two cases, output fixed valid no- and yes-instances respectively. Such fixed instances are obtained from the same parameter family with $m=1$ and $n_1=1$. Section 4 gives their gain as
$$ G= \frac{2}{3(1-1/16)} \left(\frac18-\frac1{64}\right) = \frac7{90}. $$
Choose $\varepsilon=0$ for the fixed no-instance and $\varepsilon=1$ for the fixed yes-instance. Both thresholds are allowed, and Section 3 verifies their regularity promises.
Finally, the reduction has polynomial bit complexity. If the source encoding length is $b$, then $m$ and every $\log n_j$ are bounded by $b$. The rational number
$$ S=\sum_j\frac1{n_j} $$
can be computed using the common denominator $\prod_jn_j$, whose bit length is at most $\sum_j\log_2n_j+1$. Its numerator also has polynomial bit length.
Every output quantity is obtained from these integers and rationals by polynomially many additions, multiplications, and divisions. The powers $D^2$ and $D^3$ have polynomial bit length. There are $m$ explicitly encoded auctions, one initial atom, and one linear density piece. Hence both the output length and the construction time are polynomial in $b$.
This completes the claimed polynomial-time many-one reduction.
The reduction proves that an algorithm polynomial in $m,\tau,L,T$ for the full verification problem would yield a polynomial-time algorithm for square-root-sum comparison.
The obstacle occurs with $T=1$, a single supported type, and a linear density, while satisfying the strong-monotonicity promise globally. It therefore arises before any growth of state support over time. The inverse participation weights cancel the extra integer factors in the cubic truncated valuation moments, leaving exactly the desired sum of square roots.
The requested complexity classification remains unresolved. This reduction supplies neither an NP-hardness proof nor a general polynomial-time algorithm.
⟨structured verdict parsed — rendered above⟩
The square-root-sum reduction is correct as written. It preserves the requested weak inequality, has polynomial encoding length, and satisfies the stated input and functional regularity promises.
However, it does not resolve USER_TASK: it establishes neither a polynomial-time algorithm nor NP-hardness. The prover explicitly acknowledges this limitation. The appropriate overall status is partial, with no identified mathematical defect in the reduction itself.
The source question is stated precisely:
$$ \sum_{j=1}^m\sqrt{n_j}\le K, $$
where the $n_j$ are positive integers and $K$ is an integer.
The split into the nontrivial range
$$ m\le K<\sum_j n_j $$
and the two remaining ranges is exhaustive. The treatment of the remaining ranges in Section 5 is valid.
All encoded parameters in the main construction are rational. The auxiliary quantities
$$ h_j=\frac{\sqrt{n_j}}{D} $$
are used only in the analysis, so their possible irrationality does not violate the rational-input requirement.
The stated bounds
$$ \frac1D\le h_j\le\frac12 $$
hold for every positive integer $n_j\le N$ with $D=2N$. In particular, the construction includes the case $N=1$ wherever the parameter family is used.
Finding: This part is correct.
The single type has admissible mass $1$. The initial atom has positive balance and multiplier
$$ 1<M=\frac{21}{20}<\frac{11}{10}. $$
The valuation support satisfies
$$ 0<a=\frac1{2D}\le\frac14<1. $$
The polynomial density is normalized, continuously differentiable on the specified support, bounded above, and bounded strictly away from zero there. The normalization and bounds given in the output are correct.
The participation probabilities are positive and sum to $1$. Since
$$ a^2<h_j^2<1, $$
the capacity formula gives precisely
$$ 0<\kappa_j<\pi_j. $$
Thus the auction-capacity promise holds for the one-type society.
The threshold bounds are also correct. The lower-bound argument establishes $\varepsilon>0$ in the nontrivial source range. The upper-bound calculation gives
$$ \varepsilon\le\frac4{45}<1=\Delta. $$
The restrictions on $\Delta$, the multiplier interval, and $\eta$ are satisfied.
Finding: All elementary input promises are verified.
This is the main nontrivial part of the proof. The output correctly verifies the promises for arbitrary admissible measurable profiles, rather than checking only the constant initial multiplier.
For every admissible profile $q$, the proposed price is
$$ p_j(q)=\frac{h_j}{\sqrt{R(q)}}. $$
The bounds on $q$ and $R(q)$ place every valuation threshold $p_j(q)q(a)$ strictly inside the valuation support, with a uniform positive margin. Therefore the polynomial tail formula applies throughout a neighborhood of the proposed price.
Substitution gives aggregate tail mass exactly $\kappa_j$. The output also checks the point required by the infimum definition: every smaller nonnegative price has tail mass strictly greater than capacity. Local strict decrease, together with global monotonicity of the tail, justifies that conclusion.
Conditional bid distributions have no atoms, and integrating their point masses over labels preserves this property. Thus the tie lottery does not alter the payment formula at these prices.
Finding: The clearing-price formula is justified under the task’s precise price convention.
The expected-payment expression includes the participation probability $\pi_j$. The redistribution term uses the same clearing prices and capacities.
The subtraction and simplification yield correctly
$$ \ell(q)(a) = C_0\frac{R(q)-q(a)^2}{R(q)^{3/2}}. $$
The constant profile $q^\star(a)=M$ lies in the required hyperplane and strictly inside the multiplier interval. Substituting $R(q^\star)=M^2$ gives $\ell(q^\star)=0$.
Finding: The drift formula and interior-zero promise are verified.
For admissible $q,q'$, the segment $q_s=q'+s(q-q')$ remains in the multiplier interval and in the hyperplane. In particular, its direction $h=q-q'$ has zero integral, as required by the subsequent cancellations.
The displayed directional derivative of $\ell$ is correct. Pairing it with $h$ correctly eliminates the term proportional to $\int_A h$.
The estimates for the negative term and the mixed term are valid. The uses of Cauchy–Schwarz have the necessary hypotheses: the profiles and directions are bounded on a unit-measure space and hence belong to $L^2$.
The numerical calculation checks out:
$$ \frac{2000}{1331}-\frac{129}{8000} = \frac{15828301}{10648000}>1. $$
Also,
$$ C_0\ge\frac1{D^3}=\alpha. $$
These bounds give the required derivative inequality with the stated $\alpha$. The bounded-domination justification is adequate: profiles and directions are bounded, and the denominator stays bounded away from zero along the entire segment. Integrating the derivative therefore establishes the required inequality for every admissible pair $q,q'$.
Finally,
$$ \eta=1\le\frac{D^3}{2}=\frac1{2\alpha} $$
holds because $D\ge2$.
Finding: The global functional regularity promises are fully verified. No missing lemma or unverified theorem application was identified here.
At the initial state, projection leaves $M$ unchanged, and the balance cap is inactive. Therefore the actual strategy-$K$ bid distribution agrees with the uncapped distribution used in Section 3.
The resulting price is correctly
$$ p_{j,1}=\frac{h_j}{M}. $$
The strategy-$K$ win condition is $v>h_j$, with equality having probability zero.
The proposed deviation bids the available balance $2$ in the selected auction. This is an admissible strategy, and its bid exceeds every constructed price. Since the tagged agent has zero mass, this deviation leaves aggregate prices and redistribution unchanged.
For $\Delta=1$, winning produces zero cost. All admissible strategies have nonnegative cost. Consequently, the claimed equality
$$ \inf_\beta\bar C_\theta(\beta;K)=0 $$
is justified; the output establishes an attained optimum, rather than merely an upper bound on the infimum.
The truncated valuation-moment computation is correct. Weighting by the participation probabilities yields the stated expression for $G$. The identity
$$ \pi_jh_j^3=\frac{\sqrt{n_j}}{SD^3} $$
is also correct.
The coefficient used to compare $G$ with $\varepsilon$ is strictly positive. Thus the equivalence
$$ G\le\varepsilon \quad\Longleftrightarrow\quad \sum_j\sqrt{n_j}\le K $$
preserves both direction and equality.
Finding: The target decision is exactly equivalent to the source decision on the constructed instances.
For $K<m$, the source instance is correctly identified as a no-instance. For $K\ge\sum_jn_j$, it is correctly identified as a yes-instance.
The fixed-instance calculation is correct:
$$ G=\frac7{90}. $$
Hence $\varepsilon=0$ gives a valid no-instance and $\varepsilon=1$ gives a valid yes-instance. Both thresholds satisfy the task’s allowed range. The regularity verification applies to these instances independently of the original source-range restriction.
The encoding argument is sufficient. The common denominator for $S$ has polynomial bit length, and its numerator does as well. The remaining formulas use polynomially many rational operations on quantities whose bit lengths remain polynomial in the source encoding length. The explicit number of auctions is also polynomial in that length.
Finding: The output defines a polynomial-time many-one reduction on all source inputs.
The proved consequence is conditional: a polynomial-time algorithm for the verification problem would give a polynomial-time algorithm for square-root-sum comparison.
The output assumes no hardness classification for square-root-sum comparison. Accordingly, the reduction supplies no NP-hardness conclusion. It also supplies no general algorithm for the verification problem.
Major scope issue: The polynomial-time-versus-NP-hardness question in USER_TASK remains unanswered. This is an acknowledged limitation of the result, not a mathematical flaw in its proof.
The minimum additional work needed to settle the assigned task is a valid polynomial-time algorithm or an NP-hardness proof for the stated verification problem, including its regularity promises. No repair to the present reduction 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.