Operations Research

Motivation

Financial networks are webs of liabilities: firm $u$ owes firm $v$ an amount $c_{(u,v)}$, and every firm holds some external assets. When firms cannot pay in full, how much money actually moves through the network depends on how each firm splits its available funds among its creditors. The classical clearing model of Eisenberg and Noe (2001) fixes this split by a proportional rule. Flow allocation games, introduced by Bertschinger, Hoefer and Schmand (arXiv:1908.01714, Mathematics of Operations Research, 2025), make it strategic: every firm chooses how to allocate whatever it receives, and the resulting payments are the clearing state of the chosen strategies.

Because money that circulates comes back, the total amount of flow in such a network is driven by cycles, and cycles require several firms to cooperate. The natural solution concept is therefore the strong equilibrium, which is stable against joint deviations of coalitions. The paper shows that in unit-ranking games a strong equilibrium maximizing total flow always exists (Theorem 9, price of stability $1$). This mission concerns the other side: how much total flow can the worst strong equilibrium lose, and which structural parameter of the network controls the loss.

Setting

A flow allocation game $\Gamma=(G,(b_v)_{v\in V},(c_e)_{e\in E})$ consists of a finite directed graph $G=(V,E)$ (parallel edges allowed), a fixed supply $b_v\in\mathbb N_0$ at each node and a capacity $c_e\in\mathbb N_0$ on each edge. Every node is a player. $E^+(v)$ and $E^-(v)$ denote the outgoing and incoming edges of $v$, and $c_v^+=\sum_{e\in E^+(v)}c_e$.

In a unit-ranking game, player $v$ chooses for each edge $e\in E^+(v)$ a non-decreasing function $a_e:\mathbb N_0\to\mathbb N_0$ with $a_e(y)\le c_e$ and $\sum_{e\in E^+(v)}a_e(y)=\min\{c_v^+,y\}$: given a total supply $y$, it forwards all of it until its outgoing edges are full, one unit at a time according to a ranking of unit capacities. A flow $f$ is feasible for a profile $\mathbf a$ if $f_{(v,w)}=a_{(v,w)}(f_v)$ with $f_v=b_v+\sum_{e\in E^-(v)}f_e$. The clearing state $\hat f$ is the coordinatewise largest feasible flow; player $v$'s utility is $u_v(\mathbf a)=\sum_{e\in E^+(v)}\hat f_e$, and the total flow is

$$\mathrm{Flow}(\mathbf a)=\sum_{e\in E}\hat f_e .$$

A profile is a strong equilibrium if no non-empty coalition $C\subseteq V$ can jointly switch to other unit-ranking strategies so that every member of $C$ strictly gains.

The circulation network $G'$ adds an auxiliary node $s$ with edges $(v,s)$ of unbounded capacity and $(s,v)$ of capacity $b_v$ for every $v$. An optimal circulation $f^*$ of $G'$ maximizes $\sum_{e\in E'}f^*_e$. A decomposition $\mathcal C(f^*)=\{C_1,\dots,C_k\}$ of $f^*$ into cycles of unit flow is a list of simple directed cycles of $G'$ that uses each edge exactly as often as $f^*$ has units on it. The parameter of this mission is

$$d=\min_{f^*,\ \mathcal C(f^*)}\ \max_{C_i\in\mathcal C(f^*)}|C_i| ,$$

the smallest possible size of the longest cycle, over all decompositions of all optimal circulations; sizes count auxiliary edges.

Formalization targets

Goal: Theorem 16 (p. 30)

In unit-ranking games, the price of anarchy for strong equilibria in terms of Flow is at most $d$: for every strong equilibrium $\mathbf a$ and every unit-ranking profile $\mathbf a'$,

$$\mathrm{Flow}(\mathbf a')\le d\cdot\mathrm{Flow}(\mathbf a).$$

The statement fixes no constant beyond the structural parameter $d$ and holds for all capacities and supplies.

Milestones (proof of Theorem 16, p. 30)

1. An optimal circulation yields the optimal total flow, and

$$\mathrm{Flow}(\mathbf a^*)=\sum_{C_i\in\mathcal C(f^*)}|C_i|-2\sum_{v}b_v\le\sum_{C_i\in\mathcal C(f^*)}d .$$

2. In a strong equilibrium every simple cycle of $G$ contains an edge with $\hat f_e=c_e$.
3. $\mathrm{Flow}(\mathbf a)$ is at least the number of cycles of $\mathcal C(f^*)$ that avoid $s$.

Companions

• Theorem 16 for games without fixed supplies ($b\equiv0$), the setting of Propositions 15 and 17.
• Proposition 17 (p. 30). For every $d\ge2$ there is a unit-ranking game with parameter $d$ and a strong equilibrium $\mathbf a$ with $\mathrm{Flow}(\mathbf a)>0$ and $(d-1)\,\mathrm{Flow}(\mathbf a)\le\mathrm{Flow}(\mathbf a^*)$.

Significance

The bound identifies the length of the circulating cycles as the quantity that governs the efficiency of coalition-stable payment behaviour. In networks whose optimal circulation decomposes into short cycles, such as bilateral or triangular netting of liabilities, every strong equilibrium clears at least a $1/d$ fraction of the optimal total payments; Proposition 17 shows that long cycles genuinely cost efficiency, so the bound is tight up to one. For pure Nash equilibria no such bound exists (Proposition 15, the price of anarchy is unbounded), so the result separates coalitional from unilateral stability.

The results are proved on paper; none of them is machine-checked. A formalization adds a precise account of the model (clearing state as a supremum of feasible flows, unit-ranking strategies as functions on $\mathbb N_0$, cycle decompositions of the circulation network) and checks a proof whose last step, as printed, needs repair. The printed last display, $\mathrm{Flow}(\mathbf a)\ge\sum_{C_i\in\mathcal C(f^*)}1$, does not hold for cycles passing through the auxiliary node $s$: with a single node $v$, $b_v=1$ and no outgoing edges, $\mathcal C(f^*)=\{(s,v,s)\}$ but $\mathrm{Flow}(\mathbf a)=0$. The theorem itself is not contradicted by this example, and the printed argument is complete for games without fixed supplies. The cycles through the auxiliary node need a separate count, which is part of the work this mission asks for.

Difficulty

The upper bound compares an arbitrary strong equilibrium with an optimum that may look nothing like it. The obvious approach, counting the units of each optimal cycle that also carry equilibrium flow, fails: the clearing state is a fixed point of all strategies at once, so whether a unit reaches an edge depends on decisions all around the network, and the equilibrium may route its flow along entirely different cycles. A single player cannot complete a cycle on its own, which is why the Nash price of anarchy is unbounded; any argument has to use coalitional deviations, and a deviation changes the clearing state globally, so its effect on each member's utility must be controlled through the fixed point.

The second difficulty is the auxiliary node. A cycle of the optimal decomposition that passes through $s$ contains a node that is not a player, so no coalition of players can claim it, and the unit of flow it represents may sit on an auxiliary edge that $\mathrm{Flow}$ does not count. These cycles are exactly where the printed argument stops short.

Formalization scope

Supplies, capacities, strategies and flows are natural numbers, as the paper prescribes for unit-ranking games. The graph is a finite type of nodes $V$ and a finite type of edges $E$ with tail and head maps, so parallel edges and loops are allowed. The clearing state is the coordinatewise sSup of the feasible flows. Coalitions are non-empty, and deviations range over unit-ranking profiles. Optimal circulations are optimal among integral circulations. Cycles of $G'$ are lists of edges with pairwise distinct start nodes, and decompositions are lists of cycles counted with multiplicity. Nodes of $G'$ are Option V, with none the node $s$.

The price of anarchy is stated multiplicatively, $\mathrm{Flow}(\mathbf a')\le d\cdot\mathrm{Flow}(\mathbf a)$, with no division, so a zero-flow equilibrium cannot satisfy the goal vacuously through a junk quotient. The parameter $d$ enters as a hypothesis, "some decomposition of some optimal circulation has all cycles of size at most $d$", which is equivalent to the bound for the min-max $d$ and avoids an infimum that would be $0$ on an empty set. In Proposition 17 the strong equilibrium is required to have positive flow, since otherwise the lower bound would hold trivially.

Not formalized: the complexity results of the paper, the bounds for other quality measures (Proposition 18) and for Nash equilibria (Proposition 15). A complete development needs the integral version of the lattice theorem for feasible flows (Theorem 2), the existence of a Flow-optimal profile from the proof of Theorem 9, and integral cycle decomposition of circulations; the last two are reusable beyond this mission. Contributions are welcome on each milestone, on a separate count for cycles through $s$, and on the explicit construction of Proposition 17.

Selected references

• N. Bertschinger, M. Hoefer, D. Schmand, Flow Allocation Games, Mathematics of Operations Research, 2025; preprint arXiv:1908.01714v3, 2023. https://arxiv.org/abs/1908.01714
• L. Eisenberg, T. H. Noe, Systemic Risk in Financial Systems, Management Science 47(2), 236–249, 2001. https://doi.org/10.1287/mnsc.47.2.236.9835

Why measure sensitivity by optimal transport

Global sensitivity analysis asks how much the uncertainty in an output $Y$ of a model or a data set is explained by an input $X$. A large family of indices has the form "expected discrepancy between the marginal law of $Y$ and its conditional law given $X$": the variance-based index of Sobol' and Wagner, the $L^1$ density-based index, Kuiper and Cramér–von Mises indices. Borgonovo, Figalli, Plischke and Savaré (Management Science 2025, doi:10.1287/mnsc.2023.01796) take the discrepancy to be an optimal-transport cost. The resulting indices apply to multivariate outputs, need no density, and include as special cases the numerator of Wiesel's Wasserstein correlation coefficient (Wiesel 2022, arXiv:2207.14079).

A sensitivity index is meant to measure information: how much knowing $X$, or a coarsening of $X$, tells about $Y$. Two properties make this reading legitimate. Coarser information must never be worth more than finer information, and an index computed from increasingly fine observations of $X$ must approach the value for the limiting information. This mission formalizes both properties for the optimal-transport indices, Theorems 8 and 9 of the paper. Theorem 9 is also the last step of the paper's consistency proof for its partition estimator (Theorem 21).

Setting

Let $(\Omega,\mathcal B,\mathbb P)$ be a probability space, $\mathsf X$ and $\mathsf Y$ Polish spaces with Borel σ-algebras $\mathscr B(\mathsf X)$, $\mathscr B(\mathsf Y)$, and $X:\Omega\to\mathsf X$, $Y:\Omega\to\mathsf Y$ measurable maps. Write $\mu$ and $\nu$ for the laws of $X$ and $Y$.

A cost is a continuous function $\mathsf k:\mathsf Y\times\mathsf Y\to[0,+\infty]$ with $\mathsf k(y,y')=0$ exactly when $y=y'$. The optimal-transport cost between probability measures $\nu,\nu'$ on $\mathsf Y$ is

$$K(\nu,\nu')=\inf_{\pi\in\Pi(\nu,\nu')}\iint\mathsf k(y,y')\,d\pi(y,y'),$$

where $\Pi(\nu,\nu')$ is the set of probability measures on $\mathsf Y\times\mathsf Y$ with marginals $\nu$ and $\nu'$.

For a σ-algebra $\mathcal F\subseteq\mathscr B(\mathsf X)$, representing partial information on $X$, a version of the conditional distribution of $Y$ given $(X,\mathcal F)$ is a family $(\nu^{\mathcal F}_x)_{x\in\mathsf X}$ of probability measures on $\mathsf Y$ with $x\mapsto\nu^{\mathcal F}_x(B)$ $\mathcal F$-measurable and

$$\mathbb P(X\in A,\ Y\in B)=\int_A\nu^{\mathcal F}_x(B)\,d\mu(x)\qquad(A\in\mathcal F,\ B\in\mathscr B(\mathsf Y)).$$

The OT-based sensitivity measure (Definition 1) is

$$\xi^K(Y,X\mid\mathcal F)=\int_{\mathsf X}K(\nu,\nu^{\mathcal F}_x)\,d\mu(x)\in[0,+\infty],$$

written $\xi^K(Y,X)$ when $\mathcal F=\mathscr B(\mathsf X)$. For a Borel map $g:\mathsf X\to\mathsf U$ into a Polish space, $U=g\circ X$ is a new random variable and $\xi^K(Y,U)$ is defined in the same way on $\mathsf U$; $\sigma(g)$ is the σ-algebra generated by $g$.

Formalization targets

Goal: continuity along increasing σ-algebras (Theorem 9)

For an increasing sequence $\mathcal F^1\subseteq\mathcal F^2\subseteq\cdots$ of sub-σ-algebras of $\mathscr B(\mathsf X)$ with join $\mathcal F=\bigvee_n\mathcal F^n$,

$$\lim_{n\to\infty}\xi^K(Y,X\mid\mathcal F^n)=\xi^K(Y,X\mid\mathcal F)\quad\text{in }[0,+\infty].$$

Milestones

• (66) and (68): the conditional law given coarser information is a mixture of the conditional laws given $X$, against the disintegration of $\mu$.
• Jensen step: $K\big(\nu,\int\eta_x\,d\rho(x)\big)\le\int K(\nu,\eta_x)\,d\rho(x)$.
• Theorem 8: $\xi^K(Y,X)\ge\xi^K(Y,X\mid\mathcal F)$ (23); $\xi^K(Y,X)\ge\xi^K(Y,U)=\xi^K(Y,X\mid\sigma(g))$ (24); equality $\xi^K(Y,X)=\xi^K(Y,U)$ when $g$ is injective almost everywhere.
• Relative monotonicity: $\xi^K(Y,X\mid\mathcal G)\le\xi^K(Y,X\mid\mathcal F)$ for $\mathcal G\subseteq\mathcal F$.
• Almost-sure weak convergence of the conditional laws $\nu^n_x\to\nu^\infty_x$ for $\mu$-a.e. $x$.
• Lower semicontinuity of $K(\nu,\cdot)$ under weak convergence.

Significance

The results. Theorem 8 is the formal statement that the OT indices value information monotonically: a transformation $g(X)$ of an input, such as a discretization or an aggregation of features, can only lose explanatory power, and loses none when $g$ is injective. Theorem 9 makes the indices continuous in the information: refining a partition of the input space, as an estimator does when the sample grows, recovers the index of the limiting σ-algebra. The paper relies on Theorem 9 to prove that its given-data estimator is consistent, and on Theorem 8 to justify its interpretation of the indices as values of information.

The formalization. The proofs are on pp. 35–36 of the authors' manuscript. As far as we know, none of these statements has been machine-checked. Formalizing them requires conditional distributions relative to arbitrary sub-σ-algebras, the convexity of optimal-transport costs under mixtures, and their lower semicontinuity under weak convergence, which are general facts of optimal transport that the platform does not yet have.

Difficulty

The monotonicity in Theorem 8 is a Jensen inequality, but it is applied to a function of a measure, $K(\nu,\cdot)$, along a mixture indexed by a disintegration, so the step needs a measurable choice of near-optimal couplings. Without such a choice the averaged coupling is not defined.

For Theorem 9, the inequality $\limsup\le$ follows from monotonicity, and $\liminf\ge$ is the substance. The natural first idea, Lévy's upward theorem applied to $\mathbb E[\varphi(Y)\mid X,\mathcal F^n]$, gives convergence for one test function at a time and outside a null set that depends on $\varphi$. Weak convergence of the conditional laws for almost every $x$ is a statement about all test functions at once. Even with it, $K(\nu,\cdot)$ is only lower semicontinuous, not continuous, and the cost $\mathsf k$ may be unbounded and take the value $+\infty$. No integrability hypothesis is available: the theorem holds without assuming $\mathbb M^K[Y]<\infty$, including when the limit is $+\infty$.

Formalization scope

• $\mathsf X$, $\mathsf Y$, $\mathsf U$ are Polish spaces with Borel σ-algebras; the paper's supports in $\mathbb R^{n_X}$, $\mathbb R^{n_Y}$ are such spaces.
• $X$, $Y$, $g$ are measurable, and $\mathbb P$ is a probability measure.
• Costs, $K$, $\mathbb M^K$ and $\xi^K$ take values in $[0,+\infty]$ (ℝ≥0∞); integrals are lower Lebesgue integrals.
• $K$ is the published platform definition RWPI.SqrtLasso.transportCost. Its first argument is the marginal $\nu$ and its second the conditional law.
• Conditional distributions are characterized by the defining property above (IsCondDistrib), never constructed. Every statement holds for every version, and versions for different $n$ need not be compatible.
• The join $\bigvee_n\mathcal F^n$ is the supremum of σ-algebras (⨆ n, Fs n), and the sequence is indexed from $0$.
• Weak convergence is tested against all bounded continuous real functions.
• "Injective almost everywhere" means injective on a measurable set of full $\mu$-measure.

The goal is a Tendsto in $[0,+\infty]$, not a one-sided bound. In particular, a proof of only $\limsup\le$ (monotonicity) or of the statement under a finiteness hypothesis on $\mathbb M^K[Y]$ does not close it. $\xi^K(Y,U)$ uses the conditional distribution of $Y$ given the random variable $U$ on $\mathsf U$, not that given $(X,\sigma(g))$; their equality is part of (24).

Two readings are disclosed corrections. Theorem 9's "sub-σ-algebras in $\mathcal F$" is read as sub-σ-algebras of $\mathscr B(\mathsf X)$. The comparison of two sub-σ-algebras $\mathcal G\subseteq\mathcal F$, used in the proof of Theorem 9 but stated in Theorem 8 only for $\mathcal F=\mathscr B(\mathsf X)$, is posed as its own milestone.

Reusable infrastructure includes the following, and contributions of any of them are welcome:

• existence and uniqueness of conditional distributions given a sub-σ-algebra;
• mixture convexity and lower semicontinuity of optimal-transport costs;
• almost-sure weak convergence of conditional laws along a filtration.

Selected references

• E. Borgonovo, A. Figalli, E. Plischke, G. Savaré, Global Sensitivity Analysis via Optimal Transport, Management Science, 2025 (authors' manuscript of 7 March 2024). https://doi.org/10.1287/mnsc.2023.01796
• J. Wiesel, Measuring association with Wasserstein distances, arXiv preprint, 2022. https://arxiv.org/abs/2207.14079
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
• L. Schwartz, Radon Measures on Arbitrary Topological Spaces and Cylindrical Measures, Oxford University Press, 1973.
• I. M. Sobol', Sensitivity estimates for nonlinear mathematical models, Mathematical Modeling and Computational Experiment, 1993.

Motivation

Music streaming platforms collect a subscription fee from each user and pass a large share of the revenue to the artists. How that money is divided has become a policy question. Most platforms use the pro-rata rule: all fees are pooled and each artist is paid in proportion to their share of all streams. The main alternative is the user-centric rule: each user's fee is divided only among the artists that user played, in proportion to that user's own streams. The choice decides whether a heavy listener's tastes count for more than a light listener's, and it has been debated by platforms, rights holders and regulators.

G. Bergantiños and J. D. Moreno-Ternero, Revenue Sharing at Music Streaming Platforms (arXiv:2310.11861, Management Science, 2025), study the question axiomatically and through cooperative game theory. This mission formalizes their Theorem 3: once one asks that no group of artists can be paid less than the money of the users who only listened to that group, the user-centric rule is the only homogeneous and additive option. Two sibling missions treat Theorem 1 (axiomatic characterizations of pro-rata and user-centric) and Theorem 2 (the core of the streaming game).

Setting

There are $n$ artists $N$. A streaming problem $(N, M, t)$ consists of a finite set $M$ of users and the numbers $t_{ij} \in \mathbb N$ of times user $j$ played artist $i$; every user has played at least one artist. For a user $j$ let

$$T^j = \sum_{i\in N} t_{ij}, \qquad L^j = \{i \in N : t_{ij} > 0\},$$

the user's total streams and the list of artists the user played. Each user pays $1$, so the amount to be shared is $m = |M|$.

A popularity index $I$ assigns to each problem a nonnegative vector $I(N,M,t) \in \mathbb R^N$ with positive total. Artist $i$ is then paid

$$R^I_i(N,M,t) = \frac{I_i(N,M,t)}{\sum_{i'\in N} I_{i'}(N,M,t)}\, m .$$

Indices that are positive multiples of each other pay the same, and are identified. The user-centric index is $U_i(N,M,t) = \sum_{j\in M} t_{ij}/T^j$.

The streaming game of a problem is the cooperative game on the artists with worth $v(S) = |\{j \in M : L^j \subseteq S\}|$, the money of the users who only played artists in $S$. Its core is

$$C(N,v) = \Big\{x \in \mathbb R^N : \sum_{i\in N} x_i = v(N),\ \sum_{i\in S} x_i \ge v(S) \text{ for all } S \subseteq N\Big\}.$$

The axioms are:

• homogeneity: if $\lambda \ge 0$ and $t_{ij} = \lambda t_{i'j}$ for every user $j$, then $I_i = \lambda I_{i'}$;
• additivity: the index of the union of two problems with disjoint sets of users is the sum of their indices;
• core selection: $R^I(N,M,t) \in C(N,v)$.

The domain $\mathcal P^*$ consists of the problems in which no user has played every artist, $L^j \neq N$ for all $j\in M$.

Formalization targets

Goal: Theorem 3 (p. 14)

On $\mathcal P^*$, an index satisfies homogeneity, additivity and core selection if and only if there is $c > 0$ with

$$I_i(N,M,t) = c\, U_i(N,M,t) \qquad \text{for every } (N,M,t) \in \mathcal P^*,\ i \in N.$$

Milestones

1. The user-centric rewards belong to $A(N,M,t)$, the vectors $\sum_{j\in M} x^j$ with each $x^j$ a probability vector on $L^j$; and they belong to the core $C(N,v)$, on every problem (p. 14).
2. The user-centric index satisfies homogeneity, additivity and core selection on $\mathcal P^*$ (p. 23).
3. Display (1): under core selection, the index of a one-user problem vanishes outside the user's list (pp. 23–24).
4. On a one-user problem, $I_i = \big[\sum_{i'} I_{i'}\big] U_i$ (p. 24).
5. The Claim: two distinct users with disjoint lists have one-user problems with equal index totals (p. 24).
6. The same equality for any two distinct users (p. 25).

Significance

The theorem singles out the user-centric rule by a stability property rather than by a fairness postulate about users. Core selection says that no coalition of artists receives less than the payments of the users who listen exclusively to that coalition; the pro-rata rule violates it already in a two-user example (p. 14). Together with Theorem 1 of the same paper, it gives two independent routes to the user-centric rule, which is the form in which the result enters the policy discussion.

The paper proves the theorem in its appendix (pp. 23–25). Nothing about streaming problems, popularity indices or this characterization has been formalized before; the mission produces a machine-checked version of the model, of the user-centric index's membership in the core, and of the characterization. The model layer (problems as finitely supported stream tables, rewards, the streaming game) is shared in shape with the two sibling missions.

Difficulty

Each axiom is easy to verify for the user-centric index; the content is the converse. Homogeneity and additivity alone allow every weighted index, where each user's streams are weighted by an arbitrary positive function of the user and the profile, and pro-rata is one of them. The difficulty is to extract from core selection, which only constrains ratios of index values through the reward normalization, that every user carries exactly the same total weight. Core selection on a single user only fixes the shape of the index on that user's list; comparing two users requires problems with several users, and the comparison of two users whose lists overlap cannot be made directly.

Formalization scope

Artists are Fin n (0-based). Users are natural numbers, and a problem is a finitely supported map t : ℕ →₀ (Fin n → ℕ) whose support is the user set $M$. This builds in three standing assumptions of the paper: every user of a problem has played some artist ($L^j \neq \emptyset$), streams are natural numbers, and an index can depend only on the columns of the users of the problem. The core is the published Supermodularity.Cooperative.Core on Finset.univ. Rewards use $m = |M|$; at the empty problem the reward vector is $0$ and the core of the zero game is $\{0\}$.

Two readings are committed to and disclosed:

• Additivity is for disjoint user groups. The page's "$M = M^1 \cup M^2$" without disjointness would force $I = 2I$ and no index would satisfy it; every proof in the paper splits users disjointly.
• The domain $\mathcal P^*$. The page defines $\mathcal P^*$ as the problems with at least three users in which no user played every artist. The proof applies core selection and additivity to one- and two-user problems "in $\mathcal P^*$" and draws a third user from outside the problem. The formalization follows the proof: $\mathcal P^*$ is every problem in which no user played every artist, the axioms and the conclusion are quantified over it, and "at least three users" is a property of the user population $\mathbb N$, which is infinite. A version restricting the axioms to problems with at least three users is a different statement not covered by the paper's proof.

The index requirements (nonnegativity, positive total) are imposed on nonempty problems of $\mathcal P^*$ only; demanding a positive total at the empty problem would make every index impossible and the theorem vacuous. "Is the user-centric index" is one global $c > 0$, not a constant depending on the problem: a problem-dependent constant would turn the conclusion into a much weaker statement. With one artist $\mathcal P^*$ holds only the empty problem and the theorem is vacuous, as on the page; no hypothesis on $n$ is added. The milestones on one-user problems are stated for arbitrary nonzero profiles of a user, which is the same as the page's columns of a problem in $\mathcal P^*$.

A complete development needs finite-sum manipulation over Finsupp supports and the decomposition of a problem into its one-user problems. Proofs of any milestone are welcome, as are proofs of Theorem 2's inclusion $A \subseteq C$, which milestone 1 needs.

Selected references

• G. Bergantiños, J. D. Moreno-Ternero, Revenue Sharing at Music Streaming Platforms, arXiv:2310.11861v1, 2023; Management Science, 2025. https://arxiv.org/abs/2310.11861
• V. A. Vasil'ev, On a class of imputations in cooperative games, Soviet Mathematics Doklady 23, 53–57, 1981 (used by the paper's Theorem 2, from which milestone 1 is drawn).
• J. C. Harsanyi, A bargaining model for cooperative n-person games, in A. W. Tucker, R. D. Luce (eds.), Contributions to the Theory of Games IV, Princeton University Press, 1959, pp. 325–355 (dividends, used by Theorem 2).

Motivation

Remote driving, or tele-driving, separates the driver from the vehicle: a human sitting in a control centre drives a car over a network link and can switch to another car as soon as a trip ends. Commercial pilots of this model exist for car delivery and ride-hailing, and it gives a platform a new design choice. A conventional ride-hailing fleet has one driver per car. A tele-driven fleet can run more cars than drivers.

Benjaafar, Wang and Yang model this choice as a queueing system and ask how the service level depends on the number of drivers when the number of vehicles is fixed (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687). Idle vehicles still matter even when nobody is driving them: they are spread over the service region, so the car nearest a new request is closer, and trips (pick-up plus ride) finish faster. A driver count below the vehicle count therefore trades fewer servers for shorter service times. This mission formalizes the paper's first main result, Theorem 1.A, which says when that trade can strictly improve service. The mission follows the 2023 SSRN working paper (version of 1 June 2023) and its numbering.

Setting

A platform has $m$ vehicles and $n \le m$ remote drivers. Trip requests arrive as a Poisson process of rate $\lambda > 0$. A request that finds all $n$ drivers busy is lost. While $q$ customers are in service, each trip ends at the exponential rate $\mu(m, q)$, a function of a real $q \in [1, m]$. The paper's standing assumptions on this rate are:

• Assumption 1: $\mu(m,q)$ is strictly increasing in $m$ and decreasing in $q$, strictly concave in $q$, tends to $1/s$ as $m \to \infty$ (where $s > 0$ is the expected trip time between two uniform locations), and $\mu(m,m)$ does not depend on $m$;
• Assumption 2: there is $\bar m > 0$ such that for $m \ge \bar m$ the trip-completion rate $q\mu(m,q)$ first increases and then decreases in $q$.

The number of customers in service is a birth–death chain with birth rate $\lambda$ and death rate $q\mu(m,q)$, truncated at $n$. With

$$\rho(q) = \frac{\lambda}{q\,\mu(m,q)},$$

its stationary law is $\pi_{m,n}(q) = \prod_{k=1}^{q}\rho(k) \big/ \big[1 + \sum_{i=1}^{n}\prod_{k=1}^{i}\rho(k)\big]$ for $0 \le q \le n$. The service level, the long-run fraction of requests served, is

$$SL(m,n) = 1 - \pi_{m,n}(n).$$

The paper restricts throughout to $m \ge \bar m$ and $\lambda > \max\{1/s, \max_{q \le \bar m} q\mu(\bar m, q)\}$. It splits fleet sizes into three regimes by thresholds $\gamma_1(\lambda) < \gamma_2(\lambda)$. In the supply-limited regime $m < \gamma_1(\lambda)$, demand exceeds the trip-completion rate in every state: $\rho(q) > 1$ for all $q \in [1, m]$.

Formalization targets

Goal: Theorem 1.A

For $m < \gamma_1(\lambda)$, if

$$\lambda\, SL(m,m) > m\,\mu(m,m), \qquad (5)$$

then there is a threshold $1 \le \tilde n_1 \le m - 1$ such that $SL(m,n)$ is strictly increasing in $n$ for $n \le \tilde n_1$ and strictly decreasing for $n > \tilde n_1$, with $SL(m,\tilde n_1) \ge SL(m,\tilde n_1 + 1)$. If (5) fails, $SL(m,n)$ is non-decreasing in $n$ on $\{1,\dots,m\}$.

Milestones

1. Lemma 3 (first sentence): $\rho$ is strictly convex and $1/\rho$ strictly concave on $[1,m]$.
2. Lemma 4: for $1 \le n \le m$, $\pi_{m,n-1}(n-1) > \pi_{m,n}(n)$ holds if and only if $\pi_{m,n-1}(n-1) > \frac{\rho(n)-1}{\rho(n)}$, if and only if $\pi_{m,n}(n) > \frac{\rho(n)-1}{\rho(n)}$.
3. App. C.1, dichotomy: the blocking probability $\pi_{m,n}(n)$ is strictly decreasing on $\{1,\dots,m\}$, or strictly decreasing up to some $\tilde n_1$ and strictly increasing from $\tilde n_1 + 1$.
4. App. C.1, Condition (5): $\pi_{m,m}(m) > \pi_{m,m-1}(m-1)$ if and only if (5) holds.

Significance

Theorem 1.A says that removing drivers from a fleet can strictly raise the fraction of demand served, and Condition (5) says exactly when. The condition compares the average trip-completion rate $\lambda SL(m,m)$ with the completion rate $m\mu(m,m)$ when every vehicle is occupied. In a standard multi-server loss system, where $q\mu(m,q) = q\mu$, the condition never holds and more servers always help. The result makes the optimal driver count a well-posed line search over a unimodal function, and the companion Theorems 1.B and 1.C of the paper (intermediate and supply-rich regimes) rest on the same recursion.

The paper's proofs are short but leave gaps a formal proof must close. To our knowledge no part of the paper has been machine-checked. The mission produces a complete formal statement of the model and of the theorem, under the paper's own assumptions, together with the lemmas the published argument passes through. Milestones 2–4 hold in every regime, so they also serve the proof of Theorem 1.B.

Difficulty

Two steps resist the obvious argument. First, the blocking probability $\pi_{m,n}(n)$ is not a monotone function of anything simple: each driver count truncates the birth–death chain at a different state, so the comparison between $n-1$ and $n$ drivers is a comparison of two different stationary laws. Second, the published argument for the first step of the dichotomy appeals to "$\rho(1) > \rho(2)$ by Assumption 2", which Assumption 2 does not imply. A correct proof must handle the case where the blocking probability increases already from one driver to two. Strict convexity of $\rho$ must also be proved without derivatives, because the formal rate $\mu$ is only assumed concave, not differentiable.

Formalization scope

All objects live in the namespace TeleDriving.ScarceFleet. The rate is a function mu : ℕ → ℝ → ℝ, meaningful for real $q \in [1, m]$. $\rho$, the products $\prod_{k\le i}\rho(k)$, $\pi_{m,n}(q)$ and $SL(m,n)$ are explicit definitions following (1)–(3). The committed conventions are:

• Positivity of $\mu$ on $[1,m]$ and $s > 0$, implicit on the page, are part of Assumption 1.
• "Decreasing in $q$" is non-strict.
• "First increases then decreases" means a turning point $\hat q \in (1, m)$, with strict increase on $[1,\hat q]$ and strict decrease on $[\hat q, m]$.
• Assumptions 1–2 and the size restriction of p. 13 are hypotheses of every theorem.
• The regime $m < \gamma_1(\lambda)$ is encoded by its characterization in Lemma 3(i), $\rho(q) > 1$ on $[1, m]$, because $\gamma_1(\lambda)$ is a real root in $m$ that an integer fleet size almost never equals.
• Driver counts range over $\{1,\dots,m\}$; monotonicity is stated on that set.
• The junction $SL(m,\tilde n_1) \ge SL(m,\tilde n_1+1)$ is non-strict, as the proof gives it.

The threshold is bounded, $1 \le \tilde n_1 \le m - 1$, and no hypothesis on the shape of $\pi$ or $SL$ is assumed. A threshold $\tilde n_1 = m$ or an assumed monotonicity would make the theorem trivial. The dichotomy milestone carries no regime hypothesis, because the argument of App. C.1 does not use one.

Useful infrastructure, reusable beyond this mission, includes: mediant inequalities for $\frac{a+c}{b+d}$ with $b, d > 0$; the fact that the product of a positive linear function and a positive, antitone, strictly concave function is strictly concave; and the induction pattern that turns a one-step recursion test into global unimodality. Proofs of any milestone, alternative arguments, and proofs that dispense with the regime hypothesis are all welcome.

Selected references

• S. Benjaafar, Z. Wang, X. Yang, Human in the Loop Automation: Ride-Hailing with Remote (Tele-)Drivers, SSRN working paper 4130757, version of 1 June 2023. https://ssrn.com/abstract=4130757
• S. Benjaafar, Z. Wang, X. Yang, Human in the Loop Automation: Ride-Hailing with Remote (Tele-)Drivers, Management Science, 2024. https://doi.org/10.1287/mnsc.2022.01687
• O. Besbes, F. Castro, I. Lobel, Spatial Capacity Planning, Operations Research 70(2), 2022. https://doi.org/10.1287/opre.2021.2112
• J. Cheah, J. M. Smith, Generalized M/G/C/C state dependent queueing models and pedestrian traffic flows, Queueing Systems 15, 1994. https://doi.org/10.1007/BF01189240

Motivation

Decision theory under uncertainty distinguishes risk, where probabilities are known, from ambiguity, where they are not. Ellsberg's (1961) urn experiments showed that people's choices between bets on the same kind of event depend on where the uncertainty comes from: a bet on a known urn is preferred to the matching bet on an unknown urn. Tversky and Fox (1995) found that basketball fans prefer bets on basketball games to bets with matched objective chances. Models of ambiguity therefore have to let attitudes depend on the source of uncertainty.

Baillon, Bleichrodt, Li and Wakker (Source Theory: A Tractable and Positive Ambiguity Theory, Management Science 71(10), 2025) take sources to be algebras of events and propose source theory: within each source the agent behaves as if events carry probabilities, transformed by a source-dependent weighting function, while different sources may be weighted differently. The behavior within one source is probabilistic sophistication in the sense of Machina and Schmeidler (1992), restricted to that source. This mission formalizes the paper's first main result, Theorem 1: a characterization of when a single source admits such a probability, entirely in terms of two ambiguity attitudes that are measured in experiments.

Setting

A state space $S$ carries an algebra $\mathcal E$ of events, and $\Gamma$ is a set of outcomes. An act is a finite-valued map $x : S \to \Gamma$ whose level sets are events; it is from an algebra $\mathcal A$ if its level sets lie in $\mathcal A$. The binary act $\gamma E \beta$ pays $\gamma$ on $E$ and $\beta$ on $E^c$. The agent has a preference $\succcurlyeq$ on acts.

Structural Assumption 1 (p. 8771) requires that $\succcurlyeq$ is a weak order represented on binary acts by biseparable utility: there are a utility $U : \Gamma \to \mathbb R$ and a weighting function $W$ on events ($W(\emptyset)=0$, $W(S)=1$, monotone) such that for $\gamma \succcurlyeq \beta$ the act $\gamma E\beta$ is valued $W(E)U(\gamma)+(1-W(E))U(\beta)$. It further requires three nonindifferent outcomes, convex rangedness of $W$ (between two nested events every intermediate weight is attained by a nested event), strong monotonicity, cumulative dominance and the Archimedean axiom. Events are ranked by $W$: $A \succcurlyeq B$ means $W(A) \ge W(B)$.

A source $\mathcal S$ is a subalgebra of $\mathcal E$ on which $W$ is convex ranged. It is uniform (source theory holds for it, Definition 1) if there is a finitely additive probability measure $P$ on $\mathcal S$ such that for all acts $x, y$ from $\mathcal S$

$$\bigl[\forall \alpha\in\Gamma:\ P(x\succcurlyeq\alpha)\ge P(y\succcurlyeq\alpha)\bigr]\ \Longrightarrow\ x\succcurlyeq y. \tag{2}$$

Two attitudes compare sources $\mathcal A$ and $\mathcal C$. $\mathcal C$ is preferred to $\mathcal A$ (Definition 2) if for all $A_1\in\mathcal A$, $C_1\in\mathcal C$,

$$W(A_1)=W(C_1)\ \Longrightarrow\ W(A_1^c)\le W(C_1^c). \tag{6}$$

$\mathcal A$ is more insensitive than $\mathcal C$ with insensitivity region $[B,D]$ (Definition 4) if for all ordered threefold partitions $(C_1,C_2,C_3)$ of $S$ from $\mathcal C$ and $(A_1,A_2,A_3)$ from $\mathcal A$,

$$W(A_1)=W(C_1)\ \&\ W(A_3^c)=W(C_3^c)\le W(D)\ \Rightarrow\ W(A_2)\ge W(C_2), \tag{8}$$ $$W(B)\le W(A_1)=W(C_1)\ \&\ W(A_3^c)=W(C_3^c)\ \Rightarrow\ W(A_2^c)\le W(C_2^c). \tag{9}$$

The region is regular for $\mathcal S$ if every fourfold partition $(E_1,\dots,E_4)$ of $S$ from $\mathcal S$ has a cell with $E_j \succcurlyeq B$ and $E_j^c \preccurlyeq D$.

Formalization targets

Goal: Theorem 1 (p. 8774)

For a source $\mathcal S$ under Assumption 1,

$$\mathcal S \text{ is uniform}\iff \mathcal S \text{ is preferred to itself, and } \exists\, B,D\in\mathcal E:\ [B,D] \text{ regular for } \mathcal S,\ \mathcal S \text{ more insensitive than itself w.r.t. } [B,D].$$

Milestones (in proof order)

1. Necessity (App. B, p. 8779): a uniform source is preferred to itself and more insensitive than itself with the maximal region $[\emptyset, S]$.
2. Lemma A.1 (p. 8779): (6) is equivalent to its weak-premise form (7), $W(A_1)\ge W(C_1)\Rightarrow W(A_1^c)\le W(C_1^c)$.
3. Lemma A.2 (p. 8779): (8) and (9) are equivalent to their weak-premise forms (A.1) and (A.2).
4. (B.1) (p. 8780): in a source preferred to itself, $A\succcurlyeq C \iff A^c\preccurlyeq C^c$.
5. Lemma B.1 (p. 8780): under statement (ii), for $E\cap H=F\cap H=\emptyset$ in $\mathcal S$, $E\succcurlyeq F\iff E\cup H\succcurlyeq F\cup H$.
6. The representing probability (p. 8780): under statement (ii), a unique probability measure on $\mathcal S$ represents event preference on $\mathcal S$.
7. The aside (p. 8780): a representing probability $P$ gives $W = w\circ P$ on $\mathcal S$ for a continuous, strictly increasing $w$ with $w(0)=0$, $w(1)=1$.
8. Uniqueness (p. 8774): the probability measure of a uniform source is uniquely determined.

Significance

Theorem 1 gives source theory a behavioral foundation: whether a source admits an a-neutral probability measure can be read off from comparisons of bets on its own events, without assuming expected utility for risk. Uniformity is what makes the paper's quantitative tools available. Once a source is uniform, its weighting function factors as $W = w_{\mathcal S}\circ P_{\mathcal S}$, and Theorems 2–4 of the paper compare sources through the pmatcher between their source functions; Theorem 4 uses Theorem 1 as a step. The uniqueness of $P_{\mathcal S}$ (milestone 8) is what makes the source function well defined.

The result is proved in the paper; nothing in it is formalized anywhere to our knowledge. The proof relies on a classical representation theorem for qualitative probability (Krantz, Luce, Suppes and Tversky, 1971, Theorem 5.2.2), which is not in Mathlib either. A complete development would give Lean a first framework of Savage-style acts, biseparable utility and comparative probability, which other decision-theory missions could reuse.

Difficulty

The necessity half rests on the probability $P$ of a uniform source representing event preference strictly, which needs strong monotonicity and the range of $P$ on a convex-ranged source. The sufficiency half is the hard one. From the two attitude conditions alone one has to derive de Finetti's additivity (Lemma B.1). Its proof is a case analysis that uses regularity of the region to guarantee that one of the cells is a genuine middle event. One then needs a representation theorem for qualitative probabilities on an algebra, with uniqueness, in the finitely additive setting. Dropping regularity is not an option: without it the region $B=S$, $D=\emptyset$ makes insensitivity nearly empty, and source preference alone does not imply uniformity (the paper's Example 1). The obvious route through countably additive measure theory is not available either, because the probabilities are only finitely additive.

Formalization scope

All statements share one module, SourceTheory.Uniform.Model. It holds acts (IsActFrom), binary acts (bet), null events, convex rangedness, Assumption1 (a structure with one field per clause of Assumption 1), sources (IsSource), finitely additive probabilities (IsProbOn), uniformity (IsUniformWith, IsUniform), IsPreferredTo (Definition 2), IsMoreInsensitive (Definition 4) and IsRegularRegion. Its text is shared verbatim by the four missions on this paper. The conventions are:

• Events are the members of an algebra $\mathcal E$ (endnote 1 licenses any algebra; the power set is a special case). Every quantified event lies in $\mathcal E$ or in the source, so the values of $W$ off $\mathcal E$ never matter.
• Event preference is $W$-order, as Assumption 1 prescribes. The preference forms (15)–(17), (A.3)–(A.5) therefore coincide with the $W$-forms.
• Assumption 1's "W is convex ranged for every source" is split. Convex rangedness on all events is part of Assumption1, and each source carries its own via IsSource. Reading it over every subalgebra would make Assumption 1 unsatisfiable, because $\{\emptyset,S\}$ has no event of weight $1/2$.
• Twofold partitions are $(A_1,A_1^c)$. Threefold and fourfold partitions are ordered and may have empty cells.
• Probability measures on a source are finitely additive, real valued and nonnegative, with total mass 1.
• In the goal, the boundary events $B, D$ are arbitrary events, and "equally preferred/insensitive to itself" is one copy of each condition: for $\mathcal A=\mathcal C=\mathcal S$ both directions coincide.

Statement (ii) carries an existential region, and it must be regular. A version without regularity, or with uniformity replaced by "$W=w\circ P$ for some $P$", would be a different and weaker theorem.

Needed infrastructure: comparative-probability representation (Krantz et al. 1971, Theorem 5.2.2, or a direct construction via convex rangedness), finitely additive measures on set algebras, and the range of a finitely additive probability that represents a convex-ranged weighting. Proofs of the milestones, of the representation theorem as a reusable lemma, and sanity models of Assumption 1 (for instance an expected-utility agent on $[0,1)$ with Lebesgue measure) are all welcome.

Selected references

• A. Baillon, H. Bleichrodt, C. Li, P. P. Wakker, Source Theory: A Tractable and Positive Ambiguity Theory, Management Science 71(10):8767–8782, 2025. https://doi.org/10.1287/mnsc.2023.03307
• D. Ellsberg, Risk, Ambiguity, and the Savage Axioms, Quarterly Journal of Economics 75(4):643–669, 1961. https://doi.org/10.2307/1884324
• I. Gilboa, Expected Utility with Purely Subjective Non-Additive Probabilities, Journal of Mathematical Economics 16(1):65–88, 1987. https://doi.org/10.1016/0304-4068(87)90022-X
• D. H. Krantz, R. D. Luce, P. Suppes, A. Tversky, Foundations of Measurement, Vol. I, Academic Press, New York, 1971 (cited in the paper for Theorem 5.2.2).
• M. J. Machina, D. Schmeidler, A More Robust Definition of Subjective Probability, Econometrica 60(4):745–780, 1992. https://doi.org/10.2307/2951565
• A. Tversky, C. R. Fox, Weighing Risk and Uncertainty, Psychological Review 102(2):269–283, 1995. https://doi.org/10.1037/0033-295X.102.2.269

Motivation

Optimal auction theory in the tradition of Myerson (1981) assumes that the seller knows the distribution of the buyers' valuations. In practice that distribution is estimated, misspecified, or simply unknown. Prior-independent mechanism design asks for a mechanism that performs well across a whole class of distributions, without being tuned to any one of them. A natural yardstick is regret: the gap between the revenue the seller would extract if she knew the valuations, namely the highest valuation, and the revenue her mechanism actually collects. The seller chooses a mechanism to minimize the worst case of this gap over all distributions Nature may pick.

For a single buyer, Bergemann and Schlag (2008) showed that the minimax regret over valuations supported on $[0,1]$ is $1/e$, attained by a posted price drawn at random with CDF $\log v + 1$ on $[1/e, 1]$. Whether a comparably explicit answer exists for $n$ buyers, and whether the familiar second-price auction remains optimal among all dominant-strategy mechanisms, was open. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478v5, Operations Research 2025) answer both questions for i.i.d. valuations. This mission formalizes that answer: their Theorem 1.

Setting

A seller has one indivisible item and $n \ge 1$ buyers with valuations $v = (v_1, \dots, v_n) \in [0,1]^n$. A mechanism $m = (x, p)$ assigns to every valuation profile allocation probabilities $x_i(v) \in [0,1]$ and expected payments $p_i(v)$. It is dominant-strategy incentive compatible (DSIC), written $m \in \mathcal M$, if for all $i$, all $v$ and every misreport $\hat v_i$:

$$v_i x_i(v) - p_i(v) \ge 0 \;\;\text{(IR)}, \qquad v_i x_i(v) - p_i(v) \ge v_i x_i(\hat v_i, v_{-i}) - p_i(\hat v_i, v_{-i}) \;\;\text{(IC)}, \qquad \textstyle\sum_i x_i(v) \le 1 \;\;\text{(AC)}.$$

For a joint distribution $F$ of $v$, the regret is

$$\mathrm{Regret}(m, F) = \mathbb E_{v \sim F}\Big[\max(v) - \sum_{i=1}^n p_i(v)\Big],$$

and the minimax regret over a class $\mathcal F$ of distributions is $\mathcal R^*_n(\mathcal F) = \inf_{m \in \mathcal M} \sup_{F \in \mathcal F} \mathrm{Regret}(m, F)$. Here $\mathcal F_{\mathrm{iid}}$ is the class of product laws $G^{\otimes n}$ whose marginal $G$ is supported on $[0,1]$.

A second-price auction with random reserve $\mathrm{SPA}(\Phi)$ draws a reserve price $q$ from a distribution $\Phi$. The highest bidder wins if her bid is at least $q$ and pays $\max(v^{(2)}, q)$, where $v^{(1)} \ge v^{(2)}$ are the two highest valuations. Otherwise nothing is sold.

Two explicit functions enter the answer. For $r \in (0,1)$, let

$$\mathrm{rEq}_n(r) = (1-r)^{n-1} + \log r + \sum_{k=1}^{n-1} \frac{(1-r)^k}{k},$$

and, for $r < v \le 1$,

$$\Phi^*_n(v) = \Big(\frac{v}{v-r}\Big)^{n-1}\log\Big(\frac vr\Big) - \sum_{k=1}^{n-1} \frac1k \Big(\frac{v}{v-r}\Big)^{n-1-k},$$

with $\Phi^*_n = 0$ below $r$ and $1$ above $1$. The isorevenue marginal $F^*_n(v) = 1 - r/v$ on $[r, 1)$, $F^*_n(1) = 1$, is the law under which every posted price in $[r,1]$ earns the same revenue $r$.

Formalization targets

Goal: Theorem 1

Let $r^*_n$ be the root of $\mathrm{rEq}_n$ in $(0, 1/n)$; it is the only root in $(0,1)$. A reserve distribution on $[r^*_n, 1]$ with CDF $\Phi^*_n$ exists. The auction $\mathrm{SPA}(\Phi^*_n)$ is DSIC and minimax-regret optimal, and

$$\mathcal R^*_n(\mathcal F_{\mathrm{iid}}) = (1-r^*_n)^{n-1} - \int_{r^*_n}^1 \Big(1 - \frac{r^*_n}{v}\Big)^{n-1} dv.$$

The Lean goal states the location and uniqueness of the root, the existence of the reserve law, the DSIC property, the upper bound for $\mathrm{SPA}(\Phi^*_n)$ against every i.i.d. law, the matching lower bound for every DSIC mechanism, and the literal identity for $\mathcal R^*_n(\mathcal F_{\mathrm{iid}})$.

Milestones

1. Lemma B-1 (p. App-4): an integration-by-parts identity for $\int h\,dG$, split at $r^*$.
2. Proposition 1 (p. 16): the regret of $\mathrm{SPA}(\Phi)$, for $\Phi$ with a density on $[r^*, 1]$, in terms of the order-statistic CDFs; joint and i.i.d. forms.
3. Proposition A-3 (p. App-2): the root $r^*_n$; $\Phi^*_n$ equals a power series, solves the ODE $(\Phi^*)' + \frac{(n-1)r^*_n}{v(v-r^*_n)}\Phi^* = \frac1v$, and satisfies $\Phi^*_n(r^*_n) = 0$ and $\Phi^*_n(1) = 1$; the regret at the candidate saddle point equals the value.
4. Step 1 of the proof of Theorem 1 (p. 17): against $\mathrm{SPA}(\Phi^*_n)$, the i.i.d. isorevenue law is a worst case.
5. Step 2 (p. 17): against the i.i.d. isorevenue law, $\mathrm{SPA}(\Phi^*_n)$ has the least regret among all DSIC mechanisms.

A companion item states Corollary 1 (p. 14): for $n = 1$, $r^*_1 = 1/e$, $\Phi^*_1(v) = \log v + 1$ on $[1/e, 1]$, and the minimax regret is $1/e$.

Significance

The theorem gives, for every number of buyers, a closed-form description of the minimax-regret optimal mechanism among all DSIC mechanisms, together with its value. The optimum is a familiar format, a second-price auction, but its reserve price must be randomized. The same saddle point is the starting point for the paper's results on affiliated and arbitrary joint valuations, which are separate missions of this series.

The result is proved on paper. To our knowledge none of it has been formalized. A complete development would supply machine-checked versions of several tools that recur in robust mechanism design: DSIC mechanisms with randomized allocations, the regret functional, order-statistic CDFs of product measures, Myerson-type revenue characterizations under distributions with atoms, and saddle-point arguments for inf–sup problems over mechanisms and distributions.

Difficulty

The upper bound (Step 1) is a pointwise optimization once the regret of $\mathrm{SPA}(\Phi)$ is written through the CDFs of the order statistics. Writing it that way already requires integration by parts against arbitrary distributions on $[0,1]$, which may have atoms.

The lower bound (Step 2) is the hard direction. One must show that no DSIC mechanism beats $\mathrm{SPA}(\Phi^*_n)$ against the isorevenue law. The standard route through Myerson's virtual values does not apply directly: the isorevenue law is a mixture of a density and a point mass at $1$, so the revenue of a general DSIC mechanism has to be characterized from first principles. That characterization starts from the payment identity for dominant-strategy mechanisms. The closed forms also involve a transcendental root $r^*_n$ and a logarithmic ODE solution, so the monotonicity and boundary facts about $\Phi^*_n$ (it is a CDF, $\Phi^*_n(1) = 1$) need real analysis rather than numerics.

Formalization scope

Buyers are indexed by Fin n, valuations are functions Fin n → ℝ, and distributions are measures on that space. (IR), (IC) and (AC) are imposed for valuations in $[0,1]^n$, which is all the seller considers. Two conditions are added to DSIC so that the expectation in the regret is meaningful: the allocation and payment rules are measurable, and payments are bounded on the cube. The second-price auction breaks ties in favour of the lowest index; the revenue does not depend on the rule. A reserve law or an isorevenue law is described by a hypothesis on its CDF. $\Phi^*_n$ is defined piecewise, so its closed form is never evaluated at the singular point $v = r^*_n$, and "$\Phi^*_n(r^*_n) = 0$" is stated as a one-sided limit. The minimax regret is a real infimum over the nonempty class of DSIC mechanisms of real suprema of bounded families. Uniqueness of $r^*_n$ is stated on $(0,1)$, which is what the paper's proof establishes.

Trivializing formalizations are ruled out explicitly. The regret is not a Bochner integral of a possibly non-integrable payment, which Lean would set to $0$. The mechanism class is not restricted to second-price auctions. The value is the explicit integral, not a sSup. The root's location in $(0, 1/n)$ is part of the claim.

Contributions are welcome at every level. These include the DSIC property of $\mathrm{SPA}(\Phi)$, order-statistic CDFs of product measures, Lemma B-1 and Proposition 1, the analytic facts about $\mathrm{rEq}_n$ and $\Phi^*_n$, the payment identity for DSIC mechanisms with randomized allocations, and the revenue bound of Step 2. The analytic and mechanism-design infrastructure is reusable beyond this paper.

Selected references

• J. Anunrojwong, S. R. Balseiro, O. Besbes, On the Robustness of Second-Price Auctions in Prior-Independent Mechanism Design, arXiv:2204.10478v5, 2024; Operations Research, 2025. https://arxiv.org/abs/2204.10478
• D. Bergemann, K. Schlag, Pricing without Priors, Journal of the European Economic Association 6(2–3), 2008. https://doi.org/10.1162/JEEA.2008.6.2-3.560
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58

Motivation

Appointment systems, airport runways, outpatient clinics and container terminals do not receive customers at random: each customer is scheduled at a fixed slot and arrives near it, early or late by a random amount. Queues fed by such scheduled traffic have been studied since Winsten (1959) and Mercer (1960). Kingman (1962) showed that, below critical load and for perturbations that are positive with finite mean, the heavy-traffic limit of the equilibrium waiting time of an S/G/1 queue ("S" for scheduled) is the same as for the D/G/1 queue with perfectly punctual arrivals. Araman and Glynn (2012) proved a functional central limit theorem for scheduled traffic when the perturbations have infinite mean, where fractional Brownian motion appears, and Araman, Chen, Glynn and Xia (2022) established properties of scheduled traffic, among them the decomposition and exponential moments used below, and showed that with Pareto-like perturbations the critically loaded S/D/1 workload grows without bound.

Araman and Glynn (arXiv:2212.04164, published as a technical note in Operations Research, 2025) settle the critically loaded case. This mission formalizes their diffusion limit (Corollary 1): when the mean service time equals the slot length, the workload grows like $\sqrt t$ with an explicit reflected-Brownian limit, exactly as if arrivals were punctual. A companion mission formalizes their Theorem 1, the stability criterion for deterministic service times.

Setting

Fix $h>0$. Customer $j\in\mathbb Z$ is scheduled at time $jh$ and arrives at

$$A_j = jh + hU + \xi_j ,$$

where the perturbations $\xi_j$ are i.i.d. real random variables with $\mathbb E|\xi_0|<\infty$, and the uniform shift $U$ is uniform on $[0,1]$ and independent of $\xi=(\xi_j)_{j\in\mathbb Z}$; the shift makes the arrival point process time-stationary. The counting function is $N(t)=\#\{j: A_j\in(0,t]\}$ for $t\ge0$, so $N(0)=0$.

Customers arriving after time $0$ are numbered $1,2,\dots$ in order of arrival and bring service times $V_1,V_2,\dots$, i.i.d., with $\operatorname{Var}V_1<\infty$, independent of $(U,\xi)$. A single server works at unit rate and is empty at time $0$, so the workload is

$$W(t)=\sup_{0\le s\le t}\Big(\sum_{i=N(s)+1}^{N(t)}V_i-(t-s)\Big).$$

The queue is critically loaded when $\mathbb EV_1=h$. The proof works with the counts of early and late customers, $\mathcal E(t)=\#\{i: ih+Uh>t,\ ih+Uh+\xi_i\le t\}$ and $\mathcal L(t)=\#\{i: ih+Uh<t,\ ih+Uh+\xi_i\ge t\}$. Finally, reflected Brownian motion with mean $0$, unit volatility and $X(0)=0$ is $X(t)=B(t)-\inf_{0\le u\le t}B(u)$ for a standard Brownian motion $B$.

Formalization targets

Goal: Corollary 1

If $\mathbb E|\xi_0|<\infty$, $\operatorname{Var}V_1<\infty$ and $h=\mathbb EV_1$, then

$$t^{-1/2}\,W(t)\;\Rightarrow\;\sigma X(1)\qquad(t\to\infty),\qquad \sigma^2=\frac{\operatorname{Var}V_1}{h}.$$

The case $\operatorname{Var}V_1=0$ is included; the limit is then $0$.

Intermediate targets (milestones)

1. Exponential moments $\mathbb E e^{\theta\mathcal E(0)}\le\exp\big((e^\theta-1)(\mathbb E\xi_0^-/h+1)\big)$ and $\mathbb E e^{\theta\mathcal L(0)}\le\exp\big((e^\theta-1)(\mathbb E\xi_0^+/h+1)\big)$ for $\theta>0$ (pp. 3–4).
2. Stationarity of $\mathcal E$ and $\mathcal L$ (p. 3); the decomposition $N(t)=\#\{ih+Uh\in(0,t]\}+(\mathcal E(t)-\mathcal L(t))-(\mathcal E(0)-\mathcal L(0))$ (p. 4); identically distributed slot increments of $N$ with all exponential moments (p. 4).
3. The maximal bounds $\frac1{\log n}\max_k\mathcal E(kh)$, $\frac1{\log n}\max_k\mathcal L(kh)$, $\frac1{\log n}\max_k(N((k+1)h)-N(kh))\to0$ in probability (p. 4).
4. Proposition 1 (p. 3): $\dfrac{1}{\log n}\max_{0\le s\le1}|hN(ns)-ns|\Rightarrow0$.
5. The reversed-time representation $W(t)\overset{D}{=}\max_{0\le s\le t}\big(\sum_{i=1}^{\hat N(s)}V_i-s\big)$, with $\hat N$ the count of the time-reversed input (p. 4, implicit in the proof).
6. $N(ts)/t\to s/h$ almost surely (p. 5); the $o_p(1)$ reduction to $t^{-1/2}\max_{0\le s\le1}\sum_{i=1}^{N(st)}(V_i-h)$ (p. 5); and its limit $\sigma X(1)$ (p. 5).

Significance

The result. At critical loading a queue fed by a renewal process with non-degenerate interarrival or service times is null-recurrent at best, and its workload grows like $\sqrt t$. Corollary 1 shows that scheduled traffic behaves the same way as soon as service times vary, however heavy the (finite-mean) tail of the perturbations: the arrival process contributes nothing on the diffusion scale, and the limit $\sigma X(1)$ depends only on $\operatorname{Var}V_1$ and $h$. In particular, $W(t)\Rightarrow\infty$ whenever $\operatorname{Var}V_1>0$, which is why the paper's stability question (Theorem 1, the companion mission) is posed for deterministic service. Proposition 1, that scheduled traffic deviates from its fluid path by only $o(\log n)$ over $[0,n]$, is of independent use for any functional of scheduled arrivals.

Formalizing it. The result is proved on paper in a short note that cites two ingredients (the decomposition of $N$ and the exponential moments of $N(h)$) from Araman et al. (2022) and leaves the time reversal implicit. A formalization makes those steps explicit and checks the constant: the proof's final display prints $\frac{\sigma}{\sqrt h}X(1)$, which matches (1.1) only when its $\sigma^2$ is $\operatorname{Var}V_1$. No part of the argument has been machine-checked so far.

Difficulty

The arrival-process part (Proposition 1) is elementary in each step but long: independent-indicator moment generating functions, stationarity of a perturbed lattice under shifts, and a union bound over $n$ slots. The obstacle is the last step. The obvious route, "apply Donsker's theorem", does not apply directly: the random walk $\sum_{i\le m}(V_i-h)$ is evaluated at the random times $N(st)$, which are not independent stopping times of the walk but come from an independent process, and the target is the law of a Brownian maximum, identified with $X(1)$ through Lévy's reflection identity. Mathlib has the central limit theorem and Brownian motion but no invariance principle and no reflection principle. A second trap is the time reversal: the proof's starting expression uses the counting function of the reversed process (perturbations $-\xi_j$), and replacing it by the forward count gives a statement that is false in law for asymmetric perturbations.

Formalization scope

Lean conventions: the perturbations are a sequence ξ : ℤ → Ω → ℝ; the standing assumptions are bundled in ScheduledInput (measurable, iIndepFun, identically distributed, Integrable (ξ 0), U with the uniform law on $[0,1]$, U independent of the whole sequence) and ServiceInput (i.i.d. V : ℕ → Ω → ℝ, MemLp (V 1) 2, V independent of the pair (U, ξ); V 0 is unused). $N(t)$ is an ncard in ℕ; $\mathcal E$, $\mathcal L$ and slot increments are encard in ℕ∞, and every statement that converts them to numbers carries an almost-sure finiteness conjunct. Suprema are real suprema over $[0,t]$ or $[0,1]$. Convergence in distribution is TendstoInDistribution (which includes almost-everywhere measurability), convergence in probability is TendstoInMeasure. The Brownian motion is Mathlib's IsBrownianReal, indexed by ℝ≥0, on an arbitrary probability space, and $X(1)$ is B 1 − ⨅ u ∈ [0,1], B u. $\sigma=\sqrt{\operatorname{Var}V_1/h}$ is written out.

Corrections to the printed text, each recorded in the item notes: the workload index range is $N(s)+1,\dots,N(t)$ (the page's $N(s),\dots,N(t)$ gives $W(0)\ne0$); $N$ counts arrivals in $(0,t]$ instead of the page's non-additive closed intervals; the constant is $\sqrt{\operatorname{Var}V_1/h}$ for the proof's "$\sigma/\sqrt h$"; the counting function in the reversed representation is that of the reversed input; "as $n\to\infty$" on p. 5 means $t\to\infty$; and the misprinted intermediate lines of the bound on $\mathbb Ee^{\theta\mathcal E(0)}$ are not used.

Trivializing formalizations are ruled out as follows: counts that are infinite on a set of positive probability cannot make a bound easier, since finiteness is asserted; the limit is a probability law on $\mathbb R$, not on an extended line; the limit is reflected Brownian motion at time $1$, not a substituted half-normal formula; and $\operatorname{Var}V_1=0$ is not excluded.

Needed infrastructure: a Donsker-type invariance principle (or at least the convergence of the maximum of a random walk, which is an open platform goal of its own), a random time-change lemma, Lévy's identity $\sup_{u\le1}B(u)\overset{D}{=}B(1)-\inf_{u\le1}B(u)$, and stationarity of perturbed lattices. These are reusable well beyond this paper. Contributions to any milestone, or to these supporting results, are welcome.

Selected references

• V. F. Araman and P. W. Glynn, Stability of a Queue Fed by Scheduled Traffic at Critical Loading, arXiv:2212.04164v1, 2022; Operations Research (technical note), 2025. https://arxiv.org/abs/2212.04164
• V. F. Araman and P. W. Glynn, Fractional Brownian motion with H < 1/2 as a limit of scheduled traffic, Journal of Applied Probability 49(3), 1169–1188, 2012.
• V. F. Araman, H. Chen, P. W. Glynn and L. Xia, On a single server queue fed by scheduled traffic with Pareto perturbations, Queueing Systems 100, 61–91, 2022 (cited in the paper as Araman et al. (2022) for Proposition 2 and the exponential moments of $N(h)$).
• J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society B 24(2), 383–392, 1962. http://www.jstor.org/stable/2984229
• R. M. Loynes, The stability of a queue with non-independent inter-arrival and service times, Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 497–520, 1962. https://doi.org/10.1017/S0305004100036781