← back to the atlas

Deterministic, Strategyproof, and Fair Cake Cutting (d4-conf-ijcai-2017-0805)

Answer: —

The anchor (named result in the paper)

Theorem 8 — class: algorithmic

The continuous mirror question, as graded

Given a finite support \(T\) of complete piecewise-constant valuation types, a rational mass vector \(\mu\in\Delta(T)\), and normalized per-capita cake supply, define the weighted-quantile and middle-piece recursion of Algorithm 3 together with a report-indexed allocation kernel and deterministic implementations on sufficiently large \(q\)-replicas; compute the allocation and the smallest uniform \(\epsilon\) such that every present type receives value at least \(1/n\) and no single representative gains more than \(\epsilon\) by misreporting.

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

A society is given by its support: a list \(T\) of \(\tau\) types with positive binary-rational masses \(\mu_t\), where \(\sum_t\mu_t=1\); \(\tau\) is the support size, not the number of possible types. Each type is a nonnegative piecewise-constant density on \([0,1]\), with rational breakpoints and heights and total value \(1\); let \(m\) count the common elementary intervals and \(L\) be the input bit length.
Fix an integer \(n\geq2\). A compatible \(q\)-replica has \(N=nq\) representatives, \(N\mu_t\) of each type, and cake supply \(q\) copies of \([0,1]\). Run the following rule on one copy and give each representative the same resulting piece in every copy, so utility is \(qV_t(A_i)\) and proportionality means utility at least \(1/n\).
Representatives have fixed identities, ordered first by input type index and then within type; reports never change identities. On an interval \([a,b]\) with \(k>1\) representatives, each reports its leftmost cut worth \(\lfloor k/2\rfloor/k\) of its reported interval value. Sort cuts by coordinate and then identity, and assign the first \(h=\lfloor k/2\rfloor\) representatives to the left group and the remainder to the right group.
The modified recursion allocates \([d_h,d_{h+1}]\) among all \(k\) representatives using the ordinary recursion, and recurses on \([a,d_h]\) with the left group and \([d_{h+1},b]\) with the right group. The ordinary recursion instead recurses on \([a,d_h]\) and \([d_h,b]\) with these groups. Both return the entire interval when \(k=1\); a zero-value cut is \(a\), and endpoints have no utility.
For any normalized nonnegative rational piecewise-constant report \(r\), let \(A_i^q(r)\) be the piece obtained after replacing only representative \(i\)'s report by \(r\). Its report-indexed per-capita allocation measure is \(K_i^q(r)(B)=q|A_i^q(r)\cap B|\). Define the truthful type-average measure \(\overline K_t^q=(N\mu_t)^{-1}\sum_{i:t(i)=t}K_i^q(v_t)\), and define the continuous type allocation as its weak limit along compatible \(q\), when that limit exists.
Given a binary integer \(q_0\geq1\), define the smallest uniform incentive loss by \(\epsilon^*=\sup_{q\geq q_0:\,N\mu_t\in\mathbb Z\ \forall t}\sup_i\sup_r\max\{0,q[V_{t(i)}(A_i^q(r))-V_{t(i)}(A_i^q(v_{t(i)}))]\}\). Reports may introduce arbitrarily many breakpoints; all other representatives report truthfully.
Does the continuous type allocation always exist, and can it be computed together with the decision \(\epsilon^*\leq e\) in polynomial time, or is that decision NP-hard?
Here \(e\geq0\) is a binary rational; computation of the limiting allocation means evaluating its mass on a queried rational interval to additive error \(\delta>0\). State running times in \(m,\tau,L,n,\log q_0\), and \(\log(1/\delta)\), without expanding the replicas.
For finite populations, the modified recursion is deterministic and proportional and has incentive-loss bound \(1-3/(2N)\) for even \(N\), and \(1-3/(2N)+1/(2N^2)\) for odd \(N\). [Menon–Larson](https://arxiv.org/pdf/1705.06306) proves these bounds; it does not compute the smallest instance-specific loss or establish the replica limits. No result settling this precise continuous problem was located.

Modeling choices made when packaging the task

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

Partial results: exact allocation limits and finite-replica incentive certificates

The allocation component is completely resolved under the interpretation that binary-rational masses are dyadic rationals. The truthful type-average measures are then independent of the compatible replica size, and their interval masses can be computed exactly in polynomial time.

The new incentive result proved below is that, for any fixed compatible replica size given in binary, a violation of a rational incentive threshold has a report witness of polynomial bit length. Such a witness can also be verified in polynomial time without expanding the population. This strengthens the report-compression result in the notes by controlling report-parameter bit lengths.

The general decision whether $\epsilon^*\leq e$ remains unresolved: the finite-replica certificate theorem does not bound the replica size needed to witness a violation.

1. Definitions and interpretation

Write $\lambda$ for Lebesgue measure and
$$ V_t(B)=\int_B v_t(x)\,dx $$
for the true valuation of type $t$. Endpoints have zero measure and zero utility.

For a fixed compatible $q$, define
$$ \epsilon_q = \sup_i\sup_r \max\!\left\{ 0,\, q\left[V_{t(i)}(A_i^q(r))-V_{t(i)}(A_i^q(v_{t(i)}))\right] \right\}. $$
Thus
$$ \epsilon^*=\sup_{\substack{q\geq q_0\\q\text{ compatible}}}\epsilon_q. $$

For the allocation theorem, interpret a binary-rational mass as
$$ \mu_t=\frac{a_t}{2^S} $$
with integer $a_t>0$. If “binary-rational” instead means an arbitrary rational encoded in binary, the allocation theorem below establishes only the dyadic subclass. The finite-replica incentive theorem does not require dyadic masses.

Let $L_I$ denote the encoding length of the queried interval endpoints. For incentive computations, let $E$ denote the encoding length of $e$. These lengths must be included in any running-time bound if they are not already included in $L$.

2. Partition and proportionality properties

These properties are used below, so they are proved here.

Lemma 1. Both recursions partition their input interval, up to endpoints. Each representative in a call on $[a,b]$ with $k$ representatives receives reported value at least $1/k$ of its reported value of $[a,b]$.

Proof. Both statements follow by induction on $k$.

For $k=1$, the representative receives the entire interval.

For $k>1$, put
$$ h=\left\lfloor\frac{k}{2}\right\rfloor. $$
The ordinary recursion partitions $[a,b]$ into $[a,d_h]$ and $[d_h,b]$. The modified recursion partitions it into
$$ [a,d_h],\qquad[d_h,d_{h+1}],\qquad[d_{h+1},b], $$
and applies a partitioning recursion to each interval.

For proportionality, let $R$ be a representative’s reported valuation. Its cut $c$ satisfies
$$ R([a,c])=\frac{h}{k}R([a,b]). $$
This equation also holds when the interval value is zero, because then $c=a$.

If the representative belongs to the left group, then $c\leq d_h$, hence
$$ R([a,d_h])\geq\frac{h}{k}R([a,b]). $$
Induction on the left child, which has $h$ representatives, gives value at least
$$ \frac{R([a,d_h])}{h}\geq\frac{R([a,b])}{k}. $$

For a right-group representative in the ordinary recursion, $d_h\leq c$, so
$$ R([d_h,b])\geq\frac{k-h}{k}R([a,b]). $$
The corresponding induction gives the same guarantee.

In the modified recursion, every right-group representative has $d_{h+1}\leq c$. Applying the same argument to $[d_{h+1},b]$ proves its guarantee. The middle allocation adds nonnegative value. $\square$

This directly proves the proportionality property stated for the modified rule in [Menon–Larson](https://arxiv.org/pdf/1705.06306). The instance-specific incentive results below do not use their worst-case incentive bound.

3. Exact truthful allocation invariance for dyadic masses

For truthful reporting, let
$$ U_t^q=\bigcup_{i:t(i)=t}A_i^q(v_t) $$
be the aggregate region allocated to type $t$.

By Lemma 1, individual pieces have disjoint interiors. Therefore, for every Borel set $B$,
$$ \overline K_t^q(B) = \frac{q}{N\mu_t}\lambda(U_t^q\cap B) = \frac{1}{n\mu_t}\lambda(U_t^q\cap B). $$

Lemma 2. In computing aggregate truthful regions, a recursive call containing only one type can be replaced by assigning its entire interval to that type.

Proof. Every descendant contains only that type, and Lemma 1 says that the descendants partition the input interval. Thus their aggregate region is the entire interval, up to endpoints. This remains true when its valuation is zero. $\square$

At every other truthful call, all representatives of one type have the same cut. Sorting by cut and identity consequently gives consecutive type blocks. The split can be computed from their counts, without listing representatives.

Theorem 3. Suppose all masses are dyadic. There are finite unions of rational intervals $W_t$, independent of compatible $q$, such that
$$ \overline K_t^q(B)=\frac{1}{n\mu_t}\lambda(W_t\cap B) $$
for every compatible $q$ and every Borel set $B$. In particular, the continuous type allocation exists.

Proof. Choose the smallest common dyadic denominator
$$ D=2^S,\qquad \mu_t=\frac{a_t}{D},\qquad \sum_t a_t=D. $$
If $D>1$, minimality implies that some $a_t$ is odd. Compatibility then implies
$$ D\mid N. $$
Indeed, integrality of $Na_t/D$, together with $\gcd(a_t,D)=1$, implies this divisibility.

Every compatible population therefore has
$$ N=Db,\qquad N\mu_t=ba_t $$
for an integer $b>0$. If $D=1$, positivity of the masses implies that there is only one type, and Lemma 2 already proves the theorem.

Run an auxiliary truthful population with $D$ representatives and $a_t$ representatives of type $t$. This auxiliary population is used only to define the aggregate regions; it need not itself be a compatible replica.

Compare its compressed execution with that of a compatible population. At corresponding calls, maintain:

These statements hold at the root. A call containing several types has auxiliary size
$$ g=2^j,\qquad j\geq1. $$
Its actual size is $bg$. Both sizes are even, so both calls request cuts at exactly half the reported interval value. Identical intervals and valuations imply identical type cuts, including the leftmost-cut convention.

Let the auxiliary blocks in sorted order have sizes
$$ c_1,c_2,\ldots. $$
The actual block sizes are $bc_1,bc_2,\ldots$, and the median ranks are respectively $g/2$ and $bg/2$.

If the auxiliary median rank ends a block, the actual median rank ends the corresponding block. Thus both median boundary coordinates coincide. If it lies strictly inside a block, scaling preserves that fact, and both adjacent median coordinates equal that block’s common cut in both populations.

Consequently, the two exterior intervals coincide and their type-count vectors remain scaled by $b$. Each auxiliary exterior child has size $g/2$. The middle ordinary call has auxiliary size $g$, and its children also have size $g/2$. Thus the same comparison applies throughout both recursion modes.

Whenever a call contains one type, Lemma 2 assigns the same interval to that type in both executions. Every group split halves the auxiliary size, so the comparison terminates after at most $S$ group splits along any path.

Let $W_t$ be the aggregate region recorded for type $t$ by the auxiliary execution. All its endpoints are rational, because cuts of rational piecewise-constant densities on rational intervals are rational. The comparison proves
$$ \lambda(U_t^q\mathbin{\triangle}W_t)=0. $$
Substituting this equality into the formula for $\overline K_t^q$ proves the result. The measures are identical for all compatible $q$, hence converge weakly to that same measure. $\square$

The argument includes zero densities, flat cumulative valuations, and coincident cuts: corresponding calls use exactly the same leftmost cuts and identity order.

4. Polynomial-time allocation computation

The auxiliary population has $2^S$ representatives, but it can be processed using binary type counts.

For a nonempty group containing $r$ types, define its potential to be $r-1$. At a group split, at most one type block is split between the children. If the children contain $r_L$ and $r_R$ types, then
$$ r_L+r_R\leq r+1, $$
and therefore
$$ (r_L-1)+(r_R-1)\leq r-1. $$

For the modified exterior recursion, the total potential at any depth is consequently at most $\tau-1$. Every call containing several types has potential at least one. There are thus at most $\tau-1$ such calls at each depth and at most $(\tau-1)S$ overall.

Each of those calls starts one middle ordinary recursion. Applying the same potential argument separately to every such recursion gives the conservative total call bound
$$ R=O\!\left(1+\tau^2(S+1)^2\right), $$
including terminal calls. This also bounds the number of recorded interval pieces.

Each call needs
$$ O\!\left(m\tau+\tau\log(\tau+1)\right) $$
rational operations: compute type cuts, sort the type blocks, and split their counts.

Here is a bit-length justification. On each common elementary interval, a cumulative valuation has the form
$$ F_t(x)=h_{tj}x+\beta_{tj}. $$
For a positive-value half cut lying in an interval with positive height,
$$ c= \frac{(F_t(a)+F_t(b))/2-\beta_{tj}}{h_{tj}}. $$
Thus each cut is an affine rational expression in its parent endpoints. Zero-value cuts are existing endpoints.

There is an integer $H$ with
$$ \log H=O(L) $$
such that all denominators of these affine coefficients divide $H$. To obtain one, take a sufficiently large fixed power of the product of the input denominators, positive-height numerators, and $2$. Cumulative-value coefficients introduce no additional prime factors.

An endpoint produced at affine-operation depth $d$ therefore has denominator dividing $H^d$. Since it lies in $[0,1]$, its numerator and denominator have bit length $O(L(d+1))$. In this execution, $d\leq S+1$: a path can follow exterior recursion and then enter one middle ordinary recursion, but cannot subsequently enter another middle recursion.

For a queried rational interval $I$, compute
$$ \overline K_t(I) = \frac{1}{n\mu_t} \sum_{\substack{J\text{ recorded}\\\text{for type }t}} \lambda(J\cap I). $$
Recorded intervals have disjoint interiors, so the sum has no positive-measure multiplicity.

Put
$$ p=\max\!\left\{0,\left\lceil\log_2(1/\delta)\right\rceil\right\}. $$
A conservative bit-operation bound is
$$ O\!\left( R\bigl(m\tau+\tau\log(\tau+1)\bigr) \bigl(L(S+1)+L_I+\log(n+1)+p+1\bigr)^3 +\log(q_0+1) \right). $$
Here rational numbers are reduced during arithmetic; their denominators divide the common powers described above, together with the queried endpoint denominators and the final normalization denominator.

Under an explicit binary rational encoding, $S\leq L$. The bound is therefore polynomial in the requested parameters and the query encoding length. The answer can be returned exactly or rounded to additive error $\delta$.

5. New result: polynomial-bit incentive witnesses at fixed replica size

Theorem 4. Fix a compatible $q$ given in binary. If
$$ \epsilon_q>e, $$
then some representative has a permitted rational report whose total encoding length is polynomial in
$$ m,\ \tau,\ L,\ \log(nq),\ E $$
and whose gain is strictly greater than $e$.

Such a report can be verified in polynomial time without expanding the representatives. Hence the fixed-replica predicate $\epsilon_q>e$ belongs to $\mathrm{NP}$, and $\epsilon_q\leq e$ belongs to $\mathrm{coNP}$.

This theorem applies to arbitrary rational masses.

5.1. The relevant execution has few queries

Distinguish the deviator from all truthful representatives. Follow its modified exterior path. At every nonterminal modified call, also follow its single path through that call’s middle ordinary recursion.

Put
$$ N=nq,\qquad d=\lceil\log_2 N\rceil. $$
The exterior path has at most $d$ nonterminal calls. At exterior depth $j$, its population size is at most
$$ \left\lceil\frac{N}{2^j}\right\rceil, $$
so the corresponding middle ordinary path has at most $d-j$ nonterminal calls. The number $Q$ of deviator cut queries is therefore at most
$$ Q\leq d+\sum_{j=0}^{d-1}(d-j) =\frac{d(d+3)}2. $$

The deviator’s final piece is a union of at most $d+1$ intervals: one ordinary terminal interval from each middle recursion and one exterior terminal interval.

Only these paths affect its allocation. Other branches contain no deviator and cannot affect these paths.

5.2. Compressed simulation preserves identities

At a relevant call, store the truthful count of each type. For the deviator’s true type, additionally distinguish truthful identities before and after the deviator. Initially these counts are its within-type ordinal minus one and the number of identities following it.

All truthful representatives of one type have a common cut. Sort these blocks and the deviator by coordinate and identity. If the deviator ties its true type’s cut, its earlier and later identity blocks lie on the stipulated sides of it. A split at rank $h$ requires only subtraction of binary counts, and updates the earlier and later counts directly.

This representation therefore reproduces exact group membership and both boundary cuts. It stores $O(\tau)$ counts per call, each using $O(\log N)$ bits.

Given a report with $J$ elementary intervals, its cuts can be computed by scanning those intervals. Since there are $O(d^2)$ relevant calls, verification uses polynomially many rational operations in
$$ m,\ \tau,\ J,\ L,\ d $$
and the report’s encoding length.

The same procedure computes the distinguished representative’s truthful baseline allocation.

5.3. A guessed execution is a rational linear system

Fix a deviator and guess the discrete data of its relevant execution:

There are
$$ P=O\!\left((\tau+1)(d+1)^2\right) $$
coordinate and cumulative-value variables. For a fixed guess, every condition below is linear.

For a truthful type $s$ at a call with population size $k$, write
$$ \alpha=\frac{\lfloor k/2\rfloor}{k}. $$
Its cut satisfies
$$ F_s(c_s)-F_s(a) = \alpha\bigl(F_s(b)-F_s(a)\bigr). $$
Once elementary intervals containing the coordinates have been guessed, every occurrence of $F_s$ is an affine function.

Leftmostness is also expressible linearly. If
$$ F_s(b)=F_s(a), $$
require $c_s=a$. Otherwise, require positive interval value and choose a positive-height elementary interval $[\ell,u]$ with
$$ \ell<c_s\leq u,\qquad a<c_s, $$
together with the cut equation.

These conditions are sufficient: the cumulative value strictly increases immediately before $c_s$, so no earlier point can reach the target. They are necessary: a positive leftmost target cut cannot have a zero-height interval immediately to its left, because that would provide an earlier point attaining the target.

For the deviator, collect $0,1$ and every queried coordinate $a,b,c$. Guess their equality pattern and order, and write their distinct coordinates as
$$ 0=x_0<x_1<\cdots<x_J=1. $$
Introduce variables $z_j$ for reported cumulative values, imposing
$$ 0=z_0\leq z_1\leq\cdots\leq z_J=1. $$

Every deviator query imposes
$$ R(c)-R(a)=\alpha\bigl(R(b)-R(a)\bigr), $$
where $R$ at a collected point means its corresponding $z$ variable.

If $R(b)=R(a)$, require $c=a$. Otherwise, require $R(b)>R(a)$ and, for the collected point $x_\ell$ immediately preceding $c$, impose
$$ R(x_\ell)<R(c). $$
The queried endpoint $a$ was collected, so $x_\ell\geq a$.

These constraints construct a report: linearly interpolate the cumulative values between successive collected points, giving density
$$ r(x)=\frac{z_{j+1}-z_j}{x_{j+1}-x_j} \qquad\text{for }x_j<x<x_{j+1}. $$
It is nonnegative and normalized. For a positive target, cumulative values before $x_\ell$ are below $R(c)$, and the interpolation strictly increases from $x_\ell$ to $c$. Thus $c$ is exactly the leftmost cut. Zero-value queries obey the required convention.

There are at most $3Q+1$ report intervals.

Finally, suppose the terminal allocation intervals are $[u_\ell,v_\ell]$, and let $U_0$ be the already computed truthful baseline value. The desired violation is the strict linear inequality
$$ q\sum_\ell \bigl(F_{t(i)}(v_\ell)-F_{t(i)}(u_\ell)\bigr) -qU_0>e. $$
The cumulative functions are affine on the guessed elementary intervals.

The system contains $O(P)$ constraints. Its cut orders and rank counts enforce the guessed group assignments. Induction through the relevant calls consequently shows that every feasible report realizes the guessed allocation.

5.4. Coefficient and solution bit lengths

The truthful baseline has polynomial bit length. To see this explicitly, let $H$ cover the input-dependent affine coefficient denominators as in Section 4, and multiply it by the population sizes of all relevant baseline calls. There are $O(d^2)$ calls, each of size at most $N$, so the resulting integer $H_N$ satisfies
$$ \log H_N=O(L+d^3). $$
All baseline cut coefficients have denominators dividing $H_N$. The endpoint-operation depth is at most $d+1$, giving endpoint bit length
$$ O\!\left(L(d+1)+(d+1)^4\right). $$
The terminal utility sum has the same polynomial bound because these endpoints have a common bounded denominator.

Accordingly, every coefficient of the guessed linear system has bit length at most
$$ B=O\!\left(L(d+1)+(d+1)^4+E\right). $$

A feasible bounded rational linear system with strict inequalities has a polynomial-bit rational solution. Here is the argument needed for this application.

Write its strict inequalities as
$$ g_j(y)>0. $$
All coordinate and cumulative-value variables are bounded in $[0,1]$. Introduce $t$ and replace the strict inequalities by
$$ g_j(y)\geq t,\qquad 0\leq t\leq1. $$
If the original system is feasible, its finitely many strict margins have positive minimum, so the new system has a feasible point with $t>0$.

The new feasible set is a bounded rational polytope. Maximizing $t$ therefore gives a positive optimum at a vertex. For completeness, an optimal point with fewer than a full set of independent active constraints admits a direction preserving its active constraints. Small perturbations in both directions are feasible, so optimality forces the objective to be constant along that direction. Moving until another constraint becomes active, and repeating, produces an optimal vertex; boundedness prevents indefinite movement.

A vertex is determined by a nonsingular system of active rational constraints. Clearing denominators row by row gives integer coefficients of bit length $O(PB)$. Cramer’s rule and the determinant expansion then bound every vertex coordinate’s bit length by
$$ O\!\left(P^2(B+\log(P+1))\right). $$
The interpolated report heights are ratios of differences of these coordinates and cumulative values, so they have the same polynomial bit bound.

Thus the full report, together with the deviator’s identity, has encoding length at most
$$ O\!\left(P^3(B+\log(P+1))\right). $$

5.5. Completion of the certificate proof

If $\epsilon_q>e$, the definition of supremum implies that some permitted report gives a gain strictly greater than $e$. Choose that report’s actual execution data in Section 5.3. Its actual coordinates and cumulative values satisfy the resulting system.

Section 5.4 supplies a polynomial-bit rational feasible solution. Interpolation constructs a permitted rational report, and the execution argument proves that its gain remains strictly greater than $e$.

Conversely, any valid report certificate whose exact simulated gain exceeds $e$ proves $\epsilon_q>e$. The compressed simulation, report normalization checks, and rational arithmetic all take polynomial time in the input and certificate lengths. This proves Theorem 4. $\square$

An explicit, though exponential, fixed-replica decision procedure is obtained by enumerating all certificates up to the proved length bound and verifying them. Its running time is bounded by
$$ 2^{O(P^3(B+\log(P+1)))} \operatorname{poly}(m,\tau,L,d,E). $$
Each verification uses binary counts rather than an expanded population. This is not a polynomial-time algorithm for the target uniform decision.

6. Consequences and an exactly solved incentive case

Theorem 4 implies that violations of the uniform threshold are semidecidable.

Enumerate compatible $q\geq q_0$ and apply the finite-replica decision procedure to each. If $\epsilon^*>e$, some such $q$ has $\epsilon_q>e$, and the procedure eventually finds a certificate. If $\epsilon^*\leq e$, this enumeration need not terminate.

This gives no running-time bound in $\log q_0$: the size of a witnessing replica remains uncontrolled.

There is also a complete homogeneous incentive result.

Proposition 5. If every representative has the same true normalized valuation $V$, then
$$ \epsilon^*=0. $$

Proof. Under truthful reporting, Lemma 1 gives each representative value at least $1/N$. Since the allocations partition a cake of value one, every representative receives exactly $1/N$.

After one representative deviates, the other $N-1$ representatives still report $V$. Lemma 1 guarantees each of them true value at least $1/N$. Their pieces are disjoint up to endpoints, so the deviator’s true value is at most
$$ 1-\frac{N-1}{N}=\frac1N. $$
Its gain is therefore nonpositive for every report and every compatible replica. Taking positive parts and suprema proves the proposition. $\square$

In particular, when $\tau=1$, the continuous allocation measure is
$$ \overline K_1=\frac{\lambda}{n}, $$
and $\epsilon^*\leq e$ holds for every allowed $e\geq0$.

7. What remains open

For dyadic masses, continuous truthful type allocation existence and polynomial-time computation are proved completely.

For incentives, the new theorem controls report complexity and parameter bit length at each fixed replica size. It does not control the binary length of a replica witnessing $\epsilon^*>e$. Consequently, neither a polynomial-time algorithm nor an NP-hardness reduction for the precise uniform predicate has been established here.

Exact invariance of truthful type-average measures does not imply invariance of individual incentive opportunities: replacing one report breaks the scaled truthful block comparison used in Theorem 3.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Overall assessment: partial, with sound substantive results. The output establishes exact truthful allocation invariance and polynomial-time allocation computation for dyadic masses, a polynomial-size report certificate theorem at each fixed replica size, and the homogeneous incentive result. It does not resolve the uniform decision requested in USER_TASK.

I found no false central step or substantive gap in the proofs of these partial results.

1. Scope and interpretation

The output explicitly interprets “binary-rational masses” as dyadic rationals. This is a natural reading of that term, and the assumption is stated clearly rather than hidden.

Under that reading, the allocation theorem addresses the allocation part of the task. If the intended inputs instead include arbitrary rationals encoded in binary, the allocation theorem covers only a subclass; existence and computation for the remaining inputs are not established. The output correctly acknowledges this limitation.

The fixed-replica incentive theorem does not rely on the dyadic assumption.

2. Lemma 1: partition and proportionality

The argument is correct.

The zero-value convention preserves the cut equation and causes no problem.

Although the modified middle call retains population size $k$, it invokes the ordinary recursion. The ordinary assertion at size $k$ follows from assertions at smaller sizes, so the proof has no circular dependency.

3. Theorem 3: exact allocation invariance

The scaling argument is valid for dyadic masses.

Compatibility

For the smallest common denominator $D=2^S>1$, at least one numerator $a_t$ is odd. Thus $\gcd(a_t,D)=1$, and compatibility forces $D\mid N$. Consequently, every compatible population has counts $ba_t$ for an integer $b>0$.

The case $D=1$ is correctly handled: positivity and total mass one imply a single supported type.

Corresponding executions

At every mixed auxiliary call, its size is a power of two greater than one. Both the auxiliary and scaled calls therefore use the fraction $1/2$.

Truthful representatives of a type have identical cuts. Identity ordering resolves ties into consecutive type blocks, so scaling block sizes preserves:

The argument also applies to the ordinary middle recursion. Homogeneous calls can be terminated for aggregate allocation purposes by Lemma 2.

Limit conclusion

The comparison proves equality of aggregate regions up to a null set. The normalization
$$ \overline K_t^q(B)=\frac{1}{n\mu_t}\lambda(U_t^q\cap B) $$
is correct. Therefore the measures are identical for every compatible replica size, which directly establishes their weak limit.

Zero densities, coincident cuts, and zero-length middle intervals do not invalidate this argument.

4. Polynomial-time allocation computation

The operation and bit-length arguments are sound.

At each split, at most one type block is divided between the children. Hence
$$ (r_L-1)+(r_R-1)\leq r-1. $$
This bounds the number of mixed calls at a depth. Applying that bound to the modified exterior tree and to each attached ordinary tree supports the conservative bound
$$ R=O\!\left(1+\tau^2(S+1)^2\right). $$

The half-cut formula is correct on a positive-height elementary interval. Its affine coefficients have a common denominator of bit length $O(L)$: the stated input denominators, positive-height numerators, and factor $2$ suffice after taking a fixed power.

The endpoint-depth bound is also consistent with the recursion. A path may enter one middle ordinary recursion, but that recursion never creates further middle recursions. Thus endpoint bit lengths remain polynomial.

The interval-mass computation has no positive-measure multiplicity, and final normalization has polynomial bit length. The stated running time is polynomial under explicit dyadic encoding, where $S\leq L$. Including the query endpoint length $L_I$ is necessary and appropriate.

5. Theorem 4: fixed-replica incentive certificates

The certificate argument is valid.

Relevant execution size

The deviator follows one modified exterior path and one ordinary path through each middle allocation encountered. The population-size bound gives
$$ Q\leq \frac{d(d+3)}2, \qquad d=\lceil\log_2N\rceil. $$
Its allocation consequently contains at most $d+1$ terminal intervals.

Other branches cannot influence these paths.

Identity-preserving simulation

Truthful type counts, together with counts before and after the deviator within its true type, suffice to reproduce tie-breaking. Other types precede or follow the deviator according to their fixed type indices. Binary rank arithmetic therefore reproduces group membership without expanding the population.

Linear constraints and leftmostness

After guessing elementary-interval locations, truthful cumulative values are affine functions of coordinates.

For positive truthful targets, the condition that the cut lies in a positive-height interval immediately to its left correctly enforces leftmostness. Zero-value queries correctly require $c=a$.

For the deviator, the strict increase from the immediately preceding collected coordinate to the cut enforces leftmostness under the constructed interpolation. The conditions are also satisfied by an actual permitted report: any earlier coordinate within the queried interval must have cumulative value strictly below a positive leftmost target.

The interpolated density is rational, nonnegative, and normalized. The gain inequality is linear after the terminal endpoint locations are fixed.

Polynomial bit lengths

The baseline denominator construction includes the population-size denominators appearing in cut fractions. Its bit length is polynomial in $L$ and $d$.

The strict-inequality argument is valid: introducing a common positive slack produces a bounded rational polytope with a positive optimal slack. An optimal vertex exists, and clearing denominators followed by Cramer’s rule yields polynomial coordinate bit lengths. Forming report heights from coordinate and cumulative-value differences preserves a polynomial encoding bound.

Finally, strict violation of a supremum threshold supplies an actual violating report; attainment of the supremum is unnecessary.

Thus the fixed-replica $\mathrm{NP}$ and $\mathrm{coNP}$ statements follow.

6. Semidecidability and the homogeneous case

Both conclusions are correct.

If $\epsilon^*>e$, some compatible replica satisfies $\epsilon_q>e$. Enumerating replicas and using the finite decision procedure therefore eventually detects a violation. No termination claim is made when $\epsilon^*\leq e$.

For homogeneous valuations, truthful proportionality and partitioning force every truthful allocation to have value exactly $1/N$. After a deviation, the other representatives retain true value at least $1/N$ each, leaving the deviator value at most $1/N$. Hence $\epsilon^*=0$.

7. Blocking issue and minimum required completion

Major issue — the uniform incentive decision remains unresolved.

The certificate bound depends on $\log(nq)$, while the uniform predicate quantifies over arbitrarily large compatible $q$. Nothing proved bounds the binary length of a witnessing replica or otherwise gives a terminating uniform decision procedure.

This is an acknowledged incompleteness, not an error in Theorem 4. Fixed-replica membership in $\mathrm{NP}$ does not establish polynomial-time solvability, NP-hardness, or a corresponding uniform certificate bound.

To complete the assigned task, the prover must supply either the requested polynomial-time uniform decision algorithm with its complexity bound, or the requested hardness argument. If proceeding through finite-replica witnesses, the uncontrolled replica size must be addressed. No expositional clarification alone closes this gap.

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