All missions

Motivation

Many allocation problems hand out indivisible goods without money: course seats, shifts, donated food, inherited items. An integral allocation of such goods can rarely be envy-free. With one good and two agents, someone always envies. The standard remedies are of two kinds. Randomization restores fairness in expectation: the probabilistic serial rule of Bogomolnaia and Moulin (J. Econ. Theory 2001) yields a fractional allocation that is envy-free and can be implemented as a lottery over integral allocations. Approximation restores fairness after the draw: envy-freeness up to one good (EF1), introduced by Lipton, Markakis, Mossel and Saberi (EC 2004) and named by Budish (J. Political Economy 2011), asks only that any envy disappear once a single good is removed from the envied bundle.

The two remedies pull apart. Giving all goods to one agent chosen uniformly at random is envy-free ex-ante, but after the draw one agent holds everything. Round-robin picking with a uniformly random order is EF1 after every draw, and proportional but not envy-free in expectation (Proposition 2 and Example 1 of the paper). Freeman, Shah and Vaish (arXiv:2005.14122, 2020; with Aziz, Operations Research 2024) ask whether one lottery can be fair in both senses at once. They show that it can, and that the answer depends on how the lottery is built, not only on which fractional allocation it implements.

Setting

There is a finite set $N$ of $n \ge 1$ agents and a finite set $M$ of $m$ goods. Agent $i$ has an additive valuation with values $v_{i,g} \ge 0$. A fractional allocation is a matrix $X$ with $X_{i,g} \in [0,1]$ the share of good $g$ given to agent $i$, and $v_i(X_i) = \sum_g X_{i,g} v_{i,g}$. An integral allocation gives each agent a bundle $A_i \subseteq M$, with bundles pairwise disjoint, and $v_i(A_i) = \sum_{g \in A_i} v_{i,g}$. A randomized allocation is a finite lottery $\{(p^k, A^k)\}_k$ over integral allocations. It implements the fractional allocation $\sum_k p^k A^k$.

$X$ is envy-free (EF) if $v_i(X_i) \ge v_i(X_h)$ for all $i, h$. An integral allocation $A$ is EF1 if for all $i, h$ with $A_h \neq \emptyset$ some $j \in A_h$ satisfies $v_i(A_i) \ge v_i(A_h \setminus \{j\})$. A lottery is ex-ante EF if the allocation it implements is EF. It is ex-post EF1 if every allocation it draws is EF1.

The eating protocol $\mathrm{Eating}(M', 1)$ runs for one unit of time on the goods $M'$, each of mass one. At every moment each agent eats her favorite good among those not yet fully consumed, at rate one. Recursive Probabilistic Serial (Algorithm 1) proceeds in $\lceil m/n \rceil$ stages, starting from $M^1 = M$. Stage $t$ computes $X^t = \mathrm{Eating}(M^t, 1)$ and decomposes it as $X^t = \sum_k w^{t,k} A^{t,k}$ by the generalized Birkhoff–von Neumann theorem, Theorem 1 of the paper. It then draws $B^t = A^{t,k}$ with probability $w^{t,k}$ and continues on $M^{t+1} = M^t \setminus \bigcup_i B^t_i$. The final bundles are $B_i = \bigcup_t B^t_i$.

Formalization targets

Goal: Theorem 2 (p. 11)

For every instance, every way of breaking ties between equally valued goods, and every decomposition rule satisfying the conclusions of Theorem 1,

$$\text{the lottery of Algorithm 1 is ex-ante envy-free and ex-post EF1.}$$

Milestones

1. Theorem 1 (p. 9). A matrix with entries in $[0,1]$ and row and column sums at most $1$ is a convex combination of $0/1$ allocations. Each of their row and column sums is the floor or the ceiling of the corresponding sum of $X$.
2. One eating stage (§3.1, p. 9). $\mathrm{Eating}(M', 1)$ satisfies the hypotheses of Theorem 1 and is supported on $M'$. If $|M'| \ge n$, every agent eats a total mass of exactly one.
3. One item per stage (§3.1, p. 9). Every allocation of the decomposition uses only goods of $M'$. If $|M'| \ge n$, it gives each agent exactly one good.
4. Each eating stage is envy-free (proof of Theorem 2, p. 11).
5. Lemma 1 (p. 11). In iteration $t < \lceil m/n \rceil$, each agent weakly prefers the good she receives to every good still unallocated.
6. Lemma 2 (p. 11). Every allocation returned by Algorithm 1 is EF1.
7. Algorithm 1 returns a randomized allocation (§3.1, p. 9).
8. The expectation recursion (proof of Theorem 2, p. 11; Algorithm 3, p. 33). The implemented allocation is the first eating stage plus the weighted sum of the allocations implemented on the remaining goods.

Significance

Theorem 2 shows that ex-ante envy-freeness and ex-post EF1 are compatible for additive goods. Algorithm 1 is a constructive witness. The paper builds on this in two directions. A polynomial-time variant (§3.2) computes such a lottery. An impossibility result (Theorem 3) shows that adding ex-post fractional Pareto optimality is too much. The paper also extends the approach to bads and mixed manna (§7), where the natural extension guarantees only ex-post EF2.

The result is proved on paper. No formalization of probabilistic serial, the eating protocol, EF1 of randomized allocations or the rectangular Birkhoff–von Neumann theorem with floor and ceiling bounds is known to us in any proof assistant. Mathlib has the square doubly stochastic case (doublyStochastic_eq_convexHull_permMatrix), and Prove2Me has it as FamousTheorems.birkhoff_von_neumann. This mission asks for a machine-checked proof of Theorem 2 about an explicit definition of the eating protocol and of Algorithm 1.

Difficulty

The proof is short on paper but hides two pieces of continuous-time bookkeeping. First, the eating protocol is a process in time. The stage statements need a description of it in which "agent $i$ ate a positive share of $g$ while $g^*$ was still available" can be stated and checked. Second, the ex-ante argument conditions on the history of earlier draws. Because the decomposition may have exponentially many branches, it has to be turned into an induction over the recursive lottery. The obvious shortcut, proving the result for "the" BvN decomposition of each stage, fails because the decomposition is not unique and the theorem must hold for all of them. Weight-zero terms of a decomposition can violate Lemma 1. They are never drawn, but any argument over the whole support must exclude them explicitly.

Formalization scope

Agents and goods are finite types with decidable equality. The good set $M$ is the whole type of goods, and $n \ge 1$ is [Nonempty N]. Values are real and non-negative. All quantities are in $\mathbb R$, and $\lceil m/n \rceil$ is Nat.ceil of a real quotient. Integral allocations are bundle maps N → Finset G, and lotteries are finite lists of (probability, allocation) pairs.

The eating protocol is a definition computed event by event. Between events every agent eats a fixed good chosen by a choice rule. The next event comes when the time budget ends or a good being eaten is exhausted. The minimum runs only over goods actually being eaten, so no division by zero occurs. $|M| + 1$ events suffice, and later iterations change nothing. Algorithm 1 is a definition: a recursion over stages producing a lottery over stage histories.

The only free parameters of the goal are the tie-breaking rule, constrained to choose a most valuable available good, and the decomposition rule, constrained to satisfy Theorem 1's conclusions. The eating outcome, the lottery and its support are computed by the definitions, never assumed. A statement taking $X^t$ or the lottery as free variables with envy-freeness as a hypothesis would trivialize the goal and is not this mission.

Conventions that differ from the page:

• Ex-post EF1 is over allocations drawn with positive probability.
• The without-loss-of-generality assumption that every good is valued positively by some agent is omitted. The proof does not use it, so the goal is stronger.
• Theorem 1 is stated as existence, without its running-time clause.
• Algorithm 1's printed line 2 initializes $M^0$, while the loop reads $M^1$. Its line 8 is a union over all stages inside the loop. Both are read as the intended algorithm, consistent with Algorithm 3 and with the proof of Theorem 2.
• Histories are indexed from $0$.

Not included are Proposition 1, the §3.2 polynomial-time variant, the SD-EF remark after Theorem 2, and §§4–7 (Theorem 3, the group-fairness results, the MNW characterization, bads). A proof of Theorem 1 in this rectangular form, with the floor and ceiling bounds, would be reusable well beyond this mission, for example in other fair-division and assignment results. So would a clean theory of the eating protocol. Contributions to either are welcome.

Selected references

• R. Freeman, N. Shah, R. Vaish, Best of Both Worlds: Ex-Ante and Ex-Post Fairness in Resource Allocation, arXiv:2005.14122v1, 2020. https://arxiv.org/abs/2005.14122 (journal version with H. Aziz, Operations Research, 2024).
• A. Bogomolnaia, H. Moulin, A New Solution to the Random Assignment Problem, Journal of Economic Theory 100(2), 2001. https://doi.org/10.1006/jeth.2000.2710
• R. J. Lipton, E. Markakis, E. Mossel, A. Saberi, On Approximately Fair Allocations of Indivisible Goods, ACM EC 2004. https://doi.org/10.1145/988772.988792
• E. Budish, The Combinatorial Assignment Problem: Approximate Competitive Equilibrium from Equal Incomes, Journal of Political Economy 119(6), 2011. https://doi.org/10.1086/664613
• E. Budish, Y.-K. Che, F. Kojima, P. Milgrom, Designing Random Allocation Mechanisms: Theory and Applications, American Economic Review 103(2), 2013. https://doi.org/10.1257/aer.103.2.585

Motivation

A one-warehouse, multi-retailer (OWMR) distribution system is the basic model of a supply chain in which a central warehouse buys from an outside supplier and ships to several retail locations. When every shipment carries a fixed cost and a positive lead time, the optimal policy of the stochastic system is unknown, and the classical approach is to search over a structured class of policies and bound its cost. Exact evaluation of even a simple policy is hard, because the warehouse can run out of stock and then the retailers' replenishments interact.

Zhu, Chen, Hu and Yang (SSRN 2921743; Operations Research, 2021, doi:10.1287/opre.2021.2101) study modified echelon $(r,Q)$ policies for continuous-review OWMR systems with Poisson demand. Their central tool is an explicit upper bound on the long-run average cost of any such policy, written as the retailers' single-stage $(r,Q)$ costs, a warehouse term that depends on the retailer policies, and a fixed-cost allowance. Their heuristic policy, its worst-case performance guarantee and its asymptotic optimality (Theorems 2–4 of the paper) are all built on this bound. The single-stage cost functions follow Zheng (1992) and the echelon cost accounting follows Chen and Zheng (1994).

Setting

There are $N\ge1$ retailers, indexed $i=1,\dots,N$, and one warehouse, indexed $0$. Retailer $i$ faces Poisson demand of rate $\lambda_i>0$, independent across retailers, so the warehouse sees Poisson demand of rate $\lambda_0=\sum_i\lambda_i$. Installation $i$ has a constant lead time $L_i>0$, a fixed cost $K_i>0$ per shipment, and an echelon holding cost rate $h_i>0$; unmet retailer demand is backlogged at rate $p_i>0$. Write $\bar K=\max_iK_i$.

A modified echelon $(r,Q)$ policy has reorder levels $r_i$ and order quantities $Q_i>0$ for every installation. When the echelon inventory position $IP_i$ of installation $i$ is at or below $r_i$ and the upstream installation has stock on hand, a shipment raises $IP_i$ as close as possible to $r_i+Q_i$.

With $D_i\sim\mathrm{Poisson}(\lambda_iL_i)$ the lead-time demand of retailer $i$, the single-stage holding-and-backlog rate and the single-stage $(r,Q)$ cost are

$$G_i(y)=\mathbb E\big[h_i(y-D_i)^++(h_0+p_i)(y-D_i)^-\big],\qquad C_i(r_i,Q_i)=\frac{\lambda_iK_i+\int_{r_i}^{r_i+Q_i}G_i(y)\,dy}{Q_i}.$$

With $G_i(w_i)=\sup_{r_i<z\le r_i+Q_i}G_i(z)$, $M_j=\max\{G_j(w_j),C_j(r_j,Q_j)\}$ and $S_i=\sum_{j\ne i}(r_j+Q_j)$, the envelope of Lemma 3 at warehouse echelon level $x$ is

$$\bar\Gamma_i(x)=\sum_{j\ne i}M_j+\begin{cases}M_i & x-S_i>r_i,\\ \max\{G_i(x-S_i),M_i\} & \text{otherwise},\end{cases}\qquad \bar\Gamma(x)=\max_i\bar\Gamma_i(x).$$

With $D_0\sim\mathrm{Poisson}(\lambda_0L_0)$, set $\hat G=\bar\Gamma-\sum_iC_i$, $\Lambda_0(y)=\mathbb E[h_0(y-D_0)+\hat G(y-D_0)]$ and

$$\hat C_0(r_0,Q_0)=\frac1{Q_0}\Big[\lambda_0K_0+\int_{r_0}^{r_0+Q_0}\Lambda_0(y)\,dy\Big].$$

The long-run average system cost is (1) of the paper,

$$C(r,Q)=\frac1{Q_0}\Big[\lambda_0K_0+\int_{r_0}^{r_0+Q_0}\mathbb E\big[h_0(y-D_0)+\Omega(y)\big]\,dy\Big],$$

where $\Omega(y)$ is the expected cost rate of all retailers when the warehouse inventory position is $y$.

Formalization targets

Goal: Theorem 1 (p. 13)

$$C(r,Q)\le C^U(r,Q)\equiv\sum_{i=1}^NC_i(r_i,Q_i)+\hat C_0(r_0,Q_0)+\frac{\lambda_0\bar K}{Q_0}.$$

It is stated for every policy, with no assumption on the parameters beyond $Q_i,Q_0>0$.

Milestones

1. App. A (3): the per-retailer bound: the charge of retailer $i$ is at most the own-retailer term of $\bar\Gamma_i(x)$.
2. Lemma 3: the total retailer charge at a feasible state is at most $\bar\Gamma(x)$.
3. App. A (8): $\hat\Gamma(x)\le\bar\Gamma(x)=\hat G(x)+\sum_iC_i$.
4. App. A (9): $\Gamma_0(y)\le\Lambda_0(y)+\sum_iC_i$.
5. App. A (10): $\frac1{Q_0}[\lambda_0K_0+\int_{r_0}^{r_0+Q_0}\Gamma_0]\le\hat C_0(r_0,Q_0)+\sum_iC_i$.

Significance

The bound replaces the cost of an $(N+1)$-installation stochastic system, which has no closed form, by computable retailer costs and a warehouse term. This is what makes the paper's heuristic policy computable and what its performance guarantees compare against: each retailer uses its single-stage optimal $(r_i^*,Q_i^*)$, and the warehouse minimizes the remaining term. Bounds of this decomposition type are a standard device in multi-echelon inventory theory, and Lemma 3's envelope, which charges each retailer at the lowest inventory position the others can leave it, is the step specific to the distribution setting.

The result is proved in the paper's online appendix. It has not been formalized. A formal development adds to the platform a single-stage $(r,Q)$ cost with Poisson lead-time demand, the echelon envelope of Lemma 3 for general $N$, and an explicit OWMR cost decomposition, all of which are reusable by later work on distribution systems, including the paper's own performance bounds.

Difficulty

The core is Lemma 3 for general $N$. Bounding each retailer separately by its worst case $\max\{G_i(w_i),C_i\}$ fails, because a retailer below its reorder level can have a much larger cost rate $G_i(IP_i)$; the bound must use that the inventory positions are coupled through the warehouse echelon level. The printed proof is an induction on $N$ whose step needs convexity of a sum in which one term is only bounded by a convex function, so the order of bounding and convexity arguments matters. Convexity and continuity of $G_i$ (a Poisson mixture of piecewise-linear functions) must be established, and every expectation against the Poisson law needs an integrability argument, since the integrands grow linearly.

Formalization scope

All declarations live in the namespace DistribRQ.UpperBound. Retailers are indexed by Fin N with [NeZero N]; the warehouse data $L_0,K_0,h_0,r_0,Q_0$ are separate. The primitives are bundled in Primitives N (all rates and costs positive) and the policy in Policy N (real $r_i,r_0$; $Q_i,Q_0>0$), following the paper's continuous approximation (p. 7). Poisson expectations are Bochner integrals over $\mathbb N$ against poissonMeasure, evaluated at real arguments $y-n$. $G_i(w_i)$ is the supremum of $G_i$ over $(r_i,r_i+Q_i]$, since the paper's $\arg\max$ need not be attained on a half-open interval.

The sample-path model (cycles, shipment intervals, the paper's Lemmas 1–2) has no substrate, so the system is encoded as the paper's proof uses it:

• $C(r,Q)$ is (1), with $\Omega$ any interval-integrable function satisfying the bound of p. 12, $\Omega(y)\le\lambda_0\bar K/Q_0+\mathbb E[\hat\Gamma(y-D_0)]$; this bound is where Lemmas 1–2 enter and is a hypothesis.
• $\hat\Gamma(x)=\int\sum_ic_i(z_i)\,\kappa(x)(dz)$ for any Markov kernel $\kappa$ concentrated on the feasible states of p. A1 ($z_j\le r_j+Q_j$; $\sum_jz_j\le x$; and $\sum_jz_j<x$ forces $z_i>r_i$ for all $i$), and any measurable, nonnegative admissible charges ($c_i(z)\le\max\{G_i(z),C_i\}$ for $z>r_i$, $c_i(z)\le G_i(z)$ for $z\le r_i$).
• The theorem holds for every such $\kappa$, $c$ and $\Omega$, so the real system is an instance.

$\hat\Gamma$ is never a free function bounded by $\bar\Gamma$, the feasible set keeps the clause for positive warehouse stock, and $G_i$, $C_i$, $\Lambda_0$ are computed from the Poisson law rather than taken as parameters; formalizations that relax any of these, or that rely on a junk value of sSup, an integral or a division, trivialize the statement and are not accepted.

Contributions welcome: convexity and continuity of $G_i$, Poisson integrability lemmas, Lemma 3 for general $N$, and the averaging steps of App. A (8)–(10).

Selected references

• H. Zhu, Y. (F.) Chen, M. Hu, Y. Yang, Technical Note—A Simple Heuristic Policy for Stochastic Distribution Inventory Systems with Fixed Shipment Costs, Operations Research, 2021. SSRN copy of 2020-09-08: https://ssrn.com/abstract=2921743; doi:10.1287/opre.2021.2101.
• Y.-S. Zheng, On properties of stochastic inventory systems, Management Science 38(1), 1992. https://doi.org/10.1287/mnsc.38.1.87
• F. Chen, Y.-S. Zheng, Lower bounds for multi-echelon stochastic inventory systems, Management Science 40(11), 1994. https://doi.org/10.1287/mnsc.40.11.1426

Motivation

In sequential multi-class diagnosis, a decision maker observes a system repeatedly, then chooses when to stop and which hidden class to report. Each new observation can improve the diagnosis, but waiting has a cost. A direct dynamic program uses the vector of posterior class probabilities as its state. With $N+1$ possible classes, that state lies in an $N$-dimensional probability simplex. Wang's model asks when the observed sequence can instead be summarized by fewer coordinates, so that the same posterior can be recovered without retaining a full belief vector as an independent state Wang, §2–§3.

The paper considers class distributions related by exponential tilting. This relationship appears in common one-dimensional distribution families, including the normal, binomial, Poisson, and gamma examples collected in its Table 1 Wang, p. 8. The result targeted here is the belief reconstruction identity of Theorem 1. Later parts of the paper use the reduced statistic in optimality equations and study stopping regions; those results are outside this mission Wang, pp. 12–18.

Setting

The hidden class is $j\in\{0,\ldots,N\}$. Before observing data, the decision maker has a prior belief $\theta=(\theta_0,\ldots,\theta_N)$: every component is nonnegative and their sum is one. Conditional on class $j$, observations $y_1,\ldots,y_t$ are independent and have the same density $f_j$ on the observation space $\mathcal Y$. Class $0$ supplies a baseline density $f_0$. The one-step Bayesian operator $\mathcal B$ multiplies each current class weight by that class's likelihood at the new observation and divides by the sum of all weighted likelihoods. Starting at $\Pi_0=\theta$, the belief $\Pi_t$ is obtained by applying $\mathcal B$ once for each observation in arrival order Wang, pp. 6–7.

In the exponential tilting model, a transformed observation $h(y)\in\mathbb R^p$ and a parameter $\beta_j\in\mathbb R^p$ describe each nonbaseline density:

$$f_j(y)=f_0(y)\exp\{\beta_{j0}+\beta_j^{\mathsf T}h(y)\},\qquad \beta_{j0}=-\log\int_{\mathcal Y}\exp\{\beta_j^{\mathsf T}h(y)\}f_0(y)\,dy.$$

Here $j=1,\ldots,N$. Place the $\beta_j^{\mathsf T}$ in the rows of the diagnostic parameter matrix $\mathbb B$. Its rank decomposition is $\mathbb B=\mathbb R\mathbb P$, where $\mathbb R$ has $N$ rows and $r$ linearly independent columns, while $\mathbb P$ has $r$ linearly independent rows and $p$ columns. Thus $r=\operatorname{rank}(\mathbb B)$. The paper calls $\mathbb R$ the reconstruction matrix and $\mathbb P$ the projection matrix Wang, Definition 1, p. 8.

Formalization targets

Theorem 1: posterior reconstruction

For $t\ge1$, define the diagnostic statistic $x_t=\mathbb P\big(\sum_{m=1}^t h(y_m)\big)/t\in\mathbb R^r$. For classes $j=1,\ldots,N$, the target identity is

$$\Pi_t(y_1,\ldots,y_t,\theta)_j =\mathcal T_j^t(x_t,\theta) =\frac{\theta_j\exp\{t(\beta_{j0}+e_j\mathbb R x_t)\}} {\theta_0+\sum_{i=1}^{N}\theta_i\exp\{t(\beta_{i0}+e_i\mathbb R x_t)\}}.$$

The baseline coordinate is $\mathcal T_0^t=1-\sum_{j=1}^{N}\mathcal T_j^t$. The normalizer appearing in $\mathcal T^t$ is evaluated from the row $e_i\mathbb R\mathbb P$, as in equation (3), and the theorem identifies it with the model normalizer through $\mathbb B=\mathbb R\mathbb P$. The target also identifies the set of posteriors reachable after exactly $t$ observations with $\mathcal T^t(\Omega_t,\theta)$, where $\Omega_t$ is the set of attainable diagnostic statistics. These statements give a precise reading of the paper's claim that reachable beliefs admit an $r$-coordinate representation Wang, Theorem 1, p. 9; Definition 2, p. 10.

The goal additionally states that the map $x\mapsto\mathcal T^t(x,\theta)$ is injective on $\mathbb R^r$ when every prior component is positive. This is an explicit, qualified reading of the paper's phrase that the dimensionality is equal to $r$. For discrete observations, the reachable set $\Omega_t$ can be finite, so the phrase cannot always mean its geometric dimension is literally $r$. The five milestones follow the source's Bayes operator and the displayed identities in its proof of Theorem 1 Wang, p. ec1.

Significance

The formula determines every posterior component from $r$ real coordinates, the prior, and the observation count. When $r$ is smaller than $N$, this supplies the representation used by the paper to reformulate a diagnosis problem in a smaller state space. The paper's examples show cases with one or two diagnostic coordinates; Proposition 1 then rewrites its optimality equations using those coordinates Wang, pp. 9–12. This mission formalizes the reconstruction claim itself, including the exact reachable-set statement, while leaving the decision costs and Bellman equations for later work.

A completed development would provide reusable definitions for a finite-class Bayes update and its sequential iterate, an exponential-tilting model over densities, and a rank-factorized reconstruction map. The result is proved in the cited paper. The Lean declarations in this proposal compile as statements, but their sorry bodies are open proof obligations; this mission seeks machine-checked proofs of them.

Difficulty

The main verification burden is connecting several expressions for the same posterior without quietly replacing one definition by another. A sequential posterior is an iterated one-step update; the paper's closed form is a normalized product of likelihoods; and equation (3) is an exponential expression in a projected sum of transformed observations. Each form has its own denominator, so the positivity conditions that make division meaningful must be stated. The rank claim also requires full-rank assumptions on both factors of $\mathbb B$. For a prior with zero mass on a class, the posterior formula remains meaningful, but the injectivity assertion needs a separate full-support condition.

Formalization scope

Lean represents classes by Fin (N + 1), with class zero as the baseline. Row i : Fin N of the diagnostic matrix is class i.succ. Observations form a List in arrival order; $t$ is its length, and the posterior is the list fold of $\mathcal B$. The observation space is a measurable type with a reference measure $\mu$, covering continuous and discrete densities with one notation. This generalizes the paper's $\mathcal Y\subseteq\mathbb R$; no order or arithmetic operation on observations is used by Theorem 1. Integrals are real-valued, and $N=0$ and $p=0$ are permitted. The reconstruction identity is stated for $t\ge1$, matching the paper and avoiding the division by zero in $x_t$.

The standing assumptions say that every $f_j$ is measurable, $f_0$ is positive at every admitted observation, its integral is one, and each tilted baseline density is integrable. These make the normalizers and the Bayesian denominators meaningful. Positivity, normalization, and integrability are explicit refinements of the paper's use of densities and normalizing constants. The prior lies in the standard simplex; $\theta_0$ need not be positive for reconstruction. The additional full-support condition appears only in the injectivity clause. The paper's conditional independence assumption is represented by multiplying class likelihoods along the list.

The generic Bayesian update and its reachable set are separate from the paper-specific model. In particular, the posterior is an actual fold of the one-step update, and the class densities are given data constrained by exponential tilting. Defining the posterior directly as equation (3), or defining the densities to make the tilting identity true by construction, would erase the result being formalized. A complete proof needs finite-sum identities, exponential and logarithm facts, integrability facts, matrix rank and row identities, and the algebra of probability normalization. The generic Bayes definitions and list-level likelihood identity are reusable beyond this paper; contributions that establish those interfaces or close any source-derived milestone are welcome.

Selected references

• J. Wang, Optimal Sequential Multi-class Diagnosis, Operations Research 70(5), 2022; arXiv:1506.08915v4. The mission cites the v4 preprint's pages and indices.

Motivation

In continuous-review inventory systems with backlogging, the classical constant base-stock (CBS) policy orders one unit whenever one unit of demand arrives, so that the inventory position (net inventory plus in-transit inventory) stays constant. Under CBS with Poisson demand of rate $r$ and i.i.d. lead times with mean $1/\beta$, the in-transit inventory has a Poisson law with mean $r/\beta$, and the steady-state net inventory level $Y^r(\infty)$ fluctuates on the scale $\sqrt r$: $\mathbb E|Y^r(\infty)|/\sqrt r \to 2(2\pi\beta)^{-1/2}$. Average holding and backlog costs therefore grow like $\sqrt r$.

Stolyar and Wang (arXiv:1801.02646, Operations Research 2022) observe that when lead times are random and orders may cross, an inventory manager can exploit the randomness: by ordering more aggressively when the inventory level is low and less when it is high, the variance of the inventory level can be reduced. Their generalized base-stock (GBS) policy implements this with a single gain parameter $\gamma$. The main theoretical result, Theorem 1, identifies the diffusion-scale steady-state law of the inventory level under GBS when lead times are exponential: it is normal with variance $1/(\beta\gamma)$, a factor $\gamma$ below the CBS variance. With $\gamma = \gamma(r) \to \infty$ (Corollary 2), the scaled average cost $\mathbb E|Y^r(\infty)|/\sqrt r$ tends to $0$, so GBS becomes infinitely better than CBS in the limit.

Setting

Demand units (customers) arrive as a Poisson process of rate $r$. Supply units (items) are ordered by the policy and each arrives after an independent exponential lead time with mean $1/\beta$. Let $Y$ be the net inventory level (positive or negative, backlog allowed) and $Z \ge 0$ the number of items in transit. Write $a\vee b=\max(a,b)$, $a\wedge b=\min(a,b)$, $a^+=a\vee 0$, $a^-=(-a)^+$.

The GBS policy has an integer gain $\gamma\ge 1$, a truncation level $f>0$ and a centering $x_*$. With $X_* = r/\beta$ it uses the target and the truncated target

$$X = X_* - \gamma(Y - x_*), \qquad T = [X\wedge(X_*+f)]\vee 0 .$$

At every arrival: a customer sets $Y := Y-1$; an item sets $Y := Y+1$, $Z := Z-1$. Then $T$ is recomputed and $A = \lceil T - Z\rceil\vee 0$ items are ordered, $Z := Z + A$. Under exponential lead times $(Y,Z)$ is a continuous-time Markov chain on $\mathbb Z\times\mathbb Z_+$ with customer rate $r$ and item rate $\beta Z$.

The systems are indexed by $r\to\infty$, with $f = f(r)$ satisfying

$$f(r)/r\to 0, \qquad f(r)/\sqrt r\to\infty,$$

and $x_* = x_*(r)$ arbitrary. A stationary distribution $p$ of a countable chain with rates $q(s,s')$ and exit rates $q(s)$ is a probability mass function with finite mean exit rate satisfying global balance $\sum_s p(s)q(s,s') = p(s')q(s')$.

Formalization targets

Goal: Theorem 1

For every $r>0$ some state is reachable from every state, for all large $r$ the chain has a unique stationary distribution, and for every choice of stationary distributions

$$\frac{Y^r(\infty)-x_*}{\sqrt r}\Rightarrow\mathcal N\big(0,(\beta\gamma)^{-1}\big),\qquad \mathbb E\Big[\frac{Y^r(\infty)-x_*}{\sqrt r}\Big]^{\pm}\to(2\pi\beta\gamma)^{-1/2}.$$

Milestones

In proof order: the stability part of Theorem 1; the conservation law $\beta\mathbb E Z^r(\infty)=r$ (14); the mean bound for the reflected random walk $Q_n$ that dominates the order gap (p. 16, EC.3); Lemma 4, $\mathbb E D^r(\infty)\le\mathbb E\tilde D^r(\infty)\le C$; the conservation law (19) and Lemma 5 for the artificial process, a birth–death chain $\hat Y^r$ that keeps $\hat Z = \lceil\hat T\rceil$ exactly; Corollary 6; the stochastic comparison Lemma 8, $\hat Y^r(\infty)\le_{st}Y^r(\infty)$ and $\hat T^r(\infty)\ge_{st}T^r(\infty)$; the target-gap bound (31); the transfer Lemma 9; and the reduction (36), $\mathbb E Y^r(\infty)/\sqrt r - \mathbb E\hat Y^r(\infty)/\sqrt r\to 0$. For §4 milestones the centering is $x_*\equiv 0$, as in the paper (p. 12).

Significance

The result. Theorem 1 quantifies the value of random lead times: the GBS policy divides the asymptotic variance of the steady-state inventory level by $\gamma$, and the half-normal limits of $\mathbb E[\cdot]^\pm$ give the asymptotic holding and backlog costs, which is what makes the cost comparison with CBS (bounds (12)–(13) and Corollary 2) possible. The artificial-process comparison and Lemma 9 form a reusable template for transferring a diffusion limit from a tractable one-dimensional chain to a higher-dimensional controlled chain.

Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission formalizes the GBS chain itself as explicit transition rates, so the theorem cannot be discharged by a model that only resembles the policy. The stability part is only sketched in the paper ("We omit further details of the stability proof", p. 13), so a complete formal proof also fills that gap. Lemma 5 is a stationary Halfin–Whitt-type limit for a birth–death chain with state-dependent up-rates, including uniform integrability of the scaled tails.

Difficulty

The two-dimensional chain has no product form, and its in-transit inventory does not track the target: after an item arrival $Y$ rises by one while the target $X$ falls by $\gamma$, but only one item leaves transit, so $Z$ overshoots its target and the gap $D = Z - \lceil T\rceil$ is random. The natural argument, "the chain behaves like the birth–death chain with $Z = \lceil T\rceil$", fails on two counts: the steady-state gap must be bounded uniformly in $r$ (Lemma 4), although the rates of the chain grow with $r$ and $Z$ is unbounded on the state space, and the truncations of $T$ at $0$ and at $X_*+f$ produce error terms that must vanish after $1/\sqrt r$ scaling (Corollary 6). Stochastic order alone gives only an inequality between the two laws; closing it needs the mean identity (36), which rests on the exact conservation laws (14) and (19).

Formalization scope

All objects live in the namespace RandomLeadGBS.Diffusion. The state is $(Y,Z)\in\mathbb Z\times\mathbb N$; the demand rate $r$ is real and $r\to\infty$ along atTop. The parameters are $\beta>0$, $\gamma\in\mathbb N$ with $\gamma\ge 1$, $f:\mathbb R\to\mathbb R$ with $f>0$ and (10), and arbitrary $x_*:\mathbb R\to\mathbb R$. The policy is encoded literally: target (4), truncated target (5), order step $Z + \mathrm{toNat}\lceil T - Z\rceil$ applied after every arrival; the item rate is $\beta Z$ and the cap is $X_*+f$ (not $X_*+\gamma x_*+f$).

Conventions committed to:

• a stationary distribution is a probability solution of global balance with finite mean exit rate (the state space is unbounded in $Z$);
• expectations and probabilities are series over states, and every expectation bound also asserts the summability it needs;
• weak convergence $\Rightarrow$ is stated by its definition, through every bounded continuous test function, against Mathlib's gaussianReal 0 (1/(βγ));
• the paper's "irreducible" is replaced by "some state is reachable from every state", because states with $Z<\lceil T(Y)\rceil$ are never entered;
• "uniformly in $r$" and "$\sup_r$" (Lemma 4, Corollary 6, (31)) are stated for all $r\ge r_0$.

The goal concerns the two-dimensional GBS chain; stating it for the artificial chain, or only for an empty family of stationary laws, would trivialize it. The uniqueness clause and the existence clause of Lemma 5 rule out the vacuous reading.

A complete development needs a theory of stationary laws of countable continuous-time chains (existence via drift/Foster criteria, embedded-chain time change), birth–death stationary laws and their local normal asymptotics, and stochastic comparison of chains by coupling. The countable-chain stationarity layer and Lemma 9 are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome. Propositions 3 and 7 (generic comparison results used for Lemma 4 and Lemma 8) are not posed as milestones.

Selected references

• A. L. Stolyar and Q. Wang, Exploiting random lead times for significant inventory cost savings, Operations Research, 2022; preprint arXiv:1801.02646v6, 2021. https://arxiv.org/abs/1801.02646
• S. M. Disney, A. Maltz, X. Wang and R. D. H. Warburton, Inventory management for stochastic lead times with order crossovers, European Journal of Operational Research 248(2), 473–486, 2016. https://doi.org/10.1016/j.ejor.2015.07.047
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• T. Lindvall, Lectures on the Coupling Method, Dover, 1992.
• S. P. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, Springer, 1993. https://doi.org/10.1007/978-1-4471-3267-7

Motivation

A seller that supplies several competing buyers may negotiate a wholesale price with each of them independently and simultaneously (simultaneous negotiation, SN), or may commit to charge all of them the same price (price-matching negotiation, PM). PM is the bargaining counterpart of the most-favoured-customer clause, a contractual guarantee that a customer receives the best price the vendor gives anyone. Retailers such as Walmart and Costco demand such clauses from common suppliers, and buyers command them expecting to obtain the same price as their rivals (Shang and Cai, §1). Shang and Cai (MSOM, 2021; SSRN 3021563) ask who benefits from PM relative to SN when wholesale prices are the outcome of Nash bargaining between the seller and each buyer, and show that with symmetric buyers PM benefits the seller and hurts both buyers.

The model builds on the bilateral-bargaining framework of Horn and Wolinsky (1988), in which a common supplier negotiates simultaneously with competing downstream firms, and on the analysis of negotiated wholesale contracts by O'Brien and Shaffer (2005, RAND Journal of Economics 36, 573–595) and Dukes, Gal-Or and Srinivasan (2006).

Setting

A seller supplies an intermediate good to Buyer 1 and Buyer 2, who each turn one unit of it into one unit of a substitutable end product. With demand base $a > 0$ and substitutability $\gamma \in [0,1)$, retail prices and quantities satisfy the reverse demand system $p_i = a - x_i - \gamma x_j$, $j = 3 - i$.

The game has two stages.

1. Retail stage. Given wholesale prices $(w_i, w_j)$, the buyers set retail prices in a differentiated Bertrand game. Buyer $i$ earns $\pi_i = (p_i - w_i)x_i$ and the seller earns $\pi_s = w_i x_i + w_j x_j$. Writing $\hat p_i(w_i,w_j)$ and $\hat x_i(w_i,w_j)$ for the equilibrium prices and quantities, the second-stage profits are $\pi_i(w_i,w_j)$ and $\pi_s(w_i,w_j)$.
2. Negotiation stage. Wholesale prices are set by generalized Nash bargaining: Buyer $i$ has bargaining power $\theta_i \in (0,1)$ against the seller, who has $1-\theta_i$. A bargain over a price $w \ge 0$ with buyer payoff $U(w)$, seller payoff $V(w)$ and disagreement point $(0, d)$ selects the individually rational $w$ maximizing $U(w)^{\theta_i}(V(w) - d)^{1-\theta_i}$.

If a negotiation fails, the seller can sell to the other buyer alone. Then Buyer $j$ faces demand $a - p_j$, and the seller earns the monopoly profit $\pi^M_s(w_j)$.

The two mechanisms are:

• Simultaneous negotiation (SN). The seller bargains with both buyers at once. A pair $(w^{SN}_1, w^{SN}_2)$ is an equilibrium if each $w^{SN}_i$ solves dyad $i$'s bargain with payoffs $\pi_i(\cdot, w^{SN}_j)$, $\pi_s(\cdot, w^{SN}_j)$ and disagreement point $(0, \pi^M_s(w^{SN}_j))$.
• Price matching (PM). The seller bargains with one buyer first; the other buyer accepts the same price. If the first bargain fails, the seller bargains with the other buyer alone, reaching $\hat w_j$. The PM price $w^{PM}$ solves the bargain with payoffs $\pi_i(w,w)$, $\pi_s(w,w)$ and disagreement point $(0, \pi^M_s(\hat w_j))$.

The Lean development uses this notation: pHat, xHat, piB ($\pi_i$), piS ($\pi_s$), piMb, piMs, IsNashBargain, IsSNEq, IsPMPrice.

Formalization targets

Goal: Theorem 1 (p. 10)

With symmetric power $\theta_1 = \theta_2 = \theta \in (0,1)$, an SN equilibrium and a PM equilibrium price exist, and for every SN equilibrium $(w_1, w_2)$ and every PM price $w$

$$\pi_s(w_1,w_2) < \pi_s(w,w), \qquad \pi_1(w,w) < \pi_1(w_1,w_2), \qquad \pi_2(w,w) < \pi_2(w_2,w_1).$$

The goal is stated about the equilibrium predicates, not about the closed-form prices, so that it asserts the comparison of the two mechanisms as the paper defines them.

Milestones

1. The retail equilibrium $\hat p_i$, $\hat x_i$ and the profit formulas (1)–(2), §3.1.1.
2. The single-channel monopoly price and profits, §3.1.2.
3. The single-channel bargain $\hat w_j = (1-\theta_j)a/2$, with $\pi^M_s(\hat w_j) = (1-\theta_j^2)a^2/8$, §3.2.2.
4. The SN equilibrium is unique and equals $w^{SN} = \dfrac{(1-\theta)(1-\gamma)(2+\gamma)a}{2(1-\gamma)(2+\gamma) + \gamma^2(1+\gamma)(2-\gamma)\theta}$, §3.2.1.
5. The PM equilibrium price is unique and equals $w^{PM}_i = \tfrac a4\bigl(3 - \theta_i - \sqrt{1 - \gamma\theta_i + \gamma^2\theta_i + \theta_i^2 + (1+\gamma)(2-\gamma)\theta_i\theta_j^2}\bigr)$, §3.2.2, for general $\theta_i, \theta_j$.
6. $0 < w^{SN} < w^{PM} \le a/2$ under symmetric power, §3.2.2.
7. At a common price, $\pi_s(w,w)$ increases on $[0, a/2]$ and $\pi_i(w,w)$ decreases on $[0,a]$ (proof of Theorem 1, Online Supplement p. 1).

Significance

Theorem 1 separates the effect of the negotiation mechanism from any asymmetry between buyers: under symmetric power the buyers are interchangeable, SN gives them the same price, and still the mechanism alone moves surplus from the buyers to the seller. The paper's explanation is that price matching lowers a buyer's incentive to negotiate the price down, so the matched wholesale price is higher (p. 10). The paper builds its asymmetric-power, side-payment and spot-market results (§§4–6) on this comparison.

The result is proved in the paper; nothing here is open. Neither the result nor its ingredients have been formalized. The mission produces a machine-checked account of a two-stage bargaining-over-competition model: the Bertrand stage, the Nash-bargaining stage with endogenous disagreement points, and the closed-form equilibria. Two steps the paper only asserts become formal obligations: uniqueness of the SN equilibrium, and the claim that the closed-form PM price is the global maximizer of the Nash product.

Difficulty

The comparison step is short once the closed forms are known: by milestones 6 and 7 the PM price is higher, the seller's diagonal profit increases, and the buyers' decreases. The work is in the equilibrium characterizations.

• In SN each dyad's disagreement payoff $\pi^M_s(w_j)$ depends on the other dyad's outcome, so an equilibrium is a fixed point of two coupled Nash-product maximizations. The paper asserts uniqueness. The best-response map is not a contraction for $\gamma$ near $1$, so a contraction argument does not give uniqueness directly.
• The Nash products involve real powers with exponents $\theta$ and $1-\theta$. Showing that the first-order condition picks out the global maximizer over the individually rational set requires a concavity or single-peakedness argument, not just a derivative computation.
• The PM closed form contains a square root. Comparing it with the rational function $w^{SN}$ is an inequality in three parameters $(\gamma, \theta, a)$.

Formalization scope

All quantities are real numbers. The standing assumptions are $a > 0$, $\gamma \in [0,1)$ and every bargaining power in $(0,1)$. The sign $a > 0$ is added; the paper never states it.

• Bargaining. A Nash bargaining solution maximizes $U^{\theta}(V-d)^{1-\theta}$ over the individually rational prices $\{w \ge 0 : U(w) \ge 0,\ V(w) \ge d\}$. Lean's Real.rpow is the real power only on non-negative bases, and the individually rational set guarantees non-negative bases.
• Feasible domain. Equilibrium wholesale prices are required to lie in $[0,a]$, the paper's "entire feasible domain" (p. 9; Online Supplement p. 1); bargaining deviations range over all individually rational $w \ge 0$.
• Second-stage profits. $\pi_i$ and $\pi_s$ are defined from the demand system at $(\hat p_i,\hat p_j)$, not by the closed forms (1)–(2), so milestone 1 is a genuine identity.
• PM outcome. In PM the matched price applies to both buyers, and the seller negotiates first with Buyer 1. With symmetric power the choice of first buyer is immaterial.
• Preference. "Prefers" is strict; $\theta \in (0,1)$ excludes the paper's equality cases.

Substituting the closed-form prices $w^{SN}$, $w^{PM}$ into the profit comparison would turn Theorem 1 into the algebra of milestones 6–7. The goal is therefore stated for every equilibrium of each mechanism, together with existence of both equilibria, so neither the closed forms nor a vacuous equilibrium set can discharge it.

A complete development needs:

• concavity of the Nash product along the individually rational interval (reusable for other one-dimensional Nash-bargaining models);
• the Bertrand equilibrium of a linear differentiated duopoly;
• real-analysis inequalities involving square roots.

Contributions to any milestone, or to reusable lemmas on maximizing $u^{\theta} v^{1-\theta}$ over an interval, are welcome.

Selected references

• W. Shang and G. Cai, Implications of Price Matching in Supply Chain Negotiation, Manufacturing & Service Operations Management, 2021 (accepted manuscript, SSRN 3021563). https://ssrn.com/abstract=3021563 — DOI https://doi.org/10.1287/msom.2021.0992
• H. Horn and A. Wolinsky, Bilateral Monopolies and Incentives for Merger, RAND Journal of Economics 19(3), 408–419, 1988. https://doi.org/10.2307/2555721
• D. P. O'Brien and G. Shaffer, Bargaining, Bundling, and Clout: The Portfolio Effects of Horizontal Mergers, RAND Journal of Economics 36, 573–595, 2005.
• A. Dukes, E. Gal-Or and K. Srinivasan, Channel Bargaining with Retailer Asymmetry, Journal of Marketing Research 43, 84–97, 2006. https://doi.org/10.1509/jmkr.43.1.84
• E. Kalai, Nonsymmetric Nash Solutions and Replications of 2-Person Bargaining, International Journal of Game Theory 6(3), 129–133, 1977. https://doi.org/10.1007/BF01770215

Motivation

Shared computing infrastructure — a data-centre cluster, a cloud platform's memory — is divided among users who arrive over time. Two requirements pull against each other. Proportional fairness asks that, when $t$ users are present, each holds at least a $1/t$ fraction of the resource. Limited disruption asks that the system not take resource away from running jobs at every arrival, because preemption and reallocation are costly; production cluster managers such as Google's Borg impose an explicit cap on the number of task disruptions an update may cause (Verma et al., 2015, as quoted in Vardi–Psomas–Friedman 2022, pp. 945–946). If reallocation were free, the resource could be re-split evenly at every arrival; if fairness did not matter, the first user could keep everything. The question is how much fairness survives a hard cap on disruptions.

Earlier work on dynamic fair division (Walsh 2011, online cake cutting; Kash, Procaccia and Shah 2014) did not allow reallocation at all. Friedman, Psomas and Vardi (EC 2017) introduced control vectors and gave non-optimal algorithms. Vardi, Psomas and Friedman (Mathematics of Operations Research, 2022) give an optimal algorithm for every control vector once the target ratio is known, and compute the optimal ratio exactly for uniform disruption budgets. This mission formalizes that exact computation.

Setting

One unit of a homogeneous, divisible resource is shared. Users arrive one at a time and never leave (the paper treats arrivals and departures separately; §§3–5, which this mission covers, are arrivals only). Users are labelled by arrival order, and $X^t_k$ is the share of the $(k+1)$-th user when $t$ users are present.

A control vector $\psi$ of length $n \in \{1,2,\dots\}\cup\{\infty\}$ fixes, for each arrival $1 \le t \le n$, a budget $\psi[t]$: when the $t$-th user arrives, at most $\psi[t]$ of the $t-1$ users already present may have their share strictly reduced (disrupted). Increasing a share is free. The $d$-uniform control vector has $\psi[t] = d$ for every $t$, of any length, finite or infinite.

An allocation sequence $X = (X^1, X^2, \dots)$ for $\psi$ is feasible if at every time $1 \le t \le n$ the shares are nonnegative, sum to at most $1$, and respect the disruption budget. Its fairness ratio is

$$\inf_{1 \le t \le n}\; t \cdot \min_{k<t} X^t_k ,$$

the smallest share relative to the proportional share $1/t$, in the worst time step. The fairness ratio of the control vector, $\mathrm{FAIRNESS}(\psi)$, is the supremum of this quantity over all feasible allocation sequences, and

$$\mathrm{FAIRNESS}(d\text{-uniform}) = \inf_{\psi\ d\text{-uniform}} \mathrm{FAIRNESS}(\psi).$$

The frugally fair algorithm $\mathrm{FFA}(\psi,\sigma)$ takes a target ratio $\sigma$: when user $t$ arrives, it gives the newcomer $\sigma/t$ and cuts the $\psi[t]$ largest existing shares to $\sigma/t$. It may allocate more than one unit; $S^t$ denotes its total allocation at time $t$.

Formalization targets

Goal: Theorem 4

For every integer $d \ge 1$,

$$\mathrm{FAIRNESS}(d\text{-uniform}) \;=\; \sigma^*_d \;:=\; \frac{1}{(d+1)\ln\!\big(\frac{d+1}{d}\big)} .$$

The goal states this in three parts: the infinite $d$-uniform vector admits one feasible allocation sequence with ratio at least $\sigma^*_d$; for every $\sigma > \sigma^*_d$ some finite $d$-uniform vector admits no feasible allocation sequence with ratio $\sigma$; and the infimum over all lengths of $\mathrm{FAIRNESS}$ equals $\sigma^*_d$. For $d = 1$, $\sigma^*_1 = 1/(2\ln 2) \approx 0.721$.

Milestones

1. Feasible runs of FFA yield feasible allocation sequences with the same shares and ratio $\sigma$ (§3, p. 949).
2. Theorem 1 (p. 950): if any algorithm achieves a nonnegative ratio $\sigma$ on $\psi$, then $\mathrm{FFA}(\psi,\sigma)$ is feasible at every time.
3. Lemma 1 (p. 951): $\mathrm{FFA}(\psi,\sigma)$ is $\mathrm{FFA}(\psi,\sigma')$ scaled by $\sigma/\sigma'$.
4. Proposition 2 (p. 952): $\mathrm{FAIRNESS}(\psi) \le \mathrm{FAIRNESS}(\psi')$ when $\psi'$ is a prefix of $\psi$.
5. Lemma E.1 (p. 959): the explicit allocation of FFA on the infinite $d$-uniform vector at time $t = \ell(d+1)+i$.
6. $S^t$ is nondecreasing in $t$ on the $d$-uniform vector (p. 959).
7. Display (E.1) (p. 959): $\lim_{\ell\to\infty} S^{\ell(d+1)} = \sigma(d+1)\ln\frac{d+1}{d}$.

Significance

The theorem gives a closed-form price of limited disruption: with $d$ reallocations per arrival, a system can guarantee every user $\sigma^*_d/t$ of the resource forever, and no algorithm can guarantee more uniformly over all horizons. Since $\sigma^*_d = 1 - \frac{1}{2d} + O(d^{-2})$, a modest budget already recovers most of proportional fairness, which is the quantitative content a system designer needs to choose $d$. Combined with Theorem 1, the value also turns FFA into a concrete optimal algorithm for the infinite $d$-uniform vector, running online with no knowledge of the horizon.

The result is proved in the paper; to the best of a search of the Prove2Me catalogue, nothing about control vectors, disruption-limited fair division or this constant is formalized there. The mission produces a machine-checked model of disruption-limited dynamic allocation, a formal optimality proof for a greedy online algorithm (Theorem 1) that is reusable for other control vectors (the paper's finite-vector algorithm and $c$-gap bounds rest on the same theorem), and an explicit harmonic-sum asymptotic.

Difficulty

The impossibility half must rule out every algorithm, including ones that over-allocate early, raise shares opportunistically and choose whom to disrupt adaptively. The first idea, comparing total allocations time by time, fails: an arbitrary algorithm's allocation is not entrywise comparable with any fixed reference allocation, and a single well-chosen disruption can change which users are largest. The attainment half needs one allocation sequence for an unbounded horizon, so it cannot be obtained from finitely many feasibility checks; and the value $\sigma^*_d$ is not the outcome of any finite computation but a limit of harmonic-number differences. The paper's own computation of the one-step change in total allocation contains a slip (a missing factor $\ell$; the sign is unaffected), so that step cannot be transcribed as printed.

Formalization scope

Everything is real-valued and lives in DynFairDiv.Uniform. A control vector is ψ : ℕ → ℕ (index $t \ge 1$) with a horizon n : ℕ∞, where ⊤ is the infinite vector; uniformCV d is the constant vector. Allocation sequences are X : ℕ → ℕ → ℝ with users labelled by arrival order, which is equivalent to the paper's sorted vectors because feasibility uses only sums, fairness only minima, and a disruption is a strict decrease of a given user's share; the newcomer is never counted as disrupted. Fairness at least $\sigma$ is σ / t ≤ X t k for all $1 \le t \le n$ and $k < t$. $\mathrm{FAIRNESS}(\psi)$ is a real sSup, genuine for $n \ge 1$. FFA's state is a list of shares kept in nonincreasing order, so "the $\psi[t]$ largest shares" is the front of the list. Departures (the paper's §6) are not modelled.

Added hypotheses, each disclosed in its item: $d \ge 1$ throughout §5.1 (the paper's own assumption); $\sigma \ge 0$ for milestones 1, 2 and 6 (the paper's fairness ratios lie in $[0,1]$); $\sigma' \ne 0$ in Lemma 1; a prefix of length at least $1$ in Proposition 2. Milestone 1 identifies the resulting sequence's shares with FFA's shares at each time.

A trivializing reading is ruled out: the impossibility half quantifies over every feasible allocation sequence, not only FFA-like or sorted ones, and the attainment half asks for a single sequence on the infinite horizon rather than one per finite length.

A complete development needs basic facts about FFA's list (length, order, scaling) and the harmonic asymptotics already in Mathlib (Real.tendsto_harmonic_sub_log). The FFA model and Theorem 1 apply to arbitrary control vectors and are reusable for the paper's finite-vector and $c$-gap results; contributions of auxiliary lemmas about FFA (length, sortedness, scaling) are welcome.

Selected references

• S. Vardi, A. Psomas, E. Friedman, Dynamic Fair Resource Division, Mathematics of Operations Research 47(2):945–968, 2022. https://doi.org/10.1287/moor.2021.1155
• E. Friedman, C.-A. Psomas, S. Vardi, Controlled Dynamic Fair Division, Proc. 18th ACM Conference on Economics and Computation (EC), 461–478, 2017.
• I. A. Kash, A. D. Procaccia, N. Shah, No Agent Left Behind: Dynamic Fair Division of Multiple Resources, Journal of Artificial Intelligence Research 51:579–603, 2014.
• T. Walsh, Online Cake Cutting, Algorithmic Decision Theory (ADT), Springer, 292–305, 2011.
• A. Verma, L. Pedrosa, M. Korupolu, D. Oppenheimer, E. Tune, J. Wilkes, Large-Scale Cluster Management at Google with Borg, Proc. 10th European Conference on Computer Systems (EuroSys), 2015.