Algorithmic Game Theory

Motivation

In a prophet inequality, a decision maker observes random rewards one at a time and must choose without seeing future realizations. The benchmark is a prophet who sees all rewards and selects their maximum. A nonadaptive threshold rule chooses a threshold for each reward before observations begin, then accepts the first arriving reward that crosses its threshold. This model captures a simple class of stopping rules and, through the prophet inequality connection, informs posted price mechanisms in which prices are set before buyers arrive. Correa et al. (2021) prove that under uniformly random arrival order some such rule earns at least a $1-1/e$ fraction of the prophet's expected reward. The question here is whether that guarantee improves when the reward distributions are identical.

Setting

Fix an integer $n\ge 2$ and draw $n^2$ independent rewards $X_1,\ldots,X_{n^2}$ from the same three point law. A reward is $H_n=n/(e-2)$ with probability $1/n^3$, is $1$ with probability $1/n$, and is $0$ otherwise. The three probabilities are nonnegative and sum to one for $n\ge2$. Thus a typical sample contains roughly $n$ unit rewards, while a high reward is rare enough that its presence among all $n^2$ draws has probability on the order of $1/n$. Its magnitude is on the order of $n$, so it still makes a nonvanishing contribution to the prophet's expected reward.

Give each coordinate $i$ a predetermined threshold $\tau_i\in[0,\infty]$. A uniformly random order reveals the sampled rewards, and the rule accepts the first $X_i>\tau_i$. Conditional on a sample, let $A(x,\tau)=\{i:x_i>\tau_i\}$. Each accepted coordinate is equally likely to arrive first among $A(x,\tau)$, so the conditional expected reward is

$$R_n(x,\tau)=\frac{\sum_{i\in A(x,\tau)}x_i}{|A(x,\tau)|},\qquad R_n(x,\tau)=0\text{ if }A(x,\tau)=\varnothing.$$

Write $V_n(\tau)=\mathbb E[R_n(X,\tau)]$ for the rule's reward and $P_n=\mathbb E[\max_i X_i]$ for the prophet's reward. These are expectations of nonnegative random variables. The thresholds may be infinite, allowing a coordinate to be discarded in advance.

Formalization targets

The goal is the paper's i.i.d. tightness claim: for every $\varepsilon>0$, sufficiently large members of this explicit family satisfy

$$\forall\tau\in[0,\infty]^{n^2},\qquad V_n(\tau)<(1+\varepsilon)(1-1/e)P_n.$$

The universal quantifier includes every nonadaptive threshold vector, including asymmetric thresholds and coordinates that are never accepted. The proof in Appendix B supports the displayed statement for every sufficiently large $n$, which strengthens the existence of one hard instance stated in Section 3.1. Together with the paper's $1-1/e$ lower bound, this shows that the factor cannot be raised for this rule class even under identical distributions.

The milestones cover the prophet limit $P_n\to(e-1)/(e-2)$, reduction of arbitrary thresholds to two-level rules, the three contributions to a two-level rule's expected reward according to the number of high observations, Proposition A.3's scalar maximization, and the resulting uniform asymptotic bound on all two-level rules. The first $k$ coordinates of a two-level rule accept both $1$ and $H_n$; the remaining coordinates accept only $H_n$. These targets correspond to Section 3.1, Proposition A.3, and Appendix B of Correa et al..

Significance

The explicit i.i.d. family locates a limit of nonadaptive thresholds under random arrivals. Identical distributions remove heterogeneity as an explanation for the loss against a prophet: the obstruction remains even when every reward has the same law. Consequently, an improved guarantee requires a richer rule class or additional assumptions on the distribution. The paper studies an adaptive threshold rule separately and obtains a stronger i.i.d. guarantee; this mission isolates the upper bound for the nonadaptive class.

Formalizing this result supplies a reusable model for random-order threshold selection on a finite i.i.d. product space, including its conditional reward formula and extended nonnegative expectations. The paper proves the tightness result; the Lean declarations in this proposal state it and its supporting results as proof obligations. The published i.i.d. product-measure model from the Samuel-Cahn development already has machine-checked definitions and is reused here. The proposed upper-bound theorems have not yet been proved in Lean.

Difficulty

Bounding each coordinate's expected contribution in isolation loses the interaction between unit rewards and the rare high reward. When a high reward occurs, accepting many unit rewards can dilute its share of the random-order reward; rejecting unit rewards sacrifices ordinary samples. The reduction to two-level rules must apply to every threshold vector before the count of unit-accepting coordinates can be optimized. Appendix B then controls the cases of zero, one, and at least two high observations uniformly in that count. The one-high-value case contains a printed final inequality that drops a positive $1/n$ term; the formal target uses the preceding, valid bound, whose extra term vanishes in the limit.

Formalization scope

Lean represents a sample as Fin (n ^ 2) → ℝ and its law as a finite product measure. The index set is 0-based: the paper's $X_1,\ldots,X_k$ are coordinates $0,\ldots,k-1$. The law is used only for $n\ge2$, where it is a probability measure. Thresholds have type $\mathbb R_{\ge0}\cup\{\infty\}$, and crossing is strict, matching Theorem 1's indicator $Y_i=\mathbf1\{X_i>\tau_i\}$. The page describes its two-level rule with weak threshold language; under strict crossing the same acceptance sets use thresholds $0$ and $1$. The reward uses the paper's $0/0=0$ convention. Expectations are lintegrals with values in $[0,\infty]`, avoiding a zero default for nonintegrable real integrals. The goal quantifies over all threshold vectors and uses the actual prophet expectation of the same law; no restricted rule class or surrogate benchmark can replace either one.

The general i.i.d. law, sample maximum, and expected maximum come from SamuelCahnProphet.IID.Setting. The paper's three point law, random-order reward, canonical two-level rule, and high-value count are local definitions. Useful contributions include exact finite-law calculations, dominance of two-level rules, uniform estimates in $k$, and the scalar exponential inequality of Proposition A.3. These parts can also support formal work on other finite-support prophet inequalities.

Selected references

• Correa, Foncea, Hoeksma, Oosterwijk, and Vredeveld, Posted price mechanisms and optimal threshold strategies for random arrivals, Mathematics of Operations Research 46(4):1452–1478, 2021. DOI 10.1287/moor.2020.1105.
• Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Annals of Probability 12(4):1213–1216, 1984. DOI 10.1214/aop/1176993150.

Motivation

A prophet inequality compares a gambler who sees nonnegative random rewards $X_1,\ldots,X_n$ one at a time, and must accept or reject each on arrival, with a prophet who knows all values in advance and simply takes $\max_i X_i$. For independent and identically distributed (i.i.d.) rewards the question is the best constant $\beta$ such that some online rule always earns at least $E(\max_i X_i)/\beta$. The question matters in operations research and mechanism design because a seller who posts take-it-or-leave-it prices to arriving customers faces exactly this stopping problem on the customers' virtual values; prophet inequalities translate into revenue guarantees for posted price mechanisms relative to Myerson's optimal auction (Chawla, Hartline, Malec and Sivan 2010).

Timeline (as recounted in §1 of the paper):

• Hill and Kertz (1982) characterized, through a recursion, the smallest constants $a_n$ with $E(\max_iX_i)\le a_n\sup_tE(X_t)$ for $n$ i.i.d. nonnegative variables, showed $1.1<a_n<1.6$, gave instances where $a_n$ cannot be beaten, and conjectured that $(a_n)$ is monotone; the computation of its limit was left open.
• Kertz (1986) proved $a_n\to\beta^*\approx1.341$, the solution of the integral equation (2) below, and conjectured that $\beta^*$ bounds every $a_n$; the best uniform bound then known was $a_n\le e/(e-1)\approx1.582$.
• Abolhassani et al. (2017) improved the uniform bound to $1/0.738\approx1.355$.
• Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (EC 2017; Math. Oper. Res. 2021) proved $E(\max_iX_i)\le\beta^*E(X_t)$ for a threshold rule $t$, so $a_n\le\beta^*$ for all $n$ and $1/\beta^*\approx0.745$ is the tight i.i.d. guarantee.

Setting

Let $X_1,\ldots,X_n$ be i.i.d. nonnegative random variables with distribution function $F$. A threshold rule fixes real numbers $\tau_1,\ldots,\tau_n$ and stops at

$$t=\min\{i\in\{1,\ldots,n\}: X_i\ge\tau_i\},$$

receiving $X_t$. Because the thresholds may change with the step $i$, the rule is adaptive; for i.i.d. variables the number of variables already seen is all the history the rule needs.

The analysis works with quantiles. The generalized inverse is $F^{-1}(q)=\inf\{x\ge0: F(x)\ge q\}$, and $\tau(q)=F^{-1}(1-q)$ is the threshold that accepts with probability $q$ (with a coin toss to break ties at an atom). The function

$$R(q)=\int_0^qF^{-1}(1-\theta)\,d\theta$$

is the expected reward from a variable accepted with probability $q$. The quantile stopping rule of Algorithm 2 partitions $[0,1]$ into intervals $A_i=[\varepsilon_{i-1},\varepsilon_i]$, draws an acceptance probability $q_i\in A_i$ with density proportional to $\psi(q)=(n-1)(1-q)^{n-2}$, and stops at step $i$ with probability $q_i$; its value is $E(X_r)$. The analysis then passes through the normalizations $\gamma_i=\int_{A_i}\psi$ and $\rho_i$, the recursion (8)–(9) on $x_i=1-\varepsilon_i$, and the differential equation

$$y'(t)=y(t)\big(\ln y(t)-1\big)-(\beta-1),\qquad y(0)=1.\qquad\text{(ODE)}$$

Formalization targets

Goal: Theorem 2

Let $\beta^*>1$ be the unique solution of

$$\int_0^1\frac{dy}{y(1-\ln y)+(\beta-1)}=1.\qquad(2)$$

For every $n\ge1$ and every law of nonnegative i.i.d. $X_1,\ldots,X_n$ there are thresholds $\tau_1,\ldots,\tau_n$ with

$$E(\max\{X_1,\ldots,X_n\})\le\beta^*E(X_t).$$

Milestones

In order: the quantile sandwich $P(X\ge\tau(q))\ge q\ge P(X>\tau(q))$; the representation (7) $E(\max_iX_i)=n\int_0^1\psi(q)R(q)\,dq$; the identity "expected reward of the quantile rule at $q$ equals $R(q)$"; Lemma 4 ($E(X_r)=\sum_i\rho_i\int_{A_i}\psi R$); Lemma 5 ($E(\max_iX_i)=n\gamma_1E(X_r)$ when all $\rho_i$ agree); the equivalence of equal $\rho_i$ with the recursion (8) and $\gamma_1=1-x_1^{n-1}$; the closed form (9)–(10); Lemma 6 on (ODE); Proposition D.1; Lemma 7 ($x_i^{n-1}<y(i/n)$); uniqueness of $\beta^*$ in (2); optimality of the dynamic-programming thresholds; domination of the randomized rule by them; and $n(1-x_1^{n-1})\le\beta^*$.

A companion statement records the numerical guarantee $1/\beta^*>0.745$.

Significance

The result. Theorem 2 gives the optimal constant of the i.i.d. prophet inequality and, through $a_n=n(1-x_1^{n-1})$, shows $a_n\le\beta^*$ for every $n$, which settles the problem posed by Hill and Kertz in 1982. Since $a_n\to\beta^*$ (Kertz 1986), no rule of any kind achieves a better constant uniformly in $n$. Through the virtual-value connection it implies that, for customers with i.i.d. valuations, an adaptive posted price mechanism earns at least a $1/\beta^*>0.745$ fraction of the optimal auction's revenue (Corollary 2 of the paper).

Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of any of its lemmas is known. The proof combines a measure-theoretic part (quantile functions, randomized tie-breaking at atoms, Tonelli and integration by parts), a combinatorial recursion, and real analysis of an autonomous ODE with a third-derivative Taylor argument. Formal versions of these parts are reusable: the quantile representation of $E(\max_iX_i)$, the expected reward of a quantile rule, and the optimality of dynamic-programming thresholds are standard tools across prophet inequalities and optimal stopping.

Difficulty

The obvious attempt, computing the optimal dynamic-programming thresholds and bounding their value against $E(\max_iX_i)$, does not lead to a closed-form constant: the optimal values satisfy a nonlinear recursion that depends on the whole distribution. The paper avoids it by analysing a randomized rule whose value is exactly a $\psi$-weighted average of $R$, which reduces the problem to a distribution-free recursion. Two steps then carry the weight. First, randomizing correctly at atoms of $F$ so that every step accepts with probability exactly $q$; without this, $R(q)$ is not the step reward. Second, comparing the discrete recursion (9) with the continuous (ODE): the comparison needs strict convexity and $y'''>0$, and the latter holds only because $\beta>1.25$, a standing assumption validated at $\beta^*$ at the end. The existence of the partition with all $\rho_i$ equal (a solution of (8) with $x_0=1$, $x_n=0$, $x_i\in(0,1)$) is taken from Hill and Kertz and is not proved in the paper.

Formalization scope

Lean conventions:

• The common law is a probability measure $\mu$ on $\mathbb R$ with $\mu((-\infty,0))=0$; the sample is the coordinate vector of SamuelCahnProphet.IID.iidLaw μ n (the published i.i.d. setting), and $E(\max_iX_i)$ is its Emax. Coordinates are 0-based; the partition $\varepsilon_i$, $\gamma_i$, $\rho_i$ and the recursion keep the paper's 1-based index.
• All expectations of the random variables, $R(q)$ and $E(X_r)$ are lower Lebesgue integrals in $[0,\infty]$; no integrability is assumed in the goal, so infinite means are covered. Only bounded deterministic integrals ($\gamma_i$, $\rho_i$, (2)) are interval integrals.
• $X_t$ is $0$ when no $X_i$ reaches its threshold (the page leaves it undefined; $0$ is the least favourable choice).
• The quantile rule's coin at an atom is an independent uniform variable on $[0,1]$; acceptance probabilities are drawn independently with density $\psi/\gamma_i$ on $A_i$.
• $\beta^*$ enters through (2) and $\beta^*>1$, not through a choice function; uniqueness is a milestone.
• Statements involving $\psi$, $\gamma_i$, $\rho_i$ or the recursion assume $n\ge2$ (for $n=1$, $\psi\equiv0$). Lemmas 6 and 7 carry §4's standing assumption $\beta>1.25$; Proposition D.1 carries $\beta>1.25$. Lemma 6 does not assert existence of a solution of (ODE) on $[0,1]$, which fails for $\beta>\beta^*$.
• The dynamic-programming milestones assume $E X<\infty$ and use the optimal-stopping recurrence $V_i=E[\max(X,V_{i+1})]$; the page prints $V_i=E(X\mid X\ge\tau_i)$, which is a slip.
• The page's "$\beta^*\approx1.341>1/0.745$" has its inequality reversed and is not formalized.

A degenerate $\beta$ cannot trivialize the goal: $\beta$ is pinned by (2) and $\beta>1$, and the goal is stated for every $n\ge1$ and every nonnegative law, including laws with infinite mean.

A complete development needs the quantile function of a law on $\mathbb R$, Tonelli's theorem on product measures, uniqueness for ODEs with locally Lipschitz right-hand side (ODE_solution_unique), and Taylor's theorem; the existence of the Hill–Kertz partition is a further proof obligation. Contributions to any milestone, and reusable lemmas on quantile functions and finite-horizon optimal stopping, are welcome.

Selected references

• J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted price mechanisms and optimal threshold strategies for random arrivals, Mathematics of Operations Research 46(4):1452–1478, 2021. https://doi.org/10.1287/moor.2020.1105
• T. P. Hill, R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, Annals of Probability 10(2):336–345, 1982. https://doi.org/10.1214/aop/1176993861
• R. P. Kertz, Stop rule and supremum expectations of i.i.d. random variables: a complete comparison by conjugate duality, Journal of Multivariate Analysis 19(1):88–112, 1986. https://doi.org/10.1016/0047-259X(86)90095-3
• M. Abolhassani, S. Ehsani, H. Esfandiari, M. T. HajiAghayi, R. Kleinberg, B. Lucier, Beating 1−1/e for ordered prophets, Proc. 49th ACM STOC, 61–71, 2017. https://doi.org/10.1145/3055399.3055479
• S. Chawla, J. D. Hartline, D. L. Malec, B. Sivan, Multi-parameter mechanism design and sequential posted pricing, Proc. 42nd ACM STOC, 311–320, 2010. https://doi.org/10.1145/1806689.1806733

Motivation

When indivisible goods are shared among people, comparing each person's bundle with another person's bundle is only one way to judge fairness. A second test asks whether a group could repartition the goods it collectively received so that one of its members would reliably obtain more. Groupwise maximin share (GMMS) makes this test for every subgroup. It strengthens the ordinary maximin-share benchmark, which tests only the grand coalition and all goods. Chaudhury, Kavitha, Mehlhorn and Sgouritsa use this distinction to study a complete allocation obtained from their almost envy-free allocation: goods initially left unassigned are given to one unenvied agent. Their Theorem 16 proves that the resulting allocation gives every agent at least four sevenths of her groupwise maximin share under additive valuations. Chaudhury et al., pp. 4–5, 15–16.

The paper first constructs a partial EFX allocation whose unallocated goods have bounded value to every agent. Its Section 3 then assumes additive valuations and derives maximin-share and GMMS guarantees. This mission addresses the GMMS consequence of that construction. The existence of the starting allocation is the subject of the first mission in this series; the present theorem specifies what happens when its pool is donated. Chaudhury et al., Theorems 8 and 16.

Setting

Let $N$ be a finite set of agents and $M$ a finite set of indivisible goods. Each agent $i$ has a valuation $v_i(S)$ for a bundle $S\subseteq M$. Here valuations are nonnegative and additive: $v_i(S)$ is the sum of the values of the individual goods in $S$. A partial allocation $X=(X_i)_{i\in N}$ gives pairwise disjoint bundles to the agents. The remaining goods form its pool, $P=M\setminus\bigcup_{i\in N}X_i$. An allocation is complete when its pool is empty. These are the paper's allocation conventions. Chaudhury et al., pp. 3–4.

An allocation is envy-free up to any good (EFX) if, after any single good $g$ is removed from agent $j$'s bundle, agent $i$ values that remainder no more than her own bundle: $v_i(X_j\setminus\{g\})\le v_i(X_i)$ for all $i,j$ and $g\in X_j$. The envy graph has a directed edge $i\to j$ when $i$ values $j$'s bundle more than her own. A source is a vertex with no incoming edge, so nobody envies that agent. Chaudhury et al., pp. 3, 8.

For a set $S$ and a positive number $k$ of parts, $\operatorname{MMS}_i(k,S)$ is the largest worst-part value agent $i$ can secure by partitioning $S$ into $k$ bundles. A complete allocation $Y$ is $\alpha$-GMMS when each agent meets an $\alpha$ fraction of this benchmark for every subgroup containing her:

$$v_i(Y_i)\ge\alpha\operatorname{MMS}_i\!\left(|N'|,\bigcup_{j\in N'}Y_j\right) \qquad(N'\subseteq N,\ i\in N').$$

The benchmark uses only goods allocated to that subgroup. The paper states it both as a complete-allocation property in its introduction and in Definition 15. Chaudhury et al., pp. 5, 15.

Formalization targets

The donated allocation

Assume $X$ is partial and EFX, every agent satisfies $v_i(P)\le v_i(X_i)$, and $s$ is a source of its envy graph. Define $Y_s=X_s\cup P$ and $Y_j=X_j$ for $j\ne s$. The goal states that $Y$ is complete, that donation does not lower any agent's own value, and that

$$v_i(Y_i)\ge\frac47\operatorname{MMS}_i\!\left(|N'|,\bigcup_{j\in N'}Y_j\right) \qquad(N'\subseteq N,\ i\in N').$$

This is the GMMS bullet of Theorem 16 applied to the particular allocation the authors define immediately before it. The paper obtains a suitable $X$ from Lemma 12, which has the relevant properties of Theorem 8. Chaudhury et al., pp. 11–12, 14–16.

Intermediate results

The milestones are Proposition 13, the reduction step in Theorem 16's proof, and all three parts of Lemma 17. Proposition 13 compares maximin shares after deleting agents and at most as many goods. Lemma 17 bounds the value of each bad good, the donated bundle, and the other good bundles. They retain the constants $2$ and $3/2$ used in the paper. Chaudhury et al., pp. 14, 16–17.

Significance

The result turns an almost envy-free partial allocation into a complete allocation with a guarantee for every coalition. A plain maximin-share statement would only compare each agent with a partition of all goods among all agents; here every subgroup and its allocated goods count. The distinction matters even when an ordinary maximin-share bound is easy to meet because there are fewer goods than agents. Chaudhury et al., p. 5.

The paper proves Theorem 16 mathematically. The remaining work for this mission is a machine-checked proof of its stated GMMS consequence and its supporting results. Its definitions of partial allocation, pool, finite maximin share and groupwise guarantee can also serve later formalizations of fair division. The Nash-social-welfare half-guarantee in the printed theorem depends on the starting allocation from Lemma 12; this mission records only the value preservation under donation. Chaudhury et al., pp. 14, 16.

Difficulty

Giving all leftover goods to one agent makes the allocation complete, but it can change how another agent values that enlarged bundle and how a subgroup's benchmark is calculated. EFX alone compares bundles after deleting one good; GMMS compares an agent with every repartition of a subgroup's goods. The difficulty is to control those repartitions while keeping the exact $4/7$ constant. Merely applying an ordinary maximin-share bound to the grand coalition does not establish the required subgroup inequalities. Chaudhury et al., pp. 15–17.

Formalization scope

Agents and goods are represented by Fin n and Fin m; Lean numbers agents from zero, and the paper's “agent 1” is an explicit source $s$. Bundles are finite sets. Valuations are real-valued but include nonnegativity alongside additivity, representing the paper's codomain $\mathbb R_{\ge0}$. The pool is computed from $X$, and the donated allocation is a function of $X$ and $s$. No independent pool or arbitrary completed allocation is allowed. Completeness is a conclusion. The maximin share is a finite maximum of finite minima over labelled partitions, which may have empty parts. Every use has a positive part count; in the GMMS definition this follows from $i\in N'$. Cardinality is converted to real numbers before fractions are formed. These choices exclude zero-part maximin shares and integer division. Chaudhury et al., pp. 3–5, 15–16.

The theorem is conditional on the EFX and pool-value properties of the source allocation, rather than repeating its existence proof. It states the conclusion for every such allocation and every source. The paper's half-optimal-Nash-social-welfare bullet is outside this mission because it invokes the separate black-box starting allocation of Lemma 12. Contributions toward finite-partition comparisons, EFX value bounds, and the groupwise estimate are welcome. Chaudhury et al., pp. 14–17.

Selected references

• B. R. Chaudhury, T. Kavitha, K. Mehlhorn and A. Sgouritsa, A Little Charity Guarantees Almost Envy-Freeness, SIAM Journal on Computing, 2021. Formalization source: arXiv:1907.04596v3.

Fair division of indivisible goods

A set of $n$ agents must share a set $M$ of $m$ indivisible goods, each agent valuing bundles of goods by her own valuation. Two fairness notions dominate the literature. Envy-freeness up to any good (EFX), introduced by Caragiannis, Kurokawa, Moulin, Procaccia, Shah and Wang (EC 2016), asks that no agent prefer another's bundle once any single good is removed from it. The maximin share (MMS), proposed by Budish (JPE 2011), asks that every agent receive at least what she could secure by splitting the goods into $n$ bundles herself and taking the worst one.

Neither notion is known to be achievable in full. Whether complete EFX allocations always exist is open in general. Complete MMS allocations need not exist: Procaccia and Wang (EC 2014) gave a counterexample with three agents, and the best known approximation factors for additive valuations are $3/4-\varepsilon$ (Ghodsi et al., EC 2018) and $3/4$ (Garg and Taki, arXiv:1903.00029). Amanatidis, Birmpas and Markakis (IJCAI 2018) showed that every complete EFX allocation is a $4/7$-MMS allocation.

Caragiannis, Gravin and Huang (EC 2019) showed that EFX can be achieved if some goods are left unallocated, with no bound on how many. Chaudhury, Kavitha, Mehlhorn and Sgouritsa (arXiv:1907.04596, SODA 2020, SIAM J. Comput. 2021) relax completeness instead: some goods may be "donated to charity". Their Theorem 8 produces an EFX partial allocation in which nobody envies the donated set and the donated set has fewer goods than there are unenvied agents. This mission formalizes their Theorem 14: such an allocation also gives every agent a maximin-share guarantee that improves as more goods are donated.

Setting

Agents are $N=[n]$ and goods are $M$, $|M|=m$. Agent $i$ has a valuation $v_i:2^M\to\mathbb{R}_{\ge 0}$, assumed additive: $v_i(S)=\sum_{g\in S}v_i(\{g\})$ for every $S\subseteq M$.

A (partial) allocation $X=\langle X_1,\dots,X_n\rangle$ gives agent $i$ the bundle $X_i\subseteq M$, the bundles being pairwise disjoint. The pool of unallocated goods is $P=M\setminus\bigcup_i X_i$, and $k=|P|$.

• $X$ is EFX if $v_i(X_i)\ge v_i(X_j\setminus\{g\})$ for all agents $i,j$ and every $g\in X_j$.
• The envy graph $G_X$ has the agents as vertices and an edge $i\to j$ exactly when $v_i(X_i)<v_i(X_j)$. A source is a vertex of indegree zero: an agent nobody envies.
• The maximin share of agent $i$ over $k'\ge1$ bundles of a set $S$ of goods is

$$\mathrm{MMS}_i(k',S)=\max_{(S_1,\dots,S_{k'})}\ \min_{1\le j\le k'} v_i(S_j),$$

the maximum over partitions of $S$ into $k'$ possibly empty bundles. Agent $i$'s maximin share in the instance is $\mathrm{MMS}_i(n,M)$.

The three conditions of Theorem 8 on $(X,P)$ are:

1. $X$ is EFX;
2. $v_i(X_i)\ge v_i(P)$ for every agent $i$;
3. $|P|$ is less than the number of sources of $G_X$; in particular $|P|<n$.

Formalization targets

Goal: Theorem 14 (MMS bullet)

For every allocation $X$ with pool $P$ satisfying conditions 1–3, and every agent $i$,

$$v_i(X_i)\ \ge\ \frac{\mathrm{MMS}_i(n,M)}{2-\frac{k}{n}},\qquad k=|P|.$$

The factor ranges from $\tfrac12$ when $P=\emptyset$ to $(1+\tfrac1n)^{-1}$ when $|P|=n-1$.

Milestones

1. Proposition 13 (quoted by the paper from Garg, McGlaughlin and Taki, SOSA 2019): for $N'\subseteq N$ and $M'\subseteq M$ with $|N\setminus N'|\ge|M\setminus M'|$ and $i\in N'$,

$$\mathrm{MMS}_i(|N'|,M')\ \ge\ \mathrm{MMS}_i(|N|,M).$$

2. MMS is at most the proportional share: $\mathrm{MMS}_i(k',S)\le v_i(S)/k'$ for additive valuations and $k'\ge1$.
3. The EFX half-bound: if $X$ is EFX and $|X_j|\ge2$, then $v_i(X_i)\ge(1-1/|X_j|)\,v_i(X_j)\ge\tfrac12 v_i(X_j)$.
4. The counting step (summing inequalities (1)–(3) of the proof): with $N'$ the sources of $G_X$, agent $i$ and all agents holding at least two goods, $n'=|N'|$ and $M'=\bigcup_{j\in N'}X_j$,

$$(2n'-k)\,v_i(X_i)\ \ge\ v_i(M'\cup P).$$

Significance

Theorem 14 shows that leaving goods unallocated is not merely a cost: under conditions 1–3, each donated good buys a quantitative improvement of every agent's maximin-share guarantee, interpolating between the factor $\tfrac12$ the bound gives when the pool is empty and a factor tending to $1$ when nearly $n$ goods are donated. Together with Theorem 8 it shows that a single allocation can be simultaneously EFX, envy-free towards the charity, small in its charity, and approximately MMS. The same reduction (Proposition 13 applied to a carefully chosen sub-instance) is the template for the paper's $4/7$-groupwise-maximin-share result, Theorem 16, formalized in mission III of this series.

The result is proved in the paper; no machine-checked proof of it, of Proposition 13, or of the existence of EFX allocations with bounded charity is known to exist. The mission produces a formal maximin-share definition on arbitrary subsets of goods with an arbitrary number of bundles, a formal proof of the monotonicity of the maximin share under removal of agents and goods (Proposition 13, which the paper quotes without proof), and the guarantee itself. Combined with mission I of this series (Theorem 8), it yields the printed existence statement.

Difficulty

The guarantee compares an agent's own bundle with a benchmark defined over all partitions of all goods, while EFX and the source condition speak only about the allocation at hand. The obvious attempt, summing $v_i(X_i)\ge\tfrac12 v_i(X_j)$ over all agents and adding the pool, gives only a factor near $\tfrac12$ and ignores the pool's size. Agents holding a single good are the obstruction: EFX gives no bound on the value of their bundles relative to $v_i(X_i)$, and the benchmark $\mathrm{MMS}_i(n,M)$ is defined on the full instance, which contains them. Proposition 13, the comparison of maximin shares across instances, is a combinatorial statement about all partitions of the original instance and requires nonnegativity of the valuations: with a good of negative value it fails.

Formalization scope

Agents are Fin n (0-based) and goods Fin m; the set $M$ is the whole of Fin m. Valuations are functions Fin n → Finset (Fin m) → ℝ; additivity is the sum formula together with nonnegativity, which is the paper's codomain $\mathbb{R}_{\ge0}$. An allocation is a family of pairwise disjoint finsets and the pool is always computed as the complement of their union, never taken as a free parameter. Sources are agents of indegree zero in the envy graph (nobody envies them), not agents who envy nobody. The maximin share $\mathrm{MMS}(k',S)$ is a supremum over labellings Fin m → Fin k' restricted to $S$ of the minimum bundle value; it is used only with $k'\ge1$, which every statement has in its hypotheses or derives from them (in the goal, condition 3 forces $n\ge1$). Every cardinality is cast to $\mathbb{R}$ before division or subtraction, and $2-k/n>1$ under condition 3, so no division by zero occurs.

The goal is posed as an implication for every allocation satisfying conditions 1–3, rather than as the paper's "there exists an allocation"; the paper's proof of the MMS bullet uses only those three conditions, and existence is Theorem 8. The Nash-social-welfare bullet of Theorem 14 is not posed: it depends on Lemma 12, which takes the allocation of an earlier paper as a black box. The goal cannot be trivialized by a free pool, by overlapping bundles, by zero agents (condition 3 excludes them), by a junk maximin share over zero bundles, or by natural-number division; the statement keeps all three conditions, each of which is needed.

Contributions welcome: a library-quality maximin-share API for additive valuations (attainment of the maximum, monotonicity, the proportional bound), which is reusable for other MMS results; proofs of the milestones; and the final assembly.

Selected references

• B. R. Chaudhury, T. Kavitha, K. Mehlhorn, A. Sgouritsa, A Little Charity Guarantees Almost Envy-Freeness, SIAM J. Comput. 50(4), 2021; cited from arXiv:1907.04596v3. https://arxiv.org/abs/1907.04596
• E. Budish, The Combinatorial Assignment Problem: Approximate Competitive Equilibrium from Equal Incomes, J. Political Economy 119(6), 2011. https://doi.org/10.1086/664613
• I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah, J. Wang, The Unreasonable Fairness of Maximum Nash Welfare, EC 2016. https://doi.org/10.1145/2940716.2940726
• A. D. Procaccia, J. Wang, Fair Enough: Guaranteeing Approximate Maximin Shares, EC 2014. https://doi.org/10.1145/2600057.2602835
• M. Ghodsi, M. HajiAghayi, M. Seddighin, S. Seddighin, H. Yami, Fair Allocation of Indivisible Goods: Improvements and Generalizations, EC 2018. https://doi.org/10.1145/3219166.3219238
• J. Garg, S. Taki, An Improved Approximation Algorithm for Maximin Shares, CoRR abs/1903.00029, 2019. https://arxiv.org/abs/1903.00029
• J. Garg, P. McGlaughlin, S. Taki, Approximating Maximin Share Allocations, SOSA 2019. https://doi.org/10.4230/OASIcs.SOSA.2019.20
• I. Caragiannis, N. Gravin, X. Huang, Envy-Freeness up to Any Item with High Nash Welfare: The Virtue of Donating Items, EC 2019. https://doi.org/10.1145/3328526.3329574
• G. Amanatidis, G. Birmpas, E. Markakis, Comparing Approximate Relaxations of Envy-Freeness, IJCAI 2018. https://doi.org/10.24963/ijcai.2018/7

Why a cloudlet price matters

Mobile devices can divide work between local execution, a nearby shared cloudlet, and a remote cloud. A cloudlet has limited capacity, so one user's choice changes the delay faced by the others. Cardellini and coauthors model this as a generalized Nash equilibrium problem, in which each user's feasible choices depend on the aggregate cloudlet load. The shared utilization cap makes a direct distributed solution awkward: a user must know how much capacity all other users consume before choosing a feasible deviation. The paper therefore introduces an additional player who sets a cloudlet price. This mission formalizes the relationship between the original coupled game and that extended, ordinary Nash game Cardellini et al., accepted manuscript, pp. 10–16.

The offloading game

There are $N$ users and $n$ cloudlet servers. User $u$ chooses fractions $x_{u,m}$, $x_{u,\mathrm{clet}}$, and $x_{u,\mathrm{cloud}}$ for local, cloudlet, and remote-cloud execution. These fractions are nonnegative and sum to one. At most a fraction $\chi$ can be offloaded, and a user-specific linear power constraint applies. The set $\widetilde K_u$ contains these private feasible choices. The cloudlet load and the shared feasible set are

$$L(x)=\frac1n\sum_{u=1}^{N}\delta_u x_{u,\mathrm{clet}},\qquad \Omega=\{x:L(x)\le U_{\max}\},\qquad K=\left(\prod_{u=1}^{N}\widetilde K_u\right)\cap\Omega.$$

Each user's cost $\lambda_u R_u$ is the response-time expression on p. 10, with coefficients $\alpha_u,\beta_u,\gamma_u,\delta_u$. The VI map $F$ is the stack of the user's partial gradients, written in closed form on p. 11. A variational solution $\bar x$ belongs to $K$ and satisfies $\langle F(\bar x),x-\bar x\rangle\ge0$ for every $x\in K$. The pairing sums all three coordinates for each user. Section 5 assumes $0<U_{\max}<1$ and $0<\alpha_u,\delta_u<1$ for every user; the model also has $n>0$ and $0<\chi\le1$ Cardellini et al., pp. 7, 9–11.

The extended game replaces the joint cap in each user's feasible set by a price. User $u$ minimizes $\lambda_uR_u(x)+\rho(\delta_u/n)x_{u,\mathrm{clet}}$ over $\widetilde K_u$. A cloudlet manager chooses $\rho\ge0$ to maximize $\rho(L(x)-U_{\max})$. The manager's choice is part of the Nash equilibrium condition, not a preimposed complementary-slackness equation. The extended game's VI set is $K_e=(\prod_u\widetilde K_u)\times\mathbb R_+$ and its map is $F_e(x,\rho)=(F(x)+\operatorname{price}(\rho),U_{\max}-L(x))$ Cardellini et al., p. 15.

Formalization targets

The goal is the two-part assertion of Theorem 2. Under the standing assumptions and a strict load bound on the full product of private feasible sets, its equilibrium characterization is

$$\bar x\in\operatorname{SOL}(K,F) \quad\Longleftrightarrow\quad \exists\bar\rho,\; (\bar x,\bar\rho)\in\operatorname{NE}_{\mathrm{ext}}.$$

The same goal states that monotonicity of $F$ on $\prod_u\widetilde K_u$ implies monotonicity of $F_e$ on $K_e$. The three milestones follow the paper's path: the extended Nash game is equivalent to its VI; the shared affine constraint has a scalar multiplier at a VI solution; and the price-load coupling cancels in the monotonicity pairing. The source states the first as a classical result and gives the last two in its proof Cardellini et al., pp. 15–16.

What the result provides

The characterization lets a variational solution of a game with coupled feasible sets be found as an equilibrium of a game whose $N$ users have separate feasible sets. The additional scalar has a concrete interpretation: it is the multiplier of the shared cloudlet-utilization cap. The monotonicity assertion connects the paper's analysis of the original VI to methods for the extended one. The paper uses this relationship as the entry point for its distributed algorithms in the next section Cardellini et al., pp. 16–17.

The result is proved in the paper but is not yet machine checked in this mission. A complete development would give reusable Lean interfaces for a finite-dimensional VI on an intersection of a product polytope and one affine half-space, a multiplier characterization for that intersection, and an equilibrium-to-VI conversion for separable player constraints. Those components could support other capacity-sharing games. The theorem drafts remain proof obligations; the definitions compile locally.

Where the proof is delicate

A Nash equilibrium requires each user to be optimal against every privately feasible deviation, including deviations that violate the original shared cap. Consequently, the user's cloudlet cost must remain well defined throughout $\widetilde K_u$ for the equivalence to hold. A load bound only on $K$ does not cover those deviations. The multiplier comparison must also account for the manager's maximization condition and the sign of the load term in $F_e$. For monotonicity, $F_e$ evaluates $F$ on the whole product $\prod_u\widetilde K_u$, a larger domain than $K$. These domain distinctions explain why the statement needs two explicit repairs to the printed theorem Cardellini et al., pp. 15–16.

Formalization scope

Lean represents the users as Fin N and the three processing locations as a finite tier type. Indices therefore start at zero. The costs, the map $F$, the private sets, $\Omega$, and $K$ are separate definitions. The Euclidean pairing is written as a finite sum; no Pi-type sup norm is used. The extended Nash predicate quantifies over user deviations in $\widetilde K_u$ and over every nonnegative manager price. The VI predicates are in their own module so the game is not built into their meaning. The theorem's statement remains meaningful at $N=0$; no positive-user hypothesis is added to Section 5's assumptions.

The first repair requires $L(x)<1$ at every $x\in\prod_u\widetilde K_u$. The paper's Theorem 1 condition (18) implies this bound, but is stronger than needed. Without the bound, a private deviation can cross the pole of $\delta_u x_{u,\mathrm{clet}}/(1-L(x))$; Lean's total division then assigns a value at a zero denominator even though the paper's cost has none. In a two-user instance with $n=1$, $\delta_u=0.9$ and $U_{\max}=0.5$, the pole can lie within one user's private feasible interval. The second repair reads “the original game is monotone” on $\prod_u\widetilde K_u$, because that is precisely the $x$-domain of $K_e$. Monotonicity on $K$ alone is insufficient. Both repairs are disclosed in the item notes, and the source wording remains visible in the milestone quotations.

An empty $K$ would make a solution statement vacuous; the formal development should retain concrete feasible parameter instances. The map $F$ is the paper's displayed formula, rather than a derivative chosen to make a milestone tautological. The VI uses all user coordinates, and the extended game does not silently reinstate the shared constraint in user deviations. Contributions toward the stated multiplier theorem, Nash-to-VI equivalence, and the cancellation identity are welcome, along with reusable finite-dimensional convex-analysis lemmas.

Selected references

• V. Cardellini, V. De Nitto Personé, V. Di Valerio, F. Facchinei, V. Grassi, F. Lo Presti, and V. Piccialli, A game-theoretic approach to computation offloading in mobile cloud computing, accepted manuscript for Mathematical Programming, 2015, DOI 10.1007/s10107-015-0881-6.

Motivation

Allocating indivisible goods fairly is difficult because a single good can change how an agent compares two bundles. Exact envy-freeness can be impossible (one good, two agents), so the field works with relaxations. Envy-freeness up to any good (EFX) requires each agent to prefer her own bundle to every other agent's bundle after any one good of that other bundle is removed. Whether EFX allocations of all goods always exist is open; the question motivates weakening the requirement that every good be assigned, and asking how little must be left over. Chaudhury, Kavitha, Mehlhorn and Sgouritsa show that leaving a small, unenvied set of goods unallocated (donated to "charity") suffices for every normalized monotone valuation profile (arXiv:1907.04596v3, Theorem 8, pp. 11–12).

Timeline (as recounted on pp. 2–3 of the source):

• 2004: Lipton, Markakis, Mossel and Saberi introduce the envy-graph and cycle-elimination technique and compute allocations now called EF1 (DOI 10.1145/988772.988792).
• 2016: Caragiannis, Kurokawa, Moulin, Procaccia, Shah and Wang define EFX (DOI 10.1145/2940716.2940726).
• 2018: Plaut and Roughgarden prove EFX allocations of all goods exist for two agents, or for any number of agents with identical valuations (arXiv:1707.04769).
• 2019: Caragiannis, Gravin and Huang introduce EFX with charity: a partial EFX allocation in which each agent gets at least half her value in a Nash-optimal allocation, with no bound on the number or value of donated goods (arXiv:1902.04319).
• 2020: Chaudhury, Garg and Mehlhorn prove existence of complete EFX allocations for three agents with additive valuations (arXiv:2002.05119).
• 2020/2021: the present paper bounds the charity: fewer goods than unenvied agents, and no agent envies the donated set. Its SODA 2020 version assumed gross-substitute valuations; the journal version (arXiv v3) needs only normalized monotone valuations (p. 8, §1.4).

The two bounds matter separately. The empty allocation is EFX and donates everything; a cardinality bound alone still lets the donated goods carry most of an agent's value; the value bound alone allows almost all goods to be donated. The paper's later maximin-share and groupwise-maximin-share guarantees (Theorems 14 and 16, treated in the next missions of this series) are derived from exactly the allocation produced here.

Setting

There are $n\ge1$ agents, indexed by $N=\{1,\ldots,n\}$ in the paper, and a finite set $M$ of $m$ indivisible goods. Agent $i$ has a valuation $v_i:2^M\to\mathbb R_{\ge0}$. It is normalized if $v_i(\varnothing)=0$ and monotone if $S\subseteq T$ implies $v_i(S)\le v_i(T)$. No additivity, submodularity or substitutes condition is assumed. These are the general valuations of §1.1.1, p. 3, and §2 of the source.

A partial allocation $X=(X_i)_{i\in N}$ consists of pairwise disjoint bundles $X_i\subseteq M$. Its pool is the goods not assigned to anyone,

$$P(X)=M\setminus\bigcup_{i\in N}X_i.$$

The allocation is EFX when

$$v_i(X_j\setminus\{g\})\le v_i(X_i) \qquad\text{for all }i,j\in N\text{ and every }g\in X_j.$$

The paper calls allocations partial by default (p. 3, footnote 5). The envy graph $G_X$ has the agents as vertices and an edge $i\to j$ when $v_i(X_i)<v_i(X_j)$. A source is a vertex with no incoming edge. Its reachability component $C(s)$ includes $s$ itself. The social welfare of $X$ is $\phi(X)=\sum_i v_i(X_i)$. These notions are introduced on pp. 8–9 of the source.

For a set $S$ of goods, an envied set is one some agent values more than her own bundle. An inclusion-wise minimal envied subset $Z$ is envied, but no strict subset of $Z$ is envied by anyone. An agent who envies such a $Z$ is a most envious agent of $S$; the paper allows ties. The three update rules U0, U1 and U2 use these sets to change an allocation while maintaining EFX (Definition 3 and Algorithm 2, p. 9).

Formalization targets

The goal is the allocation guarantee of Theorem 8:

$$\exists X\text{ partial}:\quad X\text{ is EFX},\qquad v_i(P(X))\le v_i(X_i)\ (i\in N),\qquad |P(X)|<|\operatorname{sources}(G_X)|\le n.$$

Both the stronger source-count bound and its consequence $|P(X)|<n$ are stated. The theorem asserts existence for every normalized, monotone valuation profile, including nonadditive profiles. It does not require the returned envy graph to be acyclic; acyclicity is an invariant used during construction, rather than an additional advertised property of the final allocation.

The attack path consists of the paper's numbered Lemmas 2, 4, 5, 6 and 7. Lemma 2 concerns removal of envy cycles; its Lean form keeps the page's conditional "if $X$ is EFX then $X'$ is EFX" and the unconditional strict welfare increase. Lemma 4 records what U0 does and what its failure implies. Lemma 5 records U1's welfare and EFX guarantees. Lemma 6 supplies the finite source, good and agent data required for U2. Lemma 7 states U2's welfare and EFX guarantees. Their source wording and page locations appear in the milestone list; the Lean statements include the exact allocation updates where those lemmas rely on them.

Significance

The theorem guarantees a partial EFX allocation even for general monotone valuations, while limiting the unallocated pool more tightly than the number of agents: its size is below the number of unenvied agents. Every agent also values that entire pool no more than her own bundle. These two bounds distinguish the allocation from a merely EFX partial allocation. They provide the starting point for the paper's later statements on approximate maximin shares under additive valuations (Theorems 14 and 16).

The mathematical result is proved in the paper. The mission asks for a machine-checked proof of its allocation guarantee and of the supporting lemmas, with a reusable Lean account of finite partial allocations, the unallocated pool, envy graphs, minimal envied subsets and the update rules. Such definitions are useful for other fair-division questions involving unallocated indivisible goods.

Difficulty

EFX must hold after the allocation is changed, for every agent pair and for removal of every good from the other agent's new bundle. Simply giving a pool good to an agent may violate that condition, even though it makes the pool smaller. Conversely, replacing a bundle with an envied subset can improve welfare while returning goods to the pool. The source-count bound depends on controlling both kinds of progress. Rule U2 adds a further complication: its bundle moves follow envy paths, so an overlap between selected paths would make the new allocation ambiguous. These are the points at which the straightforward approach of distributing the remaining goods one at a time stops working.

Formalization scope

Lean represents agents by Fin n, goods by Fin m, bundles by finite sets of goods, and valuations by real-valued functions on bundles. The paper's one-based subscripts become zero-based Lean indices. Nonnegative values need no separate hypothesis: normalization and monotonicity imply them. The hypothesis $n>0$ is explicit because the paper presumes agents and the strict bound $|P|<n$ is false when $n=0$. The pool is computed as the complement of the union of pairwise disjoint assigned bundles. It is never a free set. EFX ranges over every pair $i,j$, including $i=j$, and every good of $X_j$.

The minimal-envied-subset definition checks every strict subset against every agent. The most envious agent is a relation, allowing the paper's arbitrary tie choice. Reachability includes a path of length zero. U2's new allocation is calculated from its paths and chosen subsets. Lemma 6 includes Algorithm 1's acyclic-graph invariant and the ordering property established in its proof. It replaces the printed threshold $|P|\ge n$ with $|P|\ge|\operatorname{sources}(G_X)|$, the exact number of fresh goods its construction needs and the threshold used by the goal. Lemma 7 takes that ordering property to make path assignments unambiguous.

The printed U2 pool expression in Algorithm 2, line 13, is malformed; the formal statement uses the pool of the constructed allocation and the corrected union of leftover goods. Theorem 8's final sentence also asserts an $nmV/\Delta$ iteration bound. This mission poses the allocation conclusions, while a future run-level formalization would be needed to state and check the iteration count. The paper's preceding count of U1/U2 steps and successive U0 steps does not by itself imply the printed number. Definitions and the numbered lemma statements are welcome contributions; a purported proof that uses a free empty pool, overlapping bundles, zero agents or an arbitrary replacement allocation would not establish this target.

Selected references

• B. R. Chaudhury, T. Kavitha, K. Mehlhorn and A. Sgouritsa, A Little Charity Guarantees Almost Envy-Freeness, arXiv:1907.04596v3, 2020; published in SIAM Journal on Computing, 2021. Pinned preprint.
• R. J. Lipton, E. Markakis, E. Mossel and A. Saberi, On approximately fair allocations of indivisible goods, ACM EC 2004. https://doi.org/10.1145/988772.988792
• I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah and J. Wang, The unreasonable fairness of maximum Nash welfare, ACM EC 2016. https://doi.org/10.1145/2940716.2940726
• B. Plaut and T. Roughgarden, Almost envy-freeness with general valuations, SODA 2018. https://arxiv.org/abs/1707.04769
• I. Caragiannis, N. Gravin and X. Huang, Envy-freeness up to any item with high Nash welfare: the virtue of donating items, ACM EC 2019. https://arxiv.org/abs/1902.04319
• B. R. Chaudhury, J. Garg and K. Mehlhorn, EFX exists for three agents, ACM EC 2020. https://arxiv.org/abs/2002.05119

Motivation

In a congestion game, several users choose facilities and each facility becomes more costly as more users choose it. Such games model settings in which each participant chooses a route or collection of resources for personal use while the resulting load is shared. A pure Nash equilibrium is a stable choice of routes: no single participant can lower their own cost by switching. Stability alone gives no assurance that the resulting allocation serves the group well. The price of anarchy compares the social cost of an equilibrium with the best social cost attainable by coordinated choices.

Christodoulou and Koutsoupias studied finite congestion games with linear latency functions and several notions of social cost. For the maximum cost borne by any player, their STOC 2005 paper gives both an upper bound valid for all such games and a family of instances showing that its square-root dependence on the number of players has the right order. This mission formalizes those two claims together. The maximum criterion matters when a single heavily delayed user is significant even if the total cost of the population is moderate.

Setting

Let $N\ge1$ be the number of players and let $E$ be a finite set of facilities. Player $i$ has a finite collection $\Sigma_i$ of available pure strategies, each a subset of $E$. A profile $A$ chooses one strategy $A_i\in\Sigma_i$ for every player. For a facility $e$, its load $n_e(A)$ is the number of players whose chosen strategy contains $e$. The latency of $e$ at load $n$ is $f_e(n)$. Player $i$ pays the sum of the latencies on the facilities they chose:

$$c_i(A)=\sum_{e\in A_i}f_e(n_e(A)).$$

A profile is a pure Nash equilibrium if no player can decrease this cost by replacing their own strategy while the others keep theirs. The paper calls latencies linear when $f_e(n)=a_en+b_e$ with $a_e,b_e\ge0$; these are affine functions in standard terminology. The paper displays many calculations for the special case $f_e(n)=n$ and states the general nonnegative affine convention in its model section. The maximum social cost is $\operatorname{MAX}(A)=\max_i c_i(A)$; the total cost is $\operatorname{SUM}(A)=\sum_i c_i(A)$. The paper's average social cost is $\operatorname{SUM}(A)/N$.

For a game with at least one pure Nash equilibrium and a positive optimal maximum cost, the maximum-cost pure price of anarchy is the largest equilibrium value of $\operatorname{MAX}$ divided by the smallest feasible value. The Lean targets use inequalities against every feasible comparison profile $P$ rather than dividing by an optimum. This form continues to say something when an optimum has cost zero, and finite strategy sets ensure an optimum exists whenever the profile space is nonempty.

Formalization targets

Universal upper bound

For every $N\ge1$, every finite game with nonnegative affine latencies, every pure Nash equilibrium $A$, and every feasible profile $P$, Theorem 5's proof yields

$$\operatorname{MAX}(A)\le \left(1+\sqrt{\frac{5N}{2}}\right)\operatorname{MAX}(P).$$

This states a numerical version of the paper's $O(\sqrt N)$ theorem without an unspecified constant. Taking $P$ to minimize $\operatorname{MAX}$ gives the corresponding price-of-anarchy bound. The bound is about asymmetric games: players may have different strategy sets, and no symmetry assumption is present.

Lower-bound family

For every integer $k\ge2$, let $N=k(k-1)+1$. Theorem 6 provides an identity-latency congestion game with $N$ players and $kN$ facilities, a pure Nash profile $A$, and an optimal profile $P$ for which

$$\operatorname{MAX}(A)=k^2,\qquad \operatorname{MAX}(P)=k.$$

Every feasible profile in the instance has maximum cost at least $k$. Thus the ratio is $k$, and $k\ge\sqrt N$. The proof's explicit instance has positive comparison cost, so the lower bound cannot be satisfied by a zero-cost game. The source also says such behavior occurs in network congestion games and sketches a network realization in Figure 2; this mission's formal lower target is the finite congestion-game construction.

Significance

Together these results identify the order of growth of the worst pure equilibrium maximum cost relative to an optimum: it can grow with the population, yet for linear latencies it grows no faster than a constant times $\sqrt N$. The upper statement applies to any feasible comparison profile, so it can also be used when a convenient benchmark is known without solving the entire optimization problem. The lower family prevents replacing the square-root dependence by a bound independent of $N$ for this class of games.

The results are proved in the 2005 paper; the mission is to give them machine-checked Lean proofs in a common finite-game representation. The development also supplies reusable definitions of congestion games, loads, pure cost equilibria, and maximum social cost, together with the total-cost estimate of Theorem 1 and the intermediate bounds appearing in Theorem 5. The current draft contains statements with sorry placeholders, not completed proofs.

Difficulty

A bound on total player cost does not directly control the cost of the most expensive player sharply enough. An individual player can use several facilities whose loads interact, and bounding each load separately loses the dependence required for the square-root result. Affine coefficients add another issue: the proof printed for identity latencies writes a cardinality where the general statement needs a coefficient-weighted quantity. The lower example has an indexing discrepancy in the printed alternative strategies, so the intended Nash profile must be checked against the costs on every permitted deviation.

Formalization scope

Players are represented by Fin N; facilities by an arbitrary finite type in upper bounds and by a type with $kN$ elements in the lower family. A profile is a function from players to finite facility sets, with feasibility stated separately. Latencies are real-valued on natural-number loads. The IsLinear predicate requires explicit nonnegative affine coefficients. Pure Nash uses a cost inequality; it is the negative-payoff version of a standard finite game's payoff equilibrium. MAX requires at least one player, and all upper-bound targets therefore require $N\ge1$. The lower family begins at $k=2$, where $N=k(k-1)+1$ is positive.

The source's number $k^2-k+1$ is written as $k(k-1)+1$ in Lean to keep natural-number subtraction inside its valid range. The two expressions agree for $k\ge2$. In the source's one-based indexing, the proposed alternative strategy uses a ceiling index. The printed denominator $k$ makes some alternative facilities carry $k+1$ users and breaks the Nash assertion; denominator $k-1$ agrees with Figure 2's $k-1$ short-route users per layer and gives the stated costs. This correction is recorded with the lower theorem. No normalization of coefficients or artificially restricted strategy class is assumed. Contributions to the finite-game definitions, Theorem 1, the player-cost bounds, and the explicit lower instance are all in scope.

Selected references

• G. Christodoulou and E. Koutsoupias, The Price of Anarchy of Finite Congestion Games, Proceedings of the 37th Annual ACM Symposium on Theory of Computing, 2005. DOI: 10.1145/1060590.1060600.

Motivation

Mean field games describe the limit of symmetric stochastic differential games with $n$ players as $n\to\infty$. A basic question of the theory is which mean field equilibria are limits of Nash equilibria of the $n$-player games. For closed-loop equilibria, in which each player's control may depend on the states of all players, this question was open in general until D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745, Ann. Appl. Probab. 2020). That paper shows that limits of closed-loop $\varepsilon_n$-Nash equilibria are weak mean field equilibria, a class that can be strictly larger than the classical (strong) one.

Section 7.3 of the paper gives an explicit game in which the difference is visible. It has exactly three strong equilibria (Lacker, Probab. Theory Related Fields 165, 2016, Proposition 3.6, cited as [43] in the paper) and infinitely many weak ones. The weak equilibria form a family indexed by a switching time $t_0\in[0,T]$, and for $t_0\in(0,T)$ they are not mixtures of strong equilibria (Remark 7.1). Proposition 7.2, the subject of this mission, treats $t_0=0$: the natural symmetric feedback is an $n$-player approximate Nash equilibrium, and its population mean selects the equal mixture of the two strong equilibria $m^{\pm1}$ rather than the third one, $m^0$. The selection mechanism is regularization by noise: the mean of the population solves an ill-posed ODE, and the small noise of the $n$-player system picks out a particular random solution (Trevisan, Electron. Commun. Probab. 18, 2013, cited as [57] in the paper).

Setting

Fix a horizon $T>0$. In the mean-sign game each of $n$ players controls a real state

$$X^i_t = \int_0^t \alpha^i_s\,ds + W^i_t,\qquad X^i_0=0,$$

with controls $\alpha^i_s\in A=[-1,1]$ and independent standard Brownian motions $W^1,\dots,W^n$. The mean process is $\overline\mu^n_t=\frac1n\sum_{k=1}^n X^k_t$, the mean of the empirical measure $\mu^n_t=\frac1n\sum_k\delta_{X^k_t}$. Player $i$ maximizes the expected terminal reward

$$J^n_i=\mathbb E\big[X^i_T\,\overline\mu^n_T\big],$$

that is, $b(t,x,m,a)=a$, $f\equiv0$, $g(x,m)=x\,\overline m$ with $\overline m=\int y\,m(dy)$, and initial law $\lambda=\delta_0$.

A Markovian control of player $i$ is a Borel function $\beta:[0,T]\times\mathbb R^n\to[-1,1]$ of time and the current states of all players. A profile $(\alpha^1,\dots,\alpha^n)$ is a Markovian $\varepsilon$-Nash equilibrium if no player can raise their payoff by more than $\varepsilon$ by switching to another Markovian control while the others keep theirs (Definition 2.1).

With $\operatorname{sgn}(x)=1,-1,0$ for $x>0$, $x<0$, $x=0$, the sign feedback (7.13) with $t_0=0$ is

$$\alpha^{n,i}_0(t,x_1,\dots,x_n)=\operatorname{sgn}\Big(\frac1n\sum_{k=1}^n x_k\Big)\mathbf 1_{(0,T]}(t),$$

the same for every player. Finally $H^\pm_0(t)=\pm t$ on $[0,T]$ (7.11).

Formalization targets

Goal: Proposition 7.2

For the profile $\alpha^n=(\alpha^{n,1}_0,\dots,\alpha^{n,n}_0)$:

$$\exists\,\varepsilon_n\ge0,\ \varepsilon_n\to0:\quad \alpha^n\ \text{is a Markovian }\varepsilon_n\text{-Nash equilibrium for each }n,$$ $$\mathcal L\big((\overline\mu^n_t[\alpha^n])_{t\in[0,T]}\big)\ \Longrightarrow\ \tfrac12\delta_{H^+_0}+\tfrac12\delta_{H^-_0}\quad\text{on }C([0,T];\mathbb R).$$

The goal also asserts that the $n$-player system under $\alpha^n$ has a solution, so that the equilibrium property cannot hold vacuously.

Milestones

1. The equilibrium payoff: $J^n_1(\alpha^n)=\mathbb E[|\overline\mu^n_T|^2]\to T^2$ (proof of Proposition 7.2, p. 49).
2. Lemma 7.4, the part about the mean $Y^n$ and player 1's noise $W^1$ when player 1 deviates to a $\frac1n$-optimal control (7.15): the laws of $(Y^n,W^1)$ are tight, and every limit $(Y,W)$ has $\mathcal L(Y)=\tfrac12\delta_{H^+_0}+\tfrac12\delta_{H^-_0}$, solves $Y_t=\int_0^t\operatorname{sgn}(Y_s)\,ds$, and has $Y$ independent of $W$.
3. The upper bound (7.14): $\limsup_n\sup_{\beta}J^n_1(\beta,\alpha^{n,2}_0,\dots,\alpha^{n,n}_0)\le T^2$.

Significance

Proposition 7.2 is a concrete instance of the paper's main theme. Theorem 2.7 says that limits of closed-loop equilibria are weak equilibria; this example exhibits explicit, symmetric, Markovian approximate equilibria whose limit is a genuinely random equilibrium (the sign of the mean is a fair coin), selected by noise among infinitely many candidates, and it identifies the limiting law of the population mean exactly. The paper states that the analogous claim for $t_0\in(0,T)$, where the limit would be a weak equilibrium that is not a mixture of strong ones, is not resolved; a formal treatment of the $t_0=0$ case makes the structure of that question precise.

Nothing of this proposition is machine-checked. Formalizing it requires weak solutions of SDEs with discontinuous drift, Nash equilibria over Markovian feedback controls, and weak convergence of laws on path space, all stated so that the junk values of Lean's total functions never enter. The objects defined here (the $n$-player game with quantified weak solutions, its payoffs and Markovian $\varepsilon$-Nash equilibria) are shared with the other missions of this series.

Difficulty

The obvious argument for $\varepsilon_n\to0$ compares player 1's payoff under a deviation with $T^2$. A deviation changes the drift of the mean only by $O(1/n)$, but the dynamics of the mean, $dY_t=\operatorname{sgn}(Y_t)dt+n^{-1/2}d\overline W_t$, is ill-posed in the limit: the ODE $\dot y=\operatorname{sgn}(y)$, $y_0=0$, has infinitely many solutions $\pm(t-s)^+$. Continuity of the solution map, the usual tool, is unavailable, and one must instead identify the limit law, which comes from the vanishing noise, and show that it is unchanged by the deviation. The second difficulty is that the payoff $X^1_TY_T$ is unbounded, so convergence of laws does not give convergence of payoffs without a uniform integrability estimate. The proof in the paper is short, but relies on a cited result on the vanishing-noise limit and on a compactness argument in a weak $L^2$ topology for the deviating controls.

Formalization scope

• Dimension and state. $d=1$; $\mathbb R^1$ is EuclideanSpace ℝ (Fin 1) (the platform's EthierKurtz.SDEState 1) and its coordinate is y 0. Controls are real, $A=[-1,1]$.
• Pathwise equations. Volatility is the identity, so the SDE of each player is stated as $X^i_t=X^i_0+\int_0^t b\,ds+W^i_t$ almost surely for all $t\in[0,T]$, with a Lebesgue integral of a bounded measurable integrand.
• Solutions are quantified. A weak solution of the $n$-player system is a structure (probability space, filtration, independent $\mathbb F$-Brownian motions, i.i.d. initial states independent of the noise, adapted path-valued states, the empirical flow). Payoffs are functions of a solution; the Nash inequality and every limit statement are required for every solution. Solutions exist and are unique in law, so this matches the paper's definitions; the goal asserts existence explicitly.
• Index shift. Term $n$ of every sequence is the $(n+1)$-player game; the factor $\frac1n$ in the controls and the mean is then $\frac1{n+1}$.
• sgn and time. $\operatorname{sgn}$ is Real.sign ($\operatorname{sgn}0=0$), and the control vanishes at $t=0$, both as printed.
• Unbounded payoff. Assumption A fails ($g$ is unbounded) and is not assumed anywhere. Payoffs are Bochner integrals; $X^i_T\overline\mu^n_T$ is integrable on every solution (bounded drift, $X^i_0=0$), which is a fact to be proved rather than an assumption.
• Laws. Laws on $C([0,T];\mathbb R)$ carry the topology of weak convergence; the mean path is a continuous function of the state paths, so its law is a probability measure by construction.
• Lemma 7.4. Only the $(Y,W)$ coordinates are stated: tightness, (i), the equation for $Y$ in (ii), and (iv). The coordinates $X$ and $\beta$, which need the weak topology of $L^2([0,T];[-1,1])$, and item (iii) are not stated; the norm topology must not be substituted, because the deviating controls are not tight in it.
• Ruled out. A statement in which the profiles have no solutions would make the Nash clause vacuous; the existence clause of the goal excludes it.

Contributions welcome: the existence of weak solutions for bounded measurable Markovian drifts, the vanishing-noise limit of $dZ=\operatorname{sgn}(Z)dt+\epsilon\,dW$, and Girsanov-type change-of-measure estimates are all reusable beyond this mission.

Selected references

• D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit, Ann. Appl. Probab. 30(4), 2020; arXiv:1808.02745v1, 2018. https://arxiv.org/abs/1808.02745
• D. Lacker, A general characterization of the mean field limit for stochastic differential games, Probab. Theory Related Fields 165(3–4), 581–648, 2016 (reference [43] of the paper).
• D. Trevisan, Zero noise limits using local times, Electron. Commun. Probab. 18, 2013 (reference [57] of the paper).
• R. Carmona, D. Lacker, A probabilistic weak formulation of mean field games and applications, Ann. Appl. Probab. 25(3), 2015. https://arxiv.org/abs/1307.1152

Motivation

How should a set of indivisible items (courses, shifts, inherited objects) be divided among people who have different entitlements but no money to transfer? A classical answer for divisible goods is the competitive equilibrium from equal incomes (CEEI): give every agent a budget of artificial currency, find prices at which every agent can afford her favourite bundle and the market clears. The resulting allocation is Pareto optimal and fair. With indivisible items a CEEI can fail to exist already for one item and two agents with equal budgets: at any price, either both agents can afford the item or neither can.

Babaioff, Nisan and Talgam-Cohen (arXiv:1703.08150; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1062) study this Fisher market with indivisible goods when budgets are generic: unequal budgets, with a measure-zero set of exceptional budget pairs excluded. Their main result is for two agents with almost equal budgets. This mission formalizes the companion result for two agents with identical additive preferences and arbitrary unequal budgets (Theorem 8.1 of the paper, its informal Theorem 1.4). With identical preferences the division problem is a discrete claims (bankruptcy) problem: one cake of fixed value is split between claimants with different entitlements $b_1, b_2$.

Timeline of the relevant results:

• Budish (2011, doi:10.1086/664613): approximate CEEI with almost equal budgets for many agents, with an approximate market-clearing error.
• Segal-Halevi (AAMAS 2018, arXiv:1705.04212), a follow-up to the preprint of this paper: for four agents with arbitrary budgets, non-existence of CE persists even with generic budgets.
• Babaioff, Nisan and Talgam-Cohen (preprint 2017, journal 2021): exact CE for two additive agents with almost equal unequal budgets (Theorem 7.1), and for two agents with identical preferences and generic budgets (Theorem 8.1).

Setting

There are $m$ indivisible items $M$ and two agents. Agent $i$ has a valuation $v_i : 2^M \to \mathbb R$ that is additive, normalized ($v_i(M)=1$), non-negative, monotone and strict (different bundles have different values), and a budget $b_i > 0$, with $b_1 + b_2 = 1$. An allocation $\mathcal S = (\mathcal S_1, \mathcal S_2)$ gives every item to exactly one agent. Item prices $p_j \ge 0$ price a bundle at $p(S) = \sum_{j \in S} p_j$.

A bundle $S$ is demanded by agent $i$ at prices $p$ if $p(S) \le b_i$ and $p(T) > b_i$ for every bundle $T$ with $v_i(T) > v_i(S)$. A competitive equilibrium (CE) is a pair $(\mathcal S, p)$ in which each $\mathcal S_i$ is demanded by agent $i$. An allocation is Pareto optimal (PO) if every other allocation is strictly worse for some agent. It is budget-proportional if $v_i(\mathcal S_i) \ge b_i$ for both agents, and anti-proportional if $v_i(\mathcal S_i) \le b_i$ for both, strictly for one.

The truncated share of agent $i$ is

$$b_i^- = \max\{ v_i(\mathcal S'_i) : \mathcal S' \text{ PO},\ v_i(\mathcal S'_i) \le b_i \},$$

the best she can get in a PO allocation that gives her at most her budget share; an allocation gives her the truncated share if $v_i(\mathcal S_i) \ge b_i^-$. The exceptional set $R_i$ (Definition 6.2) consists of the budget pairs $(b_i, 1-b_i)$ for which two PO allocations $\mathcal S(r), \mathcal S(r+1)$, consecutive in agent $i$'s order of preference, satisfy $b_i / v_i(\mathcal S(r+1)_i) = (1-b_i)/(1-v_i(\mathcal S(r)_i))$. It is finite. The rectangle $T_i$ (Definition 6.1) is a set of allocations between the truncated-share maximizers of the two agents.

In Lean all objects live in GenericBudgets.IdenticalPrefs: bundle, price, IsDemanded, IsCE, IsPO, IsStandardValuation, IsBudgetProportional, IsAntiProportional, GetsTruncatedShare, IsTruncMaximizer, InRectT, InR.

Formalization targets

Goal: Theorem 8.1 (p. 20)

If $v_1 = v_2$, $b_1 > b_2$, and $(b_1,b_2) \notin R_i$ for some agent $i$, then

$$\exists\, (\mathcal S, p) \text{ a CE with } v_j(\mathcal S_j) \ge b_j^- \text{ for } j = 1, 2.$$

Milestones

1. Proposition 5.1 (p. 12): every budget-proportional, and every anti-proportional, PO allocation is supported in a CE.
2. Lemma 6.3 (p. 15): no budget-proportional allocation, no PO anti-proportional allocation, $(b_1,b_2) \notin R_i$ and $T_i = \emptyset$ imply a CE with truncated shares.
3. Constant-sum claim (p. 20): with identical preferences every allocation is PO and none is anti-proportional.
4. Lemma 8.2 (p. 20): if every allocation is PO and $(b_1,b_2) \notin R_i$ for some $i$, a CE exists; if moreover no PO allocation is anti-proportional, the same CE gives truncated shares.

Significance

Theorem 8.1 shows that the non-existence of CEEI for identical preferences is a knife-edge phenomenon: for every market with identical strict additive preferences, every unequal budget pair outside a finite set admits a CE, and the CE allocation is as close to budget-proportional as indivisibility allows. It gives a market-based solution to the indivisible claims problem with unequal entitlements, and its CE inherits Pareto optimality from the first welfare theorem (Theorem 2.4 of the paper).

The formalization targets three things on top of the paper. First, a machine-checked proof of the paper's main technical tool, Lemma 6.3, which also drives the paper's main Theorem 7.1 (mission 1 of this series), where it is applied to almost equal budgets instead of identical preferences. Second, precise definitions of the truncated share, the rectangle $T_i$ and the exceptional set $R_i$, whose informal versions leave conventions implicit (the maximization runs over PO allocations only; $R_i$ is indexed by consecutive PO allocations). Third, verification of the proof chain Proposition 5.1 → Lemma 6.3 → Lemma 8.2 → Theorem 8.1. The statements compile, but none of these results has a machine-checked proof yet.

Difficulty

The reduction of Theorem 8.1 to Lemma 8.2 and the proof of Lemma 8.2 from Proposition 5.1 and Lemma 6.3 are short. The substance is in Lemma 6.3, which must exhibit prices supporting a PO allocation when no allocation gives both agents their budget shares. Demand is a condition over all $2^m$ bundles, so a candidate price vector has to be checked against every bundle each agent prefers, and the paper's construction breaks down on the exceptional budget pairs $R_i$, which is why they are excluded; the argument is a case analysis over the finite Pareto frontier. The easy case, Proposition 5.1, covers only markets with a budget-proportional or anti-proportional PO allocation; with identical preferences and unequal budgets neither typically exists (no allocation is ever anti-proportional), so Lemma 6.3 cannot be avoided.

Formalization scope

Items are Fin m; agents are Fin 2, with indices $0, 1$ for the paper's agents $1, 2$, so $b_1 > b_2$ is b 1 < b 0. Valuations are functions Finset (Fin m) → ℝ bundled with the standing assumptions in IsStandardValuation; identical preferences are the hypothesis v 0 = v 1. An allocation is a map Fin m → Fin 2, so every item is allocated exactly once. Budgets are positive reals summing to $1$. All quantities are real.

Committed conventions and disclosed restrictions:

• Strictness is injectivity of each valuation on bundles. The paper allows one exception, identical items; that exception is dropped, so markets with identical items are not covered by these statements.
• The budget-proportional share is written $b_i\,v_i(M)$, which equals $b_i$ under normalization.
• The truncated share is stated without a max: $v_i(\mathcal S_i) \ge v_i(\mathcal S'_i)$ for every PO $\mathcal S'$ with $v_i(\mathcal S'_i) \le b_i$.
• "$(b_1,b_2)$ does not belong to $R_i$ for some agent $i$" is read as an existential over $i$.
• $R_i$ is encoded with consecutive PO allocations and the cross-multiplied equation, equivalent to the page's quotient form.
• The constant-sum sentence of p. 20 says "at most their truncated share"; the definition it paraphrases (anti-proportional, p. 12) uses the budget-proportional share, and that is what is stated.

Trivializing formalizations are ruled out: the demand condition quantifies over every bundle with strict inequality, allocations must assign every item, prices are non-negative, the truncated share is maximized over PO allocations only (not over all allocations), and the budget hypothesis excludes only the finite set $R_i$ for one agent, never all unequal budgets.

Proposition 5.1 and Lemma 6.3 are posed with the same statement as in mission 1 of this series; a proof of either transfers verbatim. Contributions welcome: the finite-frontier infrastructure (existence and uniqueness of the truncated-share maximizer), Proposition 5.1 through budget-exhausting combination pricing, and Lemma 6.3.

Selected references

• M. Babaioff, N. Nisan, I. Talgam-Cohen, Competitive Equilibrium with Indivisible Goods and Generic Budgets, arXiv:1703.08150v2, 2018; Mathematics of Operations Research 46(1), 2021. https://arxiv.org/abs/1703.08150, https://doi.org/10.1287/moor.2020.1062
• 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. Segal-Halevi, Competitive Equilibrium for Almost All Incomes, Proceedings of the 17th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), 2018, pp. 1267–1275. https://arxiv.org/abs/1705.04212