Answer: —
Theorem 2.2 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateWhen $U_i(\mathbf{x}) = \sum_j u_{ij} f_j(x_j)$ where $\{f_j\}$ satisfy Def.~\ref{def:non-sat}, the Lindahl equilibrium (and therefore a core solution) can be computed as the solution to a convex program.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given \(k\) public projects, budget \(B\), rational type masses \(\mu_t\) over a finite type set \(T\), and non-satiating scalar-separable utilities \(U_t(x)=\sum_j u_{tj}f_j(x_j)\), compute a feasible allocation \(x\) satisfying \(\sum_{t\in T}\mu_t\frac{u_{tj}f'_j(x_j)}{\sum_\ell u_{t\ell}x_\ell f'_\ell(x_\ell)}\le 1/B\) for every project \(j\), with equality whenever \(x_j>0\), and output the resulting allocation as a core outcome against all blocking submasses.
Let \(T\) be a finite set of types with rational masses \(\mu_t\geq0\) summing to \(1\). An allocation is \(x\in\mathbb{R}_{\geq0}^k\) with \(\sum_jx_j\leq B\), and \(U_t(x)=\sum_j u_{tj}f_j(x_j)\), where \(u_{tj}\geq0\) and every \(f_j\) is differentiable, strictly increasing, concave, and has \(x f_j'(x)\) nondecreasing with value \(0\) at \(x=0\).
A blocking submass is \(s\in\mathbb{R}_{\geq0}^T\) with \(s_t\leq\mu_t\): writing \(a=\sum_ts_t\), it blocks \(x\) if some \(y\geq0\) with \(\sum_jy_j\leq aB\) satisfies \(U_t(y)>U_t(x)\) for every \(t\) with \(s_t>0\). A continuous core outcome admits no blocking submass.
Is computing an allocation \(x\) satisfying \(\sum_t\mu_t\frac{u_{tj}f_j'(x_j)}{\sum_\ell u_{t\ell}x_\ell f_\ell'(x_\ell)}\leq1/B\) for every \(j\), with equality when \(x_j>0\), and which is a continuous core outcome, in \(\mathrm{P}\) or NP-hard?
For a finite list of agents with the same non-satiating scalar-separable utilities, the discrete Lindahl equilibrium, hence a core allocation, is computable by convex programming.
No result for the distribution-over-types formulation above is verified here.
The distribution-over-types formulation admits a convex program whose exact optimizers yield the displayed conditions and exclude every positive-mass blocking submass. Rational masses enter directly as weights; expanding them into individual agents is unnecessary.
This establishes a structural extension of the finite-agent convex-programming result. It does not, under the input specification given, establish an unconditional \(\mathrm{P}\) classification: representations of the functions and of exact real outputs are unspecified.
Necessary conventions. Literally, the stated definition allows \(s=0\), which blocks every allocation: choose \(y=0\), and the improvement condition is vacuous. Below, blocking therefore requires \(a>0\).
Also assume \(B>0\), discard zero-mass types from the displayed sums, and assume \(\sum_j u_{tj}>0\) for every remaining type. The last assumption expresses non-satiation and is necessary for the denominators: an all-zero utility vector gives an undefined quotient at every allocation.
Under these explicit conventions, the following result is fully proved.
Proposition. There is a convex minimization problem with \(k\) variables and one weighted logarithmic term per type such that:
The proof also handles flat intervals of \(x f_j'(x)\).
Proof: construction of the scalar convex costs. For each coordinate, replace \(f_j\) beyond \(B\) by its tangent extension:
\( \widetilde f_j(z)=f_j(z)\quad\text{for }0\leq z\leq B,\qquad \widetilde f_j(z)=f_j(B)+f_j'(B)(z-B)\quad\text{for }z>B. \)
This preserves differentiability, concavity and strict increase. It also preserves the assumption that \(z\widetilde f_j'(z)\) is nondecreasing: beyond \(B\), that expression is \(z f_j'(B)\).
The derivative \(f_j'(z)\) is positive at every finite \(z\). Indeed, monotonicity gives a nonnegative derivative; if it vanished anywhere, concavity would force the function to be constant thereafter, contradicting strict increase. Thus, in particular, \(f_j'(B)>0\).
Write \(h_j(z)=z\widetilde f_j'(z)\). This function is continuous and nondecreasing, satisfies \(h_j(0)=0\), is positive for \(z>0\), and tends to infinity. Continuity follows from continuity of the derivative of a differentiable concave function; at the origin, the derivative is interpreted as the finite right derivative.
For \(q>0\), the level set \(h_j^{-1}(\{q\})\) is therefore a nonempty compact interval. Denote its endpoints by
\( \alpha_j(q)=\min\{z:h_j(z)=q\},\qquad \beta_j(q)=\max\{z:h_j(z)=q\}. \)
Define
\( C_j(q)=\int_0^q\frac{\alpha_j(v)}{v}\,dv\quad(q\geq0). \)
The integrand has the finite right limit \(1/f_j'(0)\) at zero. To see this, use
\( \frac{\alpha_j(v)}{v} =\frac{1}{\widetilde f_j'(\alpha_j(v))}, \)
and observe that \(\alpha_j(v)\to0\) as \(v\downarrow0\).
The function \(\alpha_j\) is nondecreasing, while \(\widetilde f_j'\) is nonincreasing. Consequently, the integrand is nondecreasing, so \(C_j\) is convex. Moreover,
\( \frac{q}{f_j'(0)}\leq C_j(q)\leq\frac{q}{f_j'(B)}. \)
We will use its one-sided derivatives:
\( C'_{j,-}(q)=\frac{\alpha_j(q)}q,\qquad C'_{j,+}(q)=\frac{\beta_j(q)}q\quad(q>0),\qquad C'_{j,+}(0)=\frac1{f_j'(0)}. \)
Here is why flat intervals cause precisely this derivative interval. As \(v\uparrow q\), continuity and monotonicity of \(h_j\) imply \(\alpha_j(v)\to\alpha_j(q)\). As \(v\downarrow q\) from above, they imply \(\alpha_j(v)\to\beta_j(q)\). For example, in the second limit, every \(\alpha_j(v)\) exceeds \(\beta_j(q)\); its limiting value lies in the level set at \(q\), so it must equal that level set’s largest element. Taking the corresponding one-sided limits of the integrand gives the asserted derivatives.
Proof: the weighted convex program and existence. For \(q\geq0\), put \(D_t(q)=\sum_j u_{tj}q_j\). Consider
\( \displaystyle \operatorname{maximize}_{q\geq0}\; F(q)=\sum_t\mu_t\log D_t(q)-\frac1B\sum_j C_j(q), \)
with \(F(q)=-\infty\) when some \(D_t(q)=0\). Equivalently, minimize the convex function \(-F\).
All logarithmic arguments are positive when every coordinate of \(q\) is positive, because every type has some positive coefficient. Hence the objective is finite somewhere.
An optimizer exists. To verify boundedness of maximizing sequences, let
\( R=\sum_jq_j,\qquad M=\max_{t,j}u_{tj}>0,\qquad c=\min_j\frac1{f_j'(0)}>0. \)
Whenever \(F(q)\) is finite, \(D_t(q)\leq MR\), and therefore
\( F(q)\leq\log(MR)-\frac cB R. \)
This tends to \(-\infty\) as \(R\to\infty\). Thus a maximizing sequence can be chosen bounded. It has a convergent subsequence. No \(D_t\) can tend to zero along that subsequence: its positive-weight logarithm would tend to \(-\infty\), while all other terms are bounded above, contradicting the finite lower bound on the sequence’s objective values. The limit consequently has all \(D_t>0\), and continuity there proves attainment.
Fix an optimizer \(q^*\), and abbreviate
\( D_t=D_t(q^*),\qquad g_j=\sum_t\mu_t\frac{u_{tj}}{D_t}. \)
These are finite. Coordinatewise optimality and the one-sided derivative formulas imply
\( \frac{\alpha_j(q_j^*)}{q_j^*}\leq B g_j \leq\frac{\beta_j(q_j^*)}{q_j^*}\quad\text{if }q_j^*>0, \)
and
\( B g_j\leq\frac1{f_j'(0)}\quad\text{if }q_j^*=0. \)
For completeness, at a positive coordinate, the derivative of \(F\) from the left must be nonnegative and its derivative from the right nonpositive. At a zero coordinate, its right derivative must be nonpositive. Substitution gives exactly these inequalities.
Proof: recovering the allocation. Define
\( x_j=Bq_j^*g_j. \)
If \(q_j^*>0\), the preceding inequalities give
\( \alpha_j(q_j^*)\leq x_j\leq\beta_j(q_j^*), \)
so \(h_j(x_j)=q_j^*\). If \(q_j^*=0\), then \(x_j=0\), and the same identity holds.
The recovered allocation spends exactly the available budget:
\( \displaystyle \sum_jx_j =B\sum_jq_j^*\sum_t\mu_t\frac{u_{tj}}{D_t} =B\sum_t\mu_t\frac{\sum_j u_{tj}q_j^*}{D_t} =B. \)
In particular, every \(x_j\leq B\), so the tangent extensions agree with the original functions at all recovered coordinates. Consequently,
\( q_j^*=x_jf_j'(x_j),\qquad D_t=\sum_j u_{tj}x_jf_j'(x_j)>0. \)
For \(x_j>0\), both \(q_j^*>0\) and \(x_j=Bq_j^*g_j\), hence
\( f_j'(x_j)g_j=\frac{q_j^*}{x_j}g_j=\frac1B. \)
For \(x_j=0\), necessarily \(q_j^*=0\), and coordinatewise optimality gives \(f_j'(0)g_j\leq1/B\).
These are exactly the required conditions:
\( \displaystyle \sum_t\mu_t \frac{u_{tj}f_j'(x_j)} {\sum_\ell u_{t\ell}x_\ell f_\ell'(x_\ell)} \leq\frac1B, \)
with equality whenever \(x_j>0\).
Proof: exclusion of arbitrary blocking submasses. This part applies to any feasible allocation satisfying the displayed conditions with positive denominators, independently of how it was obtained.
Define a nonnegative price vector for each type by
\( p_{tj}=\frac{B u_{tj}f_j'(x_j)} {\sum_\ell u_{t\ell}x_\ell f_\ell'(x_\ell)}. \)
Then
\( \sum_jp_{tj}x_j=B\quad\text{for every }t,\qquad \sum_t\mu_tp_{tj}\leq1\quad\text{for every }j. \)
Suppose a positive-mass submass \(s\) blocks through \(y\). Concavity gives, for every participating type,
\( 0<U_t(y)-U_t(x) \leq\sum_j u_{tj}f_j'(x_j)(y_j-x_j). \)
Multiplying by the positive normalization defining \(p_t\), we obtain \(p_t\cdot y>p_t\cdot x=B\). Since \(a=\sum_ts_t>0\),
\( \displaystyle aB <\sum_ts_t(p_t\cdot y) =\sum_jy_j\sum_ts_tp_{tj} \leq\sum_jy_j\sum_t\mu_tp_{tj} \leq\sum_jy_j \leq aB. \)
The first weak inequality uses \(s_t\leq\mu_t\) and nonnegative prices. The contradiction proves the continuous-core assertion. No rationality assumption on the blocking submass was used. This completes the proposition.
What this establishes computationally. The program has \(k\) variables, \(|T|\) logarithmic terms, and \(k\) scalar convex costs. The masses appear only as the coefficients \(\mu_t\). Thus their denominators do not force population expansion. The distribution-over-types issue is resolved at the level of an exact convex formulation and continuous-core certification.
This is consistent with the finite-agent convex-programming result described by [Fain, Goel and Munagala](https://arxiv.org/abs/1610.03474); the weighted formulation and the blocking-submass argument above are proved independently here.
A formal polynomial-time claim still needs more than convexity. The question permits arbitrary differentiable functions and arbitrary real utility coefficients without specifying their finite encoding or oracle access. Nor does it specify an output representation or approximation criterion.
Even simple formulas can require irrational exact allocations. For example, take one type of mass \(1\), coefficients \(u_{11}=u_{12}=1\), budget \(B=4\), and
\( f_1(z)=\log(1+z),\qquad f_2(z)=\sqrt{1+z}. \)
Both satisfy the assumptions, including monotonicity of \(z f_j'(z)\). Any allocation satisfying the requested conditions spends the whole budget: multiply each coordinate condition by \(x_j\) and sum to obtain \(\sum_jx_j/B=1\). Neither boundary allocation satisfies the conditions, because its unused coordinate has the larger marginal utility. Therefore both coordinates are positive and their marginal utilities are equal:
\( \frac1{1+x_1}=\frac1{2\sqrt{1+x_2}},\qquad x_1+x_2=4. \)
Solving gives
\( x_1=-3+2\sqrt7,\qquad x_2=7-2\sqrt7. \)
Thus even rational formula parameters do not make exact rational output possible. This example does not prove hardness; it demonstrates why the computational model must be specified.
The remaining issue is therefore a bit-complexity theorem for a specified representation and accuracy requirement. The weighted convex formulation and its protection against all positive-mass blocking submasses are established.
⟨structured verdict parsed — rendered above⟩
The appropriate status is partial. The conditional convex-programming proposition is correct: under the prover’s explicit conventions, the construction, optimizer recovery, and exclusion of positive-mass blocking submasses are rigorous. No central mathematical error was found.
However, the output does not establish a polynomial-time algorithm or hardness result. It also explicitly changes the task’s literal definition of blocking and restricts its admissible inputs. These are substantive limitations relative to USER_TASK, although the prover acknowledges them accurately.
Step-by-step verification
The observation about the zero submass is correct. For \(s=0\), one has \(a=0\), and \(y=0\) satisfies the budget constraint. There are no participating types, so the universal strict-improvement condition is vacuously true. Thus every allocation is blocked under the definition as written.
Requiring \(a>0\) changes that definition. The subsequent proposition correctly addresses this amended definition; it cannot establish existence of a continuous core outcome under the literal definition.
The other restrictions also matter. The expression \(1/B\) requires \(B>0\), and a positive-mass type with \(u_{tj}=0\) for every \(j\) has a zero denominator at every allocation. Such coefficient vectors are permitted by the formal assumptions in USER_TASK. Removing zero-mass types is harmless for blocking, but interpreting their potentially undefined summands as absent is an explicit convention about the displayed formula.
Assessment: Correct diagnosis and transparent conditional treatment, but a major scope limitation relative to the original task.
For a differentiable, increasing, concave function on the nonnegative half-line, the derivative is nonnegative and nonincreasing. If it vanishes at a finite point, it must vanish thereafter, contradicting strict increase. Thus the claimed positivity is correct.
The tangent extension matches both value and derivative at \(B\), preserves concavity and strict increase, and makes \(z\widetilde f_j'(z)=zf_j'(B)\) beyond \(B\). This agrees at the join and remains nondecreasing.
The finite right derivative at zero is explicitly assumed in the write-up’s interpretation of differentiability. Under that interpretation, the continuity assertions are valid, including at zero.
Assessment: Verified.
The stated properties of \(h_j\) imply that each positive level has a nonempty compact interval as its inverse image. Positivity away from zero ensures \(\alpha_j(v)\to0\) as \(v\downarrow0\).
The identity \(\alpha_j(v)/v=1/\widetilde f_j'(\alpha_j(v))\) is valid. Its right-hand side is nondecreasing in \(v\), and its limit at zero is finite. Consequently, the integral defining \(C_j\) is well-defined and convex.
The bounds follow from \(f_j'(B)\leq\widetilde f_j'(z)\leq f_j'(0)\). The inverse limits from below and above correctly yield the endpoints \(\alpha_j(q)\) and \(\beta_j(q)\), respectively. Hence both one-sided derivative formulas are correct, including when \(h_j\) has flat intervals.
Assessment: Verified; no strict monotonicity of \(h_j\) is being improperly assumed.
After zero-mass types are removed, every logarithmic term has positive weight. Nonzero utility vectors ensure that an everywhere-positive \(q\) gives positive logarithmic arguments, so the objective is finite somewhere.
With \(R=\sum_jq_j\), the bound \(F(q)\leq\log(MR)-cR/B\) correctly uses both \(\sum_t\mu_t=1\) and the lower bound on the scalar costs. Its right-hand side tends to negative infinity as \(R\) grows, which provides the required boundedness of a maximizing sequence with objective values bounded below.
On a bounded sequence, every other logarithmic term is bounded above. Therefore, if any positive-weight logarithmic argument approached zero, the entire objective would approach negative infinity. This excludes such a limit. Continuity at the resulting limit then proves attainment.
Assessment: Verified.
At a positive coordinate, the left derivative of the maximized objective must be nonnegative and its right derivative nonpositive. Substituting the previously established derivatives gives exactly the two claimed bounds on \(Bg_j\).
At a zero coordinate, only the right derivative is relevant, giving \(Bg_j\leq1/f_j'(0)\). Positive denominators ensure that these derivatives of the logarithmic terms are legitimate.
Assessment: Verified. The proof uses direct necessary optimality conditions and does not require an unstated constraint qualification.
The definition \(x_j=Bq_j^*g_j\), together with coordinate optimality, places \(x_j\) in the level interval associated with \(q_j^*\) whenever \(q_j^*>0\). For a zero coordinate, both quantities vanish. Thus \(h_j(x_j)=q_j^*\) holds in every case.
The budget identity is correct: \(\sum_jx_j=B\sum_t\mu_tD_t/D_t=B\). Consequently each \(x_j\leq B\), which justifies replacing the tangent-extended derivatives by the original derivatives.
The resulting denominators are positive. The equality for positive coordinates and inequality for zero coordinates then follow exactly as written.
Assessment: Verified, including unused coordinates and flat intervals.
The personalized prices are finite and nonnegative, satisfy \(p_t\cdot x=B\), and have aggregate coordinate prices at most one.
Concavity gives the asserted supporting-tangent bound on utility differences. Strict improvement therefore implies \(p_t\cdot y>B\) for every participating type. Because the type set is finite and \(a>0\), summing with the weights \(s_t\) preserves strictness.
Each subsequent inequality is justified by nonnegativity, \(s_t\leq\mu_t\), the aggregate price bounds, and the blocking budget. The contradiction is valid for arbitrary real submasses.
Assessment: Verified for the amended blocking definition only.
The variable and term counts are correct, and rational masses enter as weights without population expansion. This establishes a mathematical convex formulation, not a polynomial-time implementation.
The output supplies no finite representation, evaluation guarantees for the scalar costs, optimization precision bounds, or exact-output procedure. It correctly acknowledges these omissions rather than asserting a complexity classification.
The cited [Fain–Goel–Munagala paper](https://arxiv.org/abs/1610.03474) describes polynomial-time Lindahl-equilibrium computation for a broad class of utilities. The present argument does not invoke that result as a proof step, so no unverified application of its hypotheses is needed for the conditional proposition.
Assessment: The structural conclusion is justified; the requested complexity classification remains unresolved.
Both proposed scalar functions satisfy the required assumptions. Their derivatives are positive, and the derivatives of their respective expressions \(zf_j'(z)\) are \(1/(1+z)^2\) and \((z+2)/(4(1+z)^{3/2})\), both positive.
Multiplying the coordinate conditions by \(x_j\) and summing indeed forces total spending \(B\), provided the denominators are positive.
At \((0,4)\), the unused marginal is \(1\), exceeding the used marginal \(1/(2\sqrt5)\). At \((4,0)\), the unused marginal is \(1/2\), exceeding the used marginal \(1/5\). Thus both boundary allocations fail.
The interior equation yields \(x_1^2+6x_1-19=0\), and the feasible solution is exactly the one stated. Both coordinates are positive and irrational.
Assessment: Verified. As the prover explicitly states, this excludes exact rational output in general; it does not establish hardness or exclude other exact representations.
Minimum actionable feedback
No mathematical repair is needed for the conditional structural proposition itself.
⟨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.