Answer: Yes. Every admissible instance satisfies \(R\ge g\) for every fixed tie order, and the guarantee is asymptotically tight with cost satisfaction.
Theorem 2 — class: algorithmic
Given a finite project set \(P\), budget \(b\), project costs \(c(p)\), DNS satisfaction values \(s(p)\), and a finite-support rational distribution \(\lambda\) over approval types \(A\subseteq P\), with \(\sum_A\lambda_A=1\), define welfare by \(W(S)=\sum_{p\in S}s(p)\sum_{A\ni p}\lambda_A\). Each type starts with per-person wallet \(r_A=b\). For project \(p\), its MES price \(\rho\) satisfies \(\sum_{A\ni p}\lambda_A\min(r_A,\rho s(p))=c(p)\); select an affordable project with minimum price and update the approving types’ wallets by their per-person contributions. Complete MES by greedily selecting remaining projects in decreasing order of weighted welfare per cost. Relative to the maximum-welfare feasible integral project set, does this rule always attain ratio at least \(2\sqrt{c_{\min}/b}-(c_{\min}+c_{\max})/b\), and is that guarantee asymptotically tight over continuous societies?
Let \(P\) be a nonempty set of \(m\) indivisible projects, with binary rational budget \(b>0\), costs \(0<c(p)\le b\), and satisfaction values \(s(p)>0\). DNS means that \(c(p)\le c(q)\) implies both \(s(p)\le s(q)\) and \(s(p)/c(p)\ge s(q)/c(q)\).
A society is given by its support: a list of \(\tau\) distinct approval types \(A\subseteq P\), each with positive binary rational mass \(\lambda_A\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible approval types. Let \(L\) be the total input bit length; express any running times in \(m,\tau,L\) and any additional parameters used.
Define \(W(S)=\sum_{p\in S}s(p)\sum_{A\ni p}\lambda_A\), \(\mathrm{OPT}=\max_{S\subseteq P:\,\sum_{p\in S}c(p)\le b}W(S)>0\), \(c_{\min}=\min_p c(p)\), and \(c_{\max}=\max_p c(p)\). Satisfaction values are binary rationals; empty approval types and unsupported projects are allowed.
MES starts with \(S=\varnothing\) and per-person wallets \(r_A=b\). For each unselected project, let \(\rho(p)\) be the least nonnegative solution of \(\sum_{A\ni p}\lambda_A\min\{r_A,\rho(p)s(p)\}=c(p)\), or \(\infty\) if none exists. Repeatedly select a project of minimum finite price and subtract \(\min\{r_A,\rho(p)s(p)\}\) from each approving type's wallet; stop when all prices are infinite.
Complete MES by scanning remaining projects in decreasing order of \(W(\{p\})/c(p)\), adding each project that fits the remaining global budget and continuing past projects that do not fit. Use one arbitrary fixed total order on projects to resolve all ties. Let \(S_M\) be the completed outcome and \(R=W(S_M)/\mathrm{OPT}\).
Write \(g=2\sqrt{c_{\min}/b}-(c_{\min}+c_{\max})/b\). Asymptotic tightness means the existence of a sequence of admissible instances with \(g>0\), \(b/c_{\min}\to\infty\), and \(R/g\to1\); cost satisfaction \(s(p)=c(p)\) suffices for this part.
Does every such continuous society, for every fixed tie order, satisfy \(R\ge g\), and is this guarantee asymptotically tight in the stated sense?
For finite electorates, greedy-completed MES satisfies the same DNS welfare bound, with asymptotic tightness established already for cost satisfaction ([Baychkov, Brill, and Peters](https://arxiv.org/html/2511.20929v1)).
No separate result treating exactly this finite-support rational-mass formulation was located in the literature search.
1. Result and the finite-electorate theorem
Yes. Every instance in the question satisfies \(R\ge g\) for every fixed tie order, and the guarantee is asymptotically tight in the stated sense.
We use the finite-electorate theorem supplied in the question: for positive additive DNS satisfaction, MES completed by welfare-density greedy satisfies
\( \displaystyle \frac{U(S_M)}{\max_{c(T)\le b}U(T)} \ge 2\sqrt{\frac{c_{\min}}b}-\frac{c_{\min}+c_{\max}}b. \)
Here \(U\) denotes total voter satisfaction, and ties may be resolved by any fixed project order. This is [Theorem 2 of Baychkov, Brill, and Peters](https://arxiv.org/html/2511.20929v1#S5).
We prove that this theorem applies exactly to the rational-mass formulation, then give an explicit tightness sequence.
2. Exact reduction to a finite electorate
Write each mass in lowest terms as \(\lambda_A=a_A/d_A\), and let
\( \displaystyle n=\operatorname{lcm}\{d_A:A\text{ is a listed type}\},\qquad n_A=n\lambda_A. \)
Each \(n_A\) is a positive integer, and \(\sum_A n_A=n\). Construct a finite electorate containing \(n_A\) voters with approval set \(A\). Give every voter initial wallet \(b/n\), retain all project costs and satisfaction values, and use the prescribed project order for ties.
We show inductively that the finite and continuous MES executions select exactly the same projects. The inductive invariant is that every voter of type \(A\) has finite wallet
\( \displaystyle u_A=\frac{r_A}{n}. \)
It holds initially. Suppose it holds before a selection. For an unselected project \(p\), the finite electorate’s payment function at price \(\theta\) is
\( \displaystyle \sum_{A\ni p}n_A\min\{u_A,\theta s(p)\} =\sum_{A\ni p}n\lambda_A\min\{r_A/n,\theta s(p)\} =\sum_{A\ni p}\lambda_A\min\{r_A,n\theta s(p)\}. \)
Consequently, its solution set is precisely the continuous solution set scaled by \(1/n\). Thus \(p\) has a finite price in one execution exactly when it does in the other, and their least prices satisfy
\( \displaystyle \rho_{\mathrm{finite}}(p)=\frac{\rho_{\mathrm{continuous}}(p)}n. \)
Scaling every finite price by the same positive factor preserves comparisons and ties. Both executions therefore select the same project. For each approving type, the finite wallet update is
\( \displaystyle u_A-\min\{u_A,\rho_{\mathrm{finite}}(p)s(p)\} =\frac{r_A-\min\{r_A,\rho_{\mathrm{continuous}}(p)s(p)\}}n, \)
which preserves the invariant. Nonapproving wallets remain unchanged. This completes the induction, including simultaneous termination.
For completeness, continuous MES is globally feasible: initially \(\sum_A\lambda_A r_A=b\), and purchasing \(p\) decreases this sum by exactly \(c(p)\). Nonnegative wallets therefore imply \(c(S)\le b\).
For every project set \(T\), finite welfare satisfies
\( \displaystyle U(T)=\sum_{p\in T}s(p)\sum_{A\ni p}n_A=nW(T). \)
Hence the finite and continuous completion densities differ by the common factor \(n\). Their greedy scans, fit decisions, and tie decisions coincide, so their completed outcomes coincide. Their optimal welfare values also differ by \(n\), because their feasible project sets are identical.
All finite-theorem hypotheses hold: the electorate is finite and nonempty; each voter has an approval set; costs and satisfaction are positive; costs do not exceed \(b\); and the given DNS inequalities are unchanged. Empty types become voters who never pay. Unsupported projects have infinite MES price in both executions.
Applying the finite theorem gives
\( \displaystyle R=\frac{W(S_M)}{\mathrm{OPT}} =\frac{U(S_M)}{n\,\mathrm{OPT}} \ge 2\sqrt{\frac{c_{\min}}b}-\frac{c_{\min}+c_{\max}}b=g. \)
If \(g\le0\), the same conclusion also follows directly from nonnegative welfare.
The replication is a proof device: \(n\) can be exponentially large in \(L\), although its binary length is at most \(L+1\). No electorate expansion is needed to define the original execution.
3. Explicit asymptotic tightness
Fix an integer \(a\ge2\), and put \(k=a^2\). Set \(b=k\), and give every project cost and satisfaction \(1\). This is cost satisfaction and satisfies DNS.
Create two disjoint project sets:
These types are distinct, their masses are positive rational numbers, and their total mass is
\( \displaystyle \frac1a+\frac{k-a}{k}=1. \)
The instance has \(m=2a^2-a\) projects and support size \(\tau=a^2-a+1\).
Initially, every project in \(H\) has MES price \(a\): its payment equation is \((1/a)\min\{k,\rho\}=1\). Every project in \(D\) has price \(k\).
After \(j<a\) projects from \(H\) have been purchased, the large type’s wallet is
\( \displaystyle k-ja=a(a-j)\ge a. \)
Thus every remaining \(H\)-project still has price \(a<k\). MES selects exactly \(a\) projects from \(H\), exhausting that type’s wallet. It then selects all \(k-a\) projects from \(D\), each funded by its own type. The total cost is \(k=b\), so completion adds nothing. This description holds for every tie order.
The resulting welfare is
\( \displaystyle W(S_M)=a\cdot\frac1a+(k-a)\cdot\frac1k=2-\frac1a. \)
Each \(H\)-project has welfare \(1/a\), and each \(D\)-project has welfare \(1/k\le1/a\). Any feasible set contains at most \(k\) projects, so its welfare is at most \(k/a=a\). Selecting all of \(H\) attains this value. Therefore
\( \displaystyle \mathrm{OPT}=a,\qquad R_a=\frac2a-\frac1{a^2}. \)
Since \(c_{\min}=c_{\max}=1\),
\( \displaystyle g_a=\frac2a-\frac2{a^2}>0,\qquad \frac{b}{c_{\min}}=a^2\longrightarrow\infty. \)
Finally,
\( \displaystyle \frac{R_a}{g_a}=\frac{2a-1}{2a-2}\longrightarrow1. \)
This proves the required asymptotic tightness with rational masses and cost satisfaction.
⟨structured verdict parsed — rendered above⟩
The prover’s answer is correct and resolves both parts of the task. The rational replication preserves the entire MES execution and its greedy completion, and the explicit sequence satisfies the stated definition of asymptotic tightness. I found no major or minor issues.
The prover states the external theorem precisely enough for its application: positive additive DNS satisfaction, MES followed by welfare-density greedy completion, and the displayed welfare bound.
The cited [Theorem 2 and definitions](https://arxiv.org/html/2511.20929v1#S5) agree with this statement. The paper allows arbitrary approval subsets, initializes individual wallets at \(b/n\), and defines greedy completion by repeatedly selecting a highest-density affordable project. Its voting rules allow multiple outcomes, so the guarantee is not restricted to a particular tie-breaking order.
The task’s fixed-density scan with skipped unaffordable projects implements that greedy rule: once a project fails to fit, it cannot become affordable as the remaining budget decreases.
The theorem is supplied as a premise in USER_TASK; relying on it is legitimate.
Integrality and normalization. For the chosen common denominator \(n\), every \(n_A=n\lambda_A\) is a positive integer. The normalization of the masses gives \(\sum_A n_A=n\). Thus the constructed electorate is finite and nonempty.
Initial invariant. Continuous wallets start at \(b\), and finite wallets start at \(b/n\), so \(u_A=r_A/n\) holds initially.
Payment functions. The displayed identity is correct:
\[
\sum_{A\ni p}n_A\min\{u_A,\theta s(p)\}
=
\sum_{A\ni p}\lambda_A\min\{r_A,n\theta s(p)\}.
\]
It follows by substituting \(n_A=n\lambda_A\) and \(u_A=r_A/n\).
Prices and ties. The substitution \(\rho=n\theta\) is a bijection on nonnegative prices. It preserves solvability and maps least solutions to least solutions. Consequently, all finite prices are the corresponding continuous prices divided by \(n\). Minimum-price comparisons and ties are preserved.
Wallet updates. The displayed update identity is correct and preserves the invariant after every purchase. Voters with the same approval type remain identical because they receive identical updates. Nonapproving wallets do not change.
These facts justify the induction, including identical selected projects and simultaneous termination.
Each continuous purchase reduces \(\sum_A\lambda_A r_A\) by exactly its cost. Since wallets remain nonnegative, the selected set is globally feasible.
For every set \(T\), the identity \(U(T)=nW(T)\) is correct. Therefore:
All relevant theorem hypotheses survive replication. Empty approval types contribute voters who never pay; unsupported projects have no solution to their positive-cost payment equations. Neither case invalidates the argument. The assumption \(\mathrm{OPT}>0\) ensures the welfare ratio is defined.
The resulting application establishes \(R\ge g\). The separate observation for \(g\le0\) is also correct.
The comment on representation size is sound: \(n\) divides the product of the listed denominators, giving binary length at most \(L+1\). The proof makes no running-time claim and does not present replication as an efficient implementation.
Admissibility. For every integer \(a\ge2\), the construction has positive rational masses summing to
\[
\frac1a+\frac{a^2-a}{a^2}=1.
\]
The approval types are distinct. All project costs and satisfaction values equal \(1\), so the budget restriction and DNS conditions hold. The stated counts \(m=2a^2-a\) and \(\tau=a^2-a+1\) are correct.
MES execution. The initial prices \(a\) for \(H\) and \(a^2\) for \(D\) follow from their payment equations. After \(j<a\) purchases from \(H\), its approving type has wallet \(a(a-j)\ge a\), so the remaining \(H\)-projects retain price \(a\). After exactly \(a\) purchases, that wallet is zero. Every \(D\)-project remains independently affordable through its singleton type.
Thus MES purchases exactly the stated projects and spends the entire budget. The argument works for every tie order.
Welfare and optimum. The calculation \(W(S_M)=2-1/a\) is correct. Every feasible set contains at most \(a^2\) projects, each having welfare at most \(1/a\), so its welfare is at most \(a\). All of \(H\) attains that bound. Hence \(\mathrm{OPT}=a\) and \(R_a=2/a-1/a^2\).
Required limit. The calculations
\[
g_a=\frac2a-\frac2{a^2}>0,\qquad
\frac{b}{c_{\min}}=a^2\to\infty,\qquad
\frac{R_a}{g_a}=\frac{2a-1}{2a-2}\to1
\]
are correct. They establish precisely the requested asymptotic tightness.
No additional clarification or repair is needed. The answer establishes a welfare guarantee and its tightness; it does not classify computational complexity.
⟨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.