← back to the atlas

d4-conf-atal-2015-0225 (d4-conf-atal-2015-0225)

Answer: All asserted limits hold, and \(V_j\leq V_\star\) for every identity. Exact computation is polynomial-time solvable, in \(\mathrm{FP}\).

The anchor (named result in the paper)

Theorem 4 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateMechanism 2 satisfies ex-post envy-freeness, ex-post proportionality, Pareto efficiency, and weak false- name-proofness.

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

The continuous mirror question, as graded

Given finitely many types \(T\) with rational masses \(\mu_t>0\) summing to \(1\), rational reference pieces \(r_t\), a focal type \(t^\star\), and finitely many reports \(s_0,\ldots,s_k\), refine the endpoint partition using the population and report reference pieces. For each cell \(I\), let \(\alpha_I=\sum_{t:I\subseteq r_t}\mu_t\). Compute and prove, for every population sequence whose type frequencies converge to \(\mu\), the limits of the aggregate allocation to type \(t\), \(Y_t(I)=\mu_t\lambda(I)/\alpha_I\) when \(I\subseteq r_t\) and \(\alpha_I>0\), and \(0\) otherwise; and the focal user's \(N\)-scaled expected utility from identity \(j\), \(V_j=\lambda(r_{t^\star})^{-1}\sum_{I\subseteq r_{t^\star}\cap r_{s_j}}\lambda(I)/\alpha_I\). Also establish the limiting truthful comparison \(V_j\leq V_\star\) for every reported identity.

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

A society is given by its support: a list of \(\tau\) types \(T\), each with positive binary-rational mass \(\mu_t\), with \(\sum_t\mu_t=1\); \(\tau\) counts supported types, not possible types.
The cake is \([0,1]\). Each reference piece is a finite union of intervals with rational endpoints and positive length; writing \(\lambda\) for length, type \(t\) has utility \(U_t(X)=\lambda(X\cap r_t)/\lambda(r_t)\). Endpoints are immaterial.
The allocation rule partitions the cake at all reported endpoints. On each cell desired by \(q>0\) identities, it cuts \(q\) equal consecutive pieces and assigns them by a uniform random bijection; cells desired by nobody remain unallocated.
Fix \(t^\star\in T\) and reports \(s_0,\ldots,s_k\), each specified by a reference piece. The focal user submits these \(k+1\) identities simultaneously but receives only one identity's allocation, selected before randomization; the truthful alternative submits just \(r_{t^\star}\).
For each \(N\), take \(N\) truthful background agents with types in \(T\), whose counts satisfy \(n_t(N)/N\to\mu_t\). Add the focal identities separately. Let \(G_{t,N}(I)\) be the expected total length allocated to background type \(t\) inside \(I\), and let \(u_{j,N}\) and \(u_{\star,N}\) be the focal user's expected utilities from identity \(j\) and the truthful alternative.
Use the common endpoint refinement of all population pieces and reports, with \(m\) positive-length cells; set \(\alpha_I=\sum_{t:I\subseteq r_t}\mu_t\). Let \(L\) be the total binary input length; state running times in \(m,\tau,k,L\).
Define candidate values \(Y_t(I)=\mu_t\lambda(I)/\alpha_I\) when \(I\subseteq r_t\) and \(\alpha_I>0\), and zero otherwise; define \(V_j=\lambda(r_{t^\star})^{-1}\sum_{I\subseteq r_{t^\star}\cap r_{s_j}}\lambda(I)/\alpha_I\) and \(V_\star=\lambda(r_{t^\star})^{-1}\sum_{I\subseteq r_{t^\star}}\lambda(I)/\alpha_I\).

Do \(G_{t,N}(I)\to Y_t(I)\), \(Nu_{j,N}\to V_j\), \(Nu_{\star,N}\to V_\star\), and \(V_j\leq V_\star\) hold for every such population sequence and every identity?
Is exact computation of these limiting allocations and utilities in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?

For finite populations, this rule satisfies ex-post envy-freeness, ex-post proportionality, Pareto efficiency, and weak false-name-proofness: truthful participation dominates the expected utility obtainable from any single submitted identity. [Finite-agent guarantees](https://ifaamas.csc.liv.ac.uk/Proceedings/aamas2015/aamas/p909.pdf)
No prior result establishing this exact distributional limit was identified in the literature search.

Modeling choices made when packaging the task

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

Result

All four assertions hold for every population sequence satisfying the stated hypotheses. Exact computation of the limiting allocations and utilities is polynomial-time solvable, more precisely in \(\mathrm{FP}\).

The finite mechanism agrees with Mechanism 2 in the [cited paper](https://ifaamas.csc.liv.ac.uk/Proceedings/aamas2015/aamas/p909.pdf). The proof below derives the limits directly from the allocation rule.

1. Expected allocations on a refinement

Let \(\mathcal I\) be the common endpoint refinement, including the cake endpoints. For each cell \(I\in\mathcal I\), define

\(a_t(I)=\mathbf 1_{\{I\subseteq r_t\}},\qquad b_j(I)=\mathbf 1_{\{I\subseteq r_{s_j}\}},\)

\(D_N(I)=\sum_{t\in T}n_t(N)a_t(I),\qquad h(I)=\sum_{j=0}^{k}b_j(I).\)

Containment is understood up to endpoints. Thus \(D_N(I)\) counts background identities desiring \(I\), and \(h(I)\) counts submitted focal identities desiring it.

We first justify using this common refinement even when some of its endpoints are absent from the mechanism’s actual partition.

Expected-density lemma. Suppose an actual mechanism cell \(J\) is desired by \(q>0\) identities. Write its equal consecutive pieces as \(P_1,\ldots,P_q\). For a fixed desiring identity with allocation \(X\), and every measurable \(A\subseteq J\), uniform random assignment gives

\(\mathbb E[\lambda(X\cap A)]=\frac1q\sum_{\ell=1}^{q}\lambda(P_\ell\cap A)=\frac{\lambda(A)}q.\)

Indeed, the identity receives each piece with probability \(1/q\), and the pieces partition \(J\) up to endpoints. An identity not desiring \(J\) receives nothing there.

Every common-refinement cell lies in an actual mechanism cell, and the set of identities desiring it is constant on that actual cell. Consequently, the lemma applies to every \(I\in\mathcal I\). Linearity of expectation requires no independence between cells.

In the scenario with all focal reports, we therefore have

\(G_{t,N}(I)=\frac{n_t(N)a_t(I)\lambda(I)}{D_N(I)+h(I)}\)

whenever the denominator is positive; otherwise \(G_{t,N}(I)=0\).

Set \(\rho=\lambda(r_{t^\star})>0\), and abbreviate \(a_\star(I)=a_{t^\star}(I)\). The same lemma gives the exact identities

\(u_{j,N}=\frac1\rho\sum_{\substack{I\in\mathcal I\\a_\star(I)b_j(I)=1}}\frac{\lambda(I)}{D_N(I)+h(I)},\)

\(u_{\star,N}=\frac1\rho\sum_{\substack{I\in\mathcal I\\a_\star(I)=1}}\frac{\lambda(I)}{D_N(I)+1}.\)

Every denominator in the first sum is positive because \(b_j(I)=1\) implies \(h(I)\geq1\). Every denominator in the second sum is positive because the truthful focal identity desires the cell.

2. Limits of background allocations

For every fixed cell, convergence of the type proportions implies

\(\frac{D_N(I)}N=\sum_{t\in T}\frac{n_t(N)}N a_t(I)\longrightarrow\sum_{t\in T}\mu_ta_t(I)=\alpha_I.\)

If \(\alpha_I>0\), then \(D_N(I)+h(I)>0\) for all sufficiently large \(N\). Since the reports are fixed, \(h(I)/N\to0\). Hence

\(G_{t,N}(I)=\lambda(I)\frac{(n_t(N)/N)a_t(I)}{D_N(I)/N+h(I)/N}\longrightarrow\lambda(I)\frac{\mu_ta_t(I)}{\alpha_I}=Y_t(I).\)

If \(\alpha_I=0\), positivity of every supported mass implies \(a_t(I)=0\) for every \(t\in T\). All background agents have types in \(T\), so none desires this cell for any \(N\). Therefore

\(G_{t,N}(I)=0=Y_t(I)\)

for every \(N\).

This proves the asserted background-allocation limit on every cell, including unsupported cells.

3. Limits of focal utilities and truthful dominance

Every cell contained in the focal user’s true piece satisfies

\(\alpha_I=\sum_{t\in T}\mu_ta_t(I)\geq\mu_{t^\star}>0.\)

This verifies that all denominators defining \(V_j\) and \(V_\star\) are strictly positive, even if reports also cover unsupported regions.

For every cell contributing to \(u_{j,N}\),

\(\frac{N}{D_N(I)+h(I)}=\frac1{D_N(I)/N+h(I)/N}\longrightarrow\frac1{\alpha_I}.\)

The refinement has finitely many cells, so taking limits term by term yields

\(Nu_{j,N}\longrightarrow\frac1\rho\sum_{\substack{I\in\mathcal I\\a_\star(I)b_j(I)=1}}\frac{\lambda(I)}{\alpha_I}=V_j.\)

Likewise,

\(\frac{N}{D_N(I)+1}=\frac1{D_N(I)/N+1/N}\longrightarrow\frac1{\alpha_I}\)

on every true-piece cell. Thus

\(Nu_{\star,N}\longrightarrow\frac1\rho\sum_{\substack{I\in\mathcal I\\a_\star(I)=1}}\frac{\lambda(I)}{\alpha_I}=V_\star.\)

Finally,

\(V_\star-V_j=\frac1\rho\sum_{\substack{I\in\mathcal I\\a_\star(I)=1,\ b_j(I)=0}}\frac{\lambda(I)}{\alpha_I}\geq0.\)

Every summand is positive. Consequently, \(V_j=V_\star\) exactly when the report covers the entire true piece up to a set of length zero.

The exact finite formulas also establish finite expected dominance directly: on a cell contributing to \(u_{j,N}\), we have \(h(I)\geq1\), and therefore

\(\frac{\lambda(I)}{D_N(I)+h(I)}\leq\frac{\lambda(I)}{D_N(I)+1}.\)

Summing these inequalities, and adding the nonnegative truthful contributions from omitted cells, gives \(u_{j,N}\leq u_{\star,N}\).

4. Exact computation and bit complexity

We compute the entire table of \(m\tau\) values \(Y_t(I)\), together with \(V_0,\ldots,V_k,V_\star\).

Constructing the refinement

Sort all input endpoints together with the cake endpoints, merge equal endpoints, and form consecutive positive-length cells.

A sweep through endpoint events determines the membership indicators for every type and report on every cell. If a reference piece contains overlapping listed intervals, maintain an active-interval count for that piece; its membership indicator is one exactly when this count is positive. Apply all events at a shared endpoint together.

There are \(O(L)\) interval endpoints in the explicit input. Sorting, sweeping, and recording memberships use

\(O\!\left(L\log(L+1)+m(\tau+k+1)\right)\)

comparisons and elementary arithmetic operations. In particular, we enumerate supported types and actual cells, rather than possible type patterns.

A common-denominator construction

Let \(Q\) be the product of all input endpoint denominators, and let \(M\) be the product of all input mass denominators. Both integers have \(O(L)\) bits.

Because every endpoint denominator divides \(Q\), each cell length has the form

\(\lambda(I)=d_I/Q,\qquad 1\leq d_I\leq Q.\)

Likewise write

\(\mu_t=p_t/M,\qquad p_t\in\mathbb Z_{>0}.\)

The mass normalization gives \(\sum_t p_t=M\). Define

\(A_I=\sum_{t\in T}p_ta_t(I),\qquad R=\sum_{\substack{I\in\mathcal I\\a_\star(I)=1}}d_I.\)

Then

\(\alpha_I=A_I/M,\qquad \rho=R/Q,\qquad 1\leq R\leq Q,\)

and \(0\leq A_I\leq M\). Hence, when \(a_t(I)=1\),

\(Y_t(I)=\frac{p_td_I}{QA_I}.\)

All remaining table entries are zero.

To compute the utilities without uncontrolled growth from repeated fraction addition, form

\(H=\prod_{\substack{I\in\mathcal I\\A_I>0}}A_I.\)

For each submitted identity and for the truthful alternative, compute the integers

\(E_j=\sum_{\substack{I\in\mathcal I\\a_\star(I)b_j(I)=1}}d_I(H/A_I),\)

\(E_\star=\sum_{\substack{I\in\mathcal I\\a_\star(I)=1}}d_I(H/A_I).\)

The divisions are exact, and their denominators are positive by Section 3. The outputs are then

\(V_j=\frac{ME_j}{RH},\qquad V_\star=\frac{ME_\star}{RH}.\)

These expressions are exactly the required sums.

Running time

Each factor \(A_I\) has \(O(L)\) bits, so \(H\) has \(O(mL)\) bits. Moreover,

\(0\leq E_j,E_\star\leq mQH.\)

Thus all constructed integers, intermediate values, and output numerators and denominators have \(O(mL)\) bits. Reducing the output fractions cannot increase their size.

Including construction and optional reduction of every output fraction, the number of arithmetic operations is

\(O\!\left(L\log(L+1)+m(\tau+k+1)\right).\)

For an explicit conservative bit bound, arithmetic and fraction reduction on integers of at most \(B\) bits can be performed in \(O(B^3)\) bit operations using schoolbook arithmetic and Euclid’s algorithm. Taking \(B=O(mL)\) yields

\(O\!\left(\bigl[L\log(L+1)+m(\tau+k+1)\bigr](mL)^3\right)\)

bit operations.

The explicit endpoint representation implies \(m=O(L)\), while \(\tau\) and \(k+1\) are also \(O(L)\). Therefore this is a polynomial bound in the total input length.

5. Conclusion

All stated limits and the inequality \(V_j\leq V_\star\) are proved for every allowed population sequence and every fixed submitted identity. The limiting values are rational and exactly computable in polynomial time.

⟨structured verdict parsed — rendered above⟩

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

The target is resolved in substance: all asserted limits and inequalities follow, and the exact computation has a valid polynomial bit-complexity bound. There are two minor presentation issues, neither of which affects those conclusions.

On an actual cell desired by \(q>0\) identities, a fixed desiring identity receives each consecutive piece with probability \(1/q\). The displayed expectation therefore holds for every measurable subset of that cell, including a smaller common-refinement cell.

The common refinement includes every endpoint used in either focal scenario. Its cells consequently lie within actual mechanism cells, up to immaterial endpoints. Missing background types and additional report endpoints cause no difficulty. Independence between cells is unnecessary for the expectations used here.

The denominator \(D_N(I)+h(I)\) counts precisely the identities desiring the cell in the simultaneous-report scenario. Multiplying the individual expected length by \(n_t(N)a_t(I)\) correctly gives \(G_{t,N}(I)\).

The formula for \(u_{j,N}\) includes exactly the cells both desired by identity \(j\) and valued by the focal user. Its denominators are positive because \(h(I)\geq1\) there. The truthful formula correctly replaces all focal reports with one truthful identity, giving denominator \(D_N(I)+1\) on true-piece cells.

The finite sum defining \(D_N(I)/N\) converges to \(\alpha_I\). When \(\alpha_I>0\), the denominator is eventually positive, and the quotient limit is justified.

When \(\alpha_I=0\), positivity of every supported mass forces every background membership indicator on that cell to vanish. Thus \(G_{t,N}(I)\) is identically zero, rather than merely converging to zero. This correctly handles cells desired only by focal reports and cells desired by nobody.

Every true-piece cell satisfies \(\alpha_I\geq\mu_{t^\star}>0\). Consequently, all candidate utility denominators are defined, including when reports also cover unsupported regions.

The reports and refinement are fixed as \(N\) varies. Hence \(h(I)/N\to0\), and both displayed reciprocal limits are valid. Passing the limit through each finite sum requires no further uniformity assumption. The argument applies to every allowed population sequence and every submitted identity.

The displayed difference \(V_\star-V_j\) consists exactly of the omitted true-piece cells. Every included term has positive length and positive denominator, so the difference is nonnegative.

Because membership is constant on refinement cells, equality holds precisely when the report omits no positive-length portion of the true piece. This verifies the stated characterization up to sets of length zero.

The additional finite inequality \(u_{j,N}\leq u_{\star,N}\) also follows from the written cellwise comparison and the nonnegative contributions from omitted cells.

Products of the explicitly encoded endpoint and mass denominators have \(O(L)\) bits. The definitions of \(d_I,p_t,A_I,R\) and their stated bounds are consistent with the normalized masses and positive true-piece length.

Substitution verifies both output formulas:
\(Y_t(I)=p_td_I/(QA_I)\) on desired cells and \(V_j=ME_j/(RH)\). No division by zero occurs: a desired background cell has \(A_I>0\), and every utility summand lies in the true piece.

Every division \(H/A_I\) is exact. The bounds on \(H\) and the \(E\)-values ensure that intermediate integers and output fractions have \(O(mL)\) bits. Thus the construction controls output size as well as arithmetic size.

Endpoint sorting and the membership sweep have the stated operation bound. Explicit membership recording accounts for the dependence on \(m,\tau,k\). The representation gives \(m,\tau,k+1=O(L)\).

The conservative \(O(B^3)\) cost per arithmetic operation or complete fraction reduction suffices for the stated final bit bound. Therefore the claimed membership in \(\mathrm{FP}\) is established.

Minor issue: The sentence claiming the same number of “arithmetic operations” *including optional fraction reductions* is imprecise. A complete Euclidean greatest-common-divisor computation can require multiple elementary divisions; it is not generally one elementary arithmetic operation.

Minimum clarification: State whether the operation count treats a complete fraction reduction as a separate procedure call, or give the arithmetic-operation count before reduction and count reduction calls separately. The existing bit-complexity conclusion survives this clarification.

The paper’s Mechanism 2 uses a *minimal valid partition*, whereas the task explicitly partitions at all reported endpoints. These coincide when the reported endpoints are precisely membership-change boundaries. They need not coincide for redundant interval descriptions. [Definition 7 and Mechanism 2](https://ifaamas.csc.liv.ac.uk/Proceedings/aamas2015/aamas/p909.pdf)

For example, let two identities both desire the entire cake, with one reporting it as \([0,1/2]\cup[1/2,1]\). The task’s rule partitions at \(1/2\) and gives each identity length \(1/4\) in each half. The paper’s minimal partition has one cell, so each identity receives one entire half. Their allocation distributions differ.

Minor issue: “The finite mechanism agrees with Mechanism 2” is therefore too broad if it asserts identical allocation distributions for every permitted interval encoding.

Minimum clarification: Qualify the identification by the partition convention or restrict it to the expected quantities used here. The supplied expected-density lemma already makes the target proof independent of this identification.

No additional lemma or substantive mathematical argument is needed to establish the requested results.

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