All missions

Motivation

Online advertising exchanges sell most impressions through second-price auctions with reserve prices. A seller who has logged the bids of many past auctions wants reserves that would have earned the most revenue on that history. When the bids are drawn i.i.d. from a distribution, the revenue-optimal reserves on a large sample approximate the revenue-optimal reserves for the distribution (Morgenstern–Roughgarden 2015, cited in the paper's §2). This makes the data-driven problem the computational core of reserve optimization.

With one reserve per buyer (personalized reserves) in the eager second-price auction, the data-driven problem is APX-hard (Roughgarden–Wang 2016). A $1/4$-approximation was given by Paes Leme, Pál, Vassilvitskii 2016, and the best factor previously known was the $1/2$ of Roughgarden and Wang. Derakhshan, Golrezaei and Paes Leme give a linear-programming relaxation and a randomized rounding that earn a $(1+2(\sqrt2-1)e^{\sqrt2-2})^{-1}\approx0.684$ fraction of the optimum (arXiv:1905.01526; Management Science 2022). They also show that the analysis is tight and that the integrality gap of the relaxation is at least $0.828$.

Setting

There is a finite set $\mathsf A$ of auctions and a finite set $\mathsf B$ of buyers. Buyer $b$ bids $\beta_{a,b}\ge0$ in auction $a$. Two auxiliary buyers $b_0\neq b_{00}$ bid $0$ everywhere. Given a reserve vector $r=(r_b)_{b\in\mathsf B}$, auction $a$ proceeds in two steps:

1. Every buyer with $\beta_{a,b}<r_b$ is removed. The rest form the cleared set $S_a$.
2. If $S_a\neq\emptyset$, a highest bidder $b^\star_a$ of $S_a$ wins and pays

$$\mathrm{Rev}_a(r)=\max\Big(r_{b^\star_a},\ \max_{b\in S_a,\,b\neq b^\star_a}\beta_{a,b}\Big).$$

If $S_a=\emptyset$, then $\mathrm{Rev}_a(r)=0$. The eager second-price problem is

$$\mathsf{ESP}^\star=\max_{r}\ \mathrm{Rev}(r),\qquad \mathrm{Rev}(r)=\sum_{a\in\mathsf A}\mathrm{Rev}_a(r).$$

Let $\mathsf R=\{0,\infty\}\cup\{\beta_{a,b}\}$ be the candidate reserves. A valid profile of auction $a$ is a tuple $p=(b_1,b_2,r_1,r_2)$ with $b_1\neq b_2$, $\beta_{a,b_1}\ge\beta_{a,b_2}$, $r_1\le\beta_{a,b_1}$ and $r_2\le\beta_{a,b_2}$. Its revenue is $\mathrm{Rev}_a(p)=\max(\beta_{a,b_2},r_1)$. The set of valid profiles of auction $a$ is $\mathcal P_a$, and $\mathcal Q_{b,r,a}\subseteq\mathcal P_a$ contains the profiles that give buyer $b$ reserve $r$.

Profile-LP has variables $s_{a,p}\ge0$ (a distribution over profiles of auction $a$) and $q_{b,r}\ge0$ (a distribution over reserves of buyer $b$):

$$\max\ \sum_a\sum_{p\in\mathcal P_a}s_{a,p}\,\mathrm{Rev}_a(p)\quad\text{s.t.}\quad\sum_{p\in\mathcal P_a}s_{a,p}\le1,\quad\sum_{p\in\mathcal Q_{b,r,a}}s_{a,p}\le q_{b,r},\quad\sum_{r\in\mathsf R}q_{b,r}=1.$$

Pro-LPR solves Profile-LP and draws a reserve $r^{\mathcal R}_b$ for each buyer independently with $\Pr[r^{\mathcal R}_b=r]=q^\star_{b,r}$. It then outputs whichever of $r^{\mathcal R}$ and the zero vector earns more.

The analysis passes through the nonlinear program (10). For $n$ buyers, $\mathsf{OPT}(\theta)$ is the maximum of $e^{\theta-1}\big[\prod_i(1-x_i)+\sum_ix_i\prod_{j\neq i}(1-x_j)\big]$ over $x\ge0$ with $\tfrac12\sum_ix_i=\theta$ and $x_i\le\theta$.

Formalization targets

Goal: Theorem 1 with the exact constant

Profile-LP has an optimal solution, and every optimal solution $(s^\star,q^\star)$ satisfies

$$\mathbb E\big[\max(\mathrm{Rev}(r^{\mathcal R}),\mathrm{Rev}(0))\big]\ \ge\ \frac{1}{1+2(\sqrt2-1)e^{\sqrt2-2}}\ \mathrm{Rev}(r)\qquad\text{for every reserve vector }r\ge0.$$

Milestones

The milestones follow the paper's proof:

1. Lemma 4.3. The LP value bounds every $\mathrm{Rev}(r)$ from above.
2. Lemma 5.1. Two per-auction tail conditions, with constant $c$, give a $(1+c)^{-1}$-approximation.
3. Lemma 5.2. The first tail condition holds above $\beta^{(2)}_a$.
4. Lemma 5.3. The second tail condition holds with $c=\max_{\theta\in[0,1]}\mathsf{OPT}(\theta)$.
5. Lemmas 5.7 and 5.8. One-variable inequalities for the two candidate families $\mathsf{OPT}^1(\theta,k)$ and $\mathsf{OPT}^2(\theta,k)$.
6. Corollary 5.6. $\mathsf{OPT}(\theta)$ is at most the larger of the two families.
7. The §5.1 bound. $\mathsf{OPT}(\theta)\le2(\sqrt2-1)e^{\sqrt2-2}$ for all $n\ge2$ and $\theta\in[0,1]$.

Lemma 5.4 remains a supporting draft item for Lemma 5.3.

Significance

The theorem shows that eager personalized reserves can be approximated beyond the factor $1/2$ by a polynomial-size LP. The LP has only $O(|\mathsf A|\,|\mathsf B|^2|\mathsf R|^2)$ profile variables, whereas the search space has $|\mathsf R|^{|\mathsf B|}$ reserve vectors. Lemma 5.1 shows that the rounding can be analyzed auction by auction, and the paper's tightness example shows the constant $0.684$ cannot be improved for this algorithm.

The paper's proof is complete on paper except at one point. Corollary 5.6 relies on Lemma 5.5, a KKT claim that is false as printed: $n=3$, $\theta=\tfrac12$, $x=(0.2,0.3,0.5)$ satisfies the stated KKT system with two unequal interior coordinates. The corollary itself agrees with numerical optimization, but it currently lacks a correct proof. The paper also checks Lemma 5.7 numerically for $3\le k\le39$. A machine-checked development would close both gaps and certify the constant. No part of this result is formalized elsewhere.

Difficulty

Lemma 4.3 and Lemma 5.2 are close to direct counting arguments. The difficulty lies in Lemma 5.3 and the bound on $\mathsf{OPT}$. Lemma 5.3 must compare the LP's profile mass with the probability that independently rounded reserves produce two cleared bids above $t$. The LP couples buyers only through the marginals $q_{b,r}$, and the comparison must hold for every optimal solution.

Bounding $\mathsf{OPT}(\theta)$ is a nonconvex optimization over the simplex-like region of (10), for every $n$. The printed reduction to two symmetric families uses a KKT argument that does not hold, so a different argument is needed: a symmetrization or smoothing argument, or a direct inequality. Lemma 5.7 is tight at $k=2$, $\theta=\sqrt2-1$, so its bound leaves no slack, and the paper's numerical range of $k$ has to be covered by analysis.

Formalization scope

All statements live in the namespace ReserveLP.ProLPR and share one definition file, ReserveLP.ProLPR.Model. The formalization fixes these conventions:

1. Numbers. All values are real numbers.
2. The reserve $\infty$. It is encoded by the sentinel $1+\sum_{a,b}\beta_{a,b}$, which lies strictly above every bid, so a buyer with this reserve never clears.
3. Ties. $\mathrm{Rev}_a(r)$ is the maximum over all highest cleared bidders, which equals the value for any tie-breaking.
4. Empty maxima. An empty second-price maximum counts as $0$.
5. Second highest bid. $\beta^{(2)}_a$ is the largest $\min(\beta_{a,b},\beta_{a,b'})$ over $b\neq b'$.
6. Valid profiles. They require $b_1\neq b_2$, which Definition 4.1 omits. The paper's reading of profiles as the highest and second highest cleared bidders needs it, and without it Theorem 1 is false on one auction with bids $(1,0,0)$.
7. $q\ge0$. The constraint $q_{b,r}\ge0$ appears on p. 7 and is included in the LP.
8. Probability. Probabilities and expectations are finite sums over $\mathsf R^{\mathsf B}$ with product weights. No measure theory is involved.
9. The benchmark. $\mathsf{ESP}^\star$ is replaced by "for every reserve vector $r\ge0$". Reserves are taken nonnegative, since a negative reserve would let a lone winner pay a negative price under the paper's formula.
10. $\mathsf{OPT}$. $\mathsf{OPT}(\theta)$ and $c$ are real suprema over nonempty sets that are bounded above, for $n\ge2$ and $\theta\in[0,1]$.
11. Running time. "Polynomial time" is not formalized.

The goal includes the existence of an optimal LP solution, so the guarantee is not vacuous. The goal compares against every reserve vector, not against the LP value. It uses the expectation of the per-realization better vector, not the larger of the two expectations. It uses the exact constant $(1+c^\star)^{-1}$, not $\max_\theta\mathsf{OPT}(\theta)$.

A complete development needs several ingredients:

• finite-sum manipulations of the product distribution: marginals, and independence across buyers;
• the integral identity $\sum_p s_p\,\mathrm{Rev}(p)=\int_0^\infty\sum_{\mathrm{Rev}(p)\ge t}s_p\,dt$ and its probabilistic counterpart, which can also be done as a finite layer-cake sum over the values in $\mathsf R$;
• compactness of the LP feasible region;
• one-variable calculus for Lemmas 5.7 and 5.8.

The layer-cake sums and the product-measure marginals are reusable beyond this mission. Contributions are welcome on any milestone, especially a correct proof of Corollary 5.6.

Selected references

• M. Derakhshan, N. Golrezaei, R. Paes Leme, LP-based Approximation for Personalized Reserve Prices, arXiv:1905.01526v5, 2020; published as Linear Program-Based Approximation for Personalized Reserve Prices, Management Science 68(3), 2022. https://arxiv.org/abs/1905.01526
• T. Roughgarden, J. R. Wang, Minimizing Regret with Multiple Reserves, EC 2016. https://doi.org/10.1145/2940716.2940775
• R. Paes Leme, M. Pál, S. Vassilvitskii, A Field Guide to Personalized Reserve Prices, WWW 2016. https://doi.org/10.1145/2872427.2883071
• J. Morgenstern, T. Roughgarden, On the Pseudo-Dimension of Nearly Optimal Auctions, NeurIPS 2015. https://arxiv.org/abs/1506.03684

Why the game matters

In a buck-passing game, each participant chooses who will receive a task, burden, or token next. The eventual share of time spent holding it depends on every participant's choice. This makes a small network into a game: a local change of one outgoing edge can alter the long-run burden across an entire part of the network. Cominetti, Quattropani, and Scarsini study this setting in The Buck-Passing Game, including deterministic and stochastic versions. The deterministic result targeted here says that players can choose their outgoing edges without knowing where the buck will start and still reach a pure Nash equilibrium.

That independence from the starting distribution matters because an initial probability law can be unknown or disputed. A Nash equilibrium found for one chosen law may cease to be an equilibrium under another. The paper calls a profile that works for every law a prior-free Nash equilibrium. Its existence is the subject of Theorem 2 on p. 10 of arXiv:1808.03206v4.

The deterministic setting

Start with a finite directed graph $G=(V,E)$ without loops. Each vertex $i$ is a player and has a nonempty set $N_i^+$ of outgoing neighbors. Player $i$ chooses one neighbor $s_i\in N_i^+$; the collection $s=(s_i)_{i\in V}$ is a strategy profile. Once these choices are fixed, the graph becomes a functional graph: from each vertex there is exactly one selected outgoing edge, and the buck moves according to the map $f_s(i)=s_i$.

At time zero, Nature places the buck at a vertex drawn from a probability distribution $\mu$ on $V$. At time $t\geq1$, the buck is at $f_s^t(j)$ if it started at $j$. The cost $c_i(s)$ of player $i$ is the expected limiting fraction of positive times for which $i$ holds it. Players minimize their own costs. The definition follows equation (3) on p. 6: for each possible start $j$, count visits at times $1,\ldots,T$, divide by $T$, take the limit, and average the resulting value with weights $\mu_j$.

Every orbit on a finite functional graph eventually enters a directed cycle. The vertices whose orbits enter the same cycle form its basin, called a unicycle in the paper. The cycles $C_s^\ell$ are pairwise disjoint, and their basins $A_s^\ell$ partition the vertices. Equation (6) on p. 7 says that a player outside a cycle has zero long-run cost, while a player on cycle $C_s^\ell$ has cost $\mu(A_s^\ell)/|C_s^\ell|$. A unilateral change is profitable when it strictly lowers the changing player's cost; a profile with no profitable change is a pure Nash equilibrium. Definitions 1–3 and equations (3)–(6) fix these terms.

Formalization targets

The main target is Theorem 2. The order of its quantifiers is essential: one profile must work for every initial probability distribution. Writing $\Delta(V)$ for the probability distributions on $V$, the claim is

$$\exists s\in\prod_{i\in V}N_i^+\quad\forall\mu\in\Delta(V)\quad\forall i\in V\quad\forall x\in N_i^+,\qquad c_i(s)\leq c_i(x,s_{-i}).$$

The proposed milestones match the claims leading up to this result in §3.1 of the paper. A component-wise minimizer of a generalized ordinal potential is a Nash equilibrium. Proposition 1 guarantees an equilibrium for a finite generalized ordinal potential game and also for the compact, lower semicontinuous case. Equation (6) identifies costs from the limiting visit frequencies. The p. 9 classification describes the two types of profitable deviation. Theorem 1 supplies a generalized ordinal potential that depends only on the selected cycles:

$$\Psi(s)=\sum_{\ell=1}^{M(s)}\bigl(|V|-|C_s^\ell|\bigr),\qquad c_i(x,s_{-i})<c_i(s)\;\Longrightarrow\;\Psi(x,s_{-i})<\Psi(s).$$

The full-support assertion in the second sentence of Theorem 1 is outside this mission's milestone list. The existence target uses its first assertion. Theorem 3's bound on improvement-path length and the paper's stochastic, constrained, and buck-holding games are also outside this target.

What the result provides

Theorem 2 guarantees a pure strategy profile with stability across all starting distributions, including distributions concentrated at a single vertex. It strengthens the statement that each fixed distribution has some equilibrium, which could choose a different profile each time. In this deterministic model the same strategy choices serve all initial laws. The paper's proof ties that claim to a graph quantity, $\Psi$, whose value has no $\mu$ parameter. Theorems 1–2, pp. 9–10 state the potential and equilibrium conclusions.

The research result is already proved in the paper. The work here is to give its definitions and statements precise Lean types and to establish machine-checked proofs of the limit identity, graph-change classification, potential property, and existence theorem. The drafted theorem files currently contain sorry, so their compilation checks statement well-formedness rather than proving the claims. The finite cost-game definitions and orbit-frequency statement can also support later formalizations of deterministic dynamics and potential games.

Where the proof is difficult

A finite orbit is eventually periodic, but the cost is defined using a limit of averages from time $1$ through $T$. The formal development must establish that limit for every initial vertex before substituting the cycle-and-basin formula. It must then track what a one-player change does to the cycles of a functional graph. The changed edge can lengthen one cycle or remove it by sending its vertices toward a different cycle; costs also depend on how much initial mass reaches the affected basin. Merely knowing that a player's new out-neighbor is in the same basin does not show an improvement, because the new cycle may be shorter or unchanged. These are the concrete issues behind equation (6) and Theorem 1.

Formalization scope

Lean gives the general cost-game predicates their own definition module. The deterministic model represents $V$ by a finite type, with the paper's loopless and nonempty out-neighborhood assumptions bundled into BPGraph. A strategy is an out-neighbor subtype, so every profile selects only legal edges. The distribution is a real vector with nonnegative coordinates summing to one. Costs and the potential are real-valued. The cost is built from the orbit's Cesàro limit in equation (3); equation (6) is a separate theorem asserting convergence and the resulting value. Cycles are finite sets of periodic points, deduplicated so that $\Psi$ has exactly one summand per cycle; basins contain the vertices whose orbits reach that cycle. Classical decidability constructs these finite sets.

The empty vertex type is permitted by the Lean representation; it has one empty strategy profile and no probability distribution. A one-vertex graph cannot satisfy both the loopless and nonempty out-neighborhood assumptions. The prior-free goal explicitly places the profile before the quantifier over distributions. Defining cost by the cycle formula, or choosing a separate equilibrium after seeing each distribution, would change the target. Proposition 1 makes nonempty strategy sets explicit, as an empty compact strategy set has no profile. The first profitable-deviation case requires that the changed edge lengthen the cycle; membership in the basin alone does not do so.

The development needs reusable results on finite function iteration, periodic points, Cesàro frequencies, finite products, and lower semicontinuous minimization. The goal and its milestones invite proofs of those statements under the recorded hypotheses. All mission items are drafted locally and remain unproved until solvers supply proofs.

Selected references

• R. Cominetti, M. Quattropani, and M. Scarsini, The Buck-Passing Game, Mathematics of Operations Research, 2022. arXiv:1808.03206v4. The formalization cites the version 4 preprint's pages and numbering.

Motivation

In atomic dynamic routing, indivisible agents (vehicles, packets, travellers) enter a network over time and travel along fixed routes. Each road admits a limited number of agents per unit of time, so agents queue at its entrance. A basic question for traffic models, packet-switching networks and dynamic routing games is how long an agent can stay in the network, its residence time. Upper bounds on residence times are what make it possible to bound queue lengths and the price of anarchy in dynamic routing games.

Greedy packet scheduling, where an edge never idles while packets wait for it, was studied by Cidon, Kutten, Mansour and Peleg (SIAM J. Comput. 1995), who showed that cycles can make delays large, and by Mansour and Patt-Shamir (J. Algorithms 1993), who bounded delivery times when every route is a shortest path. Cao, Chen, Chen and Wang (MOR 2022) prove a bound for arbitrary routes on acyclic networks. It holds under any rule that decides which waiting agent may leave next, and agents may keep entering forever. Their Theorem 1 is the goal of this mission. The paper then uses it to show that equilibria of three dynamic routing games on series-parallel networks have bounded queues (§6).

Setting

A network $G=(V,E)$ is a finite directed multigraph (parallel edges allowed) that is acyclic. Every edge has unit length and unit capacity. A path is a sequence of edges, each starting where the previous one ends. $L_{vw}$ is the number of edges of a longest $v$-$w$ path.

Time is discrete, $0,1,2,\dots$. Agents form a set $\Delta$, possibly infinite. At each time finitely many agents enter. Agent $i$ enters at time $r_i$ at his origin $o_i$ and follows a fixed route, a nonempty $o_i$-$d_i$ path. The tail of each edge holds a buffer. Two rules govern the dynamics:

• (A1) an agent reaching a vertex that is not his destination enters the buffer of his next edge at once;
• (A2) at every integer time, whenever a buffer is nonempty, exactly one agent leaves it and reaches the head of the edge one time unit later; the others wait.

No rule says which agent leaves. Every choice consistent with (A2) is an admissible run. An agent exits $G$ on reaching his destination. His residence time is his exit time minus his entry time (Definition 1).

Fix a focal agent $\zeta$ with entry time $r$. $G_\zeta$ is the subnetwork formed by all $o_\zeta$-$d_\zeta$ paths. For an integer time $r_0$:

• $A_{\zeta,p}$ is the set of agents who enter after time $r$ and use an edge of $G_\zeta$;
• $B_{\zeta,p}(r_0)$ is the set of agents $i\neq\zeta$ who entered by time $r$, are still inside $G$ at time $r_0$, and use an edge of $G_\zeta$.

An agent exits $G_\zeta$ when he reaches the head of the last edge of his route lying in $G_\zeta$.

Formalization targets

Goal: Theorem 1 (p. 7)

For every admissible run and every integer $r_0\ge r$: if no agent of $A_{\zeta,p}$ exits $G_\zeta$ before $\zeta$ exits $G$, then

$$t_\zeta\ \le\ r_0+L_{o_\zeta d_\zeta}+\bigl|B_{\zeta,p}(r_0)\bigr|,$$

where $t_\zeta$ is the exit time of $\zeta$.

Milestones (§3.2, p. 9)

When $\zeta$ is still inside $G$ at $r_0$, the proof follows tokens: imaginary markers that $\zeta$ produces from time $r_0$ on, and that travel with the agents leaving buffers ((s1), (s2), p. 8). The milestones are the paper's statements about them, with $L=L_{o_\zeta d_\zeta}$:

1. (p1) each agent holds at most one token, and a buffer never contains more tokens than agents;
2. (p2) the agent leaving $\zeta$'s buffer always holds exactly one token;
3. (p3) after $r_0$, $\zeta$ produces a new token only while he waits;
4. Claim 1 the induction step of Lemma 1 at the vertices where token $k$ departs right after a smaller token;
5. Lemma 1 token $k$ departs every vertex $v$ of its trail inside $G_\zeta$ by time $r_0+(L-L_{vd_\zeta}+k-1)$;
6. token exit token $k$ exits $G_\zeta$ by time $r_0+(L+k-1)$.

Significance

The result. The bound does not depend on the rule that selects the leaving agent, so it covers every queueing discipline at once: FIFO, global agent priorities, and the edge-priority rules of earlier dynamic routing games. With $r_0=r$ and no later entrants on $G_\zeta$, it gives Corollary 1: the residence time of $\zeta$ is at most $L_{o_\zeta d_\zeta}+|B_{\zeta,p}(r)|$. Example 1 (p. 8) shows that the bound can be attained. The freedom in $r_0$ is what §6 uses to show that queue lengths stay bounded at equilibria of dynamic routing games on series-parallel networks.

Formalizing it. The theorem is proved on paper. No machine-checked version is known to exist, and the platform has no rule-free model of atomic dynamic routing. The mission adds that model: a run is a set of leave times constrained by (A1)–(A2), not a fixed simulation. It also adds the multi-token process and the paper's chain of statements leading to Theorem 1.

Difficulty

The obvious argument is wrong. One might reason that $\zeta$ travels at most $L_{o_\zeta d_\zeta}$ edges and each earlier agent delays him at most once, giving the bound at once. The paper notes (p. 7) that this intuition fails even with two agents: a single agent can delay $\zeta$ more than $|\Delta|$ times, because delays propagate through other buffers. Bounding the total therefore means tracking chains of delays across the network rather than charging each delay to one agent.

Formally, the hard parts are:

• the run is only constrained, not determined;
• the token process is defined by recursion over time, using the unique leaver of each buffer;
• (p1)–(p3) are invariants proved by induction on time;
• Lemma 1 combines induction on the token index with longest-path inequalities in an acyclic graph.

Formalization scope

• Model. Network V E (tail and head maps) with finite V, E and a hypothesis Acyclic: no nonempty closed walk. Paths are edge lists. longest v w is the supremum of path lengths in $\mathbb N$; it is a maximum wherever it is used.

• Runs. RunData holds entry times, routes, origins and destinations, and leave times leave i j in $\mathbb N\cup\{\infty\}$ for the $j$-th edge of $i$'s route, numbered from $0$. IsADR states that:

  • routes are nonempty origin–destination paths;
  • finitely many agents enter per time;
  • nobody leaves a buffer before entering it;
  • (A2) holds, as unique existence of the leaver of each nonempty buffer at each time.

  Agents form an arbitrary type and may be infinitely many. An agent may never be served (leave time $\infty$), as in the paper, so the theorem also asserts that $\zeta$ exits.

• Derived objects. Exit times, $G_\zeta$, $A_{\zeta,p}$, $B_{\zeta,p}(r_0)$ and the exit time from $G_\zeta$ are definitions computed from the run, never free parameters. $|B_{\zeta,p}(r_0)|$ is Set.ncard of a set that is finite under IsADR.

• Tokens. The token milestones assume that $\zeta$ is inside $G$ at $r_0$, as §3.1 requires when starting the construction. Tokens are indexed from $1$. A new token gets index one plus the number produced so far. Bounds with subtraction are written additively over $\mathbb N$, e.g. $s+L_{vd_\zeta}+1\le r_0+L+k$, which is the same inequality over the integers.

• Ruled out. None of these is used, since each proves a different statement: a fixed tie-breaking rule (FIFO or priorities), exit times as free parameters, finitely many agents, or dropping acyclicity, which Remark 2 shows is necessary.

Contributions welcome: proofs of the token invariants, of Lemma 1, and of the goal. The network and run definitions can be reused for the paper's other results (Theorem 2 on uniform capacities, the routing games of §5–6).

Selected references

• Z. Cao, B. Chen, X. Chen, C. Wang, Bounding residence times for atomic dynamic routings, Mathematics of Operations Research, 2022 (accepted manuscript: WRAP 160244). https://doi.org/10.1287/moor.2021.1242 , https://wrap.warwick.ac.uk/160244
• Y. Mansour, B. Patt-Shamir, Greedy packet scheduling on shortest paths, Journal of Algorithms 14(3):449–465, 1993.
• I. Cidon, S. Kutten, Y. Mansour, D. Peleg, Greedy packet scheduling, SIAM Journal on Computing 24(1):148–157, 1995.
• T. Harks, B. Peis, D. Schmand, B. Tauer, L. Vargas Koch, Competitive packet routing with priority lists, ACM Transactions on Economics and Computation 6(1):4:1–4:26, 2018.

Motivation

We present a bouquet of continuity bounds for quantum entropies, falling broadly into two classes: First, a tight analysis of the Alicki-Fannes continuity bounds for the conditional von Neumann entropy, reaching almost the best possible form that depends only on the system dimension and the trace distance of the states. Almost the same proof can be used to derive similar continuity bounds for the relative entropy distance from a convex set of states or positive operators. As applications we give new proofs, with tighter bounds, of the asymptotic continuity of the relative entropy of entanglement, $E_R$, and its regularization $E_R^\infty$, as well as of the entanglement of formation, $E_F$. Using a novel "quantum coupling" of density operators, which may be of independent interest, we extend the latter to an asymptotic continuity bound for the regularized entanglement of formation, aka entanglement cost, $E_C=E_F^\infty$. Second, analogous continuity bounds for the von Neumann entropy and conditional entropy in infinite dimensional systems under an energy constraint, most importantly systems of multiple quantum harmonic oscillators. While without an energy bound the entropy is discontinuous, it is well-known to be continuous on states of bounded energy. However, a quantitative statement to that effect seems not to have been known. Here, under some regularity assumptions on the Hamiltonian, we find that, quite intuitively, the Gibbs entropy at the given energy roughly takes the role of the Hilbert space dimension in the finite-dimensional Fannes inequality.

This mission is the statement-level formalization of Tight uniform continuity bounds for quantum entropies: conditional entropy, relative entropy distance and energy constraints (arXiv:1507.07775v6). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Remark 3: explicit near-tightness example for Lemma 2 (Remark 3: explicit near-tightness example for Lemma 2, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

12 results of the paper are not stated yet, because the library lacks an interface they need:

• Lemma 2: almost tight conditional entropy continuity (paper headline): Normalized trace-class bipartite states, partial traces, extended conditional entropy, common-basis qc/cq predicates (hard)
• Corollary 4: continuity of entanglement of formation and entanglement cost: Countable exact pure-state ensembles, entanglement of formation, and its tensor-power regularization with an infinite factor (hard)
• Remark 6: separable infinite-dimensional extension of Proposition 5: Trace-class tensor-square states, Hilbert-Schmidt vectorization, marginals, basis transpose and root fidelity (hard)
• Corollary 8: continuity of relative entropy of entanglement and its regularization: Infinite-factor Umegaki relative entropy, closed separable-state set, E_R and E_R-infinity (hard)
• Proposition 14: quantum coupling with large operator norm: Arbitrary separable trace-class couplings, tensor marginals and operator norm (hard)
• Lemma 15: energy-constrained entropy continuity by coupling: Arbitrary finite-energy trace-class states, full spectral entropy, trace distance and quadratic-form energy (hard)
• Meta-Lemma 16: adjustable-cutoff energy-constrained entropy continuity: Arbitrary finite-energy trace-class states and their spectral entropy and trace distance (hard)
• Meta-Lemma 17: energy-constrained conditional entropy continuity: Infinite-dimensional bipartite trace-class states with finite-A-entropy conditional extension and A-only form energy (hard)
• Eq. (19): oscillator Gibbs entropy bound and equal-allocation maximization: A correct optimizing equality for the unequal-frequency allocation simplex (source-ambiguity)
• Lemma 18: explicit harmonic-oscillator entropy and conditional entropy bounds: Full Fock trace-class input states, oscillator quadratic-form energy, and arbitrary-ancilla conditional entropy (hard)
• Remark 19: large-energy sharpness of oscillator leading coefficients: Actual mixed Fock witnesses, Gibbs purification, trace distance and conditional entropy, plus large-energy comparison (hard)
• Unnumbered consequence: uniform continuity at each fixed energy: A trace-distance state domain of arbitrary bounded-energy densities and uniform-in-B conditional entropy (hard)

Selected references

• Tight uniform continuity bounds for quantum entropies: conditional entropy, relative entropy distance and energy constraints, arXiv:1507.07775v6, https://arxiv.org/abs/1507.07775v6

Motivation

The squashed entanglement of a quantum channel is an additive function of quantum channels, which finds application as an upper bound on the rate at which secret key and entanglement can be generated when using a quantum channel a large number of times in addition to unlimited classical communication. This quantity has led to an upper bound of $\log((1+\eta)/(1-\eta))$ on the capacity of a pure-loss bosonic channel for such a task, where $\eta$ is the average fraction of photons that make it from the input to the output of the channel. The purpose of the present paper is to extend these results beyond the single-sender single-receiver setting to the more general case of a single sender and multiple receivers (a quantum broadcast channel). We employ multipartite generalizations of the squashed entanglement to constrain the rates at which secret key and entanglement can be generated between any subset of the users of such a channel, along the way developing several new properties of these measures. We apply our results to the case of a pure-loss broadcast channel with one sender and two receivers.

This mission is the statement-level formalization of Bounds on entanglement distillation and secret key agreement for quantum broadcast channels (arXiv:1503.08139v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Thermal-entropy difference: monotonicity and finite or infinite limit (§7, paragraph containing (7.18), PDF p. 28). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

11 results of the paper are not stated yet, because the library lacks an interface they need:

• Abstract seed pinned to Theorem 12, §5: simultaneous eight-rate outer bound: Operational eight-rate broadcast achievability and computed channel-output squashed measures (hard)
• Lemma 3: characterization by squashing a fixed purification: Unrestricted-extension and fixed-purification squashing definitions (hard)
• Lemma 6 (Subadditivity): Both computed squashed measures on three marginals/groupings of one pure state (hard)
• Lemma 7: monotonicity under grouping: Same-state tensor regrouping and both computed squashed measures (hard)
• Lemma 8: reduction for a product party: Tensor-product density states and computed unrestricted-extension measures (hard)
• Unnumbered §3.4: four cut bounds for the eight-factor ideal target, (3.62)–(3.71): Independent eight-factor GHZ/private target and its grouped measures (hard)
• Lemma 11: resource lower bound across every nontrivial partition: Subset-indexed independent quantum-resource target and computed grouped measures (hard)
• Theorem 13, §6: all-partition m-receiver outer bound: Subset-rate broadcast protocols and one pure witness for every partition (hard)
• Unnumbered §7: both output-entropy bounds and finite-energy bounds, (7.11),(7.17),(7.23),(7.28): Fock broadcast dilation, environmental beamsplitter and actual conditional output entropies (hard)
• Proposition 14: optimized photon-number independent broadcast squashed-entanglement bound: Computed Fock-channel squashed-measure suprema and boundary-aware optimization (hard)
• Theorem 15: four explicit two-receiver bosonic rate bounds: Operational bosonic eight-rate protocols and corrected vacuum passive splitter (hard)

Selected references

• Bounds on entanglement distillation and secret key agreement for quantum broadcast channels, arXiv:1503.08139v2, https://arxiv.org/abs/1503.08139v2

Motivation

Large manufacturers procure components by competitive bidding, and many of them also run cost-reduction investigations: the buyer's engineers visit a supplier's plant and look for process changes that lower the cost of the contracted part. The savings are passed to the buyer as a lower contract price. In practice such investigations usually happen after the contract is awarded, on the winner only. Chen, Beil and Duenyas (Operations Research 70(6), 2022) compare that convention with a mechanism in which the buyer investigates before the award, possibly several suppliers, and then awards the contract on the investigated prices.

Investigating before the award obviously helps the buyer for fixed bids: she sees more cost reductions before choosing. The question is whether suppliers lose. The buyer keeps every identified saving, and investigations of competitors make their prices more aggressive, so suppliers seem to have reason to resist. The paper shows that, when suppliers are ex ante symmetric, they do not: every supplier's ex ante expected profit is at least as high when investigations come before the award. This mission formalizes that result.

Setting

A buyer procures one contract from suppliers $\mathcal N=\{1,\dots,N\}$ and must transact with one of them. Supplier $i$ has a private cost $c_i=\Delta^c_i+\epsilon^c_i$, where $\Delta^c_i\ge0$ is public and $\epsilon^c_i$ has density $f$ on $[\underline c,\bar c]$ with mean $0$; so $c_i$ has density $f_i(c)=f(c-\Delta^c_i)$, c.d.f. $F_i$, and support $C_i=[\underline c_i,\bar c_i]$. Costs are independent.

An investigation of supplier $i$ costs the buyer $d\ge0$ and reveals a cost reduction $t_i=\Delta^t_i+\epsilon^t_i\ge0$, where $\epsilon^t_i$ has density $g$ on $[\underline t,\bar t]$ with mean $0$, independently of everything else. At most $\hat N\in\{1,\dots,N\}$ suppliers can be investigated, and costs always exceed reductions: $\Delta^t_i+\bar t<\Delta^c_i+\underline c$. Each supplier submits a sealed bid $b_i\in B_i=[0,\bar c_i]$. If an investigated supplier wins, he is paid his updated bid $b_i-t_i$ and his cost becomes $c_i-t_i$, so his margin is $b_i-c_i$ in every case.

• BAI (bid, award, investigate). The buyer awards the contract to the lowest $\lambda_i=b_i-r_i$, where $r_i=\max\{0,\Delta^t_i-d\}$ is the expected saving from investigating the winner afterwards. Ties are broken at random.
• BIA (bid, investigate, award). The buyer investigates sequentially. Each round she uses the bids and the reductions revealed so far to stop or to investigate one more supplier, and stopping is final. She then awards the contract to the lowest updated bid. Her policy minimizes the expected payment plus investigation cost, problem (1). Theorem 1 solves (1) by an index policy: with $\tau$ the root of $d=\int_\tau^\infty(\epsilon^t-\tau)\,dG(\epsilon^t)$, each supplier gets the index $\mu_i(b_i)=b_i-\max\{0,\tau+\Delta^t_i\}$. The buyer investigates in increasing order of index while the current lowest updated bid is at least the next index, up to a cap $\bar N\le\hat N$.

Supplier $i$'s winning probability at bids $b$ is $W_i(b)$, over $t$ and the tie-break. With the others bidding $\beta_{-i}(c_{-i})$, his expected profit from bidding $b$ at cost $c$ is $u_i(b;c)=(b-c)\,\mathbf E_{c_{-i}}[W_i(b,\beta_{-i}(c_{-i}))]$, equation (5). A Bayesian Nash equilibrium is a profile of strategies $\beta_i:C_i\to B_i$ that are best replies at every type. Supplier $i$'s ex ante expected profit is $\mathbf E_{c_i}[u_i(\beta_i(c_i);c_i)]$.

Formalization targets

Goal: Theorem 2 (weak form)

Suppose that suppliers are ex ante symmetric ($\Delta^c_i=\Delta^c$, $\Delta^t_i=\Delta^t$), that $F_i/f_i$ is nondecreasing (Assumption 1), and that $d<\max_i\Delta^t_i$ (Assumption 2). Let $\beta^{\mathrm{BIA}}$ be a symmetric equilibrium of BIA, and $\beta^{\mathrm{BAI}}$ a symmetric nondecreasing equilibrium of BAI. Then for every supplier $i$,

$$\mathbf E_{c_i}\big[u^{\mathrm{BAI}}_i(\beta^{\mathrm{BAI}}_i(c_i);c_i)\big]\;\le\;\mathbf E_{c_i}\big[u^{\mathrm{BIA}}_i(\beta^{\mathrm{BIA}}_i(c_i);c_i)\big].$$

Milestones

1. Proposition 1. There exists an equilibrium $\check\beta$ of the first-price auction with costs $c_i-r_i$ whose shifted strategy $\tilde\beta_i(c_i)=\check\beta_i(c_i-r_i)+r_i$ is a BAI equilibrium.
2. Theorem 1(a). The index policy (3) minimizes the buyer's expected cost (1) over all admissible sequential policies, for every bid vector.
3. Zero profit at the top. $U^{\mathcal M}_i(\bar c_i)=0$ for $\mathcal M\in\{\mathrm{BIA},\mathrm{BAI}\}$.
4. Envelope formula (A.2). $U^{\mathcal M}_i(c_i)=U^{\mathcal M}_i(\bar c_i)+\int_{c_i}^{\bar c_i}\phi^{\mathcal M}_i(y)\,dy$.
5. Ex ante identity. $\mathbf E_{c_i}[U^{\mathcal M}_i(c_i)]=U^{\mathcal M}_i(\bar c_i)+\mathbf E_{c}\big[A^{\mathcal M}_i(c)\,F_i(c_i)/f_i(c_i)\big]$.
6. Pointwise comparison. At cost vector $c$ and realized reduction vector $t$, $\sum_i A^{\mathrm{BAI}}_i(c) F_1(c_i)/f_1(c_i)=\min_i F_1(c_i)/f_1(c_i)\le\sum_i A^{\mathrm{BIA}}_i(c,t) F_1(c_i)/f_1(c_i)$ almost everywhere, with $\sum_iA^{\mathcal M}_i=1$.

Significance

The theorem identifies a win-win procurement design. With symmetric suppliers, a buyer who chooses the cheaper of BAI and BIA weakly lowers her own cost, and this choice never lowers any supplier's ex ante profit. The gain does not come from sharing savings, since the buyer keeps all identified savings. It comes from strategic bidding: under BIA a supplier need not submit the lowest initial bid to win, so price competition at the bid stage softens. The paper's Figure 1 shows the higher BIA bid curves. Theorem 1 is of independent interest: it is an index solution of a capped sequential search problem in which an uninvestigated bid may still win.

The paper proves the result on paper. To our knowledge none of it is machine-checked. A formalization adds three things. It makes the mechanisms precise, including the tie-breaking and the stopping rule that the text leaves partly implicit. It pins down the right inequality: the printed "higher" is not strict, and with a single supplier both mechanisms give the same profit. It also produces reusable components: an envelope-theorem layer for bidding games with an indirect mechanism, and a capped-search index theorem.

Difficulty

The proof of Theorem 2 needs the BIA winning probability only through its total, $\sum_i A^{\mathrm{BIA}}_i=1$. Everything else rests on three technical steps. The first is the envelope formula (A.2) for an indirect mechanism whose allocation $W_i$ has no closed form and need not be continuous in the bid. The usual argument assumes a differentiable direct mechanism and does not apply as stated. The second is the claim that in BAI the lowest-cost supplier wins almost surely. That needs a symmetric equilibrium that is not merely nondecreasing but free of pooling, and this must be derived from the equilibrium conditions. The third is the "by symmetry" step that equates each supplier's ex ante profit with the average over suppliers. It needs both the equilibria and the mechanisms to be invariant under relabelling the suppliers.

Theorem 1(a) is a dynamic program over adaptive policies with a cap and an outside option. A Weitzman-style argument must handle a cap $\bar N$ and suppliers whose index makes investigation worthless ($\tau_i=0$). It cannot simply be imported from Pandora's-box results.

Formalization scope

Suppliers are Fin N with $N\ge1$; all values are real numbers. A single definitions module PreAwardInvest.WinWin.Model contains the following.

• Parameters and assumptions. The parameters, and the standing assumptions of §3.1 (densities with mean zero, nonnegative costs and reductions, footnote 6, $1\le\hat N\le N$, $d\ge0$), with $f>0$ on $(\underline c,\bar c)$ added. Assumptions 1 and 2 are separate predicates.
• Laws. The cost and reduction laws are densities with respect to Lebesgue measure, and their vectors have product laws.
• Policies. A policy reads the bids, the investigated set and the revealed reductions. An admissible policy is nonanticipative and measurable in the reductions, and stopping is final.
• Index policy. It takes $\tau$ as any root of its equation. Ties in the ranking and in both awards are broken by one uniformly random priority order, so that BIA and BAI are symmetric under relabelling. Theorem 1(a) compares policies for bids in $B_i=[0,\bar c_i]$.
• Profits and equilibria. Profits follow (5), with the expectation over $c_{-i}$ taken over the whole cost vector with coordinate $i$ overwritten. Equilibria require measurable strategies into $B_i=[0,\bar c_i]$. Ex ante profit is the expectation of the equilibrium profit, not the Myerson virtual-cost expression.

Several conventions are disclosed hypotheses or corrections. The goal uses $\le$ in place of the printed "higher". The equilibria in the goal are assumed symmetric, and the BAI one nondecreasing (Lemma 1's class). Strict monotonicity is not assumed, because with one supplier the equilibrium bid is the constant $\bar c_1$.

The goal is not trivialized. BAI awards on bids through $\lambda_i=b_i-r_i$ and BIA runs the index policy on bids and revealed reductions. Neither mechanism has "lowest cost wins" built in, which is milestone 6. Ex ante profit is defined from (5), so milestones 4–5 are not definitional. A sorry-free check exhibits a one-supplier instance that satisfies every hypothesis of the goal. In it both ex ante profits equal $1/2$.

Not formalized: Theorem 1(b)–(c), Lemma 1 (existence via Athey 2001), the closed form (4) of $W_i$, the asymmetric results (Propositions 2–4), the buyer-cost comparison (Theorem 3), the optimal mechanism (Theorem 4), and the extensions of §9. Contributions welcome: the envelope theorem for monotone-selection bidding games, measurability of the winning probabilities, and the index policy's optimality.

Selected references

• Q. Chen, D. R. Beil, I. Duenyas, Procurement mechanisms with post-auction pre-award cost-reduction investigations, Operations Research 70(6):3054–3075, 2022. https://doi.org/10.1287/opre.2022.2349 (accepted manuscript: LBS Research Online eprint 2544).
• S. Athey, Single crossing properties and the existence of pure strategy equilibria in games of incomplete information, Econometrica 69(4):861–889, 2001. https://doi.org/10.1111/1468-0262.00223
• R. B. Myerson, Optimal auction design, Mathematics of Operations Research 6(1):58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• P. Milgrom, I. Segal, Envelope theorems for arbitrary choice sets, Econometrica 70(2):583–601, 2002. https://doi.org/10.1111/1468-0262.00296
• M. L. Weitzman, Optimal search for the best alternative, Econometrica 47(3):641–654, 1979. https://doi.org/10.2307/1910412
• V. Krishna, Auction Theory, 2nd ed., Academic Press, 2009. https://doi.org/10.1016/C2009-0-22474-3

Motivation

We present a framework to treat quantum networks and all possible transformations thereof, including as special cases all possible manipulations of quantum states, measurements, and channels, such as, e.g., cloning, discrimination, estimation, and tomography. Our framework is based on the concepts of quantum comb-which describes all transformations achievable by a given quantum network-and link product-the operation of connecting two quantum networks. Quantum networks are treated both from a constructive point of view-based on connections of elementary circuits-and from an axiomatic one-based on a hierarchy of admissible quantum maps. In the axiomatic context a fundamental property is shown, which we call universality of quantum memory channels: any admissible transformation of quantum networks can be realized by a suitable sequence of memory channels. The open problem whether this property fails for some nonquantum theory, e.g., for no-signaling boxes, is posed.

This mission is the statement-level formalization of Theoretical framework for quantum networks (arXiv:0904.4483v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

30 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1: trace preservation (Lemma 1: trace preservation, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

15 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 8 (Universality of quantum memory channels); seed paper result: Causally prescribed higher-order admissible maps and their physical interconnection semantics (hard)
• §III C.3: memory and coherent-control upper bounds: Resource costs and rank-bounded implementations for all prefixes (hard)
• §III C.4: probabilistic network normalization: Branchwise composition of elementary instruments along a memory network (hard)
• Corollary 2: connection of networks: Lawful labelled partial network interconnection and merged signature (hard)
• Theorem 6 (Realization of admissible N-maps): Uniform physical interleaving of two memory realizations (hard)
• §IV B: order-preserving tensor products of combs: Order-preserving tooth merges with disjoint adjacent identifications (hard)
• Lemma 7: currying an (N,M)-map: Typed currying equivalence for arbitrary (N,M)-maps without a total product order (hard)
• Theorem 7: admissible (N,M)-maps are combs: Remote-compatible admissibility under a selected merged causal prescription (hard)
• §IV C remark: independent teeth exceed the comb hierarchy: Independent-teeth domains and quantification over all causal slot schedules (hard)
• Theorem 10 (Realization of N-instruments): Physical action of measured memory-network realizations on an arbitrary inner comb (hard)
• Lemma 8: testers as instruments: Canonical endpoint-padding transport between tester and instrument signatures (hard)
• Theorem 11 (Realization of testers): Tester endpoint padding with a k-dimensional final readout wire (hard)
• Theorem 12 (Realization scheme for testers): Sequential coherent implementation of the square-root tester map (hard)
• §V B: claimed formula for the span of deterministic combs: False printed nonrecursive characterization of the deterministic-comb span (source-ambiguity)
• §VI Eq.(95): displayed two-time Pauli measurement: Nonpositive P0 in the literal displayed Eq.(95) (source-ambiguity)

Selected references

• Theoretical framework for quantum networks, arXiv:0904.4483v2, https://arxiv.org/abs/0904.4483v2

Motivation

On-demand service platforms (ride-hailing, delivery, home services) do not employ their workers. They set a price for customers and a wage per unit of work, and independent agents decide how much time to make themselves available. A recurring policy question, raised by regulators and labor advocates alike, is whether platforms should be allowed to recruit labor pools of unlimited size: a larger pool is often argued to depress what each worker earns. Benjaafar, Ding, Kong and Taylor (SSRN 3103447; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2020.0964) study this question in a model where customers care about delay. Their central result, Theorem 2, is that the answer depends on delay sensitivity: in a standard market a larger pool lowers average labor welfare, but when customers are delay-sensitive, average labor welfare first rises and then falls in the pool size.

Setting

The model has two populations, both treated as continua.

Agents. A labor pool of mass $N>0$. An agent with opportunity-cost parameter $a$ who is available for time $x$ incurs cost $a x^2$; $a$ has distribution $F$ on $[\underline a,\bar a]$ with $0<\underline a$. Given the wage $w$, demand $D$ and labor supply $S$, work is shared in proportion to availability, so the agent's effective wage is $w_e=wD/S$ and his best response is $x^*(a)=wD/(2aS)$. Aggregation gives the labor supply equation

$$S=\sqrt{wDN\,E[1/a]/2}.$$

Customers. Needs arise at rate $\Lambda$ (the market size); a customer with valuation $v\sim\mathrm{Unif}[0,\bar v]$ seeks service if $v-p-hW\ge 0$, where $h\ge0$ is the delay sensitivity and

$$W=\frac{(D/S)^\beta}{S-D},\qquad \beta\ge1,$$

is the delay. Demand is $D=\Lambda[1-G(p+hW)]$ with $G$ the uniform cdf, and an equilibrium requires $D<S$. In the benchmark $h=0$ demand is $\Lambda[1-G(p)]$ and the capacity constraint is $D\le S$.

Platform. The platform chooses $p\ge0$, $w\ge0$ to maximize $(p-w)D$ subject to these equilibrium conditions; the optimum is $(p^*,w^*,D^*,S^*)$. The agent utilization is $\rho^*=D^*/S^*$, and average labor welfare is

$$\overline{LW}=\int\Big[\frac{w^*D^*}{S^*}x^*(a)-a\,x^*(a)^2\Big]dF(a).$$

The pool sizes for which a positive optimum exists are $N>\underline N$, with $\underline N=0$ for $\beta>1$ and $\underline N=8h/(\bar v^2E[1/a])$ for $\beta=1$.

Formalization targets

Goal: Theorem 2 (p. 11)

1. If $h=0$: $w^*$, $w^*_e$ and $\overline{LW}$ are strictly decreasing in $N$.
2. If $h>0$: $w^*$ is strictly decreasing in $N$ on $(\underline N,\infty)$, and for each $Q\in\{D^*/S^*,\ w^*_e,\ \overline{LW}\}$ there is $N_0>\max(0,\underline N)$ with

$$Q\ \text{strictly increasing on}\ (\underline N,N_0),\qquad Q\ \text{strictly decreasing on}\ (N_0,\infty).$$

The thresholds are not given in closed form; the goal asserts only their existence.

Milestones (in attack order)

• Lemma 11 (p. OA1): unique positive market equilibrium for each admissible $(p,w)$.
• (8)–(9) (p. OA1): price, wage and profit as functions of $(D,S)$; (10): $\overline{LW}=E[1/a]\,w_e^2/4$.
• Lemma 12 (p. OA2): the revenue-maximizing demand $\tilde D(S)$ increases in $S$ and $\Pi(\tilde D(S),S)$ is single-peaked at $S^*$.
• Lemma 1 (pp. 9–10): a unique optimum exists iff $\beta>1$ or $\beta=1$ and $N>8h/(\bar v^2E[1/a])$.
• (17)–(18) (p. OA7): first-order conditions at the optimum.
• Lemma 13 (p. OA4): $S^*$, $D^*$ increase in $N$; $S^*\to\infty$, $D^*\to\Lambda/2$; $S^*,D^*,\rho^*\to0$ as $N\downarrow\underline N$.
• Case $h=0$ of the proof (pp. OA4–OA5): $D^*=S^*=\bar v/(2(\bar v/\Lambda+2/(NE[1/a])))$, $w^*=\bar v\Lambda/(\bar vNE[1/a]+2\Lambda)$.
• Parts (i)–(iv) of the proof (pp. OA5–OA7): the threshold statements for $w^*_e$, $\rho^*$ and $\overline{LW}$, the identity $w^*=\tfrac12\bar v-\bar vD^*/\Lambda$, and the monotonicity of $w^*$.

Significance

The result. Theorem 2 separates two regimes. In a congestion regime (small pools, large delay cost $hW^*$) extra agents reduce delay, stimulate demand faster than supply grows, and raise utilization, the effective wage and average labor welfare: agents exert a positive externality on one another. In a cost regime (large pools) the demand effect is exhausted and extra agents only dilute work. The paper uses this to argue against blunt caps on platform labor pools and as the baseline for its analysis of nominal and effective wage floors (§5). Without delay sensitivity the classical conclusion, that a larger pool lowers welfare, is recovered exactly.

Formalizing it. The theorem is proved in the paper, with an online appendix of implicit-function and envelope arguments. None of it is formalized. This mission produces a machine-checked model of a platform with endogenous supply and congestion-dependent demand, the reduced $(D,S)$ problem, and the comparative statics in $N$. The paper's Lemma 11 needs a correction at $\beta=1$ (see below), which is the kind of gap a formal development exposes.

Difficulty

The optimum is defined implicitly by two nonlinear first-order conditions, and there is no closed form for $h>0$. The obvious route, differentiating $w^*_e=2S^*/(NE[1/a])$ in $N$, gives a quantity whose sign is the competition between the growth of $S^*$ and the factor $1/N$, and that sign changes with $N$. Monotonicity arguments of the usual kind (supermodularity in $(S,N)$, which does give that $S^*$ increases) say nothing about such ratios. The obstacle is single crossing of a quantity defined only implicitly through the optimum, not differentiability. The boundary behaviour at $N\downarrow\underline N$ and $N\to\infty$ (Lemma 13) is also needed and is itself nontrivial at $\beta=1$, where $\underline N>0$.

Formalization scope

Everything lives in the namespace LaborWelfare.PoolSize, with one definitions file Setting.

• Parameters. $\bar v>0$ (vbar), $\Lambda>0$ (Lam), $h\ge0$, real $\beta\ge1$ (beta), and $F$ a probability measure on $\mathbb R$ carried by $[\underline a,\bar a]$ with $0<\underline a\le\bar a$. The density of $F$ is not required: only $E[1/a]=\int a^{-1}dF$ enters any result. $(D/S)^\beta$ is a real power.
• $N$ is a real number; all results are about functions of $N$ on $(\underline N,\infty)$ (on $(0,\infty)$ for $h=0$, where $\underline N=0$).
• Equilibrium. $D>0$, $S>0$, (2), (3)–(4), and $D<S$ for $h>0$, $D\le S$ for $h=0$; the uniform cdf is clamped to $[0,1]$.
• The optimum is an outcome maximizing $(p-w)D$ over every price $p\ge0$ and wage $w\ge0$ subject to the market equilibrium. Statements quantify over a selection $N\mapsto$ optimal outcome, which Lemma 1 (and the $h=0$ milestone) show exists and is unique on the regime, so the monotonicity claims concern the platform's actual optimum and cannot be met by a degenerate outcome or a vacuous hypothesis.
• Labor welfare is the integral of the page, not its closed form; the closed form is milestone (10).
• Strictness. "Increasing" and "decreasing" are strict (StrictMonoOn, StrictAntiOn), as the paper fixes on p. 11; the thresholds are three separate numbers.
• Correction. For $w>0$ and $p<\bar v$, Lemma 11's positive equilibrium exists exactly when $\beta>1$ or $p+2h/(wNE[1/a])<\bar v$. At $\beta=1$, the delay stays bounded away from zero as utilization vanishes; the paper omits that condition.

A complete development needs real analysis on implicitly defined functions (implicit-function theorem in one variable, envelope arguments, monotone limits) and an argmax framework for the two-variable profit; these are reusable for other platform-pricing papers. Proofs of any milestone are welcome, as are alternative routes to the threshold statements.

Selected references

• S. Benjaafar, J.-Y. Ding, G. Kong, T. Taylor, Labor Welfare in On-Demand Service Platforms, Manufacturing & Service Operations Management, 2022 (online 2021). SSRN manuscript with online appendix: https://ssrn.com/abstract=3103447; https://doi.org/10.1287/msom.2020.0964
• J. Bai, K. C. So, C. S. Tang, X. Chen, H. Wang, Coordinating supply and demand on an on-demand service platform with impatient customers, Manufacturing & Service Operations Management 21(3), 2019. https://doi.org/10.1287/msom.2018.0707
• T. A. Taylor, On-demand service platforms, Manufacturing & Service Operations Management 20(4), 2018. https://doi.org/10.1287/msom.2017.0678