← back to the atlas

d4-conf-ijcai-2020-0013 (d4-conf-ijcai-2020-0013)

Answer: —

The anchor (named result in the paper)

Theorem 2 — class: algorithmic

The continuous mirror question, as graded

Given finite driver and request type sets, compatibility edges, acceptance rates, profits, patience limits, driver masses, and known request masses at each of finitely many stages, characterize the Pareto frontier of profit and minimum matched driver-type fraction achievable by causal mass-routing policies, measured against the corresponding fluid LP benchmarks.

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

Let \(G=(U,V,E)\) be a finite compatibility graph with nonempty driver and request type sets, and \(T\geq1\) stages. Driver type \(u\) has initial mass \(B_u>0\); request type \(v\) has mass \(r_{v,t}\geq0\) arriving at stage \(t\), with \(r_v=\sum_t r_{v,t}>0\). All masses are binary rationals, are not normalized to sum to one, and the entire arrival schedule is known initially.
A society is given by its support: the list of the \(\tau=|U|+|V|\) types with positive total mass, each with its mass as a binary rational; \(\tau\) counts supported types, not possible types. Put \(m=|E|\), and let \(L\) be the total input bit length.
Each edge \((u,v)\) has rational acceptance rate \(p_{uv}\in(0,1]\) and nonnegative rational profit \(w_{uv}\); each request type has positive integer patience \(\Delta_v\), encoded in binary.
A causal mass-routing policy may split arriving request mass arbitrarily, reject portions, and sequentially probe compatible, currently unmatched drivers. Probing mass \(z\) on \((u,v)\) matches exactly \(p_{uv}z\) and leaves \((1-p_{uv})z\) eligible for another probe; only successful mass consumes driver capacity. Each request portion receives at most \(\Delta_v\) probes, stops upon success, and leaves within its arrival stage. Distinct drivers of the same type may be tried; the same individual driver may not be retried for that request. No future request mass may be used.
For total successful masses \(M_{uv}\), define profit \(P=\sum_{(u,v)\in E}w_{uv}M_{uv}\) and fairness \(F=\min_{u\in U}(\sum_v M_{uv})/B_u\).
Define fluid benchmarks \(P^*\) and \(F^*\) by separately maximizing \(\sum_{(u,v)\in E}w_{uv}p_{uv}x_{uv}\) and \(\min_u(\sum_v p_{uv}x_{uv})/B_u\), subject to \(x_{uv}\geq0\), \(\sum_v p_{uv}x_{uv}\leq B_u\), \(\sum_u x_{uv}\leq\Delta_v r_v\), and \(\sum_u p_{uv}x_{uv}\leq r_v\). Repeated probes to different drivers of one type are included in \(x_{uv}\).

Which pairs \((a,b)\in[0,1]^2\) admit a causal mass-routing policy guaranteeing \(P\geq aP^*\) and \(F\geq bF^*\) simultaneously on every instance in time polynomial in \(m,\tau,T,L\), and which pairs are impossible on some instance? What is the Pareto frontier of these simultaneous approximation guarantees?

For discrete independent identically distributed arrivals, an online algorithm guarantees \((c\alpha,c\beta)\) against its two LP benchmarks, where \(c=(e-1)/(e+1)\), \(\alpha,\beta>0\), and \(\alpha+\beta\leq1\). [Source](https://arxiv.org/html/2012.06850)
A different ridesharing model has asymptotically optimal policies based on a continuous LP, incorporating waiting-time patience and time-varying arrivals; this result does not characterize the simultaneous probing guarantees defined here. No result settling this exact fluid frontier was located. [Source](https://doi.org/10.1287/stsy.2019.0037)

Modeling choices made when packaging the task

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

Status and interpretation

Put
$$ q=1-\frac1e. $$

The polynomial-time frontier in the question remains unresolved. I prove the following partial results:

Items 3–5 advance the computational part of the previous argument. Item 6 remains conditional on the execution model and therefore does not settle the original question.

I use the intended nonatomic interpretation: driver and request masses can be divided into arbitrarily small subsets. An individual driver cannot serve two successful requests, and a request cannot retry an individual driver.

The cited discrete theorem assumes independent, identically distributed arrivals; I do not apply it to the deterministic schedule here. [Xu and Xu, Theorem 2](https://arxiv.org/html/2012.06850)

1. A universal impossibility bound

Consider one stage, one request type $v$, and two driver types $H,L$. Choose a positive integer $N$ and a positive power of two $d$, and set
$$ r_v=1,\qquad B_H=1,\qquad B_L=N,\qquad \Delta_v=d. $$
Both edges have acceptance rate $1/d$. Their profits are
$$ w_{Hv}=1,\qquad w_{Lv}=0. $$

All these data have admissible binary encodings.

Write
$$ y_H=\frac{x_{Hv}}d,\qquad y_L=\frac{x_{Lv}}d. $$
The benchmark constraints become
$$ y_H,y_L\geq0,\qquad y_H\leq1,\qquad y_L\leq N,\qquad y_H+y_L\leq1. $$
Both request constraints yield the last inequality. Consequently,
$$ P^*=1. $$
Fairness at least $f$ requires $y_H\geq f$ and $y_L\geq Nf$. Thus
$$ F^*=\frac1{N+1}, $$
with equality attained by $y_H=1/(N+1)$ and $y_L=N/(N+1)$.

Let $A_j$ be the request mass receiving its $(j+1)$-st actual probe. Every such portion must have survived its preceding probes. Therefore
$$ A_0\leq1,\qquad A_{j+1}\leq\left(1-\frac1d\right)A_j. $$
Capacity restrictions and rejection can only reduce these quantities. Hence every policy satisfies
$$ M_H+M_L =\frac1d\sum_{j=0}^{d-1}A_j \leq1-\left(1-\frac1d\right)^d =:q_d. $$

The requested guarantees imply
$$ M_H\geq a,\qquad M_L\geq\frac{bN}{N+1}. $$
A necessary condition on this instance is therefore
$$ a+\frac{bN}{N+1}\leq q_d. $$

As $d$ tends to infinity through powers of two, $q_d\to q$. For example, integrating $1/(1-t)$ gives, for $d>1$,
$$ -\frac d{d-1} \leq d\log\left(1-\frac1d\right) \leq-1, $$
which proves the limit. Letting $N$ also tend to infinity gives
$$ \boxed{a+b\leq q.} $$

This yields a finite counterexample whenever $a+b>q$. Indeed, put $\varepsilon=a+b-q>0$, and choose $d,N$ with
$$ q_d-q<\frac\varepsilon3,\qquad \frac b{N+1}<\frac\varepsilon3. $$
Then
$$ a+\frac{bN}{N+1} =a+b-\frac b{N+1} >q+\frac{2\varepsilon}3 >q_d. $$

This impossibility holds independently of computational resources.

2. Finite causal realization of a feasible benchmark solution

Let $x$ be any rational feasible benchmark solution. For each request type $v$, define
$$ d_v=\Delta_v,\qquad z_v=\frac{\sum_u p_{uv}x_{uv}}{r_v},\qquad \pi_{uv}=\frac{x_{uv}}{d_vr_v}. $$
Benchmark feasibility implies
$$ 0\leq z_v\leq1,\qquad \sum_u\pi_{uv}\leq1. $$

2.1. Routing before imposing driver availability

Give each retained request portion $d_v$ opportunities. At every opportunity, split its surviving mass: proportion $\pi_{uv}$ probes driver type $u$, while the remaining proportion skips that opportunity. Success stops the request immediately.

A skipped opportunity is not a probe, so no portion receives more than $d_v$ actual probes.

The success fraction at each opportunity is $z_v/d_v$. Define
$$ h_d(z)=\frac1d\sum_{j=0}^{d-1}\left(1-\frac zd\right)^j. $$
For arrival mass $r_{v,t}$, the resulting successful mass on an edge is
$$ M_{uv,t} =\frac{r_{v,t}}{r_v}\,p_{uv}x_{uv}h_{d_v}(z_v). $$
This follows by summing the edge's success contribution over the surviving masses at all opportunities.

If $z_v=0$, positivity of the acceptance rates forces every incident $x_{uv}$ to be zero, so the same formula remains valid.

Every summand defining $h_d$ is nonincreasing in $z$. Thus, for $0\leq z\leq1$,
$$ 1\geq h_d(z)\geq h_d(1)=q_d>q. $$
For $d=1$, the equality $h_1(1)=q_1=1$ follows directly. For $d>1$, it follows from the geometric sum and the strict inequality $\log(1-1/d)<-1/d$.

2.2. Reserve enough driver mass to prevent retries

Put
$$ D=\max_v d_v,\qquad \theta=1-\frac1{24D}. $$
Reject proportion $1-\theta$ of every arrival before applying the preceding routing law.

We need a quantitative gap above $q$. For $d\geq2$,
$$ \log(1-1/d)\leq-\frac1d-\frac1{2d^2}. $$
Consequently,
$$ q_d-q \geq e^{-1}\left(1-e^{-1/(2d)}\right). $$
For $0\leq t\leq1$, the estimate $e^{-t}\leq1-t+t^2/2$ gives $1-e^{-t}\geq t/2$. Since $e<3$,
$$ q_d-q\geq\frac1{4ed}>\frac1{12d}. $$
For $d=1$, the same weaker bound holds because $q_1-q=1/e>1/12$.

Therefore, whenever $d\leq D$,
$$ \theta q_d \geq q_d-\frac1{24D} >q+\frac1{24D}. $$

The thinned routing law has total edge masses
$$ M_{uv}=\theta p_{uv}x_{uv}h_{d_v}(z_v), $$
and hence
$$ M_{uv}\geq\left(q+\frac1{24D}\right)p_{uv}x_{uv}. $$
It also satisfies
$$ \sum_v M_{uv} \leq\theta\sum_v p_{uv}x_{uv} \leq\theta B_u. $$

Now define
$$ \rho=\min_u(1-\theta)B_u>0,\qquad \eta=\frac{\rho}{2D}. $$
Process stages in order and divide each retained arrival into finitely many batches, each of mass at most $\eta$.

Before a batch, select, for every driver type, $D$ disjoint subsets of currently unmatched drivers, each of mass $\eta$. Use subset $j$ only at opportunity $j$.

The selection is feasible: its total mass per driver type is $D\eta=\rho/2$, whereas at least $\rho$ remains unmatched. The latter assertion is justified inductively. Every executed prefix consumes no more than the total prescribed consumption, which is at most $\theta B_u$; therefore the reserve remains available before the next batch.

At any opportunity, the probing mass on a driver type is at most the batch mass, hence at most $\eta$. It can be paired injectively with drivers in the selected subset. Different opportunities use disjoint subsets, so a request never retries an individual driver. Those subsets are initially unmatched, and earlier opportunities cannot consume drivers in later subsets.

Thus the construction is a finite admissible causal policy. All requests finish in their arrival stage.

We have proved:

Finite routing lemma. Every rational feasible benchmark solution $x$ admits a finite causal policy satisfying, edge by edge,
$$ > \left(q+\frac1{24D}\right)p_{uv}x_{uv} > \leq M_{uv}\leq\theta p_{uv}x_{uv}. > $$

This lemma gives no polynomial bound on the number of executed batches or opportunities.

3. The frontier without a running-time restriction

The common benchmark feasible region is nonempty, closed, and bounded. In particular, each edge variable satisfies
$$ 0\leq x_{uv}\leq\frac{B_u}{p_{uv}}. $$
The profit optimum exists. The fairness optimum exists as well, by introducing a variable $f$ and inequalities
$$ \sum_v p_{uv}x_{uv}\geq fB_u,\qquad 0\leq f\leq1. $$
With rational input, rational optimal solutions can be chosen.

Let $x^P,x^F$ be such optimal solutions. For a rational $\lambda\in[0,1]$, put
$$ x^\lambda=\lambda x^P+(1-\lambda)x^F. $$
Convexity makes this feasible. Nonnegative profits and nonnegative edge masses give
$$ \sum_{uv}w_{uv}p_{uv}x^\lambda_{uv}\geq\lambda P^* $$
and, for every driver type,
$$ \sum_v p_{uv}x^\lambda_{uv}\geq(1-\lambda)F^*B_u. $$

Apply the finite routing lemma and put $k_D=q+1/(24D)$. The resulting policy satisfies
$$ P\geq k_D\lambda P^*,\qquad F\geq k_D(1-\lambda)F^*. $$

If $a+b\leq q$, the interval
$$ \left[\frac a{k_D},\,1-\frac b{k_D}\right] $$
has positive length and lies in $[0,1]$. Choose a rational $\lambda$ inside it. The two required inequalities follow.

Together with Section 1, this proves that the universal attainable region, when running time is disregarded, is exactly
$$ \boxed{\{(a,b)\in[0,1]^2:a+b\leq q\}.} $$
Its Pareto frontier is $a+b=q$.

Zero benchmarks cause no difficulty: the argument never divides by $P^*$ or $F^*$.

4. New result: polynomial-time rational certificates

The exact value of $h_d(z)$ can have exponentially many denominator bits. Nevertheless, a sufficiently accurate one-sided rational approximation is computable in polynomial time. This removes exact outcome representation as an obstacle to certifying the construction.

4.1. A short recurrence for the geometric average

Let
$$ a=1-\frac zd,\qquad S_n=a^n,\qquad H_n=\frac1n\sum_{j=0}^{n-1}a^j. $$
Thus $h_d(z)=H_d$. Starting from $S_1=a,H_1=1$, use
$$ S_{2n}=S_n^2,\qquad H_{2n}=\frac{H_n(1+S_n)}2 $$
and
$$ S_{n+1}=aS_n,\qquad H_{n+1}=\frac{nH_n+S_n}{n+1}. $$
The first pair follows by splitting the geometric sum into two blocks of length $n$; the second appends its last term.

Reading the binary expansion of $d$ computes $(S_d,H_d)$ using doubling and, when needed, incrementing. Let $J$ be the number of updates. Then
$$ J\leq2\lceil\log_2 d\rceil. $$

4.2. Downward rounding and a proved error bound

Fix a dyadic grid spacing $\varepsilon=2^{-K}$. Round $a$ downward to this grid, and round every newly computed $S,H$ downward after each update.

All formulas are nondecreasing in their nonnegative arguments. Inductively, the computed quantities underestimate the exact ones and remain in $[0,1]$.

Let $E$ bound the errors in both current quantities. The rounded value of $a$ has error at most $\varepsilon$.

For doubling, the error in $S^2$ is at most $2E$ before rounding. The error in $H(1+S)/2$ is at most $E+E/2$. Thus both new errors are at most $2E+\varepsilon$.

For incrementing, the error in $aS$ is at most $E+\varepsilon$ before rounding. The normalized average $(nH+S)/(n+1)$ has error at most $E$ before rounding. Thus both new errors are at most $2E+2\varepsilon$.

Initially $E\leq\varepsilon$. After $J$ updates,
$$ E\leq(3\cdot2^J-2)\varepsilon \leq3\cdot2^J\varepsilon. $$
Choose
$$ K=J+\left\lceil\log_2(288D)\right\rceil. $$
The computed dyadic number $\underline h_d(z)$ then satisfies
$$ h_d(z)-\frac1{96D} \leq\underline h_d(z) \leq h_d(z). $$

There are $O(\log d)$ updates. Their rational operands have polynomial bit length: dyadic precision is $O(\log d+\log D)$, and the integer weights have $O(\log d)$ bits. Therefore this computation takes polynomial bit time.

4.3. Certified masses

For the policy constructed from $x$, compute
$$ A_{uv} =\theta p_{uv}x_{uv}\,\underline h_{d_v}(z_v). $$
These are rational numbers of polynomial bit length. The preceding bounds prove
$$ A_{uv}\leq M_{uv} $$
and
$$ A_{uv} \geq \left(q+\frac1{24D}-\frac1{96D}\right)p_{uv}x_{uv} = \left(q+\frac1{32D}\right)p_{uv}x_{uv}. $$

Thus the rational quantities
$$ \underline P=\sum_{uv}w_{uv}A_{uv}, \qquad \underline F=\min_u\frac{\sum_v A_{uv}}{B_u} $$
can be computed in polynomial time and satisfy
$$ P\geq\underline P,\qquad F\geq\underline F. $$

The benchmark LPs have polynomially many variables and constraints, with rational coefficients of polynomial bit length. The standard polynomial-time theorem for rational linear programming therefore computes $x^P,x^F$ in polynomial bit time. Products such as $\Delta_vr_v$ have polynomial bit length despite their potentially large numerical values.

Consequently, for any polynomial-bit-length rational mixture parameter, both the compact routing parameters and the rational lower certificates are computable in polynomial time.

This certifies a potentially long execution; it does not shorten that execution.

5. New result: efficiently computable boundary slopes

Call a fixed real number $\lambda$ polynomial-time computable if, given a positive integer $s$, an algorithm produces a rational approximation within $2^{-s}$ in time polynomial in $s$.

For every such $\lambda\in[0,1]$, a compact policy description and rational lower certificates for
$$ (q\lambda,\ q(1-\lambda)) $$
can be constructed in polynomial time.

To prove this, put
$$ \delta=\frac1{32D},\qquad k=q+\delta, $$
and consider
$$ t=\frac{q\lambda+\delta/2}{q+\delta}. $$
Then $0<t<1$ and
$$ kt=q\lambda+\frac\delta2,\qquad k(1-t)=q(1-\lambda)+\frac\delta2. $$

Compute a rational $\widehat t\in[0,1]$ with
$$ |\widehat t-t|\leq\frac\delta4. $$
This requires only $O(\log D)$ bits of precision. The denominator $q+\delta$ is bounded away from zero, since $e>2$ implies $q>1/2$.

For completeness, $q$ itself is polynomial-time computable: the alternating series
$$ e^{-1}=\sum_{j=0}^{\infty}\frac{(-1)^j}{j!} $$
has truncation error at most the first omitted term. Using $O(s)$ terms gives error at most $2^{-s}$, and the exact truncated sum has polynomial bit length.

Use the rational mixture $x^{\widehat t}$ and the certificates from Section 4. Since $k<1$,
$$ k\widehat t\geq q\lambda+\frac\delta4, \qquad k(1-\widehat t)\geq q(1-\lambda)+\frac\delta4. $$
Therefore
$$ \underline P\geq q\lambda P^*,\qquad \underline F\geq q(1-\lambda)F^*. $$

This extends the compact-construction result beyond rational slopes. Every strict interior pair $a+b<q$ is also covered by a fixed rational mixture parameter: choose rational $\lambda$ satisfying
$$ \frac aq<\lambda<1-\frac bq. $$

Again, these are polynomial construction and certification results, not polynomial execution results.

6. A fully efficient special case: certain acceptance

Suppose every edge has acceptance rate one. For rational guarantee pairs, the polynomial-time region is exactly
$$ \boxed{a+b\leq1.} $$

6.1. Polynomial-time sufficiency

Here the request success constraint is
$$ \sum_u x_{uv}\leq r_v. $$
It implies the patience constraint because $\Delta_v\geq1$.

Any rational feasible $x$ can be realized exactly using one probe per assigned request portion. At stage $t$, route
$$ x_{uv,t}=\frac{r_{v,t}}{r_v}x_{uv} $$
on edge $(u,v)$.

The total assigned request mass at that stage is at most $r_{v,t}$. Also,
$$ \sum_{v,t}x_{uv,t}=\sum_vx_{uv}\leq B_u. $$
When an edge allocation is processed, previous allocations have consumed no more than their prescribed amounts. Thus enough unmatched driver mass remains for the current allocation. Since every probe succeeds, the request stops immediately and no retry is possible.

There are at most $mT$ edge allocations, all with polynomial-bit-length rational masses.

For rational $a,b$ with $a+b\leq1$, use
$$ x=a x^P+(1-a)x^F. $$
Its exact realization satisfies
$$ P\geq aP^*,\qquad F\geq(1-a)F^*\geq bF^*. $$

6.2. Necessity, including an exact tradeoff instance

Take two driver types $H,L$, each of mass one, and two request types $v_1,v_2$, each of mass one, in one stage. All patience values and acceptance rates are one. Use edges
$$ (H,v_1),\qquad(H,v_2),\qquad(L,v_1), $$
with profit one on $(H,v_1)$ and zero elsewhere.

Then $P^*=1$, while $F^*=1$ is attained by matching $H$ to $v_2$ and $L$ to $v_1$.

Every policy satisfies
$$ P=M_{Hv_1},\qquad F\leq M_{Lv_1}, $$
and request capacity gives
$$ M_{Hv_1}+M_{Lv_1}\leq1. $$
Hence $P+F\leq1$. Any simultaneous guarantee must satisfy $a+b\leq1$.

Thus $a+b=1$ is the exact frontier for rational guarantee pairs in this restricted case.

7. Why general polynomial execution is still open

Consider an execution model in which one charged elementary probe pairs request mass injectively with currently unmatched driver mass on a single edge. Under this model, a probe of mass $z$ satisfies $z\leq B_u$.

Even patience one does not prevent exponential execution costs.

Let
$$ d=2^\ell,\qquad B_u=1,\qquad r_v=d,\qquad p_{uv}=\frac1d,\qquad \Delta_v=1,\qquad w_{uv}=1, $$
with one edge and one stage. The feasible benchmark choice $x_{uv}=d$ gives
$$ P^*=F^*=1. $$

Every elementary probe has $z\leq1$, so creates at most $1/d$ successful mass. After $K$ probes,
$$ P=F\leq\frac Kd. $$
For any fixed nonzero pair, put $g=\max\{a,b\}>0$. Its guarantees require
$$ K\geq gd=g2^\ell. $$
The input length is $O(\ell)$, while $m=1$, $\tau=2$, $T=1$, and $\Delta_v=1$. Thus execution is necessarily exponential under this operation model.

Rejecting everything implements $(0,0)$ in polynomial time, so that model has only the trivial universal polynomial-time guarantee.

However, the task does not explicitly require this elementary execution model. A fluid implementation might instead charge for a compressed operation that represents many sequential interactions. The preceding lower bound cannot be applied to such an operation without specifying its semantics and cost.

The construction above now has polynomial-time rational performance certification; the exact-denominator issue therefore does not obstruct certification. What remains unproved is polynomial-time execution of its capacity-respecting, distinct-driver routing, or a different efficient construction achieving the same guarantees.

Accordingly, $a+b=q$ is the proved frontier for attainable masses, but it is not yet a proved polynomial-time frontier for the model in the question.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Overall assessment: partial, with sound substantive progress. The output establishes the unrestricted attainable region and its Pareto frontier, together with polynomial-time construction of compact routing parameters and rational performance lower bounds. It expressly leaves polynomial-time execution unresolved, so it does not settle the frontier requested in USER_TASK.

I found no false mathematical step in the stated partial results. The blocking issue is the missing general polynomial-time policy implementation.

1. Universal impossibility bound

The instance satisfies the input requirements: both driver masses are positive, the request mass is positive, patience is a positive integer, acceptance rates belong to $(0,1]$, and profits are nonnegative.

The substitution
$$ y_H=\frac{x_{Hv}}d,\qquad y_L=\frac{x_{Lv}}d $$
correctly transforms both request constraints into
$$ y_H+y_L\leq1. $$
The driver constraints become $y_H\leq1$ and $y_L\leq N$. Consequently, the stated benchmark values
$$ P^*=1,\qquad F^*=\frac1{N+1} $$
are correct.

The probe-depth argument is valid. Because every actual probe has acceptance rate $1/d$, the mass eligible for another actual probe is at most $(1-1/d)$ times the mass receiving the preceding probe. Rejection and unavailable drivers can only decrease this mass. Since each request receives at most $d$ actual probes,
$$ M_H+M_L\leq1-\left(1-\frac1d\right)^d=q_d. $$
This argument allows arbitrary routing between the two driver types and does not assume a fixed probing sequence.

The guarantee implications are also correct:
$$ M_H\geq a,\qquad M_L\geq\frac{bN}{N+1}. $$
Thus the necessary inequality on this instance follows.

The logarithmic bounds used to establish $q_d\to q$ have the correct signs and ranges. The subsequent choices of finite $d$ and $N$ correctly produce a counterexample whenever $a+b>q$, including when $b=0$.

Assessment: the universal obstruction
$$ a+b\leq1-\frac1e $$
is established independently of running time.

2. Finite causal realization

Routing formula

The definitions of $z_v$ and $\pi_{uv}$ are valid because $r_v>0$ and $d_v\geq1$. Benchmark feasibility gives
$$ 0\leq z_v\leq1,\qquad \sum_u\pi_{uv}\leq1. $$
The remaining routing proportion is therefore nonnegative.

At each opportunity, the successful fraction of surviving request mass is correctly computed as $z_v/d_v$. Summing the edge contributions over the opportunities gives the stated formula
$$ M_{uv,t} =\frac{r_{v,t}}{r_v}p_{uv}x_{uv}h_{d_v}(z_v). $$

Skipping an opportunity does not count as a probe, so using $d_v$ opportunities respects the actual-probe limit. When $z_v=0$, positivity of the acceptance rates indeed forces every incident $x_{uv}$ to vanish.

Bounds on the geometric average

Every summand in $h_d(z)$ is nonincreasing on $[0,1]$. Hence
$$ 1\geq h_d(z)\geq h_d(1)=q_d. $$
The strict inequality $q_d>q$ is correct, with $d=1$ handled separately.

The quantitative estimate is also valid. For $d\geq2$, the logarithmic bound yields
$$ q_d-q\geq e^{-1}\left(1-e^{-1/(2d)}\right). $$
The supplied exponential estimate then gives
$$ q_d-q\geq\frac1{4ed}>\frac1{12d}. $$
The stated weaker bound holds for $d=1$ as well.

Using $d\leq D$ and $q_d\leq1$, the thinning calculation correctly gives
$$ \theta q_d>q+\frac1{24D}. $$
Both edgewise bounds in the finite routing lemma follow.

Availability and distinct drivers

The batching argument successfully addresses driver availability and the prohibition on retrying an individual driver.

The reserve $\rho$ is positive because all $B_u$ are positive. The selected subsets require total mass
$$ D\eta=\frac{\rho}{2} $$
from each driver type, while the construction maintains at least $\rho$ unmatched mass.

The induction is coherent: completed allocations consume their prescribed successful masses, and every partial execution consumes at most the total prescribed consumption for that driver type. This preserves the reserve needed for the next batch.

Within a batch, each opportunity probes at most $\eta$ mass on a driver type. The initially unmatched subsets assigned to different opportunities are disjoint. Thus earlier opportunities cannot consume drivers reserved for later opportunities, and the same request cannot retry a driver.

The number of batches and opportunities is finite, and processing arrivals stage by stage establishes causality. Zero-mass arrivals require no batches.

Assessment: under the expressly stated nonatomic interpretation, the finite routing lemma is valid. It supplies no polynomial bound on execution length, as the prover acknowledges.

3. Frontier without a running-time restriction

The benchmark feasible region is nonempty, closed, and bounded. Positivity of $p_{uv}$ justifies the coordinate bound $x_{uv}\leq B_u/p_{uv}$.

Introducing $f$ with $0\leq f\leq1$ correctly expresses fairness optimization. The upper bound does not exclude an optimum because each driver’s matched fraction is at most one. Rational optimal solutions exist for these rational linear programs.

The convex mixture is feasible. Nonnegative profits justify its profit lower bound, and nonnegative successful masses justify its driverwise fairness lower bound.

For $a+b\leq q$, the interval
$$ \left[\frac a{k_D},\,1-\frac b{k_D}\right] $$
has positive length because $k_D>q$. Its endpoints lie in $[0,1]$, so selecting a rational mixture parameter is justified. This also covers boundary pairs and cases with a zero coordinate.

The resulting policy satisfies both requested inequalities. Zero benchmarks present no division or feasibility problem.

Assessment: the unrestricted attainable region is exactly
$$ \{(a,b)\in[0,1]^2:a+b\leq q\}, $$
with unrestricted Pareto frontier $a+b=q$. This is a valid partial answer, but its sufficiency does not include the required running-time guarantee.

4. Polynomial-time rational lower certificates

The doubling and incrementing recurrences are correct. Reading the binary expansion of $d$ uses at most $2\lceil\log_2d\rceil$ updates; for $d=1$, no update is needed.

Downward rounding preserves underestimation because all recurrence formulas are nondecreasing in their nonnegative arguments. The computed values remain in $[0,1]$.

The error estimates are valid:

Starting with $E\leq\varepsilon$, the stated bound
$$ E\leq(3\cdot2^J-2)\varepsilon $$
follows. The selected precision therefore ensures error at most $1/(96D)$.

The operation count and operand sizes are polynomial in the relevant binary input lengths. Exact division during an increment followed by dyadic rounding does not require storing the exponentially long exact geometric sum.

The certificate calculation correctly yields
$$ A_{uv}\leq M_{uv} $$
and
$$ A_{uv}\geq\left(q+\frac1{32D}\right)p_{uv}x_{uv}. $$
The profit and fairness lower certificates consequently have the claimed direction.

The application of rational linear programming is appropriate: both benchmark formulations have polynomially many variables and constraints, polynomial-length rational coefficients, feasible bounded optimization problems, and rational optimal solutions. Binary-encoded patience does not make the product $\Delta_vr_v$ have superpolynomial bit length.

Assessment: polynomial-time computation of the rational lower bounds is established for the stated polynomial-size routing data. These bounds certify a mathematically defined finite policy; they do not provide a polynomial-time execution procedure.

5. Computable boundary slopes

The definition of a polynomial-time computable fixed real parameter is adequate for this claim.

The transformation defining $t$ gives $0<t<1$ and the stated equalities. The denominator $q+\delta$ is bounded away from zero, so approximating $t$ to the required accuracy uses only polynomial precision.

The alternating-series argument correctly establishes polynomial-time computability of $q$. Polynomially many terms suffice, and the truncated rational sum has polynomial bit length.

Because $k<1$, the error bound for $\widehat t$ preserves the stated margins for both objectives. The certificates therefore prove the boundary guarantees claimed here.

The fixed rational mixture argument for strict interior pairs is also valid, including when one coordinate is zero.

Assessment: the polynomial-time compact-construction claim is supported. Its express distinction from polynomial execution is necessary and correct.

6. Certain-acceptance special case

When all acceptance rates equal one, the success constraint implies the patience constraint because $\Delta_v\geq1$.

The stage allocation formula respects arriving request mass. Total driver allocations stay within capacity, and processing a prescribed allocation leaves sufficient driver mass because all allocations are nonnegative and their total is bounded by $B_u$.

Every assigned portion succeeds on its first probe. Thus patience and no-retry restrictions hold. There are at most $mT$ rational edge allocations of polynomial bit length.

The convex mixture proves sufficiency for the stated rational guarantee pairs.

The tradeoff instance is correct: $P^*=F^*=1$, while every policy satisfies
$$ P+F\leq M_{Hv_1}+M_{Lv_1}\leq1. $$
This proves necessity.

Assessment: the claimed polynomial-time frontier for rational pairs in the certain-acceptance restriction is established within the fluid allocation representation used by the output. It does not settle the general case.

7. Conditional execution lower bound

The lower bound is correct under the explicitly specified elementary-probe model.

An injective probe using currently unmatched driver mass has size at most $B_u=1$. With acceptance rate $1/d$, each such operation produces at most $1/d$ successful mass. The benchmark values are both one, so a fixed nonzero guarantee requires
$$ K\geq g2^\ell. $$
The input has length $O(\ell)$, making this an exponential operation lower bound.

However, injectivity for an entire charged operation is an additional computational-model assumption. The prover correctly acknowledges that the original task does not explicitly specify that assumption or exclude compressed fluid operations.

Assessment: this is a valid conditional result. It cannot establish the polynomial-time impossibility region in USER_TASK.

Blocking issue and minimum additional clarification

Major — general polynomial-time realization remains unproved. The finite policy may execute a number of batches or opportunities exponential in the input length. Polynomial-time generation of parameters and lower certificates does not establish polynomial-time implementation of the guaranteed routing.

To complete the requested answer, the prover must specify the policy representation and charged operations used for the original task, justify that interpretation, and establish the claimed guarantees within a polynomial running-time bound. Alternatively, any computational impossibility claim must apply to that justified model. The conditional model in Section 7 cannot silently supply this missing premise.

This is an acknowledged limitation, rather than a false claim of completion. The unrestricted frontier, certificates, and restricted-case result constitute genuine progress.

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