← back to the atlas

d4-conf-atal-2011-0232 (d4-conf-atal-2011-0232)

Answer: —

The anchor (named result in the paper)

Theorem 1 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateGiven non-increasing marginal valuations and limited misreports, Greedy with on-departure and immediate burn- ing and with payment function according to Equation 2 are DSIC. PROOF. The proof of this theorem follows directly from the above lemmas. Lemmas 1 and 2 show that, for any pair of ar- rival/departure (mis)-reports ⟨ˆai ˆdi⟩the decision policy is truthful in terms of the valuation vector vi, given an appropriate payment pol- icy.

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

The continuous mirror question, as graded

Given a finite horizon \(H\), a finite set of complete EV-owner types \(\Theta\) with rational masses \(\mu_\theta\) summing to \(1\), and rational per-capita supply \(s_t\), can one compute causal fluid versions of the paper’s greedy allocation, threshold payments, and immediate or on-departure burning rules in time polynomial in \(H\), the support size \(\tau\), and input bit length \(L\), while proving that truthful reports of each tagged owner’s availability and non-increasing marginal values are weakly dominant under the paper’s limited-misreport rule?

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

A society is an atomless population of total mass \(1\), given by its support: the list of \(\tau\) types with positive binary-rational masses \(\mu_\theta\). Here \(\tau\) is the support size, not the number of possible types.
Time consists of \(H\geq1\) slots. A type is \(\theta=(a,d,v)\), with \(1\leq a\leq d\leq H\), and an explicitly listed nonnegative, non-increasing rational marginal-value vector of length at most \(m\leq H\), padded with zeros. Supply \(s_t\geq0\) is rational energy per unit population mass; energy is perishable, and each owner can receive at most one indivisible unit per active slot.
The population is tracked by cohorts of reported type and integer endowment \(k\), initially zero. Greedy preallocation selects active mass up to \(s_t\) in decreasing order of \(\hat v_{k+1}\); at a partially selected tied value, every tied cohort contributes the same fraction. A tagged owner is selected with that fraction as its probability, using fresh independent randomness each slot.
Let \(A_t\) be active mass. When \(0<s_t<A_t\), let \(c_t\) be the greedy cutoff value. Set \(c_t=+\infty\) when \(s_t=0\), and \(c_t=0\) when \(s_t>0\) and \(s_t\geq A_t\). Tagged owners above the cutoff are selected, below it are rejected, and at it use the tied fraction; with excess supply all active owners are selected.
For a tagged owner's reported interval \([\hat a,\hat d]\), let \(p^{(t)}\) be the increasingly sorted list \((c_{\hat a},\ldots,c_t)\). Counterfactual prices use the same burning variant with only that owner removed; a zero-mass tagged owner leaves the background population unchanged.
Immediate burning rejects a preallocated unit when \(\hat v_{k+1}<p^{(t)}_{k+1}\), leaving \(k\) unchanged; otherwise it increments \(k\). Burned supply is not reassigned.
On-departure burning increments \(k\) after every preallocation, then at reported departure removes precisely those units \(j\leq k\) with \(\hat v_j<p^{(\hat d)}_j\). In either variant, an owner retaining \(q\) units pays \(\sum_{j=1}^{q}p^{(\hat d)}_j\) at departure and has utility \(\sum_{j=1}^{q}v_j\) minus that payment.
Reports are made on arrival and are fixed thereafter; admissible reports satisfy \(a\leq\hat a\leq\hat d\leq d\) and have nonnegative, non-increasing rational marginal values. Truthfulness means weak dominance in expected utility for each zero-mass tagged owner against every fixed background report profile. Causality permits only reports already received and supply already revealed.
Are both fluid burning variants weakly dominant-strategy truthful under these limited misreports? Is exact causal evaluation of their cohort allocations, burning, threshold payments, and tagged-owner outcome distributions polynomial-time solvable in \(H,m,\tau,L\), or NP-hard, where \(L\) is total input bit length?
For finite societies, greedy with either burning variant and these threshold payments is stated to be DSIC; on-departure price computation is described as linear, while the immediate-burning implementation may examine exponentially many agent subsets. [Verified source](https://parkes.seas.harvard.edu/sites/g/files/omnuum8711/files/2025-05/gerding-aamas11.pdf)
No result settling this specified atomless, tagged-owner version was located in the literature search.

Modeling choices made when packaging the task

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

1. Results and interpretation.

Both fluid burning variants are weakly dominant-strategy truthful for zero-mass tagged owners under the stated limited misreports.

For computation, the following results are proved:

$$ 2^{O(b)}\operatorname{poly}(H,m,\tau,L) $$
bit operations.

No $\mathrm{NP}$-hardness reduction is established. Thus the requested complexity classification remains partially unresolved.

For the explicit-output result, a rational is represented by binary integers giving its numerator and denominator. For the succinct-output result, a rational is represented by two integer arithmetic circuits giving its numerator and a positive denominator. The tagged-owner distributions considered below include final retained quantity, total burned quantity, and payment. The transition description also specifies the joint distribution of the entire allocation history.

2. Fixed background and threshold facts.

Fix one burning variant and a background report profile for which the stipulated allocation rules are defined. Removing a zero-mass tagged owner changes no background cohort mass. Therefore its report and allocation history affect neither the background cutoffs nor the background tied fractions.

Write the resulting cutoff sequence as
$$ c_1,\ldots,c_H. $$
This argument applies separately to each burning variant; their background cutoff sequences need not coincide.

For an interval $J$, let $p_j(J)$ be the $j$-th smallest cutoff in $J$, where
$$ 1\leq j\leq |J|. $$
The entries may include $+\infty$.

If $J\subseteq I$, then
$$ p_j(I)\leq p_j(J) \qquad (1\leq j\leq |J|). $$
Indeed, the $j$ smallest entries in $J$ also occur in $I$, and all are at most $p_j(J)$. This proves the inequality, including when the right-hand side is infinite.

In particular, enlarging a reported prefix through departure cannot increase an existing order statistic.

Consider an arbitrary admissible report with interval $\widehat I=[\widehat a,\widehat d]$ and finite marginal values $\widehat v_j$.

Under immediate burning, if its $j$-th retained unit is obtained at slot $t$, then
$$ \widehat v_j \geq p_j([\widehat a,t]) \geq p_j(\widehat I). $$
Thus every finally retained unit has a finite departure price.

Under on-departure burning, retained indices form a prefix. To see this, suppose index $j$ fails the retention test. For every $\ell>j$,
$$ \widehat v_\ell \leq \widehat v_j <p_j(\widehat I) \leq p_\ell(\widehat I). $$
Hence every later index fails as well. Every retained index consequently satisfies
$$ \widehat v_j\geq p_j(\widehat I), $$
and again has a finite price.

These observations justify all payment and utility expressions below.

3. Truthfulness: truthful utility is maximal for every outcome.

Let the tagged owner's true interval be
$$ I=[a,d], \qquad T=d-a+1. $$
Pad its true marginal vector with zeros through index $T$, and write
$$ p_j=p_j(I). $$
Define
$$ r=\max\bigl(\{0\}\cup\{j\leq T:v_j>p_j\}\bigr), $$
and
$$ z=\max\bigl(\{0\}\cup\{j\leq T:v_j\geq p_j\}\bigr). $$
Since values are non-increasing and prices are non-decreasing, both sets of qualifying indices are prefixes. Thus $r\leq z$.

Let $n$ be the number of finite cutoffs in $I$. For $0\leq q\leq n$, define
$$ F_I(q)=\sum_{j=1}^{q}(v_j-p_j), \qquad F_I(0)=0. $$
Its increments are positive through index $r$, zero from index $r+1$ through $z$, and negative at all remaining finite-price indices. Therefore
$$ F_I(q)\leq F_I(r) \qquad (0\leq q\leq n), $$
with equality whenever $r\leq q\leq z$.

We next prove that truthful play retains a quantity in this maximizing interval.

Upper bound. The retention facts proved in Section 2 imply, in either variant, that every truthful retained index $j$ satisfies
$$ v_j\geq p_j. $$
Consequently, the final retained quantity $q$ satisfies $q\leq z$.

Lower bound. There is nothing to prove if $r=0$. Suppose $r>0$. Since
$$ p_r<v_r, $$
at least $r$ slots in $I$ have cutoffs strictly below $v_r$. Let the first $r$ such slots be
$$ t_1<t_2<\cdots<t_r. $$
Thus
$$ c_{t_j}<v_r \qquad (1\leq j\leq r). $$

We prove inductively that the running endowment immediately after $t_j$ is at least $j$. Running endowment means retained units for immediate burning and preallocated units for on-departure burning.

Before $t_j$, the induction hypothesis gives endowment at least $j-1$. If it is already at least $j$, the assertion follows from its monotonicity before departure. Otherwise it equals $j-1$, so the next truthful marginal is $v_j$, and
$$ v_j\geq v_r>c_{t_j}. $$
The owner is therefore preallocated a unit with probability one.

For on-departure burning, this raises its running endowment to $j$.

For immediate burning, the prefix through $t_j$ contains the $j$ slots $t_1,\ldots,t_j$, all with cutoffs below $v_r$. Hence
$$ p_j([a,t_j])<v_r\leq v_j. $$
The new unit passes the immediate retention test, also raising the endowment to $j$.

This completes the induction. Immediate burning therefore ends with at least $r$ retained units. On-departure burning obtains at least $r$ preallocations, and its first $r$ units survive because
$$ v_j>p_j \qquad (1\leq j\leq r). $$

Thus, for every allowed realization of tied selections,
$$ r\leq q\leq z. $$
Truthful utility is consequently the constant
$$ U^\star=F_I(r). $$

Now consider any admissible joint value-and-interval deviation, with reported interval $\widehat I$. Limited misreports imply
$$ \widehat I\subseteq I. $$
If the deviation retains $q$ units, all its charged prices are finite, and its realized true utility is
$$ U_{\mathrm{dev}} =\sum_{j=1}^{q}v_j-\sum_{j=1}^{q}p_j(\widehat I). $$
The interval inequality gives
$$ p_j(I)\leq p_j(\widehat I) \qquad (1\leq j\leq q). $$
In particular, these $q$ prices in $I$ are finite, so $q\leq n$. Therefore
$$ U_{\mathrm{dev}} \leq F_I(q) \leq F_I(r) =U^\star. $$

This bounds every deviation outcome by the constant truthful utility. No coupling of the truthful and deviating randomness is needed. Taking expectations proves weak dominant-strategy truthfulness for both variants.

4. A causal cohort algorithm.

For computation, $\tau$ denotes the number of reported types in the explicitly represented support. Maintain the pre-slot mass $x_{\theta,k}$ of each received type $\theta$ with running endowment $k$.

At an active slot $t$, process only states in the range
$$ 0\leq k\leq t-\widehat a_\theta. $$
Consequently, whenever the prefix-price test is needed, its index satisfies
$$ k+1\leq t-\widehat a_\theta+1. $$
There are at most $\tau(H+1)$ type-endowment coordinates.

Group active coordinates by their next marginal value and sort these values decreasingly. Summing their masses computes active mass and cumulative greedy demand.

At a partial-supply slot, let $B_{>}$ and $B_{=}$ be the masses strictly above and at the cutoff. The tied fraction is
$$ \alpha_t=\frac{s_t-B_{>}}{B_{=}}. $$
The chosen cutoff group has positive mass, so this division is defined. The zero-supply and excess-supply cases use the stated conventions.

Let $f_{\theta,k,t}$ be a cohort's preallocation fraction.

For immediate burning, define
$$ h_{\theta,k,t} = \mathbf 1\!\left\{ \widehat v_{\theta,k+1} \geq p_{\theta,k+1}^{(t)} \right\}. $$
The mass
$$ f_{\theta,k,t}h_{\theta,k,t}x_{\theta,k} $$
moves to endowment $k+1$, while the remainder stays at $k$. The burned amount is
$$ f_{\theta,k,t}(1-h_{\theta,k,t})x_{\theta,k}. $$
All transitions are simultaneous.

For on-departure burning, the entire preallocated mass
$$ f_{\theta,k,t}x_{\theta,k} $$
moves to $k+1$. At departure, put
$$ T_\theta=\widehat d_\theta-\widehat a_\theta+1, $$
and
$$ z_\theta = \max\left( \{0\}\cup \left\{ j:1\leq j\leq T_\theta,\ \widehat v_{\theta,j} \geq p_{\theta,j}^{(\widehat d_\theta)} \right\} \right). $$
The prefix-retention argument from Section 2 gives
$$ q_\theta(k)=\min(k,z_\theta). $$
Such an owner burns $k-q_\theta(k)$ units and pays
$$ \sum_{j=1}^{q_\theta(k)} p_{\theta,j}^{(\widehat d_\theta)}. $$

For a tagged owner, run the same transitions on state probabilities instead of masses. Fresh independent slot randomness makes these the correct conditional transition probabilities. To obtain the joint distribution of retained quantity and total burning under immediate burning, add an accumulated burned-count coordinate. Both coordinates lie between $0$ and $H$, so this remains a polynomial-size dynamic program. For on-departure burning, final burning is determined by the departure map.

The time-indexed transition probabilities also describe the full joint distribution of allocation histories without enumerating all histories.

Every operation uses only received reports, past and current cutoffs, current cohort masses, and supply revealed through the current slot. Maintaining sorted cutoff histories, updating cohorts, and running the tagged-owner dynamic program therefore require polynomially many causal arithmetic operations and comparisons.

5. Succinct evaluation and exact comparison upper bounds.

Define $\mathrm{PosSLP}$ as follows: given a variable-free integer arithmetic circuit using constants $0,1$ and operations $+,-,\times$, decide whether its output is positive.

A rational quantity can be maintained as a pair of integer circuits
$$ \frac{N}{D}, \qquad D>0. $$
For example,
$$ \frac{N_1}{D_1}+\frac{N_2}{D_2} = \frac{N_1D_2+N_2D_1}{D_1D_2}, $$
and
$$ \frac{N_1}{D_1}-\frac{N_2}{D_2} = \frac{N_1D_2-N_2D_1}{D_1D_2}. $$
Multiplication similarly adds only constantly many integer gates.

The only divisions needed by the cohort algorithm are by strictly positive tied-group masses. If $N_2/D_2>0$, then
$$ \frac{N_1/D_1}{N_2/D_2} = \frac{N_1D_2}{D_1N_2}, $$
whose denominator is positive.

Input integers written in binary can be constructed from $0,1$ using a number of gates linear in their bit length, by repeated doubling and addition. Thus the polynomial arithmetic-operation algorithm produces polynomial-size shared circuits for all rational quantities.

For two represented rationals,
$$ \frac{N_1}{D_1}>\frac{N_2}{D_2} \quad\Longleftrightarrow\quad N_1D_2-N_2D_1>0. $$
This is one $\mathrm{PosSLP}$ query. Equality can be decided by testing both this integer and its negative for positivity.

Consequently, active-mass comparisons, cumulative-demand comparisons, zero-mass tests, and cutoff choices can all be performed using polynomially many adaptive $\mathrm{PosSLP}$ queries. Infinite cutoffs are handled as a separate symbol. Price comparisons otherwise involve input marginal values or zero.

It follows that polynomial-size circuit descriptions of the exact outputs can be constructed in
$$ \mathrm{FP}^{\mathrm{PosSLP}}. $$
The construction remains causal because each circuit and oracle query uses only quantities available at that slot.

For a precise decision formulation, consider either of the following tasks:

The coordinate indices and threshold are part of the input. Constructing the relevant circuits and performing the final comparison places each task in
$$ \mathrm{P}^{\mathrm{PosSLP}}. $$

A known theorem of Allender, Bürgisser, Kjeldgaard-Pedersen, and Miltersen states that $\mathrm{PosSLP}$ belongs to the counting hierarchy. Its hypotheses apply here: every oracle query is a variable-free, division-free integer circuit using $0,1,+,-,\times$. [On the Complexity of Numerical Analysis](https://www3.math.tu-berlin.de/algebra/work/focs7.pdf)

For completeness, let
$$ \mathcal C_0=\mathrm P, \qquad \mathcal C_{j+1}=\mathrm{PP}^{\mathcal C_j}, \qquad \mathrm{CH}=\bigcup_{j\geq0}\mathcal C_j. $$
The cited theorem places $\mathrm{PosSLP}$ in some fixed level $\mathcal C_j$. A deterministic polynomial-time oracle computation is a special probabilistic computation, so
$$ \mathrm{P}^{\mathrm{PosSLP}} \subseteq \mathrm{P}^{\mathcal C_j} \subseteq \mathcal C_{j+1} \subseteq \mathrm{CH}. $$

Each fixed level of this hierarchy lies in $\mathrm{PSPACE}$. Inductively, enumerate the polynomially many random bits of a probabilistic oracle computation, count its accepting branches with a polynomial-bit counter, and answer each oracle query using the preceding level's polynomial-space simulation. The fixed nesting depth preserves polynomial space.

Thus the stated comparison problems lie in $\mathrm{CH}$ and in $\mathrm{PSPACE}$. These are upper bounds, not hardness reductions.

6. Explicit bit complexity and a tractable special case.

Let $b$ be the number of slots whose tied fraction satisfies
$$ 0<\alpha_t<1. $$
At all other slots, every cohort transition fraction is $0$ or $1$.

For analysis, let $D_0$ be the product of all input mass denominators. Then
$$ \log_2 D_0\leq L. $$
Using this common denominator analytically does not require the causal algorithm to inspect future reports.

Suppose current cohort masses have common denominator $D$, and write a splitting slot's quantities as
$$ s_t=\frac{u_t}{w_t}, \qquad B_{>}=\frac{a_t}{D}, \qquad B_{=}=\frac{h_t}{D}. $$
Then
$$ \alpha_t = \frac{u_tD-w_ta_t}{w_th_t}. $$
Every resulting cohort mass has a denominator dividing
$$ D'=Dw_th_t. $$
Since $B_{=}\leq1$, its numerator satisfies $h_t\leq D$. Hence
$$ \log_2 D' \leq 2\log_2 D+\log_2 w_t \leq 2\log_2 D+L. $$

At a non-splitting slot, transitions and aggregation introduce no new denominator factor. Later arrivals have denominators dividing $D_0$, which continues to divide the analytical common denominator.

After $b$ splitting slots, the recurrence therefore gives
$$ \log_2 D=O(2^bL). $$

Tagged-state probabilities have denominators dividing the product of the splitting fractions' denominator factors $w_th_t$. The logarithm of this product is also $O(2^bL)$. Adding a burned-count coordinate does not change this argument.

Every finite cutoff is an input marginal value or zero. A threshold payment is a sum of at most $H$ such values and has polynomial bit length. Combining payments with masses or probabilities preserves the bound
$$ O(2^bL)+\operatorname{poly}(H,L) $$
on operand lengths.

Using reduced rational arithmetic, each integer operation and reduction takes time polynomial in these lengths. Together with the polynomial operation count, this proves the bit-time bound
$$ 2^{O(b)}\operatorname{poly}(H,m,\tau,L). $$
In particular, explicit evaluation is polynomial-time on instances satisfying
$$ b=O\!\left(\log(H+m+\tau+L)\right). $$
Taking $b\leq H$ also gives the general upper bound
$$ 2^{O(H)}\operatorname{poly}(H,m,\tau,L). $$

7. Exponential output size with one type and two marginals.

The following construction strengthens the previous output-size obstruction.

Fix any $H\geq2$. Let $C$ be the smallest power of two satisfying
$$ C\geq \max(16,2H). $$
The entire population has the single type
$$ \theta=(1,H,(1,1)), \qquad \mu_\theta=1. $$
Thus $\tau=1$ and $m=2$. Set
$$ s_t=\frac1C \qquad (1\leq t\leq H). $$
All masses and supplies are dyadic rationals.

Let $x_{j,t}$ denote the mass with running endowment $j$ after slot $t$. We prove that both variants have identical trajectories, no burning, and only states $j=0,1,2$.

Initially,
$$ x_{0,0}=1, \qquad x_{1,0}=x_{2,0}=0. $$
Suppose this description holds through slot $t-1$, with total preallocated units $(t-1)/C$. Then
$$ x_{1,t-1}+2x_{2,t-1}=\frac{t-1}{C}, $$
so
$$ x_{2,t-1}\leq \frac{t-1}{2C}. $$
The mass with next marginal value one is
$$ B_{t-1}=x_{0,t-1}+x_{1,t-1} =1-x_{2,t-1} \geq 1-\frac{t-1}{2C} \geq \frac34. $$
Since $1/C\leq1/16$, this mass strictly exceeds supply. Therefore the cutoff is
$$ c_t=1, $$
and the tied fraction is
$$ \alpha_t=\frac{1}{CB_{t-1}}. $$
No zero-valued unit is preallocated.

Every selected first or second unit passes immediate burning: the applicable prefix price is one, equal to its marginal value. At final departure, all on-departure preallocations survive for the same reason. This completes the induction.

The common cohort recurrence is consequently
$$ x_{0,t}=x_{0,t-1}(1-\alpha_t), $$
$$ x_{1,t} =x_{1,t-1}(1-\alpha_t)+x_{0,t-1}\alpha_t, $$
$$ x_{2,t}=x_{2,t-1}+x_{1,t-1}\alpha_t. $$
Conservation of mass and the total-unit identity imply
$$ x_{0,t}+x_{1,t}+x_{2,t}=1, $$
$$ x_{1,t}+2x_{2,t}=\frac tC, $$
and hence
$$ B_t=x_{0,t}+x_{1,t} =2-\frac tC-x_{0,t}. $$

Define
$$ y_t=Cx_{0,t}. $$
Substituting the expression for $B_{t-1}$ into the recurrence for $x_{0,t}$ gives
$$ y_t = y_{t-1} \frac{2C-t-y_{t-1}}{2C-t+1-y_{t-1}}. $$
Throughout the construction,
$$ 0<y_t\leq C. $$

Cancellation lemma. Write a preceding value in lowest terms as
$$ y_{t-1}=\frac pq, \qquad p,q>0, \qquad \gcd(p,q)=1, $$
and put $A=2C-t$. Before reduction, the next numerator and denominator are
$$ N=p(Aq-p), \qquad D=q((A+1)q-p). $$
Their greatest common divisor is exactly
$$ \gcd(N,D)=\gcd(p,A+1). $$

To prove this, put
$$ U=Aq-p, \qquad V=(A+1)q-p. $$
Since $p$ and $q$ are coprime,
$$ \gcd(U,q)=1. $$
Also $V-U=q$, so
$$ \gcd(U,V)=\gcd(U,q)=1. $$
Thus $U$ is coprime to $qV$, and
$$ \gcd(pU,qV)=\gcd(p,qV)=\gcd(p,V). $$
Finally,
$$ \gcd(p,V) =\gcd(p,(A+1)q) =\gcd(p,A+1), $$
again using $\gcd(p,q)=1$.

Now write
$$ y_t=\frac{P_t}{Q_t} $$
in lowest terms. The cancellation lemma gives
$$ Q_t = \frac{Q_{t-1}^2(A+1-y_{t-1})} {\gcd(P_{t-1},A+1)}. $$
Because $y_{t-1}\leq C$, $t\leq H$, and $C\geq2H$,
$$ A+1-y_{t-1} \geq C-H+1 \geq \frac C2. $$
Furthermore,
$$ \gcd(P_{t-1},A+1)\leq A+1\leq2C. $$
Therefore
$$ Q_t\geq\frac{Q_{t-1}^2}{4}. $$

The first two values are
$$ y_1=C-1, \qquad y_2=\frac{(C-1)^2}{C}. $$
The second fraction is reduced, so $Q_2=C$. Induction now yields
$$ Q_t\geq 4\left(\frac C4\right)^{2^{t-2}} \qquad (t\geq2). $$
Consequently,
$$ \log_2 Q_H \geq 2+2^{H-2}(\log_2 C-2) \geq 2+2^{H-1}. $$

The final unserved mass is
$$ x_{0,H}=\frac{P_H}{CQ_H}. $$
Since $\gcd(P_H,Q_H)=1$, reducing this fraction cancels at most the factor $C$ from its denominator. Its reduced denominator is therefore at least $Q_H$, and requires exponentially many binary digits.

The same number is a tagged-owner outcome probability. Take a zero-mass tagged owner reporting $\theta$. Conditional on still having zero units, its probability of remaining unserved in slot $t$ is $1-\alpha_t$. No units burn. Thus
$$ \Pr(q=0) = \prod_{t=1}^{H}(1-\alpha_t) = x_{0,H}. $$

The input has
$$ \tau=1, \qquad m=2, \qquad L=O(H\log H). $$
Nevertheless, this required exact probability has at least $2^{H-1}$ denominator bits.

Any integer numerator-denominator representation of a rational has denominator at least its reduced denominator. Hence allowing unreduced fractions does not remove the obstruction.

This proves that neither variant admits polynomial-time exact evaluation with explicit binary-rational cohort masses and tagged outcome probabilities, even for this single-type, two-marginal family.

8. What remains unresolved.

The incentive question is completely settled by Section 3. Explicit polynomial-time evaluation is ruled out by Section 7, while Sections 5 and 6 give succinct and explicit upper bounds.

The denominator-growth construction does not encode an $\mathrm{NP}$-hard decision problem. Its cutoff sequence is simply constant at one. Therefore its exponential output length supplies no hardness reduction for cutoff selection or rational-coordinate comparison.

Likewise, the reduction to $\mathrm{PosSLP}$ proves an upper bound only. A reverse reduction, or a direct reduction from an $\mathrm{NP}$-hard problem, remains unproved.

⟨structured verdict parsed — rendered above⟩

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

The output establishes truthfulness for both variants and gives valid computational upper bounds and an exponential output-size obstruction. I found no false step in those arguments. It does not settle the requested complexity classification, as the prover explicitly acknowledges. The overall result is therefore partial.

1. Fixed-background and retention facts

Verified.

Removing a zero-mass tagged owner leaves every background cohort mass unchanged. Consequently, the background cutoffs and tied fractions are independent of that owner’s report and realized selections. Applying this observation separately to the two burning variants is correct.

The order-statistic inequality
$$ p_j(I)\leq p_j(J) \qquad \left(J\subseteq I,\ 1\leq j\leq |J|\right) $$
is correctly justified. It remains valid with infinite entries.

For immediate burning, a retained unit passes its acquisition-time test. Enlarging the prefix to the reported departure interval can only decrease its indexed price. Hence every retained unit has a finite departure price and satisfies the stated retention inequality.

For on-departure burning, the failed indices form a suffix because reported values are non-increasing and indexed prices are non-decreasing. Thus the retained indices form a prefix. This also justifies charging the first retained-quantity order statistics rather than prices at some nonconsecutive set of indices.

No gap appears in Section 2.

2. Truthfulness

Verified for both variants under the specified limited misreports.

Maximizing quantities

The definitions of $r$ and $z$ correctly distinguish strictly profitable units from weakly profitable units. Because the sequence of true marginal values is non-increasing and the price sequence is non-decreasing, the qualifying sets are prefixes.

Restricting $F_I(q)$ to $q\leq n$, where $n$ counts finite cutoffs, avoids subtraction involving infinite prices. On this domain, its increments have exactly the signs claimed. In particular,
$$ F_I(q)\leq F_I(r), $$
and every quantity between $r$ and $z$ attains that maximum.

This includes the edge cases $r=0$, $z=0$, and $n=0$.

Truthful upper bound

The retention inequalities established in Section 2 imply that every truthful retained index belongs to the weakly profitable prefix. Therefore $q\leq z$ in either variant.

Truthful lower bound

The strict inequality $p_r<v_r$ guarantees at least $r$ distinct slots whose cutoffs are strictly below $v_r$.

The induction through those slots is valid:

Accordingly, every truthful realization satisfies
$$ r\leq q\leq z, $$
and truthful utility equals the same finite value $F_I(r)$.

The proof correctly uses strict cutoff inequalities here; it does not assume favorable outcomes from tied selection.

Deviations

Every admissible reported interval is contained in the true interval. A deviation retaining $q$ units has finite charged prices, and $q$ cannot exceed its reported interval length because at most one unit is preallocated per active slot.

The interval order-statistic inequality therefore applies to every charged index. It also ensures that the corresponding true-interval prices are finite. The resulting bound
$$ U_{\mathrm{dev}}\leq F_I(q)\leq F_I(r) $$
is valid for every deviation realization.

No coupling of truthful and deviating random choices is needed because truthful utility is constant. Taking expectations proves the requested weak dominance against every fixed background profile for which the stipulated mechanism is defined.

3. Causal cohort evaluation

Verified as a polynomial arithmetic-operation algorithm.

The pre-slot endowment range is correct: before slot $t$, a type arriving at $\widehat a_\theta$ has had at most $t-\widehat a_\theta$ allocation opportunities. Consequently, every evaluated prefix-price index exists.

Grouping active cohorts by their next marginal value implements greedy allocation. At a partial-supply slot, the selected cutoff group has positive mass, so the tied-fraction division is defined.

The immediate-burning transitions correctly distinguish preallocation from retention. A rejected unit leaves endowment unchanged, and the displayed burning expression counts exactly the rejected preallocated mass.

The on-departure transitions correctly increment endowment after each preallocation. Its departure map
$$ q_\theta(k)=\min(k,z_\theta) $$
follows from the already-proved prefix-retention property.

Replacing cohort masses by tagged-state probabilities is valid because the background is fixed and slot randomness is fresh and independent. Adding accumulated burning as a state coordinate is sufficient for the joint distribution of retained quantity, burned quantity, and payment: payment is determined by retained quantity and the reported interval’s departure prices.

The allocation-history claim is correctly limited to a transition description. It does not assert polynomial-time enumeration of all histories.

All operations use information available by the current slot. The polynomial count of states, arithmetic operations, and comparisons is justified. This establishes an arithmetic-operation bound, not a polynomial bit-time bound.

4. Circuit representations and comparison bounds

Verified.

The numerator-denominator circuit formulas correctly implement rational arithmetic. Denominators remain positive because the only divisions are by positive tied-group masses.

Sharing previously constructed circuit nodes prevents repeated arithmetic expressions from causing exponential circuit size. Binary input integers can be built with a linear number of gates in their bit lengths.

Cross multiplication correctly reduces rational comparison to an integer sign test because both denominators are positive. The equality procedure is also valid.

Thus polynomially many adaptive sign queries suffice for the cohort algorithm, yielding the claimed circuit-output bound
$$ \mathrm{FP}^{\mathrm{PosSLP}} $$
and the coordinate-decision bound
$$ \mathrm{P}^{\mathrm{PosSLP}}. $$

The cited theorem does apply: the oracle queries are variable-free, division-free integer circuits with constants $0,1$ and operations $+,-,\times$. The source establishes membership of $\mathrm{PosSLP}$ in a fixed level of the counting hierarchy. [Allender et al., *On the Complexity of Numerical Analysis*](https://www3.math.tu-berlin.de/algebra/work/focs7.pdf)

The subsequent hierarchy inclusion and polynomial-space simulation are valid. A fixed oracle nesting depth preserves polynomial space, even though branch enumeration takes exponential time.

These are upper bounds only; they establish no hardness classification.

5. Explicit bit complexity

Verified.

At a splitting slot, the proposed common denominator
$$ D'=Dw_th_t $$
accommodates both selected and unselected cohort masses. The bound $h_t\leq D$ follows from the fact that the tied-group mass is at most the total population mass.

Therefore the recurrence
$$ \log_2 D'\leq 2\log_2 D+L $$
is valid. Non-splitting transitions introduce no new denominator factor, and later arrivals remain covered because the analytical denominator retains the factor $D_0$.

The resulting bound
$$ \log_2 D=O(2^bL) $$
is correct. The corresponding tagged-probability denominator bound follows from multiplying the splitting-fraction denominator factors.

Finite prices are input marginal values or zero. Summing at most $H$ such values has polynomial bit length. Multiplying those payments by masses or probabilities preserves the stated operand-length bound.

Polynomial-time integer arithmetic and rational reduction then give
$$ 2^{O(b)}\operatorname{poly}(H,m,\tau,L). $$
The claimed polynomial-time special case for logarithmically many splitting slots follows.

6. Exponential output-size construction

Verified, including the cancellation calculation.

The construction respects the input restrictions: one positive-mass type, two non-increasing marginal values, dyadic supplies, and an interval of length $H$.

The bound on second-unit mass ensures that the value-one cohort mass always exceeds supply. Therefore every cutoff is one, no zero-valued unit is selected, and neither variant burns any unit. The common recurrence and conservation identities are correct.

Substitution into the recurrence for $y_t$ gives the displayed rational recurrence.

For the cancellation lemma, the coprimality statements
$$ \gcd(U,q)=1, \qquad \gcd(U,V)=1 $$
correctly imply that $U$ contributes no cancellation against the denominator. The remaining cancellation is exactly
$$ \gcd(p,A+1). $$

The resulting reduced-denominator recurrence and estimates correctly yield
$$ Q_t\geq \frac{Q_{t-1}^2}{4}. $$
The initial values are correct, and $Q_2=C$ because consecutive integers are coprime. The stated inductive lower bound follows.

Passing from $y_H$ to $x_{0,H}=y_H/C$ cannot reduce the denominator below $Q_H$. Thus the exponential denominator-bit lower bound is valid.

The equality between final unserved cohort mass and the tagged owner’s probability of receiving no units follows from their identical zero-unit transition factors.

Finally, the input length is $O(H\log H)$, while a required explicit output has exponentially many bits in $H$. This unconditionally rules out a general polynomial-time algorithm that writes those outputs as binary numerator-denominator pairs. Allowing unreduced fractions does not evade the obstruction.

7. Outstanding issue and actionable feedback

Major incompleteness relative to USER_TASK: the requested complexity classification remains unsettled.

The output-size lower bound does not establish $\mathrm{NP}$-hardness. The circuit and counting-hierarchy upper bounds also do not establish polynomial-time solvability without an oracle.

This is an explicitly acknowledged limitation, not an erroneous inference by the prover. The output accurately labels its overall contribution as partial.

Minimum additional work needed to resolve the outstanding target:

No clarification alone can supply this missing result. The verified truthfulness proof and computational bounds can stand independently.

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