Algorithmic Game Theory

Motivation

In a combinatorial auction a set of $m$ items is sold to $n$ bidders who value bundles of items rather than single items. Spectrum auctions, procurement of transportation lanes and the allocation of cloud resources all have this form, and the central algorithmic question is how to allocate the items so as to maximize the social welfare, the sum of the bidders' values for what they receive. Even to describe a general valuation takes $2^m$ numbers, so algorithms access the bidders through queries, and the achievable approximation depends on the class of valuations allowed.

Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010) study bidders without complementarities. For the class of XOS valuations, maxima of additive valuations, which strictly contains the submodular valuations, they give LP-based algorithms and, in §3.3, a purely combinatorial algorithm: bidders arrive one at a time, take their demanded bundle at the current item prices, and raise the prices of what they took. Its analysis charges the welfare of any allocation to the item prices the algorithm sets, an argument that uses only the demand and XOS oracles.

Setting

The items are $M=\{1,\dots,m\}$ and the bidders $1,\dots,n$.

• An additive valuation (a clause) $w$ assigns nonnegative values $w(1),\dots,w(m)$ to the items and $w(S)=\sum_{j\in S}w(j)$ to a bundle $S\subseteq M$.
• An XOS valuation $v$ is given by a nonempty finite set of clauses $\{w_1,\dots,w_t\}$ (its XOS expression) through $v(S)=\max_k w_k(S)$. A clause $w_k$ with $w_k(S)=v(S)$ is a maximizing clause for $S$. Every XOS valuation is normalized, $v(\emptyset)=0$, and monotone.
• An allocation is a tuple of pairwise disjoint bundles $O_1,\dots,O_n$; items may stay unallocated. Its welfare is $\sum_i v_i(O_i)$.
• A demand oracle for bidder $i$ answers, given item prices $p\in\mathbb R^m$, a bundle maximizing $v_i(T)-\sum_{j\in T}p_j$. An XOS oracle answers, given a bundle $S$, a maximizing clause for $S$ in $v_i$.

The greedy price-update algorithm. Start with all bundles empty and all prices $p_j=0$. For $i=1,\dots,n$: let $S_i$ be bidder $i$'s demand at the current prices; remove the items of $S_i$ from the bundles of the earlier bidders; let $q^i$ be the maximizing clause for $S_i$ in $v_i$; set $p_j=q^i_j$ for $j\in S_i$. Write $p^k$ for the prices after stage $k$ ($p^0=0$), $p^k(T)=\sum_{j\in T}p^k_j$, and $A_1,\dots,A_n$ for the final bundles.

In the Lean development these objects are XOSExpr, XOSExpr.val, IsAllocation, welfare, IsDemandOracle, IsXOSOracle, greedyState, greedyPrices and greedyAlloc in the namespace ComplementFreeCA.XOSGreedy.

Formalization targets

Goal: Theorem 3.3

For XOS valuations $v_1,\dots,v_n$, every demand oracle and every XOS oracle, and every allocation $O_1,\dots,O_n$,

$$\sum_{i=1}^n v_i(O_i)\;\le\;2\sum_{i=1}^n v_i(A_i).$$

The comparison with every allocation is the paper's comparison with the optimal allocation.

Milestones

1. Lemma 3.4. The final prices are paid for by the algorithm's welfare:

$$p^n(M)\le\sum_i v_i(A_i).$$

2. Lemma 3.5. Prices never decrease: $p^k_j\le p^{k'}_j$ for all items $j$ and stages $k\le k'$.
3. Lemma 3.6. For every allocation $O$,

$$\sum_i v_i(O_i)\le 2\,p^n(M).$$

Three further statements are included without being milestones: the output $A_1,\dots,A_n$ is an allocation (used implicitly by the paper); the first sentence of the proof of Lemma 3.6, that with $\Delta^i=p^i(M)-p^{i-1}(M)$ one has $\Delta^i=\max_{T\subseteq M}\bigl(v_i(T)-p^{i-1}(T)\bigr)$; and the factor $2$ is attained on the paper's two-item, two-bidder example (p. 9).

Significance

Theorem 3.3 shows that a factor-2 approximation of the optimal welfare for XOS bidders needs no linear program: one pass over the bidders, one demand query and one XOS query each. The paper's LP-based algorithm of §3.2 attains the better ratio $e/(e-1)$, and Theorem 4.1 of the paper shows that for the larger class of complement-free bidders no $(2-\epsilon)$-approximation is possible with polynomial communication.

The result is proved in the paper; to the best of our knowledge it has no machine-checked proof. This mission produces a formal model of XOS valuations, demand and XOS oracles and the greedy run that is reusable for other price-based arguments, and a formal proof of the guarantee for every tie-breaking in both oracles.

Difficulty

The argument is elementary, but its bookkeeping is where a formal proof can go wrong. Items move between bidders: an item taken from an earlier bidder in step (b) is re-priced in step (d), and every priced item lies in exactly one final bundle. Lemma 3.4 needs this invariant across all $n$ stages, together with the fact that a maximizing clause for the demanded set bounds $v_i$ on every subset, which holds because it is a clause of $v_i$ itself, not merely an additive function agreeing with $v_i$ on $S_i$. Lemma 3.5 is a contradiction argument using optimality of the demand; Lemma 3.6 telescopes the price increases and needs prices to stay nonnegative. The argument must hold for arbitrary oracle answers, so no canonical demand can be assumed.

Formalization scope

• Bidders are Fin n, items Fin m, bundles Finset (Fin m), values in ℝ. An XOS valuation is represented by its expression: a nonempty Finset (Fin m → ℝ) of clauses with nonnegative entries, evaluated with Finset.sup'. The paper's standing assumptions, normalized and monotone valuations (p. 1), hold automatically in this representation.
• The oracles are function parameters dem : Fin n → (Fin m → ℝ) → Finset (Fin m) and cl : Fin n → Finset (Fin m) → (Fin m → ℝ) with hypotheses IsDemandOracle and IsXOSOracle; every theorem holds for every such pair, so no tie-breaking rule is fixed.
• The run is a recursion on the stage: stage $k+1$ processes the 0-based bidder $k$, i.e. the paper's bidder $k+1$; after stage $n$ the state is constant.
• The paper's goal compares with the optimal allocation; the Lean goal compares with every allocation, which is equivalent and avoids an argmax. Stating the bound against one particular allocation, or against the algorithm's own output, would be trivial and is excluded.
• There are no $O(\cdot)$ constants: the factor $2$ is the paper's.
• Printed slip: the model on p. 1 writes an allocation as $S_1,\dots,S_m$; it is one bundle per bidder, $S_1,\dots,S_n$.
• Out of scope: running time, the cost of simulating oracles (Proposition 2.1), and communication lower bounds.

Contributions welcome: proofs of the three milestones and of the goal, and reusable lemmas on the invariant that every priced item lies in exactly one final bundle.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• B. Lehmann, D. Lehmann, N. Nisan, Combinatorial auctions with decreasing marginal utilities, Games and Economic Behavior 55(2):270–296, 2006. https://doi.org/10.1016/j.geb.2005.02.006

Motivation

In a combinatorial auction a seller offers $m$ indivisible items to $n$ bidders, each of whom values bundles of items rather than single items. Allocating the items so as to maximize the total value (the social welfare) is the central optimization problem of the area: it models spectrum auctions, procurement and resource allocation, and it is NP-hard and hard to approximate for general valuations. A large literature therefore studies restricted classes of valuations without complementarities. Among them the class XOS (valuations that are a maximum of additive valuations, also called fractionally subadditive) sits strictly between submodular and subadditive valuations and has become a standard benchmark class in algorithmic game theory.

Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010) gave, among other results, a randomized algorithm that approximates the optimal welfare for XOS bidders within a factor $1/(1-(1-1/n)^n)$, which is at most $e/(e-1)\approx 1.582$. The algorithm rounds the standard LP relaxation and resolves conflicts between bidders using the XOS structure. This mission formalizes that guarantee (Theorem 3.2 of the paper).

A short timeline: Lehmann, Lehmann and Nisan (EC 2001) introduced the XOS terminology and a 2-approximation for submodular bidders; the conference version of the present paper (STOC 2005) gave the $e/(e-1)$ bound for XOS with demand and XOS oracles; Feige (STOC 2006) extended the $e/(e-1)$ ratio to XOS bidders with demand oracles only and gave a 2-approximation for subadditive bidders.

Setting

Items are $M=\{1,\dots,m\}$ and bidders are $N=\{1,\dots,n\}$ with $n\ge1$. Bidder $i$ has a valuation $v_i$ assigning a real number $v_i(S)$ to every bundle $S\subseteq M$. An allocation is a tuple $(O_1,\dots,O_n)$ of pairwise disjoint bundles; its welfare is $\sum_i v_i(O_i)$.

A clause is an additive valuation $w$ given by nonnegative item values $w_1,\dots,w_m$, with $w(S)=\sum_{j\in S}w_j$. A valuation $v$ is XOS if there is a nonempty finite set $W$ of clauses with

$$v(S)=\max_{w\in W}\ \sum_{j\in S}w_j\qquad(S\subseteq M).$$

A clause of $W$ attaining the maximum for $S$ is a maximizing clause for $S$ in $v$; an XOS oracle returns one (arbitrarily, if several attain it).

The LP relaxation has a variable $x_{i,S}$ for every bidder $i$ and bundle $S$ and asks to maximize $\mathrm{OPT}^*=\sum_{i,S}x_{i,S}v_i(S)$ subject to $\sum_{i}\sum_{S\ni j}x_{i,S}\le1$ for each item $j$, $\sum_S x_{i,S}\le1$ for each bidder $i$, and $x_{i,S}\ge0$.

Randomized rounding draws a preallocation $S_1,\dots,S_n$: independently for each bidder $i$, bundle $S$ is chosen with probability $x_{i,S}$ and the empty bundle with the remaining probability $1-\sum_S x_{i,S}$. The preallocation can give an item to several bidders.

The algorithm of §3.2: (i) draw a preallocation from an optimal LP solution $x$; (ii) let $p^i=(p^i_1,\dots,p^i_m)$ be the maximizing clause for $S_i$ in $v_i$; (iii) give each item $j$ to a bidder $i$ with $p^i_j\ge p^{i'}_j$ for all $i'$. Write $\mathrm{ALG}$ for the welfare of the resulting allocation.

Formalization targets

Goal: Theorem 3.2

For every XOS profile, every optimal LP solution $x$, every choice of maximizing clauses, every tie-breaking in step (iii) and every allocation $O$,

$$\Big(1-\Big(1-\frac1n\Big)^n\Big)\sum_i v_i(O_i)\ \le\ \mathbb E[\mathrm{ALG}].$$

Milestones

1. $\sum_i v_i(O_i)\le\mathrm{OPT}^*$ for an optimal LP solution (step (i) of the proof of Theorem 3.1).
2. Pointwise, $\mathrm{ALG}\ge\sum_j Q_j$ with $Q_j=\max_i p^i_j$.
3. Eq. (1): for $1\le k\le n$ and $X_1,\dots,X_k\in[0,1]$ with $\sum X_i\le1$,

$$1-\prod_{i\le k}(1-X_i)\ \ge\ 1-\Big(1-\tfrac{\sum X_i}{k}\Big)^k\ \ge\ \Big(1-\big(1-\tfrac1k\big)^k\Big)\sum X_i\ \ge\ \Big(1-\big(1-\tfrac1n\big)^n\Big)\sum X_i .$$

4. Lemma 3.3: $\mathbb E[Q_j]\ge(1-(1-1/n)^n)\sum_i\sum_{S\ni j}x_{i,S}\,p^{(i,S)}_j$ for every feasible $x$.
5. $\mathbb E[\mathrm{ALG}]\ge(1-(1-1/n)^n)\,\mathrm{OPT}^*(x)$ for every feasible $x$.

Milestone 5 is stronger than the goal (it compares with the fractional value); the goal is stated against the integral optimum because that is what Theorem 3.2 asserts.

Significance

The bound $1-(1-1/n)^n\ge1-1/e$ is a constant-factor guarantee for a class that includes every submodular valuation, obtained from nothing more than the LP relaxation and the clause structure of XOS. It shows that the integrality gap of the configuration LP for XOS bidders is at most $1/(1-(1-1/n)^n)$, a fact reused in later work on welfare maximization, online allocation and posted-price mechanisms. The per-item analysis (Lemma 3.3 and Eq. (1)) is the same "$1-1/e$" correlation-gap argument that recurs in submodular maximization and prophet-inequality proofs.

The result is proved in the paper. To our knowledge it has no machine-checked proof. This mission produces a Lean statement and proof of the guarantee with the randomness made explicit, a reusable model of the configuration LP and of randomized rounding over bundles, and a formal version of the inequality in Eq. (1), which is independently useful.

Difficulty

Each piece of the argument is short; the work is in the bookkeeping. The preallocation is infeasible, so welfare cannot be read off from the rounding directly; the proof reduces it to per-item quantities $Q_j$ and then lower-bounds $\mathbb E[Q_j]$ by comparing with a different assignment of item $j$ that is not the algorithm's. The expectation of that auxiliary assignment involves a product of probabilities over bidders ordered by a conditional expectation, and the final bound needs the calculus inequality of Eq. (1) together with a summation by parts. A naive attempt to bound $\mathbb E[\mathrm{ALG}]$ bidder by bidder fails, because a bidder's received bundle is not contained in its preallocated bundle, and the clause values of other bidders decide what it receives.

Formalization scope

• Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. XOS is stated through its expression: each $v_i$ comes with a nonempty finite clause set $W_i$ of nonnegative clauses, and $v_i(S)$ is attained by a clause of $W_i$ and bounded by all of them. Normalization and monotonicity, the paper's standing assumptions (p. 1), follow from this.
• The LP has a variable for every bundle, including $\emptyset$. "Optimal" is stated as feasible and not beaten by any feasible solution; existence of an optimum is not asserted.
• The rounding is a finite product distribution over profiles $\sigma:\mathrm{Fin}\,n\to$ bundles, with bidder $i$'s law $q_i(S)=x_{i,S}+\mathbf 1[S=\emptyset](1-\sum_T x_{i,T})$; expectations are finite sums.
• The XOS oracle is a function parameter with its specification, and step (iii) is any rule selecting a bidder with maximal clause value; every statement quantifies over all of them.
• "Approximation" in Theorem 3.2 is read in expectation, as its proof establishes. There are no $O(\cdot)$ constants in this mission.
• Printed slip: the display of Lemma 3.3 (and the identity for $\mathrm{OPT}^*$ before it) sums $x_{i,S}p^{(i,S)}_j$ over all $(i,S)$; the proof's final line restricts to $S\ni j$, and the printed version is false. The Lean states Lemma 3.3 with $S\ni j$.
• Running time, the ellipsoid method and oracle complexity are out of scope.
• Ruled out as trivializing: dropping the LP constraints on $x$ (the item constraint is what makes Eq. (1) apply), stating the bound for a fixed preallocation instead of the expectation, or allowing negative clause values.

A complete development needs finite product distributions over bundles, the AM–GM inequality, monotonicity of $(1-1/k)^k$, and a summation-by-parts argument. The LP and rounding model are reusable for the other randomized-rounding results of the paper; proofs of any milestone are welcome.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• S. Dobzinski, N. Nisan, M. Schapira, Approximation algorithms for combinatorial auctions with complement-free bidders, STOC 2005. https://doi.org/10.1145/1060590.1060681
• B. Lehmann, D. Lehmann, N. Nisan, Combinatorial auctions with decreasing marginal utilities, EC 2001. https://doi.org/10.1145/501158.501161
• U. Feige, On maximizing welfare when utility functions are subadditive, STOC 2006. https://doi.org/10.1145/1132516.1132540

Motivation

In a combinatorial auction a seller offers $m$ indivisible items to $n$ bidders, each of whom values bundles of items rather than single items. Allocating the items to maximize total value is the basic welfare problem of spectrum auctions, procurement and resource allocation, and it is the running example of algorithmic mechanism design. For general valuations no polynomial-time algorithm achieves a ratio polynomially better than $\sqrt m$ under standard assumptions, so positive results require restricting the valuations. The most natural restriction is complement freeness (subadditivity): a bundle is never worth more than the sum of its parts.

Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010; conference version STOC 2005) gave the first polynomial-time algorithms with sub-polynomial approximation ratios for complement-free bidders given demand oracles. This mission formalizes their Section 3.1 algorithm, which rounds the linear-programming relaxation of the auction and splits the resulting infeasible solution into feasible ones.

Timeline. Lehmann, Lehmann and Nisan (2001) introduced the complement-free hierarchy and treated submodular bidders. The original version of the algorithm formalized here claimed an $O(\log m)$ ratio; Feige observed that the same algorithm achieves $O(\log m/\log\log m)$ and that its ratio is at least $\Omega(\sqrt{\log m/\log\log m})$ (Feige, SIAM J. Comput. 39(1), 2009). Feige then obtained a constant ratio ($2$) for subadditive bidders by a different rounding.

Setting

Items are $M=\{1,\dots,m\}$ and bidders $N=\{1,\dots,n\}$. Bidder $i$ has a valuation $v_i$ assigning a real value $v_i(S)$ to each bundle $S\subseteq M$. Every valuation is normalized, $v_i(\emptyset)=0$, and monotone, $S\subseteq T\Rightarrow v_i(S)\le v_i(T)$. A valuation is complement free if $v(S\cup T)\le v(S)+v(T)$ for all $S,T$. An allocation is a tuple $(S_1,\dots,S_n)$ of pairwise disjoint bundles; its welfare is $\sum_i v_i(S_i)$, and $OPT$ denotes the largest welfare.

The LP relaxation has a variable $x_{i,S}\ge0$ for each bidder and bundle, with $\sum_{i,S\ni j}x_{i,S}\le1$ for each item $j$ and $\sum_S x_{i,S}\le1$ for each bidder $i$; its objective is $\sum_{i,S}x_{i,S}v_i(S)$, with optimum $OPT^*\ge OPT$. Randomized rounding lets each bidder independently draw bundle $S$ with probability $x_{i,S}$ and $\emptyset$ with the remaining probability. The result, a preallocation, has expected welfare $OPT^*$ but may give an item to several bidders.

The algorithm takes $k=\lfloor 3\log m/\log\log m\rfloor$ and:

1. rounds until the preallocation $(S_1,\dots,S_n)$ has every item in at most $k$ bundles and $\sum_i v_i(S_i)\ge OPT^*/3$;
2. splits each $S_i$ into layers $S_i^r$, $r=1,\dots,k$, where $S_i^r$ holds the items of $S_i$ that appear in exactly $r-1$ of $S_1,\dots,S_{i-1}$;
3. picks the layer index $r$ maximizing $\sum_i v_i(S_i^r)$ and sets $T_i=S_i^r$;
4. if some bidder has $v_i(M)\ge\sum_{i'}v_{i'}(T_{i'})$, gives that bidder everything instead.

Formalization targets

Goal: Theorem 3.1, with the explicit ratio

For all sufficiently large $m$, for normalized, monotone, complement-free valuations and an optimal LP solution $x$ with value $OPT^*$:

1. if $OPT^*>3\max_i v_i(M)$, one rounding meets the two conditions of step 1 with probability $>1/6$;
2. from any preallocation meeting them, every admissible run of steps 2–4 outputs an allocation with

$$\sum_i v_i(\text{output}_i)\ \ge\ \frac{OPT}{3k},\qquad k=\Big\lfloor\frac{3\log m}{\log\log m}\Big\rfloor;$$

3. if $OPT^*\le3\max_i v_i(M)$, the bidder maximizing $v_i(M)$ alone achieves $OPT/3$.

Milestones

• $OPT\le OPT^*$ (proof, step (i)).
• The layers of each index form an allocation and partition each $S_i$ (proof, step (ii)).
• Complement freeness gives $\sum_r v_i(S_i^r)\ge v_i(S_i)$, and the best layer has welfare $\ge OPT^*/(3k)$ (proof, step (iii)).
• Lemma 3.1: independent Bernoulli variables with $\sum_i p_i\le1$ exceed $3\log m/\log\log m$ with probability $\le1/m^2$.
• Lemma 3.2: for $X$ a sum of independent $[0,1]$ variables with mean $\mu$, $\Pr[|X-\mu|\ge\alpha]\le\mu/\alpha^2$.
• §3.1.1: some item appears more than $3\log m/\log\log m$ times with probability $\le1/m$; the preallocation's welfare falls below $OPT^*/3$ with probability $<3/4$.

Significance

Theorem 3.1 was among the first polynomial-time approximation guarantees for welfare maximization with general subadditive bidders, and its layering argument is the standard way to turn an LP solution that is feasible up to a factor $k$ into a feasible allocation losing only a factor $k$ for subadditive objectives. The same argument applies to the $k$-duplicates auction and reappears in later rounding schemes. Lemma 3.1 is the standard balls-in-bins tail bound behind every $\log m/\log\log m$ load estimate.

The results are proved in the paper; none of them is formalized, on this platform or in Mathlib, as far as searches show. The mission produces a machine-checked version of the algorithm's guarantee with an explicit constant $3k$ in place of $O(\cdot)$, a precise statement of the probabilistic step, and reusable statements of two concentration inequalities for sums of independent bounded variables.

Difficulty

The combinatorial part (steps (ii) and (iii)) is short. The difficulty is in step (i). The rounding is a product distribution over bundles, while the count of an item is a sum over bidders of indicators that depend on each bidder's whole bundle; connecting the finite product law to independent Bernoulli variables, and then to Lemma 3.1, requires building the independence structure explicitly. Lemma 3.1 itself does not follow from a Chernoff bound with a fixed relative deviation: the threshold $3\log m/\log\log m$ grows with $m$ while the mean stays at most $1$, and the bound must hold uniformly in the number of variables, which a fixed-deviation Chernoff statement does not give. Finally, the event-$B$ bound needs the preallocation's welfare as a sum of independent variables in $[0,1]$, which requires rescaling by $\max_i v_i(M)$ and monotonicity.

Formalization scope

Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity, the paper's standing assumptions (p. 1), are hypotheses of the goal. $\log$ is the natural logarithm; the paper does not fix a base. The rounding law is written as explicit finite sums over profiles $\sigma:\texttt{Fin } n\to\texttt{Finset (Fin } m)$ with product weights, so independence across bidders is literal; Lemmas 3.1 and 3.2 are stated measure-theoretically with Mathlib's iIndepFun.

Explicit constants and conventions that replace the paper's notation:

• The ratio $O(k)=O(\log m/\log\log m)$ is stated as $3k$ with $k=\lfloor3\log m/\log\log m\rfloor$, the constant the proof establishes (step (iii), p. 6). "Sufficiently large $m$" is an existential $m_0$.
• The w.l.o.g. scaling $\max_i v_i(M)=1$ and the split at $OPT^*=3$ become the scale-free split at $OPT^*=3\max_i v_i(M)$.
• The choice of $r$ in step (iii) and of the bidder in step (iv) are universally quantified over all admissible choices.

Printed slips resolved in the statements:

• Lemma 3.1 mixes $n$ and $m$. Here the number of variables is arbitrary, "sufficiently large" refers to $m$, and $\sum_ip_i=1$ is relaxed to $\sum_ip_i\le1$, which is what the application uses.
• The display after Lemma 3.1 writes the threshold $\log m/(3\log\log m)$; the lemma's $3\log m/\log\log m$ is used.
• "$\Pr[\vee_jE_j]<1/n$" and "$\le 1/n+3/4$" should read $1/m$.
• The event $B$ is defined without its sum; it means $\sum_iv_i(S_i)<OPT^*/3$.

Trivializing formalizations are ruled out: the guarantee assumes the item-count bound (without it the layers do not cover the bundles), the probability statements assume an LP-feasible $x$, neither the layer index nor the step-(iv) bidder is fixed, and the ratio is the explicit $3k$ rather than an unspecified constant. Running time, the ellipsoid method and oracle complexity are out of scope. Contributions of general concentration lemmas for sums of independent bounded variables are welcome and reusable beyond this mission.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• U. Feige, On Maximizing Welfare When Utility Functions Are Subadditive, SIAM Journal on Computing 39(1):122–142, 2009. https://doi.org/10.1137/070680977
• B. Lehmann, D. Lehmann, N. Nisan, Combinatorial Auctions with Decreasing Marginal Utilities, Games and Economic Behavior 55(2):270–296, 2006. https://doi.org/10.1016/j.geb.2005.02.006
• M. Mitzenmacher, E. Upfal, Probability and Computing, Cambridge University Press, 2005. https://doi.org/10.1017/CBO9780511813603

Motivation

A buyer and a seller negotiate over one indivisible good. Each knows the good's worth to themselves but not to the other side, so each shades their offer to exploit the other's uncertainty, and some mutually profitable trades fail. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this as a one-shot game of simultaneous sealed offers and computed its equilibria in closed form for uniformly distributed values.

That closed-form equilibrium became the reference example of bilateral trade with two-sided private information. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) proved that no mechanism can guarantee efficient trade in this setting and showed that, for uniform values, the equilibrium of the sealed-offer game with $k = 1/2$ attains the largest expected gains from trade of any incentive-compatible, individually rational mechanism. The later literature on the $k$-double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) studies the same game and uses the linear equilibrium as its benchmark.

Setting

A seller has reservation price $v_s$ and a buyer has reservation price $v_b$, both in $[0, \bar v]$ with $\bar v > 0$. Each knows their own value. Each believes the other's value is uniformly distributed on $[0, \bar v]$: the distribution functions are $F_s(v) = F_b(v) = v/\bar v$ on $[0, \bar v]$. In Lean this belief is the measure unif v̄, Lebesgue measure conditioned on $[0, \bar v]$.

Under the Bargaining Rule, the seller asks $s$ and the buyer offers $b$ simultaneously. If $b \ge s$ the good is sold at $P = kb + (1-k)s$ for a fixed $k \in [0, 1]$; if $b < s$ there is no sale. On a sale the seller earns $P - v_s$ and the buyer $v_b - P$; otherwise both earn zero. The case $k = 1$ gives the buyer the right to make a take-it-or-leave-it offer, $k = 0$ gives it to the seller, and $k = 1/2$ splits the difference.

An offer strategy maps values to offers: $S$ for the seller, $B$ for the buyer. Against $S$, a buyer with value $v$ who offers $b$ earns in expectation

$$\pi_b(b, v) = \int \mathbf 1\{S(v_s) \le b\}\,\bigl(v - kb - (1-k)S(v_s)\bigr)\,d\,\mathrm{unif}_{\bar v}(v_s),$$

and against $B$ a seller with value $v$ asking $s$ earns $\pi_s(s, v) = \int \mathbf 1\{s \le B(v_b)\}\,(kB(v_b) + (1-k)s - v)\,d\,\mathrm{unif}_{\bar v}(v_b)$. These are buyerProfit and sellerProfit. The pair $(S, B)$ is an equilibrium (IsEquilibrium) if, for every value in $[0, \bar v]$, each player's prescribed offer maximises their expected profit over all real offers.

Formalization targets

Goal: Example 1(a)

Write $S_{\mathrm{lin}}(v) = \frac{v}{2-k} + \frac{1-k}{2}\bar v$ and $B_{\mathrm{lin}}(v) = \frac{v}{1+k} + \frac{k(1-k)}{2(1+k)}\bar v$. If $S$ and $B$ are measurable and

$$\begin{aligned} S(v_s) &= S_{\mathrm{lin}}(v_s) && \text{for } 0 \le v_s \le \tfrac{2-k}{2}\bar v, &\qquad S(v_s) &\ge S_{\mathrm{lin}}(v_s) && \text{for } \tfrac{2-k}{2}\bar v < v_s \le \bar v,\\ B(v_b) &\le B_{\mathrm{lin}}(v_b) && \text{for } 0 \le v_b < \tfrac{1-k}{2}\bar v, &\qquad B(v_b) &= B_{\mathrm{lin}}(v_b) && \text{for } \tfrac{1-k}{2}\bar v \le v_b \le \bar v, \end{aligned}$$

then $(S, B)$ is an equilibrium. The statement leaves the no-trade branches free, as the paper does: a seller whose value exceeds every serious bid may ask anything at least $S_{\mathrm{lin}}$, and a buyer whose value is below every serious ask may bid anything at most $B_{\mathrm{lin}}$.

Milestones

1. The linear rules solve (3a)–(3b). The paper's own justification of Example 1(a): with $F_b = F_s = v/\bar v$ and densities $1/\bar v$, the pair $(S_{\mathrm{lin}}, B_{\mathrm{lin}})$ satisfies the linked differential equations of the paper's Theorem 2, $kF_b(y)S'(y) + f_b(y)S(y) = B^{-1}(S(y))f_b(y)$ and $(1-k)(1 - F_s(x))B'(x) - f_s(x)B(x) = -S^{-1}(B(x))f_s(x)$.
2. Seller half. For every seller value $v \in [0, \bar v]$ and every real ask $s$, $\pi_s(s, v) \le \pi_s(S(v), v)$.
3. Buyer half. For every buyer value $v \in [0, \bar v]$ and every real offer $b$, $\pi_b(b, v) \le \pi_b(B(v), v)$.

The goal is the conjunction of milestones 2 and 3, by definition of equilibrium. Milestone 1 is the step the paper actually writes down; it records the necessary first-order conditions and does not by itself give the global best-response property.

Significance

The result. Example 1(a) is the explicit equilibrium from which the paper derives the probability of trade, $(-k^2 + k + 2)/8$, and each party's ex ante profit as a function of $k$ (Example 1(b)–(c)). It is the equilibrium shown by Myerson and Satterthwaite to be second-best efficient at $k = 1/2$, and it is the standard test case against which other double-auction equilibria and mechanisms for bilateral trade are compared.

Formalizing it. The result is proved in the literature but, to our knowledge, has not been machine-checked. The paper itself only observes that the linear branches satisfy the first-order conditions; the global statement (no deviation to any real offer is profitable, including deviations that reach the other side's no-trade types) is left to the reader. A formal proof closes that gap and yields reusable facts about expected profits under uniform beliefs. The two companion missions of this series formalize the paper's Theorem 2 (the linked differential equations in general) and Example 1(b)–(c) (trade probability and expected profits).

Difficulty

First-order conditions do not suffice. A seller can ask below the lowest serious ask $\frac{1-k}{2}\bar v$ and trade with buyers on the free lower branch, whose bids are only bounded above; a buyer can bid above $\frac{2-k}{2}\bar v$ and meet sellers on the free upper branch, whose asks are only bounded below. The best-response inequality must hold for every such deviation and for every admissible choice of the free branches, so it cannot be read off from the linear strategies alone. The expected profit is a piecewise function of the offer, with the pieces determined by where the offer meets the opponent's linear branch and the free branches, and the inequality must be shown on each piece and at the boundaries, uniformly in $k \in [0, 1]$ including the endpoints $k = 0$ and $k = 1$, where one of the free ranges is empty.

Formalization scope

Values and offers are real numbers; strategies are functions $\mathbb R \to \mathbb R$, and their values outside $[0, \bar v]$ are irrelevant because the beliefs give that set measure zero. Beliefs are the probability measure unif v̄ = volume[|Icc 0 v̄]; expected profits are Bochner integrals against it, written over the opponent's value rather than against an offer density. The value intervals are closed; ties $b = s$ trade; deviations range over all of $\mathbb R$; $k$ ranges over the closed interval $[0, 1]$.

The strategies $S$ and $B$ are assumed measurable. Without this a deviation's expected profit could be the junk value $0$ of a non-integrable Bochner integral; with it, all integrands are bounded on the trade event. The inline coefficient $(k(1-k)/2(1+k))\bar v$ of the page is read as $\frac{k(1-k)}{2(1+k)}\bar v$, the reading under which the buyer's lowest serious bid equals the seller's lowest serious ask, as in the paper's Figure 1.

The claim is the sufficiency direction only; the paper states that other equilibria exist, and a statement that every equilibrium has the linear form would be false. The canonical linear pair satisfies all hypotheses, so the goal is not vacuous.

Useful infrastructure includes integrals of piecewise-affine functions against the uniform measure on an interval and the distribution function of volume[|Icc 0 v̄]. Contributions welcome: proofs of the milestones, and lemmas computing $\pi_s$ and $\pi_b$ in closed form on each piece.

Selected references

• K. Chatterjee and W. Samuelson, Bargaining under Incomplete Information, Operations Research 31(5):835–851, 1983. https://doi.org/10.1287/opre.31.5.835
• R. B. Myerson and M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2):265–281, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• M. A. Satterthwaite and S. R. Williams, Bilateral Trade with the Sealed Bid k-Double Auction: Existence and Efficiency, Journal of Economic Theory 48(1):107–133, 1989. https://doi.org/10.1016/0022-0531(89)90120-8
• W. Leininger, P. B. Linhart and R. Radner, Equilibria of the Sealed-Bid Mechanism for Bargaining with Incomplete Information, Journal of Economic Theory 48(1):63–106, 1989. https://doi.org/10.1016/0022-0531(89)90121-X

Motivation

Cost and benefit allocation problems arise whenever several parties share a joint undertaking: towns building a common water supply, divisions of a firm sharing overhead, users of a multi-purpose reservoir. They are modelled as cooperative games, and a rule that divides the joint value among the players is an allocation procedure. The standard such rule, the Shapley value, was characterized by Shapley (1953) through efficiency, symmetry, a dummy axiom and additivity. Additivity (the allocation of a sum of two games is the sum of the allocations) is a mathematical convenience with little direct appeal in applications, and it has been the most criticized of the four axioms.

H. P. Young's paper Monotonic Solutions of Cooperative Games (Int. J. Game Theory 14, 1985) studies allocation procedures through monotonicity: how a player's allocation should respond when the game changes. Its Theorem 1 shows that the core is incompatible with coalitional monotonicity for five or more players (the subject of the sister mission of this series). Its Theorem 2, the subject of this mission, shows that efficiency, symmetry and a single monotonicity axiom — strong monotonicity — determine the Shapley value, with no additivity axiom at all. The result is widely cited as Young's axiomatization of the Shapley value, usually in the form with the marginality condition (7) that the paper states in its remarks.

Timeline:

• 1953: Shapley introduces the value, characterized by efficiency, symmetry, dummy and additivity (A value for n-person games).
• 1985: Young replaces dummy and additivity by strong monotonicity (Theorem 2), and remarks that the weaker marginality condition (7) suffices.
• Later work (e.g. Chun 1989, Pintér 2015) extends the characterization to other classes of games; this mission covers the 1985 statement only.

Setting

Fix $n$ and the player set $N = \{1, \dots, n\}$. A game is a function $v$ on the coalitions $S \subseteq N$ with $v(\emptyset) = 0$; superadditivity is not assumed. An allocation procedure is a map $\varphi$ assigning to each game $v$ a vector $\varphi(v) \in \mathbb{R}^N$ with $\sum_{i \in N} \varphi_i(v) = v(N)$ (efficiency).

The marginal contribution of player $i$ to coalition $S$ (Eq. (3)) is

$$v^i(S) = \begin{cases} v(S) - v(S \setminus \{i\}) & i \in S,\\ v(S \cup \{i\}) - v(S) & i \notin S,\end{cases}$$

defined for every $S$. The Shapley value is

$$\mathrm{Sh}_i(v) = \sum_{S \ni i} \frac{(|S|-1)!\,(|N|-|S|)!}{|N|!}\, v^i(S).$$

The axioms:

• Strong monotonicity (6): $v^i(S) \ge w^i(S)$ for all $S$ implies $\varphi_i(v) \ge \varphi_i(w)$.
• Marginality (7): $v^i(S) = w^i(S)$ for all $S$ implies $\varphi_i(v) = \varphi_i(w)$.
• Symmetry: $\varphi_{\pi i}(\pi v) = \varphi_i(v)$ for every permutation $\pi$ of $N$, where $(\pi v)(\pi S) = v(S)$.
• Dummy axiom (11): $v^i(S) = 0$ for all $S$ implies $\varphi_i(v) = 0$.

A primitive game $v_R$ ($\emptyset \ne R \subseteq N$) takes the value $1$ on coalitions containing $R$ and $0$ elsewhere.

Formalization targets

Goal: Theorem 2 (p. 70)

For every map $\varphi$ from games on $N$ to $\mathbb{R}^N$,

$$\varphi \text{ efficient, symmetric, strongly monotonic} \iff \varphi(v) = \mathrm{Sh}(v) \text{ for every game } v.$$

Both directions are part of the goal: the Shapley value has the three properties, and it is the only map that has them.

Milestones

1. The Shapley value is strongly monotonic (p. 70).
2. Strong monotonicity implies marginality, Eq. (7).
3. Symmetry, efficiency and (7) imply that dummy players get nothing, Eq. (8).
4. Every game is a combination of primitive games, $v = \sum_{\emptyset \ne R} c_R v_R$, Eq. (9) (quoted from Shapley).
5. On such an expression, $\mathrm{Sh}_i(v) = \sum_{R \ni i} c_R / |R|$ (p. 70).
6. A symmetric efficient procedure satisfying (7) gives $c_R/|R|$ to each member of $R$ and $0$ to the others on the game $c_R v_R$ (p. 70).
7. Deleting from (9) the terms whose coalition omits $i$ leaves $i$'s marginal contributions unchanged (p. 71, leading to Eq. (10)).
8. Under symmetry, players lying in every coalition of the expression receive equal amounts (p. 71).

Stronger forms (p. 71)

• Theorem 2 with (7) in place of strong monotonicity: efficiency, symmetry and marginality characterize the Shapley value.
• Shapley's dummy axiom (11) together with additivity implies (7).

Efficiency and symmetry of the Shapley value are supporting theorems of the existence half; the paper uses them without separate statement.

Significance

The result. Theorem 2 shows that additivity is not needed to single out the Shapley value: a player's payoff is pinned down by symmetry, efficiency, and the requirement that it respond monotonically to that player's own marginal contributions. This gives the Shapley value a justification that can be checked directly in applications — a division that improves its marginal contributions to every coalition is never penalized — and the marginality form (7) is the standard starting point for characterizations on restricted classes of games and for extensions to games with a variable player set.

The formalization. The theorem is proved and classical; no machine-checked proof of it is known to exist. The mission produces a checked proof of Young's characterization together with reusable infrastructure: marginal contributions, the unanimity-game basis of the space of games (a Möbius-inversion statement on the subset lattice), the Shapley value on unanimity games, and the Shapley value's efficiency, symmetry and monotonicity for the published ShapleyValue definition. These are the ingredients of most other axiomatizations of the Shapley value (Shapley 1953, Hart–Mas-Colell's potential) and are useful beyond this mission.

Difficulty

The existence half is a direct computation. The uniqueness half cannot proceed by linearity, since $\varphi$ is not assumed additive: knowing $\varphi$ on each primitive game $c_R v_R$ says nothing directly about $\varphi$ on their sum. The obvious idea — decompose $v$ into primitive games and add up — therefore fails. What must be controlled instead is how much of a game each player "sees" through the marginal-contribution vector alone, and how symmetry and efficiency distribute what remains. The formal proof also has to manage the dependence of the argument on a minimal-length expression (9) while keeping all comparisons inside the class of games with $v(\emptyset) = 0$.

Formalization scope

• Players are Fin n: the paper's player $k$ is the Lean index $k - 1$. The player set is fixed, and $\varphi$ is a single map Game n → Fin n → ℝ, as in the paper; no lower bound on $n$ is needed (at $n = 0$ both sides of the goal hold).
• Games are Game n := {v : Finset (Fin n) → ℝ // v ∅ = 0}. The normalisation is essential: on arbitrary set functions a constant game $c \ne 0$ would receive $c/n$ per player from every efficient symmetric procedure, but $0$ from the Shapley formula, and Theorem 2 would be false.
• The Shapley value is the published definition Supermodularity.Cooperative.ShapleyValue, written as a sum over $T = S \setminus \{i\}$ with weight $|T|!\,(n-|T|-1)!/n!$; it agrees term by term with the formula above.
• Symmetry. The paper prints the permuted game as $\pi v(S) = v(\pi S)$. Read literally together with $\varphi_{\pi i}(\pi v) = \varphi_i(v)$, the Shapley value itself would fail symmetry for a 3-cycle, and Theorem 2 would be false. The formalization uses the standard reading $(\pi v)(\pi S) = v(S)$, i.e. $(\pi v)(T) = v(\pi^{-1} T)$. The two readings coincide for transpositions, the only permutations the paper's proof uses.
• Strong monotonicity quantifies over all coalitions $S$, including those not containing $i$, as in (3); this is equivalent to quantifying over $S \ni i$ only.
• The dummy axiom and additivity appear only in the stronger forms, never as hypotheses of the goal; a formalization that assumed them, or that defined any axiom through the Shapley formula, would trivialize Theorem 2.
• The paper's "index" of a game (minimum number of terms in (9)) is a proof device; milestones quantify over expressions directly.
• Not included: the variant of the proof within the class of superadditive games (p. 71, a sketch with a changed domain), and the example $\varphi_i(v) = [v^i(N)]^2$ (p. 72), whose printed claim of strong monotonicity fails when marginal contributions are negative.

Contributions welcome: proofs of the milestones in any order, general lemmas on unanimity-game expansions over Finset powersets, and alternative proofs of the uniqueness half.

Selected references

• H. P. Young, Monotonic Solutions of Cooperative Games, International Journal of Game Theory 14 (1985), 65–72. https://doi.org/10.1007/BF01769885
• L. S. Shapley, A value for n-person games, in: Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, 307–317. https://doi.org/10.1515/9781400881970-018
• Y. Chun, A new axiomatization of the Shapley value, Games and Economic Behavior 1 (1989), 119–130. https://doi.org/10.1016/0899-8256(89)90014-6
• M. Pintér, Young's axiomatization of the Shapley value: a new proof, Annals of Operations Research 235 (2015), 665–673. https://doi.org/10.1007/s10479-015-1976-2
• S. Hart, A. Mas-Colell, Potential, value, and consistency, Econometrica 57 (1989), 589–614. https://doi.org/10.2307/1911054

Motivation

Walras (1874) described an economy as a system of simultaneous equations, one per market, and argued that a set of prices clearing all markets exists because the number of equations equals the number of unknowns. Counting equations proves nothing, and the question of whether competitive equilibrium exists at all remained open for eighty years. Wald (1935–36) proved existence in special production models under restrictive assumptions on demand. In 1954 Kenneth Arrow and Gérard Debreu gave the first existence proof for a general model with production, many consumers, convex technologies and preferences given by utility indicators (Econometrica 22 (1954) 265–290); McKenzie published an independent proof for a trade model in the same year (Econometrica 22 (1954) 147–161). The resulting Arrow–Debreu model is the reference model of general equilibrium theory and the starting point of market-equilibrium problems in operations research and algorithmic game theory.

The paper proves two existence theorems. This mission is the first, Theorem I, whose key assumption is that every consumer initially holds a positive amount of every commodity. A second mission treats Theorem II, which replaces that assumption by a weaker condition on labour supply.

Setting

There are $l \ge 1$ commodities; a commodity vector is an element of $\mathbb R^l$, compared componentwise ($x \geqq y$ means $x_h \ge y_h$ for all $h$; $x > y$ means $x_h > y_h$ for all $h$). The inner product is $p\cdot x = \sum_h p_h x_h$.

• Producers $j = 1, \dots, n$ each have a production set $Y_j \subseteq \mathbb R^l$ (outputs positive, inputs negative). The aggregate production set is $Y = \sum_j Y_j$.
• Consumers $i = 1, \dots, m$ each have a consumption set $X_i \subseteq \mathbb R^l$, a utility indicator $u_i$ on $X_i$, initial holdings $\zeta_i \in \mathbb R^l$, and a share $\alpha_{ij}$ of the profit of producer $j$.

Assumptions I–IV are: (I.a) each $Y_j$ is closed, convex and contains $0$; (I.b) $Y \cap \Omega = \{0\}$ with $\Omega = \{x \geqq 0\}$; (I.c) $Y \cap (-Y) = \{0\}$; (II) each $X_i$ is closed, convex and bounded from below; (III.a) $u_i$ is continuous on $X_i$; (III.b) no $x_i \in X_i$ is a satiation point; (III.c) if $u_i(x_i) > u_i(x_i')$ and $0 < t < 1$ then $u_i[t x_i + (1-t) x_i'] > u_i(x_i')$; (IV.a) some $x_i \in X_i$ satisfies $x_i < \zeta_i$; (IV.b) $\alpha_{ij} \ge 0$ and $\sum_i \alpha_{ij} = 1$.

A competitive equilibrium is a tuple $(x_1^*, \dots, x_m^*, y_1^*, \dots, y_n^*, p^*)$ such that

1. each $y_j^*$ maximizes $p^*\cdot y_j$ over $Y_j$;
2. each $x_i^*$ maximizes $u_i$ over $\{x_i \in X_i : p^*\cdot x_i \leqq p^*\cdot\zeta_i + \sum_j \alpha_{ij}\, p^*\cdot y_j^*\}$;
3. $p^* \in P = \{p \geqq 0 : \sum_h p_h = 1\}$;
4. $z^* = \sum_i x_i^* - \sum_j y_j^* - \sum_i \zeta_i$ satisfies $z^* \leqq 0$ and $p^*\cdot z^* = 0$.

An abstract economy (§2) is a game in which each player's feasible set $A_\iota(\bar a_\iota)$ depends on the other players' actions $\bar a_\iota$; an equilibrium point is a profile at which every player maximizes its pay-off over its feasible set. The proof builds an abstract economy $E$ with the consumers, the producers and a fictitious market participant who chooses $p \in P$ and receives $p\cdot z$, and a truncated version $\tilde E$ in which all choices are restricted to a large cube $C$.

Formalization targets

Goal: Theorem I

$$\text{Assumptions I–IV} \implies \exists\, (x^*, y^*, p^*) \text{ satisfying Conditions 1–4.}$$

The statement fixes no constants; its only added hypothesis is $l \ge 1$.

Milestones

In the order of the paper's argument:

1. §1.3.1: under II, III.a and III.c, each $u_i$ is quasi-concave on $X_i$.
2. §1.4.2 (1): Condition 2 together with II, III.b and III.c gives $p^*\cdot x_i^* = p^*\cdot\zeta_i + \sum_j \alpha_{ij}\, p^*\cdot y_j^*$.
3. Lemma 2.5: an abstract economy with compact convex action sets, continuous pay-offs that are quasi-concave in the player's own action, and continuous constraint correspondences with closed graphs and nonempty convex values has an equilibrium point.
4. §3.1.2 (2): at an equilibrium point of $E$, Condition 2 holds.
5. §3.2: every equilibrium point of $E$ is a competitive equilibrium.
6. §3.3.1 (7) and §3.3.2 (2): the attainable sets $\hat Y_j$ and $\hat X_i$ (choices compatible with $z \leqq 0$) are bounded.
7. Remark §3.3.5: if $p\cdot\zeta_i > \min_{\tilde X_i} p\cdot x_i$, the truncated budget correspondence $\tilde A_i$ is continuous at that point.
8. §3.4.0: for a cube $C$ containing every $\hat X_i$ and $\hat Y_j$ in its interior, $\tilde E$ has an equilibrium point.
9. §3.4.1: every equilibrium point of $\tilde E$ is an equilibrium point of $E$.

Significance

Theorem I shows that the competitive model is consistent: under convexity, continuity, non-satiation and survival assumptions, prices exist at which profit maximization, utility maximization and market clearing hold simultaneously. The welfare theorems, comparative statics, and algorithms that compute equilibria (Scarf's method, market-equilibrium algorithms) presuppose it. Lemma 2.5, Debreu's social-equilibrium theorem (PNAS 38 (1952) 886–893), is also used on its own for generalized Nash equilibrium problems with coupled constraints.

The theorem is proved and textbook material (Debreu, Theory of Value, 1959). To the best of the catalog search, no proof assistant library contains Theorem I, Lemma 2.5, or a Kakutani-type fixed-point theorem for correspondences; on this platform the only related results are Brouwer's fixed-point theorem (AGT.brouwer_fixed_point, proved) and Nash's theorem for finite games (AGT.nash_existence), a special case of Lemma 2.5 with constant constraint sets. The mission produces a machine-checked proof of the paper's argument and, along the way, reusable statements about abstract economies and their equilibria.

Difficulty

The central difficulty is Lemma 2.5. The paper does not prove it but cites Debreu (1952), whose proof uses the Eilenberg–Montgomery fixed-point theorem for correspondences with contractible values. Brouwer's theorem alone does not suffice: the best-response correspondence of an abstract economy is set-valued, and its closed graph must be established from the continuity of the feasible-set correspondences, which is a maximum-theorem argument that Mathlib does not contain. A Kakutani-type fixed-point theorem, or an approximation argument reducing to Brouwer, is needed.

A second difficulty is non-compactness. The economy $E$ has unbounded action sets, so the Lemma does not apply to it directly. The boundedness of the attainable sets (§3.3.1) is an asymptotic argument using the irreversibility and no-free-production assumptions I.b and I.c, and the passage from $\tilde E$ back to $E$ (§3.4.1) needs the attainable choices to lie in the interior of the cube, so that local optimality implies global optimality through III.c. A fixed-point argument on an excess-demand function does not apply directly: demand need not be single-valued or even defined at every price.

Formalization scope

Commodity space is Fin l → ℝ with its componentwise order; the paper's strict vector inequality is written coordinatewise (∀ h, x h < ζ i h), not with the order-theoretic strict inequality on functions. Consumers are Fin m, producers Fin n, and the players of $E$ are Fin m ⊕ Fin n ⊕ Unit. Utilities are total functions, and every assumption on them quantifies over $X_i$ only. "Maximizes" is always written as membership plus an inequality against every feasible alternative, never through a supremum. Continuity of a constraint correspondence is the paper's sequential definition (§2.4), a lower-hemicontinuity condition, required at every point of the other players' action space; convergence is asked only in the other players' coordinates.

Two hypotheses are made explicit because the formal statements would otherwise be false: Theorem I and §3.4.0 assume $l \ge 1$ (for $l = 0$ the price simplex is empty), and Lemma 2.5 assumes every action set nonempty (otherwise, with two or more players and all action sets empty, every hypothesis holds vacuously). The Remark of §3.3.5 carries, as a hypothesis, the nonemptiness of $\tilde A_i$ established in §3.3.4. A formalization that makes Theorem I trivial, for instance by taking $P$ to contain $0$, by reading IV.a with the order-theoretic strict inequality, or by allowing an empty commodity space, is ruled out by these definitions.

A complete development needs: Kakutani's fixed-point theorem (or a Brouwer-based substitute) for compact convex subsets of $\mathbb R^l$; Berge's maximum theorem for the best-response correspondence; the asymptotic-cone argument for §3.3.1; and elementary convex analysis for the budget sets. The abstract-economy definitions and Lemma 2.5 are reusable beyond this mission, including by the Theorem II mission. Contributions of any of these components are welcome, as are alternative proofs of Lemma 2.5.

Selected references

• K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3) (1954) 265–290. https://doi.org/10.2307/1907353
• G. Debreu, A Social Equilibrium Existence Theorem, Proceedings of the National Academy of Sciences 38(10) (1952) 886–893. https://doi.org/10.1073/pnas.38.10.886
• L. W. McKenzie, On Equilibrium in Graham's Model of World Trade and Other Competitive Systems, Econometrica 22(2) (1954) 147–161. https://doi.org/10.2307/1907539
• J. Nash, Equilibrium Points in n-Person Games, Proceedings of the National Academy of Sciences 36(1) (1950) 48–49. https://doi.org/10.1073/pnas.36.1.48
• S. Kakutani, A Generalization of Brouwer's Fixed Point Theorem, Duke Mathematical Journal 8(3) (1941) 457–459. https://doi.org/10.1215/S0012-7094-41-00838-4
• G. Debreu, Theory of Value: An Axiomatic Analysis of Economic Equilibrium, Wiley, 1959 (Cowles Foundation Monograph 17).