← back to the atlas

d4-conf-sagt-2018-0021 (d4-conf-sagt-2018-0021)

Answer: Polynomial-time solvable in \(m,\tau,L,\log(1/\delta)\) under the stated certified exponential-evaluation model.

The anchor (named result in the paper)

Theorem 4 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateIt is NP-hard to compute RLCV(Γf), even under influence cooper- ative game.

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

The continuous mirror question, as graded

Given \(\tau\) types with rational masses \(\mu_t\ge 0\), \(\sum_{t=1}^{\tau}\mu_t=1\), and \(q\) audience classes with rational weights \(w_j\ge 0\) and rates \(\lambda_{tj}\ge 0\), define \(\Sigma(a)=\sum_{j=1}^{q} w_j(1-\exp(-\sum_{t=1}^{\tau}\lambda_{tj}a_t))\) for coalition masses \(a\in[0,\mu]\). For rational \(0\le\eta\le\Sigma(\mu)\), determine the bit complexity, in \(\tau,q\), input length \(L\), and accuracy \(\delta\), of approximating the least \(r\in[0,1]\) for which there is a type-level per-capita allocation \(p\ge0\) satisfying \(\sum_t\mu_tp_t=\Sigma(\mu)\) and \(\sum_ta_tp_t\ge(1-r)\Sigma(a)\) for every \(a\in[0,\mu]\) with \(\Sigma(a)\ge\eta\). Return an additive-\(\delta\) approximation to the optimum and a \(\delta\)-feasible allocation in a specified weak-optimization model for the exponential terms.

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

A society is given by its support: \(\tau\ge1\) types with positive binary rational masses \(\mu_t\), summing to \(1\); \(\tau\) is the support size, not the number of possible types. There are \(q\ge1\) audience classes with binary rational weights \(w_j\ge0\) and rates \(\lambda_{tj}\ge0\); write \(m=q\) and let \(L\) be the total input bit length.
A coalition is any real vector \(a\in\prod_{t=1}^{\tau}[0,\mu_t]\). Define \(\Sigma(a)=\sum_{j=1}^{q}w_j(1-\exp(-\sum_{t=1}^{\tau}\lambda_{tj}a_t))\), and take a binary rational threshold \(0\le\eta\le\Sigma(\mu)\). Its profit is \(\Sigma(a)\) when \(\Sigma(a)\ge\eta\), and zero otherwise; equality counts as successful.
A type-level allocation gives every unit of type \(t\) the same real payment \(p_t\ge0\). Define \(r^*\) as the minimum \(r\in[0,1]\) for which some such allocation satisfies \(\sum_t\mu_tp_t=\Sigma(\mu)\) and \(\sum_ta_tp_t\ge(1-r)\Sigma(a)\) for every successful coalition.
Use the Turing bit model: at rational \(z\ge0\), exponential evaluation supplies a certified rational interval containing \(\exp(-z)\) of width at most \(2^{-k}\), with cost polynomial in the bit length of \(z\) and \(k\); no exact transcendental comparison oracle is supplied.
For binary rational \(0<\delta<1\), the weak optimization problem asks for rational \(\widehat r\in[0,1]\), \(\widehat p\ge0\) with \(|\widehat r-r^*|\le\delta\), \(|\sum_t\mu_t\widehat p_t-\Sigma(\mu)|\le\delta\), and \(\sum_ta_t\widehat p_t\ge(1-\widehat r)\Sigma(a)-\delta\) for every coalition satisfying the exact threshold condition \(\Sigma(a)\ge\eta\).

Is this continuous weak optimization problem solvable in time polynomial in \(m=q\), \(\tau\), \(L\), and \(\log(1/\delta)\), or is it NP-hard?

For finite players, computing the relative least-core value of a truncated monotone submodular profit game is NP-hard even for independent-cascade influence profits; with \(\eta=0\), it is polynomial-time solvable given a value oracle ([source](https://www.microsoft.com/en-us/research/wp-content/uploads/2020/04/TCS20_coreness.pdf)). No result settling the continuous problem defined here was located.

Modeling choices made when packaging the task

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

Result

The continuous weak optimization problem is solvable in time polynomial in \(m,\tau,L,\log(1/\delta)\) in the stated Turing model.

The exact threshold requires care: simply invoking convex optimization over the successful coalitions would leave a numerical conditioning gap. The proof below handles thresholds very close to the grand coalition’s profit separately, and otherwise replaces the threshold constraint by a polynomially bounded exact penalty.

1. Normalization and elementary properties

Write \(n=\tau\), and introduce
\[ \]
\(x_t=a_t/\mu_t,\quad b_t=\mu_tp_t,\quad v_{tj}=\mu_t\lambda_{tj}.\)

Thus \(x\in[0,1]^n\), and the coalition’s payment is \(b\cdot x\). Define

\(F(x)=\sum_jw_j(1-\exp(-v_j\cdot x)),\qquad S=F(\mathbf 1).\)

The exact budget constraint becomes \(\sum_tb_t=S\). Put \(c=1-r\), and let \(c^*\) be the largest feasible success factor. Then \(r^*=1-c^*\).

For every \(x\in[0,1]^n\),

\(\nabla F(x)=\sum_jw_j\exp(-v_j\cdot x)v_j,\)

\(\nabla^2F(x)=-\sum_jw_j\exp(-v_j\cdot x)v_jv_j^{\mathsf T}.\)

Consequently, \(F\) is nonnegative, coordinatewise nondecreasing, and concave. In particular,

\(F(x)\le S,\qquad F(y)\le F(x)+\nabla F(x)\cdot(y-x).\)

The optimum exists: the budget simplex and \(c\in[0,1]\) form a compact set, and each coalition constraint defines a closed subset of it.

Discard audience classes with \(w_j=0\) or \(v_j\cdot\mathbf1=0\), since their contributions vanish identically. If no classes remain, then \(S=0\), the promise forces \(\eta=0\), and \(r^*=0\); outputting zero payments solves the problem.

Henceforth suppose at least one class remains. Define the positive rational quantities

\(h_j=v_j\cdot\mathbf1,\qquad h_{\min}=\min_jh_j,\qquad W=\sum_jw_j.\)

Every retained class has \(h_j>0\), so

\(0<S<W.\)

All rational quantities formed from these data by the operations below have polynomial bit length.

2. The finite-precision convex optimization tool

We use the standard finite-precision ellipsoid theorem: a bounded convex body with a polynomial-time weak separation oracle admits polynomial-time weak linear optimization. This theorem works with rational approximate separators, rather than exact real comparisons. See [Grötschel, Lovász and Schrijver, Section 4.2](https://www.zib.de/userpage/groetschel/pubnew/paper/groetschellovaszschrijver1988.pdf).

Here is the consequence needed below, including why approximate first-order information suffices.

Optimization fact. Let \(D\) be a rational cube, or a rational simplex represented in independent coordinates, possibly multiplied by an interval. Suppose a convex function \(f\) on \(D\) has known rational bounds

\(|f|\le M,\qquad |f(y)-f(z)|\le H\|y-z\|_2,\)

where the descriptions of \(M,H\) have polynomial length. Suppose that, for every rational \(z\in D\) and rational \(\nu>0\), one can compute rational \(\ell,g\) satisfying

\(|\ell-f(z)|\le\nu,\)

\(f(y)\ge f(z)+g\cdot(y-z)-\nu\quad\text{for all }y\in D,\)

in time polynomial in the query length and \(\log(1/\nu)\). Then one can return rational \(z_\epsilon\in D\) with

\(f(z_\epsilon)\le\min_Df+\epsilon\)

in polynomial time.

To verify this consequence, consider the bounded epigraph

\(E=\{(z,t):z\in D,\ f(z)\le t\le M+1\}.\)

If a queried point violates a rational defining inequality of \(D\), or \(t\le M+1\), use that inequality to separate it. Otherwise:

\(g\cdot(y-z)-(s-t)\le t-\ell+2\nu<0\).
Thus the rational vector \((g,-1)\) gives a valid separator.

This constructs a weak separation oracle without exact comparisons.

If \(D\) contains a known ball of radius \(\rho_D\) centered at \(z_0\), then \(E\) contains a ball centered at \((z_0,M+1/2)\) of radius \(\min(\rho_D,1/4)\). Mixing an optimal epigraph point with this center produces sufficiently deep points with objective increase bounded linearly in the mixing coefficient. Weak linear optimization therefore approximates \(\min f\) to any requested accuracy using polynomially many precision bits.

Finally, an approximately feasible domain coordinate can be moved into \(D\) by rational clipping and, for a simplex, normalization. The displacement is bounded by a polynomial in the dimension times the original distance. The Lipschitz bound controls the resulting objective error. This proves the stated optimization fact.

Both domains used below have explicit interior balls: the coalition cube has radius \(1/2\); a simplex in independent coordinates, multiplied by \([0,1]\), has an interior radius bounded below by an inverse polynomial in \(n\).

3. The case \(\eta=0\)

Set

\(G_t=\sum_jw_jv_{tj},\qquad G=\sum_tG_t>0.\)

Concavity at the origin gives

\(F(x)\le\sum_tG_tx_t.\)

Conversely, feasibility for coalitions \(x=se_t\), followed by division by \(s>0\) and the limit \(s\downarrow0\), requires

\(b_t\ge cG_t.\)

Summing and using the budget yields \(S\ge cG\). Therefore

\(c^*=S/G,\qquad r^*=1-S/G,\)

and the allocation \(b_t=SG_t/G\) attains this value.

For rational output, compute a certified rational upper approximation \(B\) satisfying

\(S\le B\le S+e,\qquad e=\min(\delta/8,\delta G/8).\)

Output

\(\widehat b_t=BG_t/G,\qquad \widehat c=\min(1,B/G),\qquad \widehat r=1-\widehat c,\qquad \widehat p_t=\widehat b_t/\mu_t.\)

Then \(\widehat b_t\ge\widehat cG_t\), so every coalition constraint holds exactly. The budget error is at most \(e\le\delta\), and

\(|\widehat r-r^*|\le e/G\le\delta/8.\)

The prescribed exponential evaluator computes \(B\) in polynomial time.

4. Detecting a safely solvable near-threshold case

Now assume \(\eta>0\). Define

\(d=S-\eta,\qquad D=W-\eta.\)

The promise and \(S<W\) imply that \(D>0\). Crucially, \(D\) is a positive rational of polynomial bit length; we never need a lower bound on a nonzero transcendental difference.

Let

\(\gamma=\nabla F(\mathbf1),\qquad T=\sum_t\gamma_t=\sum_jw_jh_j\exp(-h_j).\)

Then

\(T\ge h_{\min}\sum_jw_j\exp(-h_j)=h_{\min}(W-S)=h_{\min}(D-d).\)

Define rational numbers

\(t_0=h_{\min}D/2,\qquad g=\min(D/4,\delta t_0/8),\)

\(e=\min(\delta/16,\delta\eta/64).\)

Compute a certified interval \([S_-,S_+]\) containing \(S\), of width at most \(\min(g/2,e)\). Set \(B=\min(W,S_+)\). Thus

\(S\le B\le S+e.\)

Use the following rational comparison:

Indeed, in the second case,

\(d\ge S_--\eta\ge S_+-\eta-g/2>3g/2>g.\)

This decision requires no exact comparison involving \(S\).

Proof and output for the near-threshold branch

Here \(d\le2g\le D/2\), so \(T\ge t_0\), and

\(d/T\le2g/t_0\le\delta/4.\)

For every successful \(x\), concavity at \(\mathbf1\) gives

\(F(x)\le S-\gamma\cdot(\mathbf1-x).\)

Since \(F(x)\ge\eta=S-d\), it follows that

\(\gamma\cdot(\mathbf1-x)\le d.\)

The ideal allocation \(b^0=S\gamma/T\) therefore satisfies

\(b^0\cdot x\ge S(1-d/T)\ge(1-d/T)F(x).\)

Consequently,

\(0\le r^*\le d/T\le\delta/4.\)

We can approximate this allocation rationally. Compute a nonnegative rational vector \(\widetilde\gamma\) with

\(\|\widetilde\gamma-\gamma\|_1\le\rho,\qquad \rho=\min(t_0/4,\delta t_0/(32(W+1))).\)

Its sum \(\widetilde T\) is positive. Output

\(\widehat b=B\widetilde\gamma/\widetilde T,\qquad \widehat r=\delta/2,\qquad \widehat p_t=\widehat b_t/\mu_t.\)

Normalization gives

\(\|\widetilde\gamma/\widetilde T-\gamma/T\|_1\le2\rho/T.\)

Hence

\(\|\widehat b-b^0\|_1\le e+2S\rho/t_0\le\delta/8.\)

For every successful \(x\),

\(\widehat b\cdot x\ge(1-\delta/4)F(x)-\delta/8 \ge(1-\widehat r)F(x)-\delta.\)

Moreover,

\(|\widehat r-r^*|\le\delta/2,\qquad |\sum_t\widehat b_t-S|\le e\le\delta.\)

All required precision parameters have polynomial bit length.

5. An exact penalty when \(S-\eta\ge g\)

For the general branch we now have a certified lower bound \(d\ge g>0\).

Temporarily allow the rational budget \(B\). For \(b\ge0\), \(\sum_tb_t=B\), and \(c\in[0,1]\), define

\(M(b,c)=\max_{\substack{x\in[0,1]^n\\F(x)\ge\eta}}\{cF(x)-b\cdot x\}.\)

Choose the rational penalty

\(P=B/g+1,\)

and define on the entire cube

\(H_{b,c}(x)=cF(x)-b\cdot x-P(\eta-F(x))_+.\)

Exact-penalty identity.

\(\max_{x\in[0,1]^n}H_{b,c}(x)=M(b,c).\)

Successful coalitions immediately give one inequality. For the other, suppose \(F(x)<\eta\), and put \(s=\eta-F(x)>0\). Define

\(\theta=s/(S-F(x)),\qquad y=(1-\theta)x+\theta\mathbf1.\)

Concavity implies \(F(y)\ge\eta\). Also,

\(\theta\le s/g,\qquad b\cdot(y-x)\le B\theta,\qquad F(y)\ge F(x).\)

Thus

\(cF(x)-b\cdot x\le cF(y)-b\cdot y+Bs/g,\)

and therefore

\(H_{b,c}(x)\le M(b,c)-(P-B/g)s\le M(b,c).\)

This proves the identity.

Furthermore,

\(H_{b,c}(x)=\min\{cF(x)-b\cdot x,\ (c+P)F(x)-b\cdot x-P\eta\},\)

so \(H_{b,c}\) is concave. Coalition separation has become concave maximization over a full rational cube.

6. Polynomial-time approximate oracles

We next verify the finite-precision requirements rather than assuming exact value oracles.

Let \(A=\sum_jw_jh_j\). On the cube, \(\|\nabla F(x)\|_2\le A\). Consequently, a rational Lipschitz bound for \(H_{b,c}\) is

\((1+P)A+B,\)

and a rational absolute-value bound is \(W+B+P\eta\). These bounds have polynomial bit length.

At rational \(x\), all exponents \(v_j\cdot x\) are nonnegative rationals. The supplied evaluator therefore computes \(F(x)\) and its gradient to any absolute precision in polynomial time. Multiplication by weights, rates, or \(P\) requires only polynomially many additional precision bits.

For the nonsmooth minimum defining \(H_{b,c}\), approximate both branches and select the smaller approximation. If branch values are accurate to \(\nu\), the selected branch’s true value exceeds their true minimum by at most \(2\nu\). Its concavity inequality consequently gives an approximate supporting hyperplane for \(H_{b,c}\). Approximating its gradient adds another controllable error over the bounded cube.

The optimization fact applied to \(-H_{b,c}\) therefore returns rational \(x\) with

\(H_{b,c}(x)\ge M(b,c)-\xi\)

in time polynomial in \(n,m,L,\log(1/\delta),\log(1/\xi)\).

This also supplies an approximate subgradient oracle for the outer convex function \(M\). For fixed \(x\), \(H_{b,c}(x)\) is affine in \((b,c)\), with coefficients \((-x,F(x))\). Hence, for any \((b',c')\),

\(M(b',c')\ge H_{b',c'}(x) =H_{b,c}(x)-x\cdot(b'-b)+F(x)(c'-c).\)

Because \(H_{b,c}(x)\ge M(b,c)-\xi\), these coefficients form a \(\xi\)-subgradient. Certified approximations to \(F(x)\) and the constant term preserve this inequality with arbitrarily small additional error.

Thus both nested optimization levels have the required polynomial-time approximate oracles.

7. Outer optimization and rational feasibility correction

Let \(c_B^*\) be the largest exactly feasible success factor with budget \(B\), still restricted to \([0,1]\). Consider the convex objective

\(f(b,c)=-c+\frac2\eta\max(0,M(b,c))\)

over

\(b\ge0,\qquad \sum_tb_t=B,\qquad 0\le c\le1.\)

For \(V=\max(0,M(b,c))\), define

\(c'=\max(0,c-V/\eta).\)

Then \((b,c')\) is feasible. Indeed, if \(c'>0\), every successful \(x\) satisfies

\(c'F(x)-b\cdot x =cF(x)-b\cdot x-(V/\eta)F(x)\le V-V=0.\)

If \(c'=0\), feasibility follows from nonnegative payments. Since \(c-c'\le V/\eta\),

\(f(b,c)\ge-c'+V/\eta\ge-c_B^*+V/\eta.\)

An optimal feasible pair has objective \(-c_B^*\). Therefore

\(\min f=-c_B^*.\)

The approximate oracle construction from the preceding section also applies to \(\max(0,M)\): choose the better of the constant-zero branch and the approximate affine witness for \(M\). Scaling oracle accuracy by the rational factor \(2/\eta\) costs only polynomially many precision bits.

In independent simplex coordinates, the outer domain has polynomial dimension and a known interior radius. Moreover, \(f\) has polynomial-description bounds, for example

\(|f|\le1+2W/\eta,\qquad \operatorname{Lip}(f)\le1+(2/\eta)(nB+W).\)

Apply the optimization fact with \(\epsilon=\delta/16\), obtaining rational \((b,c)\) such that

\(f(b,c)\le-c_B^*+\epsilon.\)

The preceding inequalities imply

\(V\le\epsilon\eta,\qquad c\ge c_B^*-\epsilon.\)

Now make the explicit rational correction

\(\widehat c=\max(0,c-\epsilon).\)

Every successful coalition satisfies

\(b\cdot x\ge\widehat cF(x).\)

Thus this correction produces exact coalition feasibility, not merely approximate threshold feasibility. It also gives

\(c_B^*-2\epsilon\le\widehat c\le c_B^*.\)

8. Comparing the rational budget with the exact budget

Since \(B\ge S\), increasing payments shows \(c_B^*\ge c^*\).

Conversely, take a feasible budget-\(B\) allocation and scale it by \(S/B\). The payment to any coalition decreases by at most \(B-S\), because its coordinates lie in \([0,1]\). Reducing its success factor by \((B-S)/\eta\), or to zero if necessary, restores feasibility. Therefore

\(0\le c_B^*-c^*\le(B-S)/\eta\le e/\eta\le\delta/64.\)

Combining this with the outer optimization bound yields

\(|\widehat c-c^*|\le2\epsilon+e/\eta \le\delta/8+\delta/64<\delta.\)

Output

\(\widehat r=1-\widehat c,\qquad \widehat p_t=b_t/\mu_t.\)

These are rational and nonnegative, with \(\widehat r\in[0,1]\). They satisfy

\(|\widehat r-r^*|<\delta,\)

\(|\sum_t\mu_t\widehat p_t-S|=B-S\le e\le\delta,\)

and, for every coalition satisfying the exact threshold,

\(\sum_ta_t\widehat p_t\ge(1-\widehat r)\Sigma(a).\)

The last inequality is stronger than the requested inequality.

9. Complexity conclusion

The positive rational quantities \(D,h_{\min},t_0,g,e,\eta\) have polynomial bit length. Thus their inverses, all penalty and Lipschitz bounds, and every precision requested from exponential evaluation have descriptions polynomial in \(m,\tau,L,\log(1/\delta)\).

Each convex optimization level makes polynomially many oracle calls. Each outer oracle call invokes one polynomial-time inner optimization, so their composition remains polynomial-time. Division by the positive rational masses \(\mu_t\) preserves polynomial output length.

The algorithm never decides an exact transcendental equality or exact coalition membership. Its guarantees nevertheless cover every coalition satisfying the exact threshold, including equality.

⟨structured verdict parsed — rendered above⟩

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

Verdict

Proved with minor gaps. The argument supports polynomial-time solvability of the continuous weak optimization problem. The threshold handling, exact penalty, nested optimization, and rational feasibility correction are sound. No major mathematical error was found.

Two expositional issues require clarification: the coordinates used for the outer simplex, and the precise statement of the finite-precision optimization theorem. These can be resolved without new mathematics.

Step-by-step verification

1. Normalization and basic properties

The substitutions \(x_t=a_t/\mu_t\), \(b_t=\mu_tp_t\), and \(v_{tj}=\mu_t\lambda_{tj}\) are valid because every support mass is strictly positive. They preserve both coalition payments and the budget equation.

The displayed gradient and Hessian are correct. Nonnegative weights and rates imply that \(F\) is nonnegative, coordinatewise nondecreasing, and concave. Its supporting-hyperplane inequality therefore has the stated direction.

The existence argument is valid. The budget simplex and success-factor interval are compact, every coalition inequality defines a closed subset, and feasibility is nonempty at \(c=0\).

Discarding the specified audience classes is harmless. When no classes remain, \(S=0\), the threshold promise forces \(\eta=0\), and zero payments with \(r=0\) solve the problem.

For retained classes, \(h_j>0\) and \(w_j>0\), so \(0<S<W\) follows.

2. Finite-precision optimization fact

The approximate epigraph separation calculation is correct. The oracle assumptions imply that every \((y,s)\in E\) satisfies

\(g\cdot(y-z)-(s-t)\le t-\ell+2\nu.\)

Thus \(\ell>t+2\nu\) produces a valid strict separator. Otherwise, \(f(z)\le t+3\nu\), so the queried point is within \(3\nu\) of the epigraph. Raising its last coordinate remains compatible with the epigraph’s upper bound because \(f(z)\le M\).

The proposed interior ball is also valid: its domain coordinates stay inside \(D\), and its last coordinate remains strictly above \(M\) and below \(M+1\). The discussion of mixing with an interior point and correcting approximate domain feasibility is consistent with the Lipschitz assumption.

The cited separation-to-optimization implication is supported by GLS Section 4.2, specifically Theorem 4.2.2 together with the weak-optimization consequence described in Remark 4.2.5. The theorem requires quantitative bounding data, rather than boundedness alone. [GLS, Section 4.2](https://www.zib.de/userpage/groetschel/pubnew/paper/groetschellovaszschrijver1988.pdf)

Minor issue: The opening theorem statement omits these quantitative hypotheses and the precise theorem references. The subsequent epigraph discussion supplies the relevant ingredients, but the write-up should explicitly connect them to the invoked theorem.

Minor issue: The claim that the outer simplex has an interior radius bounded below by an inverse polynomial in \(n\) depends on a normalization that is not stated. In ordinary independent payment coordinates, the radius depends on \(B\). For \(n=2\), the simplex is the interval \([0,B]\), whose largest interior radius is \(B/2\). The allowed inputs permit \(B\) to be arbitrarily small while \(n\) stays fixed.

The outer Lipschitz bound involving \(nB+W\) likewise appears to use normalized simplex coordinates. The prover should specify the coordinates and state the radius, coefficient, and Lipschitz bounds consistently in those coordinates. This is a routine coordinate clarification, not a substantive obstruction.

3. The case \(\eta=0\)

The supporting inequality at the origin gives \(F(x)\le\sum_tG_tx_t\).

Because every coalition is successful when \(\eta=0\), applying feasibility to \(x=se_t\) and taking the stated limit correctly yields \(b_t\ge cG_t\). Summation gives \(c\le S/G\). The proposed allocation attains this bound. Also, \(G>0\) and \(S/G\le1\), as required.

The rational output is valid:

No gap was found in this branch.

4. Threshold decision and near-threshold branch

The distinction between \(d=S-\eta\), which may be numerically delicate, and the positive rational \(D=W-\eta\) is used correctly.

The lower bound

\(T\ge h_{\min}(D-d)\)

is correct. The definitions of \(t_0\) and \(g\) imply that the near-threshold branch satisfies \(T\ge t_0\) and \(d/T\le\delta/4\).

The branch decision is safe. If it selects the general branch, the certified interval width gives \(d>3g/2>g\). Neither branch requires deciding an exact transcendental comparison.

For successful coalitions, the supporting inequality at the grand coalition correctly implies \(\gamma\cdot(\mathbf1-x)\le d\). The ideal allocation therefore establishes \(r^*\le\delta/4\).

The normalization estimate for the approximate gradient is valid, and \(\widetilde T>0\) follows from \(\rho\le t_0/4\) and \(T\ge t_0\). The constants give

\(e+2S\rho/t_0\le\delta/8.\)

The stated payment, budget, and value guarantees follow. No exact positivity test for a transcendental quantity is needed.

5. Exact penalty

The exact-penalty identity is correct.

For an unsuccessful coalition, \(s>0\) and \(S-F(x)=d+s>0\), so the interpolation parameter is well-defined and lies in \((0,1)\). Concavity makes the interpolated coalition successful.

The payment increase is at most \(B\theta\), and \(\theta\le s/g\). Consequently, the penalty \(P=B/g+1\) makes the penalized objective at an unsuccessful coalition no larger than \(M(b,c)\).

The reverse inequality follows directly from successful coalitions. The minimum representation of \(H_{b,c}\) is correct, and both branches are concave because their coefficients of \(F\) are nonnegative.

This section handles successful coalitions satisfying threshold equality as well.

6. Approximate inner and outer oracles

The bound \(\|\nabla F(x)\|_2\le A\) is valid. The stated absolute-value and Lipschitz bounds for \(H_{b,c}\) are sufficient and have polynomial-length descriptions.

Every exponential argument queried at a rational coalition is a nonnegative rational. The prescribed evaluator therefore suffices for approximating both values and gradients. Large rational coefficients require additional precision proportional to their bit lengths, which is compatible with the claimed running time.

Selecting the smaller approximate concave branch yields the stated \(2\nu\) branch-selection error. Gradient approximation contributes a controllable error over the bounded cube.

The outer subgradient argument is also valid. The penalty is fixed over the outer domain, so each fixed-coalition witness is affine in \((b,c)\). An approximately maximizing witness consequently supplies an approximate subgradient of \(M\). The constant-zero branch permits the same construction for \(\max(0,M)\).

Apart from the coordinate clarification identified above, no oracle gap was found.

7. Outer optimization and correction

The correction \(c'=\max(0,c-V/\eta)\) is valid because every successful coalition has \(F(x)\ge\eta>0\). The zero-factor case is covered by nonnegative payments.

The inequality

\(f(b,c)\ge-c_B^*+V/\eta\)

and the identity \(\min f=-c_B^*\) follow correctly.

An \(\epsilon\)-optimal output therefore satisfies \(V\le\epsilon\eta\) and \(c\ge c_B^*-\epsilon\). Reducing the factor by \(\epsilon\), with clipping at zero, removes every coalition violation. This establishes exact coalition feasibility and the stated bounds on \(\widehat c\).

8. Budget comparison and final guarantees

Increasing the budget establishes \(c_B^*\ge c^*\).

Scaling a budget-\(B\) allocation to budget \(S\) reduces any coalition’s payment by at most \(B-S\). Since successful coalitions have profit at least \(\eta\), the stated success-factor reduction restores feasibility. Thus

\(0\le c_B^*-c^*\le e/\eta\le\delta/64.\)

Combining this with the optimization error gives the claimed value approximation. The output budget error is at most \(e\), and the coalition inequality is stronger than required.

Division by the positive rational masses preserves rationality and polynomial output length.

9. Complexity and coverage

The positive rational precision and penalty parameters have polynomial bit length. The proof does not require a lower bound on a nonzero transcendental threshold gap.

The nested optimization calls preserve polynomial running time once the outer coordinates and theorem hypotheses are stated consistently. The argument covers zero profits, zero threshold, positive threshold, inactive types, and threshold equality.

Minimal actionable feedback

Neither clarification requires changing the threshold argument or adding a new mathematical lemma.

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