Project-Fair and Truthful Mechanisms for Budget Aggregation

The paper has no numbered theorem, lemma, or corollary asserting the complexity of a computational problem: its results concern fairness, monotonicity, and mechanism guarantees. The proposed Continuum-Ladder evaluation is a plausible population extension, but it is newly posed rather than a computational result of this paper. Therefore bit (a) fails under the strict rubric.

The objection that survived

The proposed threshold evaluation is a new wrapper around an analytic fairness theorem and does not supply the missing computational anchor.

What the mirror covers

The proposed mirror covers the Ladder mechanism's underfunding question and can analogously evaluate its overfunding and ℓ1 guarantees, but not the paper's broader questions about truthful-mechanism characterization or optimal phantom systems.

Open questions for a prover

The case FOR (proponent)

The strongest honest positive case is conditional and weak: there is a coherent high-multiplicity mirror of the paper’s Ladder mechanism, but the paper contains no qualifying computational anchor under ChoCo’s rules.

The named results are Proposition 1, Proposition 2, Proposition 3, Corollary 4, Lemma 6, Theorem 7, Theorem 8, Lemma 9, and Corollary 10. They establish fairness bounds, monotonicity, or approximation guarantees. Theorem 7, Theorem 8, Lemma 9, and Corollary 10 are proved in this paper; Proposition 2 uses Caragiannis, Christodoulou, and Protopapas (2022, Theorem 7). None states that a computational problem is in P, NP-hard, FPT, W[1]-hard, or otherwise classifies its complexity. The footnote mentioning a nonlinear program is not a complexity result. Strictly, therefore, the paper has zero admissible anchors and cannot support a full ChoCo case.

The best near-anchor is Theorem 8, proved here: the Ladder mechanism underfunds no project by more than \(\frac12(1-\frac1m)\). A natural population-continuous version would be the following.

Call it Continuum-Ladder Underfunding Evaluation. An instance consists of \(m\) projects, a finite set of complete voter types \(T=\{p^1,\ldots,p^\tau\}\subseteq\Delta(m)\) of rational budget proposals, a rational mass distribution \(\mu\in\Delta(\tau)\), and a rational threshold \(\beta\). Type \(p^r\) means an agent whose ideal budget is exactly that vector; \(\mu_r\) is the fraction of the population of that type. The mean proposal is

\[ \bar p=\sum_{r=1}^{\tau}\mu_r p^r. \]

For \(s\in[0,1]\), replace the finite Ladder phantoms \(f_k(s)=\max(s-k/n,0)\) by a unit continuum of phantom indices \(u\in[0,1]\),

\[ f_u(s)=\max(s-u,0). \]

For each project \(j\), let \(q_j(s)\) be the lower median of the equally weighted mixture of the voter-coordinate distribution \(\sum_r\mu_r\delta_{p^r_j}\) and the phantom-coordinate distribution induced by \(u\mapsto f_u(s)\). Choose the least \(s^\star\) for which \(\sum_j q_j(s^\star)=1\), and output \(q=q(s^\star)\).

The decision question is whether

\[ \max_j\bigl(\bar p_j-q_j\bigr)\le \beta. \]

A solution is the witness \(s^\star\) together with the resulting allocation \(q\). Replacing the one-sided deviation by \(\max_j|q_j-\bar p_j|\) gives the direct project-fairness version; Theorem 7 supplies the corresponding overfunding bound, and Corollary 10 supplies the \(\ell_1\) versions for \(m=3,\ldots,6\).

The regime is plausible when a large participatory-budgeting electorate chooses among a finite menu of standardized budget templates—for example, recurring coalition proposals or institutionally prepared packages. There may be millions of voters but only \(\tau\) distinct complete proposals, with \(n\gg\tau\). This is a genuine population continuization: mass replaces voter counts, while the budget simplex was already continuous in the original paper. For rational \(\mu\), finite profiles with frequencies converging to \(\mu\) give the natural high-multiplicity limit of the paper’s finite Ladder rule.

I would expect this evaluation problem to be Class A for fixed finite support: each coordinate median is determined by sorting finitely many voter values together with the explicit phantom distribution, and the normalization equation is a one-dimensional piecewise-linear search. That expectation is new analysis, however, not a result of the paper.

The central weakness is substantial. In a nonatomic population, one individual has zero influence, so individual strategyproofness becomes vacuous; meaningful coalition or positive-mass strategyproofness is not supplied by the paper. Moreover, the paper never studies computational complexity. Thus this is a credible continuous extension of Theorem 8’s mechanism and fairness question, but not a continuous mirror anchored in the paper’s computational results. Under the strict ChoCo rubric, the correct verdict is therefore “no qualifying anchor,” with the Continuum-Ladder problem as the strongest possible salvage.

The case AGAINST (opponent, writing after the proponent)

The negative case wins at the programme’s first gate: this paper has no computational anchor to mirror. Proposition 1, Proposition 2, Proposition 3, Corollary 4, Lemma 6, Theorems 7 and 8, Lemma 9, and Corollary 10 establish fairness bounds, monotonicity, or approximation guarantees. None classifies an input-output problem, gives an algorithm, or proves hardness. The reference to solving a nonlinear program is incidental and carries no complexity claim. “The Ladder mechanism is optimal” is mechanism-design optimality, not computational complexity.

Theorem 8 is therefore not a qualifying near-anchor. It proves a universal analytic bound for a fixed rule over finite profiles. Replacing voter counts by a distribution over budget-proposal types gives a perfectly intelligible measure-theoretic limit, but it does not turn the theorem into a computational result. The proponent’s “Continuum-Ladder Underfunding Evaluation” is a newly invented threshold wrapper around that limit. One can put a decision question around any rule—whether its fairness loss is at most \(\beta\)—but that does not make it a mirror of a computational result in the paper.

The proposed finite-support version is also the strongest case for the other side, and it still does not rescue the programme. With finitely many proposal types, each coordinate of the continuum Ladder is obtained from an explicitly described atomic distribution and a uniform phantom distribution; normalization is a one-dimensional breakpoint or quantile calculation. This may be a useful implementation or an analytic restatement, but there is no natural population-combinatorial problem whose complexity landscape is being exposed. Passing from underfunding to absolute project fairness, or to the \(\ell_1\) corollaries for three through six projects, changes only which bound is evaluated; it supplies no computational anchor either.

A stronger repair would be to make the task “choose a truthful mechanism, or a phantom system, that minimizes worst-case continuum fairness loss.” That would be a legitimate new research problem, but not a mirror of this paper’s results. It asks for a functional mechanism-design theory over an enlarged strategyproofness domain. In an atomless population, individual deviations have zero effect, so the paper’s individual truthfulness becomes vacuous. Treating an entire positive-mass type as a strategic bloc could restore substantive incentives, but that is a new coalition- or type-strategyproof model with new guarantees, not the paper’s theorem transported across the population axis.

Nor can arbitrary continuous type distributions repair the situation cleanly. Once the distribution is supplied by a density or oracle, the difficulty depends chiefly on its representation and access model; any resulting hardness can be injected through that encoding rather than arising from high-multiplicity social choice. The finite-type model is the natural ChoCo model, and in that model the proposed evaluation is simply too detached from a source computational question.

I would not claim that no meaningful high-multiplicity extension exists. A population voting over a finite menu of standardized budget templates is plausible, and the Ladder bound may have a clean continuum analogue. The honest conclusion is narrower but decisive: this paper may support a continuous axiomatic or analytic follow-up, but it supplies no worthwhile continuous *computational* mirror under ChoCo’s rules. No choice of type space can create the missing computational result without changing the paper’s research question.

The adversarial triple: the proponent anchors on up to three named results; the opponent sees that case and must defeat every anchor; the judge decides which case convinced it. These are the pipeline’s own outputs, generated by tools/triple_run.py — no human edited them. The paper’s own text is not reproduced here beyond the quoted statement above.